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.Internal.Pattern ( hasDefP, dbPatPerm )
import Agda.Syntax.Literal
import Agda.Syntax.Position
import Agda.Syntax.TopLevelModuleName

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          -> 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: Ambigous 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 IsFibrant
f Integer
n) = case IsFibrant
f of
        IsFibrant
IsFibrant -> Term
inf forall a. Apply a => a -> Term -> ReduceM a
!@! Literal -> Term
Lit (Integer -> Literal
LitNat Integer
n)
        IsFibrant
IsStrict  -> 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
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 (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m 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)