{-# 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.Syntax.Common.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          -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError forall a b. (a -> b) -> a -> b
$ [Char]
"Cannot quote a variable " forall a. [a] -> [a] -> [a]
++ forall a. Pretty a => a -> [Char]
prettyShow Name
x
  A.Def QName
x          -> forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
  A.Macro QName
x        -> forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
  A.Proj ProjOrigin
_o AmbiguousQName
p      -> forall {m :: * -> *}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
AmbiguousQName -> m QName
unambiguous AmbiguousQName
p
  A.Con AmbiguousQName
c          -> forall {m :: * -> *}.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
AmbiguousQName -> m QName
unambiguous AmbiguousQName
c
  A.ScopedExpr ScopeInfo
_ Expr
e -> forall (m :: * -> *).
(MonadTCError m, MonadAbsToCon m) =>
Expr -> m QName
quotedName Expr
e
  Expr
e -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do
    forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"Can only quote defined names, but encountered" forall (m :: * -> *). Applicative m => m Doc -> m Doc -> 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 = forall (m :: * -> *) a. Monad m => a -> m a
return QName
x
    | Bool
otherwise =
        forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError forall a b. (a -> b) -> a -> b
$ [Char]
"quote: Ambiguous name: " forall a. [a] -> [a] -> [a]
++ 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
  TopLevelModuleName
currentModule   <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(MonadTCEnv m, ReadTCState m) =>
m (Maybe TopLevelModuleName)
currentTopLevelModule
  Term
hidden          <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHidden
  Term
instanceH       <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInstance
  Term
visible         <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primVisible
  Term
relevant        <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRelevant
  Term
irrelevant      <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIrrelevant
  Term
quantity0       <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQuantity0
  Term
quantityω       <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQuantityω
  Term
modality        <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primModalityConstructor
  Term
nil             <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNil
  Term
cons            <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primCons
  Term
abs             <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAbsAbs
  Term
arg             <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArgArg
  Term
arginfo         <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArgArgInfo
  Term
var             <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermVar
  Term
lam             <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermLam
  Term
extlam          <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermExtLam
  Term
def             <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermDef
  Term
con             <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermCon
  Term
pi              <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermPi
  Term
sort            <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermSort
  Term
meta            <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermMeta
  Term
lit             <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermLit
  Term
litNat          <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitNat
  Term
litWord64       <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitNat
  Term
litFloat        <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitFloat
  Term
litChar         <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitChar
  Term
litString       <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitString
  Term
litQName        <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitQName
  Term
litMeta         <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitMeta
  Term
normalClause    <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaClauseClause
  Term
absurdClause    <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaClauseAbsurd
  Term
varP            <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatVar
  Term
conP            <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatCon
  Term
dotP            <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatDot
  Term
litP            <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatLit
  Term
projP           <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatProj
  Term
absurdP         <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatAbsurd
  Term
set             <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortSet
  Term
setLit          <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortLit
  Term
prop            <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortProp
  Term
propLit         <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortPropLit
  Term
inf             <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortInf
  Term
unsupportedSort <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortUnsupported
  Term
sucLevel        <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc
  Term
lub             <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax
  LevelKit
lkit            <- forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m LevelKit
requireLevels
  Con ConHead
z ConInfo
_ Elims
_       <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primZero
  Con ConHead
s ConInfo
_ Elims
_       <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSuc
  Term
unsupported     <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermUnsupported

  Term
agdaDefinitionFunDef          <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionFunDef
  Term
agdaDefinitionDataDef         <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionDataDef
  Term
agdaDefinitionRecordDef       <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionRecordDef
  Term
agdaDefinitionPostulate       <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionPostulate
  Term
agdaDefinitionPrimitive       <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionPrimitive
  Term
agdaDefinitionDataConstructor <- 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 = forall t. Apply t => t -> Args -> t
apply forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ReduceM a
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((forall a. a -> [a] -> [a]
:[]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Arg a
defaultArg 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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure a
t 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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure a
t forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
u

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

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

      quoteQuantity :: Quantity -> ReduceM Term
      quoteQuantity :: Quantity -> ReduceM Term
quoteQuantity (Quantity0 Q0Origin
_) = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
quantity0
      quoteQuantity (Quantity1 Q1Origin
_) = forall a. HasCallStack => a
__IMPOSSIBLE__
      quoteQuantity (Quantityω QωOrigin
_) = 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 forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ Relevance -> ReduceM Term
quoteRelevance (forall a. LensRelevance a => a -> Relevance
getRelevance Modality
m)
                 forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ Quantity -> ReduceM Term
quoteQuantity  (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 forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ Hiding -> ReduceM Term
quoteHiding Hiding
h
                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    forall a. Apply a => a -> Term -> ReduceM a
!@! Literal -> Term
Lit Literal
l
      quoteLit l :: Literal
l@LitWord64{} = Term
litWord64 forall a. Apply a => a -> Term -> ReduceM a
!@! Literal -> Term
Lit Literal
l
      quoteLit l :: Literal
l@LitFloat{}  = Term
litFloat  forall a. Apply a => a -> Term -> ReduceM a
!@! Literal -> Term
Lit Literal
l
      quoteLit l :: Literal
l@LitChar{}   = Term
litChar   forall a. Apply a => a -> Term -> ReduceM a
!@! Literal -> Term
Lit Literal
l
      quoteLit l :: Literal
l@LitString{} = Term
litString forall a. Apply a => a -> Term -> ReduceM a
!@! Literal -> Term
Lit Literal
l
      quoteLit l :: Literal
l@LitQName{}  = Term
litQName  forall a. Apply a => a -> Term -> ReduceM a
!@! Literal -> Term
Lit Literal
l
      quoteLit l :: Literal
l@LitMeta {}  = Term
litMeta   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 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 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 Univ
u Integer
n) = case Univ
u of
        Univ
UType -> Term
inf forall a. Apply a => a -> Term -> ReduceM a
!@! Literal -> Term
Lit (Integer -> Literal
LitNat Integer
n)
        Univ
UProp -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
        Univ
USSet -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort SSet{}   = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort Sort
SizeUniv = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort Sort
LockUniv = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort Sort
LevelUniv = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort Sort
IntervalUniv = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort PiSort{} = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort FunSort{} = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort UnivSort{}   = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupportedSort
      quoteSort (MetaS MetaId
x Elims
es) = Term -> ReduceM Term
quoteTerm 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 forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
d Elims
es
      quoteSort (DummyS [Char]
s)   =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 = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Literal -> Term
Lit 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 forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. (a -> ReduceM Term) -> Arg a -> ReduceM Term
quoteArg DeBruijnPattern -> ReduceM Term
quotePat forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap 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)
       | forall x. Pattern' x -> Maybe PatOrigin
patternOrigin DeBruijnPattern
p forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just PatOrigin
PatOAbsurd = Term
absurdP forall a. Apply a => a -> Term -> ReduceM a
!@! Integer -> Term
quoteNat (forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x)
      quotePat (VarP PatternInfo
o DBPatVar
x)        = Term
varP forall a. Apply a => a -> Term -> ReduceM a
!@! Integer -> Term
quoteNat (forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x)
      quotePat (DotP PatternInfo
_ Term
t)        = Term
dotP 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 forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ QName -> ReduceM Term
quoteQName (ConHead -> QName
conName ConHead
c) 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 forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ Literal -> ReduceM Term
quoteLit Literal
l
      quotePat (ProjP ProjOrigin
_ QName
x)       = Term
projP 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 forall a. Apply a => a -> Term -> ReduceM a
!@! Integer -> Term
quoteNat (forall a. Integral a => a -> Integer
toInteger forall a b. (a -> b) -> a -> b
$ DBPatVar -> Int
dbPatVarIndex DBPatVar
x)
      quotePat DefP{}            = forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupported

      quoteClause :: Either a Projection -> Clause -> ReduceM Term
      quoteClause :: forall a. 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 forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ Telescope -> ReduceM Term
quoteTelescope Telescope
tel forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ [NamedArg DeBruijnPattern] -> ReduceM Term
quotePats [NamedArg DeBruijnPattern]
ps'
          Just Term
b  -> Term
normalClause forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ Telescope -> ReduceM Term
quoteTelescope Telescope
tel forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ [NamedArg DeBruijnPattern] -> ReduceM Term
quotePats [NamedArg DeBruijnPattern]
ps' 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 forall a. [a] -> [a] -> [a]
++ [NamedArg DeBruijnPattern]
ps
                where
                  n :: Int
n    = Projection -> Int
projIndex Projection
p forall a. Num a => a -> a -> a
- Int
1
                  pars :: [NamedArg DeBruijnPattern]
pars = forall a b. (a -> b) -> [a] -> [b]
map forall {t} {b} {name}.
(Int, Dom' t ([Char], b)) -> Arg (Named name DeBruijnPattern)
toVar forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
take Int
n forall a b. (a -> b) -> a -> b
$ forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Integral a => a -> [a]
downFrom forall a b. (a -> b) -> a -> b
$ forall a. Sized a => a -> Int
size Telescope
tel) (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) = forall t a. Dom' t a -> Arg a
argFromDom Dom' t ([Char], b)
d forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ ([Char]
x, b
_) -> forall a name. a -> Named name a
unnamed forall a b. (a -> b) -> a -> b
$ 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 = forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
quoteList Dom' Term ([Char], Type) -> ReduceM Term
quoteTelEntry forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Telescope
tel

      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
..} <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, HasConstInfo m) =>
m (Maybe SigmaKit)
getSigmaKit
        ConHead -> ConInfo -> Elims -> Term
Con ConHead
sigmaCon ConInfo
ConOSystem [] forall a. Apply a => a -> Term -> ReduceM a
!@! [Char] -> Term
quoteString [Char]
x forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ forall a. (a -> ReduceM Term) -> Dom a -> ReduceM Term
quoteDom Type -> ReduceM Term
quoteType (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd Dom' Term ([Char], Type)
dom)

      list :: [ReduceM Term] -> ReduceM Term
      list :: [ReduceM Term] -> ReduceM Term
list = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ ReduceM Term
a ReduceM Term
as -> Term
cons forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ ReduceM Term
a forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ ReduceM Term
as) (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 (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 forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ ArgInfo -> ReduceM Term
quoteArgInfo ArgInfo
info 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 forall a. Apply a => a -> Term -> ReduceM a
!@! [Char] -> Term
quoteString [Char]
s 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 forall a. Apply a => a -> Term -> ReduceM a
!@! [Char] -> Term
quoteString [Char]
s forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ a -> ReduceM Term
q (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 forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ ArgInfo -> ReduceM Term
quoteArgInfo ArgInfo
info 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 (forall a b. (a -> b) -> [a] -> [b]
map (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 -> Bool
generatedClause Clause
cl = [NamedArg DeBruijnPattern] -> Bool
hasDefP (Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl)

      quoteTerm :: Term -> ReduceM Term
      quoteTerm :: Term -> ReduceM Term
quoteTerm Term
v = do
        Term
v <- 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 = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
             in  Term
var forall a. Apply a => a -> Term -> ReduceM a
!@! Literal -> Term
Lit (Integer -> Literal
LitNat forall a b. (a -> b) -> a -> b
$ forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
n) forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ Args -> ReduceM Term
quoteArgs Args
ts
          Lam ArgInfo
info Abs Term
t -> Term
lam forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ Hiding -> ReduceM Term
quoteHiding (forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
info) forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ 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 <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
x
            Bool
r <- 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 = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ 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!
                    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Bool
null [ReduceM Term]
conOrProjPars) forall a. HasCallStack => a
__IMPOSSIBLE__
                    [Clause]
cs <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Bool
generatedClause) [Clause]
cs
                    Int
n <- forall a. Sized a => a -> Int
size forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m Telescope
lookupSection ModuleName
m
                    let (Args
pars, Args
args) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
n Args
ts
                    Term
extlam forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ [ReduceM Term] -> ReduceM Term
list (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Either a Projection -> Clause -> ReduceM Term
quoteClause (forall a b. a -> Either a b
Left ()) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall t. Apply t => t -> Args -> t
`apply` Args
pars)) [Clause]
cs)
                           forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ [ReduceM Term] -> ReduceM Term
list (forall a b. (a -> b) -> [a] -> [b]
map (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 = forall (t :: * -> *) a. Foldable t => t a -> Int
length (Clause -> [NamedArg DeBruijnPattern]
namedClausePats Clause
cl) forall a. Num a => a -> a -> a
- Int
1
                        pars :: Args
pars = forall a. Int -> [a] -> [a]
take Int
n Args
ts
                    Term
extlam forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ [ReduceM Term] -> ReduceM Term
list [forall a. Either a Projection -> Clause -> ReduceM Term
quoteClause (forall a b. a -> Either a b
Left ()) forall a b. (a -> b) -> a -> b
$ Clause
cl forall t. Apply t => t -> Args -> t
`apply` Args
pars ]
                           forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ [ReduceM Term] -> ReduceM Term
list (forall a. Int -> [a] -> [a]
drop Int
n forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. (a -> ReduceM Term) -> Arg a -> ReduceM Term
quoteArg Term -> ReduceM Term
quoteTerm) Args
ts)
              qx Defn
_ = do
                Int
n <- forall (m :: * -> *).
(Functor m, Applicative m, ReadTCState m, MonadTCEnv m) =>
QName -> m Int
getDefFreeVars QName
x
                Term
def forall a. Apply a => a -> Term -> ReduceM a
!@! QName -> Term
quoteName QName
x
                     forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ [ReduceM Term] -> ReduceM Term
list (forall a. Int -> [a] -> [a]
drop Int
n forall a b. (a -> b) -> a -> b
$ [ReduceM Term]
conOrProjPars forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (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 <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es -> do
            Bool
r <- forall (m :: * -> *). MonadTCEnv m => m Bool
isReconstructed
            Definition
cDef <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo (ConHead -> QName
conName ConHead
x)
            Int
n    <- 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 forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop Int
n forall a b. (a -> b) -> a -> b
$ Definition -> Bool -> [ReduceM Term]
defParameters Definition
cDef Bool
r forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall a. (a -> ReduceM Term) -> Arg a -> ReduceM Term
quoteArg Term -> ReduceM Term
quoteTerm) Args
ts
            Term
con forall a. Apply a => a -> Term -> ReduceM a
!@! ConHead -> Term
quoteConName ConHead
x forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ ReduceM Term
args
          Con ConHead
x ConInfo
ci Elims
es -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
unsupported
          Pi Dom Type
t Abs Type
u     -> Term
pi forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@  forall a. (a -> ReduceM Term) -> Dom a -> ReduceM Term
quoteDom Type -> ReduceM Term
quoteType Dom Type
t
                            forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ 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 forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ Literal -> ReduceM Term
quoteLit Literal
l
          Sort Sort
s     -> Term
sort forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ Sort -> ReduceM Term
quoteSort Sort
s
          MetaV MetaId
x Elims
es -> Term
meta forall a. Apply a => a -> Term -> ReduceM a
!@! TopLevelModuleName -> MetaId -> Term
quoteMeta TopLevelModuleName
currentModule MetaId
x
                              forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ Args -> ReduceM Term
quoteArgs Args
vs
            where vs :: Args
vs = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
          DontCare Term
u -> Term -> ReduceM Term
quoteTerm Term
u
          Dummy [Char]
s Elims
_  -> 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 = 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 -> Either ProjectionLikenessMissing Projection
funProjection = Right Projection
p } -> Projection -> Int
projIndex Projection
p 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     = forall a. Int -> [a] -> [a]
take Int
np forall a b. (a -> b) -> a -> b
$ 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 forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ ArgInfo -> ReduceM Term
quoteArgInfo (forall t e. Dom' t e -> ArgInfo
domInfo Dom' Term ([Char], Type)
d)
                           forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ 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 -> Either ProjectionLikenessMissing Projection
funProjection = Either ProjectionLikenessMissing Projection
proj} ->
           do
            -- re #3733: maybe these should be quoted but marked as generated?
            [Clause]
cs <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> Bool
generatedClause) [Clause]
cs
            Term
agdaDefinitionFunDef forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
quoteList (forall a. Either a Projection -> Clause -> ReduceM Term
quoteClause Either ProjectionLikenessMissing Projection
proj) [Clause]
cs
          Datatype{dataPars :: Defn -> Int
dataPars = Int
np, dataCons :: Defn -> [QName]
dataCons = [QName]
cs} ->
            Term
agdaDefinitionDataDef forall a. Apply a => a -> Term -> ReduceM a
!@! Integer -> Term
quoteNat (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
np) forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
quoteList (forall (f :: * -> *) a. Applicative f => a -> f a
pure 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
              forall a. Apply a => a -> Term -> ReduceM a
!@! QName -> Term
quoteName (ConHead -> QName
conName ConHead
c)
              forall a. Apply a => ReduceM a -> ReduceM Term -> ReduceM a
@@ forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
quoteList (forall a. (a -> ReduceM Term) -> Dom a -> ReduceM Term
quoteDom (forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Term
quoteName)) [Dom QName]
fs
          Axiom{}       -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
agdaDefinitionPostulate
          DataOrRecSig{} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
agdaDefinitionPostulate
          GeneralizableVar{} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
agdaDefinitionPostulate  -- TODO: reflect generalizable vars
          AbstractDefn{}-> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
agdaDefinitionPostulate
          Primitive{primClauses :: Defn -> [Clause]
primClauses = [Clause]
cs} | Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Clause]
cs ->
            Term
agdaDefinitionFunDef forall a. Apply a => a -> ReduceM Term -> ReduceM a
!@ forall a. (a -> ReduceM Term) -> [a] -> ReduceM Term
quoteList (forall a. Either a Projection -> Clause -> ReduceM Term
quoteClause (forall a b. a -> Either a b
Left ())) [Clause]
cs
          Primitive{}   -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
agdaDefinitionPrimitive
          PrimitiveSort{} -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
agdaDefinitionPrimitive
          Constructor{conData :: Defn -> QName
conData = QName
d} ->
            Term
agdaDefinitionDataConstructor forall a. Apply a => a -> Term -> ReduceM a
!@! QName -> Term
quoteName QName
d

  forall (m :: * -> *) a. Monad m => a -> m a
return 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 (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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> Literal
LitString 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 forall a. Ord a => a -> a -> Bool
>= Integer
0    = Literal -> Term
Lit (Integer -> Literal
LitNat Integer
n)
  | Bool
otherwise = forall a. HasCallStack => a
__IMPOSSIBLE__

quoteConName :: ConHead -> Term
quoteConName :: ConHead -> Term
quoteConName = QName -> Term
quoteName 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. TopLevelModuleName -> MetaId -> Literal
LitMeta TopLevelModuleName
m

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

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

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

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

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