{-# 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 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
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Functions
import Agda.TypeChecking.Irrelevance
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

---------------------------------------------------------------------------
-- * Checking builtin pragmas
---------------------------------------------------------------------------

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 :: String -> Maybe BuiltinInfo
findBuiltinInfo :: [Char] -> Maybe BuiltinInfo
findBuiltinInfo [Char]
b = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (([Char]
b forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinInfo -> [Char]
builtinName) [BuiltinInfo]
coreBuiltins

coreBuiltins :: [BuiltinInfo]
coreBuiltins :: [BuiltinInfo]
coreBuiltins =
  [ ([Char]
builtinList                             [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> 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) [[Char]
builtinNil, [Char]
builtinCons])
  , ([Char]
builtinArg                              [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> 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) [[Char]
builtinArgArg])
  , ([Char]
builtinAbs                              [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> 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) [[Char]
builtinAbsAbs])
  , ([Char]
builtinArgInfo                          [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [[Char]
builtinArgArgInfo])
  , ([Char]
builtinBool                             [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [[Char]
builtinTrue, [Char]
builtinFalse])
  , ([Char]
builtinNat                              [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [[Char]
builtinZero, [Char]
builtinSuc])
  , ([Char]
builtinMaybe                            [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> 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) [[Char]
builtinNothing, [Char]
builtinJust])
  , ([Char]
builtinSigma                            [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> BuiltinDescriptor
BuiltinData (forall (m :: * -> *) a. [[Char]] -> 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))
                                                              )
                                                             [[Char]
"SIGMACON"])
  , ([Char]
builtinUnit                             [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [[Char]
builtinUnitUnit])  -- actually record, but they are treated the same
  , ([Char]
builtinAgdaLiteral                      [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [[Char]
builtinAgdaLitNat, [Char]
builtinAgdaLitWord64, [Char]
builtinAgdaLitFloat,
                                                                   [Char]
builtinAgdaLitChar, [Char]
builtinAgdaLitString,
                                                                   [Char]
builtinAgdaLitQName, [Char]
builtinAgdaLitMeta])
  , ([Char]
builtinAgdaPattern                      [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [[Char]
builtinAgdaPatVar, [Char]
builtinAgdaPatCon, [Char]
builtinAgdaPatDot,
                                                                   [Char]
builtinAgdaPatLit, [Char]
builtinAgdaPatProj, [Char]
builtinAgdaPatAbsurd])
  , ([Char]
builtinAgdaPatVar                       [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tpat))
  , ([Char]
builtinAgdaPatCon                       [Char] -> 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))
  , ([Char]
builtinAgdaPatDot                       [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tpat))
  , ([Char]
builtinAgdaPatLit                       [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tliteral forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tpat))
  , ([Char]
builtinAgdaPatProj                      [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tpat))
  , ([Char]
builtinAgdaPatAbsurd                    [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tpat))
  , ([Char]
builtinLevel                            [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tset)
  , ([Char]
builtinWord64                           [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tset)
  , ([Char]
builtinInteger                          [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [[Char]
builtinIntegerPos, [Char]
builtinIntegerNegSuc])
  , ([Char]
builtinIntegerPos                       [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tinteger))
  , ([Char]
builtinIntegerNegSuc                    [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tinteger))
  , ([Char]
builtinFloat                            [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tset)
  , ([Char]
builtinChar                             [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tset)
  , ([Char]
builtinString                           [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tset)
  , ([Char]
builtinQName                            [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tset)
  , ([Char]
builtinAgdaMeta                         [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tset)
  , ([Char]
builtinIO                               [Char] -> 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))
  , ([Char]
builtinPath                             [Char] -> 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)
  , ([Char]
builtinPathP                            [Char] -> 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)))
  , ([Char]
builtinIntervalUniv                     [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> [Char] -> BuiltinDescriptor
BuiltinSort [Char]
"primIntervalUniv")
  , ([Char]
builtinInterval                         [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> 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)) [[Char]
builtinIZero,[Char]
builtinIOne])
  , ([Char]
builtinSub                              [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall (m :: * -> *) a. [[Char]] -> 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)
                                                                  ))
  , ([Char]
builtinSubIn                            [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall (m :: * -> *) a. [[Char]] -> 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)))
  , ([Char]
builtinIZero                            [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons forall {t}. TCMT IO (Type'' t Term)
tinterval)
  , ([Char]
builtinIOne                             [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons forall {t}. TCMT IO (Type'' t Term)
tinterval)
  , ([Char]
builtinPartial                          [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> [Char] -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim [Char]
"primPartial" (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()))
  , ([Char]
builtinPartialP                         [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> [Char] -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim [Char]
"primPartialP" (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()))
  , ([Char]
builtinIsOne                            [Char] -> 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)))
  , ([Char]
builtinItIsOne                          [Char] -> 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))
  , ([Char]
builtinIsOne1                           [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall (m :: * -> *) a. [[Char]] -> 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))))
  , ([Char]
builtinIsOne2                           [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall (m :: * -> *) a. [[Char]] -> 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))))
  , ([Char]
builtinIsOneEmpty                       [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall (m :: * -> *) a. [[Char]] -> 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)))

  , ([Char]
builtinId                               [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> 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)) [[Char]
builtinReflId])
  , ([Char]
builtinReflId                           [Char] -> 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. [[Char]] -> 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)))
  , ([Char]
builtinEquiv                            [Char] -> 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
CFull [Char]
"" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. [[Char]] -> 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 ()))
  , ([Char]
builtinEquivFun                         [Char] -> 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
CFull [Char]
"" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. [[Char]] -> 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 ()))
  , ([Char]
builtinEquivProof                       [Char] -> 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
CFull [Char]
"" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. [[Char]] -> 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 ()))
  , ([Char]
builtinTranspProof                       [Char] -> 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. [[Char]] -> 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 ()))
  , ([Char]
builtinAgdaSort                         [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset
                                                   [ [Char]
builtinAgdaSortSet, [Char]
builtinAgdaSortLit
                                                   , [Char]
builtinAgdaSortProp, [Char]
builtinAgdaSortPropLit
                                                   , [Char]
builtinAgdaSortInf, [Char]
builtinAgdaSortUnsupported])
  , ([Char]
builtinAgdaTerm                         [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset
                                                   [ [Char]
builtinAgdaTermVar, [Char]
builtinAgdaTermLam, [Char]
builtinAgdaTermExtLam
                                                   , [Char]
builtinAgdaTermDef, [Char]
builtinAgdaTermCon
                                                   , [Char]
builtinAgdaTermPi, [Char]
builtinAgdaTermSort
                                                   , [Char]
builtinAgdaTermLit, [Char]
builtinAgdaTermMeta
                                                   , [Char]
builtinAgdaTermUnsupported])
  , [Char]
builtinAgdaErrorPart                     [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [ [Char]
builtinAgdaErrorPartString, [Char]
builtinAgdaErrorPartTerm, [Char]
builtinAgdaErrorPartPatt, [Char]
builtinAgdaErrorPartName ]
  , [Char]
builtinAgdaErrorPartString               [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
terrorpart)
  , [Char]
builtinAgdaErrorPartTerm                 [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
terrorpart)
  , [Char]
builtinAgdaErrorPartPatt                 [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tpat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
terrorpart)
  , [Char]
builtinAgdaErrorPartName                 [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
terrorpart)
  -- Andreas, 2017-01-12, issue #2386: special handling of builtinEquality
  -- , (builtinEquality                         |-> BuiltinData (hPi "a" (el primLevel) $
  --                                                             hPi "A" (return $ sort $ varSort 0) $
  --                                                             (El (varSort 1) <$> varM 0) -->
  --                                                             (El (varSort 1) <$> varM 0) -->
  --                                                             return (sort $ varSort 1))
  --                                                            [builtinRefl])
  , ([Char]
builtinHiding                           [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [[Char]
builtinHidden, [Char]
builtinInstance, [Char]
builtinVisible])
    -- Relevance
  , ([Char]
builtinRelevance                        [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [[Char]
builtinRelevant, [Char]
builtinIrrelevant])
  , ([Char]
builtinRelevant                         [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
trelevance)
  , ([Char]
builtinIrrelevant                       [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
trelevance)
    -- Quantity
  , ([Char]
builtinQuantity                         [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [[Char]
builtinQuantity0, [Char]
builtinQuantityω])
  , ([Char]
builtinQuantity0                        [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tquantity)
  , ([Char]
builtinQuantityω                        [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tquantity)
    -- Modality
  , ([Char]
builtinModality                         [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [[Char]
builtinModalityConstructor])
  , ([Char]
builtinModalityConstructor              [Char] -> 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))
    -- Associativity
  , [Char]
builtinAssoc                             [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [[Char]
builtinAssocLeft, [Char]
builtinAssocRight, [Char]
builtinAssocNon]
  , [Char]
builtinAssocLeft                         [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tassoc
  , [Char]
builtinAssocRight                        [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tassoc
  , [Char]
builtinAssocNon                          [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tassoc
    -- Precedence
  , [Char]
builtinPrecedence                        [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [[Char]
builtinPrecRelated, [Char]
builtinPrecUnrelated]
  , [Char]
builtinPrecRelated                       [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tfloat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tprec)
  , [Char]
builtinPrecUnrelated                     [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tprec
    -- Fixity
  , [Char]
builtinFixity                            [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [[Char]
builtinFixityFixity]
  , [Char]
builtinFixityFixity                      [Char] -> 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)
  -- Andreas, 2017-01-12, issue #2386: special handling of builtinEquality
  -- , (builtinRefl                             |-> BuiltinDataCons (hPi "a" (el primLevel) $
  --                                                                 hPi "A" (return $ sort $ varSort 0) $
  --                                                                 hPi "x" (El (varSort 1) <$> varM 0) $
  --                                                                 El (varSort 2) <$> primEquality <#> varM 2 <#> varM 1 <@> varM 0 <@> varM 0))
  , ([Char]
builtinRewrite                          [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> Maybe (TCM Type) -> (Term -> Type -> TCM ()) -> BuiltinDescriptor
BuiltinUnknown forall a. Maybe a
Nothing Term -> Type -> TCM ()
verifyBuiltinRewrite)
  , ([Char]
builtinNil                              [Char] -> 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))))
  , ([Char]
builtinCons                             [Char] -> 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))))
  , ([Char]
builtinNothing                          [Char] -> 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))))
  , ([Char]
builtinJust                             [Char] -> 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))))
  , ([Char]
builtinZero                             [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tnat)
  , ([Char]
builtinSuc                              [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tnat))
  , ([Char]
builtinTrue                             [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tbool)
  , ([Char]
builtinFalse                            [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tbool)
  , ([Char]
builtinArgArg                           [Char] -> 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)))
  , ([Char]
builtinAbsAbs                           [Char] -> 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)))
  , ([Char]
builtinArgArgInfo                       [Char] -> 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))
  , ([Char]
builtinAgdaTermVar                      [Char] -> 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))
  , ([Char]
builtinAgdaTermLam                      [Char] -> 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))
  , ([Char]
builtinAgdaTermExtLam                   [Char] -> 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))
  , ([Char]
builtinAgdaTermDef                      [Char] -> 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))
  , ([Char]
builtinAgdaTermCon                      [Char] -> 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))
  , ([Char]
builtinAgdaTermPi                       [Char] -> 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))
  , ([Char]
builtinAgdaTermSort                     [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tsort forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm))
  , ([Char]
builtinAgdaTermLit                      [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tliteral forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm))
  , ([Char]
builtinAgdaTermMeta                     [Char] -> 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))
  , ([Char]
builtinAgdaTermUnsupported              [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tterm)
  , ([Char]
builtinAgdaLitNat                       [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
  , ([Char]
builtinAgdaLitWord64                    [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tword64 forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
  , ([Char]
builtinAgdaLitFloat                     [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tfloat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
  , ([Char]
builtinAgdaLitChar                      [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tchar forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
  , ([Char]
builtinAgdaLitString                    [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
  , ([Char]
builtinAgdaLitQName                     [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
  , ([Char]
builtinAgdaLitMeta                      [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tmeta forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
  , ([Char]
builtinHidden                           [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
thiding)
  , ([Char]
builtinInstance                         [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
thiding)
  , ([Char]
builtinVisible                          [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
thiding)
  , ([Char]
builtinSizeUniv                         [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate TCM Type
tsetOmega) -- SizeUniv : Setω
  , ([Char]
builtinSize                             [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tSizeUniv)
  , ([Char]
builtinSizeLt                           [Char] -> 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))
  , ([Char]
builtinSizeSuc                          [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tsize forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsize))
  , ([Char]
builtinSizeInf                          [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate TCM Type
tsize)
  -- postulate max : {i : Size} -> Size< i -> Size< i -> Size< i
  , ([Char]
builtinSizeMax                          [Char] -> 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))
     -- (hPi "i" tsize $ let a = el $ primSizeLt <@> v0 in (a --> a --> a)))
  , ([Char]
builtinAgdaSortSet                      [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsort))
  , ([Char]
builtinAgdaSortLit                      [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsort))
  , ([Char]
builtinAgdaSortProp                     [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsort))
  , ([Char]
builtinAgdaSortPropLit                  [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsort))
  , ([Char]
builtinAgdaSortInf                      [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsort))
  , ([Char]
builtinAgdaSortUnsupported              [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tsort)
  , ([Char]
builtinNatPlus                          [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> [Char] -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim [Char]
"primNatPlus" Term -> TCM ()
verifyPlus)
  , ([Char]
builtinNatMinus                         [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> [Char] -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim [Char]
"primNatMinus" Term -> TCM ()
verifyMinus)
  , ([Char]
builtinNatTimes                         [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> [Char] -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim [Char]
"primNatTimes" Term -> TCM ()
verifyTimes)
  , ([Char]
builtinNatDivSucAux                     [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> [Char] -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim [Char]
"primNatDivSucAux" Term -> TCM ()
verifyDivSucAux)
  , ([Char]
builtinNatModSucAux                     [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> [Char] -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim [Char]
"primNatModSucAux" Term -> TCM ()
verifyModSucAux)
  , ([Char]
builtinNatEquals                        [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> [Char] -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim [Char]
"primNatEquality" Term -> TCM ()
verifyEquals)
  , ([Char]
builtinNatLess                          [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> [Char] -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim [Char]
"primNatLess" Term -> TCM ()
verifyLess)
  , ([Char]
builtinLevelZero                        [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> [Char] -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim [Char]
"primLevelZero" (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()))
  , ([Char]
builtinLevelSuc                         [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> [Char] -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim [Char]
"primLevelSuc" (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()))
  , ([Char]
builtinLevelMax                         [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> [Char] -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim [Char]
"primLevelMax" forall {m :: * -> *} {p}. Monad m => p -> m ()
verifyMax)
  , ([Char]
builtinSet                              [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> [Char] -> BuiltinDescriptor
BuiltinSort [Char]
"primSet")
  , ([Char]
builtinProp                             [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> [Char] -> BuiltinDescriptor
BuiltinSort [Char]
"primProp")
  , ([Char]
builtinSetOmega                         [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> [Char] -> BuiltinDescriptor
BuiltinSort [Char]
"primSetOmega")
  , ([Char]
builtinSSetOmega                        [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> [Char] -> BuiltinDescriptor
BuiltinSort [Char]
"primStrictSetOmega")
  , ([Char]
builtinStrictSet                        [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> [Char] -> BuiltinDescriptor
BuiltinSort [Char]
"primStrictSet")
  , ([Char]
builtinAgdaClause                       [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [[Char]
builtinAgdaClauseClause, [Char]
builtinAgdaClauseAbsurd])
  , ([Char]
builtinAgdaClauseClause                 [Char] -> 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))
  , ([Char]
builtinAgdaClauseAbsurd                 [Char] -> 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))
  , ([Char]
builtinAgdaDefinition                   [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [[Char]] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [[Char]
builtinAgdaDefinitionFunDef
                                                                  ,[Char]
builtinAgdaDefinitionDataDef
                                                                  ,[Char]
builtinAgdaDefinitionDataConstructor
                                                                  ,[Char]
builtinAgdaDefinitionRecordDef
                                                                  ,[Char]
builtinAgdaDefinitionPostulate
                                                                  ,[Char]
builtinAgdaDefinitionPrimitive])
  , ([Char]
builtinAgdaDefinitionFunDef             [Char] -> 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))
  , ([Char]
builtinAgdaDefinitionDataDef            [Char] -> 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))
  , ([Char]
builtinAgdaDefinitionDataConstructor    [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tdefn))
  , ([Char]
builtinAgdaDefinitionRecordDef          [Char] -> 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))
  , ([Char]
builtinAgdaDefinitionPostulate          [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tdefn)
  , ([Char]
builtinAgdaDefinitionPrimitive          [Char] -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tdefn)
  , [Char]
builtinAgdaTCM                           [Char] -> 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)
  , [Char]
builtinAgdaTCMReturn                     [Char] -> 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))
  , [Char]
builtinAgdaTCMBind                       [Char] -> 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))
  , [Char]
builtinAgdaTCMUnify                      [Char] -> 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)
  , [Char]
builtinAgdaTCMTypeError                  [Char] -> 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))
  , [Char]
builtinAgdaTCMInferType                  [Char] -> 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)
  , [Char]
builtinAgdaTCMCheckType                  [Char] -> 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)
  , [Char]
builtinAgdaTCMNormalise                  [Char] -> 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)
  , [Char]
builtinAgdaTCMReduce                     [Char] -> 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)
  , [Char]
builtinAgdaTCMCatchError                 [Char] -> 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))
  , [Char]
builtinAgdaTCMGetContext                 [Char] -> 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))
  , [Char]
builtinAgdaTCMExtendContext              [Char] -> 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))
  , [Char]
builtinAgdaTCMInContext                  [Char] -> 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))
  , [Char]
builtinAgdaTCMFreshName                  [Char] -> 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)
  , [Char]
builtinAgdaTCMDeclareDef                 [Char] -> 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)
  , [Char]
builtinAgdaTCMDeclarePostulate           [Char] -> 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)
  , [Char]
builtinAgdaTCMDeclareData                [Char] -> 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)
  , [Char]
builtinAgdaTCMDefineData                 [Char] -> 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)
  , [Char]
builtinAgdaTCMDefineFun                  [Char] -> 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)
  , [Char]
builtinAgdaTCMGetType                    [Char] -> 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)
  , [Char]
builtinAgdaTCMGetDefinition              [Char] -> 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)
  , [Char]
builtinAgdaTCMQuoteTerm                  [Char] -> 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)
  , [Char]
builtinAgdaTCMUnquoteTerm                [Char] -> 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))
  , [Char]
builtinAgdaTCMQuoteOmegaTerm             [Char] -> 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)
  , [Char]
builtinAgdaTCMBlockOnMeta                [Char] -> 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
tmeta 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))
  , [Char]
builtinAgdaTCMCommit                     [Char] -> 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)
  , [Char]
builtinAgdaTCMIsMacro                    [Char] -> 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)
  , [Char]
builtinAgdaTCMWithNormalisation          [Char] -> 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))
  , [Char]
builtinAgdaTCMWithReconsParams           [Char] -> 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))
  , [Char]
builtinAgdaTCMFormatErrorParts           [Char] -> 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)
  , [Char]
builtinAgdaTCMDebugPrint                 [Char] -> 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)
  , [Char]
builtinAgdaTCMOnlyReduceDefs             [Char] -> 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
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))
  , [Char]
builtinAgdaTCMDontReduceDefs             [Char] -> 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
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))

  , [Char]
builtinAgdaTCMNoConstraints              [Char] -> 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))
  , [Char]
builtinAgdaTCMRunSpeculative             [Char] -> 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))
  , [Char]
builtinAgdaTCMExec                       [Char] -> 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)))))
  , [Char]
builtinAgdaTCMGetInstances               [Char] -> 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))
  ]
  where
        |-> :: [Char] -> BuiltinDescriptor -> BuiltinInfo
(|->) = [Char] -> 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. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
IsFibrant 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
        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
--        tcolors    = el (list primAgdaTerm) -- TODO guilhem
        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}.
[[Char]]
-> ((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

                -- We allow recursion on any argument
                [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}.
[[Char]]
-> ((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

                -- We allow recursion on any argument
                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}.
[[Char]]
-> ((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}.
[[Char]]
-> ((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}.
[[Char]]
-> ((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}.
[[Char]]
-> ((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}.
[[Char]]
-> ((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 ()  -- TODO: make max a postulate

        verify :: [[Char]]
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
verify [[Char]]
xs = forall a.
TCMT IO Term
-> TCMT IO Term
-> TCMT IO Term
-> [[Char]]
-> ((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 [[Char]]
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
-> [[Char]]
-> ((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 [[Char]]
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
                -- Andreas: 2013-10-21 I put primBool here on the inside
                -- since some Nat-builtins do not require Bool-builtins
                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_ [[Char]]
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. [[Char]] -> 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))

-- | Checks that builtin with name @b : String@ of type @t : Term@
--   is a data type or inductive record with @n : Int@ constructors.
--   Returns the name of the data/record type.
inductiveCheck :: String -> Int -> Term -> TCM (QName, Definition)
inductiveCheck :: [Char] -> Int -> Term -> TCM (QName, Definition)
inductiveCheck [Char]
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
$ [[Char]] -> [Char]
unwords
        [ [Char]
"The builtin", [Char]
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
$ [[Char]] -> [Char]
unwords
        [ [Char]
"The builtin", [Char]
b
        , [Char]
"must be a datatype with", forall a. Show a => a -> [Char]
show Int
n
        , [Char]
"constructors"
        ]

-- | @bindPostulatedName builtin q m@ checks that @q@ is a postulated
-- name, and binds the builtin @builtin@ to the term @m q def@,
-- where @def@ is the current 'Definition' of @q@.

bindPostulatedName ::
  String -> ResolvedName -> (QName -> Definition -> TCM Term) -> TCM ()
bindPostulatedName :: [Char]
-> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
bindPostulatedName [Char]
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 {} -> [Char] -> Term -> TCM ()
bindBuiltinName [Char]
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]
++ [Char]
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 :: String -> String -> Term -> TCM ()
bindAndSetHaskellCode :: [Char] -> [Char] -> Term -> TCM ()
bindAndSetHaskellCode [Char]
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
  [Char] -> Term -> TCM ()
bindBuiltinName [Char]
b Term
t
  QName -> [Char] -> TCM ()
addHaskellPragma QName
d [Char]
hs

bindBuiltinBool :: Term -> TCM ()
bindBuiltinBool :: Term -> TCM ()
bindBuiltinBool = [Char] -> [Char] -> Term -> TCM ()
bindAndSetHaskellCode [Char]
builtinBool [Char]
"= type Bool"

-- | Check that we're not trying to bind true and false to the same
-- constructor.
checkBuiltinBool :: TCM ()
checkBuiltinBool :: TCM ()
checkBuiltinBool = do
  Maybe Term
true  <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe Term)
getBuiltin' [Char]
builtinTrue
  Maybe Term
false <- forall (m :: * -> *). HasBuiltins m => [Char] -> m (Maybe Term)
getBuiltin' [Char]
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 = [Char] -> [Char] -> Term -> TCM ()
bindAndSetHaskellCode [Char]
builtinInteger [Char]
"= type Integer"

bindBuiltinNat :: Term -> TCM ()
bindBuiltinNat :: Term -> TCM ()
bindBuiltinNat Term
t = do
  [Char] -> Term -> TCM ()
bindBuiltinData [Char]
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"

-- | Only use for datatypes with distinct arities of constructors.
--   Binds the constructors together with the datatype.
bindBuiltinData :: String -> Term -> TCM ()
bindBuiltinData :: [Char] -> Term -> TCM ()
bindBuiltinData [Char]
s Term
t = do
  [Char] -> Term -> TCM ()
bindBuiltinName [Char]
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
  -- Order constructurs by arity
  [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
  -- Do the same for the builtins
  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
_ [[Char]]
bcs <- BuiltinInfo -> BuiltinDescriptor
builtinDesc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Char] -> Maybe BuiltinInfo
findBuiltinInfo [Char]
s
        forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM [Char] -> Maybe BuiltinInfo
findBuiltinInfo [[Char]]
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__  -- we already checked this
  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
      [Char] -> Term -> TCM ()
bindBuiltinName [Char]
builtinUnit Term
t
      [Char] -> Term -> TCM ()
bindBuiltinName [Char]
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
      [Char] -> Term -> TCM ()
bindBuiltinName [Char]
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"

-- | Bind BUILTIN EQUALITY and BUILTIN REFL.
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)

  -- Equality needs to be a data type with 1 constructor
  (QName
eq, Definition
def) <- [Char] -> Int -> Term -> TCM (QName, Definition)
inductiveCheck [Char]
builtinEquality Int
1 Term
v

  -- Check that the type is the type of a polymorphic relation, i.e.,
  -- Γ → (A : Set _) → A → A → Set _
  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"

  -- The target is a sort since eq is a data type.
  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__

  -- The types of the last two arguments must be the third-last argument
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Sized a => a -> Int
size Tele (Dom Type)
eqTel forall a. Ord a => a -> a -> Bool
>= Int
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

  -- Get the single constructor.
  case Definition -> Defn
theDef Definition
def of
    Datatype { dataCons :: Defn -> [QName]
dataCons = [QName
c] } -> do
      [Char] -> Term -> TCM ()
bindBuiltinName [Char]
builtinEquality Term
v

      -- Check type of REFL.  It has to be of the form
      -- pars → (x : A) → Eq ... x x

      -- Check the arguments
      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
      -- After dropping the parameters, there should be maximally one argument.
      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

      -- Check the target
      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
          [Char] -> Term -> TCM ()
bindBuiltinName [Char]
builtinRefl (ConHead -> ConInfo -> Elims -> Term
Con (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
c DataOrRecord
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 [Char]
s BuiltinDescriptor
d) Expr
e = do
    case BuiltinDescriptor
d of
      BuiltinData TCM Type
t [[Char]]
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 ([Char]
s forall a. Eq a => a -> a -> Bool
== [Char]
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
$ [Char] -> Int -> Term -> TCM (QName, Definition)
inductiveCheck [Char]
s (forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Char]]
cs) Term
v
        if | [Char]
s forall a. Eq a => a -> a -> Bool
== [Char]
builtinEquality -> forall a. HasCallStack => a
__IMPOSSIBLE__ -- bindBuiltinEquality v
           | [Char]
s forall a. Eq a => a -> a -> Bool
== [Char]
builtinBool     -> Term -> TCM ()
bindBuiltinBool     Term
v
           | [Char]
s forall a. Eq a => a -> a -> Bool
== [Char]
builtinNat      -> Term -> TCM ()
bindBuiltinNat      Term
v
           | [Char]
s forall a. Eq a => a -> a -> Bool
== [Char]
builtinInteger  -> Term -> TCM ()
bindBuiltinInt      Term
v
           | [Char]
s forall a. Eq a => a -> a -> Bool
== [Char]
builtinUnit     -> Term -> TCM ()
bindBuiltinUnit     Term
v
           | [Char]
s forall a. Eq a => a -> a -> Bool
== [Char]
builtinSigma    -> Term -> TCM ()
bindBuiltinSigma    Term
v
           | [Char]
s forall a. Eq a => a -> a -> Bool
== [Char]
builtinList     -> [Char] -> Term -> TCM ()
bindBuiltinData [Char]
s   Term
v
           | [Char]
s forall a. Eq a => a -> a -> Bool
== [Char]
builtinMaybe    -> [Char] -> Term -> TCM ()
bindBuiltinData [Char]
s   Term
v
           | Bool
otherwise            -> [Char] -> Term -> TCM ()
bindBuiltinName [Char]
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
$ [Char] -> Expr -> TypeError
BuiltinMustBeConstructor [Char]
s Expr
e

        let v :: Term
v@(Con ConHead
h ConInfo
_ []) = Term -> Term
name Term
v0

        [Char] -> Term -> TCM ()
bindBuiltinName [Char]
s Term
v

        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Char]
s forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[Char]
builtinFalse, [Char]
builtinTrue]) TCM ()
checkBuiltinBool

      BuiltinPrim [Char]
pfname Term -> TCM ()
axioms -> do
        case Expr
e of
          A.Def QName
qx -> do

            PrimImpl Type
t PrimFun
pf <- [Char] -> TCM PrimitiveImpl
lookupPrimitiveFunction [Char]
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
                mcc :: Maybe CompiledClauses
mcc = Definition -> Maybe CompiledClauses
defCompiled Definition
info
                inv :: FunctionInverse
inv = Definition -> FunctionInverse
defInverse Definition
info
            [Char] -> PrimFun -> TCM ()
bindPrimitive [Char]
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 :: [Char]
primName     = [Char]
pfname
                                                       , primClauses :: [Clause]
primClauses  = [Clause]
cls
                                                       , primInv :: FunctionInverse
primInv      = FunctionInverse
inv
                                                       , primCompiled :: Maybe CompiledClauses
primCompiled = Maybe CompiledClauses
mcc } }

            -- needed? yes, for checking equations for mul
            [Char] -> Term -> TCM ()
bindBuiltinName [Char]
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]
++ [Char]
s forall a. [a] -> [a] -> [a]
++ [Char]
" must be bound to a function"

      BuiltinSort{} -> forall a. HasCallStack => a
__IMPOSSIBLE__ -- always a "BuiltinNoDef"

      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]
++ [Char]
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
                [Char] -> QName -> Type -> TCM ()
builtinSizeHook [Char]
s QName
q Type
t'
                -- And compilation pragmas for base types
                forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Char]
s forall a. Eq a => a -> a -> Bool
== [Char]
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 ([Char]
s forall a. Eq a => a -> a -> Bool
== [Char]
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 ([Char]
s forall a. Eq a => a -> a -> Bool
== [Char]
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 ([Char]
s forall a. Eq a => a -> a -> Bool
== [Char]
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 ([Char]
s forall a. Eq a => a -> a -> Bool
== [Char]
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 ([Char]
s forall a. Eq a => a -> a -> Bool
== [Char]
builtinPathP)  forall a b. (a -> b) -> a -> b
$ QName -> TCM ()
builtinPathPHook QName
q
                [Char] -> Term -> TCM ()
bindBuiltinName [Char]
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 | [Char]
s forall a. Eq a => a -> a -> Bool
== [Char]
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           -> [Char] -> Term -> TCM ()
bindBuiltinName [Char]
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})

-- | Bind a builtin thing to an expression.
bindBuiltin :: String -> ResolvedName -> TCM ()
bindBuiltin :: [Char] -> ResolvedName -> TCM ()
bindBuiltin [Char]
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
    -- Andreas, 2017-11-01, issue #2824
    -- Only raise an error if the name for the builtin is defined in a parametrized module.
    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
$ [Char] -> TypeError
BuiltinInParameterisedModule [Char]
b
    -- Get the non-empty list of AbstractName for x
    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
    -- For ambiguous names, we check all of their definitions:
    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
$ ((Int
0 forall a. Eq a => a -> a -> Bool
==) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Sized a => a -> Int
size) 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
  -- Since the name was define in a parameter-free context, we can switch to the empty context.
  -- (And we should!)
  forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ do
  if | [Char]
b forall a. Eq a => a -> a -> Bool
== [Char]
builtinRefl  -> forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> Warning
OldBuiltin [Char]
b [Char]
builtinEquality
     | [Char]
b forall a. Eq a => a -> a -> Bool
== [Char]
builtinZero  -> forall {m :: * -> *}. MonadWarning m => [Char] -> [Char] -> m ()
now [Char]
builtinNat [Char]
b
     | [Char]
b forall a. Eq a => a -> a -> Bool
== [Char]
builtinSuc   -> forall {m :: * -> *}. MonadWarning m => [Char] -> [Char] -> m ()
now [Char]
builtinNat [Char]
b
     | [Char]
b forall a. Eq a => a -> a -> Bool
== [Char]
builtinNil   -> forall {m :: * -> *}. MonadWarning m => [Char] -> [Char] -> m ()
now [Char]
builtinList [Char]
b
     | [Char]
b forall a. Eq a => a -> a -> Bool
== [Char]
builtinCons  -> forall {m :: * -> *}. MonadWarning m => [Char] -> [Char] -> m ()
now [Char]
builtinList [Char]
b
     | [Char]
b forall a. Eq a => a -> a -> Bool
== [Char]
builtinInf   -> ResolvedName -> TCM ()
bindBuiltinInf ResolvedName
x
     | [Char]
b forall a. Eq a => a -> a -> Bool
== [Char]
builtinSharp -> ResolvedName -> TCM ()
bindBuiltinSharp ResolvedName
x
     | [Char]
b forall a. Eq a => a -> a -> Bool
== [Char]
builtinFlat  -> ResolvedName -> TCM ()
bindBuiltinFlat ResolvedName
x
     | [Char]
b forall a. Eq a => a -> a -> Bool
== [Char]
builtinEquality -> ResolvedName -> TCM ()
bindBuiltinEquality ResolvedName
x
     | Just BuiltinInfo
i <- [Char] -> Maybe BuiltinInfo
findBuiltinInfo [Char]
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 [Char]
b
  where
    now :: [Char] -> [Char] -> m ()
now [Char]
new [Char]
b = forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall a b. (a -> b) -> a -> b
$ [Char] -> [Char] -> Warning
OldBuiltin [Char]
b [Char]
new

isUntypedBuiltin :: String -> Bool
isUntypedBuiltin :: [Char] -> Bool
isUntypedBuiltin = forall a. Ord a => [a] -> a -> Bool
hasElem [ [Char]
builtinFromNat, [Char]
builtinFromNeg, [Char]
builtinFromString ]

bindUntypedBuiltin :: String -> ResolvedName -> TCM ()
bindUntypedBuiltin :: [Char] -> ResolvedName -> TCM ()
bindUntypedBuiltin [Char]
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 = [Char] -> Term -> TCM ()
bindBuiltinName [Char]
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]
++ [Char]
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

-- | Bind a builtin thing to a new name.
--
-- Since their type is closed, it does not matter whether we are in a
-- parameterized module when we declare them.
-- We simply ignore the parameters.
bindBuiltinNoDef :: String -> A.QName -> TCM ()
bindBuiltinNoDef :: [Char] -> QName -> TCM ()
bindBuiltinNoDef [Char]
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 ([Char]
b forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[Char]]
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]
++ [Char]
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
<$> [Char] -> Maybe BuiltinInfo
findBuiltinInfo [Char]
b of

    Just (BuiltinPostulate Relevance
rel TCM Type
mt) -> do
      -- We start by adding the corresponding postulate
      Type
t <- TCM Type
mt
      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 Defn
def
      -- And we then *modify* the definition based on our needs:
      -- We add polarity information for SIZE-related definitions
      [Char] -> QName -> Type -> TCM ()
builtinSizeHook [Char]
b QName
q Type
t
      -- Finally, bind the BUILTIN in the environment.
      [Char] -> Term -> TCM ()
bindBuiltinName [Char]
b forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
q []
      where
        -- Andreas, 2015-02-14
        -- Special treatment of SizeUniv, should maybe be a primitive.
        def :: Defn
def | [Char]
b forall a. Eq a => a -> a -> Bool
== [Char]
builtinSizeUniv = FunctionData -> Defn
FunctionDefn forall a b. (a -> b) -> a -> b
$ FunctionData
emptyFunctionData
                { _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 [Char]
name Term -> TCM ()
axioms) -> do
      PrimImpl Type
t PrimFun
pf <- [Char] -> TCM PrimitiveImpl
lookupPrimitiveFunction [Char]
name
      [Char] -> PrimFun -> TCM ()
bindPrimitive [Char]
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 :: [Char]
primName     = [Char]
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 [])
                          }
      QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
q ArgInfo
defaultArgInfo QName
q Type
t Defn
def
      Term -> TCM ()
axioms Term
v
      [Char] -> Term -> TCM ()
bindBuiltinName [Char]
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
      let
        ch :: ConHead
ch = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
q DataOrRecord
IsData Induction
Inductive []
        def :: Defn
def = Constructor
              { conPars :: Int
conPars   = Int
0   -- Andrea TODO: fix zeros
              , conArity :: Int
conArity  = Int
0
              , conSrcCon :: ConHead
conSrcCon = ConHead
ch
              , conData :: QName
conData   = QName
d
              , conAbstr :: IsAbstract
conAbstr  = IsAbstract
ConcreteDef
              , conInd :: Induction
conInd    = Induction
Inductive
              , 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
              }
      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 ([Char]
b forall a. Eq a => a -> a -> Bool
== [Char]
builtinReflId)     forall a b. (a -> b) -> a -> b
$ QName -> TCM ()
builtinReflIdHook QName
q

      [Char] -> Term -> TCM ()
bindBuiltinName [Char]
b forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
ch ConInfo
ConOSystem []

    Just (BuiltinData TCM Type
mt [[Char]]
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 ([Char]
b forall a. Eq a => a -> a -> Bool
== [Char]
builtinId)     forall a b. (a -> b) -> a -> b
$ QName -> TCM ()
builtinIdHook QName
q
      [Char] -> Term -> TCM ()
bindBuiltinName [Char]
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       = []     -- Constructors are added later
              , 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 -- Id has custom transp def.
              , dataTransp :: Maybe QName
dataTransp     = forall a. Maybe a
Nothing
              }

    Just (BuiltinSort [Char]
sortname) -> do
      let s :: Sort
s = case [Char]
sortname of
                [Char]
"primSet"      -> Integer -> Sort
mkType Integer
0
                [Char]
"primProp"     -> Integer -> Sort
mkProp Integer
0
                [Char]
"primStrictSet" -> Integer -> Sort
mkSSet Integer
0
                [Char]
"primSetOmega" -> forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
IsFibrant Integer
0
                [Char]
"primStrictSetOmega" -> forall t. IsFibrant -> Integer -> Sort' t
Inf IsFibrant
IsStrict Integer
0
                [Char]
"primIntervalUniv" -> forall t. Sort' t
IntervalUniv
                [Char]
_              -> forall a. HasCallStack => a
__IMPOSSIBLE__
          def :: Defn
def = [Char] -> Sort -> Defn
PrimitiveSort [Char]
sortname Sort
s
      -- Check for the cubical flag if the sort requries it
      case [Char]
sortname of
        [Char]
"primIntervalUniv" -> Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
""
        [Char]
_ -> 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
      [Char] -> Term -> TCM ()
bindBuiltinName [Char]
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__ -- typeError $ NoSuchBuiltinName b


builtinKindOfName :: String -> Maybe KindOfName
builtinKindOfName :: [Char] -> Maybe KindOfName
builtinKindOfName = BuiltinInfo -> KindOfName
distinguish forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> [Char] -> Maybe BuiltinInfo
findBuiltinInfo
  where
  distinguish :: BuiltinInfo -> KindOfName
distinguish BuiltinInfo
d = case BuiltinInfo -> BuiltinDescriptor
builtinDesc BuiltinInfo
d of
    BuiltinDataCons{}  -> KindOfName
ConName
    BuiltinData{}      -> KindOfName
DataName       -- Andreas, 2020-04-13: Crude.  Could be @RecName@.
    BuiltinPrim{}      -> KindOfName
PrimName
    BuiltinPostulate{} -> KindOfName
AxiomName
    BuiltinSort{}      -> KindOfName
PrimName
    BuiltinUnknown{}   -> KindOfName
OtherDefName