{-# 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
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ω
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
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
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
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)
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
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
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
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
[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
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)