{-# OPTIONS_GHC -Wunused-imports #-}

{-# LANGUAGE NondecreasingIndentation #-}

module Agda.TypeChecking.Rules.Builtin
  ( bindBuiltin
  , bindBuiltinNoDef
  , builtinKindOfName
  , bindPostulatedName
  , isUntypedBuiltin
  , bindUntypedBuiltin
  ) where

import Prelude hiding (null)

import Control.Monad
import Control.Monad.Except
import Control.Monad.Trans.Maybe

import Data.List (find, sortBy)
import Data.Function (on)

import Agda.Interaction.Options.Base

import qualified Agda.Syntax.Abstract as A
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.Syntax.Position
import Agda.Syntax.Scope.Base

import Agda.TypeChecking.Monad

import qualified Agda.TypeChecking.CompiledClause as CC
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints ( noConstraints )
import Agda.TypeChecking.Functions
import Agda.TypeChecking.Names
import Agda.TypeChecking.Pretty
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Positivity.Occurrence
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Rules.Term ( checkExpr , inferExpr )
import Agda.TypeChecking.Warnings

import {-# SOURCE #-} Agda.TypeChecking.Rules.Builtin.Coinduction
import {-# SOURCE #-} Agda.TypeChecking.Rewriting

import Agda.Utils.Functor
import Agda.Utils.List
import Agda.Utils.List1 (pattern (:|))
import Agda.Utils.Maybe
import Agda.Utils.Monad
import Agda.Utils.Null
import Agda.Utils.Size

import Agda.Utils.Impossible

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

coreBuiltins :: [BuiltinInfo]
coreBuiltins :: [BuiltinInfo]
coreBuiltins =
  [ (BuiltinId
builtinList                             BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData (forall (m :: * -> *). Applicative m => m Type
tset forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Applicative m => m Type
tset) [BuiltinId
builtinNil, BuiltinId
builtinCons])
  , (BuiltinId
builtinArg                              BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData (forall (m :: * -> *). Applicative m => m Type
tset forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Applicative m => m Type
tset) [BuiltinId
builtinArgArg])
  , (BuiltinId
builtinAbs                              BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData (forall (m :: * -> *). Applicative m => m Type
tset forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Applicative m => m Type
tset) [BuiltinId
builtinAbsAbs])
  , (BuiltinId
builtinArgInfo                          BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinArgArgInfo])
  , (BuiltinId
builtinBool                             BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinTrue, BuiltinId
builtinFalse])
  , (BuiltinId
builtinNat                              BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinZero, BuiltinId
builtinSuc])
  , (BuiltinId
builtinMaybe                            BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData (forall (m :: * -> *). Applicative m => m Type
tset forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Applicative m => m Type
tset) [BuiltinId
builtinNothing, BuiltinId
builtinJust])
  , (BuiltinId
builtinSigma                            BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData (forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
                                                              forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"la" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
                                                              forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"lb" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
b ->
                                                              forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"A" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a) forall a b. (a -> b) -> a -> b
$ \NamesT (TCMT IO) Term
bA ->
                                                              forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"B" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
b)) forall a b. (a -> b) -> a -> b
$ \NamesT (TCMT IO) Term
bB ->
                                                              ((Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
b))
                                                              )
                                                             [BuiltinId
BuiltinSigmaCon])
  , (BuiltinId
builtinUnit                             BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinUnitUnit])  -- actually record, but they are treated the same
  , (BuiltinId
builtinAgdaLiteral                      BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinAgdaLitNat, BuiltinId
builtinAgdaLitWord64, BuiltinId
builtinAgdaLitFloat,
                                                                   BuiltinId
builtinAgdaLitChar, BuiltinId
builtinAgdaLitString,
                                                                   BuiltinId
builtinAgdaLitQName, BuiltinId
builtinAgdaLitMeta])
  , (BuiltinId
builtinAgdaPattern                      BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinAgdaPatVar, BuiltinId
builtinAgdaPatCon, BuiltinId
builtinAgdaPatDot,
                                                                   BuiltinId
builtinAgdaPatLit, BuiltinId
builtinAgdaPatProj, BuiltinId
builtinAgdaPatAbsurd])
  , (BuiltinId
builtinAgdaPatVar                       BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tpat))
  , (BuiltinId
builtinAgdaPatCon                       BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
tpat) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tpat))
  , (BuiltinId
builtinAgdaPatDot                       BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tpat))
  , (BuiltinId
builtinAgdaPatLit                       BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tliteral forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tpat))
  , (BuiltinId
builtinAgdaPatProj                      BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tpat))
  , (BuiltinId
builtinAgdaPatAbsurd                    BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tpat))
  , (BuiltinId
builtinLevel                            BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tLevelUniv)
  , (BuiltinId
builtinWord64                           BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tset)
  , (BuiltinId
builtinInteger                          BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinIntegerPos, BuiltinId
builtinIntegerNegSuc])
  , (BuiltinId
builtinIntegerPos                       BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tinteger))
  , (BuiltinId
builtinIntegerNegSuc                    BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tinteger))
  , (BuiltinId
builtinFloat                            BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tset)
  , (BuiltinId
builtinChar                             BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tset)
  , (BuiltinId
builtinString                           BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tset)
  , (BuiltinId
builtinQName                            BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tset)
  , (BuiltinId
builtinAgdaMeta                         BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tset)
  , (BuiltinId
builtinIO                               BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *). Applicative m => m Type
tset forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Applicative m => m Type
tset))
  , (BuiltinId
builtinPath                             BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Maybe (TCM Type) -> (Term -> Type -> TCM ()) -> BuiltinDescriptor
BuiltinUnknown
                                                             (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
"" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                                             forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (
                                                              forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0) forall a b. (a -> b) -> a -> b
$
                                                              (forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
                                                              (forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
                                                              forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
1)))
                                                             Term -> Type -> TCM ()
verifyPath)
  , (BuiltinId
builtinPathP                            BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$
                                                              forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
nPi [Char]
"A" (forall {t}. TCMT IO (Type'' t Term)
tinterval forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0)) forall a b. (a -> b) -> a -> b
$
                                                              (forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
                                                              (forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
                                                              forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
1)))
  , (BuiltinId
builtinIntervalUniv                     BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> BuiltinSort -> BuiltinDescriptor
BuiltinSort BuiltinSort
SortIntervalUniv)
  , (BuiltinId
builtinInterval                         BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData (Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
"" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
                                                              (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort forall t. Sort' t
IntervalUniv)) [BuiltinId
builtinIZero,BuiltinId
builtinIOne])
  , (BuiltinId
builtinSub                              BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
                                                                   forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"A" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a) (Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
                                                                   forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"φ" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall {t}. TCMT IO (Type'' t Term)
tinterval) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi ->
                                                                   forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el's NamesT (TCMT IO) Term
a (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPartial forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bA) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (Level -> Type
ssort forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. t -> Level' t
atomicLevel forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a)
                                                                  ))
  , (BuiltinId
builtinSubIn                            BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
                                                                   forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
                                                                   forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"A" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a) (Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
                                                                   forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"φ" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall {t}. TCMT IO (Type'' t Term)
tinterval) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi ->
                                                                   forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"x" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
bA) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
x ->
                                                                   forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el's NamesT (TCMT IO) Term
a forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSub forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"o" (\ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Term
x)))
  , (BuiltinId
builtinIZero                            BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons forall {t}. TCMT IO (Type'' t Term)
tinterval)
  , (BuiltinId
builtinIOne                             BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons forall {t}. TCMT IO (Type'' t Term)
tinterval)
  , (BuiltinId
builtinPartial                          BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimPartial (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()))
  , (BuiltinId
builtinPartialP                         BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimPartialP (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()))
  , (BuiltinId
builtinIsOne                            BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall {t}. TCMT IO (Type'' t Term)
tinterval forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *) a. Monad m => a -> m a
return (Level -> Type
ssort forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
0)))
  , (BuiltinId
builtinItIsOne                          BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall (m :: * -> *). Functor m => m Term -> m Type
elSSet forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne))
  , (BuiltinId
builtinIsOne1                           BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
                                                                   forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"i" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall {t}. TCMT IO (Type'' t Term)
tinterval) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
i ->
                                                                   forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"j" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall {t}. TCMT IO (Type'' t Term)
tinterval) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
j ->
                                                                   forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"i1" (forall (m :: * -> *). Functor m => m Term -> m Type
elSSet forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
i1 ->
                                                                   (forall (m :: * -> *). Functor m => m Term -> m Type
elSSet forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
j))))
  , (BuiltinId
builtinIsOne2                           BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
                                                                   forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"i" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall {t}. TCMT IO (Type'' t Term)
tinterval) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
i ->
                                                                   forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"j" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall {t}. TCMT IO (Type'' t Term)
tinterval) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
j ->
                                                                   forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"j1" (forall (m :: * -> *). Functor m => m Term -> m Type
elSSet forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
j) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
j1 ->
                                                                   (forall (m :: * -> *). Functor m => m Term -> m Type
elSSet forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
i forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
j))))
  , (BuiltinId
builtinIsOneEmpty                       BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Cubical -> TCM Type -> BuiltinDescriptor
builtinPostulateC Cubical
CErased (forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
                                                                   forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"l" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
l ->
                                                                   forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"A" (forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"o" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ ->
                                                                                  forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
l) (Sort -> Term
Sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
l)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
                                                                   forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"o" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero) (\ NamesT (TCMT IO) Term
o ->
                                                                        forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
l forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
Applicative m =>
ArgInfo -> m Term -> m Term -> m Term
gApply' (forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
Irrelevant ArgInfo
defaultArgInfo) NamesT (TCMT IO) Term
bA NamesT (TCMT IO) Term
o)))

  , (BuiltinId
builtinId                               BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData (forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
(>>) (Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
"") forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$
                                                              forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0) forall a b. (a -> b) -> a -> b
$
                                                              (forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
                                                              (forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
                                                             forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
1)) [BuiltinId
builtinReflId])
  , (BuiltinId
builtinReflId                           BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
(>>) (Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
"") forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] forall a b. (a -> b) -> a -> b
$
                                                              forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"a" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
l ->
                                                              forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"A" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
l) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
                                                              forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"x" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
l NamesT (TCMT IO) Term
bA) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
x ->
                                                              forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
l (forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primId forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
x forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
x)))
  , (BuiltinId
builtinEquiv                            BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Maybe (TCM Type) -> (Term -> Type -> TCM ()) -> BuiltinDescriptor
BuiltinUnknown (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
"" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (
                                                                    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"l" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
                                                                    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"l'" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
b ->
                                                                    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"A" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a) forall a b. (a -> b) -> a -> b
$ \NamesT (TCMT IO) Term
bA ->
                                                                    forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"B" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
b) forall a b. (a -> b) -> a -> b
$ \NamesT (TCMT IO) Term
bB ->
                                                                    ((Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
b))
                                                                  ))
                                                                   (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()))
  , (BuiltinId
builtinEquivFun                         BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Maybe (TCM Type) -> (Term -> Type -> TCM ()) -> BuiltinDescriptor
BuiltinUnknown (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
"" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (
                                                                 forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"l" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
                                                                 forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"l'" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
b ->
                                                                 forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"A" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a) forall a b. (a -> b) -> a -> b
$ \NamesT (TCMT IO) Term
bA ->
                                                                 forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"B" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
b) forall a b. (a -> b) -> a -> b
$ \NamesT (TCMT IO) Term
bB ->
                                                                 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
b) (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquiv forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
b forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bB) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
                                                                 (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
b NamesT (TCMT IO) Term
bB)
                                                               ))
                                                                (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()))
  , (BuiltinId
builtinEquivProof                       BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Maybe (TCM Type) -> (Term -> Type -> TCM ()) -> BuiltinDescriptor
BuiltinUnknown (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
"" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (
                                                               forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"l" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
la ->
                                                               forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"l'" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
lb ->
                                                               forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"A" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
la) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
                                                               forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"B" (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
lb) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bB ->
                                                               forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"e" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
lb)
                                                                             (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquiv forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bB)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
e -> do
                                                               forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"b" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
lb NamesT (TCMT IO) Term
bB) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
b -> do
                                                                let f :: NamesT (TCMT IO) Term
f = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquivFun forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bA forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bB forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
e
                                                                    lub :: NamesT (TCMT IO) Term
lub = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
lb
                                                                    fiber :: NamesT (TCMT IO) Type
fiber = forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
lub
                                                                                (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSigma forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb
                                                                                  forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bA
                                                                                  forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"a" (\ NamesT (TCMT IO) Term
a ->
                                                                                         forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPath forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bB forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
f forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
b))
                                                                forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"φ" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall {t}. TCMT IO (Type'' t Term)
tinterval) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi ->
                                                                  forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"f" (forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"o" NamesT (TCMT IO) Term
phi (\ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Type
fiber)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
pfib ->
                                                                    forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
lub (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSub forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lub forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t a. Type'' t a -> a
unEl NamesT (TCMT IO) Type
fiber forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
pfib)
                                                             ))
                                                              (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()))
  , (BuiltinId
builtinTranspProof                       BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Maybe (TCM Type) -> (Term -> Type -> TCM ()) -> BuiltinDescriptor
BuiltinUnknown (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
"" forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (
                                                               forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' [Char]
"l" (forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
la -> do
                                                               forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"e" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall {t}. TCMT IO (Type'' t Term)
tinterval forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (Sort -> Type
sort forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
la)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
e -> do
                                                               let lb :: NamesT (TCMT IO) Term
lb = NamesT (TCMT IO) Term
la; bA :: NamesT (TCMT IO) Term
bA = NamesT (TCMT IO) Term
e forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero; bB :: NamesT (TCMT IO) Term
bB = NamesT (TCMT IO) Term
e forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
                                                               forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"φ" (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall {t}. TCMT IO (Type'' t Term)
tinterval) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi -> do
                                                               forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"a" (forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
[Char]
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' [Char]
"o" NamesT (TCMT IO) Term
phi (\ NamesT (TCMT IO) Term
_ -> forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
bA)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a -> do
                                                               let f :: NamesT (TCMT IO) Term
f = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrans forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" (\ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Term
la) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
e forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
                                                                   z :: NamesT (TCMT IO) Term
z = forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam [Char]
"o" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Term
f forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
a forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
o)
                                                               forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
[Char]
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' [Char]
"b" (forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el's NamesT (TCMT IO) Term
lb (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSub forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bB forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
z)) forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
b' -> do
                                                               let b :: NamesT (TCMT IO) Term
b = forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSubOut forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bB forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
phi forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
z forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
b'
                                                                   fiber :: NamesT (TCMT IO) Type
fiber = forall (m :: * -> *). Applicative m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
la
                                                                               (forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSigma forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
la forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb
                                                                                  forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
bA
                                                                                  forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"a" (\ NamesT (TCMT IO) Term
a ->
                                                                                         forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPath forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
lb forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
bB forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (NamesT (TCMT IO) Term
f forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
a) forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> NamesT (TCMT IO) Term
b))
                                                               NamesT (TCMT IO) Type
fiber
                                                             ))
                                                              (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()))
  , (BuiltinId
builtinAgdaSort                         BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset
                                                   [ BuiltinId
builtinAgdaSortSet, BuiltinId
builtinAgdaSortLit
                                                   , BuiltinId
builtinAgdaSortProp, BuiltinId
builtinAgdaSortPropLit
                                                   , BuiltinId
builtinAgdaSortInf, BuiltinId
builtinAgdaSortUnsupported])
  , (BuiltinId
builtinAgdaTerm                         BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset
                                                   [ BuiltinId
builtinAgdaTermVar, BuiltinId
builtinAgdaTermLam, BuiltinId
builtinAgdaTermExtLam
                                                   , BuiltinId
builtinAgdaTermDef, BuiltinId
builtinAgdaTermCon
                                                   , BuiltinId
builtinAgdaTermPi, BuiltinId
builtinAgdaTermSort
                                                   , BuiltinId
builtinAgdaTermLit, BuiltinId
builtinAgdaTermMeta
                                                   , BuiltinId
builtinAgdaTermUnsupported])
  , BuiltinId
builtinAgdaErrorPart                     BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [ BuiltinId
builtinAgdaErrorPartString, BuiltinId
builtinAgdaErrorPartTerm, BuiltinId
builtinAgdaErrorPartPatt, BuiltinId
builtinAgdaErrorPartName ]
  , BuiltinId
builtinAgdaErrorPartString               BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
terrorpart)
  , BuiltinId
builtinAgdaErrorPartTerm                 BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
terrorpart)
  , BuiltinId
builtinAgdaErrorPartPatt                 BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tpat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
terrorpart)
  , BuiltinId
builtinAgdaErrorPartName                 BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
terrorpart)
  , BuiltinId
builtinAgdaBlocker                       BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [ BuiltinId
builtinAgdaBlockerAll, BuiltinId
builtinAgdaBlockerAny, BuiltinId
builtinAgdaBlockerMeta ]
  , BuiltinId
builtinAgdaBlockerAny                    BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tblocker forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tblocker)
  , BuiltinId
builtinAgdaBlockerAll                    BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tblocker forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tblocker)
  , BuiltinId
builtinAgdaBlockerMeta                   BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tmeta forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tblocker)
  -- 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])
  , (BuiltinId
builtinHiding                           BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinHidden, BuiltinId
builtinInstance, BuiltinId
builtinVisible])
    -- Relevance
  , (BuiltinId
builtinRelevance                        BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinRelevant, BuiltinId
builtinIrrelevant])
  , (BuiltinId
builtinRelevant                         BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
trelevance)
  , (BuiltinId
builtinIrrelevant                       BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
trelevance)
    -- Quantity
  , (BuiltinId
builtinQuantity                         BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinQuantity0, BuiltinId
builtinQuantityω])
  , (BuiltinId
builtinQuantity0                        BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tquantity)
  , (BuiltinId
builtinQuantityω                        BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tquantity)
    -- Modality
  , (BuiltinId
builtinModality                         BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinModalityConstructor])
  , (BuiltinId
builtinModalityConstructor              BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
trelevance forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tquantity forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tmodality))
    -- Associativity
  , BuiltinId
builtinAssoc                             BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinAssocLeft, BuiltinId
builtinAssocRight, BuiltinId
builtinAssocNon]
  , BuiltinId
builtinAssocLeft                         BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tassoc
  , BuiltinId
builtinAssocRight                        BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tassoc
  , BuiltinId
builtinAssocNon                          BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tassoc
    -- Precedence
  , BuiltinId
builtinPrecedence                        BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinPrecRelated, BuiltinId
builtinPrecUnrelated]
  , BuiltinId
builtinPrecRelated                       BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tfloat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tprec)
  , BuiltinId
builtinPrecUnrelated                     BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tprec
    -- Fixity
  , BuiltinId
builtinFixity                            BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinFixityFixity]
  , BuiltinId
builtinFixityFixity                      BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tassoc forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tprec forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tfixity)
  -- 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))
  , (BuiltinId
builtinRewrite                          BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> Maybe (TCM Type) -> (Term -> Type -> TCM ()) -> BuiltinDescriptor
BuiltinUnknown forall a. Maybe a
Nothing Term -> Type -> TCM ()
verifyBuiltinRewrite)
  , (BuiltinId
builtinNil                              BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" forall (m :: * -> *). Applicative m => m Type
tset (forall (m :: * -> *). Functor m => m Term -> m Type
el (TCMT IO Term -> TCMT IO Term
list TCMT IO Term
v0))))
  , (BuiltinId
builtinCons                             BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" forall (m :: * -> *). Applicative m => m Type
tset (TCM Type
tv0 forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Functor m => m Term -> m Type
el (TCMT IO Term -> TCMT IO Term
list TCMT IO Term
v0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Functor m => m Term -> m Type
el (TCMT IO Term -> TCMT IO Term
list TCMT IO Term
v0))))
  , (BuiltinId
builtinNothing                          BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" forall (m :: * -> *). Applicative m => m Type
tset (forall (m :: * -> *). Functor m => m Term -> m Type
el (TCMT IO Term -> TCMT IO Term
tMaybe TCMT IO Term
v0))))
  , (BuiltinId
builtinJust                             BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" forall (m :: * -> *). Applicative m => m Type
tset (TCM Type
tv0 forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall (m :: * -> *). Functor m => m Term -> m Type
el (TCMT IO Term -> TCMT IO Term
tMaybe TCMT IO Term
v0))))
  , (BuiltinId
builtinZero                             BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tnat)
  , (BuiltinId
builtinSuc                              BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tnat))
  , (BuiltinId
builtinTrue                             BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tbool)
  , (BuiltinId
builtinFalse                            BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tbool)
  , (BuiltinId
builtinArgArg                           BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" forall (m :: * -> *). Applicative m => m Type
tset (TCM Type
targinfo forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tv0 forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
tv0)))
  , (BuiltinId
builtinAbsAbs                           BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" forall (m :: * -> *). Applicative m => m Type
tset (TCM Type
tstring  forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tv0 forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *} {t}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m (Type'' t Term) -> m Type
tabs TCM Type
tv0)))
  , (BuiltinId
builtinArgArgInfo                       BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
thiding forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tmodality forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
targinfo))
  , (BuiltinId
builtinAgdaTermVar                      BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
targs forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm))
  , (BuiltinId
builtinAgdaTermLam                      BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
thiding forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *} {t}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m (Type'' t Term) -> m Type
tabs TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm))
  , (BuiltinId
builtinAgdaTermExtLam                   BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tclause forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
targs forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm))
  , (BuiltinId
builtinAgdaTermDef                      BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
targs forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm))
  , (BuiltinId
builtinAgdaTermCon                      BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
targs forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm))
  , (BuiltinId
builtinAgdaTermPi                       BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
ttype forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *} {t}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m (Type'' t Term) -> m Type
tabs TCM Type
ttype forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm))
  , (BuiltinId
builtinAgdaTermSort                     BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tsort forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm))
  , (BuiltinId
builtinAgdaTermLit                      BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tliteral forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm))
  , (BuiltinId
builtinAgdaTermMeta                     BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tmeta forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
targs forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm))
  , (BuiltinId
builtinAgdaTermUnsupported              BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tterm)
  , (BuiltinId
builtinAgdaLitNat                       BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
  , (BuiltinId
builtinAgdaLitWord64                    BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tword64 forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
  , (BuiltinId
builtinAgdaLitFloat                     BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tfloat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
  , (BuiltinId
builtinAgdaLitChar                      BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tchar forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
  , (BuiltinId
builtinAgdaLitString                    BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
  , (BuiltinId
builtinAgdaLitQName                     BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
  , (BuiltinId
builtinAgdaLitMeta                      BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tmeta forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tliteral))
  , (BuiltinId
builtinHidden                           BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
thiding)
  , (BuiltinId
builtinInstance                         BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
thiding)
  , (BuiltinId
builtinVisible                          BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
thiding)
  , (BuiltinId
builtinSizeUniv                         BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate TCM Type
tsetOmega) -- SizeUniv : Setω
  , (BuiltinId
builtinSize                             BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate forall (m :: * -> *). Applicative m => m Type
tSizeUniv)
  , (BuiltinId
builtinSizeLt                           BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tsize forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
..--> forall (m :: * -> *). Applicative m => m Type
tSizeUniv))
  , (BuiltinId
builtinSizeSuc                          BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tsize forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsize))
  , (BuiltinId
builtinSizeInf                          BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate TCM Type
tsize)
  -- postulate max : {i : Size} -> Size< i -> Size< i -> Size< i
  , (BuiltinId
builtinSizeMax                          BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tsize forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsize forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsize))
     -- (hPi "i" tsize $ let a = el $ primSizeLt <@> v0 in (a --> a --> a)))
  , (BuiltinId
builtinAgdaSortSet                      BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsort))
  , (BuiltinId
builtinAgdaSortLit                      BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsort))
  , (BuiltinId
builtinAgdaSortProp                     BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsort))
  , (BuiltinId
builtinAgdaSortPropLit                  BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsort))
  , (BuiltinId
builtinAgdaSortInf                      BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tsort))
  , (BuiltinId
builtinAgdaSortUnsupported              BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tsort)
  , (BuiltinId
builtinNatPlus                          BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimNatPlus Term -> TCM ()
verifyPlus)
  , (BuiltinId
builtinNatMinus                         BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimNatMinus Term -> TCM ()
verifyMinus)
  , (BuiltinId
builtinNatTimes                         BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimNatTimes Term -> TCM ()
verifyTimes)
  , (BuiltinId
builtinNatDivSucAux                     BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimNatDivSucAux Term -> TCM ()
verifyDivSucAux)
  , (BuiltinId
builtinNatModSucAux                     BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimNatModSucAux Term -> TCM ()
verifyModSucAux)
  , (BuiltinId
builtinNatEquals                        BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimNatEquality Term -> TCM ()
verifyEquals)
  , (BuiltinId
builtinNatLess                          BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimNatLess Term -> TCM ()
verifyLess)
  , (BuiltinId
builtinLevelUniv                        BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> BuiltinSort -> BuiltinDescriptor
BuiltinSort BuiltinSort
SortLevelUniv)
  , (BuiltinId
builtinLevelZero                        BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimLevelZero (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()))
  , (BuiltinId
builtinLevelSuc                         BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimLevelSuc (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()))
  , (BuiltinId
builtinLevelMax                         BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> PrimitiveId -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim PrimitiveId
PrimLevelMax forall {m :: * -> *} {p}. Monad m => p -> m ()
verifyMax)
  , (BuiltinId
builtinProp                             BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> BuiltinSort -> BuiltinDescriptor
BuiltinSort BuiltinSort
SortProp)
  , (BuiltinId
builtinSet                              BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> BuiltinSort -> BuiltinDescriptor
BuiltinSort BuiltinSort
SortSet)
  , (BuiltinId
builtinStrictSet                        BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> BuiltinSort -> BuiltinDescriptor
BuiltinSort BuiltinSort
SortStrictSet)
  , (BuiltinId
builtinPropOmega                        BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> BuiltinSort -> BuiltinDescriptor
BuiltinSort BuiltinSort
SortPropOmega)
  , (BuiltinId
builtinSetOmega                         BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> BuiltinSort -> BuiltinDescriptor
BuiltinSort BuiltinSort
SortSetOmega)
  , (BuiltinId
builtinSSetOmega                        BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> BuiltinSort -> BuiltinDescriptor
BuiltinSort BuiltinSort
SortStrictSetOmega)
  , (BuiltinId
builtinAgdaClause                       BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinAgdaClauseClause, BuiltinId
builtinAgdaClauseAbsurd])
  , (BuiltinId
builtinAgdaClauseClause                 BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
ttelescope forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
tpat) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tclause))
  , (BuiltinId
builtinAgdaClauseAbsurd                 BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
ttelescope forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
tpat) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tclause))
  , (BuiltinId
builtinAgdaDefinition                   BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [BuiltinId] -> BuiltinDescriptor
BuiltinData forall (m :: * -> *). Applicative m => m Type
tset [BuiltinId
builtinAgdaDefinitionFunDef
                                                                  ,BuiltinId
builtinAgdaDefinitionDataDef
                                                                  ,BuiltinId
builtinAgdaDefinitionDataConstructor
                                                                  ,BuiltinId
builtinAgdaDefinitionRecordDef
                                                                  ,BuiltinId
builtinAgdaDefinitionPostulate
                                                                  ,BuiltinId
builtinAgdaDefinitionPrimitive])
  , (BuiltinId
builtinAgdaDefinitionFunDef             BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tclause forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tdefn))
  , (BuiltinId
builtinAgdaDefinitionDataDef            BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tdefn))
  , (BuiltinId
builtinAgdaDefinitionDataConstructor    BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tdefn))
  , (BuiltinId
builtinAgdaDefinitionRecordDef          BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
tqname) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tdefn))
  , (BuiltinId
builtinAgdaDefinitionPostulate          BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tdefn)
  , (BuiltinId
builtinAgdaDefinitionPrimitive          BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tdefn)
  , BuiltinId
builtinAgdaTCM                           BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0 forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0)
  , BuiltinId
builtinAgdaTCMReturn                     BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel  forall a b. (a -> b) -> a -> b
$
                                                                   forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$
                                                                   forall {f :: * -> *} {a}.
Functor f =>
Int -> f a -> f (Type'' Term a)
elV Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
  , BuiltinId
builtinAgdaTCMBind                       BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel  forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"b" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$
                                                                   forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
1) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"B" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
1) forall a b. (a -> b) -> a -> b
$
                                                                   forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
3 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
1) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> (forall {f :: * -> *} {a}.
Functor f =>
Int -> f a -> f (Type'' Term a)
elV Int
3 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
1) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
2 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0)) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
2 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
  , BuiltinId
builtinAgdaTCMUnify                      BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
  , BuiltinId
builtinAgdaTCMTypeError                  BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$ forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
terrorpart forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
  , BuiltinId
builtinAgdaTCMInferType                  BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm)
  , BuiltinId
builtinAgdaTCMCheckType                  BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
ttype forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm)
  , BuiltinId
builtinAgdaTCMNormalise                  BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm)
  , BuiltinId
builtinAgdaTCMReduce                     BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm)
  , BuiltinId
builtinAgdaTCMCatchError                 BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$
                                                                   forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
  , BuiltinId
builtinAgdaTCMGetContext                 BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ (forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Type
ttelescope))
  , BuiltinId
builtinAgdaTCMExtendContext              BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$
                                                                   TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
ttype forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
  , BuiltinId
builtinAgdaTCMInContext                  BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$
                                                                   TCM Type
ttelescope forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
  , BuiltinId
builtinAgdaTCMFreshName                  BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQName)
  , BuiltinId
builtinAgdaTCMDeclareDef                 BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
ttype forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
  , BuiltinId
builtinAgdaTCMDeclarePostulate           BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
ttype forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
  , BuiltinId
builtinAgdaTCMDeclareData                BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
ttype forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
  , BuiltinId
builtinAgdaTCMDefineData                 BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist (forall {m :: * -> *} {t} {t}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
-> m Term -> m (Type'' t Term) -> m (Type'' t Term) -> m Type
tpair forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero TCM Type
tqname TCM Type
ttype) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
  , BuiltinId
builtinAgdaTCMDefineFun                  BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tclause forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
  , BuiltinId
builtinAgdaTCMGetType                    BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm)
  , BuiltinId
builtinAgdaTCMGetDefinition              BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinition)
  , BuiltinId
builtinAgdaTCMQuoteTerm                  BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$ forall {f :: * -> *} {a}.
Functor f =>
Int -> f a -> f (Type'' Term a)
elV Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm)
  , BuiltinId
builtinAgdaTCMUnquoteTerm                BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$ TCM Type
tterm forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
  , BuiltinId
builtinAgdaTCMQuoteOmegaTerm             BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" TCM Type
tsetOmega forall a b. (a -> b) -> a -> b
$ (forall (m :: * -> *). Functor m => m Term -> m Type
elInf forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm)
  , BuiltinId
builtinAgdaTCMBlock                      BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$ TCM Type
tblocker forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
  , BuiltinId
builtinAgdaTCMCommit                     BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
  , BuiltinId
builtinAgdaTCMIsMacro                    BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primBool)
  , BuiltinId
builtinAgdaTCMWithNormalisation          BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$ TCM Type
tbool forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
  , BuiltinId
builtinAgdaTCMWithReconstructed          BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$ TCM Type
tbool forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
  , BuiltinId
builtinAgdaTCMWithExpandLast             BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$ TCM Type
tbool forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
  , BuiltinId
builtinAgdaTCMWithReduceDefs             BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$ (forall {m :: * -> *} {t} {t}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
-> m Term -> m (Type'' t Term) -> m (Type'' t Term) -> m Type
tpair forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero TCM Type
tbool (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tqname)) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
  , BuiltinId
builtinAgdaTCMAskNormalisation           BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ (forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Type
tbool))
  , BuiltinId
builtinAgdaTCMAskReconstructed           BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ (forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Type
tbool))
  , BuiltinId
builtinAgdaTCMAskExpandLast              BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ (forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Type
tbool))
  , BuiltinId
builtinAgdaTCMAskReduceDefs              BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ (forall t a. Type'' t a -> a
unEl forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall {m :: * -> *} {t} {t}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
-> m Term -> m (Type'' t Term) -> m (Type'' t Term) -> m Type
tpair forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero TCM Type
tbool (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tqname))))
  , BuiltinId
builtinAgdaTCMFormatErrorParts           BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
terrorpart forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primString)
  , BuiltinId
builtinAgdaTCMDebugPrint                 BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tnat forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
terrorpart forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)

  , BuiltinId
builtinAgdaTCMNoConstraints              BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$ forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
  , BuiltinId
builtinAgdaTCMRunSpeculative             BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"a" TCM Type
tlevel forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
[Char] -> m Type -> m Type -> m Type
hPi [Char]
"A" (forall {m :: * -> *}. Monad m => Int -> m Type
tsetL Int
0) forall a b. (a -> b) -> a -> b
$
                                                                   forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSigma forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
1 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0 forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Char] -> a -> Abs a
Abs [Char]
"_" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primBool)) forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {f :: * -> *}.
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0))
  , BuiltinId
builtinAgdaTCMExec                       BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {t}. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
-->
                                                                   forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ (forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSigma forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNat forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@>
                                                                          (ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Char] -> a -> Abs a
Abs [Char]
"_" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSigma forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primString forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@>
                                                                           (ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Char] -> a -> Abs a
Abs [Char]
"_" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primString)))))
  , BuiltinId
builtinAgdaTCMGetInstances               BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tmeta forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ (TCMT IO Term -> TCMT IO Term
list forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm))
  , BuiltinId
builtinAgdaTCMPragmaForeign              BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
  , BuiltinId
builtinAgdaTCMPragmaCompile              BuiltinId -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tqname forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> TCM Type
tstring forall (m :: * -> *). Applicative m => m Type -> m Type -> m Type
--> forall {m :: * -> *}.
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term -> m Type
tTCM_ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
  ]
  where
        |-> :: BuiltinId -> BuiltinDescriptor -> BuiltinInfo
(|->) = BuiltinId -> BuiltinDescriptor -> BuiltinInfo
BuiltinInfo

        v0 :: TCM Term
        v0 :: TCMT IO Term
v0 = forall (m :: * -> *). Applicative m => Int -> m Term
varM Int
0

        tv0 :: TCM Type
        tv0 :: TCM Type
tv0 = forall (m :: * -> *). Functor m => m Term -> m Type
el TCMT IO Term
v0

        arg :: TCM Term -> TCM Term
        arg :: TCMT IO Term -> TCMT IO Term
arg TCMT IO Term
t = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArg forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> TCMT IO Term
t

        elV :: Int -> f a -> f (Type'' Term a)
elV Int
x f a
a = forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
x) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
a

        tsetL :: Int -> m Type
tsetL Int
l    = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort (Int -> Sort
varSort Int
l)
        tsetOmega :: TCM Type
tsetOmega  = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ forall t. Univ -> Integer -> Sort' t
Inf Univ
UType Integer
0
        tlevel :: TCM Type
tlevel     = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel
        tlist :: TCMT IO (Type'' t Term) -> TCM Type
tlist TCMT IO (Type'' t Term)
x    = forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> TCMT IO Term
list (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t a. Type'' t a -> a
unEl TCMT IO (Type'' t Term)
x)
        tmaybe :: TCMT IO (Type'' t Term) -> TCM Type
tmaybe TCMT IO (Type'' t Term)
x   = forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> TCMT IO Term
tMaybe (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t a. Type'' t a -> a
unEl TCMT IO (Type'' t Term)
x)
        tpair :: m Term
-> m Term -> m (Type'' t Term) -> m (Type'' t Term) -> m Type
tpair m Term
lx m Term
ly m (Type'' t Term)
x m (Type'' t Term)
y = forall (m :: * -> *). Functor m => m Term -> m Type
el forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSigma
                            forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> m Term
lx
                            forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> m Term
ly
                            forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t a. Type'' t a -> a
unEl m (Type'' t Term)
x
                            forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> (ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Char] -> a -> Abs a
NoAbs [Char]
"_" forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t a. Type'' t a -> a
unEl m (Type'' t Term)
y)
        targ :: TCMT IO (Type'' t Term) -> TCM Type
targ TCMT IO (Type'' t Term)
x     = forall (m :: * -> *). Functor m => m Term -> m Type
el (TCMT IO Term -> TCMT IO Term
arg (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t a. Type'' t a -> a
unEl TCMT IO (Type'' t Term)
x))
        tabs :: m (Type'' t Term) -> m Type
tabs m (Type'' t Term)
x     = forall (m :: * -> *). Functor m => m Term -> m Type
el (forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAbs forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall t a. Type'' t a -> a
unEl m (Type'' t Term)
x)
        targs :: TCM Type
targs      = forall (m :: * -> *). Functor m => m Term -> m Type
el (TCMT IO Term -> TCMT IO Term
list (TCMT IO Term -> TCMT IO Term
arg forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm))
        tterm :: TCM Type
tterm      = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm
        terrorpart :: TCM Type
terrorpart = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaErrorPart
        tnat :: TCM Type
tnat       = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNat
        tword64 :: TCM Type
tword64    = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primWord64
        tinteger :: TCM Type
tinteger   = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInteger
        tfloat :: TCM Type
tfloat     = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFloat
        tchar :: TCM Type
tchar      = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primChar
        tstring :: TCM Type
tstring    = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primString
        tqname :: TCM Type
tqname     = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQName
        tmeta :: TCM Type
tmeta      = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaMeta
        tblocker :: TCM Type
tblocker   = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaBlocker
        tsize :: TCM Type
tsize      = forall t a. Sort' t -> a -> Type'' t a
El Sort
sSizeUniv forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSize
        tbool :: TCM Type
tbool      = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primBool
        thiding :: TCM Type
thiding    = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHiding
        trelevance :: TCM Type
trelevance = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRelevance
        tquantity :: TCM Type
tquantity  = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQuantity
        tmodality :: TCM Type
tmodality  = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primModality
        tassoc :: TCM Type
tassoc     = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAssoc
        tprec :: TCM Type
tprec      = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPrecedence
        tfixity :: TCM Type
tfixity    = forall (m :: * -> *). Functor m => m Term -> m Type
el forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFixity
--        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}.
Names
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
verify [[Char]
"n",[Char]
"m"] forall a b. (a -> b) -> a -> b
$ \Term -> Term -> Term
(@@) Term
zero Term -> Term
suc Term -> Term -> TCM ()
(==) Term -> Term -> TCM ()
(===) [TCM ()] -> TCM ()
choice -> do
                let m :: Term
m = Int -> Term
var Int
0
                    n :: Term
n = Int -> Term
var Int
1
                    Term
x + :: Term -> Term -> Term
+ Term
y = Term
plus Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
y

                -- 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}.
Names
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
verify [[Char]
"n",[Char]
"m"] forall a b. (a -> b) -> a -> b
$ \Term -> Term -> Term
(@@) Term
zero Term -> Term
suc Term -> Term -> TCM ()
(==) Term -> Term -> TCM ()
(===) [TCM ()] -> TCM ()
choice -> do
                let m :: Term
m = Int -> Term
var Int
0
                    n :: Term
n = Int -> Term
var Int
1
                    Term
x - :: Term -> Term -> Term
- Term
y = Term
minus Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
y

                -- 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}.
Names
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
verify [[Char]
"n",[Char]
"m"] forall a b. (a -> b) -> a -> b
$ \Term -> Term -> Term
(@@) Term
zero Term -> Term
suc Term -> Term -> TCM ()
(==) Term -> Term -> TCM ()
(===) [TCM ()] -> TCM ()
choice -> do
                let m :: Term
m = Int -> Term
var Int
0
                    n :: Term
n = Int -> Term
var Int
1
                    Term
x + :: Term -> Term -> Term
+ Term
y = Term
plus  Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
y
                    Term
x * :: Term -> Term -> Term
* Term
y = Term
times Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
y

                [TCM ()] -> TCM ()
choice
                    [ do Term
n Term -> Term -> Term
* Term
zero Term -> Term -> TCM ()
== Term
zero
                         [TCM ()] -> TCM ()
choice [ (Term
n Term -> Term -> Term
* Term -> Term
suc Term
m) Term -> Term -> TCM ()
== (Term
n Term -> Term -> Term
+ (Term
n Term -> Term -> Term
* Term
m))
                                , (Term
n Term -> Term -> Term
* Term -> Term
suc Term
m) Term -> Term -> TCM ()
== ((Term
n Term -> Term -> Term
* Term
m) Term -> Term -> Term
+ Term
n)
                                ]
                    , do Term
zero Term -> Term -> Term
* Term
n Term -> Term -> TCM ()
== Term
zero
                         [TCM ()] -> TCM ()
choice [ (Term -> Term
suc Term
n Term -> Term -> Term
* Term
m) Term -> Term -> TCM ()
== (Term
m Term -> Term -> Term
+ (Term
n Term -> Term -> Term
* Term
m))
                                , (Term -> Term
suc Term
n Term -> Term -> Term
* Term
m) Term -> Term -> TCM ()
== ((Term
n Term -> Term -> Term
* Term
m) Term -> Term -> Term
+ Term
m)
                                ]
                    ]

        verifyDivSucAux :: Term -> TCM ()
verifyDivSucAux Term
dsAux =
            forall {a}.
Names
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
verify [[Char]
"k",[Char]
"m",[Char]
"n",[Char]
"j"] forall a b. (a -> b) -> a -> b
$ \Term -> Term -> Term
(@@) Term
zero Term -> Term
suc Term -> Term -> TCM ()
(==) Term -> Term -> TCM ()
(===) [TCM ()] -> TCM ()
choice -> do
                let aux :: Term -> Term -> Term -> Term -> Term
aux Term
k Term
m Term
n Term
j = Term
dsAux Term -> Term -> Term
@@ Term
k Term -> Term -> Term
@@ Term
m Term -> Term -> Term
@@ Term
n Term -> Term -> Term
@@ Term
j
                    k :: Term
k           = Int -> Term
var Int
0
                    m :: Term
m           = Int -> Term
var Int
1
                    n :: Term
n           = Int -> Term
var Int
2
                    j :: Term
j           = Int -> Term
var Int
3

                Term -> Term -> Term -> Term -> Term
aux Term
k Term
m Term
zero    Term
j       Term -> Term -> TCM ()
== Term
k
                Term -> Term -> Term -> Term -> Term
aux Term
k Term
m (Term -> Term
suc Term
n) Term
zero    Term -> Term -> TCM ()
== Term -> Term -> Term -> Term -> Term
aux (Term -> Term
suc Term
k) Term
m Term
n Term
m
                Term -> Term -> Term -> Term -> Term
aux Term
k Term
m (Term -> Term
suc Term
n) (Term -> Term
suc Term
j) Term -> Term -> TCM ()
== Term -> Term -> Term -> Term -> Term
aux Term
k Term
m Term
n Term
j

        verifyModSucAux :: Term -> TCM ()
verifyModSucAux Term
dsAux =
            forall {a}.
Names
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
verify [[Char]
"k",[Char]
"m",[Char]
"n",[Char]
"j"] forall a b. (a -> b) -> a -> b
$ \Term -> Term -> Term
(@@) Term
zero Term -> Term
suc Term -> Term -> TCM ()
(==) Term -> Term -> TCM ()
(===) [TCM ()] -> TCM ()
choice -> do
                let aux :: Term -> Term -> Term -> Term -> Term
aux Term
k Term
m Term
n Term
j = Term
dsAux Term -> Term -> Term
@@ Term
k Term -> Term -> Term
@@ Term
m Term -> Term -> Term
@@ Term
n Term -> Term -> Term
@@ Term
j
                    k :: Term
k           = Int -> Term
var Int
0
                    m :: Term
m           = Int -> Term
var Int
1
                    n :: Term
n           = Int -> Term
var Int
2
                    j :: Term
j           = Int -> Term
var Int
3

                Term -> Term -> Term -> Term -> Term
aux Term
k Term
m Term
zero    Term
j       Term -> Term -> TCM ()
== Term
k
                Term -> Term -> Term -> Term -> Term
aux Term
k Term
m (Term -> Term
suc Term
n) Term
zero    Term -> Term -> TCM ()
== Term -> Term -> Term -> Term -> Term
aux Term
zero Term
m Term
n Term
m
                Term -> Term -> Term -> Term -> Term
aux Term
k Term
m (Term -> Term
suc Term
n) (Term -> Term
suc Term
j) Term -> Term -> TCM ()
== Term -> Term -> Term -> Term -> Term
aux (Term -> Term
suc Term
k) Term
m Term
n Term
j

        verifyEquals :: Term -> TCM ()
verifyEquals Term
eq =
            forall {a}.
Names
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
verify [[Char]
"n",[Char]
"m"] forall a b. (a -> b) -> a -> b
$ \Term -> Term -> Term
(@@) Term
zero Term -> Term
suc Term -> Term -> TCM ()
(==) Term -> Term -> TCM ()
(===) [TCM ()] -> TCM ()
choice -> do
            Term
true  <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrue
            Term
false <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFalse
            let Term
x == :: Term -> Term -> Term
== Term
y = Term
eq Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
y
                m :: Term
m      = Int -> Term
var Int
0
                n :: Term
n      = Int -> Term
var Int
1
            (Term
zero  Term -> Term -> Term
== Term
zero ) Term -> Term -> TCM ()
=== Term
true
            (Term -> Term
suc Term
n Term -> Term -> Term
== Term -> Term
suc Term
m) Term -> Term -> TCM ()
=== (Term
n Term -> Term -> Term
== Term
m)
            (Term -> Term
suc Term
n Term -> Term -> Term
== Term
zero ) Term -> Term -> TCM ()
=== Term
false
            (Term
zero  Term -> Term -> Term
== Term -> Term
suc Term
n) Term -> Term -> TCM ()
=== Term
false

        verifyLess :: Term -> TCM ()
verifyLess Term
leq =
            forall {a}.
Names
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
verify [[Char]
"n",[Char]
"m"] forall a b. (a -> b) -> a -> b
$ \Term -> Term -> Term
(@@) Term
zero Term -> Term
suc Term -> Term -> TCM ()
(==) Term -> Term -> TCM ()
(===) [TCM ()] -> TCM ()
choice -> do
            Term
true  <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrue
            Term
false <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFalse
            let Term
x < :: Term -> Term -> Term
< Term
y = Term
leq Term -> Term -> Term
@@ Term
x Term -> Term -> Term
@@ Term
y
                m :: Term
m     = Int -> Term
var Int
0
                n :: Term
n     = Int -> Term
var Int
1
            (Term
n     Term -> Term -> Term
< Term
zero)  Term -> Term -> TCM ()
=== Term
false
            (Term -> Term
suc Term
n Term -> Term -> Term
< Term -> Term
suc Term
m) Term -> Term -> TCM ()
=== (Term
n Term -> Term -> Term
< Term
m)
            (Term
zero  Term -> Term -> Term
< Term -> Term
suc Term
m) Term -> Term -> TCM ()
=== Term
true

        verifyMax :: p -> m ()
verifyMax p
maxV = forall (m :: * -> *) a. Monad m => a -> m a
return ()  -- TODO: make max a postulate

        verify :: Names
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
verify Names
xs = forall a.
TCMT IO Term
-> TCMT IO Term
-> TCMT IO Term
-> Names
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
verify' forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNat forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primZero forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSuc Names
xs

        verify' ::  TCM Term -> TCM Term -> TCM Term ->
                    [String] -> ( (Term -> Term -> Term) -> Term -> (Term -> Term) ->
                                (Term -> Term -> TCM ()) ->
                                (Term -> Term -> TCM ()) ->
                                ([TCM ()] -> TCM ()) -> TCM a) -> TCM a
        verify' :: forall a.
TCMT IO Term
-> TCMT IO Term
-> TCMT IO Term
-> Names
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
verify' TCMT IO Term
pNat TCMT IO Term
pZero TCMT IO Term
pSuc Names
xs (Term -> Term -> Term)
-> Term
-> (Term -> Term)
-> (Term -> Term -> TCM ())
-> (Term -> Term -> TCM ())
-> ([TCM ()] -> TCM ())
-> TCM a
f = do
            Type
nat  <- forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort
mkType Integer
0) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Term
pNat
            Term
zero <- TCMT IO Term
pZero
            Term
s    <- TCMT IO Term
pSuc
            let Term
x == :: Term -> Term -> TCM ()
== Term
y  = forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
nat Term
x Term
y
                -- 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_ Names
xs
            forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([Name]
xs, forall a. Arg a -> Dom a
domFromArg forall a b. (a -> b) -> a -> b
$ forall a. a -> Arg a
defaultArg Type
nat) forall a b. (a -> b) -> a -> b
$ (Term -> Term -> Term)
-> Term
-> (Term -> Term)
-> (Term -> Term -> TCM ())
-> (Term -> Term -> TCM ())
-> ([TCM ()] -> TCM ())
-> TCM a
f forall t. Apply t => t -> Term -> t
apply1 Term
zero Term -> Term
suc Term -> Term -> TCM ()
(==) forall {m :: * -> *}.
(MonadWarning m, MonadMetaSolver m, MonadStatistics m,
 MonadFresh ProblemId m, MonadFresh Int m) =>
Term -> Term -> m ()
(===) forall {a}. [TCMT IO a] -> TCMT IO a
choice

        verifyPath :: Term -> Type -> TCM ()
        verifyPath :: Term -> Type -> TCM ()
verifyPath Term
path Type
t = do
          let hlam :: [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
hlam [Char]
n NamesT m Term -> NamesT m Term
t = forall (m :: * -> *).
MonadFail m =>
ArgInfo
-> [Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam (forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden ArgInfo
defaultArgInfo) [Char]
n NamesT m Term -> NamesT m Term
t
          forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
t Term
path forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. Names -> NamesT m a -> m a
runNamesT [] (
            forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
hlam [Char]
"l" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
l -> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
hlam [Char]
"A" forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA -> forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPathP forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<#> NamesT (TCMT IO) Term
l forall (m :: * -> *). Applicative m => m Term -> m Term -> m Term
<@> forall (m :: * -> *).
MonadFail m =>
[Char] -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam [Char]
"i" (\ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Term
bA))

-- | 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 :: BuiltinId -> Int -> Term -> TCM (QName, Definition)
inductiveCheck :: BuiltinId -> Int -> Term -> TCM (QName, Definition)
inductiveCheck BuiltinId
b Int
n Term
t = do
  forall (m :: * -> *) a b.
Monad m =>
m (Maybe a) -> m b -> (a -> m b) -> m b
caseMaybeM (Term -> TCM (Maybe QName)
headSymbol Term
t) TCM (QName, Definition)
no forall a b. (a -> b) -> a -> b
$ \QName
q -> do
      Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
      let yes :: TCM (QName, Definition)
yes = forall (m :: * -> *) a. Monad m => a -> m a
return (QName
q, Definition
def)
      case Definition -> Defn
theDef Definition
def of
        Datatype { dataCons :: Defn -> [QName]
dataCons = [QName]
cs }
          | forall (t :: * -> *) a. Foldable t => t a -> Int
length [QName]
cs forall a. Eq a => a -> a -> Bool
== Int
n -> TCM (QName, Definition)
yes
          | Bool
otherwise      -> TCM (QName, Definition)
no
        Record { recInduction :: Defn -> Maybe Induction
recInduction = Maybe Induction
ind } | Int
n forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& Maybe Induction
ind forall a. Eq a => a -> a -> Bool
/= forall a. a -> Maybe a
Just Induction
CoInductive -> TCM (QName, Definition)
yes
        Defn
_ -> TCM (QName, Definition)
no
  where
  headSymbol :: Term -> TCM (Maybe QName)
  headSymbol :: Term -> TCM (Maybe QName)
headSymbol Term
t = forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce Term
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Def QName
q Elims
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just QName
q
    Lam ArgInfo
_ Abs Term
b -> Term -> TCM (Maybe QName)
headSymbol forall a b. (a -> b) -> a -> b
$ forall a. Subst a => Abs a -> SubstArg a -> a
lazyAbsApp Abs Term
b HasCallStack => Term
__DUMMY_TERM__
    Term
_       -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

  no :: TCM (QName, Definition)
no
    | Int
n forall a. Eq a => a -> a -> Bool
== Int
1 = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ Names -> [Char]
unwords
        [ [Char]
"The builtin", forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
b
        , [Char]
"must be a datatype with a single constructor"
        , [Char]
"or an (inductive) record type"
        ]
    | Bool
otherwise = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ Names -> [Char]
unwords
        [ [Char]
"The builtin", forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
b
        , [Char]
"must be a datatype with", forall a. Show a => a -> [Char]
show Int
n
        , [Char]
"constructors"
        ]

-- | @bindPostulatedName 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 ::
  BuiltinId -> ResolvedName -> (QName -> Definition -> TCM Term) -> TCM ()
bindPostulatedName :: BuiltinId
-> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
bindPostulatedName BuiltinId
builtin ResolvedName
x QName -> Definition -> TCMT IO Term
m = do
  QName
q   <- ResolvedName -> TCMT IO QName
getName ResolvedName
x
  Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  case Definition -> Defn
theDef Definition
def of
    Axiom {} -> BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
builtin forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> Definition -> TCMT IO Term
m QName
q Definition
def
    Defn
_        -> forall (m :: * -> *) a. MonadTCError m => m a
err
  where
  err :: forall m a. MonadTCError m => m a
  err :: forall (m :: * -> *) a. MonadTCError m => m a
err = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$
          [Char]
"The argument to BUILTIN " forall a. [a] -> [a] -> [a]
++ forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
builtin forall a. [a] -> [a] -> [a]
++
          [Char]
" must be a postulated name"
  getName :: ResolvedName -> TCMT IO QName
getName = \case
    DefinedName Access
_ AbstractName
d Suffix
NoSuffix -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ AbstractName -> QName
anameName AbstractName
d
    ResolvedName
_ -> forall (m :: * -> *) a. MonadTCError m => m a
err

addHaskellPragma :: QName -> String -> TCM ()
addHaskellPragma :: QName -> [Char] -> TCM ()
addHaskellPragma = [Char] -> QName -> [Char] -> TCM ()
addPragma [Char]
ghcBackendName

bindAndSetHaskellCode :: BuiltinId -> String -> Term -> TCM ()
bindAndSetHaskellCode :: BuiltinId -> [Char] -> Term -> TCM ()
bindAndSetHaskellCode BuiltinId
b [Char]
hs Term
t = do
  QName
d <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCM (Maybe QName)
getDef Term
t
  BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
b Term
t
  QName -> [Char] -> TCM ()
addHaskellPragma QName
d [Char]
hs

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

-- | 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 => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinTrue
  Maybe Term
false <- forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinFalse
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe Term
true forall a. Eq a => a -> a -> Bool
== Maybe Term
false) forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError [Char]
"Cannot bind TRUE and FALSE to the same constructor"

bindBuiltinInt :: Term -> TCM ()
bindBuiltinInt :: Term -> TCM ()
bindBuiltinInt = BuiltinId -> [Char] -> Term -> TCM ()
bindAndSetHaskellCode BuiltinId
builtinInteger [Char]
"= type Integer"

bindBuiltinNat :: Term -> TCM ()
bindBuiltinNat :: Term -> TCM ()
bindBuiltinNat Term
t = do
  BuiltinId -> Term -> TCM ()
bindBuiltinData BuiltinId
builtinNat Term
t
  QName
name <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCM (Maybe QName)
getDef Term
t
  QName -> [Char] -> TCM ()
addHaskellPragma QName
name [Char]
"= type Integer"

-- | Only use for datatypes with distinct arities of constructors.
--   Binds the constructors together with the datatype.
bindBuiltinData :: BuiltinId -> Term -> TCM ()
bindBuiltinData :: BuiltinId -> Term -> TCM ()
bindBuiltinData BuiltinId
s Term
t = do
  BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
s Term
t
  QName
name <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCM (Maybe QName)
getDef Term
t
  Datatype{ dataCons :: Defn -> [QName]
dataCons = [QName]
cs } <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
name
  let getArity :: QName -> m Int
getArity QName
c = do
        Constructor{ conArity :: Defn -> Int
conArity = Int
a } <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
        forall (m :: * -> *) a. Monad m => a -> m a
return Int
a
      getBuiltinArity :: BuiltinDescriptor -> TCMT IO Int
getBuiltinArity (BuiltinDataCons TCM Type
t) = Type -> Int
arity forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Type
t
      getBuiltinArity BuiltinDescriptor
_ = forall a. HasCallStack => a
__IMPOSSIBLE__
      sortByM :: (a -> f b) -> [a] -> f [a]
sortByM a -> f b
f [a]
xs = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> b
snd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. [a] -> [b] -> [(a, b)]
zip [a]
xs forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM a -> f b
f [a]
xs
  -- 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
_ [BuiltinId]
bcs <- BuiltinInfo -> BuiltinDescriptor
builtinDesc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> Maybe BuiltinInfo
findBuiltinInfo BuiltinId
s
        forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM BuiltinId -> Maybe BuiltinInfo
findBuiltinInfo [BuiltinId]
bcs
  [BuiltinInfo]
bcis <- forall {f :: * -> *} {b} {a}.
(Ord b, Monad f) =>
(a -> f b) -> [a] -> f [a]
sortByM (BuiltinDescriptor -> TCMT IO Int
getBuiltinArity forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinInfo -> BuiltinDescriptor
builtinDesc) [BuiltinInfo]
bcis
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall (t :: * -> *) a. Foldable t => t a -> Int
length [QName]
cs forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [BuiltinInfo]
bcis) forall a. HasCallStack => a
__IMPOSSIBLE__  -- 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
      BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
builtinUnit Term
t
      BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
builtinUnitUnit (ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem [])
    Defn
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError [Char]
"Builtin UNIT must be a singleton record type"

bindBuiltinSigma :: Term -> TCM ()
bindBuiltinSigma :: Term -> TCM ()
bindBuiltinSigma Term
t = do
  QName
sigma <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCM (Maybe QName)
getDef Term
t
  Defn
def <- Definition -> Defn
theDef forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
sigma
  case Defn
def of
    Record { recFields :: Defn -> [Dom QName]
recFields = [Dom QName
fst,Dom QName
snd], recConHead :: Defn -> ConHead
recConHead = ConHead
con } -> do
      BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
builtinSigma Term
t
    Defn
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError [Char]
"Builtin SIGMA must be a record type with two fields"

-- | 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) <- BuiltinId -> Int -> Term -> TCM (QName, Definition)
inductiveCheck BuiltinId
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 -> Peano
natSize Tele (Dom Type)
eqTel forall a. Ord a => a -> a -> Bool
>= Peano
3) forall {a}. TCMT IO a
no
  let (Dom ([Char], Type)
a, Dom ([Char], Type)
b) = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [a] -> Maybe (a, a)
last2 forall a b. (a -> b) -> a -> b
$ forall t. Tele (Dom t) -> [Dom ([Char], t)]
telToList Tele (Dom Type)
eqTel
  [Term
a,Term
b] <- forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall t a. Type'' t a -> a
unEl forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t e. Dom' t e -> e
unDom) [Dom ([Char], Type)
a,Dom ([Char], Type)
b]
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. DeBruijn a => a -> Maybe Int
deBruijnView Term
a forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Int
0) forall {a}. TCMT IO a
no
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. DeBruijn a => a -> Maybe Int
deBruijnView Term
b forall a. Eq a => a -> a -> Bool
== forall a. a -> Maybe a
Just Int
1) forall {a}. TCMT IO a
no

  -- Get the single constructor.
  case Definition -> Defn
theDef Definition
def of
    Datatype { dataCons :: Defn -> [QName]
dataCons = [QName
c] } -> do
      BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
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
          BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
builtinRefl (ConHead -> ConInfo -> Elims -> Term
Con (QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
c forall p. DataOrRecord' p
IsData Induction
Inductive []) ConInfo
ConOSystem [])
        Term
_ -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Defn
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError [Char]
"Builtin EQUALITY must be a data type with a single constructor"
  where
  wrongRefl :: TCMT IO a
wrongRefl = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError [Char]
"Wrong type of constructor of BUILTIN EQUALITY"

bindBuiltinInfo :: BuiltinInfo -> A.Expr -> TCM ()
bindBuiltinInfo :: BuiltinInfo -> Expr -> TCM ()
bindBuiltinInfo (BuiltinInfo BuiltinId
s BuiltinDescriptor
d) Expr
e = do
    case BuiltinDescriptor
d of
      BuiltinData TCM Type
t [BuiltinId]
cs -> do
        Term
v <- Expr -> Type -> TCMT IO Term
checkExpr Expr
e forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM Type
t
        forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinUnit) forall a b. (a -> b) -> a -> b
$ do
          forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ BuiltinId -> Int -> Term -> TCM (QName, Definition)
inductiveCheck BuiltinId
s (forall (t :: * -> *) a. Foldable t => t a -> Int
length [BuiltinId]
cs) Term
v
        if | BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinEquality -> forall a. HasCallStack => a
__IMPOSSIBLE__ -- bindBuiltinEquality v
           | BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinBool     -> Term -> TCM ()
bindBuiltinBool     Term
v
           | BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinNat      -> Term -> TCM ()
bindBuiltinNat      Term
v
           | BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinInteger  -> Term -> TCM ()
bindBuiltinInt      Term
v
           | BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinUnit     -> Term -> TCM ()
bindBuiltinUnit     Term
v
           | BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinSigma    -> Term -> TCM ()
bindBuiltinSigma    Term
v
           | BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinList     -> BuiltinId -> Term -> TCM ()
bindBuiltinData BuiltinId
s   Term
v
           | BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinMaybe    -> BuiltinId -> Term -> TCM ()
bindBuiltinData BuiltinId
s   Term
v
           | Bool
otherwise            -> BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
s   Term
v

      BuiltinDataCons TCM Type
t -> do

        let name :: Term -> Term
name (Lam ArgInfo
h Abs Term
b)  = Term -> Term
name (forall a. Subst a => Abs a -> a
absBody Abs Term
b)
            name (Con ConHead
c ConInfo
ci Elims
_) = ConHead -> ConInfo -> Elims -> Term
Con ConHead
c ConInfo
ci []
            name Term
_          = forall a. HasCallStack => a
__IMPOSSIBLE__

        Term
v0 <- Expr -> Type -> TCMT IO Term
checkExpr Expr
e forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TCM Type
t

        case Expr
e of
          A.Con{} -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
          Expr
_       -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ BuiltinId -> Expr -> TypeError
BuiltinMustBeConstructor BuiltinId
s Expr
e

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

        BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
s Term
v

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

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

            PrimImpl Type
t PrimFun
pf <- PrimitiveId -> TCM PrimitiveImpl
lookupPrimitiveFunction PrimitiveId
pfname
            Term
v <- Expr -> Type -> TCMT IO Term
checkExpr Expr
e Type
t

            Term -> TCM ()
axioms Term
v

            Definition
info <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qx
            let cls :: [Clause]
cls = Definition -> [Clause]
defClauses Definition
info
                a :: IsAbstract
a   = Definition -> IsAbstract
defAbstract Definition
info
                o :: IsOpaque
o   = Definition -> IsOpaque
defOpaque Definition
info
                mcc :: Maybe CompiledClauses
mcc = Definition -> Maybe CompiledClauses
defCompiled Definition
info
                inv :: FunctionInverse
inv = Definition -> FunctionInverse
defInverse Definition
info
            -- What happens if defArgOccurrences info does not match
            -- primFunArgOccurrences pf? Let's require the latter to
            -- be the empty list.
            forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (PrimFun -> [Occurrence]
primFunArgOccurrences PrimFun
pf forall a. Eq a => a -> a -> Bool
== []) forall a. HasCallStack => a
__IMPOSSIBLE__
            PrimitiveId -> PrimFun -> TCM ()
bindPrimitive PrimitiveId
pfname forall a b. (a -> b) -> a -> b
$ PrimFun
pf { primFunName :: QName
primFunName = QName
qx }
            QName -> Definition -> TCM ()
addConstant QName
qx forall a b. (a -> b) -> a -> b
$ Definition
info { theDef :: Defn
theDef = Primitive { primAbstr :: IsAbstract
primAbstr    = IsAbstract
a
                                                       , primName :: PrimitiveId
primName     = PrimitiveId
pfname
                                                       , primClauses :: [Clause]
primClauses  = [Clause]
cls
                                                       , primInv :: FunctionInverse
primInv      = FunctionInverse
inv
                                                       , primCompiled :: Maybe CompiledClauses
primCompiled = Maybe CompiledClauses
mcc
                                                       , primOpaque :: IsOpaque
primOpaque   = IsOpaque
o
                                                       } }

            -- needed? yes, for checking equations for mul
            BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
s Term
v

          Expr
_ -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
GenericError forall a b. (a -> b) -> a -> b
$ [Char]
"Builtin " forall a. [a] -> [a] -> [a]
++ forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
s forall a. [a] -> [a] -> [a]
++ [Char]
" must be bound to a function"

      BuiltinSort{} -> forall a. HasCallStack => a
__IMPOSSIBLE__ -- 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]
++ forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
s forall a. [a] -> [a] -> [a]
++ [Char]
" must be a postulated name"
        case Expr
e of
          A.Def QName
q -> do
            Definition
def <- forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
            case Definition -> Defn
theDef Definition
def of
              Axiom {} -> do
                BuiltinId -> QName -> Type -> TCM ()
builtinSizeHook BuiltinId
s QName
q Type
t'
                -- And compilation pragmas for base types
                forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinLevel)  forall a b. (a -> b) -> a -> b
$ QName -> TCM ()
setConstTranspAxiom QName
q forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QName -> [Char] -> TCM ()
addHaskellPragma QName
q [Char]
"= type ()"
                forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinChar)   forall a b. (a -> b) -> a -> b
$ QName -> TCM ()
setConstTranspAxiom QName
q forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QName -> [Char] -> TCM ()
addHaskellPragma QName
q [Char]
"= type Char"
                forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinString) forall a b. (a -> b) -> a -> b
$ QName -> TCM ()
setConstTranspAxiom QName
q forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QName -> [Char] -> TCM ()
addHaskellPragma QName
q [Char]
"= type Data.Text.Text"
                forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinFloat)  forall a b. (a -> b) -> a -> b
$ QName -> TCM ()
setConstTranspAxiom QName
q forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QName -> [Char] -> TCM ()
addHaskellPragma QName
q [Char]
"= type Double"
                forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinWord64) forall a b. (a -> b) -> a -> b
$ QName -> TCM ()
setConstTranspAxiom QName
q forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> QName -> [Char] -> TCM ()
addHaskellPragma QName
q [Char]
"= type MAlonzo.RTE.Word64"
                forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinPathP)  forall a b. (a -> b) -> a -> b
$ QName -> TCM ()
builtinPathPHook QName
q
                BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
s Term
v
              Defn
_        -> TCM ()
err
          Expr
_ -> TCM ()
err

      BuiltinUnknown Maybe (TCM Type)
mt Term -> Type -> TCM ()
f -> do
        (Term
v, Type
t) <- forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (TCM Type)
mt (Expr -> TCM (Term, Type)
inferExpr Expr
e) forall a b. (a -> b) -> a -> b
$ \ TCM Type
tcmt -> do
          Type
t <- TCM Type
tcmt
          (,Type
t) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> Type -> TCMT IO Term
checkExpr Expr
e Type
t
        Term -> Type -> TCM ()
f Term
v Type
t
        if | BuiltinId
s forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinRewrite -> forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (forall (m :: * -> *). MonadReduce m => Term -> MaybeT m QName
getQNameFromTerm Term
v) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
              Maybe QName
Nothing -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError [Char]
"Invalid rewrite relation"
              Just QName
q  -> QName -> TCM ()
bindBuiltinRewriteRelation QName
q
           | Bool
otherwise           -> BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
s Term
v

setConstTranspAxiom :: QName -> TCM ()
setConstTranspAxiom :: QName -> TCM ()
setConstTranspAxiom QName
q =
  forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef (forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ Defn
constTranspAxiom)

builtinPathPHook :: QName -> TCM ()
builtinPathPHook :: QName -> TCM ()
builtinPathPHook QName
q =
      forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q
      forall a b. (a -> b) -> a -> b
$ ([Polarity] -> [Polarity]) -> Definition -> Definition
updateDefPolarity       forall a. a -> a
id
      forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Occurrence] -> [Occurrence]) -> Definition -> Definition
updateDefArgOccurrences (forall a b. a -> b -> a
const [Occurrence
Unused,Occurrence
StrictPos,Occurrence
Mixed,Occurrence
Mixed])

builtinIdHook :: QName -> TCM ()
builtinIdHook :: QName -> TCM ()
builtinIdHook QName
q = do
      forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q
        forall a b. (a -> b) -> a -> b
$ ([Polarity] -> [Polarity]) -> Definition -> Definition
updateDefPolarity       forall a. a -> a
id
        forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Occurrence] -> [Occurrence]) -> Definition -> Definition
updateDefArgOccurrences (forall a b. a -> b -> a
const [Occurrence
Unused,Occurrence
StrictPos,Occurrence
Mixed,Occurrence
Mixed])
      forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q
        forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef (\ def :: Defn
def@Datatype{} -> Defn
def { dataPars :: Int
dataPars = Int
3, dataIxs :: Int
dataIxs = Int
1})

builtinReflIdHook :: QName -> TCM ()
builtinReflIdHook :: QName -> TCM ()
builtinReflIdHook QName
q = do
      forall (m :: * -> *).
MonadTCState m =>
(Signature -> Signature) -> m ()
modifySignature forall a b. (a -> b) -> a -> b
$ QName -> (Definition -> Definition) -> Signature -> Signature
updateDefinition QName
q
        forall a b. (a -> b) -> a -> b
$ (Defn -> Defn) -> Definition -> Definition
updateTheDef (\ def :: Defn
def@Constructor{} -> Defn
def { conPars :: Int
conPars = Int
3, conArity :: Int
conArity = Int
0})

-- | Bind a builtin thing to an expression.
bindBuiltin :: BuiltinId -> ResolvedName -> TCM ()
bindBuiltin :: BuiltinId -> ResolvedName -> TCM ()
bindBuiltin BuiltinId
b ResolvedName
x = do
  forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM ((Int
0 forall a. Eq a => a -> a -> Bool
==) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize) forall a b. (a -> b) -> a -> b
$ do
    -- 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
$ BuiltinId -> TypeError
BuiltinInParameterisedModule BuiltinId
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
$ forall a. Null a => a -> Bool
null forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Tele (Dom Type))
lookupSection forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> ModuleName
qnameModule forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName) forall a b. (a -> b) -> a -> b
$
      forall (m :: * -> *) a. MonadTCError m => m a
failure
  -- 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 | BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinRefl  -> forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall a b. (a -> b) -> a -> b
$ BuiltinId -> BuiltinId -> Warning
OldBuiltin BuiltinId
b BuiltinId
builtinEquality
     | BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinZero  -> forall {m :: * -> *}.
MonadWarning m =>
BuiltinId -> BuiltinId -> m ()
now BuiltinId
builtinNat BuiltinId
b
     | BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinSuc   -> forall {m :: * -> *}.
MonadWarning m =>
BuiltinId -> BuiltinId -> m ()
now BuiltinId
builtinNat BuiltinId
b
     | BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinNil   -> forall {m :: * -> *}.
MonadWarning m =>
BuiltinId -> BuiltinId -> m ()
now BuiltinId
builtinList BuiltinId
b
     | BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinCons  -> forall {m :: * -> *}.
MonadWarning m =>
BuiltinId -> BuiltinId -> m ()
now BuiltinId
builtinList BuiltinId
b
     | BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinInf   -> ResolvedName -> TCM ()
bindBuiltinInf ResolvedName
x
     | BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinSharp -> ResolvedName -> TCM ()
bindBuiltinSharp ResolvedName
x
     | BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinFlat  -> ResolvedName -> TCM ()
bindBuiltinFlat ResolvedName
x
     | BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinEquality -> ResolvedName -> TCM ()
bindBuiltinEquality ResolvedName
x
     | Just BuiltinInfo
i <- BuiltinId -> Maybe BuiltinInfo
findBuiltinInfo BuiltinId
b -> BuiltinInfo -> Expr -> TCM ()
bindBuiltinInfo BuiltinInfo
i (forall a. NameToExpr a => a -> Expr
A.nameToExpr ResolvedName
x)
     | Bool
otherwise -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ [Char] -> TypeError
NoSuchBuiltinName (forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
b)
  where
    now :: BuiltinId -> BuiltinId -> m ()
now BuiltinId
new BuiltinId
b = forall (m :: * -> *).
(HasCallStack, MonadWarning m) =>
Warning -> m ()
warning forall a b. (a -> b) -> a -> b
$ BuiltinId -> BuiltinId -> Warning
OldBuiltin BuiltinId
b BuiltinId
new

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

bindUntypedBuiltin :: BuiltinId -> ResolvedName -> TCM ()
bindUntypedBuiltin :: BuiltinId -> ResolvedName -> TCM ()
bindUntypedBuiltin BuiltinId
b = \case
  DefinedName Access
_ AbstractName
x Suffix
NoSuffix -> AbstractName -> TCM ()
bind AbstractName
x
  DefinedName Access
_ AbstractName
x Suffix{} -> TCM ()
wrong
  FieldName (AbstractName
x :| [])  -> AbstractName -> TCM ()
bind AbstractName
x
  FieldName (AbstractName
x :| [AbstractName]
_)   -> forall {m :: * -> *} {a} {b}.
(MonadError TCErr m, PrettyTCM a, MonadFresh NameId m,
 MonadInteractionPoints m, MonadStConcreteNames m, PureTCM m,
 IsString (m Doc), Null (m Doc), Semigroup (m Doc)) =>
a -> m b
amb AbstractName
x
  VarName Name
_x BindingSource
_bnd      -> TCM ()
wrong
  ResolvedName
UnknownName          -> TCM ()
wrong
  ConstructorName Set Induction
_ NonEmpty AbstractName
xs -> NonEmpty AbstractName -> TCM ()
err NonEmpty AbstractName
xs
  PatternSynResName NonEmpty AbstractName
xs -> NonEmpty AbstractName -> TCM ()
err NonEmpty AbstractName
xs
  where
  bind :: AbstractName -> TCM ()
bind AbstractName
x = BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
b (QName -> Elims -> Term
Def (AbstractName -> QName
anameName AbstractName
x) [])
  wrong :: TCM ()
wrong  = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError forall a b. (a -> b) -> a -> b
$ [Char]
"The argument to BUILTIN " forall a. [a] -> [a] -> [a]
++ forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
b forall a. [a] -> [a] -> [a]
++ [Char]
" must be a defined name"
  amb :: a -> m b
amb a
x  = forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
Doc -> m a
genericDocError forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< do forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
"Name " forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
prettyTCM a
x forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
<+> forall (m :: * -> *). Applicative m => [Char] -> m Doc
text [Char]
" is ambiguous"
  err :: NonEmpty AbstractName -> TCM ()
err (AbstractName
x :| [AbstractName]
xs1)
    | forall a. Null a => a -> Bool
null [AbstractName]
xs1  = TCM ()
wrong
    | Bool
otherwise = forall {m :: * -> *} {a} {b}.
(MonadError TCErr m, PrettyTCM a, MonadFresh NameId m,
 MonadInteractionPoints m, MonadStConcreteNames m, PureTCM m,
 IsString (m Doc), Null (m Doc), Semigroup (m Doc)) =>
a -> m b
amb AbstractName
x

-- | 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 :: BuiltinId -> A.QName -> TCM ()
bindBuiltinNoDef :: BuiltinId -> QName -> TCM ()
bindBuiltinNoDef BuiltinId
b QName
q = forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext forall a b. (a -> b) -> a -> b
$ do
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
b forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [BuiltinId]
sizeBuiltins) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM forall (m :: * -> *). HasOptions m => m Bool
sizedTypesOption forall a b. (a -> b) -> a -> b
$
    forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
[Char] -> m a
genericError forall a b. (a -> b) -> a -> b
$ [Char]
"Cannot declare size BUILTIN " forall a. [a] -> [a] -> [a]
++ forall a. IsBuiltin a => a -> [Char]
getBuiltinId BuiltinId
b forall a. [a] -> [a] -> [a]
++ [Char]
" with option --no-sized-types"
  case BuiltinInfo -> BuiltinDescriptor
builtinDesc forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> Maybe BuiltinInfo
findBuiltinInfo BuiltinId
b of

    Just (BuiltinPostulate Relevance
rel TCM Type
mt) -> do
      -- We start by adding the corresponding postulate
      Type
t   <- TCM Type
mt
      FunctionData
fun <- forall (m :: * -> *). HasOptions m => m FunctionData
emptyFunctionData
      QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
q (forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
rel ArgInfo
defaultArgInfo) QName
q Type
t (FunctionData -> Defn
def FunctionData
fun)
      -- And we then *modify* the definition based on our needs:
      -- We add polarity information for SIZE-related definitions
      BuiltinId -> QName -> Type -> TCM ()
builtinSizeHook BuiltinId
b QName
q Type
t
      -- Finally, bind the BUILTIN in the environment.
      BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
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 :: FunctionData -> Defn
def FunctionData
fun
            | BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinSizeUniv = FunctionData -> Defn
FunctionDefn forall a b. (a -> b) -> a -> b
$ FunctionData
fun
                { _funClauses :: [Clause]
_funClauses    = [ (forall a. Null a => a
empty :: Clause) { clauseBody :: Maybe Term
clauseBody = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ Sort -> Term
Sort Sort
sSizeUniv } ]
                , _funCompiled :: Maybe CompiledClauses
_funCompiled   = forall a. a -> Maybe a
Just (forall a. [Arg [Char]] -> a -> CompiledClauses' a
CC.Done [] forall a b. (a -> b) -> a -> b
$ Sort -> Term
Sort Sort
sSizeUniv)
                , _funMutual :: Maybe [QName]
_funMutual     = forall a. a -> Maybe a
Just []
                , _funTerminates :: Maybe Bool
_funTerminates = forall a. a -> Maybe a
Just Bool
True
                }
            | Bool
otherwise = Defn
defaultAxiom

    Just (BuiltinPrim PrimitiveId
name Term -> TCM ()
axioms) -> do
      PrimImpl Type
t PrimFun
pf <- PrimitiveId -> TCM PrimitiveImpl
lookupPrimitiveFunction PrimitiveId
name
      PrimitiveId -> PrimFun -> TCM ()
bindPrimitive PrimitiveId
name forall a b. (a -> b) -> a -> b
$ PrimFun
pf { primFunName :: QName
primFunName = QName
q }
      let v :: Term
v   = QName -> Elims -> Term
Def QName
q []
          def :: Defn
def = Primitive { primAbstr :: IsAbstract
primAbstr    = IsAbstract
ConcreteDef
                          , primName :: PrimitiveId
primName     = PrimitiveId
name
                          , primClauses :: [Clause]
primClauses  = []
                          , primInv :: FunctionInverse
primInv      = forall c. FunctionInverse' c
NotInjective
                          , primCompiled :: Maybe CompiledClauses
primCompiled = forall a. a -> Maybe a
Just (forall a. [Arg [Char]] -> a -> CompiledClauses' a
CC.Done [] forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
q [])
                          , primOpaque :: IsOpaque
primOpaque   = IsOpaque
TransparentDef
                          }
      Language
lang <- forall (m :: * -> *). HasOptions m => m Language
getLanguage
      QName -> Definition -> TCM ()
addConstant QName
q forall a b. (a -> b) -> a -> b
$
        (ArgInfo -> QName -> Type -> Language -> Defn -> Definition
defaultDefn ArgInfo
defaultArgInfo QName
q Type
t Language
lang Defn
def)
          { defArgOccurrences :: [Occurrence]
defArgOccurrences = PrimFun -> [Occurrence]
primFunArgOccurrences PrimFun
pf }
      Term -> TCM ()
axioms Term
v
      BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
b Term
v

    Just (BuiltinDataCons TCM Type
mt) -> do
      Type
t       <- TCM Type
mt
      QName
d       <- forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! Term -> QName
getPrimName forall a b. (a -> b) -> a -> b
$ forall t a. Type'' t a -> a
unEl Type
t
      Bool
erasure <- PragmaOptions -> Bool
optErasure forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasOptions m => m PragmaOptions
pragmaOptions
      let
        ch :: ConHead
ch = QName -> DataOrRecord -> Induction -> [Arg QName] -> ConHead
ConHead QName
q forall p. DataOrRecord' p
IsData Induction
Inductive []
        def :: Defn
def = Constructor
              { conPars :: Int
conPars   = Int
0   -- Andrea TODO: fix zeros
              , conArity :: Int
conArity  = Int
0
              , conSrcCon :: ConHead
conSrcCon = ConHead
ch
              , conData :: QName
conData   = QName
d
              , conAbstr :: IsAbstract
conAbstr  = IsAbstract
ConcreteDef
              , conComp :: CompKit
conComp   = CompKit
emptyCompKit
              , conProj :: Maybe [QName]
conProj   = forall a. Maybe a
Nothing
              , conForced :: [IsForced]
conForced = []
              , conErased :: Maybe [Bool]
conErased = forall a. Maybe a
Nothing
              , conErasure :: Bool
conErasure = Bool
erasure
              , conInline :: Bool
conInline  = Bool
False
              }
      QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
q ArgInfo
defaultArgInfo QName
q Type
t Defn
def
      QName -> [QName] -> TCM ()
addDataCons QName
d [QName
q]

      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinReflId)     forall a b. (a -> b) -> a -> b
$ QName -> TCM ()
builtinReflIdHook QName
q

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

    Just (BuiltinData TCM Type
mt [BuiltinId]
cs) -> do
      Type
t <- TCM Type
mt
      QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
q ArgInfo
defaultArgInfo QName
q Type
t (forall {a}. LensSort a => a -> Defn
def Type
t)
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BuiltinId
b forall a. Eq a => a -> a -> Bool
== BuiltinId
builtinId)     forall a b. (a -> b) -> a -> b
$ QName -> TCM ()
builtinIdHook QName
q
      BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
b forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
q []
      where
        def :: a -> Defn
def a
t = Datatype
              { dataPars :: Int
dataPars       = Int
0
              , dataIxs :: Int
dataIxs        = Int
0
              , dataClause :: Maybe Clause
dataClause     = forall a. Maybe a
Nothing
              , dataCons :: [QName]
dataCons       = []     -- 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 BuiltinSort
builtinSort) -> do
      let s :: Sort
s = case BuiltinSort
builtinSort of
                SortUniv Univ
u       -> forall t. Univ -> Level' t -> Sort' t
Univ Univ
u forall a b. (a -> b) -> a -> b
$ Integer -> Level
ClosedLevel Integer
0
                SortOmega Univ
u      -> forall t. Univ -> Integer -> Sort' t
Inf Univ
u Integer
0
                BuiltinSort
SortIntervalUniv -> forall t. Sort' t
IntervalUniv
                BuiltinSort
SortLevelUniv    -> forall t. Sort' t
LevelUniv
          def :: Defn
def = BuiltinSort -> Sort -> Defn
PrimitiveSort BuiltinSort
builtinSort Sort
s
      -- Check for the cubical flag if the sort requries it
      case BuiltinSort
builtinSort of
        BuiltinSort
SortIntervalUniv -> Cubical -> [Char] -> TCM ()
requireCubical Cubical
CErased [Char]
""
        BuiltinSort
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
      QName -> ArgInfo -> QName -> Type -> Defn -> TCM ()
addConstant' QName
q ArgInfo
defaultArgInfo QName
q (Sort -> Type
sort forall a b. (a -> b) -> a -> b
$ Sort -> Sort
univSort Sort
s) Defn
def
      BuiltinId -> Term -> TCM ()
bindBuiltinName BuiltinId
b forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
q []

    Just{}  -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Maybe BuiltinDescriptor
Nothing -> forall a. HasCallStack => a
__IMPOSSIBLE__ -- typeError $ NoSuchBuiltinName b


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