{-# OPTIONS_GHC -Wunused-imports #-}
{-# LANGUAGE NondecreasingIndentation #-}
module Agda.TypeChecking.Rules.Builtin
( bindBuiltin
, bindBuiltinNoDef
, builtinKindOfName
, bindPostulatedName
, isUntypedBuiltin
, bindUntypedBuiltin
) where
import Prelude hiding (null)
import Control.Monad
import Control.Monad.Except
import Control.Monad.Trans.Maybe
import Data.List (find, sortBy)
import Data.Function (on)
import Agda.Interaction.Options.Base
import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base
import Agda.TypeChecking.Monad
import qualified Agda.TypeChecking.CompiledClause as CC
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints ( noConstraints )
import Agda.TypeChecking.Functions
import Agda.TypeChecking.Names
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Rules.Term ( checkExpr , inferExpr )
import Agda.TypeChecking.Warnings
import {-# SOURCE #-} Agda.TypeChecking.Rules.Builtin.Coinduction
import {-# SOURCE #-} Agda.TypeChecking.Rewriting
import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.List1 (pattern (:|))
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Size
import Agda.Utils.Impossible
builtinPostulate :: TCM Type -> BuiltinDescriptor
builtinPostulate :: TCM Type -> BuiltinDescriptor
builtinPostulate = Relevance -> TCM Type -> BuiltinDescriptor
BuiltinPostulate Relevance
Relevant
builtinPostulateC :: Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC :: Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
c TCM Type
m =
Relevance -> TCM Type -> BuiltinDescriptor
BuiltinPostulate Relevance
Relevant forall a b. (a -> b) -> a -> b
$ Cubical -> [Char] -> TCM ()
requireCubical Cubical
c [Char]
"" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TCM Type
m
findBuiltinInfo :: BuiltinId -> Maybe BuiltinInfo
findBuiltinInfo :: BuiltinId -> Maybe BuiltinInfo
findBuiltinInfo BuiltinId
b = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((BuiltinId
b forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinInfo -> BuiltinId
builtinName) [BuiltinInfo]
coreBuiltins
coreBuiltins :: [BuiltinInfo]
coreBuiltins :: [BuiltinInfo]
coreBuiltins =
[ (BuiltinId
builtinList BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData (forall (m :: * -> *). Applicative m => m Type
tset forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Applicative m => m Type
tset) [BuiltinId
builtinNil, BuiltinId
builtinCons])
, (BuiltinId
builtinArg BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData (forall (m :: * -> *). Applicative m => m Type
tset forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Applicative m => m Type
tset) [BuiltinId
builtinArgArg])
, (BuiltinId
builtinAbs BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData (forall (m :: * -> *). Applicative m => m Type
tset forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Applicative m => m Type
tset) [BuiltinId
builtinAbsAbs])
, (BuiltinId
builtinArgInfo BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinArgArgInfo])
, (BuiltinId
builtinBool BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinTrue, BuiltinId
builtinFalse])
, (BuiltinId
builtinNat BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinZero, BuiltinId
builtinSuc])
, (BuiltinId
builtinMaybe BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData (forall (m :: * -> *). Applicative m => m Type
tset forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Applicative m => m Type
tset) [BuiltinId
builtinNothing, BuiltinId
builtinJust])
, (BuiltinId
builtinSigma BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData (forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"la" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"lb" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
b ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"A" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a) forall a b. (a -> b) -> a -> b
$ \NamesT (TCMT IO) Term
bA ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"B" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
b)) forall a b. (a -> b) -> a -> b
$ \NamesT (TCMT IO) Term
bB ->
((Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
b))
)
[BuiltinId
BuiltinSigmaCon])
, (BuiltinId
builtinUnit BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinUnitUnit])
, (BuiltinId
builtinAgdaLiteral BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinAgdaLitNat, BuiltinId
builtinAgdaLitWord64, BuiltinId
builtinAgdaLitFloat,
BuiltinId
builtinAgdaLitChar, BuiltinId
builtinAgdaLitString,
BuiltinId
builtinAgdaLitQName, BuiltinId
builtinAgdaLitMeta])
, (BuiltinId
builtinAgdaPattern BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinAgdaPatVar, BuiltinId
builtinAgdaPatCon, BuiltinId
builtinAgdaPatDot,
BuiltinId
builtinAgdaPatLit, BuiltinId
builtinAgdaPatProj, BuiltinId
builtinAgdaPatAbsurd])
, (BuiltinId
builtinAgdaPatVar BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tpat))
, (BuiltinId
builtinAgdaPatCon BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
tpat) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tpat))
, (BuiltinId
builtinAgdaPatDot BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tpat))
, (BuiltinId
builtinAgdaPatLit BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tliteral forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tpat))
, (BuiltinId
builtinAgdaPatProj BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tpat))
, (BuiltinId
builtinAgdaPatAbsurd BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tpat))
, (BuiltinId
builtinLevel BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tLevelUniv)
, (BuiltinId
builtinWord64 BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tset)
, (BuiltinId
builtinInteger BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinIntegerPos, BuiltinId
builtinIntegerNegSuc])
, (BuiltinId
builtinIntegerPos BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tinteger))
, (BuiltinId
builtinIntegerNegSuc BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tinteger))
, (BuiltinId
builtinFloat BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tset)
, (BuiltinId
builtinChar BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tset)
, (BuiltinId
builtinString BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tset)
, (BuiltinId
builtinQName BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tset)
, (BuiltinId
builtinAgdaMeta BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tset)
, (BuiltinId
builtinIO BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *). Applicative m => m Type
tset forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Applicative m => m Type
tset))
, (BuiltinId
builtinPath BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Maybe (TCM Type) -> (Term -> Type -> TCM ()) -> BuiltinDescriptor
BuiltinUnknown
(forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
"" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0) forall a b. (a -> b) -> a -> b
$
(forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
(forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
1)))
Term -> Type -> TCM ()
verifyPath)
, (BuiltinId
builtinPathP BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
nPi [Char]
"A" (forall {t}. TCMT IO (Type'' t Term)
tinterval forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0)) forall a b. (a -> b) -> a -> b
$
(forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
(forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
1)))
, (BuiltinId
builtinIntervalUniv BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> BuiltinSort -> BuiltinDescriptor
BuiltinSort BuiltinSort
SortIntervalUniv)
, (BuiltinId
builtinInterval BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData (Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
"" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
(forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort forall t. Sort' t
IntervalUniv)) [BuiltinId
builtinIZero,BuiltinId
builtinIOne])
, (BuiltinId
builtinSub BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"A" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a) (Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"φ" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall {t}. TCMT IO (Type'' t Term)
tinterval) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi ->
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el's NamesT (TCMT IO) Term
a (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPartial forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bA) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (Level -> Type
ssort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. t -> Level' t
atomicLevel forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a)
))
, (BuiltinId
builtinSubIn BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"A" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a) (Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"φ" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall {t}. TCMT IO (Type'' t Term)
tinterval) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"x" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
bA) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
x ->
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el's NamesT (TCMT IO) Term
a forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSub forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"o" (\ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Term
x)))
, (BuiltinId
builtinIZero BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons forall {t}. TCMT IO (Type'' t Term)
tinterval)
, (BuiltinId
builtinIOne BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons forall {t}. TCMT IO (Type'' t Term)
tinterval)
, (BuiltinId
builtinPartial BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimPartial (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()))
, (BuiltinId
builtinPartialP BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimPartialP (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()))
, (BuiltinId
builtinIsOne BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall {t}. TCMT IO (Type'' t Term)
tinterval forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *) a. Monad m => a -> m a
return (Level -> Type
ssort forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
0)))
, (BuiltinId
builtinItIsOne BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall (m :: * -> *). Functor m => m Term -> m Type
elSSet forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne))
, (BuiltinId
builtinIsOne1 BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"i" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall {t}. TCMT IO (Type'' t Term)
tinterval) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
i ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"j" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall {t}. TCMT IO (Type'' t Term)
tinterval) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
j ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"i1" (forall (m :: * -> *). Functor m => m Term -> m Type
elSSet forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
i1 ->
(forall (m :: * -> *). Functor m => m Term -> m Type
elSSet forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
j))))
, (BuiltinId
builtinIsOne2 BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"i" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall {t}. TCMT IO (Type'' t Term)
tinterval) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
i ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"j" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall {t}. TCMT IO (Type'' t Term)
tinterval) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
j ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"j1" (forall (m :: * -> *). Functor m => m Term -> m Type
elSSet forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
j) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
j1 ->
(forall (m :: * -> *). Functor m => m Term -> m Type
elSSet forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
j))))
, (BuiltinId
builtinIsOneEmpty BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"l" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
l ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"A" (forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"o" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ ->
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
l) (Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
l)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"o" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero) (\ NamesT (TCMT IO) Term
o ->
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
l forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
Applicative m =>
ArgInfo -> m Term -> m Term -> m Term
gApply' (forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
Irrelevant ArgInfo
defaultArgInfo) NamesT (TCMT IO) Term
bA NamesT (TCMT IO) Term
o)))
, (BuiltinId
builtinId BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData (forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
(>>) (Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
"") forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0) forall a b. (a -> b) -> a -> b
$
(forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
(forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
1)) [BuiltinId
builtinReflId])
, (BuiltinId
builtinReflId BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
(>>) (Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
"") forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
l ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"A" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
l) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"x" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
l NamesT (TCMT IO) Term
bA) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
x ->
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
l (forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primId forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
x)))
, (BuiltinId
builtinEquiv BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Maybe (TCM Type) -> (Term -> Type -> TCM ()) -> BuiltinDescriptor
BuiltinUnknown (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
"" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"l" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"l'" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
b ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"A" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a) forall a b. (a -> b) -> a -> b
$ \NamesT (TCMT IO) Term
bA ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"B" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
b) forall a b. (a -> b) -> a -> b
$ \NamesT (TCMT IO) Term
bB ->
((Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
b))
))
(forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()))
, (BuiltinId
builtinEquivFun BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Maybe (TCM Type) -> (Term -> Type -> TCM ()) -> BuiltinDescriptor
BuiltinUnknown (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
"" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"l" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"l'" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
b ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"A" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a) forall a b. (a -> b) -> a -> b
$ \NamesT (TCMT IO) Term
bA ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"B" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
b) forall a b. (a -> b) -> a -> b
$ \NamesT (TCMT IO) Term
bB ->
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
b) (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquiv forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
b forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bB) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
(forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
b NamesT (TCMT IO) Term
bB)
))
(forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()))
, (BuiltinId
builtinEquivProof BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Maybe (TCM Type) -> (Term -> Type -> TCM ()) -> BuiltinDescriptor
BuiltinUnknown (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
"" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"l" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
la ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"l'" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
lb ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"A" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
la) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"B" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
lb) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bB ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"e" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
lb)
(forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquiv forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bB)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
e -> do
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"b" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
lb NamesT (TCMT IO) Term
bB) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
b -> do
let f :: NamesT (TCMT IO) Term
f = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquivFun forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bB forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
e
lub :: NamesT (TCMT IO) Term
lub = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
lb
fiber :: NamesT (TCMT IO) Type
fiber = forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
lub
(forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSigma forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bA
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"a" (\ NamesT (TCMT IO) Term
a ->
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPath forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bB forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
f forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
b))
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"φ" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall {t}. TCMT IO (Type'' t Term)
tinterval) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi ->
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"f" (forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"o" NamesT (TCMT IO) Term
phi (\ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Type
fiber)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
pfib ->
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
lub (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSub forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lub forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t a. Type'' t a -> a
unEl NamesT (TCMT IO) Type
fiber forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
pfib)
))
(forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()))
, (BuiltinId
builtinTranspProof BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Maybe (TCM Type) -> (Term -> Type -> TCM ()) -> BuiltinDescriptor
BuiltinUnknown (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
"" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"l" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
la -> do
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"e" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall {t}. TCMT IO (Type'' t Term)
tinterval forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
la)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
e -> do
let lb :: NamesT (TCMT IO) Term
lb = NamesT (TCMT IO) Term
la; bA :: NamesT (TCMT IO) Term
bA = NamesT (TCMT IO) Term
e forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero; bB :: NamesT (TCMT IO) Term
bB = NamesT (TCMT IO) Term
e forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"φ" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall {t}. TCMT IO (Type'' t Term)
tinterval) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi -> do
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"a" (forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"o" NamesT (TCMT IO) Term
phi (\ NamesT (TCMT IO) Term
_ -> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
bA)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a -> do
let f :: NamesT (TCMT IO) Term
f = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrans forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" (\ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
e forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
z :: NamesT (TCMT IO) Term
z = forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Term
f forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
o)
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"b" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el's NamesT (TCMT IO) Term
lb (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSub forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bB forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
z)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
b' -> do
let b :: NamesT (TCMT IO) Term
b = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSubOut forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bB forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
z forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
b'
fiber :: NamesT (TCMT IO) Type
fiber = forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
la
(forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSigma forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bA
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"a" (\ NamesT (TCMT IO) Term
a ->
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPath forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bB forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
f forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
b))
NamesT (TCMT IO) Type
fiber
))
(forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()))
, (BuiltinId
builtinAgdaSort BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset
[ BuiltinId
builtinAgdaSortSet, BuiltinId
builtinAgdaSortLit
, BuiltinId
builtinAgdaSortProp, BuiltinId
builtinAgdaSortPropLit
, BuiltinId
builtinAgdaSortInf, BuiltinId
builtinAgdaSortUnsupported])
, (BuiltinId
builtinAgdaTerm BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset
[ BuiltinId
builtinAgdaTermVar, BuiltinId
builtinAgdaTermLam, BuiltinId
builtinAgdaTermExtLam
, BuiltinId
builtinAgdaTermDef, BuiltinId
builtinAgdaTermCon
, BuiltinId
builtinAgdaTermPi, BuiltinId
builtinAgdaTermSort
, BuiltinId
builtinAgdaTermLit, BuiltinId
builtinAgdaTermMeta
, BuiltinId
builtinAgdaTermUnsupported])
, BuiltinId
builtinAgdaErrorPart BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [ BuiltinId
builtinAgdaErrorPartString, BuiltinId
builtinAgdaErrorPartTerm, BuiltinId
builtinAgdaErrorPartPatt, BuiltinId
builtinAgdaErrorPartName ]
, BuiltinId
builtinAgdaErrorPartString BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
terrorpart)
, BuiltinId
builtinAgdaErrorPartTerm BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
terrorpart)
, BuiltinId
builtinAgdaErrorPartPatt BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tpat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
terrorpart)
, BuiltinId
builtinAgdaErrorPartName BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
terrorpart)
, BuiltinId
builtinAgdaBlocker BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [ BuiltinId
builtinAgdaBlockerAll, BuiltinId
builtinAgdaBlockerAny, BuiltinId
builtinAgdaBlockerMeta ]
, BuiltinId
builtinAgdaBlockerAny BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tblocker forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tblocker)
, BuiltinId
builtinAgdaBlockerAll BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tblocker forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tblocker)
, BuiltinId
builtinAgdaBlockerMeta BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tmeta forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tblocker)
, (BuiltinId
builtinHiding BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinHidden, BuiltinId
builtinInstance, BuiltinId
builtinVisible])
, (BuiltinId
builtinRelevance BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinRelevant, BuiltinId
builtinIrrelevant])
, (BuiltinId
builtinRelevant BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
trelevance)
, (BuiltinId
builtinIrrelevant BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
trelevance)
, (BuiltinId
builtinQuantity BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinQuantity0, BuiltinId
builtinQuantityω])
, (BuiltinId
builtinQuantity0 BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tquantity)
, (BuiltinId
builtinQuantityω BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tquantity)
, (BuiltinId
builtinModality BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinModalityConstructor])
, (BuiltinId
builtinModalityConstructor BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
trelevance forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tquantity forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tmodality))
, BuiltinId
builtinAssoc BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinAssocLeft, BuiltinId
builtinAssocRight, BuiltinId
builtinAssocNon]
, BuiltinId
builtinAssocLeft BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tassoc
, BuiltinId
builtinAssocRight BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tassoc
, BuiltinId
builtinAssocNon BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tassoc
, BuiltinId
builtinPrecedence BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinPrecRelated, BuiltinId
builtinPrecUnrelated]
, BuiltinId
builtinPrecRelated BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tfloat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tprec)
, BuiltinId
builtinPrecUnrelated BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tprec
, BuiltinId
builtinFixity BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinFixityFixity]
, BuiltinId
builtinFixityFixity BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tassoc forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tprec forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tfixity)
, (BuiltinId
builtinRewrite BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Maybe (TCM Type) -> (Term -> Type -> TCM ()) -> BuiltinDescriptor
BuiltinUnknown forall a. Maybe a
Nothing Term -> Type -> TCM ()
verifyBuiltinRewrite)
, (BuiltinId
builtinNil BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" forall (m :: * -> *). Applicative m => m Type
tset (forall (m :: * -> *). Functor m => m Term -> m Type
el (TCMT IO Term -> TCMT IO Term
list TCMT IO Term
v0))))
, (BuiltinId
builtinCons BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" forall (m :: * -> *). Applicative m => m Type
tset (TCM Type
tv0 forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Functor m => m Term -> m Type
el (TCMT IO Term -> TCMT IO Term
list TCMT IO Term
v0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Functor m => m Term -> m Type
el (TCMT IO Term -> TCMT IO Term
list TCMT IO Term
v0))))
, (BuiltinId
builtinNothing BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" forall (m :: * -> *). Applicative m => m Type
tset (forall (m :: * -> *). Functor m => m Term -> m Type
el (TCMT IO Term -> TCMT IO Term
tMaybe TCMT IO Term
v0))))
, (BuiltinId
builtinJust BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" forall (m :: * -> *). Applicative m => m Type
tset (TCM Type
tv0 forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Functor m => m Term -> m Type
el (TCMT IO Term -> TCMT IO Term
tMaybe TCMT IO Term
v0))))
, (BuiltinId
builtinZero BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tnat)
, (BuiltinId
builtinSuc BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tnat))
, (BuiltinId
builtinTrue BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tbool)
, (BuiltinId
builtinFalse BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tbool)
, (BuiltinId
builtinArgArg BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" forall (m :: * -> *). Applicative m => m Type
tset (TCM Type
targinfo forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tv0 forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
tv0)))
, (BuiltinId
builtinAbsAbs BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" forall (m :: * -> *). Applicative m => m Type
tset (TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tv0 forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *} {t}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m (Type'' t Term) -> m Type
tabs TCM Type
tv0)))
, (BuiltinId
builtinArgArgInfo BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
thiding forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tmodality forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
targinfo))
, (BuiltinId
builtinAgdaTermVar BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
targs forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm))
, (BuiltinId
builtinAgdaTermLam BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
thiding forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *} {t}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m (Type'' t Term) -> m Type
tabs TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm))
, (BuiltinId
builtinAgdaTermExtLam BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tclause forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
targs forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm))
, (BuiltinId
builtinAgdaTermDef BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
targs forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm))
, (BuiltinId
builtinAgdaTermCon BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
targs forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm))
, (BuiltinId
builtinAgdaTermPi BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
ttype forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *} {t}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m (Type'' t Term) -> m Type
tabs TCM Type
ttype forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm))
, (BuiltinId
builtinAgdaTermSort BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tsort forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm))
, (BuiltinId
builtinAgdaTermLit BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tliteral forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm))
, (BuiltinId
builtinAgdaTermMeta BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tmeta forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
targs forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm))
, (BuiltinId
builtinAgdaTermUnsupported BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tterm)
, (BuiltinId
builtinAgdaLitNat BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
, (BuiltinId
builtinAgdaLitWord64 BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tword64 forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
, (BuiltinId
builtinAgdaLitFloat BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tfloat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
, (BuiltinId
builtinAgdaLitChar BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tchar forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
, (BuiltinId
builtinAgdaLitString BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
, (BuiltinId
builtinAgdaLitQName BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
, (BuiltinId
builtinAgdaLitMeta BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tmeta forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
, (BuiltinId
builtinHidden BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
thiding)
, (BuiltinId
builtinInstance BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
thiding)
, (BuiltinId
builtinVisible BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
thiding)
, (BuiltinId
builtinSizeUniv BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate TCM Type
tsetOmega)
, (BuiltinId
builtinSize BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tSizeUniv)
, (BuiltinId
builtinSizeLt BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tsize forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
..--> forall (m :: * -> *). Applicative m => m Type
tSizeUniv))
, (BuiltinId
builtinSizeSuc BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tsize forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsize))
, (BuiltinId
builtinSizeInf BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate TCM Type
tsize)
, (BuiltinId
builtinSizeMax BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tsize forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsize forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsize))
, (BuiltinId
builtinAgdaSortSet BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsort))
, (BuiltinId
builtinAgdaSortLit BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsort))
, (BuiltinId
builtinAgdaSortProp BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsort))
, (BuiltinId
builtinAgdaSortPropLit BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsort))
, (BuiltinId
builtinAgdaSortInf BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsort))
, (BuiltinId
builtinAgdaSortUnsupported BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tsort)
, (BuiltinId
builtinNatPlus BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimNatPlus Term -> TCM ()
verifyPlus)
, (BuiltinId
builtinNatMinus BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimNatMinus Term -> TCM ()
verifyMinus)
, (BuiltinId
builtinNatTimes BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimNatTimes Term -> TCM ()
verifyTimes)
, (BuiltinId
builtinNatDivSucAux BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimNatDivSucAux Term -> TCM ()
verifyDivSucAux)
, (BuiltinId
builtinNatModSucAux BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimNatModSucAux Term -> TCM ()
verifyModSucAux)
, (BuiltinId
builtinNatEquals BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimNatEquality Term -> TCM ()
verifyEquals)
, (BuiltinId
builtinNatLess BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimNatLess Term -> TCM ()
verifyLess)
, (BuiltinId
builtinLevelUniv BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> BuiltinSort -> BuiltinDescriptor
BuiltinSort BuiltinSort
SortLevelUniv)
, (BuiltinId
builtinLevelZero BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimLevelZero (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()))
, (BuiltinId
builtinLevelSuc BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimLevelSuc (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()))
, (BuiltinId
builtinLevelMax BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimLevelMax forall {m :: * -> *} {p}. Monad m => p -> m ()
verifyMax)
, (BuiltinId
builtinProp BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> BuiltinSort -> BuiltinDescriptor
BuiltinSort BuiltinSort
SortProp)
, (BuiltinId
builtinSet BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> BuiltinSort -> BuiltinDescriptor
BuiltinSort BuiltinSort
SortSet)
, (BuiltinId
builtinStrictSet BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> BuiltinSort -> BuiltinDescriptor
BuiltinSort BuiltinSort
SortStrictSet)
, (BuiltinId
builtinPropOmega BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> BuiltinSort -> BuiltinDescriptor
BuiltinSort BuiltinSort
SortPropOmega)
, (BuiltinId
builtinSetOmega BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> BuiltinSort -> BuiltinDescriptor
BuiltinSort BuiltinSort
SortSetOmega)
, (BuiltinId
builtinSSetOmega BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> BuiltinSort -> BuiltinDescriptor
BuiltinSort BuiltinSort
SortStrictSetOmega)
, (BuiltinId
builtinAgdaClause BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinAgdaClauseClause, BuiltinId
builtinAgdaClauseAbsurd])
, (BuiltinId
builtinAgdaClauseClause BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
ttelescope forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
tpat) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tclause))
, (BuiltinId
builtinAgdaClauseAbsurd BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
ttelescope forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
tpat) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tclause))
, (BuiltinId
builtinAgdaDefinition BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinAgdaDefinitionFunDef
,BuiltinId
builtinAgdaDefinitionDataDef
,BuiltinId
builtinAgdaDefinitionDataConstructor
,BuiltinId
builtinAgdaDefinitionRecordDef
,BuiltinId
builtinAgdaDefinitionPostulate
,BuiltinId
builtinAgdaDefinitionPrimitive])
, (BuiltinId
builtinAgdaDefinitionFunDef BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tclause forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tdefn))
, (BuiltinId
builtinAgdaDefinitionDataDef BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tdefn))
, (BuiltinId
builtinAgdaDefinitionDataConstructor BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tdefn))
, (BuiltinId
builtinAgdaDefinitionRecordDef BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
tqname) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tdefn))
, (BuiltinId
builtinAgdaDefinitionPostulate BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tdefn)
, (BuiltinId
builtinAgdaDefinitionPrimitive BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tdefn)
, BuiltinId
builtinAgdaTCM BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0 forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0)
, BuiltinId
builtinAgdaTCMReturn BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$
forall {f :: * -> *} {a}.
Functor f =>
Int -> f a -> f (Type'' Term a)
elV Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
, BuiltinId
builtinAgdaTCMBind BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"b" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
1) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"B" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
1) forall a b. (a -> b) -> a -> b
$
forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
3 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
1) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (forall {f :: * -> *} {a}.
Functor f =>
Int -> f a -> f (Type'' Term a)
elV Int
3 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
1) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
2 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0)) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
2 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
, BuiltinId
builtinAgdaTCMUnify BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
, BuiltinId
builtinAgdaTCMTypeError BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$ forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
terrorpart forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
, BuiltinId
builtinAgdaTCMInferType BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm)
, BuiltinId
builtinAgdaTCMCheckType BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
ttype forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm)
, BuiltinId
builtinAgdaTCMNormalise BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm)
, BuiltinId
builtinAgdaTCMReduce BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm)
, BuiltinId
builtinAgdaTCMCatchError BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$
forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
, BuiltinId
builtinAgdaTCMGetContext BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ (forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Type
ttelescope))
, BuiltinId
builtinAgdaTCMExtendContext BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$
TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
ttype forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
, BuiltinId
builtinAgdaTCMInContext BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$
TCM Type
ttelescope forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
, BuiltinId
builtinAgdaTCMFreshName BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQName)
, BuiltinId
builtinAgdaTCMDeclareDef BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
ttype forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
, BuiltinId
builtinAgdaTCMDeclarePostulate BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
ttype forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
, BuiltinId
builtinAgdaTCMDeclareData BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
ttype forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
, BuiltinId
builtinAgdaTCMDefineData BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist (forall {m :: * -> *} {t} {t}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
-> m Term -> m (Type'' t Term) -> m (Type'' t Term) -> m Type
tpair forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero TCM Type
tqname TCM Type
ttype) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
, BuiltinId
builtinAgdaTCMDefineFun BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tclause forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
, BuiltinId
builtinAgdaTCMGetType BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm)
, BuiltinId
builtinAgdaTCMGetDefinition BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinition)
, BuiltinId
builtinAgdaTCMQuoteTerm BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$ forall {f :: * -> *} {a}.
Functor f =>
Int -> f a -> f (Type'' Term a)
elV Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm)
, BuiltinId
builtinAgdaTCMUnquoteTerm BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$ TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
, BuiltinId
builtinAgdaTCMQuoteOmegaTerm BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" TCM Type
tsetOmega forall a b. (a -> b) -> a -> b
$ (forall (m :: * -> *). Functor m => m Term -> m Type
elInf forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm)
, BuiltinId
builtinAgdaTCMBlock BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$ TCM Type
tblocker forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
, BuiltinId
builtinAgdaTCMCommit BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
, BuiltinId
builtinAgdaTCMIsMacro BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primBool)
, BuiltinId
builtinAgdaTCMWithNormalisation BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$ TCM Type
tbool forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
, BuiltinId
builtinAgdaTCMWithReconstructed BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$ TCM Type
tbool forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
, BuiltinId
builtinAgdaTCMWithExpandLast BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$ TCM Type
tbool forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
, BuiltinId
builtinAgdaTCMWithReduceDefs BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$ (forall {m :: * -> *} {t} {t}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
-> m Term -> m (Type'' t Term) -> m (Type'' t Term) -> m Type
tpair forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero TCM Type
tbool (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tqname)) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
, BuiltinId
builtinAgdaTCMAskNormalisation BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ (forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Type
tbool))
, BuiltinId
builtinAgdaTCMAskReconstructed BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ (forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Type
tbool))
, BuiltinId
builtinAgdaTCMAskExpandLast BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ (forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Type
tbool))
, BuiltinId
builtinAgdaTCMAskReduceDefs BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ (forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall {m :: * -> *} {t} {t}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
-> m Term -> m (Type'' t Term) -> m (Type'' t Term) -> m Type
tpair forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero TCM Type
tbool (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tqname))))
, BuiltinId
builtinAgdaTCMFormatErrorParts BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
terrorpart forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primString)
, BuiltinId
builtinAgdaTCMDebugPrint BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
terrorpart forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
, BuiltinId
builtinAgdaTCMNoConstraints BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$ forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
, BuiltinId
builtinAgdaTCMRunSpeculative BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$
forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSigma forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
1 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Char] -> a -> Abs a
Abs [Char]
"_" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primBool)) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
, BuiltinId
builtinAgdaTCMExec BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ (forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSigma forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNat forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@>
(ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Char] -> a -> Abs a
Abs [Char]
"_" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSigma forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primString forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@>
(ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Char] -> a -> Abs a
Abs [Char]
"_" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primString)))))
, BuiltinId
builtinAgdaTCMGetInstances BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tmeta forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ (TCMT IO Term -> TCMT IO Term
list forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm))
, BuiltinId
builtinAgdaTCMPragmaForeign BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
, BuiltinId
builtinAgdaTCMPragmaCompile BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
]
where
|-> :: BuiltinId -> BuiltinDescriptor -> BuiltinInfo
(|->) = BuiltinId -> BuiltinDescriptor -> BuiltinInfo
BuiltinInfo
v0 :: TCM Term
v0 :: TCMT IO Term
v0 = forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0
tv0 :: TCM Type
tv0 :: TCM Type
tv0 = forall (m :: * -> *). Functor m => m Term -> m Type
el TCMT IO Term
v0
arg :: TCM Term -> TCM Term
arg :: TCMT IO Term -> TCMT IO Term
arg TCMT IO Term
t = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> TCMT IO Term
t
elV :: Int -> f a -> f (Type'' Term a)
elV Int
x f a
a = forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
a
tsetL :: Int -> m Type
tsetL Int
l = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort (Int -> Sort
varSort Int
l)
tsetOmega :: TCM Type
tsetOmega = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ forall t. Univ -> Integer -> Sort' t
Inf Univ
UType Integer
0
tlevel :: TCM Type
tlevel = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel
tlist :: TCMT IO (Type'' t Term) -> TCM Type
tlist TCMT IO (Type'' t Term)
x = forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> TCMT IO Term
list (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t a. Type'' t a -> a
unEl TCMT IO (Type'' t Term)
x)
tmaybe :: TCMT IO (Type'' t Term) -> TCM Type
tmaybe TCMT IO (Type'' t Term)
x = forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> TCMT IO Term
tMaybe (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t a. Type'' t a -> a
unEl TCMT IO (Type'' t Term)
x)
tpair :: m Term
-> m Term -> m (Type'' t Term) -> m (Type'' t Term) -> m Type
tpair m Term
lx m Term
ly m (Type'' t Term)
x m (Type'' t Term)
y = forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSigma
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> m Term
lx
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> m Term
ly
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t a. Type'' t a -> a
unEl m (Type'' t Term)
x
forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Char] -> a -> Abs a
NoAbs [Char]
"_" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t a. Type'' t a -> a
unEl m (Type'' t Term)
y)
targ :: TCMT IO (Type'' t Term) -> TCM Type
targ TCMT IO (Type'' t Term)
x = forall (m :: * -> *). Functor m => m Term -> m Type
el (TCMT IO Term -> TCMT IO Term
arg (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t a. Type'' t a -> a
unEl TCMT IO (Type'' t Term)
x))
tabs :: m (Type'' t Term) -> m Type
tabs m (Type'' t Term)
x = forall (m :: * -> *). Functor m => m Term -> m Type
el (forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAbs forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t a. Type'' t a -> a
unEl m (Type'' t Term)
x)
targs :: TCM Type
targs = forall (m :: * -> *). Functor m => m Term -> m Type
el (TCMT IO Term -> TCMT IO Term
list (TCMT IO Term -> TCMT IO Term
arg forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm))
tterm :: TCM Type
tterm = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm
terrorpart :: TCM Type
terrorpart = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaErrorPart
tnat :: TCM Type
tnat = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNat
tword64 :: TCM Type
tword64 = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primWord64
tinteger :: TCM Type
tinteger = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInteger
tfloat :: TCM Type
tfloat = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFloat
tchar :: TCM Type
tchar = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primChar
tstring :: TCM Type
tstring = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primString
tqname :: TCM Type
tqname = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQName
tmeta :: TCM Type
tmeta = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaMeta
tblocker :: TCM Type
tblocker = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaBlocker
tsize :: TCM Type
tsize = forall t a. Sort' t -> a -> Type'' t a
El Sort
sSizeUniv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSize
tbool :: TCM Type
tbool = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primBool
thiding :: TCM Type
thiding = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHiding
trelevance :: TCM Type
trelevance = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRelevance
tquantity :: TCM Type
tquantity = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQuantity
tmodality :: TCM Type
tmodality = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primModality
tassoc :: TCM Type
tassoc = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAssoc
tprec :: TCM Type
tprec = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPrecedence
tfixity :: TCM Type
tfixity = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFixity
targinfo :: TCM Type
targinfo = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArgInfo
ttype :: TCM Type
ttype = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm
tsort :: TCM Type
tsort = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSort
tdefn :: TCM Type
tdefn = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinition
tliteral :: TCM Type
tliteral = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLiteral
tpat :: TCM Type
tpat = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPattern
tclause :: TCM Type
tclause = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaClause
ttelescope :: TCM Type
ttelescope = forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist (forall {m :: * -> *} {t} {t}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
-> m Term -> m (Type'' t Term) -> m (Type'' t Term) -> m Type
tpair forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero TCM Type
tstring (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
ttype))
tTCM :: Int -> f Term -> f Type
tTCM Int
l f Term
a = forall {f :: * -> *} {a}.
Functor f =>
Int -> f a -> f (Type'' Term a)
elV Int
l (forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCM forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> f Term
a)
tTCM_ :: m Term -> m Type
tTCM_ m Term
a = forall (m :: * -> *). Functor m => m Term -> m Type
el (forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCM forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> m Term
a)
tinterval :: TCMT IO (Type'' t Term)
tinterval = forall t a. Sort' t -> a -> Type'' t a
El forall t. Sort' t
IntervalUniv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInterval
verifyPlus :: Term -> TCM ()
verifyPlus Term
plus =
forall {a}.
Names
-> ((Term -> Term -> Term)
-> Term
-> (Term -> Term)
-> (Term -> Term -> TCM ())
-> (Term -> Term -> TCM ())
-> ([TCM ()] -> TCM ())
-> TCM a)
-> TCM a
verify [[Char]
"n",[Char]
"m"] forall a b. (a -> b) -> a -> b
$ \Term -> Term -> Term
(@@) Term
zero Term -> Term
suc Term -> Term -> TCM ()
(==) Term -> Term -> TCM ()
(===) [TCM ()] -> TCM ()
choice -> do
let m :: Term
m = Int -> Term
var Int
0
n :: Term
n = Int -> Term
var Int
1
Term
x + :: Term -> Term -> Term
+ Term
y = Term
plus Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
y
[TCM ()] -> TCM ()
choice
[ do Term
n Term -> Term -> Term
+ Term
zero Term -> Term -> TCM ()
== Term
n
Term
n Term -> Term -> Term
+ Term -> Term
suc Term
m Term -> Term -> TCM ()
== Term -> Term
suc (Term
n Term -> Term -> Term
+ Term
m)
, do Term -> Term
suc Term
n Term -> Term -> Term
+ Term
m Term -> Term -> TCM ()
== Term -> Term
suc (Term
n Term -> Term -> Term
+ Term
m)
Term
zero Term -> Term -> Term
+ Term
m Term -> Term -> TCM ()
== Term
m
]
verifyMinus :: Term -> TCM ()
verifyMinus Term
minus =
forall {a}.
Names
-> ((Term -> Term -> Term)
-> Term
-> (Term -> Term)
-> (Term -> Term -> TCM ())
-> (Term -> Term -> TCM ())
-> ([TCM ()] -> TCM ())
-> TCM a)
-> TCM a
verify [[Char]
"n",[Char]
"m"] forall a b. (a -> b) -> a -> b
$ \Term -> Term -> Term
(@@) Term
zero Term -> Term
suc Term -> Term -> TCM ()
(==) Term -> Term -> TCM ()
(===) [TCM ()] -> TCM ()
choice -> do
let m :: Term
m = Int -> Term
var Int
0
n :: Term
n = Int -> Term
var Int
1
Term
x - :: Term -> Term -> Term
- Term
y = Term
minus Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
y
Term
zero Term -> Term -> Term
- Term
zero Term -> Term -> TCM ()
== Term
zero
Term
zero Term -> Term -> Term
- Term -> Term
suc Term
m Term -> Term -> TCM ()
== Term
zero
Term -> Term
suc Term
n Term -> Term -> Term
- Term
zero Term -> Term -> TCM ()
== Term -> Term
suc Term
n
Term -> Term
suc Term
n Term -> Term -> Term
- Term -> Term
suc Term
m Term -> Term -> TCM ()
== (Term
n Term -> Term -> Term
- Term
m)
verifyTimes :: Term -> TCM ()
verifyTimes Term
times = do
Term
plus <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNatPlus
forall {a}.
Names
-> ((Term -> Term -> Term)
-> Term
-> (Term -> Term)
-> (Term -> Term -> TCM ())
-> (Term -> Term -> TCM ())
-> ([TCM ()] -> TCM ())
-> TCM a)
-> TCM a
verify [[Char]
"n",[Char]
"m"] forall a b. (a -> b) -> a -> b
$ \Term -> Term -> Term
(@@) Term
zero Term -> Term
suc Term -> Term -> TCM ()
(==) Term -> Term -> TCM ()
(===) [TCM ()] -> TCM ()
choice -> do
let m :: Term
m = Int -> Term
var Int
0
n :: Term
n = Int -> Term
var Int
1
Term
x + :: Term -> Term -> Term
+ Term
y = Term
plus Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
y
Term
x * :: Term -> Term -> Term
* Term
y = Term
times Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
y
[TCM ()] -> TCM ()
choice
[ do Term
n Term -> Term -> Term
* Term
zero Term -> Term -> TCM ()
== Term
zero
[TCM ()] -> TCM ()
choice [ (Term
n Term -> Term -> Term
* Term -> Term
suc Term
m) Term -> Term -> TCM ()
== (Term
n Term -> Term -> Term
+ (Term
n Term -> Term -> Term
* Term
m))
, (Term
n Term -> Term -> Term
* Term -> Term
suc Term
m) Term -> Term -> TCM ()
== ((Term
n Term -> Term -> Term
* Term
m) Term -> Term -> Term
+ Term
n)
]
, do Term
zero Term -> Term -> Term
* Term
n Term -> Term -> TCM ()
== Term
zero
[TCM ()] -> TCM ()
choice [ (Term -> Term
suc Term
n Term -> Term -> Term
* Term
m) Term -> Term -> TCM ()
== (Term
m Term -> Term -> Term
+ (Term
n Term -> Term -> Term
* Term
m))
, (Term -> Term
suc Term
n Term -> Term -> Term
* Term
m) Term -> Term -> TCM ()
== ((Term
n Term -> Term -> Term
* Term
m) Term -> Term -> Term
+ Term
m)
]
]
verifyDivSucAux :: Term -> TCM ()
verifyDivSucAux Term
dsAux =
forall {a}.
Names
-> ((Term -> Term -> Term)
-> Term
-> (Term -> Term)
-> (Term -> Term -> TCM ())
-> (Term -> Term -> TCM ())
-> ([TCM ()] -> TCM ())
-> TCM a)
-> TCM a
verify [[Char]
"k",[Char]
"m",[Char]
"n",[Char]
"j"] forall a b. (a -> b) -> a -> b
$ \Term -> Term -> Term
(@@) Term
zero Term -> Term
suc Term -> Term -> TCM ()
(==) Term -> Term -> TCM ()
(===) [TCM ()] -> TCM ()
choice -> do
let aux :: Term -> Term -> Term -> Term -> Term
aux Term
k Term
m Term
n Term
j = Term
dsAux Term -> Term -> Term
@@ Term
k Term -> Term -> Term
@@ Term
m Term -> Term -> Term
@@ Term
n Term -> Term -> Term
@@ Term
j
k :: Term
k = Int -> Term
var Int
0
m :: Term
m = Int -> Term
var Int
1
n :: Term
n = Int -> Term
var Int
2
j :: Term
j = Int -> Term
var Int
3
Term -> Term -> Term -> Term -> Term
aux Term
k Term
m Term
zero Term
j Term -> Term -> TCM ()
== Term
k
Term -> Term -> Term -> Term -> Term
aux Term
k Term
m (Term -> Term
suc Term
n) Term
zero Term -> Term -> TCM ()
== Term -> Term -> Term -> Term -> Term
aux (Term -> Term
suc Term
k) Term
m Term
n Term
m
Term -> Term -> Term -> Term -> Term
aux Term
k Term
m (Term -> Term
suc Term
n) (Term -> Term
suc Term
j) Term -> Term -> TCM ()
== Term -> Term -> Term -> Term -> Term
aux Term
k Term
m Term
n Term
j
verifyModSucAux :: Term -> TCM ()
verifyModSucAux Term
dsAux =
forall {a}.
Names
-> ((Term -> Term -> Term)
-> Term
-> (Term -> Term)
-> (Term -> Term -> TCM ())
-> (Term -> Term -> TCM ())
-> ([TCM ()] -> TCM ())
-> TCM a)
-> TCM a
verify [[Char]
"k",[Char]
"m",[Char]
"n",[Char]
"j"] forall a b. (a -> b) -> a -> b
$ \Term -> Term -> Term
(@@) Term
zero Term -> Term
suc Term -> Term -> TCM ()
(==) Term -> Term -> TCM ()
(===) [TCM ()] -> TCM ()
choice -> do
let aux :: Term -> Term -> Term -> Term -> Term
aux Term
k Term
m Term
n Term
j = Term
dsAux Term -> Term -> Term
@@ Term
k Term -> Term -> Term
@@ Term
m Term -> Term -> Term
@@ Term
n Term -> Term -> Term
@@ Term
j
k :: Term
k = Int -> Term
var Int
0
m :: Term
m = Int -> Term
var Int
1
n :: Term
n = Int -> Term
var Int
2
j :: Term
j = Int -> Term
var Int
3
Term -> Term -> Term -> Term -> Term
aux Term
k Term
m Term
zero Term
j Term -> Term -> TCM ()
== Term
k
Term -> Term -> Term -> Term -> Term
aux Term
k Term
m (Term -> Term
suc Term
n) Term
zero Term -> Term -> TCM ()
== Term -> Term -> Term -> Term -> Term
aux Term
zero Term
m Term
n Term
m
Term -> Term -> Term -> Term -> Term
aux Term
k Term
m (Term -> Term
suc Term
n) (Term -> Term
suc Term
j) Term -> Term -> TCM ()
== Term -> Term -> Term -> Term -> Term
aux (Term -> Term
suc Term
k) Term
m Term
n Term
j
verifyEquals :: Term -> TCM ()
verifyEquals Term
eq =
forall {a}.
Names
-> ((Term -> Term -> Term)
-> Term
-> (Term -> Term)
-> (Term -> Term -> TCM ())
-> (Term -> Term -> TCM ())
-> ([TCM ()] -> TCM ())
-> TCM a)
-> TCM a
verify [[Char]
"n",[Char]
"m"] forall a b. (a -> b) -> a -> b
$ \Term -> Term -> Term
(@@) Term
zero Term -> Term
suc Term -> Term -> TCM ()
(==) Term -> Term -> TCM ()
(===) [TCM ()] -> TCM ()
choice -> do
Term
true <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrue
Term
false <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFalse
let Term
x == :: Term -> Term -> Term
== Term
y = Term
eq Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
y
m :: Term
m = Int -> Term
var Int
0
n :: Term
n = Int -> Term
var Int
1
(Term
zero Term -> Term -> Term
== Term
zero ) Term -> Term -> TCM ()
=== Term
true
(Term -> Term
suc Term
n Term -> Term -> Term
== Term -> Term
suc Term
m) Term -> Term -> TCM ()
=== (Term
n Term -> Term -> Term
== Term
m)
(Term -> Term
suc Term
n Term -> Term -> Term
== Term
zero ) Term -> Term -> TCM ()
=== Term
false
(Term
zero Term -> Term -> Term
== Term -> Term
suc Term
n) Term -> Term -> TCM ()
=== Term
false
verifyLess :: Term -> TCM ()
verifyLess Term
leq =
forall {a}.
Names
-> ((Term -> Term -> Term)
-> Term
-> (Term -> Term)
-> (Term -> Term -> TCM ())
-> (Term -> Term -> TCM ())
-> ([TCM ()] -> TCM ())
-> TCM a)
-> TCM a
verify [[Char]
"n",[Char]
"m"] forall a b. (a -> b) -> a -> b
$ \Term -> Term -> Term
(@@) Term
zero Term -> Term
suc Term -> Term -> TCM ()
(==) Term -> Term -> TCM ()
(===) [TCM ()] -> TCM ()
choice -> do
Term
true <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrue
Term
false <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFalse
let Term
x < :: Term -> Term -> Term
< Term
y = Term
leq Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
y
m :: Term
m = Int -> Term
var Int
0
n :: Term
n = Int -> Term
var Int
1
(Term
n Term -> Term -> Term
< Term
zero) Term -> Term -> TCM ()
=== Term
false
(Term -> Term
suc Term
n Term -> Term -> Term
< Term -> Term
suc Term
m) Term -> Term -> TCM ()
=== (Term
n Term -> Term -> Term
< Term
m)
(Term
zero Term -> Term -> Term
< Term -> Term
suc Term
m) Term -> Term -> TCM ()
=== Term
true
verifyMax :: p -> m ()
verifyMax p
maxV = forall (m :: * -> *) a. Monad m => a -> m a
return ()
verify :: Names
-> ((Term -> Term -> Term)
-> Term
-> (Term -> Term)
-> (Term -> Term -> TCM ())
-> (Term -> Term -> TCM ())
-> ([TCM ()] -> TCM ())
-> TCM a)
-> TCM a
verify Names
xs = forall a.
TCMT IO Term
-> TCMT IO Term
-> TCMT IO Term
-> Names
-> ((Term -> Term -> Term)
-> Term
-> (Term -> Term)
-> (Term -> Term -> TCM ())
-> (Term -> Term -> TCM ())
-> ([TCM ()] -> TCM ())
-> TCM a)
-> TCM a
verify' forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNat forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primZero forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSuc Names
xs
verify' :: TCM Term -> TCM Term -> TCM Term ->
[String] -> ( (Term -> Term -> Term) -> Term -> (Term -> Term) ->
(Term -> Term -> TCM ()) ->
(Term -> Term -> TCM ()) ->
([TCM ()] -> TCM ()) -> TCM a) -> TCM a
verify' :: forall a.
TCMT IO Term
-> TCMT IO Term
-> TCMT IO Term
-> Names
-> ((Term -> Term -> Term)
-> Term
-> (Term -> Term)
-> (Term -> Term -> TCM ())
-> (Term -> Term -> TCM ())
-> ([TCM ()] -> TCM ())
-> TCM a)
-> TCM a
verify' TCMT IO Term
pNat TCMT IO Term
pZero TCMT IO Term
pSuc Names
xs (Term -> Term -> Term)
-> Term
-> (Term -> Term)
-> (Term -> Term -> TCM ())
-> (Term -> Term -> TCM ())
-> ([TCM ()] -> TCM ())
-> TCM a
f = do
Type
nat <- forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort
mkType Integer
0) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Term
pNat
Term
zero <- TCMT IO Term
pZero
Term
s <- TCMT IO Term
pSuc
let Term
x == :: Term -> Term -> TCM ()
== Term
y = forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
MonadFresh ProblemId m) =>
m a -> m a
noConstraints forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
nat Term
x Term
y
Term
x === :: Term -> Term -> m ()
=== Term
y = do Type
bool <- forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort
mkType Integer
0) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primBool
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
MonadFresh ProblemId m) =>
m a -> m a
noConstraints forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
bool Term
x Term
y
suc :: Term -> Term
suc Term
n = Term
s forall t. Apply t => t -> Term -> t
`apply1` Term
n
choice :: [TCMT IO a] -> TCMT IO a
choice = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\TCMT IO a
x TCMT IO a
y -> TCMT IO a
x forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ -> TCMT IO a
y)
[Name]
xs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ Names
xs
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([Name]
xs, forall a. Arg a -> Dom a
domFromArg forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg Type
nat) forall a b. (a -> b) -> a -> b
$ (Term -> Term -> Term)
-> Term
-> (Term -> Term)
-> (Term -> Term -> TCM ())
-> (Term -> Term -> TCM ())
-> ([TCM ()] -> TCM ())
-> TCM a
f forall t. Apply t => t -> Term -> t
apply1 Term
zero Term -> Term
suc Term -> Term -> TCM ()
(==) forall {m :: * -> *}.
(MonadWarning m, MonadMetaSolver m, MonadStatistics m,
MonadFresh ProblemId m, MonadFresh Int m) =>
Term -> Term -> m ()
(===) forall {a}. [TCMT IO a] -> TCMT IO a
choice
verifyPath :: Term -> Type -> TCM ()
verifyPath :: Term -> Type -> TCM ()
verifyPath Term
path Type
t = do
let hlam :: [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
hlam [Char]
n NamesT m Term -> NamesT m Term
t = forall (m :: * -> *).
MonadFail m =>
ArgInfo
-> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam (forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden ArgInfo
defaultArgInfo) [Char]
n NamesT m Term -> NamesT m Term
t
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
MonadFresh ProblemId m) =>
m a -> m a
noConstraints forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
t Term
path forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (
forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
hlam [Char]
"l" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
l -> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
hlam [Char]
"A" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA -> forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPathP forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" (\ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Term
bA))
inductiveCheck :: BuiltinId -> Int -> Term -> TCM (QName, Definition)
inductiveCheck :: BuiltinId -> Int -> Term -> TCM (QName, Definition)
inductiveCheck BuiltinId
b Int
n Term
t = do
forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Term -> TCM (Maybe QName)
headSymbol Term
t) TCM (QName, Definition)
no forall a b. (a -> b) -> a -> b
$ \QName
q -> do
Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
let yes :: TCM (QName, Definition)
yes = forall (m :: * -> *) a. Monad m => a -> m a
return (QName
q, Definition
def)
case Definition -> Defn
theDef Definition
def of
Datatype { dataCons :: Defn -> [QName]
dataCons = [QName]
cs }
| forall (t :: * -> *) a. Foldable t => t a -> Int
length [QName]
cs forall a. Eq a => a -> a -> Bool
== Int
n -> TCM (QName, Definition)
yes
| Bool
otherwise -> TCM (QName, Definition)
no
Record { recInduction :: Defn -> Maybe Induction
recInduction = Maybe Induction
ind } | Int
n forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& Maybe Induction
ind forall a. Eq a => a -> a -> Bool
/= forall a. a -> Maybe a
Just Induction
CoInductive -> TCM (QName, Definition)
yes
Defn
_ -> TCM (QName, Definition)
no
where
headSymbol :: Term -> TCM (Maybe QName)
headSymbol :: Term -> TCM (Maybe QName)
headSymbol Term
t = forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Def QName
q Elims
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just QName
q
Lam ArgInfo
_ Abs Term
b -> Term -> TCM (Maybe QName)
headSymbol forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp Abs Term
b HasCallStack => Term
__DUMMY_TERM__
Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
no :: TCM (QName, Definition)
no
| Int
n forall a. Eq a => a -> a -> Bool
== Int
1 = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ Names -> [Char]
unwords
[ [Char]
"The builtin", forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
b
, [Char]
"must be a datatype with a single constructor"
, [Char]
"or an (inductive) record type"
]
| Bool
otherwise = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ Names -> [Char]
unwords
[ [Char]
"The builtin", forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
b
, [Char]
"must be a datatype with", forall a. Show a => a -> [Char]
show Int
n
, [Char]
"constructors"
]
bindPostulatedName ::
BuiltinId -> ResolvedName -> (QName -> Definition -> TCM Term) -> TCM ()
bindPostulatedName :: BuiltinId
-> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
bindPostulatedName BuiltinId
builtin ResolvedName
x QName -> Definition -> TCMT IO Term
m = do
QName
q <- ResolvedName -> TCMT IO QName
getName ResolvedName
x
Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
case Definition -> Defn
theDef Definition
def of
Axiom {} -> BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
builtin forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> Definition -> TCMT IO Term
m QName
q Definition
def
Defn
_ -> forall (m :: * -> *) a. MonadTCError m => m a
err
where
err :: forall m a. MonadTCError m => m a
err :: forall (m :: * -> *) a. MonadTCError m => m a
err = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
[Char]
"The argument to BUILTIN " forall a. [a] -> [a] -> [a]
++ forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
builtin forall a. [a] -> [a] -> [a]
++
[Char]
" must be a postulated name"
getName :: ResolvedName -> TCMT IO QName
getName = \case
DefinedName Access
_ AbstractName
d Suffix
NoSuffix -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AbstractName -> QName
anameName AbstractName
d
ResolvedName
_ -> forall (m :: * -> *) a. MonadTCError m => m a
err
addHaskellPragma :: QName -> String -> TCM ()
addHaskellPragma :: QName -> [Char] -> TCM ()
addHaskellPragma = [Char] -> QName -> [Char] -> TCM ()
addPragma [Char]
ghcBackendName
bindAndSetHaskellCode :: BuiltinId -> String -> Term -> TCM ()
bindAndSetHaskellCode :: BuiltinId -> [Char] -> Term -> TCM ()
bindAndSetHaskellCode BuiltinId
b [Char]
hs Term
t = do
QName
d <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCM (Maybe QName)
getDef Term
t
BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
b Term
t
QName -> [Char] -> TCM ()
addHaskellPragma QName
d [Char]
hs
bindBuiltinBool :: Term -> TCM ()
bindBuiltinBool :: Term -> TCM ()
bindBuiltinBool = BuiltinId -> [Char] -> Term -> TCM ()
bindAndSetHaskellCode BuiltinId
builtinBool [Char]
"= type Bool"
checkBuiltinBool :: TCM ()
checkBuiltinBool :: TCM ()
checkBuiltinBool = do
Maybe Term
true <- forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinTrue
Maybe Term
false <- forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinFalse
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe Term
true forall a. Eq a => a -> a -> Bool
== Maybe Term
false) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError [Char]
"Cannot bind TRUE and FALSE to the same constructor"
bindBuiltinInt :: Term -> TCM ()
bindBuiltinInt :: Term -> TCM ()
bindBuiltinInt = BuiltinId -> [Char] -> Term -> TCM ()
bindAndSetHaskellCode BuiltinId
builtinInteger [Char]
"= type Integer"
bindBuiltinNat :: Term -> TCM ()
bindBuiltinNat :: Term -> TCM ()
bindBuiltinNat Term
t = do
BuiltinId -> Term -> TCM ()
bindBuiltinData BuiltinId
builtinNat Term
t
QName
name <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCM (Maybe QName)
getDef Term
t
QName -> [Char] -> TCM ()
addHaskellPragma QName
name [Char]
"= type Integer"
bindBuiltinData :: BuiltinId -> Term -> TCM ()
bindBuiltinData :: BuiltinId -> Term -> TCM ()
bindBuiltinData BuiltinId
s Term
t = do
BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
s Term
t
QName
name <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCM (Maybe QName)
getDef Term
t
Datatype{ dataCons :: Defn -> [QName]
dataCons = [QName]
cs } <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name
let getArity :: QName -> m Int
getArity QName
c = do
Constructor{ conArity :: Defn -> Int
conArity = Int
a } <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
forall (m :: * -> *) a. Monad m => a -> m a
return Int
a
getBuiltinArity :: BuiltinDescriptor -> TCMT IO Int
getBuiltinArity (BuiltinDataCons TCM Type
t) = Type -> Int
arity forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Type
t
getBuiltinArity BuiltinDescriptor
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
sortByM :: (a -> f b) -> [a] -> f [a]
sortByM a -> f b
f [a]
xs = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [a] -> [b] -> [(a, b)]
zip [a]
xs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> f b
f [a]
xs
[QName]
cs <- forall {f :: * -> *} {b} {a}.
(Ord b, Monad f) =>
(a -> f b) -> [a] -> f [a]
sortByM forall {m :: * -> *}. HasConstInfo m => QName -> m Int
getArity [QName]
cs
let bcis :: [BuiltinInfo]
bcis = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ do
BuiltinData TCM Type
_ [BuiltinId]
bcs <- BuiltinInfo -> BuiltinDescriptor
builtinDesc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> Maybe BuiltinInfo
findBuiltinInfo BuiltinId
s
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM BuiltinId -> Maybe BuiltinInfo
findBuiltinInfo [BuiltinId]
bcs
[BuiltinInfo]
bcis <- forall {f :: * -> *} {b} {a}.
(Ord b, Monad f) =>
(a -> f b) -> [a] -> f [a]
sortByM (BuiltinDescriptor -> TCMT IO Int
getBuiltinArity forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinInfo -> BuiltinDescriptor
builtinDesc) [BuiltinInfo]
bcis
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Int
length [QName]
cs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [BuiltinInfo]
bcis) forall a. HasCallStack => a
__IMPOSSIBLE__
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (\ QName
c BuiltinInfo
bci -> BuiltinInfo -> Expr -> TCM ()
bindBuiltinInfo BuiltinInfo
bci (AmbiguousQName -> Expr
A.Con forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous forall a b. (a -> b) -> a -> b
$ forall a. SetRange a => Range -> a -> a
setRange (forall a. HasRange a => a -> Range
getRange QName
name) QName
c)) [QName]
cs [BuiltinInfo]
bcis
bindBuiltinUnit :: Term -> TCM ()
bindBuiltinUnit :: Term -> TCM ()
bindBuiltinUnit Term
t = do
QName
unit <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCM (Maybe QName)
getDef Term
t
Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
unit
case Defn
def of
Record { recFields :: Defn -> [Dom QName]
recFields = [], recConHead :: Defn -> ConHead
recConHead = ConHead
con } -> do
BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
builtinUnit Term
t
BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
builtinUnitUnit (ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem [])
Defn
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError [Char]
"Builtin UNIT must be a singleton record type"
bindBuiltinSigma :: Term -> TCM ()
bindBuiltinSigma :: Term -> TCM ()
bindBuiltinSigma Term
t = do
QName
sigma <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCM (Maybe QName)
getDef Term
t
Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
sigma
case Defn
def of
Record { recFields :: Defn -> [Dom QName]
recFields = [Dom QName
fst,Dom QName
snd], recConHead :: Defn -> ConHead
recConHead = ConHead
con } -> do
BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
builtinSigma Term
t
Defn
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError [Char]
"Builtin SIGMA must be a record type with two fields"
bindBuiltinEquality :: ResolvedName -> TCM ()
bindBuiltinEquality :: ResolvedName -> TCM ()
bindBuiltinEquality ResolvedName
x = do
(Term
v, Type
_t) <- Expr -> TCM (Term, Type)
inferExpr (forall a. NameToExpr a => a -> Expr
A.nameToExpr ResolvedName
x)
(QName
eq, Definition
def) <- BuiltinId -> Int -> Term -> TCM (QName, Definition)
inductiveCheck BuiltinId
builtinEquality Int
1 Term
v
TelV Tele (Dom Type)
eqTel Type
eqCore <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
let no :: TCMT IO a
no = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError [Char]
"The type of BUILTIN EQUALITY must be a polymorphic relation"
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Maybe a -> Bool
isJust forall a b. (a -> b) -> a -> b
$ Term -> Maybe Sort
isSort forall a b. (a -> b) -> a -> b
$ forall t a. Type'' t a -> a
unEl Type
eqCore) forall a. HasCallStack => a
__IMPOSSIBLE__
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Sized a => a -> Peano
natSize Tele (Dom Type)
eqTel forall a. Ord a => a -> a -> Bool
>= Peano
3) forall {a}. TCMT IO a
no
let (Dom ([Char], Type)
a, Dom ([Char], Type)
b) = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Maybe (a, a)
last2 forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
eqTel
[Term
a,Term
b] <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall t a. Type'' t a -> a
unEl forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) [Dom ([Char], Type)
a,Dom ([Char], Type)
b]
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. DeBruijn a => a -> Maybe Int
deBruijnView Term
a forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Int
0) forall {a}. TCMT IO a
no
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. DeBruijn a => a -> Maybe Int
deBruijnView Term
b forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Int
1) forall {a}. TCMT IO a
no
case Definition -> Defn
theDef Definition
def of
Datatype { dataCons :: Defn -> [QName]
dataCons = [QName
c] } -> do
BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
builtinEquality Term
v
Definition
cdef <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
TelV Tele (Dom Type)
conTel Type
conCore <- forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
cdef
[Term]
ts <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall t a. Type'' t a -> a
unEl forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop (Defn -> Int
conPars forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
cdef) forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
conTel
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
ts forall a. Ord a => a -> a -> Bool
<= Int
1) forall {a}. TCMT IO a
wrongRefl
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((forall a. a -> Maybe a
Just Int
0 forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. DeBruijn a => a -> Maybe Int
deBruijnView) [Term]
ts) forall {a}. TCMT IO a
wrongRefl
case forall t a. Type'' t a -> a
unEl Type
conCore of
Def QName
_ Elims
es -> do
let vs :: [Term]
vs = forall a b. (a -> b) -> [a] -> [b]
map forall e. Arg e -> e
unArg forall a b. (a -> b) -> a -> b
$ 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
(Term
a,Term
b) <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Maybe (a, a)
last2 [Term]
vs
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. DeBruijn a => a -> Maybe Int
deBruijnView Term
a forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Int
0) forall {a}. TCMT IO a
wrongRefl
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. DeBruijn a => a -> Maybe Int
deBruijnView Term
b forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Int
0) forall {a}. TCMT IO a
wrongRefl
BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
builtinRefl (ConHead -> ConInfo -> Elims -> Term
Con (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
c forall p. DataOrRecord' p
IsData Induction
Inductive []) ConInfo
ConOSystem [])
Term
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
Defn
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError [Char]
"Builtin EQUALITY must be a data type with a single constructor"
where
wrongRefl :: TCMT IO a
wrongRefl = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError [Char]
"Wrong type of constructor of BUILTIN EQUALITY"
bindBuiltinInfo :: BuiltinInfo -> A.Expr -> TCM ()
bindBuiltinInfo :: BuiltinInfo -> Expr -> TCM ()
bindBuiltinInfo (BuiltinInfo BuiltinId
s BuiltinDescriptor
d) Expr
e = do
case BuiltinDescriptor
d of
BuiltinData TCM Type
t [BuiltinId]
cs -> do
Term
v <- Expr -> Type -> TCMT IO Term
checkExpr Expr
e forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM Type
t
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinUnit) forall a b. (a -> b) -> a -> b
$ do
forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ BuiltinId -> Int -> Term -> TCM (QName, Definition)
inductiveCheck BuiltinId
s (forall (t :: * -> *) a. Foldable t => t a -> Int
length [BuiltinId]
cs) Term
v
if | BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinEquality -> forall a. HasCallStack => a
__IMPOSSIBLE__
| BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinBool -> Term -> TCM ()
bindBuiltinBool Term
v
| BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinNat -> Term -> TCM ()
bindBuiltinNat Term
v
| BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinInteger -> Term -> TCM ()
bindBuiltinInt Term
v
| BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinUnit -> Term -> TCM ()
bindBuiltinUnit Term
v
| BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinSigma -> Term -> TCM ()
bindBuiltinSigma Term
v
| BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinList -> BuiltinId -> Term -> TCM ()
bindBuiltinData BuiltinId
s Term
v
| BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinMaybe -> BuiltinId -> Term -> TCM ()
bindBuiltinData BuiltinId
s Term
v
| Bool
otherwise -> BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
s Term
v
BuiltinDataCons TCM Type
t -> do
let name :: Term -> Term
name (Lam ArgInfo
h Abs Term
b) = Term -> Term
name (forall a. Subst a => Abs a -> a
absBody Abs Term
b)
name (Con ConHead
c ConInfo
ci Elims
_) = ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci []
name Term
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
Term
v0 <- Expr -> Type -> TCMT IO Term
checkExpr Expr
e forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM Type
t
case Expr
e of
A.Con{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
Expr
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ BuiltinId -> Expr -> TypeError
BuiltinMustBeConstructor BuiltinId
s Expr
e
let v :: Term
v@(Con ConHead
h ConInfo
_ []) = Term -> Term
name Term
v0
BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
s Term
v
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
s forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BuiltinId
builtinFalse, BuiltinId
builtinTrue]) TCM ()
checkBuiltinBool
BuiltinPrim PrimitiveId
pfname Term -> TCM ()
axioms -> do
case Expr
e of
A.Def QName
qx -> do
PrimImpl Type
t PrimFun
pf <- PrimitiveId -> TCM PrimitiveImpl
lookupPrimitiveFunction PrimitiveId
pfname
Term
v <- Expr -> Type -> TCMT IO Term
checkExpr Expr
e Type
t
Term -> TCM ()
axioms Term
v
Definition
info <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qx
let cls :: [Clause]
cls = Definition -> [Clause]
defClauses Definition
info
a :: IsAbstract
a = Definition -> IsAbstract
defAbstract Definition
info
o :: IsOpaque
o = Definition -> IsOpaque
defOpaque Definition
info
mcc :: Maybe CompiledClauses
mcc = Definition -> Maybe CompiledClauses
defCompiled Definition
info
inv :: FunctionInverse
inv = Definition -> FunctionInverse
defInverse Definition
info
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (PrimFun -> [Occurrence]
primFunArgOccurrences PrimFun
pf forall a. Eq a => a -> a -> Bool
== []) forall a. HasCallStack => a
__IMPOSSIBLE__
PrimitiveId -> PrimFun -> TCM ()
bindPrimitive PrimitiveId
pfname forall a b. (a -> b) -> a -> b
$ PrimFun
pf { primFunName :: QName
primFunName = QName
qx }
QName -> Definition -> TCM ()
addConstant QName
qx forall a b. (a -> b) -> a -> b
$ Definition
info { theDef :: Defn
theDef = Primitive { primAbstr :: IsAbstract
primAbstr = IsAbstract
a
, primName :: PrimitiveId
primName = PrimitiveId
pfname
, primClauses :: [Clause]
primClauses = [Clause]
cls
, primInv :: FunctionInverse
primInv = FunctionInverse
inv
, primCompiled :: Maybe CompiledClauses
primCompiled = Maybe CompiledClauses
mcc
, primOpaque :: IsOpaque
primOpaque = IsOpaque
o
} }
BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
s Term
v
Expr
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ [Char]
"Builtin " forall a. [a] -> [a] -> [a]
++ forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
s forall a. [a] -> [a] -> [a]
++ [Char]
" must be bound to a function"
BuiltinSort{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
BuiltinPostulate Relevance
rel TCM Type
t -> do
Type
t' <- TCM Type
t
Term
v <- forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext Relevance
rel forall a b. (a -> b) -> a -> b
$ Expr -> Type -> TCMT IO Term
checkExpr Expr
e Type
t'
let err :: TCM ()
err = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
[Char]
"The argument to BUILTIN " forall a. [a] -> [a] -> [a]
++ forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
s forall a. [a] -> [a] -> [a]
++ [Char]
" must be a postulated name"
case Expr
e of
A.Def QName
q -> do
Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
case Definition -> Defn
theDef Definition
def of
Axiom {} -> do
BuiltinId -> QName -> Type -> TCM ()
builtinSizeHook BuiltinId
s QName
q Type
t'
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinLevel) forall a b. (a -> b) -> a -> b
$ QName -> TCM ()
setConstTranspAxiom QName
q forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QName -> [Char] -> TCM ()
addHaskellPragma QName
q [Char]
"= type ()"
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinChar) forall a b. (a -> b) -> a -> b
$ QName -> TCM ()
setConstTranspAxiom QName
q forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QName -> [Char] -> TCM ()
addHaskellPragma QName
q [Char]
"= type Char"
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinString) forall a b. (a -> b) -> a -> b
$ QName -> TCM ()
setConstTranspAxiom QName
q forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QName -> [Char] -> TCM ()
addHaskellPragma QName
q [Char]
"= type Data.Text.Text"
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinFloat) forall a b. (a -> b) -> a -> b
$ QName -> TCM ()
setConstTranspAxiom QName
q forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QName -> [Char] -> TCM ()
addHaskellPragma QName
q [Char]
"= type Double"
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinWord64) forall a b. (a -> b) -> a -> b
$ QName -> TCM ()
setConstTranspAxiom QName
q forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QName -> [Char] -> TCM ()
addHaskellPragma QName
q [Char]
"= type MAlonzo.RTE.Word64"
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinPathP) forall a b. (a -> b) -> a -> b
$ QName -> TCM ()
builtinPathPHook QName
q
BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
s Term
v
Defn
_ -> TCM ()
err
Expr
_ -> TCM ()
err
BuiltinUnknown Maybe (TCM Type)
mt Term -> Type -> TCM ()
f -> do
(Term
v, Type
t) <- forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (TCM Type)
mt (Expr -> TCM (Term, Type)
inferExpr Expr
e) forall a b. (a -> b) -> a -> b
$ \ TCM Type
tcmt -> do
Type
t <- TCM Type
tcmt
(,Type
t) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Type -> TCMT IO Term
checkExpr Expr
e Type
t
Term -> Type -> TCM ()
f Term
v Type
t
if | BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinRewrite -> forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (forall (m :: * -> *). MonadReduce m => Term -> MaybeT m QName
getQNameFromTerm Term
v) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Maybe QName
Nothing -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError [Char]
"Invalid rewrite relation"
Just QName
q -> QName -> TCM ()
bindBuiltinRewriteRelation QName
q
| Bool
otherwise -> BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
s Term
v
setConstTranspAxiom :: QName -> TCM ()
setConstTranspAxiom :: QName -> TCM ()
setConstTranspAxiom QName
q =
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Defn
constTranspAxiom)
builtinPathPHook :: QName -> TCM ()
builtinPathPHook :: QName -> TCM ()
builtinPathPHook QName
q =
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q
forall a b. (a -> b) -> a -> b
$ ([Polarity] -> [Polarity]) -> Definition -> Definition
updateDefPolarity forall a. a -> a
id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Occurrence] -> [Occurrence]) -> Definition -> Definition
updateDefArgOccurrences (forall a b. a -> b -> a
const [Occurrence
Unused,Occurrence
StrictPos,Occurrence
Mixed,Occurrence
Mixed])
builtinIdHook :: QName -> TCM ()
builtinIdHook :: QName -> TCM ()
builtinIdHook QName
q = do
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q
forall a b. (a -> b) -> a -> b
$ ([Polarity] -> [Polarity]) -> Definition -> Definition
updateDefPolarity forall a. a -> a
id
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Occurrence] -> [Occurrence]) -> Definition -> Definition
updateDefArgOccurrences (forall a b. a -> b -> a
const [Occurrence
Unused,Occurrence
StrictPos,Occurrence
Mixed,Occurrence
Mixed])
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef (\ def :: Defn
def@Datatype{} -> Defn
def { dataPars :: Int
dataPars = Int
3, dataIxs :: Int
dataIxs = Int
1})
builtinReflIdHook :: QName -> TCM ()
builtinReflIdHook :: QName -> TCM ()
builtinReflIdHook QName
q = do
forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q
forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef (\ def :: Defn
def@Constructor{} -> Defn
def { conPars :: Int
conPars = Int
3, conArity :: Int
conArity = Int
0})
bindBuiltin :: BuiltinId -> ResolvedName -> TCM ()
bindBuiltin :: BuiltinId -> ResolvedName -> TCM ()
bindBuiltin BuiltinId
b ResolvedName
x = do
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM ((Int
0 forall a. Eq a => a -> a -> Bool
==) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize) forall a b. (a -> b) -> a -> b
$ do
let
failure :: forall m a. MonadTCError m => m a
failure :: forall (m :: * -> *) a. MonadTCError m => m a
failure = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ BuiltinId -> TypeError
BuiltinInParameterisedModule BuiltinId
b
NonEmpty AbstractName
xs <- case ResolvedName
x of
VarName{} -> forall (m :: * -> *) a. MonadTCError m => m a
failure
DefinedName Access
_ AbstractName
x Suffix
NoSuffix -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AbstractName
x forall a. a -> [a] -> NonEmpty a
:| []
DefinedName Access
_ AbstractName
x Suffix{} -> forall (m :: * -> *) a. MonadTCError m => m a
failure
FieldName NonEmpty AbstractName
xs -> forall (m :: * -> *) a. Monad m => a -> m a
return NonEmpty AbstractName
xs
ConstructorName Set Induction
_ NonEmpty AbstractName
xs -> forall (m :: * -> *) a. Monad m => a -> m a
return NonEmpty AbstractName
xs
PatternSynResName NonEmpty AbstractName
xs -> forall (m :: * -> *) a. MonadTCError m => m a
failure
ResolvedName
UnknownName -> forall (m :: * -> *) a. MonadTCError m => m a
failure
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, Monad m) =>
f a -> (a -> m Bool) -> m Bool
allM NonEmpty AbstractName
xs forall a b. (a -> b) -> a -> b
$ forall a. Null a => a -> Bool
null forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Tele (Dom Type))
lookupSection forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> ModuleName
qnameModule forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName) forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a. MonadTCError m => m a
failure
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ do
if | BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinRefl -> forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall a b. (a -> b) -> a -> b
$ BuiltinId -> BuiltinId -> Warning
OldBuiltin BuiltinId
b BuiltinId
builtinEquality
| BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinZero -> forall {m :: * -> *}.
MonadWarning m =>
BuiltinId -> BuiltinId -> m ()
now BuiltinId
builtinNat BuiltinId
b
| BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinSuc -> forall {m :: * -> *}.
MonadWarning m =>
BuiltinId -> BuiltinId -> m ()
now BuiltinId
builtinNat BuiltinId
b
| BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinNil -> forall {m :: * -> *}.
MonadWarning m =>
BuiltinId -> BuiltinId -> m ()
now BuiltinId
builtinList BuiltinId
b
| BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinCons -> forall {m :: * -> *}.
MonadWarning m =>
BuiltinId -> BuiltinId -> m ()
now BuiltinId
builtinList BuiltinId
b
| BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinInf -> ResolvedName -> TCM ()
bindBuiltinInf ResolvedName
x
| BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinSharp -> ResolvedName -> TCM ()
bindBuiltinSharp ResolvedName
x
| BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinFlat -> ResolvedName -> TCM ()
bindBuiltinFlat ResolvedName
x
| BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinEquality -> ResolvedName -> TCM ()
bindBuiltinEquality ResolvedName
x
| Just BuiltinInfo
i <- BuiltinId -> Maybe BuiltinInfo
findBuiltinInfo BuiltinId
b -> BuiltinInfo -> Expr -> TCM ()
bindBuiltinInfo BuiltinInfo
i (forall a. NameToExpr a => a -> Expr
A.nameToExpr ResolvedName
x)
| Bool
otherwise -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
NoSuchBuiltinName (forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
b)
where
now :: BuiltinId -> BuiltinId -> m ()
now BuiltinId
new BuiltinId
b = forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall a b. (a -> b) -> a -> b
$ BuiltinId -> BuiltinId -> Warning
OldBuiltin BuiltinId
b BuiltinId
new
isUntypedBuiltin :: BuiltinId -> Bool
isUntypedBuiltin :: BuiltinId -> Bool
isUntypedBuiltin = forall a. Ord a => [a] -> a -> Bool
hasElem [ BuiltinId
builtinFromNat, BuiltinId
builtinFromNeg, BuiltinId
builtinFromString ]
bindUntypedBuiltin :: BuiltinId -> ResolvedName -> TCM ()
bindUntypedBuiltin :: BuiltinId -> ResolvedName -> TCM ()
bindUntypedBuiltin BuiltinId
b = \case
DefinedName Access
_ AbstractName
x Suffix
NoSuffix -> AbstractName -> TCM ()
bind AbstractName
x
DefinedName Access
_ AbstractName
x Suffix{} -> TCM ()
wrong
FieldName (AbstractName
x :| []) -> AbstractName -> TCM ()
bind AbstractName
x
FieldName (AbstractName
x :| [AbstractName]
_) -> forall {m :: * -> *} {a} {b}.
(MonadError TCErr m, PrettyTCM a, MonadFresh NameId m,
MonadInteractionPoints m, MonadStConcreteNames m, PureTCM m,
IsString (m Doc), Null (m Doc), Semigroup (m Doc)) =>
a -> m b
amb AbstractName
x
VarName Name
_x BindingSource
_bnd -> TCM ()
wrong
ResolvedName
UnknownName -> TCM ()
wrong
ConstructorName Set Induction
_ NonEmpty AbstractName
xs -> NonEmpty AbstractName -> TCM ()
err NonEmpty AbstractName
xs
PatternSynResName NonEmpty AbstractName
xs -> NonEmpty AbstractName -> TCM ()
err NonEmpty AbstractName
xs
where
bind :: AbstractName -> TCM ()
bind AbstractName
x = BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
b (QName -> Elims -> Term
Def (AbstractName -> QName
anameName AbstractName
x) [])
wrong :: TCM ()
wrong = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError forall a b. (a -> b) -> a -> b
$ [Char]
"The argument to BUILTIN " forall a. [a] -> [a] -> [a]
++ forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
b forall a. [a] -> [a] -> [a]
++ [Char]
" must be a defined name"
amb :: a -> m b
amb a
x = 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]
"Name " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
" is ambiguous"
err :: NonEmpty AbstractName -> TCM ()
err (AbstractName
x :| [AbstractName]
xs1)
| forall a. Null a => a -> Bool
null [AbstractName]
xs1 = TCM ()
wrong
| Bool
otherwise = forall {m :: * -> *} {a} {b}.
(MonadError TCErr m, PrettyTCM a, MonadFresh NameId m,
MonadInteractionPoints m, MonadStConcreteNames m, PureTCM m,
IsString (m Doc), Null (m Doc), Semigroup (m Doc)) =>
a -> m b
amb AbstractName
x
bindBuiltinNoDef :: BuiltinId -> A.QName -> TCM ()
bindBuiltinNoDef :: BuiltinId -> QName -> TCM ()
bindBuiltinNoDef BuiltinId
b QName
q = forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
b forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BuiltinId]
sizeBuiltins) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM forall (m :: * -> *). HasOptions m => m Bool
sizedTypesOption forall a b. (a -> b) -> a -> b
$
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError forall a b. (a -> b) -> a -> b
$ [Char]
"Cannot declare size BUILTIN " forall a. [a] -> [a] -> [a]
++ forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
b forall a. [a] -> [a] -> [a]
++ [Char]
" with option --no-sized-types"
case BuiltinInfo -> BuiltinDescriptor
builtinDesc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> Maybe BuiltinInfo
findBuiltinInfo BuiltinId
b of
Just (BuiltinPostulate Relevance
rel TCM Type
mt) -> do
Type
t <- TCM Type
mt
FunctionData
fun <- forall (m :: * -> *). HasOptions m => m FunctionData
emptyFunctionData
QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
q (forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
rel ArgInfo
defaultArgInfo) QName
q Type
t (FunctionData -> Defn
def FunctionData
fun)
BuiltinId -> QName -> Type -> TCM ()
builtinSizeHook BuiltinId
b QName
q Type
t
BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
b forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
q []
where
def :: FunctionData -> Defn
def FunctionData
fun
| BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinSizeUniv = FunctionData -> Defn
FunctionDefn forall a b. (a -> b) -> a -> b
$ FunctionData
fun
{ _funClauses :: [Clause]
_funClauses = [ (forall a. Null a => a
empty :: Clause) { clauseBody :: Maybe Term
clauseBody = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Sort -> Term
Sort Sort
sSizeUniv } ]
, _funCompiled :: Maybe CompiledClauses
_funCompiled = forall a. a -> Maybe a
Just (forall a. [Arg [Char]] -> a -> CompiledClauses' a
CC.Done [] forall a b. (a -> b) -> a -> b
$ Sort -> Term
Sort Sort
sSizeUniv)
, _funMutual :: Maybe [QName]
_funMutual = forall a. a -> Maybe a
Just []
, _funTerminates :: Maybe Bool
_funTerminates = forall a. a -> Maybe a
Just Bool
True
}
| Bool
otherwise = Defn
defaultAxiom
Just (BuiltinPrim PrimitiveId
name Term -> TCM ()
axioms) -> do
PrimImpl Type
t PrimFun
pf <- PrimitiveId -> TCM PrimitiveImpl
lookupPrimitiveFunction PrimitiveId
name
PrimitiveId -> PrimFun -> TCM ()
bindPrimitive PrimitiveId
name forall a b. (a -> b) -> a -> b
$ PrimFun
pf { primFunName :: QName
primFunName = QName
q }
let v :: Term
v = QName -> Elims -> Term
Def QName
q []
def :: Defn
def = Primitive { primAbstr :: IsAbstract
primAbstr = IsAbstract
ConcreteDef
, primName :: PrimitiveId
primName = PrimitiveId
name
, primClauses :: [Clause]
primClauses = []
, primInv :: FunctionInverse
primInv = forall c. FunctionInverse' c
NotInjective
, primCompiled :: Maybe CompiledClauses
primCompiled = forall a. a -> Maybe a
Just (forall a. [Arg [Char]] -> a -> CompiledClauses' a
CC.Done [] forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
q [])
, primOpaque :: IsOpaque
primOpaque = IsOpaque
TransparentDef
}
Language
lang <- forall (m :: * -> *). HasOptions m => m Language
getLanguage
QName -> Definition -> TCM ()
addConstant QName
q forall a b. (a -> b) -> a -> b
$
(ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn ArgInfo
defaultArgInfo QName
q Type
t Language
lang Defn
def)
{ defArgOccurrences :: [Occurrence]
defArgOccurrences = PrimFun -> [Occurrence]
primFunArgOccurrences PrimFun
pf }
Term -> TCM ()
axioms Term
v
BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
b Term
v
Just (BuiltinDataCons TCM Type
mt) -> do
Type
t <- TCM Type
mt
QName
d <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! Term -> QName
getPrimName forall a b. (a -> b) -> a -> b
$ forall t a. Type'' t a -> a
unEl Type
t
Bool
erasure <- PragmaOptions -> Bool
optErasure forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
let
ch :: ConHead
ch = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
q forall p. DataOrRecord' p
IsData Induction
Inductive []
def :: Defn
def = Constructor
{ conPars :: Int
conPars = Int
0
, conArity :: Int
conArity = Int
0
, conSrcCon :: ConHead
conSrcCon = ConHead
ch
, conData :: QName
conData = QName
d
, conAbstr :: IsAbstract
conAbstr = IsAbstract
ConcreteDef
, conComp :: CompKit
conComp = CompKit
emptyCompKit
, conProj :: Maybe [QName]
conProj = forall a. Maybe a
Nothing
, conForced :: [IsForced]
conForced = []
, conErased :: Maybe [Bool]
conErased = forall a. Maybe a
Nothing
, conErasure :: Bool
conErasure = Bool
erasure
, conInline :: Bool
conInline = Bool
False
}
QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
q ArgInfo
defaultArgInfo QName
q Type
t Defn
def
QName -> [QName] -> TCM ()
addDataCons QName
d [QName
q]
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinReflId) forall a b. (a -> b) -> a -> b
$ QName -> TCM ()
builtinReflIdHook QName
q
BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
b forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
ch ConInfo
ConOSystem []
Just (BuiltinData TCM Type
mt [BuiltinId]
cs) -> do
Type
t <- TCM Type
mt
QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
q ArgInfo
defaultArgInfo QName
q Type
t (forall {a}. LensSort a => a -> Defn
def Type
t)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinId) forall a b. (a -> b) -> a -> b
$ QName -> TCM ()
builtinIdHook QName
q
BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
b forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
q []
where
def :: a -> Defn
def a
t = Datatype
{ dataPars :: Int
dataPars = Int
0
, dataIxs :: Int
dataIxs = Int
0
, dataClause :: Maybe Clause
dataClause = forall a. Maybe a
Nothing
, dataCons :: [QName]
dataCons = []
, dataSort :: Sort
dataSort = forall a. LensSort a => a -> Sort
getSort a
t
, dataAbstr :: IsAbstract
dataAbstr = IsAbstract
ConcreteDef
, dataMutual :: Maybe [QName]
dataMutual = forall a. Maybe a
Nothing
, dataPathCons :: [QName]
dataPathCons = []
, dataTranspIx :: Maybe QName
dataTranspIx = forall a. Maybe a
Nothing
, dataTransp :: Maybe QName
dataTransp = forall a. Maybe a
Nothing
}
Just (BuiltinSort BuiltinSort
builtinSort) -> do
let s :: Sort
s = case BuiltinSort
builtinSort of
SortUniv Univ
u -> forall t. Univ -> Level' t -> Sort' t
Univ Univ
u forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
0
SortOmega Univ
u -> forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
0
BuiltinSort
SortIntervalUniv -> forall t. Sort' t
IntervalUniv
BuiltinSort
SortLevelUniv -> forall t. Sort' t
LevelUniv
def :: Defn
def = BuiltinSort -> Sort -> Defn
PrimitiveSort BuiltinSort
builtinSort Sort
s
case BuiltinSort
builtinSort of
BuiltinSort
SortIntervalUniv -> Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
""
BuiltinSort
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
q ArgInfo
defaultArgInfo QName
q (Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ Sort -> Sort
univSort Sort
s) Defn
def
BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
b forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
q []
Just{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
Maybe BuiltinDescriptor
Nothing -> forall a. HasCallStack => a
__IMPOSSIBLE__
builtinKindOfName :: BuiltinId -> Maybe KindOfName
builtinKindOfName :: BuiltinId -> Maybe KindOfName
builtinKindOfName = BuiltinInfo -> KindOfName
distinguish forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> BuiltinId -> Maybe BuiltinInfo
findBuiltinInfo
where
distinguish :: BuiltinInfo -> KindOfName
distinguish BuiltinInfo
d = case BuiltinInfo -> BuiltinDescriptor
builtinDesc BuiltinInfo
d of
BuiltinDataCons{} -> KindOfName
ConName
BuiltinData{} -> KindOfName
DataName
BuiltinPrim{} -> KindOfName
PrimName
BuiltinPostulate{} -> KindOfName
AxiomName
BuiltinSort{} -> KindOfName
PrimName
BuiltinUnknown{} -> KindOfName
OtherDefName