    module Agda.TypeChecking.Quote where

    import Control.Arrow ((&&&))
    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.Literal
    import Agda.Syntax.Position

    import Agda.TypeChecking.CompiledClause
    import Agda.TypeChecking.DropArgs
    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.FileName
    import Agda.Utils.Functor
    import Agda.Utils.List
    import Agda.Utils.Pretty (prettyShow)
    import Agda.Utils.Size

    -- | Parse @quote@.
    quotedName :: (MonadTCError m, MonadAbsToCon m) => A.Expr -> m QName
    quotedName :: forall (m :: * -> *).
    (MonadTCError m, MonadAbsToCon m) =>
    Expr -> m QName
    quotedName = \case
      A.Var Name
    x          -> [Char] -> m QName
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    [Char] -> m a
    genericError ([Char] -> m QName) -> [Char] -> m QName
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "Cannot quote a variable " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ Name -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow Name
    x
      A.Def QName
    x          -> QName -> m QName
    forall (m :: * -> *) a. Monad m => a -> m a
    return QName
    x
      A.Macro QName
    x        -> QName -> m QName
    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 -> Doc -> m QName
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    Doc -> m a
    genericDocError (Doc -> m QName) -> m Doc -> m QName
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< do
        [Char] -> m Doc
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
    text [Char]
    "Can only quote defined names, but encountered" m Doc -> m Doc -> m Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    <+> Expr -> m Doc
    forall a (m :: * -> *).
    (ToConcrete a, Pretty (ConOfAbs a), MonadAbsToCon m) =>
    a -> m Doc
    prettyA Expr
    e
      where
      unambiguous :: AmbiguousQName -> m QName
    unambiguous AmbiguousQName
    xs
        | Just QName
    x <- AmbiguousQName -> Maybe QName
    getUnambiguous AmbiguousQName
    xs = QName -> m QName
    forall (m :: * -> *) a. Monad m => a -> m a
    return QName
    x
        | Bool
    otherwise =
            [Char] -> m QName
    forall (m :: * -> *) a.
    (HasCallStack, MonadTCError m) =>
    [Char] -> m a
    genericError ([Char] -> m QName) -> [Char] -> m QName
    forall a b. (a -> b) -> a -> b
    $ [Char]
    "quote: Ambigous name: " [Char] -> [Char] -> [Char]
    forall a. [a] -> [a] -> [a]
    ++ List1 QName -> [Char]
    forall a. Pretty a => a -> [Char]
    prettyShow (AmbiguousQName -> List1 QName
    unAmbQ AmbiguousQName
    xs)

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

      Term
    agdaDefinitionFunDef          <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaDefinitionFunDef
      Term
    agdaDefinitionDataDef         <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaDefinitionDataDef
      Term
    agdaDefinitionRecordDef       <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaDefinitionRecordDef
      Term
    agdaDefinitionPostulate       <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaDefinitionPostulate
      Term
    agdaDefinitionPrimitive       <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaDefinitionPrimitive
      Term
    agdaDefinitionDataConstructor <- TCMT IO Term
    forall (m :: * -> *).
    (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
    m Term
    primAgdaDefinitionDataConstructor

      let (@@) :: Apply a => ReduceM a -> ReduceM Term -> ReduceM a
          ReduceM a
    t @@ :: forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ 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 (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 !@ :: forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@ ReduceM Term
    u = 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 !@! :: forall a. Apply a => a -> Term -> ReduceM a
    !@! Term
    u = 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 (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    u

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

          quoteRelevance :: Relevance -> ReduceM Term
          quoteRelevance :: Relevance -> ReduceM Term
    quoteRelevance Relevance
    Relevant   = Term -> ReduceM Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    relevant
          quoteRelevance Relevance
    Irrelevant = Term -> ReduceM Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    irrelevant
          quoteRelevance Relevance
    NonStrict  = Term -> ReduceM Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    relevant

          quoteQuantity :: Quantity -> ReduceM Term
          quoteQuantity :: Quantity -> ReduceM Term
    quoteQuantity (Quantity0 Q0Origin
    _) = Term -> ReduceM Term
    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 (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    quantityω

          -- TODO: quote Annotation
          quoteModality :: Modality -> ReduceM Term
          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 -> 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 :: 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 -> 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 :: 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 IsFibrant
    f Integer
    n) = case IsFibrant
    f of
            IsFibrant
    IsFibrant -> Term
    inf Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! Literal -> Term
    Lit (Integer -> Literal
    LitNat Integer
    n)
            IsFibrant
    IsStrict  -> Term -> ReduceM Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupportedSort
          quoteSort SSet{}   = Term -> ReduceM Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupportedSort
          quoteSort Sort
    SizeUniv = Term -> ReduceM Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupportedSort
          quoteSort Sort
    LockUniv = Term -> ReduceM Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupportedSort
          quoteSort PiSort{} = Term -> ReduceM Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupportedSort
          quoteSort FunSort{} = Term -> ReduceM Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupportedSort
          quoteSort UnivSort{}   = Term -> ReduceM Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupportedSort
          quoteSort (MetaS MetaId
    x Elims
    es) = Term -> ReduceM Term
    quoteTerm (Term -> ReduceM Term) -> Term -> ReduceM Term
    forall a b. (a -> b) -> a -> b
    $ MetaId -> Elims -> Term
    MetaV MetaId
    x Elims
    es
          quoteSort (DefS QName
    d Elims
    es)  = Term -> ReduceM Term
    quoteTerm (Term -> ReduceM Term) -> Term -> ReduceM Term
    forall a b. (a -> b) -> a -> b
    $ QName -> Elims -> Term
    Def QName
    d Elims
    es
          quoteSort (DummyS [Char]
    s)   =[Char] -> ReduceM Term
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    [Char] -> m a
    __IMPOSSIBLE_VERBOSE__ [Char]
    s

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

          quoteQName :: QName -> ReduceM Term
          quoteQName :: QName -> ReduceM Term
    quoteQName QName
    x = Term -> ReduceM Term
    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] -> 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 (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 :: 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
          quotePat (IApplyP PatternInfo
    o Term
    t Term
    u DBPatVar
    x) = Term -> ReduceM Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupported
          quotePat DefP{}            = Term -> ReduceM Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupported

          quoteClause :: Maybe Projection -> Clause -> ReduceM Term
          quoteClause :: Maybe Projection -> Clause -> ReduceM Term
    quoteClause Maybe 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 Maybe Projection
    proj of
                  Maybe Projection
    Nothing -> [NamedArg DeBruijnPattern]
    ps
                  Just 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 ([Char], Type)) -> NamedArg DeBruijnPattern)
    -> [(Int, Dom' Term ([Char], Type))] -> [NamedArg DeBruijnPattern]
    forall a b. (a -> b) -> [a] -> [b]
    map (Int, Dom' Term ([Char], Type)) -> NamedArg DeBruijnPattern
    forall {t} {b} {name}.
    (Int, Dom' t ([Char], b)) -> Arg (Named name DeBruijnPattern)
    toVar ([(Int, Dom' Term ([Char], Type))] -> [NamedArg DeBruijnPattern])
    -> [(Int, Dom' Term ([Char], Type))] -> [NamedArg DeBruijnPattern]
    forall a b. (a -> b) -> a -> b
    $ Int
    -> [(Int, Dom' Term ([Char], Type))]
    -> [(Int, Dom' Term ([Char], Type))]
    forall a. Int -> [a] -> [a]
    take Int
    n ([(Int, Dom' Term ([Char], Type))]
     -> [(Int, Dom' Term ([Char], Type))])
    -> [(Int, Dom' Term ([Char], Type))]
    -> [(Int, Dom' Term ([Char], Type))]
    forall a b. (a -> b) -> a -> b
    $ [Int]
    -> [Dom' Term ([Char], Type)] -> [(Int, Dom' Term ([Char], 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 ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Telescope
    tel)
                      toVar :: (Int, Dom' t ([Char], b)) -> Arg (Named name DeBruijnPattern)
    toVar (Int
    i, Dom' t ([Char], b)
    d) = Dom' t ([Char], b) -> Arg ([Char], b)
    forall t a. Dom' t a -> Arg a
    argFromDom Dom' t ([Char], b)
    d Arg ([Char], b)
    -> (([Char], b) -> Named name DeBruijnPattern)
    -> Arg (Named name DeBruijnPattern)
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    <&> \ ([Char]
    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 ([Char] -> Int -> DBPatVar
    DBPatVar [Char]
    x Int
    i)

          quoteTelescope :: Telescope -> ReduceM Term
          quoteTelescope :: Telescope -> ReduceM Term
    quoteTelescope Telescope
    tel = (Dom' Term ([Char], Type) -> ReduceM Term)
    -> [Dom' Term ([Char], Type)] -> ReduceM Term
    forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
    quoteList Dom' Term ([Char], Type) -> ReduceM Term
    quoteTelEntry ([Dom' Term ([Char], Type)] -> ReduceM Term)
    -> [Dom' Term ([Char], Type)] -> ReduceM Term
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom' Term ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Telescope
    tel
            where
              quoteTelEntry :: Dom (ArgName, Type) -> ReduceM Term
              quoteTelEntry :: Dom' Term ([Char], Type) -> ReduceM Term
    quoteTelEntry dom :: Dom' Term ([Char], Type)
    dom@Dom{ unDom :: forall t e. Dom' t e -> e
    unDom = ([Char]
    x , Type
    t) } = do
                SigmaKit{QName
    ConHead
    sigmaSnd :: SigmaKit -> QName
    sigmaFst :: SigmaKit -> QName
    sigmaCon :: SigmaKit -> ConHead
    sigmaName :: SigmaKit -> QName
    sigmaSnd :: QName
    sigmaFst :: QName
    sigmaCon :: ConHead
    sigmaName :: QName
    ..} <- 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
                ConHead -> ConInfo -> Elims -> Term
    Con ConHead
    sigmaCon ConInfo
    ConOSystem [] Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! [Char] -> Term
    quoteString [Char]
    x ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM 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 ((([Char], Type) -> Type) -> Dom' Term ([Char], Type) -> Dom Type
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ([Char], Type) -> Type
    forall a b. (a, b) -> b
    snd Dom' Term ([Char], Type)
    dom)

          list :: [ReduceM Term] -> ReduceM Term
          list :: [ReduceM Term] -> ReduceM Term
    list = (ReduceM Term -> ReduceM Term -> ReduceM Term)
    -> ReduceM Term -> [ReduceM Term] -> ReduceM Term
    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 (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    nil)

          quoteList :: (a -> ReduceM Term) -> [a] -> ReduceM Term
          quoteList :: forall a. (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 :: forall a. (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 :: forall a. Subst a => (a -> ReduceM Term) -> Abs a -> ReduceM Term
    quoteAbs a -> ReduceM Term
    q (Abs [Char]
    s a
    t)   = Term
    abs Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! [Char] -> Term
    quoteString [Char]
    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 [Char]
    s a
    t) = Term
    abs Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! [Char] -> Term
    quoteString [Char]
    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 :: forall a. (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 -> 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)

          quoteTerm :: Term -> ReduceM Term
          quoteTerm :: Term -> ReduceM Term
    quoteTerm Term
    v = do
            Term
    v <- Term -> ReduceM Term
    forall t. Instantiate t => t -> ReduceM t
    instantiate' Term
    v
            case Term -> Term
    unSpine Term
    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
                Definition
    defn <- QName -> ReduceM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo QName
    x
                Bool
    r <- ReduceM Bool
    forall (m :: * -> *). MonadTCEnv m => m Bool
    isReconstructed
                -- #2220: remember to restore dropped parameters
                let
                  conOrProjPars :: [ReduceM Term]
    conOrProjPars = Definition -> Bool -> [ReduceM Term]
    defParameters Definition
    defn Bool
    r
                  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
                  qx :: Defn -> ReduceM Term
    qx Function{ funExtLam :: Defn -> Maybe ExtLamInfo
    funExtLam = Just (ExtLamInfo ModuleName
    m Bool
    False Maybe System
    _), funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cs } = 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 (t :: * -> *) a. Foldable t => t a -> Bool
    null [ReduceM Term]
    conOrProjPars) ReduceM ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                        Int
    n <- Telescope -> Int
    forall a. Sized a => a -> Int
    size (Telescope -> Int) -> ReduceM Telescope -> ReduceM Int
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ModuleName -> ReduceM Telescope
    forall (m :: * -> *).
    (Functor m, ReadTCState m) =>
    ModuleName -> m Telescope
    lookupSection ModuleName
    m
                        let (Args
    pars, Args
    args) = Int -> Args -> (Args, Args)
    forall a. Int -> [a] -> ([a], [a])
    splitAt 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 ((Clause -> ReduceM Term) -> [Clause] -> [ReduceM Term]
    forall a b. (a -> b) -> [a] -> [b]
    map (Maybe Projection -> Clause -> ReduceM Term
    quoteClause Maybe Projection
    forall a. Maybe a
    Nothing (Clause -> ReduceM Term)
    -> (Clause -> Clause) -> Clause -> ReduceM Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Clause -> Args -> Clause
    forall t. Apply t => t -> Args -> t
    `apply` Args
    pars)) [Clause]
    cs)
                               ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ [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
    args)
                  qx df :: Defn
    df@Function{ funExtLam :: Defn -> Maybe ExtLamInfo
    funExtLam = Just (ExtLamInfo ModuleName
    _ Bool
    True Maybe System
    _), funCompiled :: Defn -> Maybe CompiledClauses
    funCompiled = Just Fail{}, funClauses :: Defn -> [Clause]
    funClauses = [Clause
    cl] } = do
                        -- See also corresponding code in InternalToAbstract
                        let n :: Int
    n = [NamedArg DeBruijnPattern] -> 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 [Maybe Projection -> Clause -> ReduceM Term
    quoteClause Maybe Projection
    forall a. Maybe a
    Nothing (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
                    Int
    n <- QName -> ReduceM Int
    forall (m :: * -> *).
    (Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
    QName -> m Int
    getDefFreeVars QName
    x
                    Term
    def Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! QName -> Term
    quoteName QName
    x
                         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
    $ [ReduceM Term]
    conOrProjPars [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)
                Defn -> ReduceM Term
    qx (Definition -> Defn
    theDef Definition
    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
                Bool
    r <- ReduceM Bool
    forall (m :: * -> *). MonadTCEnv m => m Bool
    isReconstructed
                Definition
    cDef <- QName -> ReduceM Definition
    forall (m :: * -> *). HasConstInfo m => QName -> m Definition
    getConstInfo (ConHead -> QName
    conName ConHead
    x)
                Int
    n    <- QName -> ReduceM Int
    forall (m :: * -> *).
    (Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
    QName -> m Int
    getDefFreeVars (ConHead -> QName
    conName ConHead
    x)
                let args :: ReduceM Term
    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
                Term
    con Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! ConHead -> Term
    quoteConName ConHead
    x ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ ReduceM Term
    args
              Con ConHead
    x ConInfo
    ci Elims
    es -> Term -> ReduceM Term
    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
    !@! AbsolutePath -> MetaId -> Term
    quoteMeta AbsolutePath
    currentFile 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 [Char]
    s Elims
    _  -> [Char] -> ReduceM Term
    forall (m :: * -> *) a.
    (HasCallStack, MonadDebug m) =>
    [Char] -> m a
    __IMPOSSIBLE_VERBOSE__ [Char]
    s

          defParameters :: Definition -> Bool -> [ReduceM Term]
          defParameters :: Definition -> Bool -> [ReduceM Term]
    defParameters Definition
    def Bool
    True  = []
          defParameters Definition
    def Bool
    False = (Dom' Term ([Char], Type) -> ReduceM Term)
    -> [Dom' Term ([Char], Type)] -> [ReduceM Term]
    forall a b. (a -> b) -> [a] -> [b]
    map Dom' Term ([Char], Type) -> ReduceM Term
    par [Dom' Term ([Char], Type)]
    hiding
            where
              np :: Int
    np = case Definition -> Defn
    theDef Definition
    def of
                     Constructor{ conPars :: Defn -> Int
    conPars = Int
    np }        -> Int
    np
                     Function{ funProjection :: Defn -> Maybe Projection
    funProjection = Just Projection
    p } -> Projection -> Int
    projIndex Projection
    p Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1
                     Defn
    _                                  -> Int
    0
              TelV Telescope
    tel Type
    _ = Type -> TelV Type
    telView' (Definition -> Type
    defType Definition
    def)
              hiding :: [Dom' Term ([Char], Type)]
    hiding     = Int -> [Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)]
    forall a. Int -> [a] -> [a]
    take Int
    np ([Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)])
    -> [Dom' Term ([Char], Type)] -> [Dom' Term ([Char], Type)]
    forall a b. (a -> b) -> a -> b
    $ Telescope -> [Dom' Term ([Char], Type)]
    forall t. Tele (Dom t) -> [Dom ([Char], t)]
    telToList Telescope
    tel
              par :: Dom' Term ([Char], Type) -> ReduceM Term
    par Dom' Term ([Char], Type)
    d      = Term
    arg Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => a -> ReduceM Term -> ReduceM a
    !@ ArgInfo -> ReduceM Term
    quoteArgInfo (Dom' Term ([Char], Type) -> ArgInfo
    forall t e. Dom' t e -> ArgInfo
    domInfo Dom' Term ([Char], Type)
    d)
                               ReduceM Term -> ReduceM Term -> ReduceM Term
    forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
    @@ Term -> ReduceM Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    unsupported

          quoteDefn :: Definition -> ReduceM Term
          quoteDefn :: Definition -> ReduceM Term
    quoteDefn Definition
    def =
            case Definition -> Defn
    theDef Definition
    def of
              Function{funClauses :: Defn -> [Clause]
    funClauses = [Clause]
    cs, funProjection :: Defn -> Maybe Projection
    funProjection = Maybe Projection
    proj} ->
                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 (Maybe Projection -> Clause -> ReduceM Term
    quoteClause Maybe Projection
    proj) [Clause]
    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 (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 (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 (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    agdaDefinitionPostulate
              DataOrRecSig{} -> Term -> ReduceM Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    agdaDefinitionPostulate
              GeneralizableVar{} -> Term -> ReduceM Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    agdaDefinitionPostulate  -- TODO: reflect generalizable vars
              AbstractDefn{}-> Term -> ReduceM Term
    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 (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 (Maybe Projection -> Clause -> ReduceM Term
    quoteClause Maybe Projection
    forall a. Maybe a
    Nothing) [Clause]
    cs
              Primitive{}   -> Term -> ReduceM Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    agdaDefinitionPrimitive
              PrimitiveSort{} -> Term -> ReduceM Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Term
    agdaDefinitionPrimitive
              Constructor{conData :: Defn -> QName
    conData = QName
    d} ->
                Term
    agdaDefinitionDataConstructor Term -> Term -> ReduceM Term
    forall a. Apply a => a -> Term -> ReduceM a
    !@! QName -> Term
    quoteName QName
    d

      QuotingKit -> TCM QuotingKit
    forall (m :: * -> *) a. Monad m => a -> m a
    return (QuotingKit -> TCM QuotingKit) -> QuotingKit -> TCM QuotingKit
    forall a b. (a -> b) -> a -> b
    $ (Term -> ReduceM Term)
    -> (Type -> ReduceM Term)
    -> (Dom Type -> ReduceM Term)
    -> (Definition -> ReduceM Term)
    -> (forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term)
    -> QuotingKit
    QuotingKit Term -> ReduceM Term
    quoteTerm Type -> ReduceM Term
    quoteType ((Type -> ReduceM Term) -> Dom Type -> ReduceM Term
    forall a. (a -> ReduceM Term) -> Dom a -> ReduceM Term
    quoteDom Type -> ReduceM Term
    quoteType) Definition -> ReduceM Term
    quoteDefn forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
    quoteList

    quoteString :: String -> Term
    quoteString :: [Char] -> Term
    quoteString = Literal -> Term
    Lit (Literal -> Term) -> ([Char] -> Literal) -> [Char] -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> Literal
    LitString (Text -> Literal) -> ([Char] -> Text) -> [Char] -> Literal
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Char] -> 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 :: AbsolutePath -> MetaId -> Term
    quoteMeta :: AbsolutePath -> MetaId -> Term
    quoteMeta AbsolutePath
    file = Literal -> Term
    Lit (Literal -> Term) -> (MetaId -> Literal) -> MetaId -> Term
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . AbsolutePath -> MetaId -> Literal
    LitMeta AbsolutePath
    file

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

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

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

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

    quoteList :: [Term] -> TCM Term
    quoteList :: [Term] -> TCMT IO Term
    quoteList [Term]
    xs = do
      QuotingKit
    kit <- TCM QuotingKit
    quotingKit
      ReduceM Term -> TCMT IO Term
    forall a. ReduceM a -> TCM a
    runReduceM (QuotingKit -> forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
    quoteListWithKit QuotingKit
    kit Term -> ReduceM Term
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure [Term]
    xs)