{-# LANGUAGE NondecreasingIndentation #-}

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

import Control.Monad
import Data.List (find, sortBy)
import Data.List.NonEmpty (NonEmpty(..))
import qualified Data.List.NonEmpty as NonEmpty
import Data.Function (on)

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

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Monad.Builtin
import Agda.TypeChecking.Monad.SizedTypes ( builtinSizeHook )

import qualified Agda.TypeChecking.CompiledClause as CC
import Agda.TypeChecking.Conversion
import Agda.TypeChecking.Constraints
import Agda.TypeChecking.EtaContract
import Agda.TypeChecking.Functions
import Agda.TypeChecking.Irrelevance
import Agda.TypeChecking.Names
import Agda.TypeChecking.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.Except ( MonadError(catchError) )
import Agda.Utils.Functor
import Agda.Utils.List
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 :: TCM Type -> BuiltinDescriptor
builtinPostulateC :: TCM Type -> BuiltinDescriptor
builtinPostulateC TCM Type
m = Relevance -> TCM Type -> BuiltinDescriptor
BuiltinPostulate Relevance
Relevant (TCM Type -> BuiltinDescriptor) -> TCM Type -> BuiltinDescriptor
forall a b. (a -> b) -> a -> b
$ TCM ()
requireCubical TCM () -> TCM Type -> TCM Type
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> TCM Type
m

findBuiltinInfo :: String -> Maybe BuiltinInfo
findBuiltinInfo :: String -> Maybe BuiltinInfo
findBuiltinInfo String
b = (BuiltinInfo -> Bool) -> [BuiltinInfo] -> Maybe BuiltinInfo
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((String
b String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==) (String -> Bool) -> (BuiltinInfo -> String) -> BuiltinInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinInfo -> String
builtinName) [BuiltinInfo]
coreBuiltins

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

  , (String
builtinId                               String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulateC (String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"a" (TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
                                                              String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"A" (Type -> TCM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
                                                              (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) (Term -> Type) -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0) TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
-->
                                                              (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) (Term -> Type) -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0) TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
-->
                                                              Type -> TCM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Sort -> Type
sort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
1)))
  , (String
builtinConId                            String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulateC (String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"a" (TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
                                                           String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"A" (Type -> TCM Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> TCM Type) -> Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort (Sort -> Type) -> Sort -> Type
forall a b. (a -> b) -> a -> b
$ Int -> Sort
varSort Int
0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
                                                           String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"x" (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
1) (Term -> Type) -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
                                                           String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"y" (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
2) (Term -> Type) -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
1) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
                                                           TCM Type
forall t. TCMT IO (Type'' t Term)
tinterval TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
-->
                                                           (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
3) (Term -> Type) -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPath TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
3 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
2 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
1 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0) TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
-->
                                                           (Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Int -> Sort
varSort Int
3) (Term -> Type) -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primId TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
3 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
2 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
1 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0)))
  , (String
builtinEquiv                            String -> BuiltinDescriptor -> BuiltinInfo
|-> Maybe (TCM Type) -> (Term -> Type -> TCM ()) -> BuiltinDescriptor
BuiltinUnknown (TCM Type -> Maybe (TCM Type)
forall a. a -> Maybe a
Just (TCM Type -> Maybe (TCM Type)) -> TCM Type -> Maybe (TCM Type)
forall a b. (a -> b) -> a -> b
$ TCM ()
requireCubical TCM () -> TCM Type -> TCM Type
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [String] -> NamesT (TCMT IO) Type -> TCM Type
forall (m :: * -> *) a. [String] -> NamesT m a -> m a
runNamesT [] (
                                                                    String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"l" (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
                                                                    String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"l'" (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
b ->
                                                                    String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"A" (Sort -> Type
sort (Sort -> Type) -> (Term -> Sort) -> Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Type) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \NamesT (TCMT IO) Term
bA ->
                                                                    String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"B" (Sort -> Type
sort (Sort -> Type) -> (Term -> Sort) -> Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Type) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
b) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \NamesT (TCMT IO) Term
bB ->
                                                                    ((Sort -> Type
sort (Sort -> Type) -> (Term -> Sort) -> Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort) (Term -> Type) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
b))
                                                                  ))
                                                                   ((Type -> TCM ()) -> Term -> Type -> TCM ()
forall a b. a -> b -> a
const ((Type -> TCM ()) -> Term -> Type -> TCM ())
-> (Type -> TCM ()) -> Term -> Type -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> Type -> TCM ()
forall a b. a -> b -> a
const (TCM () -> Type -> TCM ()) -> TCM () -> Type -> TCM ()
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()))
  , (String
builtinEquivFun                         String -> BuiltinDescriptor -> BuiltinInfo
|-> Maybe (TCM Type) -> (Term -> Type -> TCM ()) -> BuiltinDescriptor
BuiltinUnknown (TCM Type -> Maybe (TCM Type)
forall a. a -> Maybe a
Just (TCM Type -> Maybe (TCM Type)) -> TCM Type -> Maybe (TCM Type)
forall a b. (a -> b) -> a -> b
$ TCM ()
requireCubical TCM () -> TCM Type -> TCM Type
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [String] -> NamesT (TCMT IO) Type -> TCM Type
forall (m :: * -> *) a. [String] -> NamesT m a -> m a
runNamesT [] (
                                                                 String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"l" (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
                                                                 String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"l'" (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
b ->
                                                                 String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"A" (Sort -> Type
sort (Sort -> Type) -> (Term -> Sort) -> Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Type) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
a) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \NamesT (TCMT IO) Term
bA ->
                                                                 String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"B" (Sort -> Type
sort (Sort -> Type) -> (Term -> Sort) -> Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Type) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
b) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \NamesT (TCMT IO) Term
bB ->
                                                                 NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Monad m => m Term -> m Term -> m Type
el' (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
b) (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquiv NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
b NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
bA NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
bB) NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
-->
                                                                 (NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Monad m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
bA NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Monad m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
b NamesT (TCMT IO) Term
bB)
                                                               ))
                                                                ((Type -> TCM ()) -> Term -> Type -> TCM ()
forall a b. a -> b -> a
const ((Type -> TCM ()) -> Term -> Type -> TCM ())
-> (Type -> TCM ()) -> Term -> Type -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> Type -> TCM ()
forall a b. a -> b -> a
const (TCM () -> Type -> TCM ()) -> TCM () -> Type -> TCM ()
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()))
  , (String
builtinEquivProof                       String -> BuiltinDescriptor -> BuiltinInfo
|-> Maybe (TCM Type) -> (Term -> Type -> TCM ()) -> BuiltinDescriptor
BuiltinUnknown (TCM Type -> Maybe (TCM Type)
forall a. a -> Maybe a
Just (TCM Type -> Maybe (TCM Type)) -> TCM Type -> Maybe (TCM Type)
forall a b. (a -> b) -> a -> b
$ TCM ()
requireCubical TCM () -> TCM Type -> TCM Type
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [String] -> NamesT (TCMT IO) Type -> TCM Type
forall (m :: * -> *) a. [String] -> NamesT m a -> m a
runNamesT [] (
                                                               String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"l" (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
la ->
                                                               String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"l'" (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
lb ->
                                                               String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"A" (Sort -> Type
sort (Sort -> Type) -> (Term -> Sort) -> Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Type) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
la) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA ->
                                                               String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"B" (Sort -> Type
sort (Sort -> Type) -> (Term -> Sort) -> Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Type) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
lb) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bB ->
                                                               String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"e" (NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Monad m => m Term -> m Term -> m Type
el' (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
lb)
                                                                             (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquiv NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
lb NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
bA NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
bB)) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
e -> do
                                                               String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"b" (NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Monad m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
lb NamesT (TCMT IO) Term
bB) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
b -> do
                                                                let f :: NamesT (TCMT IO) Term
f = TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquivFun NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
lb NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
bA NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
bB NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
e
                                                                    fiber :: NamesT (TCMT IO) Type
fiber = NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Monad m => m Term -> m Term -> m Type
el' (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
lb)
                                                                                (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSigma NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
lb
                                                                                  NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
bA
                                                                                  NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> (String
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"a" ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
 -> NamesT (TCMT IO) Term)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
                                                                                         TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPath NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
lb NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
bB NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> (NamesT (TCMT IO) Term
f NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
a) NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
b))
                                                                String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"φ" (TCM Type -> NamesT (TCMT IO) Type
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCM Type
forall t. TCMT IO (Type'' t Term)
tinterval) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi ->
                                                                  (String
-> NamesT (TCMT IO) Term
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
String
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' String
"o" NamesT (TCMT IO) Term
phi ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Type
fiber) NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> NamesT (TCMT IO) Type
fiber
                                                             ))
                                                              ((Type -> TCM ()) -> Term -> Type -> TCM ()
forall a b. a -> b -> a
const ((Type -> TCM ()) -> Term -> Type -> TCM ())
-> (Type -> TCM ()) -> Term -> Type -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> Type -> TCM ()
forall a b. a -> b -> a
const (TCM () -> Type -> TCM ()) -> TCM () -> Type -> TCM ()
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()))
  , (String
builtinTranspProof                       String -> BuiltinDescriptor -> BuiltinInfo
|-> Maybe (TCM Type) -> (Term -> Type -> TCM ()) -> BuiltinDescriptor
BuiltinUnknown (TCM Type -> Maybe (TCM Type)
forall a. a -> Maybe a
Just (TCM Type -> Maybe (TCM Type)) -> TCM Type -> Maybe (TCM Type)
forall a b. (a -> b) -> a -> b
$ TCM ()
requireCubical TCM () -> TCM Type -> TCM Type
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [String] -> NamesT (TCMT IO) Type -> TCM Type
forall (m :: * -> *) a. [String] -> NamesT m a -> m a
runNamesT [] (
                                                               String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
hPi' String
"l" (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
la -> do
                                                               String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"e" (TCM Type -> NamesT (TCMT IO) Type
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCM Type
forall t. TCMT IO (Type'' t Term)
tinterval NamesT (TCMT IO) Type
-> NamesT (TCMT IO) Type -> NamesT (TCMT IO) Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> (Sort -> Type
sort (Sort -> Type) -> (Term -> Sort) -> Term -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Sort
tmSort (Term -> Type) -> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NamesT (TCMT IO) Term
la)) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
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 NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
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 NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne
                                                               String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"φ" (TCM Type -> NamesT (TCMT IO) Type
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCM Type
forall t. TCMT IO (Type'' t Term)
tinterval) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
phi -> do
                                                               String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"a" (String
-> NamesT (TCMT IO) Term
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadAddContext m, HasBuiltins m, MonadDebug m) =>
String
-> NamesT m Term
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
pPi' String
"o" NamesT (TCMT IO) Term
phi (\ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Monad m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
bA)) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a -> do
                                                               let f :: NamesT (TCMT IO) Term
f = TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrans NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> (String
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"i" ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
 -> NamesT (TCMT IO) Term)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Term
la) NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
e NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero
                                                                   z :: NamesT (TCMT IO) Term
z = String
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
ilam String
"o" ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
 -> NamesT (TCMT IO) Term)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
o -> NamesT (TCMT IO) Term
f NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> (NamesT (TCMT IO) Term
a NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
o)
                                                               String
-> NamesT (TCMT IO) Type
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall (m :: * -> *).
(MonadFail m, MonadAddContext m, MonadDebug m) =>
String
-> NamesT m Type
-> (NamesT m Term -> NamesT m Type)
-> NamesT m Type
nPi' String
"b" (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
elInf (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSub NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
lb NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
bB NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
phi NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
z)) ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
 -> NamesT (TCMT IO) Type)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type)
-> NamesT (TCMT IO) Type
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
b' -> do
                                                               let b :: NamesT (TCMT IO) Term
b = TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSubOut NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
lb NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
bB NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
phi NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
z NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
b'
                                                                   fiber :: NamesT (TCMT IO) Type
fiber = NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Type
forall (m :: * -> *). Monad m => m Term -> m Term -> m Type
el' NamesT (TCMT IO) Term
la
                                                                               (TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSigma NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
la NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
lb
                                                                                  NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
bA
                                                                                  NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> (String
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"a" ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
 -> NamesT (TCMT IO) Term)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
a ->
                                                                                         TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPath NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
lb NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
bB NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> (NamesT (TCMT IO) Term
f NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
a) NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> NamesT (TCMT IO) Term
b))
                                                               NamesT (TCMT IO) Type
fiber
                                                             ))
                                                              ((Type -> TCM ()) -> Term -> Type -> TCM ()
forall a b. a -> b -> a
const ((Type -> TCM ()) -> Term -> Type -> TCM ())
-> (Type -> TCM ()) -> Term -> Type -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCM () -> Type -> TCM ()
forall a b. a -> b -> a
const (TCM () -> Type -> TCM ()) -> TCM () -> Type -> TCM ()
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()))
  , (String
builtinAgdaSort                         String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [String] -> BuiltinDescriptor
BuiltinData TCM Type
forall (tcm :: * -> *). Monad tcm => tcm Type
tset [String
builtinAgdaSortSet, String
builtinAgdaSortLit, String
builtinAgdaSortUnsupported])
  , (String
builtinAgdaTerm                         String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [String] -> BuiltinDescriptor
BuiltinData TCM Type
forall (tcm :: * -> *). Monad tcm => tcm Type
tset
                                                   [ String
builtinAgdaTermVar, String
builtinAgdaTermLam, String
builtinAgdaTermExtLam
                                                   , String
builtinAgdaTermDef, String
builtinAgdaTermCon
                                                   , String
builtinAgdaTermPi, String
builtinAgdaTermSort
                                                   , String
builtinAgdaTermLit, String
builtinAgdaTermMeta
                                                   , String
builtinAgdaTermUnsupported])
  , String
builtinAgdaErrorPart                     String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [String] -> BuiltinDescriptor
BuiltinData TCM Type
forall (tcm :: * -> *). Monad tcm => tcm Type
tset [ String
builtinAgdaErrorPartString, String
builtinAgdaErrorPartTerm, String
builtinAgdaErrorPartName ]
  , String
builtinAgdaErrorPartString               String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tstring TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
terrorpart)
  , String
builtinAgdaErrorPartTerm                 String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tterm TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
terrorpart)
  , String
builtinAgdaErrorPartName                 String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
terrorpart)
  -- Andreas, 2017-01-12, issue #2386: special handling of builtinEquality
  -- , (builtinEquality                         |-> BuiltinData (hPi "a" (el primLevel) $
  --                                                             hPi "A" (return $ sort $ varSort 0) $
  --                                                             (El (varSort 1) <$> varM 0) -->
  --                                                             (El (varSort 1) <$> varM 0) -->
  --                                                             return (sort $ varSort 1))
  --                                                            [builtinRefl])
  , (String
builtinHiding                           String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [String] -> BuiltinDescriptor
BuiltinData TCM Type
forall (tcm :: * -> *). Monad tcm => tcm Type
tset [String
builtinHidden, String
builtinInstance, String
builtinVisible])
    -- Relevance
  , (String
builtinRelevance                        String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [String] -> BuiltinDescriptor
BuiltinData TCM Type
forall (tcm :: * -> *). Monad tcm => tcm Type
tset [String
builtinRelevant, String
builtinIrrelevant])
  , (String
builtinRelevant                         String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
trelevance)
  , (String
builtinIrrelevant                       String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
trelevance)
    -- Associativity
  , String
builtinAssoc                             String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [String] -> BuiltinDescriptor
BuiltinData TCM Type
forall (tcm :: * -> *). Monad tcm => tcm Type
tset [String
builtinAssocLeft, String
builtinAssocRight, String
builtinAssocNon]
  , String
builtinAssocLeft                         String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tassoc
  , String
builtinAssocRight                        String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tassoc
  , String
builtinAssocNon                          String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tassoc
    -- Precedence
  , String
builtinPrecedence                        String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [String] -> BuiltinDescriptor
BuiltinData TCM Type
forall (tcm :: * -> *). Monad tcm => tcm Type
tset [String
builtinPrecRelated, String
builtinPrecUnrelated]
  , String
builtinPrecRelated                       String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tfloat TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tprec)
  , String
builtinPrecUnrelated                     String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tprec
    -- Fixity
  , String
builtinFixity                            String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [String] -> BuiltinDescriptor
BuiltinData TCM Type
forall (tcm :: * -> *). Monad tcm => tcm Type
tset [String
builtinFixityFixity]
  , String
builtinFixityFixity                      String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tassoc TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tprec TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm 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))
  , (String
builtinRewrite                          String -> BuiltinDescriptor -> BuiltinInfo
|-> Maybe (TCM Type) -> (Term -> Type -> TCM ()) -> BuiltinDescriptor
BuiltinUnknown Maybe (TCM Type)
forall a. Maybe a
Nothing Term -> Type -> TCM ()
verifyBuiltinRewrite)
  , (String
builtinNil                              String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"A" TCM Type
forall (tcm :: * -> *). Monad tcm => tcm Type
tset (TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el (TCMT IO Term -> TCMT IO Term
list TCMT IO Term
v0))))
  , (String
builtinCons                             String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"A" TCM Type
forall (tcm :: * -> *). Monad tcm => tcm Type
tset (TCM Type
tv0 TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el (TCMT IO Term -> TCMT IO Term
list TCMT IO Term
v0) TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el (TCMT IO Term -> TCMT IO Term
list TCMT IO Term
v0))))
  , (String
builtinZero                             String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tnat)
  , (String
builtinSuc                              String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tnat))
  , (String
builtinTrue                             String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tbool)
  , (String
builtinFalse                            String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tbool)
  , (String
builtinArgArg                           String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"A" TCM Type
forall (tcm :: * -> *). Monad tcm => tcm Type
tset (TCM Type
targinfo TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tv0 TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
tv0)))
  , (String
builtinAbsAbs                           String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"A" TCM Type
forall (tcm :: * -> *). Monad tcm => tcm Type
tset (TCM Type
tstring  TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tv0 TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type -> TCM Type
forall (tcm :: * -> *) t.
(HasBuiltins tcm, MonadError TCErr tcm, MonadTCEnv tcm,
 ReadTCState tcm) =>
tcm (Type'' t Term) -> tcm Type
tabs TCM Type
tv0)))
  , (String
builtinArgArgInfo                       String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
thiding TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
trelevance TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
targinfo))
  , (String
builtinAgdaTermVar                      String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
targs TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tterm))
  , (String
builtinAgdaTermLam                      String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
thiding TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type -> TCM Type
forall (tcm :: * -> *) t.
(HasBuiltins tcm, MonadError TCErr tcm, MonadTCEnv tcm,
 ReadTCState tcm) =>
tcm (Type'' t Term) -> tcm Type
tabs TCM Type
tterm TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tterm))
  , (String
builtinAgdaTermExtLam                   String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tclause TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
targs TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tterm))
  , (String
builtinAgdaTermDef                      String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
targs TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tterm))
  , (String
builtinAgdaTermCon                      String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
targs TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tterm))
  , (String
builtinAgdaTermPi                       String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
ttype TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type -> TCM Type
forall (tcm :: * -> *) t.
(HasBuiltins tcm, MonadError TCErr tcm, MonadTCEnv tcm,
 ReadTCState tcm) =>
tcm (Type'' t Term) -> tcm Type
tabs TCM Type
ttype TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tterm))
  , (String
builtinAgdaTermSort                     String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tsort TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tterm))
  , (String
builtinAgdaTermLit                      String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tliteral TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tterm))
  , (String
builtinAgdaTermMeta                     String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tmeta TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
targs TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tterm))
  , (String
builtinAgdaTermUnsupported              String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tterm)
  , (String
builtinAgdaLitNat                       String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tliteral))
  , (String
builtinAgdaLitWord64                    String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tword64 TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tliteral))
  , (String
builtinAgdaLitFloat                     String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tfloat TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tliteral))
  , (String
builtinAgdaLitChar                      String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tchar TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tliteral))
  , (String
builtinAgdaLitString                    String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tstring TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tliteral))
  , (String
builtinAgdaLitQName                     String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tliteral))
  , (String
builtinAgdaLitMeta                      String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tmeta TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tliteral))
  , (String
builtinHidden                           String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
thiding)
  , (String
builtinInstance                         String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
thiding)
  , (String
builtinVisible                          String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
thiding)
  , (String
builtinSizeUniv                         String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate TCM Type
forall (tcm :: * -> *). Monad tcm => tcm Type
tSizeUniv) -- SizeUniv : SizeUniv
-- See comment on tSizeUniv: the following does not work currently.
--  , (builtinSizeUniv                          |-> builtinPostulate tSetOmega) -- SizeUniv : Setω
  , (String
builtinSize                             String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate TCM Type
forall (tcm :: * -> *). Monad tcm => tcm Type
tSizeUniv)
  , (String
builtinSizeLt                           String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tsize TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
..--> TCM Type
forall (tcm :: * -> *). Monad tcm => tcm Type
tSizeUniv))
  , (String
builtinSizeSuc                          String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tsize TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tsize))
  , (String
builtinSizeInf                          String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate TCM Type
tsize)
  -- postulate max : {i : Size} -> Size< i -> Size< i -> Size< i
  , (String
builtinSizeMax                          String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tsize TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tsize TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tsize))
     -- (hPi "i" tsize $ let a = el $ primSizeLt <@> v0 in (a --> a --> a)))
  , (String
builtinAgdaSortSet                      String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tterm TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tsort))
  , (String
builtinAgdaSortLit                      String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tsort))
  , (String
builtinAgdaSortUnsupported              String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tsort)
  , (String
builtinNatPlus                          String -> BuiltinDescriptor -> BuiltinInfo
|-> String -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim String
"primNatPlus" Term -> TCM ()
verifyPlus)
  , (String
builtinNatMinus                         String -> BuiltinDescriptor -> BuiltinInfo
|-> String -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim String
"primNatMinus" Term -> TCM ()
verifyMinus)
  , (String
builtinNatTimes                         String -> BuiltinDescriptor -> BuiltinInfo
|-> String -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim String
"primNatTimes" Term -> TCM ()
verifyTimes)
  , (String
builtinNatDivSucAux                     String -> BuiltinDescriptor -> BuiltinInfo
|-> String -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim String
"primNatDivSucAux" Term -> TCM ()
verifyDivSucAux)
  , (String
builtinNatModSucAux                     String -> BuiltinDescriptor -> BuiltinInfo
|-> String -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim String
"primNatModSucAux" Term -> TCM ()
verifyModSucAux)
  , (String
builtinNatEquals                        String -> BuiltinDescriptor -> BuiltinInfo
|-> String -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim String
"primNatEquality" Term -> TCM ()
verifyEquals)
  , (String
builtinNatLess                          String -> BuiltinDescriptor -> BuiltinInfo
|-> String -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim String
"primNatLess" Term -> TCM ()
verifyLess)
  , (String
builtinLevelZero                        String -> BuiltinDescriptor -> BuiltinInfo
|-> String -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim String
"primLevelZero" (TCM () -> Term -> TCM ()
forall a b. a -> b -> a
const (TCM () -> Term -> TCM ()) -> TCM () -> Term -> TCM ()
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()))
  , (String
builtinLevelSuc                         String -> BuiltinDescriptor -> BuiltinInfo
|-> String -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim String
"primLevelSuc" (TCM () -> Term -> TCM ()
forall a b. a -> b -> a
const (TCM () -> Term -> TCM ()) -> TCM () -> Term -> TCM ()
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()))
  , (String
builtinLevelMax                         String -> BuiltinDescriptor -> BuiltinInfo
|-> String -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim String
"primLevelMax" Term -> TCM ()
forall (m :: * -> *) p. Monad m => p -> m ()
verifyMax)
  , (String
builtinSetOmega                         String -> BuiltinDescriptor -> BuiltinInfo
|-> String -> (Term -> TCM ()) -> BuiltinDescriptor
BuiltinPrim String
"primSetOmega" (TCM () -> Term -> TCM ()
forall a b. a -> b -> a
const (TCM () -> Term -> TCM ()) -> TCM () -> Term -> TCM ()
forall a b. (a -> b) -> a -> b
$ () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()))
  , (String
builtinAgdaClause                       String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [String] -> BuiltinDescriptor
BuiltinData TCM Type
forall (tcm :: * -> *). Monad tcm => tcm Type
tset [String
builtinAgdaClauseClause, String
builtinAgdaClauseAbsurd])
  , (String
builtinAgdaClauseClause                 String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
tlist (TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
tpat) TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tterm TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tclause))
  , (String
builtinAgdaClauseAbsurd                 String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
tlist (TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
tpat) TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tclause))
  , (String
builtinAgdaDefinition                   String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> [String] -> BuiltinDescriptor
BuiltinData TCM Type
forall (tcm :: * -> *). Monad tcm => tcm Type
tset [String
builtinAgdaDefinitionFunDef
                                                                  ,String
builtinAgdaDefinitionDataDef
                                                                  ,String
builtinAgdaDefinitionDataConstructor
                                                                  ,String
builtinAgdaDefinitionRecordDef
                                                                  ,String
builtinAgdaDefinitionPostulate
                                                                  ,String
builtinAgdaDefinitionPrimitive])
  , (String
builtinAgdaDefinitionFunDef             String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tclause TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tdefn))
  , (String
builtinAgdaDefinitionDataDef            String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tnat TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tqname TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tdefn))
  , (String
builtinAgdaDefinitionDataConstructor    String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tdefn))
  , (String
builtinAgdaDefinitionRecordDef          String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons (TCM Type
tqname TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
tlist (TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
tqname) TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tdefn))
  , (String
builtinAgdaDefinitionPostulate          String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tdefn)
  , (String
builtinAgdaDefinitionPrimitive          String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
BuiltinDataCons TCM Type
tdefn)
  , String
builtinAgdaTCM                           String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"a" TCM Type
tlevel (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Int -> TCM Type
forall (m :: * -> *). Monad m => Int -> m Type
tsetL Int
0 TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> Int -> TCM Type
forall (m :: * -> *). Monad m => Int -> m Type
tsetL Int
0)
  , String
builtinAgdaTCMReturn                     String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"a" TCM Type
tlevel  (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
                                                                   String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"A" (Int -> TCM Type
forall (m :: * -> *). Monad m => Int -> m Type
tsetL Int
0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
                                                                   Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a.
Functor f =>
Int -> f a -> f (Type'' Term a)
elV Int
1 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0) TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *).
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0))
  , String
builtinAgdaTCMBind                       String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"a" TCM Type
tlevel  (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"b" TCM Type
tlevel (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
                                                                   String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"A" (Int -> TCM Type
forall (m :: * -> *). Monad m => Int -> m Type
tsetL Int
1) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"B" (Int -> TCM Type
forall (m :: * -> *). Monad m => Int -> m Type
tsetL Int
1) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
                                                                   Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *).
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
3 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
1) TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> (Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a.
Functor f =>
Int -> f a -> f (Type'' Term a)
elV Int
3 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
1) TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *).
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
2 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0)) TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *).
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
2 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0))
  , String
builtinAgdaTCMUnify                      String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tterm TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tterm TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCMT IO Term -> TCM Type
forall (tcm :: * -> *).
(HasBuiltins tcm, MonadError TCErr tcm, MonadTCEnv tcm,
 ReadTCState tcm) =>
tcm Term -> tcm Type
tTCM_ TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
  , String
builtinAgdaTCMTypeError                  String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"a" TCM Type
tlevel (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"A" (Int -> TCM Type
forall (m :: * -> *). Monad m => Int -> m Type
tsetL Int
0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
terrorpart TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *).
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0))
  , String
builtinAgdaTCMInferType                  String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tterm TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCMT IO Term -> TCM Type
forall (tcm :: * -> *).
(HasBuiltins tcm, MonadError TCErr tcm, MonadTCEnv tcm,
 ReadTCState tcm) =>
tcm Term -> tcm Type
tTCM_ TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm)
  , String
builtinAgdaTCMCheckType                  String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tterm TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
ttype TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCMT IO Term -> TCM Type
forall (tcm :: * -> *).
(HasBuiltins tcm, MonadError TCErr tcm, MonadTCEnv tcm,
 ReadTCState tcm) =>
tcm Term -> tcm Type
tTCM_ TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm)
  , String
builtinAgdaTCMNormalise                  String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tterm TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCMT IO Term -> TCM Type
forall (tcm :: * -> *).
(HasBuiltins tcm, MonadError TCErr tcm, MonadTCEnv tcm,
 ReadTCState tcm) =>
tcm Term -> tcm Type
tTCM_ TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm)
  , String
builtinAgdaTCMReduce                     String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tterm TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCMT IO Term -> TCM Type
forall (tcm :: * -> *).
(HasBuiltins tcm, MonadError TCErr tcm, MonadTCEnv tcm,
 ReadTCState tcm) =>
tcm Term -> tcm Type
tTCM_ TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm)
  , String
builtinAgdaTCMCatchError                 String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"a" TCM Type
tlevel (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"A" (Int -> TCM Type
forall (m :: * -> *). Monad m => Int -> m Type
tsetL Int
0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
                                                                   Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *).
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0) TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *).
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0) TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *).
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0))
  , String
builtinAgdaTCMGetContext                 String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCMT IO Term -> TCM Type
forall (tcm :: * -> *).
(HasBuiltins tcm, MonadError TCErr tcm, MonadTCEnv tcm,
 ReadTCState tcm) =>
tcm Term -> tcm Type
tTCM_ (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> TCM Type -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
tlist (TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
ttype)))
  , String
builtinAgdaTCMExtendContext              String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"a" TCM Type
tlevel (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"A" (Int -> TCM Type
forall (m :: * -> *). Monad m => Int -> m Type
tsetL Int
0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
                                                                   TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
ttype TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *).
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0) TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *).
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0))
  , String
builtinAgdaTCMInContext                  String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"a" TCM Type
tlevel (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"A" (Int -> TCM Type
forall (m :: * -> *). Monad m => Int -> m Type
tsetL Int
0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
                                                                   TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
tlist (TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
ttype) TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *).
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0) TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *).
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0))
  , String
builtinAgdaTCMFreshName                  String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tstring TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCMT IO Term -> TCM Type
forall (tcm :: * -> *).
(HasBuiltins tcm, MonadError TCErr tcm, MonadTCEnv tcm,
 ReadTCState tcm) =>
tcm Term -> tcm Type
tTCM_ TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQName)
  , String
builtinAgdaTCMDeclareDef                 String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
tqname TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
ttype TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCMT IO Term -> TCM Type
forall (tcm :: * -> *).
(HasBuiltins tcm, MonadError TCErr tcm, MonadTCEnv tcm,
 ReadTCState tcm) =>
tcm Term -> tcm Type
tTCM_ TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
  , String
builtinAgdaTCMDeclarePostulate           String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
targ TCM Type
tqname TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
ttype TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCMT IO Term -> TCM Type
forall (tcm :: * -> *).
(HasBuiltins tcm, MonadError TCErr tcm, MonadTCEnv tcm,
 ReadTCState tcm) =>
tcm Term -> tcm Type
tTCM_ TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
  , String
builtinAgdaTCMDefineFun                  String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tqname TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
tclause TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCMT IO Term -> TCM Type
forall (tcm :: * -> *).
(HasBuiltins tcm, MonadError TCErr tcm, MonadTCEnv tcm,
 ReadTCState tcm) =>
tcm Term -> tcm Type
tTCM_ TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
  , String
builtinAgdaTCMGetType                    String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tqname TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCMT IO Term -> TCM Type
forall (tcm :: * -> *).
(HasBuiltins tcm, MonadError TCErr tcm, MonadTCEnv tcm,
 ReadTCState tcm) =>
tcm Term -> tcm Type
tTCM_ TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm)
  , String
builtinAgdaTCMGetDefinition              String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tqname TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCMT IO Term -> TCM Type
forall (tcm :: * -> *).
(HasBuiltins tcm, MonadError TCErr tcm, MonadTCEnv tcm,
 ReadTCState tcm) =>
tcm Term -> tcm Type
tTCM_ TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinition)
  , String
builtinAgdaTCMQuoteTerm                  String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"a" TCM Type
tlevel (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"A" (Int -> TCM Type
forall (m :: * -> *). Monad m => Int -> m Type
tsetL Int
0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a.
Functor f =>
Int -> f a -> f (Type'' Term a)
elV Int
1 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0) TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCMT IO Term -> TCM Type
forall (tcm :: * -> *).
(HasBuiltins tcm, MonadError TCErr tcm, MonadTCEnv tcm,
 ReadTCState tcm) =>
tcm Term -> tcm Type
tTCM_ TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm)
  , String
builtinAgdaTCMUnquoteTerm                String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"a" TCM Type
tlevel (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"A" (Int -> TCM Type
forall (m :: * -> *). Monad m => Int -> m Type
tsetL Int
0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ TCM Type
tterm TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *).
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0))
  , String
builtinAgdaTCMBlockOnMeta                String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"a" TCM Type
tlevel (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"A" (Int -> TCM Type
forall (m :: * -> *). Monad m => Int -> m Type
tsetL Int
0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ TCM Type
tmeta TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *).
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0))
  , String
builtinAgdaTCMCommit                     String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCMT IO Term -> TCM Type
forall (tcm :: * -> *).
(HasBuiltins tcm, MonadError TCErr tcm, MonadTCEnv tcm,
 ReadTCState tcm) =>
tcm Term -> tcm Type
tTCM_ TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
  , String
builtinAgdaTCMIsMacro                    String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tqname TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCMT IO Term -> TCM Type
forall (tcm :: * -> *).
(HasBuiltins tcm, MonadError TCErr tcm, MonadTCEnv tcm,
 ReadTCState tcm) =>
tcm Term -> tcm Type
tTCM_ TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primBool)
  , String
builtinAgdaTCMWithNormalisation          String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"a" TCM Type
tlevel (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"A" (Int -> TCM Type
forall (m :: * -> *). Monad m => Int -> m Type
tsetL Int
0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ TCM Type
tbool TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *).
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0) TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *).
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0))
  , String
builtinAgdaTCMDebugPrint                 String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (TCM Type
tstring TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type
tnat TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCM Type -> TCM Type
forall t. TCMT IO (Type'' t Term) -> TCM Type
tlist TCM Type
terrorpart TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> TCMT IO Term -> TCM Type
forall (tcm :: * -> *).
(HasBuiltins tcm, MonadError TCErr tcm, MonadTCEnv tcm,
 ReadTCState tcm) =>
tcm Term -> tcm Type
tTCM_ TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit)
  , String
builtinAgdaTCMNoConstraints              String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"a" TCM Type
tlevel (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"A" (Int -> TCM Type
forall (m :: * -> *). Monad m => Int -> m Type
tsetL Int
0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *).
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0) TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
--> Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *).
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0))
  , String
builtinAgdaTCMRunSpeculative          String -> BuiltinDescriptor -> BuiltinInfo
|-> TCM Type -> BuiltinDescriptor
builtinPostulate (String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"a" TCM Type
tlevel (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$ String -> TCM Type -> TCM Type -> TCM Type
forall (m :: * -> *).
(MonadAddContext m, MonadDebug m) =>
String -> m Type -> m Type -> m Type
hPi String
"A" (Int -> TCM Type
forall (m :: * -> *). Monad m => Int -> m Type
tsetL Int
0) (TCM Type -> TCM Type) -> TCM Type -> TCM Type
forall a b. (a -> b) -> a -> b
$
                                                                Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *).
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSigma TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
1 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0 TCMT IO Term -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@>
                                                                          (ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo (Abs Term -> Term) -> (Term -> Abs Term) -> Term -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Term -> Abs Term
forall a. String -> a -> Abs a
Abs String
"_" (Term -> Term) -> TCMT IO Term -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primBool)) TCM Type -> TCM Type -> TCM Type
forall (tcm :: * -> *).
Monad tcm =>
tcm Type -> tcm Type -> tcm Type
-->
                                                                Int -> TCMT IO Term -> TCM Type
forall (f :: * -> *).
(HasBuiltins f, MonadError TCErr f, MonadTCEnv f, ReadTCState f) =>
Int -> f Term -> f Type
tTCM Int
1 (Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0))
  ]
  where
        |-> :: String -> BuiltinDescriptor -> BuiltinInfo
(|->) = String -> BuiltinDescriptor -> BuiltinInfo
BuiltinInfo

        v0,v1,v2,v3 :: TCM Term
        v0 :: TCMT IO Term
v0 = Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
0
        v1 :: TCMT IO Term
v1 = Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
1
        v2 :: TCMT IO Term
v2 = Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
2
        v3 :: TCMT IO Term
v3 = Int -> TCMT IO Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
3

        tv0,tv1 :: TCM Type
        tv0 :: TCM Type
tv0 = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
v0
        tv1 :: TCM Type
tv1 = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
v1
        tv2 :: TCM Type
tv2 = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
v2
        tv3 :: TCM Type
tv3 = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
v3

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

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

        tsetL :: Int -> m Type
tsetL Int
l    = Type -> m Type
forall (m :: * -> *) a. Monad m => a -> m a
return (Type -> m Type) -> Type -> m Type
forall a b. (a -> b) -> a -> b
$ Sort -> Type
sort (Int -> Sort
varSort Int
l)
        tlevel :: TCM Type
tlevel     = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
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    = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el (TCMT IO Term -> TCM Type) -> TCMT IO Term -> TCM Type
forall a b. (a -> b) -> a -> b
$ TCMT IO Term -> TCMT IO Term
list ((Type'' t Term -> Term) -> TCMT IO (Type'' t Term) -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type'' t Term -> Term
forall t a. Type'' t a -> a
unEl TCMT IO (Type'' t Term)
x)
        targ :: TCMT IO (Type'' t Term) -> TCM Type
targ TCMT IO (Type'' t Term)
x     = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el (TCMT IO Term -> TCMT IO Term
arg ((Type'' t Term -> Term) -> TCMT IO (Type'' t Term) -> TCMT IO Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type'' t Term -> Term
forall t a. Type'' t a -> a
unEl TCMT IO (Type'' t Term)
x))
        tabs :: tcm (Type'' t Term) -> tcm Type
tabs tcm (Type'' t Term)
x     = tcm Term -> tcm Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el (tcm Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAbs tcm Term -> tcm Term -> tcm Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> (Type'' t Term -> Term) -> tcm (Type'' t Term) -> tcm Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type'' t Term -> Term
forall t a. Type'' t a -> a
unEl tcm (Type'' t Term)
x)
        targs :: TCM Type
targs      = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el (TCMT IO Term -> TCMT IO Term
list (TCMT IO Term -> TCMT IO Term
arg TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm))
        tterm :: TCM Type
tterm      = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm
        terrorpart :: TCM Type
terrorpart = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaErrorPart
        tnat :: TCM Type
tnat       = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNat
        tword64 :: TCM Type
tword64    = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primWord64
        tinteger :: TCM Type
tinteger   = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInteger
        tfloat :: TCM Type
tfloat     = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFloat
        tchar :: TCM Type
tchar      = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primChar
        tstring :: TCM Type
tstring    = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primString
        tqname :: TCM Type
tqname     = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQName
        tmeta :: TCM Type
tmeta      = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaMeta
        tsize :: TCM Type
tsize      = Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort
sSizeUniv (Term -> Type) -> TCMT IO Term -> TCM Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSize
        tbool :: TCM Type
tbool      = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primBool
        thiding :: TCM Type
thiding    = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHiding
        trelevance :: TCM Type
trelevance = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRelevance
        tassoc :: TCM Type
tassoc     = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAssoc
        tprec :: TCM Type
tprec      = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPrecedence
        tfixity :: TCM Type
tfixity    = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFixity
--        tcolors    = el (list primAgdaTerm) -- TODO guilhem
        targinfo :: TCM Type
targinfo   = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArgInfo
        ttype :: TCM Type
ttype      = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm
        tsort :: TCM Type
tsort      = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSort
        tdefn :: TCM Type
tdefn      = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinition
        tliteral :: TCM Type
tliteral   = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLiteral
        tpat :: TCM Type
tpat       = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPattern
        tclause :: TCM Type
tclause    = TCMT IO Term -> TCM Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaClause
        tTCM :: Int -> f Term -> f Type
tTCM Int
l f Term
a   = Int -> f Term -> f Type
forall (f :: * -> *) a.
Functor f =>
Int -> f a -> f (Type'' Term a)
elV Int
l (f Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCM f Term -> f Term -> f Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> Int -> f Term
forall (tcm :: * -> *). Monad tcm => Int -> tcm Term
varM Int
l f Term -> f Term -> f Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> f Term
a)
        tTCM_ :: tcm Term -> tcm Type
tTCM_ tcm Term
a    = tcm Term -> tcm Type
forall (tcm :: * -> *). Functor tcm => tcm Term -> tcm Type
el (tcm Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCM tcm Term -> tcm Term -> tcm Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> tcm Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero tcm Term -> tcm Term -> tcm Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> tcm Term
a)
        tinterval :: TCMT IO (Type'' t Term)
tinterval  = Sort' t -> Term -> Type'' t Term
forall t a. Sort' t -> a -> Type'' t a
El Sort' t
forall t. Sort' t
Inf (Term -> Type'' t Term) -> TCMT IO Term -> TCMT IO (Type'' t Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInterval

        verifyPlus :: Term -> TCM ()
verifyPlus Term
plus =
            [String]
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM ())
-> TCM ()
forall a.
[String]
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
verify [String
"n",String
"m"] (((Term -> Term -> Term)
  -> Term
  -> (Term -> Term)
  -> (Term -> Term -> TCM ())
  -> (Term -> Term -> TCM ())
  -> ([TCM ()] -> TCM ())
  -> TCM ())
 -> TCM ())
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM ())
-> TCM ()
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 =
            [String]
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM ())
-> TCM ()
forall a.
[String]
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
verify [String
"n",String
"m"] (((Term -> Term -> Term)
  -> Term
  -> (Term -> Term)
  -> (Term -> Term -> TCM ())
  -> (Term -> Term -> TCM ())
  -> ([TCM ()] -> TCM ())
  -> TCM ())
 -> TCM ())
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM ())
-> TCM ()
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 <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNatPlus
            [String]
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM ())
-> TCM ()
forall a.
[String]
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
verify [String
"n",String
"m"] (((Term -> Term -> Term)
  -> Term
  -> (Term -> Term)
  -> (Term -> Term -> TCM ())
  -> (Term -> Term -> TCM ())
  -> ([TCM ()] -> TCM ())
  -> TCM ())
 -> TCM ())
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM ())
-> TCM ()
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 =
            [String]
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM ())
-> TCM ()
forall a.
[String]
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
verify [String
"k",String
"m",String
"n",String
"j"] (((Term -> Term -> Term)
  -> Term
  -> (Term -> Term)
  -> (Term -> Term -> TCM ())
  -> (Term -> Term -> TCM ())
  -> ([TCM ()] -> TCM ())
  -> TCM ())
 -> TCM ())
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM ())
-> TCM ()
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 =
            [String]
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM ())
-> TCM ()
forall a.
[String]
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
verify [String
"k",String
"m",String
"n",String
"j"] (((Term -> Term -> Term)
  -> Term
  -> (Term -> Term)
  -> (Term -> Term -> TCM ())
  -> (Term -> Term -> TCM ())
  -> ([TCM ()] -> TCM ())
  -> TCM ())
 -> TCM ())
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM ())
-> TCM ()
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 =
            [String]
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM ())
-> TCM ()
forall a.
[String]
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
verify [String
"n",String
"m"] (((Term -> Term -> Term)
  -> Term
  -> (Term -> Term)
  -> (Term -> Term -> TCM ())
  -> (Term -> Term -> TCM ())
  -> ([TCM ()] -> TCM ())
  -> TCM ())
 -> TCM ())
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM ())
-> TCM ()
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  <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrue
            Term
false <- TCMT IO Term
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 =
            [String]
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM ())
-> TCM ()
forall a.
[String]
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
verify [String
"n",String
"m"] (((Term -> Term -> Term)
  -> Term
  -> (Term -> Term)
  -> (Term -> Term -> TCM ())
  -> (Term -> Term -> TCM ())
  -> ([TCM ()] -> TCM ())
  -> TCM ())
 -> TCM ())
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM ())
-> TCM ()
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  <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrue
            Term
false <- TCMT IO Term
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 = () -> m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()  -- TODO: make max a postulate

        verify :: [String]
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
verify [String]
xs = TCMT IO Term
-> TCMT IO Term
-> TCMT IO Term
-> [String]
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
forall a.
TCMT IO Term
-> TCMT IO Term
-> TCMT IO Term
-> [String]
-> ((Term -> Term -> Term)
    -> Term
    -> (Term -> Term)
    -> (Term -> Term -> TCM ())
    -> (Term -> Term -> TCM ())
    -> ([TCM ()] -> TCM ())
    -> TCM a)
-> TCM a
verify' TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNat TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primZero TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSuc [String]
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' :: TCMT IO Term
-> TCMT IO Term
-> TCMT IO Term
-> [String]
-> ((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 [String]
xs (Term -> Term -> Term)
-> Term
-> (Term -> Term)
-> (Term -> Term -> TCM ())
-> (Term -> Term -> TCM ())
-> ([TCM ()] -> TCM ())
-> TCM a
f = do
            Type
nat  <- Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort
mkType Integer
0) (Term -> Type) -> TCMT IO Term -> TCM Type
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 -> m ()
== Term
y  = m () -> m ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Term -> Term -> m ()
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 <- Sort -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort
mkType Integer
0) (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primBool
                             m () -> m ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ Type -> Term -> Term -> m ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
bool Term
x Term
y
                suc :: Term -> Term
suc Term
n  = Term
s Term -> Term -> Term
forall t. Apply t => t -> Term -> t
`apply1` Term
n
                choice :: [TCMT IO a] -> TCMT IO a
choice = (TCMT IO a -> TCMT IO a -> TCMT IO a) -> [TCMT IO a] -> TCMT IO a
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (\TCMT IO a
x TCMT IO a
y -> TCMT IO a
x TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
`catchError` \TCErr
_ -> TCMT IO a
y)
            [Name]
xs <- (String -> TCMT IO Name) -> [String] -> TCMT IO [Name]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> TCMT IO Name
forall a (m :: * -> *).
(FreshName a, MonadFresh NameId m) =>
a -> m Name
freshName_ [String]
xs
            ([Name], Dom Type) -> TCM a -> TCM a
forall b (m :: * -> *) a.
(AddContext b, MonadAddContext m) =>
b -> m a -> m a
addContext ([Name]
xs, Arg Type -> Dom Type
forall a. Arg a -> Dom a
domFromArg (Arg Type -> Dom Type) -> Arg Type -> Dom Type
forall a b. (a -> b) -> a -> b
$ Type -> Arg Type
forall a. a -> Arg a
defaultArg Type
nat) (TCM a -> TCM a) -> TCM a -> TCM a
forall a b. (a -> b) -> a -> b
$ (Term -> Term -> Term)
-> Term
-> (Term -> Term)
-> (Term -> Term -> TCM ())
-> (Term -> Term -> TCM ())
-> ([TCM ()] -> TCM ())
-> TCM a
f Term -> Term -> Term
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 ()
(==) Term -> Term -> TCM ()
forall (m :: * -> *).
(MonadWarning m, MonadMetaSolver m, MonadStatistics m,
 MonadFresh ProblemId m, MonadFresh Int m) =>
Term -> Term -> m ()
(===) [TCM ()] -> TCM ()
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 :: String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
hlam String
n NamesT m Term -> NamesT m Term
t = ArgInfo
-> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
forall (m :: * -> *).
MonadFail m =>
ArgInfo
-> String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
glam (Hiding -> ArgInfo -> ArgInfo
forall a. LensHiding a => Hiding -> a -> a
setHiding Hiding
Hidden ArgInfo
defaultArgInfo) String
n NamesT m Term -> NamesT m Term
t
          TCM () -> TCM ()
forall (m :: * -> *) a.
(MonadConstraint m, MonadWarning m, MonadError TCErr m,
 MonadFresh ProblemId m) =>
m a -> m a
noConstraints (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ Type -> Term -> Term -> TCM ()
forall (m :: * -> *).
MonadConversion m =>
Type -> Term -> Term -> m ()
equalTerm Type
t Term
path (Term -> TCM ()) -> TCMT IO Term -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ([String] -> NamesT (TCMT IO) Term -> TCMT IO Term
forall (m :: * -> *) a. [String] -> NamesT m a -> m a
runNamesT [] (NamesT (TCMT IO) Term -> TCMT IO Term)
-> NamesT (TCMT IO) Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$
            String
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
hlam String
"l" ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
 -> NamesT (TCMT IO) Term)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
l -> String
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
hlam String
"A" ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
 -> NamesT (TCMT IO) Term)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
bA -> TCMT IO Term -> NamesT (TCMT IO) Term
forall (m :: * -> *) a. Monad m => m a -> NamesT m a
cl TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPathP NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<#> NamesT (TCMT IO) Term
l NamesT (TCMT IO) Term
-> NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term
forall (tcm :: * -> *).
Monad tcm =>
tcm Term -> tcm Term -> tcm Term
<@> (String
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall (m :: * -> *).
MonadFail m =>
String -> (NamesT m Term -> NamesT m Term) -> NamesT m Term
lam String
"i" ((NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
 -> NamesT (TCMT IO) Term)
-> (NamesT (TCMT IO) Term -> NamesT (TCMT IO) Term)
-> NamesT (TCMT IO) Term
forall a b. (a -> b) -> a -> b
$ \ NamesT (TCMT IO) Term
_ -> NamesT (TCMT IO) Term
bA))

-- | Checks that builtin with name @b : String@ of type @t : Term@
--   is a data type or inductive record with @n : Int@ constructors.
--   Returns the name of the data/record type.
inductiveCheck :: String -> Int -> Term -> TCM (QName, Definition)
inductiveCheck :: String -> Int -> Term -> TCM (QName, Definition)
inductiveCheck String
b Int
n Term
t = do
  Term
t <- Term -> TCMT IO Term
forall (m :: * -> *) a.
(MonadTCEnv m, HasConstInfo m, HasOptions m, TermLike a) =>
a -> m a
etaContract (Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Term -> TCMT IO Term
forall a (m :: * -> *). (Normalise a, MonadReduce m) => a -> m a
normalise Term
t
  case Term
t of
    Def QName
q Elims
_ -> do
      Definition
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
      let yes :: TCM (QName, Definition)
yes = (QName, Definition) -> TCM (QName, Definition)
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 }
          | [QName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [QName]
cs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n -> TCM (QName, Definition)
yes
          | Bool
otherwise      -> TCM (QName, Definition)
forall a. TCMT IO a
no
        Record { recInduction :: Defn -> Maybe Induction
recInduction = Maybe Induction
ind } | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& Maybe Induction
ind Maybe Induction -> Maybe Induction -> Bool
forall a. Eq a => a -> a -> Bool
/= Induction -> Maybe Induction
forall a. a -> Maybe a
Just Induction
CoInductive -> TCM (QName, Definition)
yes
        Defn
_ -> TCM (QName, Definition)
forall a. TCMT IO a
no
    Term
_ -> TCM (QName, Definition)
forall a. TCMT IO a
no
  where
  no :: TCMT IO a
no
    | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords
        [ String
"The builtin", String
b
        , String
"must be a datatype with a single constructor"
        , String
"or an (inductive) record type"
        ]
    | Bool
otherwise = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords
        [ String
"The builtin", String
b
        , String
"must be a datatype with", Int -> String
forall a. Show a => a -> String
show Int
n
        , String
"constructors"
        ]

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

bindPostulatedName ::
  String -> ResolvedName -> (QName -> Definition -> TCM Term) -> TCM ()
bindPostulatedName :: String
-> ResolvedName -> (QName -> Definition -> TCMT IO Term) -> TCM ()
bindPostulatedName String
builtin ResolvedName
x QName -> Definition -> TCMT IO Term
m = do
  QName
q   <- ResolvedName -> TCMT IO QName
getName ResolvedName
x
  Definition
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
  case Definition -> Defn
theDef Definition
def of
    Axiom {} -> String -> Term -> TCM ()
bindBuiltinName String
builtin (Term -> TCM ()) -> TCMT IO Term -> TCM ()
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< QName -> Definition -> TCMT IO Term
m QName
q Definition
def
    Defn
_        -> TCM ()
forall a. TCMT IO a
err
  where
  err :: TCMT IO a
err = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$
          String
"The argument to BUILTIN " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
builtin String -> String -> String
forall a. [a] -> [a] -> [a]
++
          String
" must be a postulated name"
  getName :: ResolvedName -> TCMT IO QName
getName = \case
    DefinedName Access
_ AbstractName
d -> QName -> TCMT IO QName
forall (m :: * -> *) a. Monad m => a -> m a
return (QName -> TCMT IO QName) -> QName -> TCMT IO QName
forall a b. (a -> b) -> a -> b
$ AbstractName -> QName
anameName AbstractName
d
    ResolvedName
_ -> TCMT IO QName
forall a. TCMT IO a
err

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

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

bindBuiltinBool :: Term -> TCM ()
bindBuiltinBool :: Term -> TCM ()
bindBuiltinBool = String -> String -> Term -> TCM ()
bindAndSetHaskellCode String
builtinBool String
"= 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  <- String -> TCMT IO (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinTrue
  Maybe Term
false <- String -> TCMT IO (Maybe Term)
forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinFalse
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Maybe Term
true Maybe Term -> Maybe Term -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Term
false) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    String -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
genericError String
"Cannot bind TRUE and FALSE to the same constructor"

bindBuiltinInt :: Term -> TCM ()
bindBuiltinInt :: Term -> TCM ()
bindBuiltinInt = String -> String -> Term -> TCM ()
bindAndSetHaskellCode String
builtinInteger String
"= type Integer"

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

-- | Only use for datatypes with distinct arities of constructors.
--   Binds the constructors together with the datatype.
bindBuiltinData :: String -> Term -> TCM ()
bindBuiltinData :: String -> Term -> TCM ()
bindBuiltinData String
s Term
t = do
  String -> Term -> TCM ()
bindBuiltinName String
s Term
t
  QName
name <- QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe QName -> QName) -> TCMT IO (Maybe QName) -> TCMT IO QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCMT IO (Maybe QName)
getDef Term
t
  Datatype{ dataCons :: Defn -> [QName]
dataCons = [QName]
cs } <- Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
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 (Definition -> Defn) -> m Definition -> m Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> m Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
        Int -> m Int
forall (m :: * -> *) a. Monad m => a -> m a
return Int
a
      getBuiltinArity :: BuiltinDescriptor -> TCMT IO Int
getBuiltinArity (BuiltinDataCons TCM Type
t) = Type -> Int
arity (Type -> Int) -> TCM Type -> TCMT IO Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCM Type
t
      getBuiltinArity BuiltinDescriptor
_ = TCMT IO Int
forall a. HasCallStack => a
__IMPOSSIBLE__
      sortByM :: (a -> f b) -> [a] -> f [a]
sortByM a -> f b
f [a]
xs = ((a, b) -> a) -> [(a, b)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, b) -> a
forall a b. (a, b) -> a
fst ([(a, b)] -> [a]) -> ([b] -> [(a, b)]) -> [b] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, b) -> (a, b) -> Ordering) -> [(a, b)] -> [(a, b)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (b -> b -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (b -> b -> Ordering)
-> ((a, b) -> b) -> (a, b) -> (a, b) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (a, b) -> b
forall a b. (a, b) -> b
snd) ([(a, b)] -> [(a, b)]) -> ([b] -> [(a, b)]) -> [b] -> [(a, b)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> [b] -> [(a, b)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a]
xs ([b] -> [a]) -> f [b] -> f [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (a -> f b) -> [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 <- (QName -> TCMT IO Int) -> [QName] -> TCMT IO [QName]
forall (f :: * -> *) b a.
(Ord b, Monad f) =>
(a -> f b) -> [a] -> f [a]
sortByM QName -> TCMT IO Int
forall (m :: * -> *). HasConstInfo m => QName -> m Int
getArity [QName]
cs
  -- Do the same for the builtins
  let bcis :: [BuiltinInfo]
bcis = [BuiltinInfo] -> Maybe [BuiltinInfo] -> [BuiltinInfo]
forall a. a -> Maybe a -> a
fromMaybe [BuiltinInfo]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [BuiltinInfo] -> [BuiltinInfo])
-> Maybe [BuiltinInfo] -> [BuiltinInfo]
forall a b. (a -> b) -> a -> b
$ do
        BuiltinData TCM Type
_ [String]
bcs <- BuiltinInfo -> BuiltinDescriptor
builtinDesc (BuiltinInfo -> BuiltinDescriptor)
-> Maybe BuiltinInfo -> Maybe BuiltinDescriptor
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Maybe BuiltinInfo
findBuiltinInfo String
s
        (String -> Maybe BuiltinInfo) -> [String] -> Maybe [BuiltinInfo]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM String -> Maybe BuiltinInfo
findBuiltinInfo [String]
bcs
  [BuiltinInfo]
bcis <- (BuiltinInfo -> TCMT IO Int)
-> [BuiltinInfo] -> TCMT IO [BuiltinInfo]
forall (f :: * -> *) b a.
(Ord b, Monad f) =>
(a -> f b) -> [a] -> f [a]
sortByM (BuiltinDescriptor -> TCMT IO Int
getBuiltinArity (BuiltinDescriptor -> TCMT IO Int)
-> (BuiltinInfo -> BuiltinDescriptor) -> BuiltinInfo -> TCMT IO Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinInfo -> BuiltinDescriptor
builtinDesc) [BuiltinInfo]
bcis
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([QName] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [QName]
cs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [BuiltinInfo] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [BuiltinInfo]
bcis) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__  -- we already checked this
  (QName -> BuiltinInfo -> TCM ())
-> [QName] -> [BuiltinInfo] -> TCM ()
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 (AmbiguousQName -> Expr) -> AmbiguousQName -> Expr
forall a b. (a -> b) -> a -> b
$ QName -> AmbiguousQName
unambiguous (QName -> AmbiguousQName) -> QName -> AmbiguousQName
forall a b. (a -> b) -> a -> b
$ Range -> QName -> QName
forall t. SetRange t => Range -> t -> t
setRange (QName -> Range
forall t. HasRange t => t -> Range
getRange QName
name) QName
c)) [QName]
cs [BuiltinInfo]
bcis

bindBuiltinUnit :: Term -> TCM ()
bindBuiltinUnit :: Term -> TCM ()
bindBuiltinUnit Term
t = do
  QName
unit <- QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe QName -> QName) -> TCMT IO (Maybe QName) -> TCMT IO QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCMT IO (Maybe QName)
getDef Term
t
  Defn
def <- Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
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
      String -> Term -> TCM ()
bindBuiltinName String
builtinUnit Term
t
      String -> Term -> TCM ()
bindBuiltinName String
builtinUnitUnit (ConHead -> ConInfo -> Elims -> Term
Con ConHead
con ConInfo
ConOSystem [])
    Defn
_ -> String -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
genericError String
"Builtin UNIT must be a singleton record type"

bindBuiltinSigma :: Term -> TCM ()
bindBuiltinSigma :: Term -> TCM ()
bindBuiltinSigma Term
t = do
  QName
sigma <- QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe QName -> QName) -> TCMT IO (Maybe QName) -> TCMT IO QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term -> TCMT IO (Maybe QName)
getDef Term
t
  Defn
def <- Definition -> Defn
theDef (Definition -> Defn) -> TCMT IO Definition -> TCMT IO Defn
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> QName -> TCMT IO Definition
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
      String -> Term -> TCM ()
bindBuiltinName String
builtinSigma Term
t
    Defn
_ -> String -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
genericError String
"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 (ResolvedName -> Expr
forall a. NameToExpr a => a -> Expr
A.nameToExpr ResolvedName
x)

  -- Equality needs to be a data type with 1 constructor
  (QName
eq, Definition
def) <- String -> Int -> Term -> TCM (QName, Definition)
inductiveCheck String
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 <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Type -> TCMT IO (TelV Type)) -> Type -> TCMT IO (TelV Type)
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
def
  let no :: TCMT IO a
no = String -> TCMT IO a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
genericError String
"The type of BUILTIN EQUALITY must be a polymorphic relation"

  -- The target is a sort since eq is a data type.
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Maybe Sort -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Sort -> Bool) -> Maybe Sort -> Bool
forall a b. (a -> b) -> a -> b
$ Term -> Maybe Sort
isSort (Term -> Maybe Sort) -> Term -> Maybe Sort
forall a b. (a -> b) -> a -> b
$ Type -> Term
forall t a. Type'' t a -> a
unEl Type
eqCore) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__

  -- The types of the last two arguments must be the third-last argument
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size Tele (Dom Type)
eqTel Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
3) TCM ()
forall a. TCMT IO a
no
  let (Dom (String, Type)
a, Dom (String, Type)
b) = (Dom (String, Type), Dom (String, Type))
-> Maybe (Dom (String, Type), Dom (String, Type))
-> (Dom (String, Type), Dom (String, Type))
forall a. a -> Maybe a -> a
fromMaybe (Dom (String, Type), Dom (String, Type))
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Dom (String, Type), Dom (String, Type))
 -> (Dom (String, Type), Dom (String, Type)))
-> Maybe (Dom (String, Type), Dom (String, Type))
-> (Dom (String, Type), Dom (String, Type))
forall a b. (a -> b) -> a -> b
$ [Dom (String, Type)]
-> Maybe (Dom (String, Type), Dom (String, Type))
forall a. [a] -> Maybe (a, a)
last2 ([Dom (String, Type)]
 -> Maybe (Dom (String, Type), Dom (String, Type)))
-> [Dom (String, Type)]
-> Maybe (Dom (String, Type), Dom (String, Type))
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Tele (Dom Type)
eqTel
  [Term
a,Term
b] <- [Term] -> TCMT IO [Term]
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce ([Term] -> TCMT IO [Term]) -> [Term] -> TCMT IO [Term]
forall a b. (a -> b) -> a -> b
$ (Dom (String, Type) -> Term) -> [Dom (String, Type)] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term)
-> (Dom (String, Type) -> Type) -> Dom (String, Type) -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Type) -> Type
forall a b. (a, b) -> b
snd ((String, Type) -> Type)
-> (Dom (String, Type) -> (String, Type))
-> Dom (String, Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (String, Type) -> (String, Type)
forall t e. Dom' t e -> e
unDom) [Dom (String, Type)
a,Dom (String, Type)
b]
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Term -> Maybe Int
forall a. DeBruijn a => a -> Maybe Int
deBruijnView Term
a Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Maybe Int
forall a. a -> Maybe a
Just Int
0) TCM ()
forall a. TCMT IO a
no
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Term -> Maybe Int
forall a. DeBruijn a => a -> Maybe Int
deBruijnView Term
b Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1) TCM ()
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
      String -> Term -> TCM ()
bindBuiltinName String
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 <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
c
      TelV Tele (Dom Type)
conTel Type
conCore <- Type -> TCMT IO (TelV Type)
forall (m :: * -> *).
(MonadReduce m, MonadAddContext m) =>
Type -> m (TelV Type)
telView (Type -> TCMT IO (TelV Type)) -> Type -> TCMT IO (TelV Type)
forall a b. (a -> b) -> a -> b
$ Definition -> Type
defType Definition
cdef
      [Term]
ts <- [Term] -> TCMT IO [Term]
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce ([Term] -> TCMT IO [Term]) -> [Term] -> TCMT IO [Term]
forall a b. (a -> b) -> a -> b
$ (Dom (String, Type) -> Term) -> [Dom (String, Type)] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term)
-> (Dom (String, Type) -> Type) -> Dom (String, Type) -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, Type) -> Type
forall a b. (a, b) -> b
snd ((String, Type) -> Type)
-> (Dom (String, Type) -> (String, Type))
-> Dom (String, Type)
-> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Dom (String, Type) -> (String, Type)
forall t e. Dom' t e -> e
unDom) ([Dom (String, Type)] -> [Term]) -> [Dom (String, Type)] -> [Term]
forall a b. (a -> b) -> a -> b
$ Int -> [Dom (String, Type)] -> [Dom (String, Type)]
forall a. Int -> [a] -> [a]
drop (Defn -> Int
conPars (Defn -> Int) -> Defn -> Int
forall a b. (a -> b) -> a -> b
$ Definition -> Defn
theDef Definition
cdef) ([Dom (String, Type)] -> [Dom (String, Type)])
-> [Dom (String, Type)] -> [Dom (String, Type)]
forall a b. (a -> b) -> a -> b
$ Tele (Dom Type) -> [Dom (String, Type)]
forall t. Tele (Dom t) -> [Dom (String, t)]
telToList Tele (Dom Type)
conTel
      -- After dropping the parameters, there should be maximally one argument.
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Term] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
ts Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1) TCM ()
forall a. TCMT IO a
wrongRefl
      Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ((Term -> Bool) -> [Term] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Int -> Maybe Int
forall a. a -> Maybe a
Just Int
0 Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
==) (Maybe Int -> Bool) -> (Term -> Maybe Int) -> Term -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term -> Maybe Int
forall a. DeBruijn a => a -> Maybe Int
deBruijnView) [Term]
ts) TCM ()
forall a. TCMT IO a
wrongRefl

      -- Check the target
      case Type -> Term
forall t a. Type'' t a -> a
unEl Type
conCore of
        Def QName
_ Elims
es -> do
          let vs :: [Term]
vs = (Arg Term -> Term) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Term
forall e. Arg e -> e
unArg ([Arg Term] -> [Term]) -> [Arg Term] -> [Term]
forall a b. (a -> b) -> a -> b
$ [Arg Term] -> Maybe [Arg Term] -> [Arg Term]
forall a. a -> Maybe a -> a
fromMaybe [Arg Term]
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe [Arg Term] -> [Arg Term]) -> Maybe [Arg Term] -> [Arg Term]
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe [Arg Term]
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
          (Term
a,Term
b) <- (Term, Term) -> TCMT IO (Term, Term)
forall a (m :: * -> *). (Reduce a, MonadReduce m) => a -> m a
reduce ((Term, Term) -> TCMT IO (Term, Term))
-> (Term, Term) -> TCMT IO (Term, Term)
forall a b. (a -> b) -> a -> b
$ (Term, Term) -> Maybe (Term, Term) -> (Term, Term)
forall a. a -> Maybe a -> a
fromMaybe (Term, Term)
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe (Term, Term) -> (Term, Term))
-> Maybe (Term, Term) -> (Term, Term)
forall a b. (a -> b) -> a -> b
$ [Term] -> Maybe (Term, Term)
forall a. [a] -> Maybe (a, a)
last2 [Term]
vs
          Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Term -> Maybe Int
forall a. DeBruijn a => a -> Maybe Int
deBruijnView Term
a Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Maybe Int
forall a. a -> Maybe a
Just Int
0) TCM ()
forall a. TCMT IO a
wrongRefl
          Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Term -> Maybe Int
forall a. DeBruijn a => a -> Maybe Int
deBruijnView Term
b Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Maybe Int
forall a. a -> Maybe a
Just Int
0) TCM ()
forall a. TCMT IO a
wrongRefl
          String -> Term -> TCM ()
bindBuiltinName String
builtinRefl (ConHead -> ConInfo -> Elims -> Term
Con (QName -> Induction -> [Arg QName] -> ConHead
ConHead QName
c Induction
Inductive []) ConInfo
ConOSystem [])
        Term
_ -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
    Defn
_ -> String -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
genericError String
"Builtin EQUALITY must be a data type with a single constructor"
  where
  wrongRefl :: TCMT IO a
wrongRefl = String -> TCMT IO a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
genericError String
"Wrong type of constructor of BUILTIN EQUALITY"

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

      BuiltinDataCons TCM Type
t -> do

        let name :: Term -> Term
name (Lam ArgInfo
h Abs Term
b)  = Term -> Term
name (Abs Term -> Term
forall t a. Subst t 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
_          = Term
forall a. HasCallStack => a
__IMPOSSIBLE__

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

        case Expr
e of
          A.Con{} -> () -> TCM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          Expr
_       -> TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> Expr -> TypeError
BuiltinMustBeConstructor String
s Expr
e

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

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

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

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

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

            Term -> TCM ()
axioms Term
v

            Definition
info <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
qx
            let cls :: [Clause]
cls = Definition -> [Clause]
defClauses Definition
info
                a :: IsAbstract
a   = Definition -> IsAbstract
defAbstract Definition
info
                mcc :: Maybe CompiledClauses
mcc = Definition -> Maybe CompiledClauses
defCompiled Definition
info
                inv :: FunctionInverse
inv = Definition -> FunctionInverse
defInverse Definition
info
            String -> PrimFun -> TCM ()
bindPrimitive String
pfname (PrimFun -> TCM ()) -> PrimFun -> TCM ()
forall a b. (a -> b) -> a -> b
$ PrimFun
pf { primFunName :: QName
primFunName = QName
qx }
            QName -> Definition -> TCM ()
addConstant QName
qx (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$ Definition
info { theDef :: Defn
theDef = Primitive :: IsAbstract
-> String
-> [Clause]
-> FunctionInverse
-> Maybe CompiledClauses
-> Defn
Primitive { primAbstr :: IsAbstract
primAbstr    = IsAbstract
a
                                                       , primName :: String
primName     = String
pfname
                                                       , primClauses :: [Clause]
primClauses  = [Clause]
cls
                                                       , primInv :: FunctionInverse
primInv      = FunctionInverse
inv
                                                       , primCompiled :: Maybe CompiledClauses
primCompiled = Maybe CompiledClauses
mcc } }

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

          Expr
_ -> TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$ String
"Builtin " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" must be bound to a function"

      BuiltinPostulate Relevance
rel TCM Type
t -> do
        Type
t' <- TCM Type
t
        Term
v <- Relevance -> TCMT IO Term -> TCMT IO Term
forall (tcm :: * -> *) r a.
(MonadTCEnv tcm, LensRelevance r) =>
r -> tcm a -> tcm a
applyRelevanceToContext Relevance
rel (TCMT IO Term -> TCMT IO Term) -> TCMT IO Term -> TCMT IO Term
forall a b. (a -> b) -> a -> b
$ Expr -> Type -> TCMT IO Term
checkExpr Expr
e Type
t'
        let err :: TCMT IO a
err = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ String -> TypeError
GenericError (String -> TypeError) -> String -> TypeError
forall a b. (a -> b) -> a -> b
$
                    String
"The argument to BUILTIN " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" must be a postulated name"
        case Expr
e of
          A.Def QName
q -> do
            Definition
def <- QName -> TCMT IO Definition
forall (m :: * -> *). HasConstInfo m => QName -> m Definition
getConstInfo QName
q
            case Definition -> Defn
theDef Definition
def of
              Axiom {} -> do
                String -> QName -> Type -> TCM ()
builtinSizeHook String
s QName
q Type
t'
                -- And compilation pragmas for base types
                Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
builtinLevel)  (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> String -> TCM ()
addHaskellPragma QName
q String
"= type ()"
                Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
builtinChar)   (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> String -> TCM ()
addHaskellPragma QName
q String
"= type Char"
                Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
builtinString) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> String -> TCM ()
addHaskellPragma QName
q String
"= type Data.Text.Text"
                Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
builtinFloat)  (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> String -> TCM ()
addHaskellPragma QName
q String
"= type Double"
                Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
builtinWord64) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> String -> TCM ()
addHaskellPragma QName
q String
"= type MAlonzo.RTE.Word64"
                Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
builtinPathP)  (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> TCM ()
builtinPathPHook QName
q
                String -> Term -> TCM ()
bindBuiltinName String
s Term
v
              Defn
_        -> TCM ()
forall a. TCMT IO a
err
          Expr
_ -> TCM ()
forall a. TCMT IO a
err

      BuiltinUnknown Maybe (TCM Type)
mt Term -> Type -> TCM ()
f -> do
        (Term
v, Type
t) <- Maybe (TCM Type)
-> TCM (Term, Type)
-> (TCM Type -> TCM (Term, Type))
-> TCM (Term, Type)
forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe (TCM Type)
mt (Expr -> TCM (Term, Type)
inferExpr Expr
e) ((TCM Type -> TCM (Term, Type)) -> TCM (Term, Type))
-> (TCM Type -> TCM (Term, Type)) -> TCM (Term, Type)
forall a b. (a -> b) -> a -> b
$ \ TCM Type
tcmt -> do
          Type
t <- TCM Type
tcmt
          (,Type
t) (Term -> (Term, Type)) -> TCMT IO Term -> TCM (Term, Type)
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
        String -> Term -> TCM ()
bindBuiltinName String
s Term
v

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

-- | Bind a builtin thing to an expression.
bindBuiltin :: String -> ResolvedName -> TCM ()
bindBuiltin :: String -> ResolvedName -> TCM ()
bindBuiltin String
b ResolvedName
x = do
  TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM ((Int
0 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==) (Int -> Bool) -> TCMT IO Int -> TCMT IO Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TCMT IO Int
forall (m :: * -> *). (Applicative m, MonadTCEnv m) => m Int
getContextSize) (TCM () -> TCM ()) -> TCM () -> TCM ()
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 :: TCMT IO a
failure = TypeError -> TCMT IO a
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCMT IO a) -> TypeError -> TCMT IO a
forall a b. (a -> b) -> a -> b
$ String -> TypeError
BuiltinInParameterisedModule String
b
    -- Get the non-empty list of AbstractName for x
    NonEmpty AbstractName
xs <- case ResolvedName
x of
      VarName{}            -> TCMT IO (NonEmpty AbstractName)
forall a. TCMT IO a
failure
      DefinedName Access
_ AbstractName
x      -> NonEmpty AbstractName -> TCMT IO (NonEmpty AbstractName)
forall (m :: * -> *) a. Monad m => a -> m a
return (NonEmpty AbstractName -> TCMT IO (NonEmpty AbstractName))
-> NonEmpty AbstractName -> TCMT IO (NonEmpty AbstractName)
forall a b. (a -> b) -> a -> b
$ AbstractName
x AbstractName -> [AbstractName] -> NonEmpty AbstractName
forall a. a -> [a] -> NonEmpty a
:| []
      FieldName NonEmpty AbstractName
xs         -> NonEmpty AbstractName -> TCMT IO (NonEmpty AbstractName)
forall (m :: * -> *) a. Monad m => a -> m a
return NonEmpty AbstractName
xs
      ConstructorName NonEmpty AbstractName
xs   -> NonEmpty AbstractName -> TCMT IO (NonEmpty AbstractName)
forall (m :: * -> *) a. Monad m => a -> m a
return NonEmpty AbstractName
xs
      PatternSynResName NonEmpty AbstractName
xs -> TCMT IO (NonEmpty AbstractName)
forall a. TCMT IO a
failure
      ResolvedName
UnknownName          -> TCMT IO (NonEmpty AbstractName)
forall a. TCMT IO a
failure
    -- For ambiguous names, we check all of their definitions:
    TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM (NonEmpty AbstractName
-> (AbstractName -> TCMT IO Bool) -> TCMT IO Bool
forall (f :: * -> *) (m :: * -> *) a.
(Functor f, Foldable f, Monad m) =>
f a -> (a -> m Bool) -> m Bool
allM NonEmpty AbstractName
xs ((AbstractName -> TCMT IO Bool) -> TCMT IO Bool)
-> (AbstractName -> TCMT IO Bool) -> TCMT IO Bool
forall a b. (a -> b) -> a -> b
$ ((Int
0 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
==) (Int -> Bool)
-> (Tele (Dom Type) -> Int) -> Tele (Dom Type) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tele (Dom Type) -> Int
forall a. Sized a => a -> Int
size) (Tele (Dom Type) -> Bool)
-> (AbstractName -> TCMT IO (Tele (Dom Type)))
-> AbstractName
-> TCMT IO Bool
forall (m :: * -> *) b c a.
Functor m =>
(b -> c) -> (a -> m b) -> a -> m c
<.> ModuleName -> TCMT IO (Tele (Dom Type))
forall (m :: * -> *).
(Functor m, ReadTCState m) =>
ModuleName -> m (Tele (Dom Type))
lookupSection (ModuleName -> TCMT IO (Tele (Dom Type)))
-> (AbstractName -> ModuleName)
-> AbstractName
-> TCMT IO (Tele (Dom Type))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> ModuleName
qnameModule (QName -> ModuleName)
-> (AbstractName -> QName) -> AbstractName -> ModuleName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AbstractName -> QName
anameName) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
      TCM ()
forall a. TCMT IO a
failure
  -- Since the name was define in a parameter-free context, we can switch to the empty context.
  -- (And we should!)
  TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  if | String
b String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
builtinRefl  -> Warning -> TCM ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (Warning -> TCM ()) -> Warning -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> String -> Warning
OldBuiltin String
b String
builtinEquality
     | String
b String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
builtinZero  -> String -> String -> TCM ()
forall (m :: * -> *). MonadWarning m => String -> String -> m ()
now String
builtinNat String
b
     | String
b String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
builtinSuc   -> String -> String -> TCM ()
forall (m :: * -> *). MonadWarning m => String -> String -> m ()
now String
builtinNat String
b
     | String
b String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
builtinNil   -> String -> String -> TCM ()
forall (m :: * -> *). MonadWarning m => String -> String -> m ()
now String
builtinList String
b
     | String
b String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
builtinCons  -> String -> String -> TCM ()
forall (m :: * -> *). MonadWarning m => String -> String -> m ()
now String
builtinList String
b
     | String
b String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
builtinInf   -> ResolvedName -> TCM ()
bindBuiltinInf ResolvedName
x
     | String
b String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
builtinSharp -> ResolvedName -> TCM ()
bindBuiltinSharp ResolvedName
x
     | String
b String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
builtinFlat  -> ResolvedName -> TCM ()
bindBuiltinFlat ResolvedName
x
     | String
b String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
builtinEquality -> ResolvedName -> TCM ()
bindBuiltinEquality ResolvedName
x
     | Just BuiltinInfo
i <- String -> Maybe BuiltinInfo
findBuiltinInfo String
b -> BuiltinInfo -> Expr -> TCM ()
bindBuiltinInfo BuiltinInfo
i (ResolvedName -> Expr
forall a. NameToExpr a => a -> Expr
A.nameToExpr ResolvedName
x)
     | Bool
otherwise -> TypeError -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> TypeError
NoSuchBuiltinName String
b
  where
    now :: String -> String -> m ()
now String
new String
b = Warning -> m ()
forall (m :: * -> *). MonadWarning m => Warning -> m ()
warning (Warning -> m ()) -> Warning -> m ()
forall a b. (a -> b) -> a -> b
$ String -> String -> Warning
OldBuiltin String
b String
new

isUntypedBuiltin :: String -> Bool
isUntypedBuiltin :: String -> Bool
isUntypedBuiltin String
b = String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
b [String
builtinFromNat, String
builtinFromNeg, String
builtinFromString]

bindUntypedBuiltin :: String -> ResolvedName -> TCM ()
bindUntypedBuiltin :: String -> ResolvedName -> TCM ()
bindUntypedBuiltin String
b = \case
  DefinedName Access
_ AbstractName
x -> String -> Term -> TCM ()
bindBuiltinName String
b (QName -> Elims -> Term
Def (AbstractName -> QName
anameName AbstractName
x) [])
  FieldName (AbstractName
x :| []) -> String -> Term -> TCM ()
bindBuiltinName String
b (QName -> Elims -> Term
Def (AbstractName -> QName
anameName AbstractName
x) [])
  ResolvedName
_ -> String -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
genericError (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ String
"The argument to BUILTIN " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" must be a defined unambiguous name"

-- | Bind a builtin thing to a new name.
--
-- Since their type is closed, it does not matter whether we are in a
-- parameterized module when we declare them.
-- We simply ignore the parameters.
bindBuiltinNoDef :: String -> A.QName -> TCM ()
bindBuiltinNoDef :: String -> QName -> TCM ()
bindBuiltinNoDef String
b QName
q = TCM () -> TCM ()
forall (tcm :: * -> *) a.
(MonadTCEnv tcm, ReadTCState tcm) =>
tcm a -> tcm a
inTopContext (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ do
  Bool -> TCM () -> TCM ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (String
b String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
sizeBuiltins) (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$ TCMT IO Bool -> TCM () -> TCM ()
forall (m :: * -> *). Monad m => m Bool -> m () -> m ()
unlessM TCMT IO Bool
forall (m :: * -> *). HasOptions m => m Bool
sizedTypesOption (TCM () -> TCM ()) -> TCM () -> TCM ()
forall a b. (a -> b) -> a -> b
$
    String -> TCM ()
forall (m :: * -> *) a.
(MonadTCEnv m, ReadTCState m, MonadError TCErr m) =>
String -> m a
genericError (String -> TCM ()) -> String -> TCM ()
forall a b. (a -> b) -> a -> b
$ String
"Cannot declare size BUILTIN " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
b String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" with option --no-sized-types"
  case BuiltinInfo -> BuiltinDescriptor
builtinDesc (BuiltinInfo -> BuiltinDescriptor)
-> Maybe BuiltinInfo -> Maybe BuiltinDescriptor
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> Maybe BuiltinInfo
findBuiltinInfo String
b of

    Just (BuiltinPostulate Relevance
rel TCM Type
mt) -> do
      -- We start by adding the corresponding postulate
      Type
t <- TCM Type
mt
      QName -> Definition -> TCM ()
addConstant QName
q (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgInfo -> QName -> Type -> Defn -> Definition
defaultDefn (Relevance -> ArgInfo -> ArgInfo
forall a. LensRelevance a => Relevance -> a -> a
setRelevance Relevance
rel ArgInfo
defaultArgInfo) QName
q Type
t Defn
def
      -- And we then *modify* the definition based on our needs:
      -- We add polarity information for SIZE-related definitions
      String -> QName -> Type -> TCM ()
builtinSizeHook String
b QName
q Type
t
      -- Finally, bind the BUILTIN in the environment.
      String -> Term -> TCM ()
bindBuiltinName String
b (Term -> TCM ()) -> Term -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
q []
      where
        -- Andreas, 2015-02-14
        -- Special treatment of SizeUniv, should maybe be a primitive.
        def :: Defn
def | String
b String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
builtinSizeUniv = Defn
emptyFunction
                { funClauses :: [Clause]
funClauses = [ (Clause
forall a. Null a => a
empty :: Clause) { clauseBody :: Maybe Term
clauseBody = Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ Sort -> Term
Sort Sort
sSizeUniv } ]
                , funCompiled :: Maybe CompiledClauses
funCompiled = CompiledClauses -> Maybe CompiledClauses
forall a. a -> Maybe a
Just ([Arg String] -> Term -> CompiledClauses
forall a. [Arg String] -> a -> CompiledClauses' a
CC.Done [] (Term -> CompiledClauses) -> Term -> CompiledClauses
forall a b. (a -> b) -> a -> b
$ Sort -> Term
Sort Sort
sSizeUniv)
                , funMutual :: Maybe [QName]
funMutual    = [QName] -> Maybe [QName]
forall a. a -> Maybe a
Just []
                , funTerminates :: Maybe Bool
funTerminates = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
                }
            | Bool
otherwise = Defn
Axiom

    Just (BuiltinPrim String
name Term -> TCM ()
axioms) -> do
      PrimImpl Type
t PrimFun
pf <- String -> TCM PrimitiveImpl
lookupPrimitiveFunction String
name
      String -> PrimFun -> TCM ()
bindPrimitive String
name (PrimFun -> TCM ()) -> PrimFun -> TCM ()
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 :: IsAbstract
-> String
-> [Clause]
-> FunctionInverse
-> Maybe CompiledClauses
-> Defn
Primitive { primAbstr :: IsAbstract
primAbstr    = IsAbstract
ConcreteDef
                          , primName :: String
primName     = String
name
                          , primClauses :: [Clause]
primClauses  = []
                          , primInv :: FunctionInverse
primInv      = FunctionInverse
forall c. FunctionInverse' c
NotInjective
                          , primCompiled :: Maybe CompiledClauses
primCompiled = CompiledClauses -> Maybe CompiledClauses
forall a. a -> Maybe a
Just ([Arg String] -> Term -> CompiledClauses
forall a. [Arg String] -> a -> CompiledClauses' a
CC.Done [] (Term -> CompiledClauses) -> Term -> CompiledClauses
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
q [])
                          }
      QName -> Definition -> TCM ()
addConstant QName
q (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgInfo -> QName -> Type -> Defn -> Definition
defaultDefn ArgInfo
defaultArgInfo QName
q Type
t Defn
def
      Term -> TCM ()
axioms Term
v
      String -> Term -> TCM ()
bindBuiltinName String
b Term
v

    Just (BuiltinDataCons TCM Type
mt) -> do
      Type
t <- TCM Type
mt
      QName
d <- QName -> TCMT IO QName
forall (m :: * -> *) a. Monad m => a -> m a
return (QName -> TCMT IO QName) -> QName -> TCMT IO QName
forall a b. (a -> b) -> a -> b
$! Term -> QName
getPrimName (Term -> QName) -> Term -> QName
forall a b. (a -> b) -> a -> b
$ Type -> Term
forall t a. Type'' t a -> a
unEl Type
t
      let
        ch :: ConHead
ch = QName -> Induction -> [Arg QName] -> ConHead
ConHead QName
q Induction
Inductive []
        def :: Defn
def = Constructor :: Int
-> Int
-> ConHead
-> QName
-> IsAbstract
-> Induction
-> CompKit
-> Maybe [QName]
-> [IsForced]
-> Maybe [Bool]
-> Defn
Constructor
              { conPars :: Int
conPars   = Int
0   -- Andrea TODO: fix zeros
              , conArity :: Int
conArity  = Int
0
              , conSrcCon :: ConHead
conSrcCon = ConHead
ch
              , conData :: QName
conData   = QName
d
              , conAbstr :: IsAbstract
conAbstr  = IsAbstract
ConcreteDef
              , conInd :: Induction
conInd    = Induction
Inductive
              , conComp :: CompKit
conComp   = CompKit
emptyCompKit
              , conProj :: Maybe [QName]
conProj   = Maybe [QName]
forall a. Maybe a
Nothing
              , conForced :: [IsForced]
conForced = []
              , conErased :: Maybe [Bool]
conErased = Maybe [Bool]
forall a. Maybe a
Nothing
              }
      QName -> Definition -> TCM ()
addConstant QName
q (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgInfo -> QName -> Type -> Defn -> Definition
defaultDefn ArgInfo
defaultArgInfo QName
q Type
t Defn
def
      QName -> [QName] -> TCM ()
addDataCons QName
d [QName
q]
      String -> Term -> TCM ()
bindBuiltinName String
b (Term -> TCM ()) -> Term -> TCM ()
forall a b. (a -> b) -> a -> b
$ ConHead -> ConInfo -> Elims -> Term
Con ConHead
ch ConInfo
ConOSystem []

    Just (BuiltinData TCM Type
mt [String]
cs) -> do
      Type
t <- TCM Type
mt
      QName -> Definition -> TCM ()
addConstant QName
q (Definition -> TCM ()) -> Definition -> TCM ()
forall a b. (a -> b) -> a -> b
$ ArgInfo -> QName -> Type -> Defn -> Definition
defaultDefn ArgInfo
defaultArgInfo QName
q Type
t Defn
def
      String -> Term -> TCM ()
bindBuiltinName String
b (Term -> TCM ()) -> Term -> TCM ()
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
q []
      where
        def :: Defn
def = Datatype :: Int
-> Int
-> Maybe Clause
-> [QName]
-> Sort
-> Maybe [QName]
-> IsAbstract
-> [QName]
-> Defn
Datatype
              { dataPars :: Int
dataPars       = Int
0
              , dataIxs :: Int
dataIxs        = Int
0
              , dataClause :: Maybe Clause
dataClause     = Maybe Clause
forall a. Maybe a
Nothing
              , dataCons :: [QName]
dataCons       = []     -- Constructors are added later
              , dataSort :: Sort
dataSort       = Sort
forall t. Sort' t
Inf
              , dataAbstr :: IsAbstract
dataAbstr      = IsAbstract
ConcreteDef
              , dataMutual :: Maybe [QName]
dataMutual     = Maybe [QName]
forall a. Maybe a
Nothing
              , dataPathCons :: [QName]
dataPathCons   = []
              }

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


builtinKindOfName :: String -> Maybe KindOfName
builtinKindOfName :: String -> Maybe KindOfName
builtinKindOfName String
b = BuiltinInfo -> KindOfName
distinguish (BuiltinInfo -> KindOfName)
-> Maybe BuiltinInfo -> Maybe KindOfName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (BuiltinInfo -> Bool) -> [BuiltinInfo] -> Maybe BuiltinInfo
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((String
b String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==) (String -> Bool) -> (BuiltinInfo -> String) -> BuiltinInfo -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BuiltinInfo -> String
builtinName) [BuiltinInfo]
coreBuiltins
  where
  distinguish :: BuiltinInfo -> KindOfName
distinguish BuiltinInfo
d = case BuiltinInfo -> BuiltinDescriptor
builtinDesc BuiltinInfo
d of
    BuiltinDataCons{}  -> KindOfName
ConName
    BuiltinData{}      -> KindOfName
DataName
    BuiltinPrim{}      -> KindOfName
PrimName
    BuiltinPostulate{} -> KindOfName
AxiomName
    BuiltinUnknown{}   -> KindOfName
OtherDefName