    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.TypeChecking.Quote where

    import Control.Monad

    import Data.Maybe (fromMaybe)
    import qualified Data.Text as T

    import qualified Agda.Syntax.Abstract as A
    import Agda.Syntax.Common
    import Agda.Syntax.Internal as I
    import Agda.Syntax.Internal.Pattern ( hasDefP )
    import Agda.Syntax.Literal
    import Agda.Syntax.TopLevelModuleName

    import Agda.TypeChecking.CompiledClause
    import Agda.TypeChecking.Level
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Primitive.Base
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Substitute

    import Agda.Utils.Impossible
    import Agda.Utils.Functor
    import Agda.Utils.List
    import Agda.Utils.List1 ( pattern (:|) )
    import Agda.Utils.List2 ( pattern List2 )
    import Agda.Utils.Size
    import qualified Agda.Utils.Maybe.Strict as Strict

    -- | Parse @quote@.
    quotedName :: (MonadTCError m, MonadAbsToCon m) => A.Expr -> m QName
    quotedName :: forall (m :: * -> *).
    (MonadTCError m, MonadAbsToCon m) =>
    Expr -> m QName
    quotedName = \case
      -- Andreas, 2024-09-27, issue #7514
      -- Is it intended to be able to quote Set but not Set1?
      A.Def' QName
    x Suffix
    NoSuffix -> QName -> m QName
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return QName
    x
      A.Macro QName
    x         -> QName -> m QName
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return QName
    x
      A.Proj ProjOrigin
    _o AmbiguousQName
    p       -> AmbiguousQName -> m QName
    forall {m :: * -> *}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
    AmbiguousQName -> m QName
    unambiguous AmbiguousQName
    p
      A.Con AmbiguousQName
    c           -> AmbiguousQName -> m QName
    forall {m :: * -> *}.
    (MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
    AmbiguousQName -> m QName
    unambiguous AmbiguousQName
    c
      A.ScopedExpr ScopeInfo
    _ Expr
    e  -> Expr -> m QName
    forall (m :: * -> *).
    (MonadTCError m, MonadAbsToCon m) =>
    Expr -> m QName
    quotedName Expr
    e
      Expr
    e -> TypeError -> m QName
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m QName) -> TypeError -> m QName
    forall a b. (a -> b) -> a -> b
    $ CannotQuote -> TypeError
    CannotQuote (CannotQuote -> TypeError) -> CannotQuote -> TypeError
    forall a b. (a -> b) -> a -> b
    $ Expr -> CannotQuote
    CannotQuoteExpression Expr
    e
      where
        unambiguous :: AmbiguousQName -> m QName
    unambiguous (AmbQ (QName
    x :| [QName]
    xs)) = case [QName]
    xs of
          []   -> QName -> m QName
    forall a. a -> m a
    forall (m :: * -> *) a. Monad m => a -> m a
    return QName
    x
          QName
    y:[QName]
    ys -> TypeError -> m QName
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    TypeError -> m a
    typeError (TypeError -> m QName) -> TypeError -> m QName
    forall a b. (a -> b) -> a -> b
    $ CannotQuote -> TypeError
    CannotQuote (CannotQuote -> TypeError) -> CannotQuote -> TypeError
    forall a b. (a -> b) -> a -> b
    $ List2 QName -> CannotQuote
    CannotQuoteAmbiguous (List2 QName -> CannotQuote) -> List2 QName -> CannotQuote
    forall a b. (a -> b) -> a -> b
    $ QName -> QName -> [QName] -> List2 QName
    forall a. a -> a -> [a] -> List2 a
    List2 QName
    x QName
    y [QName]
    ys

    data QuotingKit = QuotingKit
      { QuotingKit -> Term -> ReduceM Term
    quoteTermWithKit   :: Term       -> ReduceM Term
      , QuotingKit -> Type -> ReduceM Term
    quoteTypeWithKit   :: Type       -> ReduceM Term
      , QuotingKit -> Dom Type -> ReduceM Term
    quoteDomWithKit    :: Dom Type   -> ReduceM Term
      , QuotingKit -> Definition -> ReduceM Term
    quoteDefnWithKit   :: Definition -> ReduceM Term
      , QuotingKit -> forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
    quoteListWithKit   :: forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
      }

    quotingKit :: TCM QuotingKit
    quotingKit :: TCM QuotingKit
    quotingKit = do
      currentModule   <- TopLevelModuleName
    -> Maybe TopLevelModuleName -> TopLevelModuleName
    forall a. a -> Maybe a -> a
    fromMaybe TopLevelModuleName
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe TopLevelModuleName -> TopLevelModuleName)
    -> TCMT IO (Maybe TopLevelModuleName) -> TCMT IO TopLevelModuleName
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> TCMT IO (Maybe TopLevelModuleName)
    forall (m :: * -> *).
    (MonadTCEnv m, ReadTCState m) =>
    m (Maybe TopLevelModuleName)
    currentTopLevelModule
      hidden          <- primHidden
      instanceH       <- primInstance
      visible         <- primVisible
      relevant        <- primRelevant
      irrelevant      <- primIrrelevant
      quantity0       <- primQuantity0
      quantityω       <- primQuantityω
      modality        <- primModalityConstructor
      nil             <- primNil
      cons            <- primCons
      abs             <- primAbsAbs
      arg             <- primArgArg
      arginfo         <- primArgArgInfo
      var             <- primAgdaTermVar
      lam             <- primAgdaTermLam
      extlam          <- primAgdaTermExtLam
      def             <- primAgdaTermDef
      con             <- primAgdaTermCon
      pi              <- primAgdaTermPi
      sort            <- primAgdaTermSort
      meta            <- primAgdaTermMeta
      lit             <- primAgdaTermLit
      litNat          <- primAgdaLitNat
      litWord64       <- primAgdaLitNat
      litFloat        <- primAgdaLitFloat
      litChar         <- primAgdaLitChar
      litString       <- primAgdaLitString
      litQName        <- primAgdaLitQName
      litMeta         <- primAgdaLitMeta
      normalClause    <- primAgdaClauseClause
      absurdClause    <- primAgdaClauseAbsurd
      varP            <- primAgdaPatVar
      conP            <- primAgdaPatCon
      dotP            <- primAgdaPatDot
      litP            <- primAgdaPatLit
      projP           <- primAgdaPatProj
      absurdP         <- primAgdaPatAbsurd
      set             <- primAgdaSortSet
      setLit          <- primAgdaSortLit
      prop            <- primAgdaSortProp
      propLit         <- primAgdaSortPropLit
      inf             <- primAgdaSortInf
      unsupportedSort <- primAgdaSortUnsupported
      sucLevel        <- primLevelSuc
      lub             <- primLevelMax
      lkit            <- requireLevels
      Con z _ _       <- primZero
      Con s _ _       <- primSuc
      unsupported     <- primAgdaTermUnsupported

      agdaDefinitionFunDef          <- primAgdaDefinitionFunDef
      agdaDefinitionDataDef         <- primAgdaDefinitionDataDef
      agdaDefinitionRecordDef       <- primAgdaDefinitionRecordDef
      agdaDefinitionPostulate       <- primAgdaDefinitionPostulate
      agdaDefinitionPrimitive       <- primAgdaDefinitionPrimitive
      agdaDefinitionDataConstructor <- primAgdaDefinitionDataConstructor

      let (@@) :: Apply a => ReduceM a -> ReduceM Term -> ReduceM a
          ReduceM a
    t @@ ReduceM Term
    u = a -> Args -> a
    forall t. Apply t => t -> Args -> t
    apply (a -> Args -> a) -> ReduceM a -> ReduceM (Args -> a)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReduceM a
    t ReduceM (Args -> a) -> ReduceM Args -> ReduceM a
    forall a b. ReduceM (a -> b) -> ReduceM a -> ReduceM b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> ((Arg Term -> Args -> Args
    forall a. a -> [a] -> [a]
    :[]) (Arg Term -> Args) -> (Term -> Arg Term) -> Term -> Args
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Term -> Arg Term
    forall a. a -> Arg a
    defaultArg (Term -> Args) -> ReduceM Term -> ReduceM Args
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReduceM Term
    u)

          (!@) :: Apply a => a -> ReduceM Term -> ReduceM a
          a
    t !@ ReduceM Term
    u = a -> ReduceM a
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    t ReduceM a -> ReduceM Term -> ReduceM a
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ ReduceM Term
    u

          (!@!) :: Apply a => a -> Term -> ReduceM a
          a
    t !@! Term
    u = a -> ReduceM a
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure a
    t ReduceM a -> ReduceM Term -> ReduceM a
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    u

          quoteHiding :: Hiding -> ReduceM Term
          quoteHiding Hiding
    Hidden     = Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    hidden
          quoteHiding Instance{} = Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    instanceH
          quoteHiding Hiding
    NotHidden  = Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    visible

          quoteRelevance :: Relevance -> ReduceM Term
          quoteRelevance = \case
            Relevant        {} -> Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    relevant
            Irrelevant      {} -> Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    irrelevant
            ShapeIrrelevant {} -> Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    relevant

          quoteQuantity :: Quantity -> ReduceM Term
          quoteQuantity (Quantity0 Q0Origin
    _) = Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    quantity0
          quoteQuantity (Quantity1 Q1Origin
    _) = ReduceM Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          quoteQuantity (Quantityω QωOrigin
    _) = Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    quantityω

          -- TODO: quote Annotation
          quoteModality :: Modality -> ReduceM Term
          quoteModality Modality
    m =
            Term
    modality Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@ Relevance -> ReduceM Term
    quoteRelevance (Modality -> Relevance
    forall a. LensRelevance a => a -> Relevance
    getRelevance Modality
    m)
                     ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ Quantity -> ReduceM Term
    quoteQuantity  (Modality -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity  Modality
    m)

          quoteArgInfo :: ArgInfo -> ReduceM Term
          quoteArgInfo (ArgInfo Hiding
    h Modality
    m Origin
    _ FreeVariables
    _ Annotation
    _) =
            Term
    arginfo Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@ Hiding -> ReduceM Term
    quoteHiding Hiding
    h
                    ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ Modality -> ReduceM Term
    quoteModality Modality
    m

          quoteLit :: Literal -> ReduceM Term
          quoteLit l :: Literal
    l@LitNat{}    = Term
    litNat    Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! Literal -> Term
    Lit Literal
    l
          quoteLit l :: Literal
    l@LitWord64{} = Term
    litWord64 Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! Literal -> Term
    Lit Literal
    l
          quoteLit l :: Literal
    l@LitFloat{}  = Term
    litFloat  Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! Literal -> Term
    Lit Literal
    l
          quoteLit l :: Literal
    l@LitChar{}   = Term
    litChar   Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! Literal -> Term
    Lit Literal
    l
          quoteLit l :: Literal
    l@LitString{} = Term
    litString Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! Literal -> Term
    Lit Literal
    l
          quoteLit l :: Literal
    l@LitQName{}  = Term
    litQName  Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! Literal -> Term
    Lit Literal
    l
          quoteLit l :: Literal
    l@LitMeta {}  = Term
    litMeta   Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! Literal -> Term
    Lit Literal
    l

          -- We keep no ranges in the quoted term, so the equality on terms
          -- is only on the structure.
          quoteSortLevelTerm :: Term -> Term -> Level -> ReduceM Term
          quoteSortLevelTerm Term
    fromLit Term
    fromLevel (ClosedLevel Integer
    n) = Term
    fromLit Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! Literal -> Term
    Lit (Integer -> Literal
    LitNat Integer
    n)
          quoteSortLevelTerm Term
    fromLit Term
    fromLevel Level
    l               = Term
    fromLevel Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@ Term -> ReduceM Term
    quoteTerm (LevelKit -> Level -> Term
    unlevelWithKit LevelKit
    lkit Level
    l)

          quoteSort :: Sort -> ReduceM Term
          quoteSort (Type Level
    t) = Term -> Term -> Level -> ReduceM Term
    quoteSortLevelTerm Term
    setLit Term
    set Level
    t
          quoteSort (Prop Level
    t) = Term -> Term -> Level -> ReduceM Term
    quoteSortLevelTerm Term
    propLit Term
    prop Level
    t
          quoteSort (Inf Univ
    u Integer
    n) = case Univ
    u of
            Univ
    UType -> Term
    inf Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! Literal -> Term
    Lit (Integer -> Literal
    LitNat Integer
    n)
            Univ
    UProp -> Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupportedSort
            Univ
    USSet -> Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupportedSort
          quoteSort SSet{}   = Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupportedSort
          quoteSort Sort
    SizeUniv = Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupportedSort
          quoteSort Sort
    LockUniv = Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupportedSort
          quoteSort Sort
    LevelUniv = Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupportedSort
          quoteSort Sort
    IntervalUniv = Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupportedSort
          quoteSort PiSort{} = Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupportedSort
          quoteSort FunSort{} = Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupportedSort
          quoteSort UnivSort{}   = Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupportedSort
          quoteSort (MetaS MetaId
    x Elims
    es) = Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupportedSort
          quoteSort (DefS QName
    d Elims
    es)  = Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupportedSort
          quoteSort (DummyS String
    s)   =String -> ReduceM Term
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    String -> m a
    __IMPOSSIBLE_VERBOSE__ String
    s

          quoteType :: Type -> ReduceM Term
          quoteType (El Sort
    _ Term
    t) = Term -> ReduceM Term
    quoteTerm Term
    t

          quoteQName :: QName -> ReduceM Term
          quoteQName QName
    x = Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> ReduceM Term) -> Term -> ReduceM Term
    forall a b. (a -> b) -> a -> b
    $ Literal -> Term
    Lit (Literal -> Term) -> Literal -> Term
    forall a b. (a -> b) -> a -> b
    $ QName -> Literal
    LitQName QName
    x

          quotePats :: [NamedArg DeBruijnPattern] -> ReduceM Term
          quotePats [NamedArg DeBruijnPattern]
    ps = [ReduceM Term] -> ReduceM Term
    list ([ReduceM Term] -> ReduceM Term) -> [ReduceM Term] -> ReduceM Term
    forall a b. (a -> b) -> a -> b
    $ (NamedArg DeBruijnPattern -> ReduceM Term)
    -> [NamedArg DeBruijnPattern] -> [ReduceM Term]
    forall a b. (a -> b) -> [a] -> [b]
    map ((DeBruijnPattern -> ReduceM Term)
    -> Arg DeBruijnPattern -> ReduceM Term
    forall a. (a -> ReduceM Term) -> Arg a -> ReduceM Term
    quoteArg DeBruijnPattern -> ReduceM Term
    quotePat (Arg DeBruijnPattern -> ReduceM Term)
    -> (NamedArg DeBruijnPattern -> Arg DeBruijnPattern)
    -> NamedArg DeBruijnPattern
    -> ReduceM Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Named NamedName DeBruijnPattern -> DeBruijnPattern)
    -> NamedArg DeBruijnPattern -> Arg DeBruijnPattern
    forall a b. (a -> b) -> Arg a -> Arg b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Named NamedName DeBruijnPattern -> DeBruijnPattern
    forall name a. Named name a -> a
    namedThing) [NamedArg DeBruijnPattern]
    ps

          quotePat :: DeBruijnPattern -> ReduceM Term
          quotePat p :: DeBruijnPattern
    p@(VarP PatternInfo
    _ DBPatVar
    x)
           | DeBruijnPattern -> Maybe PatOrigin
    forall x. Pattern' x -> Maybe PatOrigin
    patternOrigin DeBruijnPattern
    p Maybe PatOrigin -> Maybe PatOrigin -> Bool
    forall a. Eq a => a -> a -> Bool
    == PatOrigin -> Maybe PatOrigin
    forall a. a -> Maybe a
    Just PatOrigin
    PatOAbsurd = Term
    absurdP Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! Integer -> Term
    quoteNat (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (Int -> Integer) -> Int -> Integer
    forall a b. (a -> b) -> a -> b
    $ DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x)
          quotePat (VarP PatternInfo
    o DBPatVar
    x)        = Term
    varP Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! Integer -> Term
    quoteNat (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (Int -> Integer) -> Int -> Integer
    forall a b. (a -> b) -> a -> b
    $ DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x)
          quotePat (DotP PatternInfo
    _ Term
    t)        = Term
    dotP Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@ Term -> ReduceM Term
    quoteTerm Term
    t
          quotePat (ConP ConHead
    c ConPatternInfo
    _ [NamedArg DeBruijnPattern]
    ps)     = Term
    conP Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@ QName -> ReduceM Term
    quoteQName (ConHead -> QName
    conName ConHead
    c) ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ [NamedArg DeBruijnPattern] -> ReduceM Term
    quotePats [NamedArg DeBruijnPattern]
    ps
          quotePat (LitP PatternInfo
    _ Literal
    l)        = Term
    litP Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@ Literal -> ReduceM Term
    quoteLit Literal
    l
          quotePat (ProjP ProjOrigin
    _ QName
    x)       = Term
    projP Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@ QName -> ReduceM Term
    quoteQName QName
    x
          -- #4763: quote IApply co/patterns as though they were variables
          quotePat (IApplyP PatternInfo
    _ Term
    _ Term
    _ DBPatVar
    x) = Term
    varP Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! Integer -> Term
    quoteNat (Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger (Int -> Integer) -> Int -> Integer
    forall a b. (a -> b) -> a -> b
    $ DBPatVar -> Int
    dbPatVarIndex DBPatVar
    x)
          quotePat DefP{}            = Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupported

          quoteClause :: Either a Projection -> Clause -> ReduceM Term
          quoteClause Either a Projection
    proj cl :: Clause
    cl@Clause{ clauseTel :: Clause -> Telescope
    clauseTel = Telescope
    tel, namedClausePats :: Clause -> [NamedArg DeBruijnPattern]
    namedClausePats = [NamedArg DeBruijnPattern]
    ps, clauseBody :: Clause -> Maybe Term
    clauseBody = Maybe Term
    body} =
            case Maybe Term
    body of
              Maybe Term
    Nothing -> Term
    absurdClause Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@ Telescope -> ReduceM Term
    quoteTelescope Telescope
    tel ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ [NamedArg DeBruijnPattern] -> ReduceM Term
    quotePats [NamedArg DeBruijnPattern]
    ps'
              Just Term
    b  -> Term
    normalClause Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@ Telescope -> ReduceM Term
    quoteTelescope Telescope
    tel ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ [NamedArg DeBruijnPattern] -> ReduceM Term
    quotePats [NamedArg DeBruijnPattern]
    ps' ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ Term -> ReduceM Term
    quoteTerm Term
    b
            where
              -- #5128: restore dropped parameters if projection-like
              ps' :: [NamedArg DeBruijnPattern]
    ps' =
                case Either a Projection
    proj of
                  Left a
    _ -> [NamedArg DeBruijnPattern]
    ps
                  Right Projection
    p  -> [NamedArg DeBruijnPattern]
    pars [NamedArg DeBruijnPattern]
    -> [NamedArg DeBruijnPattern] -> [NamedArg DeBruijnPattern]
    forall a. [a] -> [a] -> [a]
    ++ [NamedArg DeBruijnPattern]
    ps
                    where
                      n :: Int
    n    = Projection -> Int
    projIndex Projection
    p Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1
                      pars :: [NamedArg DeBruijnPattern]
    pars = ((Int, Dom' Term (String, Type)) -> NamedArg DeBruijnPattern)
    -> [(Int, Dom' Term (String, Type))] -> [NamedArg DeBruijnPattern]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, Dom' Term (String, Type)) -> NamedArg DeBruijnPattern
    forall {t} {b} {name}.
    (Int, Dom' t (String, b)) -> Arg (Named name DeBruijnPattern)
    toVar ([(Int, Dom' Term (String, Type))] -> [NamedArg DeBruijnPattern])
    -> [(Int, Dom' Term (String, Type))] -> [NamedArg DeBruijnPattern]
    forall a b. (a -> b) -> a -> b
    $ Int
    -> [(Int, Dom' Term (String, Type))]
    -> [(Int, Dom' Term (String, Type))]
    forall a. Int -> [a] -> [a]
    take Int
    n ([(Int, Dom' Term (String, Type))]
     -> [(Int, Dom' Term (String, Type))])
    -> [(Int, Dom' Term (String, Type))]
    -> [(Int, Dom' Term (String, Type))]
    forall a b. (a -> b) -> a -> b
    $ [Int]
    -> [Dom' Term (String, Type)] -> [(Int, Dom' Term (String, Type))]
    forall a b. [a] -> [b] -> [(a, b)]
    zip (Int -> [Int]
    forall a. Integral a => a -> [a]
    downFrom (Int -> [Int]) -> Int -> [Int]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> Int
    forall a. Sized a => a -> Int
    size Telescope
    tel) (Telescope -> [Dom' Term (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    tel)
                      toVar :: (Int, Dom' t (String, b)) -> Arg (Named name DeBruijnPattern)
    toVar (Int
    i, Dom' t (String, b)
    d) = Dom' t (String, b) -> Arg (String, b)
    forall t a. Dom' t a -> Arg a
    argFromDom Dom' t (String, b)
    d Arg (String, b)
    -> ((String, b) -> Named name DeBruijnPattern)
    -> Arg (Named name DeBruijnPattern)
    forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
    <&> \ (String
    x, b
    _) -> DeBruijnPattern -> Named name DeBruijnPattern
    forall a name. a -> Named name a
    unnamed (DeBruijnPattern -> Named name DeBruijnPattern)
    -> DeBruijnPattern -> Named name DeBruijnPattern
    forall a b. (a -> b) -> a -> b
    $ DBPatVar -> DeBruijnPattern
    forall a. a -> Pattern' a
    I.varP (String -> Int -> DBPatVar
    DBPatVar String
    x Int
    i)

          quoteTelescope :: Telescope -> ReduceM Term
          quoteTelescope Telescope
    tel = (Dom' Term (String, Type) -> ReduceM Term)
    -> [Dom' Term (String, Type)] -> ReduceM Term
    forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
    quoteList Dom' Term (String, Type) -> ReduceM Term
    quoteTelEntry ([Dom' Term (String, Type)] -> ReduceM Term)
    -> [Dom' Term (String, Type)] -> ReduceM Term
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom' Term (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    tel

          quoteTelEntry :: Dom (ArgName, Type) -> ReduceM Term
          quoteTelEntry dom :: Dom' Term (String, Type)
    dom@Dom{ unDom :: forall t e. Dom' t e -> e
    unDom = (String
    x , Type
    t) } = do
            SigmaKit{..} <- SigmaKit -> Maybe SigmaKit -> SigmaKit
    forall a. a -> Maybe a -> a
    fromMaybe SigmaKit
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe SigmaKit -> SigmaKit)
    -> ReduceM (Maybe SigmaKit) -> ReduceM SigmaKit
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ReduceM (Maybe SigmaKit)
    forall (m :: * -> *).
    (HasBuiltins m, HasConstInfo m) =>
    m (Maybe SigmaKit)
    getSigmaKit
            Con sigmaCon ConOSystem [] !@! quoteString x @@ quoteDom quoteType (fmap snd dom)

          list :: [ReduceM Term] -> ReduceM Term
          list = (ReduceM Term -> ReduceM Term -> ReduceM Term)
    -> ReduceM Term -> [ReduceM Term] -> ReduceM Term
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (\ ReduceM Term
    a ReduceM Term
    as -> Term
    cons Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@ ReduceM Term
    a ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ ReduceM Term
    as) (Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    nil)

          quoteList :: (a -> ReduceM Term) -> [a] -> ReduceM Term
          quoteList a -> ReduceM Term
    q [a]
    xs = [ReduceM Term] -> ReduceM Term
    list ((a -> ReduceM Term) -> [a] -> [ReduceM Term]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> ReduceM Term
    q [a]
    xs)

          quoteDom :: (a -> ReduceM Term) -> Dom a -> ReduceM Term
          quoteDom a -> ReduceM Term
    q Dom{domInfo :: forall t e. Dom' t e -> ArgInfo
    domInfo = ArgInfo
    info, unDom :: forall t e. Dom' t e -> e
    unDom = a
    t} = Term
    arg Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@ ArgInfo -> ReduceM Term
    quoteArgInfo ArgInfo
    info ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ a -> ReduceM Term
    q a
    t

          quoteAbs :: Subst a => (a -> ReduceM Term) -> Abs a -> ReduceM Term
          quoteAbs a -> ReduceM Term
    q (Abs String
    s a
    t)   = Term
    abs Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! String -> Term
    quoteString String
    s ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ a -> ReduceM Term
    q a
    t
          quoteAbs a -> ReduceM Term
    q (NoAbs String
    s a
    t) = Term
    abs Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! String -> Term
    quoteString String
    s ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ a -> ReduceM Term
    q (Int -> a -> a
    forall a. Subst a => Int -> a -> a
    raise Int
    1 a
    t)

          quoteArg :: (a -> ReduceM Term) -> Arg a -> ReduceM Term
          quoteArg a -> ReduceM Term
    q (Arg ArgInfo
    info a
    t) = Term
    arg Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@ ArgInfo -> ReduceM Term
    quoteArgInfo ArgInfo
    info ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ a -> ReduceM Term
    q a
    t

          quoteArgs :: Args -> ReduceM Term
          quoteArgs Args
    ts = [ReduceM Term] -> ReduceM Term
    list ((Arg Term -> ReduceM Term) -> Args -> [ReduceM Term]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Term -> ReduceM Term) -> Arg Term -> ReduceM Term
    forall a. (a -> ReduceM Term) -> Arg a -> ReduceM Term
    quoteArg Term -> ReduceM Term
    quoteTerm) Args
    ts)

          -- has the clause been generated (in particular by --cubical)?
          -- TODO: have an explicit clause origin field?
          generatedClause :: Clause -> Bool
          generatedClause Clause
    cl = [NamedArg DeBruijnPattern] -> Bool
    hasDefP (Clause -> [NamedArg DeBruijnPattern]
    namedClausePats Clause
    cl)

          quoteTerm :: Term -> ReduceM Term
          quoteTerm Term
    v = do
            v <- Term -> ReduceM Term
    forall t. Instantiate t => t -> ReduceM t
    instantiate' Term
    v
            case unSpine v of
              Var Int
    n Elims
    es   ->
                 let ts :: Args
    ts = Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
                 in  Term
    var Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! Literal -> Term
    Lit (Integer -> Literal
    LitNat (Integer -> Literal) -> Integer -> Literal
    forall a b. (a -> b) -> a -> b
    $ Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    n) ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ Args -> ReduceM Term
    quoteArgs Args
    ts
              Lam ArgInfo
    info Abs Term
    t -> Term
    lam Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@ Hiding -> ReduceM Term
    quoteHiding (ArgInfo -> Hiding
    forall a. LensHiding a => a -> Hiding
    getHiding ArgInfo
    info) ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ (Term -> ReduceM Term) -> Abs Term -> ReduceM Term
    forall a. Subst a => (a -> ReduceM Term) -> Abs a -> ReduceM Term
    quoteAbs Term -> ReduceM Term
    quoteTerm Abs Term
    t
              Def QName
    x Elims
    es   -> do
                defn <- QName -> ReduceM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x
                patlams <- viewTC ePrintingPatternLambdas
                let isSeenPatLam = QName -> [QName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    elem QName
    x [QName]
    patlams
                r <- isReconstructed
                -- #2220: remember to restore dropped parameters
                let
                  conOrProjPars = Definition -> Bool -> [ReduceM Term]
    defParameters Definition
    defn Bool
    r
                  ts = Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
                  qx Function{ funExtLam :: Defn -> Maybe ExtLamInfo
    funExtLam = Just (ExtLamInfo ModuleName
    m Bool
    False Maybe System
    Strict.Nothing), funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cs }
                    | Bool -> Bool
    not Bool
    isSeenPatLam = Lens' TCEnv [QName]
    -> ([QName] -> [QName]) -> ReduceM Term -> ReduceM Term
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' TCEnv a -> (a -> a) -> m b -> m b
    locallyTC ([QName] -> f [QName]) -> TCEnv -> f TCEnv
    Lens' TCEnv [QName]
    ePrintingPatternLambdas (QName
    x QName -> [QName] -> [QName]
    forall a. a -> [a] -> [a]
    :) (ReduceM Term -> ReduceM Term) -> ReduceM Term -> ReduceM Term
    forall a b. (a -> b) -> a -> b
    $ do

                        -- An extended lambda should not have any extra parameters!
                        Bool -> ReduceM () -> ReduceM ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless ([ReduceM Term] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [ReduceM Term]
    conOrProjPars) ReduceM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                        cs <- [Clause] -> ReduceM [Clause]
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Clause] -> ReduceM [Clause]) -> [Clause] -> ReduceM [Clause]
    forall a b. (a -> b) -> a -> b
    $ (Clause -> Bool) -> [Clause] -> [Clause]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool) -> (Clause -> Bool) -> Clause -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> Bool
    generatedClause) [Clause]
    cs
                        n <- size <$> lookupSection m
                        let (pars, args) = splitAt n ts
                        extlam !@ list (map (quoteClause (Left ()) . (`apply` pars)) cs)
                               @@ list (map (quoteArg quoteTerm) args)
                  qx df :: Defn
    df@Function{ funExtLam :: Defn -> Maybe ExtLamInfo
    funExtLam = Just (ExtLamInfo ModuleName
    _ Bool
    True Maybe System
    Strict.Nothing), funCompiled :: Defn -> Maybe CompiledClauses
    funCompiled = Just Fail{}, funClauses :: Defn -> [Clause]
    funClauses = [Clause
    cl] }
                    | Bool -> Bool
    not Bool
    isSeenPatLam = Lens' TCEnv [QName]
    -> ([QName] -> [QName]) -> ReduceM Term -> ReduceM Term
    forall (m :: * -> *) a b.
    MonadTCEnv m =>
    Lens' TCEnv a -> (a -> a) -> m b -> m b
    locallyTC ([QName] -> f [QName]) -> TCEnv -> f TCEnv
    Lens' TCEnv [QName]
    ePrintingPatternLambdas (QName
    x QName -> [QName] -> [QName]
    forall a. a -> [a] -> [a]
    :) (ReduceM Term -> ReduceM Term) -> ReduceM Term -> ReduceM Term
    forall a b. (a -> b) -> a -> b
    $ do
                        -- See also corresponding code in InternalToAbstract
                        let n :: Int
    n = [NamedArg DeBruijnPattern] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length (Clause -> [NamedArg DeBruijnPattern]
    namedClausePats Clause
    cl) Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1
                            pars :: Args
    pars = Int -> Args -> Args
    forall a. Int -> [a] -> [a]
    take Int
    n Args
    ts
                        Term
    extlam Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@ [ReduceM Term] -> ReduceM Term
    list [Either () Projection -> Clause -> ReduceM Term
    forall a. Either a Projection -> Clause -> ReduceM Term
    quoteClause (() -> Either () Projection
    forall a b. a -> Either a b
    Left ()) (Clause -> ReduceM Term) -> Clause -> ReduceM Term
    forall a b. (a -> b) -> a -> b
    $ Clause
    cl Clause -> Args -> Clause
    forall t. Apply t => t -> Args -> t
    `apply` Args
    pars ]
                               ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ [ReduceM Term] -> ReduceM Term
    list (Int -> [ReduceM Term] -> [ReduceM Term]
    forall a. Int -> [a] -> [a]
    drop Int
    n ([ReduceM Term] -> [ReduceM Term])
    -> [ReduceM Term] -> [ReduceM Term]
    forall a b. (a -> b) -> a -> b
    $ (Arg Term -> ReduceM Term) -> Args -> [ReduceM Term]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Term -> ReduceM Term) -> Arg Term -> ReduceM Term
    forall a. (a -> ReduceM Term) -> Arg a -> ReduceM Term
    quoteArg Term -> ReduceM Term
    quoteTerm) Args
    ts)
                  qx Defn
    _ = do
                    n <- QName -> ReduceM Int
    forall (m :: * -> *).
    (Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
    QName -> m Int
    getDefFreeVars QName
    x
                    def !@! quoteName x
                         @@ list (drop n $ conOrProjPars ++ map (quoteArg quoteTerm) ts)
                qx (theDef defn)
              Con ConHead
    x ConInfo
    ci Elims
    es | Just Args
    ts <- Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es -> do
                r <- ReduceM Bool
    forall (m :: * -> *). MonadTCEnv m => m Bool
    isReconstructed
                cDef <- getConstInfo (conName x)
                n    <- getDefFreeVars (conName x)
                let args = [ReduceM Term] -> ReduceM Term
    list ([ReduceM Term] -> ReduceM Term) -> [ReduceM Term] -> ReduceM Term
    forall a b. (a -> b) -> a -> b
    $ Int -> [ReduceM Term] -> [ReduceM Term]
    forall a. Int -> [a] -> [a]
    drop Int
    n ([ReduceM Term] -> [ReduceM Term])
    -> [ReduceM Term] -> [ReduceM Term]
    forall a b. (a -> b) -> a -> b
    $ Definition -> Bool -> [ReduceM Term]
    defParameters Definition
    cDef Bool
    r [ReduceM Term] -> [ReduceM Term] -> [ReduceM Term]
    forall a. [a] -> [a] -> [a]
    ++ (Arg Term -> ReduceM Term) -> Args -> [ReduceM Term]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Term -> ReduceM Term) -> Arg Term -> ReduceM Term
    forall a. (a -> ReduceM Term) -> Arg a -> ReduceM Term
    quoteArg Term -> ReduceM Term
    quoteTerm) Args
    ts
                con !@! quoteConName x @@ args
              Con ConHead
    x ConInfo
    ci Elims
    es -> Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupported
              Pi Dom Type
    t Abs Type
    u     -> Term
    pi Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@  (Type -> ReduceM Term) -> Dom Type -> ReduceM Term
    forall a. (a -> ReduceM Term) -> Dom a -> ReduceM Term
    quoteDom Type -> ReduceM Term
    quoteType Dom Type
    t
                                ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ (Type -> ReduceM Term) -> Abs Type -> ReduceM Term
    forall a. Subst a => (a -> ReduceM Term) -> Abs a -> ReduceM Term
    quoteAbs Type -> ReduceM Term
    quoteType Abs Type
    u
              Level Level
    l    -> Term -> ReduceM Term
    quoteTerm (LevelKit -> Level -> Term
    unlevelWithKit LevelKit
    lkit Level
    l)
              Lit Literal
    l      -> Term
    lit Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@ Literal -> ReduceM Term
    quoteLit Literal
    l
              Sort Sort
    s     -> Term
    sort Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@ Sort -> ReduceM Term
    quoteSort Sort
    s
              MetaV MetaId
    x Elims
    es -> Term
    meta Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! TopLevelModuleName -> MetaId -> Term
    quoteMeta TopLevelModuleName
    currentModule MetaId
    x
                                  ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ Args -> ReduceM Term
    quoteArgs Args
    vs
                where vs :: Args
    vs = Args -> Maybe Args -> Args
    forall a. a -> Maybe a -> a
    fromMaybe Args
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
    forall a b. (a -> b) -> a -> b
    $ Elims -> Maybe Args
    forall a. [Elim' a] -> Maybe [Arg a]
    allApplyElims Elims
    es
              DontCare Term
    u -> Term -> ReduceM Term
    quoteTerm Term
    u
              Dummy String
    s Elims
    _  -> String -> ReduceM Term
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    String -> m a
    __IMPOSSIBLE_VERBOSE__ String
    s

          defParameters :: Definition -> Bool -> [ReduceM Term]
          defParameters Definition
    def Bool
    True  = []
          defParameters Definition
    def Bool
    False = (Dom' Term (String, Type) -> ReduceM Term)
    -> [Dom' Term (String, Type)] -> [ReduceM Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom' Term (String, Type) -> ReduceM Term
    par [Dom' Term (String, Type)]
    hiding
            where
              np :: Int
    np         = Definition -> Int
    droppedPars Definition
    def
              TelV Telescope
    tel Type
    _ = Type -> TelV Type
    telView' (Definition -> Type
    defType Definition
    def)
              hiding :: [Dom' Term (String, Type)]
    hiding     = Int -> [Dom' Term (String, Type)] -> [Dom' Term (String, Type)]
    forall a. Int -> [a] -> [a]
    take Int
    np ([Dom' Term (String, Type)] -> [Dom' Term (String, Type)])
    -> [Dom' Term (String, Type)] -> [Dom' Term (String, Type)]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom' Term (String, Type)]
    forall t. Tele (Dom t) -> [Dom (String, t)]
    telToList Telescope
    tel
              par :: Dom' Term (String, Type) -> ReduceM Term
    par Dom' Term (String, Type)
    d      = Term
    arg Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@ ArgInfo -> ReduceM Term
    quoteArgInfo (Dom' Term (String, Type) -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom' Term (String, Type)
    d)
                               ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupported

          quoteDefn :: Definition -> ReduceM Term
          quoteDefn Definition
    def =
            case Definition -> Defn
    theDef Definition
    def of
              Function{funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cs, funProjection :: Defn -> Either ProjectionLikenessMissing Projection
    funProjection = Either ProjectionLikenessMissing Projection
    proj} ->
               do
                -- re #3733: maybe these should be quoted but marked as generated?
                cs <- [Clause] -> ReduceM [Clause]
    forall a. a -> ReduceM a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Clause] -> ReduceM [Clause]) -> [Clause] -> ReduceM [Clause]
    forall a b. (a -> b) -> a -> b
    $ (Clause -> Bool) -> [Clause] -> [Clause]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Bool -> Bool
    not (Bool -> Bool) -> (Clause -> Bool) -> Clause -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Clause -> Bool
    generatedClause) [Clause]
    cs
                agdaDefinitionFunDef !@ quoteList (quoteClause proj) cs
              Datatype{dataPars :: Defn -> Int
    dataPars = Int
    np, dataCons :: Defn -> [QName]
    dataCons = [QName]
    cs} ->
                Term
    agdaDefinitionDataDef Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! Integer -> Term
    quoteNat (Int -> Integer
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral Int
    np) ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ (QName -> ReduceM Term) -> [QName] -> ReduceM Term
    forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
    quoteList (Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> ReduceM Term) -> (QName -> Term) -> QName -> ReduceM Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Term
    quoteName) [QName]
    cs
              Record{recConHead :: Defn -> ConHead
    recConHead = ConHead
    c, recFields :: Defn -> [Dom QName]
    recFields = [Dom QName]
    fs} ->
                Term
    agdaDefinitionRecordDef
                  Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! QName -> Term
    quoteName (ConHead -> QName
    conName ConHead
    c)
                  ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ (Dom QName -> ReduceM Term) -> [Dom QName] -> ReduceM Term
    forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
    quoteList ((QName -> ReduceM Term) -> Dom QName -> ReduceM Term
    forall a. (a -> ReduceM Term) -> Dom a -> ReduceM Term
    quoteDom (Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Term -> ReduceM Term) -> (QName -> Term) -> QName -> ReduceM Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QName -> Term
    quoteName)) [Dom QName]
    fs
              Axiom{}       -> Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    agdaDefinitionPostulate
              DataOrRecSig{} -> Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    agdaDefinitionPostulate
              GeneralizableVar{} -> Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    agdaDefinitionPostulate  -- TODO: reflect generalizable vars
              AbstractDefn{}-> Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    agdaDefinitionPostulate
              Primitive{primClauses :: Defn -> [Clause]
    primClauses = [Clause]
    cs} | Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ [Clause] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [Clause]
    cs ->
                Term
    agdaDefinitionFunDef Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@ (Clause -> ReduceM Term) -> [Clause] -> ReduceM Term
    forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
    quoteList (Either () Projection -> Clause -> ReduceM Term
    forall a. Either a Projection -> Clause -> ReduceM Term
    quoteClause (() -> Either () Projection
    forall a b. a -> Either a b
    Left ())) [Clause]
    cs
              Primitive{}   -> Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    agdaDefinitionPrimitive
              PrimitiveSort{} -> Term -> ReduceM Term
    forall a. a -> ReduceM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    agdaDefinitionPrimitive
              Constructor{conData :: Defn -> QName
    conData = QName
    d, conSrcCon :: Defn -> ConHead
    conSrcCon = ConHead
    c} -> do
                q <- Definition -> Quantity
    forall a. LensQuantity a => a -> Quantity
    getQuantity (Definition -> Quantity) -> ReduceM Definition -> ReduceM Quantity
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> QName -> ReduceM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo (ConHead -> QName
    conName ConHead
    c)
                agdaDefinitionDataConstructor !@! quoteName d @@ quoteQuantity q

      return $ QuotingKit quoteTerm quoteType (quoteDom quoteType) quoteDefn quoteList

    quoteString :: String -> Term
    quoteString :: String -> Term
    quoteString = Literal -> Term
    Lit (Literal -> Term) -> (String -> Literal) -> String -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> Literal
    LitString (Text -> Literal) -> (String -> Text) -> String -> Literal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . String -> Text
    T.pack

    quoteName :: QName -> Term
    quoteName :: QName -> Term
    quoteName QName
    x = Literal -> Term
    Lit (QName -> Literal
    LitQName QName
    x)

    quoteNat :: Integer -> Term
    quoteNat :: Integer -> Term
    quoteNat Integer
    n
      | Integer
    n Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Integer
    0    = Literal -> Term
    Lit (Integer -> Literal
    LitNat Integer
    n)
      | Bool
    otherwise = Term
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    quoteConName :: ConHead -> Term
    quoteConName :: ConHead -> Term
    quoteConName = QName -> Term
    quoteName (QName -> Term) -> (ConHead -> QName) -> ConHead -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ConHead -> QName
    conName

    quoteMeta :: TopLevelModuleName -> MetaId -> Term
    quoteMeta :: TopLevelModuleName -> MetaId -> Term
    quoteMeta TopLevelModuleName
    m = Literal -> Term
    Lit (Literal -> Term) -> (MetaId -> Literal) -> MetaId -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TopLevelModuleName -> MetaId -> Literal
    LitMeta TopLevelModuleName
    m

    quoteTerm :: Term -> TCM Term
    quoteTerm :: Term -> TCMT IO Term
    quoteTerm Term
    v = do
      kit <- TCM QuotingKit
    quotingKit
      runReduceM (quoteTermWithKit kit v)

    quoteType :: Type -> TCM Term
    quoteType :: Type -> TCMT IO Term
    quoteType Type
    v = do
      kit <- TCM QuotingKit
    quotingKit
      runReduceM (quoteTypeWithKit kit v)

    quoteDom :: Dom Type -> TCM Term
    quoteDom :: Dom Type -> TCMT IO Term
    quoteDom Dom Type
    v = do
      kit <- TCM QuotingKit
    quotingKit
      runReduceM (quoteDomWithKit kit v)

    quoteDefn :: Definition -> TCM Term
    quoteDefn :: Definition -> TCMT IO Term
    quoteDefn Definition
    def = do
      kit <- TCM QuotingKit
    quotingKit
      runReduceM (quoteDefnWithKit kit def)

    quoteList :: [Term] -> TCM Term
    quoteList :: [Term] -> TCMT IO Term
    quoteList [Term]
    xs = do
      kit <- TCM QuotingKit
    quotingKit
      runReduceM (quoteListWithKit kit pure xs)