module Agda.TypeChecking.Monad.Builtin
  ( module Agda.TypeChecking.Monad.Builtin
  , module Agda.Syntax.Builtin  -- The names are defined here.
  ) where

import qualified Control.Monad.Fail as Fail

import Control.Monad                ( liftM2, void )
import Control.Monad.Except
import Control.Monad.IO.Class       ( MonadIO(..) )
import Control.Monad.Reader
import Control.Monad.State
import Control.Monad.Trans.Identity (IdentityT)
import Control.Monad.Trans.Maybe
import Control.Monad.Writer

import Data.Function ( on )
import qualified Data.Map as Map
import Data.Set (Set)

import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Builtin
import Agda.Syntax.Internal as I
import Agda.Interaction.Options.Base (PragmaOptions(..))
import Agda.TypeChecking.Monad.Base
-- import Agda.TypeChecking.Functions  -- LEADS TO IMPORT CYCLE
import Agda.TypeChecking.Substitute

import Agda.Utils.Functor
import Agda.Utils.ListT
import Agda.Utils.Monad
import Agda.Utils.Maybe
import Agda.Utils.Singleton
import Agda.Utils.Tuple

import Agda.Utils.Impossible

class ( Functor m
      , Applicative m
      , Fail.MonadFail m
      ) => HasBuiltins m where
  getBuiltinThing :: String -> m (Maybe (Builtin PrimFun))

  default getBuiltinThing :: (MonadTrans t, HasBuiltins n, t n ~ m) => String -> m (Maybe (Builtin PrimFun))
  getBuiltinThing = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *).
HasBuiltins m =>
String -> m (Maybe (Builtin PrimFun))
getBuiltinThing

instance HasBuiltins m => HasBuiltins (ExceptT e m)
instance HasBuiltins m => HasBuiltins (IdentityT m)
instance HasBuiltins m => HasBuiltins (ListT m)
instance HasBuiltins m => HasBuiltins (MaybeT m)
instance HasBuiltins m => HasBuiltins (ReaderT e m)
instance HasBuiltins m => HasBuiltins (StateT s m)
instance (HasBuiltins m, Monoid w) => HasBuiltins (WriterT w m)

deriving instance HasBuiltins m => HasBuiltins (BlockT m)

instance MonadIO m => HasBuiltins (TCMT m) where
  getBuiltinThing :: String -> TCMT m (Maybe (Builtin PrimFun))
getBuiltinThing String
b =
    forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionMaybeWith forall a. Builtin a -> Builtin a -> Builtin a
unionBuiltin)
      (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (BuiltinThings PrimFun) TCState
stLocalBuiltins)
      (forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
b forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. ReadTCState m => Lens' a TCState -> m a
useTC Lens' (BuiltinThings PrimFun) TCState
stImportedBuiltins)

-- If Agda is changed so that the type of a literal can belong to an
-- inductive family (with at least one index), then the implementation
-- of split' in Agda.TypeChecking.Coverage should be changed.

litType
  :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
  => Literal -> m Type
litType :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Literal -> m Type
litType = \case
  LitNat Integer
n    -> do
    Term
_ <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primZero
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
n forall a. Ord a => a -> a -> Bool
> Integer
0) forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a. Functor f => f a -> f ()
void forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSuc
    forall {a}. a -> Type'' Term a
el forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNat
  LitWord64 Word64
_ -> forall {a}. a -> Type'' Term a
el forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primWord64
  LitFloat Double
_  -> forall {a}. a -> Type'' Term a
el forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFloat
  LitChar Char
_   -> forall {a}. a -> Type'' Term a
el forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primChar
  LitString Text
_ -> forall {a}. a -> Type'' Term a
el forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primString
  LitQName QName
_  -> forall {a}. a -> Type'' Term a
el forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQName
  LitMeta TopLevelModuleName
_ MetaId
_ -> forall {a}. a -> Type'' Term a
el forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaMeta
  where
    el :: a -> Type'' Term a
el a
t = forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort
mkType Integer
0) a
t

setBuiltinThings :: BuiltinThings PrimFun -> TCM ()
setBuiltinThings :: BuiltinThings PrimFun -> TCM ()
setBuiltinThings BuiltinThings PrimFun
b = Lens' (BuiltinThings PrimFun) TCState
stLocalBuiltins forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> a -> m ()
`setTCLens` BuiltinThings PrimFun
b

bindBuiltinName :: String -> Term -> TCM ()
bindBuiltinName :: String -> Term -> TCM ()
bindBuiltinName String
b Term
x = do
  Maybe (Builtin PrimFun)
builtin <- forall (m :: * -> *).
HasBuiltins m =>
String -> m (Maybe (Builtin PrimFun))
getBuiltinThing String
b
  case Maybe (Builtin PrimFun)
builtin of
    Just (Builtin Term
y) -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> Term -> Term -> TypeError
DuplicateBuiltinBinding String
b Term
y Term
x
    Just (Prim PrimFun
_)    -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
NoSuchBuiltinName String
b
    Just BuiltinRewriteRelations{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Maybe (Builtin PrimFun)
Nothing          -> Lens' (BuiltinThings PrimFun) TCState
stLocalBuiltins forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
b (forall pf. Term -> Builtin pf
Builtin Term
x)

bindPrimitive :: String -> PrimFun -> TCM ()
bindPrimitive :: String -> PrimFun -> TCM ()
bindPrimitive String
b PrimFun
pf = do
  Maybe (Builtin PrimFun)
builtin <- forall (m :: * -> *).
HasBuiltins m =>
String -> m (Maybe (Builtin PrimFun))
getBuiltinThing String
b
  case Maybe (Builtin PrimFun)
builtin of
    Just (Builtin Term
_) -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
NoSuchPrimitiveFunction String
b
    Just (Prim PrimFun
x)    -> forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ (String -> QName -> QName -> TypeError
DuplicatePrimitiveBinding String
b forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` PrimFun -> QName
primFunName) PrimFun
x PrimFun
pf
    Just BuiltinRewriteRelations{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Maybe (Builtin PrimFun)
Nothing          -> Lens' (BuiltinThings PrimFun) TCState
stLocalBuiltins forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens` forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
b (forall pf. pf -> Builtin pf
Prim PrimFun
pf)

-- | Add one (more) relation symbol to the rewrite relations.
bindBuiltinRewriteRelation :: QName -> TCM ()
bindBuiltinRewriteRelation :: QName -> TCM ()
bindBuiltinRewriteRelation QName
x =
  Lens' (BuiltinThings PrimFun) TCState
stLocalBuiltins forall (m :: * -> *) a.
MonadTCState m =>
Lens' a TCState -> (a -> a) -> m ()
`modifyTCLens`
    forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith forall a. Builtin a -> Builtin a -> Builtin a
unionBuiltin String
builtinRewrite (forall pf. Set QName -> Builtin pf
BuiltinRewriteRelations forall a b. (a -> b) -> a -> b
$ forall el coll. Singleton el coll => el -> coll
singleton QName
x)

-- | Get the currently registered rewrite relation symbols.
getBuiltinRewriteRelations :: HasBuiltins m => m (Maybe (Set QName))
getBuiltinRewriteRelations :: forall (m :: * -> *). HasBuiltins m => m (Maybe (Set QName))
getBuiltinRewriteRelations = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall {pf}. Builtin pf -> Set QName
rels forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasBuiltins m =>
String -> m (Maybe (Builtin PrimFun))
getBuiltinThing String
builtinRewrite
  where
  rels :: Builtin pf -> Set QName
rels = \case
    BuiltinRewriteRelations Set QName
xs -> Set QName
xs
    Prim{}    -> forall a. HasCallStack => a
__IMPOSSIBLE__
    Builtin{} -> forall a. HasCallStack => a
__IMPOSSIBLE__

getBuiltin :: (HasBuiltins m, MonadTCError m)
           => String -> m Term
getBuiltin :: forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
x =
  forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
NoBindingForBuiltin String
x) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
x

getBuiltin' :: HasBuiltins m => String -> m (Maybe Term)
getBuiltin' :: forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
x = do
    Maybe (Builtin PrimFun)
builtin <- forall (m :: * -> *).
HasBuiltins m =>
String -> m (Maybe (Builtin PrimFun))
getBuiltinThing String
x
    case Maybe (Builtin PrimFun)
builtin of
        Just BuiltinRewriteRelations{} -> forall a. HasCallStack => a
__IMPOSSIBLE__
        Just (Builtin Term
t) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. KillRange a => KillRangeT a
killRange Term
t
        Maybe (Builtin PrimFun)
_                -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing

getPrimitive' :: HasBuiltins m => String -> m (Maybe PrimFun)
getPrimitive' :: forall (m :: * -> *). HasBuiltins m => String -> m (Maybe PrimFun)
getPrimitive' String
x = (forall {a}. Builtin a -> Maybe a
getPrim forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
HasBuiltins m =>
String -> m (Maybe (Builtin PrimFun))
getBuiltinThing String
x
  where
    getPrim :: Builtin a -> Maybe a
getPrim (Prim a
pf) = forall (m :: * -> *) a. Monad m => a -> m a
return a
pf
    getPrim BuiltinRewriteRelations{} = forall a. HasCallStack => a
__IMPOSSIBLE__
    getPrim Builtin a
_         = forall a. Maybe a
Nothing

getPrimitive :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
             => String -> m PrimFun
getPrimitive :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m PrimFun
getPrimitive String
x =
  forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError forall a b. (a -> b) -> a -> b
$ String -> TypeError
NoSuchPrimitiveFunction String
x) forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). HasBuiltins m => String -> m (Maybe PrimFun)
getPrimitive' String
x

getPrimitiveTerm :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
                 => String -> m Term
getPrimitiveTerm :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m Term
getPrimitiveTerm String
x = (QName -> Elims -> Term
`Def` []) forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimFun -> QName
primFunName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m PrimFun
getPrimitive String
x

getPrimitiveTerm' :: HasBuiltins m => String -> m (Maybe Term)
getPrimitiveTerm' :: forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getPrimitiveTerm' String
x = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (QName -> Elims -> Term
`Def` []) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' String
x

getTerm' :: HasBuiltins m => String -> m (Maybe Term)
getTerm' :: forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getTerm' String
x = forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getPrimitiveTerm' String
x

getName' :: HasBuiltins m => String -> m (Maybe QName)
getName' :: forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getName' String
x = forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
mplus forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getBuiltinName' String
x forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' String
x

-- | @getTerm use name@ looks up @name@ as a primitive or builtin, and
-- throws an error otherwise.
-- The @use@ argument describes how the name is used for the sake of
-- the error message.
getTerm :: (HasBuiltins m) => String -> String -> m Term
getTerm :: forall (m :: * -> *). HasBuiltins m => String -> String -> m Term
getTerm String
use String
name = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getTerm' String
name) forall a b. (a -> b) -> a -> b
$
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall a. Impossible -> a
throwImpossible ([String] -> String -> Impossible
ImpMissingDefinitions [String
name] String
use)


-- | Rewrite a literal to constructor form if possible.
constructorForm :: HasBuiltins m => Term -> m Term
constructorForm :: forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
v = do
  let pZero :: m Term
pZero = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinZero
      pSuc :: m Term
pSuc  = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinSuc
  forall (m :: * -> *).
Applicative m =>
m Term -> m Term -> Term -> m Term
constructorForm' m Term
pZero m Term
pSuc Term
v

constructorForm' :: Applicative m => m Term -> m Term -> Term -> m Term
constructorForm' :: forall (m :: * -> *).
Applicative m =>
m Term -> m Term -> Term -> m Term
constructorForm' m Term
pZero m Term
pSuc Term
v =
  case Term
v of
    Lit (LitNat Integer
n)
      | Integer
n forall a. Eq a => a -> a -> Bool
== Integer
0    -> m Term
pZero
      | Integer
n forall a. Ord a => a -> a -> Bool
> Integer
0     -> (forall t. Apply t => t -> Term -> t
`apply1` Literal -> Term
Lit (Integer -> Literal
LitNat forall a b. (a -> b) -> a -> b
$ Integer
n forall a. Num a => a -> a -> a
- Integer
1)) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Term
pSuc
      | Bool
otherwise -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
v
    Term
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
v

---------------------------------------------------------------------------
-- * The names of built-in things
---------------------------------------------------------------------------

primInteger, primIntegerPos, primIntegerNegSuc,
    primFloat, primChar, primString, primUnit, primUnitUnit, primBool, primTrue, primFalse,
    primSigma,
    primList, primNil, primCons, primIO, primNat, primSuc, primZero, primMaybe, primNothing, primJust,
    primPath, primPathP, primIntervalUniv, primInterval, primIZero, primIOne, primPartial, primPartialP,
    primIMin, primIMax, primINeg,
    primIsOne, primItIsOne, primIsOne1, primIsOne2, primIsOneEmpty,
    primSub, primSubIn, primSubOut,
    primTrans, primHComp,
    primId, primConId, primIdElim,
    primEquiv, primEquivFun, primEquivProof,
    primTranspProof,
    primGlue, prim_glue, prim_unglue,
    prim_glueU, prim_unglueU,
    primFaceForall,
    primNatPlus, primNatMinus, primNatTimes, primNatDivSucAux, primNatModSucAux,
    primNatEquality, primNatLess,
    -- Machine words
    primWord64,
    primSizeUniv, primSize, primSizeLt, primSizeSuc, primSizeInf, primSizeMax,
    primInf, primSharp, primFlat,
    primEquality, primRefl,
    primLevel, primLevelZero, primLevelSuc, primLevelMax,
    primLockUniv,
    primSet, primProp, primSetOmega, primStrictSet, primSSetOmega,
    primFromNat, primFromNeg, primFromString,
    -- builtins for reflection:
    primQName, primArgInfo, primArgArgInfo, primArg, primArgArg, primAbs, primAbsAbs, primAgdaTerm, primAgdaTermVar,
    primAgdaTermLam, primAgdaTermExtLam, primAgdaTermDef, primAgdaTermCon, primAgdaTermPi,
    primAgdaTermSort, primAgdaTermLit, primAgdaTermUnsupported, primAgdaTermMeta,
    primAgdaErrorPart, primAgdaErrorPartString, primAgdaErrorPartTerm, primAgdaErrorPartPatt, primAgdaErrorPartName,
    primHiding, primHidden, primInstance, primVisible,
    primRelevance, primRelevant, primIrrelevant,
    primQuantity, primQuantity0, primQuantityω,
    primModality, primModalityConstructor,
    primAssoc, primAssocLeft, primAssocRight, primAssocNon,
    primPrecedence, primPrecRelated, primPrecUnrelated,
    primFixity, primFixityFixity,
    primAgdaLiteral, primAgdaLitNat, primAgdaLitWord64, primAgdaLitFloat, primAgdaLitString, primAgdaLitChar, primAgdaLitQName, primAgdaLitMeta,
    primAgdaSort, primAgdaSortSet, primAgdaSortLit, primAgdaSortProp, primAgdaSortPropLit, primAgdaSortInf, primAgdaSortUnsupported,
    primAgdaDefinition, primAgdaDefinitionFunDef, primAgdaDefinitionDataDef, primAgdaDefinitionRecordDef,
    primAgdaDefinitionPostulate, primAgdaDefinitionPrimitive, primAgdaDefinitionDataConstructor,
    primAgdaClause, primAgdaClauseClause, primAgdaClauseAbsurd,
    primAgdaPattern, primAgdaPatCon, primAgdaPatVar, primAgdaPatDot,
    primAgdaPatLit, primAgdaPatProj,
    primAgdaPatAbsurd,
    primAgdaMeta,
    primAgdaTCM, primAgdaTCMReturn, primAgdaTCMBind, primAgdaTCMUnify,
    primAgdaTCMTypeError, primAgdaTCMInferType, primAgdaTCMCheckType,
    primAgdaTCMNormalise, primAgdaTCMReduce,
    primAgdaTCMCatchError, primAgdaTCMGetContext, primAgdaTCMExtendContext, primAgdaTCMInContext,
    primAgdaTCMFreshName, primAgdaTCMDeclareDef, primAgdaTCMDeclarePostulate, primAgdaTCMDeclareData, primAgdaTCMDefineData, primAgdaTCMDefineFun,
    primAgdaTCMGetType, primAgdaTCMGetDefinition,
    primAgdaTCMQuoteTerm, primAgdaTCMUnquoteTerm, primAgdaTCMQuoteOmegaTerm,
    primAgdaTCMBlockOnMeta, primAgdaTCMCommit, primAgdaTCMIsMacro,
    primAgdaTCMFormatErrorParts, primAgdaTCMDebugPrint,
    primAgdaTCMWithNormalisation, primAgdaTCMWithReconsParams,
    primAgdaTCMOnlyReduceDefs, primAgdaTCMDontReduceDefs,
    primAgdaTCMNoConstraints,
    primAgdaTCMRunSpeculative,
    primAgdaTCMExec,
    primAgdaTCMGetInstances
    :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

primInteger :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInteger                           = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinInteger
primIntegerPos :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIntegerPos                        = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinIntegerPos
primIntegerNegSuc :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIntegerNegSuc                     = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinIntegerNegSuc
primFloat :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFloat                             = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinFloat
primChar :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primChar                              = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinChar
primString :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primString                            = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinString
primBool :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primBool                              = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinBool
primSigma :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSigma                             = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinSigma
primUnit :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit                              = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinUnit
primUnitUnit :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnitUnit                          = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinUnitUnit
primTrue :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrue                              = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinTrue
primFalse :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFalse                             = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinFalse
primList :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primList                              = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinList
primNil :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNil                               = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinNil
primCons :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primCons                              = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinCons
primMaybe :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primMaybe                             = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinMaybe
primNothing :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNothing                           = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinNothing
primJust :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primJust                              = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinJust
primIO :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIO                                = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinIO
primId :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primId                                = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinId
primConId :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primConId                             = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m Term
getPrimitiveTerm String
builtinConId
primIdElim :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIdElim                            = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m Term
getPrimitiveTerm String
builtinIdElim
primPath :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPath                              = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinPath
primPathP :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPathP                             = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinPathP
primIntervalUniv :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIntervalUniv                      = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinIntervalUniv
primInterval :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInterval                          = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinInterval
primIZero :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero                             = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinIZero
primIOne :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne                              = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinIOne
primIMin :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMin                              = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m Term
getPrimitiveTerm String
builtinIMin
primIMax :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMax                              = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m Term
getPrimitiveTerm String
builtinIMax
primINeg :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg                              = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m Term
getPrimitiveTerm String
builtinINeg
primPartial :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPartial                           = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m Term
getPrimitiveTerm String
"primPartial"
primPartialP :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPartialP                          = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m Term
getPrimitiveTerm String
"primPartialP"
primIsOne :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne                             = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinIsOne
primItIsOne :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primItIsOne                           = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinItIsOne
primTrans :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrans                             = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m Term
getPrimitiveTerm String
builtinTrans
primHComp :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHComp                             = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m Term
getPrimitiveTerm String
builtinHComp
primEquiv :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquiv                             = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinEquiv
primEquivFun :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquivFun                          = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinEquivFun
primEquivProof :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquivProof                        = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinEquivProof
primTranspProof :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTranspProof                       = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinTranspProof
prim_glueU :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
prim_glueU                            = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m Term
getPrimitiveTerm String
builtin_glueU
prim_unglueU :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
prim_unglueU                          = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m Term
getPrimitiveTerm String
builtin_unglueU
primGlue :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primGlue                              = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m Term
getPrimitiveTerm String
builtinGlue
prim_glue :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
prim_glue                             = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m Term
getPrimitiveTerm String
builtin_glue
prim_unglue :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
prim_unglue                           = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m Term
getPrimitiveTerm String
builtin_unglue
primFaceForall :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFaceForall                        = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m Term
getPrimitiveTerm String
builtinFaceForall
primIsOne1 :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne1                            = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinIsOne1
primIsOne2 :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne2                            = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinIsOne2
primIsOneEmpty :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOneEmpty                        = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinIsOneEmpty
primSub :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSub                               = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinSub
primSubIn :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSubIn                             = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinSubIn
primSubOut :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSubOut                            = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m Term
getPrimitiveTerm String
builtinSubOut
primNat :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNat                               = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinNat
primSuc :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSuc                               = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinSuc
primZero :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primZero                              = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinZero
primNatPlus :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNatPlus                           = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinNatPlus
primNatMinus :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNatMinus                          = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinNatMinus
primNatTimes :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNatTimes                          = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinNatTimes
primNatDivSucAux :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNatDivSucAux                      = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinNatDivSucAux
primNatModSucAux :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNatModSucAux                      = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinNatModSucAux
primNatEquality :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNatEquality                       = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinNatEquals
primNatLess :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNatLess                           = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinNatLess
primWord64 :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primWord64                            = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinWord64
primSizeUniv :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeUniv                          = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinSizeUniv
primSize :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSize                              = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinSize
primSizeLt :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeLt                            = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinSizeLt
primSizeSuc :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeSuc                           = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinSizeSuc
primSizeInf :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf                           = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinSizeInf
primSizeMax :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeMax                           = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinSizeMax
primInf :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInf                               = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinInf
primSharp :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSharp                             = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinSharp
primFlat :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFlat                              = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinFlat
primEquality :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquality                          = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinEquality
primRefl :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRefl                              = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinRefl
primLevel :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel                             = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinLevel
primLevelZero :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero                         = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinLevelZero
primLevelSuc :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc                          = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinLevelSuc
primLevelMax :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax                          = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinLevelMax
primSet :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSet                               = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinSet
primProp :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primProp                              = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinProp
primSetOmega :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSetOmega                          = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinSetOmega
primLockUniv :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLockUniv                          = forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
String -> m Term
getPrimitiveTerm String
builtinLockUniv
primSSetOmega :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSSetOmega                         = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinSSetOmega
primStrictSet :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primStrictSet                         = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinStrictSet
primFromNat :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFromNat                           = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinFromNat
primFromNeg :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFromNeg                           = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinFromNeg
primFromString :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFromString                        = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinFromString
primQName :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQName                             = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinQName
primArg :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArg                               = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinArg
primArgArg :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArgArg                            = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinArgArg
primAbs :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAbs                               = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAbs
primAbsAbs :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAbsAbs                            = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAbsAbs
primAgdaSort :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSort                          = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaSort
primHiding :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHiding                            = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinHiding
primHidden :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHidden                            = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinHidden
primInstance :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInstance                          = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinInstance
primVisible :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primVisible                           = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinVisible
primRelevance :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRelevance                         = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinRelevance
primRelevant :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRelevant                          = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinRelevant
primIrrelevant :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIrrelevant                        = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinIrrelevant
primQuantity :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQuantity                          = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinQuantity
primQuantity0 :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQuantity0                         = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinQuantity0
primQuantityω :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQuantityω                         = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinQuantityω
primModality :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primModality                          = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinModality
primModalityConstructor :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primModalityConstructor               = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinModalityConstructor
primAssoc :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAssoc                             = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAssoc
primAssocLeft :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAssocLeft                         = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAssocLeft
primAssocRight :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAssocRight                        = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAssocRight
primAssocNon :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAssocNon                          = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAssocNon
primPrecedence :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPrecedence                        = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinPrecedence
primPrecRelated :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPrecRelated                       = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinPrecRelated
primPrecUnrelated :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPrecUnrelated                     = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinPrecUnrelated
primFixity :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFixity                            = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinFixity
primFixityFixity :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFixityFixity                      = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinFixityFixity
primArgInfo :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArgInfo                           = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinArgInfo
primArgArgInfo :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArgArgInfo                        = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinArgArgInfo
primAgdaSortSet :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortSet                       = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaSortSet
primAgdaSortLit :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortLit                       = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaSortLit
primAgdaSortProp :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortProp                      = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaSortProp
primAgdaSortPropLit :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortPropLit                   = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaSortPropLit
primAgdaSortInf :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortInf                       = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaSortInf
primAgdaSortUnsupported :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortUnsupported               = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaSortUnsupported
primAgdaTerm :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm                          = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTerm
primAgdaTermVar :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermVar                       = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTermVar
primAgdaTermLam :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermLam                       = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTermLam
primAgdaTermExtLam :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermExtLam                    = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTermExtLam
primAgdaTermDef :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermDef                       = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTermDef
primAgdaTermCon :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermCon                       = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTermCon
primAgdaTermPi :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermPi                        = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTermPi
primAgdaTermSort :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermSort                      = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTermSort
primAgdaTermLit :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermLit                       = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTermLit
primAgdaTermUnsupported :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermUnsupported               = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTermUnsupported
primAgdaTermMeta :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermMeta                      = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTermMeta
primAgdaErrorPart :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaErrorPart                     = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaErrorPart
primAgdaErrorPartString :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaErrorPartString               = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaErrorPartString
primAgdaErrorPartTerm :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaErrorPartTerm                 = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaErrorPartTerm
primAgdaErrorPartPatt :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaErrorPartPatt                 = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaErrorPartPatt
primAgdaErrorPartName :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaErrorPartName                 = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaErrorPartName
primAgdaLiteral :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLiteral                       = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaLiteral
primAgdaLitNat :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitNat                        = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaLitNat
primAgdaLitWord64 :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitWord64                     = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaLitWord64
primAgdaLitFloat :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitFloat                      = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaLitFloat
primAgdaLitChar :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitChar                       = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaLitChar
primAgdaLitString :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitString                     = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaLitString
primAgdaLitQName :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitQName                      = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaLitQName
primAgdaLitMeta :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitMeta                       = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaLitMeta
primAgdaPattern :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPattern                       = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaPattern
primAgdaPatCon :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatCon                        = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaPatCon
primAgdaPatVar :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatVar                        = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaPatVar
primAgdaPatDot :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatDot                        = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaPatDot
primAgdaPatLit :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatLit                        = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaPatLit
primAgdaPatProj :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatProj                       = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaPatProj
primAgdaPatAbsurd :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatAbsurd                     = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaPatAbsurd
primAgdaClause :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaClause                        = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaClause
primAgdaClauseClause :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaClauseClause                  = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaClauseClause
primAgdaClauseAbsurd :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaClauseAbsurd                  = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaClauseAbsurd
primAgdaDefinitionFunDef :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionFunDef              = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaDefinitionFunDef
primAgdaDefinitionDataDef :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionDataDef             = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaDefinitionDataDef
primAgdaDefinitionRecordDef :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionRecordDef           = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaDefinitionRecordDef
primAgdaDefinitionDataConstructor :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionDataConstructor     = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaDefinitionDataConstructor
primAgdaDefinitionPostulate :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionPostulate           = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaDefinitionPostulate
primAgdaDefinitionPrimitive :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionPrimitive           = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaDefinitionPrimitive
primAgdaDefinition :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinition                    = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaDefinition
primAgdaMeta :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaMeta                          = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaMeta
primAgdaTCM :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCM                           = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCM
primAgdaTCMReturn :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMReturn                     = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMReturn
primAgdaTCMBind :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMBind                       = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMBind
primAgdaTCMUnify :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMUnify                      = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMUnify
primAgdaTCMTypeError :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMTypeError                  = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMTypeError
primAgdaTCMInferType :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMInferType                  = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMInferType
primAgdaTCMCheckType :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMCheckType                  = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMCheckType
primAgdaTCMNormalise :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMNormalise                  = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMNormalise
primAgdaTCMReduce :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMReduce                     = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMReduce
primAgdaTCMCatchError :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMCatchError                 = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMCatchError
primAgdaTCMGetContext :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMGetContext                 = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMGetContext
primAgdaTCMExtendContext :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMExtendContext              = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMExtendContext
primAgdaTCMInContext :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMInContext                  = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMInContext
primAgdaTCMFreshName :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMFreshName                  = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMFreshName
primAgdaTCMDeclareDef :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDeclareDef                 = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMDeclareDef
primAgdaTCMDeclarePostulate :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDeclarePostulate           = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMDeclarePostulate
primAgdaTCMDeclareData :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDeclareData                = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMDeclareData
primAgdaTCMDefineData :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDefineData                 = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMDefineData
primAgdaTCMDefineFun :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDefineFun                  = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMDefineFun
primAgdaTCMGetType :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMGetType                    = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMGetType
primAgdaTCMGetDefinition :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMGetDefinition              = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMGetDefinition
primAgdaTCMQuoteTerm :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMQuoteTerm                  = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMQuoteTerm
primAgdaTCMQuoteOmegaTerm :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMQuoteOmegaTerm             = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMQuoteOmegaTerm
primAgdaTCMUnquoteTerm :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMUnquoteTerm                = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMUnquoteTerm
primAgdaTCMBlockOnMeta :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMBlockOnMeta                = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMBlockOnMeta
primAgdaTCMCommit :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMCommit                     = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMCommit
primAgdaTCMIsMacro :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMIsMacro                    = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMIsMacro
primAgdaTCMWithNormalisation :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMWithNormalisation          = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMWithNormalisation
primAgdaTCMWithReconsParams :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMWithReconsParams           = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMWithReconsParams
primAgdaTCMFormatErrorParts :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMFormatErrorParts           = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMFormatErrorParts
primAgdaTCMDebugPrint :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDebugPrint                 = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMDebugPrint
primAgdaTCMOnlyReduceDefs :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMOnlyReduceDefs             = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMOnlyReduceDefs
primAgdaTCMDontReduceDefs :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDontReduceDefs             = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMDontReduceDefs
primAgdaTCMNoConstraints :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMNoConstraints              = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMNoConstraints
primAgdaTCMRunSpeculative :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMRunSpeculative             = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMRunSpeculative
primAgdaTCMExec :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMExec                       = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMExec
primAgdaTCMGetInstances :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMGetInstances               = forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinAgdaTCMGetInstances

-- | The coinductive primitives.

data CoinductionKit = CoinductionKit
  { CoinductionKit -> QName
nameOfInf   :: QName
  , CoinductionKit -> QName
nameOfSharp :: QName
  , CoinductionKit -> QName
nameOfFlat  :: QName
  }

-- | Tries to build a 'CoinductionKit'.

coinductionKit' :: TCM CoinductionKit
coinductionKit' :: TCM CoinductionKit
coinductionKit' = do
  Def QName
inf   Elims
_ <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInf
  Def QName
sharp Elims
_ <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSharp
  Def QName
flat  Elims
_ <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFlat
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ CoinductionKit
    { nameOfInf :: QName
nameOfInf   = QName
inf
    , nameOfSharp :: QName
nameOfSharp = QName
sharp
    , nameOfFlat :: QName
nameOfFlat  = QName
flat
    }

coinductionKit :: TCM (Maybe CoinductionKit)
coinductionKit :: TCM (Maybe CoinductionKit)
coinductionKit = forall e (m :: * -> *) a.
(MonadError e m, Functor m) =>
m a -> m (Maybe a)
tryMaybe TCM CoinductionKit
coinductionKit'

-- | Sort primitives.

data SortKit = SortKit
  { SortKit -> QName
nameOfSet      :: QName
  , SortKit -> QName
nameOfProp     :: QName
  , SortKit -> QName
nameOfSSet     :: QName
  , SortKit -> IsFibrant -> QName
nameOfSetOmega :: IsFibrant -> QName
  }

-- | Compute a 'SortKit' in an environment that supports failures.
--
-- When 'optLoadPrimitives' is set to 'False', 'sortKit' is a fallible operation,
-- so for the uses of 'sortKit' in fallible contexts (e.g. 'TCM'),
-- we report a type error rather than exploding.
sortKit :: (HasBuiltins m, MonadTCError m, HasOptions m) => m SortKit
sortKit :: forall (m :: * -> *).
(HasBuiltins m, MonadTCError m, HasOptions m) =>
m SortKit
sortKit = do
  Def QName
set      Elims
_  <- forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinSet
  Def QName
prop     Elims
_  <- forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinProp
  Def QName
setomega Elims
_  <- forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinSetOmega
  Def QName
sset     Elims
_  <- forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinStrictSet
  Def QName
ssetomega Elims
_ <- forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
String -> m Term
getBuiltin String
builtinSSetOmega
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SortKit
    { nameOfSet :: QName
nameOfSet      = QName
set
    , nameOfProp :: QName
nameOfProp     = QName
prop
    , nameOfSSet :: QName
nameOfSSet     = QName
sset
    , nameOfSetOmega :: IsFibrant -> QName
nameOfSetOmega = \case
        IsFibrant
IsFibrant -> QName
setomega
        IsFibrant
IsStrict  -> QName
ssetomega
    }

-- | Compute a 'SortKit' in contexts that do not support failure (e.g.
-- 'Reify'). This should only be used when we are sure that the
-- primitive sorts have been bound, i.e. because it is "after" type
-- checking.
infallibleSortKit :: HasBuiltins m => m SortKit
infallibleSortKit :: forall (m :: * -> *). HasBuiltins m => m SortKit
infallibleSortKit = do
  Def QName
set      Elims
_  <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinSet
  Def QName
prop     Elims
_  <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinProp
  Def QName
setomega Elims
_  <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinSetOmega
  Def QName
sset     Elims
_  <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinStrictSet
  Def QName
ssetomega Elims
_ <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinSSetOmega
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ SortKit
    { nameOfSet :: QName
nameOfSet      = QName
set
    , nameOfProp :: QName
nameOfProp     = QName
prop
    , nameOfSSet :: QName
nameOfSSet     = QName
sset
    , nameOfSetOmega :: IsFibrant -> QName
nameOfSetOmega = \case
        IsFibrant
IsFibrant -> QName
setomega
        IsFibrant
IsStrict  -> QName
ssetomega
    }

------------------------------------------------------------------------
-- * Path equality
------------------------------------------------------------------------

getPrimName :: Term -> QName
getPrimName :: Term -> QName
getPrimName Term
ty = do
  let lamV :: Term -> ([Hiding], Term)
lamV (Lam ArgInfo
i Abs Term
b)  = forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst (forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
i forall a. a -> [a] -> [a]
:) forall a b. (a -> b) -> a -> b
$ Term -> ([Hiding], Term)
lamV (forall a. Abs a -> a
unAbs Abs Term
b)
      lamV (Pi Dom Type
_ Abs Type
b)   = Term -> ([Hiding], Term)
lamV (forall t a. Type'' t a -> a
unEl forall a b. (a -> b) -> a -> b
$ forall a. Abs a -> a
unAbs Abs Type
b)
      lamV Term
v          = ([], Term
v)
  case Term -> ([Hiding], Term)
lamV Term
ty of
            ([Hiding]
_, Def QName
path Elims
_) -> QName
path
            ([Hiding]
_, Con ConHead
nm ConInfo
_ Elims
_)   -> ConHead -> QName
conName ConHead
nm
            ([Hiding]
_, Var Int
0 [Proj ProjOrigin
_ QName
l]) -> QName
l
            ([Hiding]
_, Term
t)          -> forall a. HasCallStack => a
__IMPOSSIBLE__

getBuiltinName', getPrimitiveName' :: HasBuiltins m => String -> m (Maybe QName)
getBuiltinName' :: forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getBuiltinName' String
n = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> QName
getPrimName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
n
getPrimitiveName' :: forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' String
n = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PrimFun -> QName
primFunName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe PrimFun)
getPrimitive' String
n

isPrimitive :: HasBuiltins m => String -> QName -> m Bool
isPrimitive :: forall (m :: * -> *). HasBuiltins m => String -> QName -> m Bool
isPrimitive String
n QName
q = (forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
==) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' String
n

intervalSort :: Sort
intervalSort :: Sort
intervalSort = forall t. Sort' t
IntervalUniv

intervalView' :: HasBuiltins m => m (Term -> IntervalView)
intervalView' :: forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView' = do
  Maybe QName
iz <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getBuiltinName' String
builtinIZero
  Maybe QName
io <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getBuiltinName' String
builtinIOne
  Maybe QName
imax <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' String
"primIMax"
  Maybe QName
imin <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' String
"primIMin"
  Maybe QName
ineg <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' String
"primINeg"
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \ Term
t ->
    case Term
t of
      Def QName
q Elims
es ->
        case Elims
es of
          [Apply Arg Term
x,Apply Arg Term
y] | forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== Maybe QName
imin -> Arg Term -> Arg Term -> IntervalView
IMin Arg Term
x Arg Term
y
          [Apply Arg Term
x,Apply Arg Term
y] | forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== Maybe QName
imax -> Arg Term -> Arg Term -> IntervalView
IMax Arg Term
x Arg Term
y
          [Apply Arg Term
x]         | forall a. a -> Maybe a
Just QName
q forall a. Eq a => a -> a -> Bool
== Maybe QName
ineg -> Arg Term -> IntervalView
INeg Arg Term
x
          Elims
_                 -> Term -> IntervalView
OTerm Term
t
      Con ConHead
q ConInfo
_ [] | forall a. a -> Maybe a
Just (ConHead -> QName
conName ConHead
q) forall a. Eq a => a -> a -> Bool
== Maybe QName
iz -> IntervalView
IZero
                 | forall a. a -> Maybe a
Just (ConHead -> QName
conName ConHead
q) forall a. Eq a => a -> a -> Bool
== Maybe QName
io -> IntervalView
IOne
      Term
_ -> Term -> IntervalView
OTerm Term
t

intervalView :: HasBuiltins m => Term -> m IntervalView
intervalView :: forall (m :: * -> *). HasBuiltins m => Term -> m IntervalView
intervalView Term
t = do
  Term -> IntervalView
f <- forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
  forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> IntervalView
f Term
t)

intervalUnview :: HasBuiltins m => IntervalView -> m Term
intervalUnview :: forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview IntervalView
t = do
  IntervalView -> Term
f <- forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
  forall (m :: * -> *) a. Monad m => a -> m a
return (IntervalView -> Term
f IntervalView
t)

intervalUnview' :: HasBuiltins m => m (IntervalView -> Term)
intervalUnview' :: forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview' = do
  Term
iz <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinIZero -- should it be a type error instead?
  Term
io <- forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinIOne
  Term
imin <- (QName -> Elims -> Term
`Def` []) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' String
"primIMin"
  Term
imax <- (QName -> Elims -> Term
`Def` []) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' String
"primIMax"
  Term
ineg <- (QName -> Elims -> Term
`Def` []) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getPrimitiveName' String
"primINeg"
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \ IntervalView
v -> case IntervalView
v of
             IntervalView
IZero -> Term
iz
             IntervalView
IOne  -> Term
io
             IMin Arg Term
x Arg Term
y -> forall t. Apply t => t -> Args -> t
apply Term
imin [Arg Term
x,Arg Term
y]
             IMax Arg Term
x Arg Term
y -> forall t. Apply t => t -> Args -> t
apply Term
imax [Arg Term
x,Arg Term
y]
             INeg Arg Term
x   -> forall t. Apply t => t -> Args -> t
apply Term
ineg [Arg Term
x]
             OTerm Term
t -> Term
t

------------------------------------------------------------------------
-- * Path equality
------------------------------------------------------------------------

-- | Check whether the type is actually an path (lhs ≡ rhs)
--   and extract lhs, rhs, and their type.
--
--   Precondition: type is reduced.

pathView :: HasBuiltins m => Type -> m PathView
pathView :: forall (m :: * -> *). HasBuiltins m => Type -> m PathView
pathView Type
t0 = do
  Type -> PathView
view <- forall (m :: * -> *). HasBuiltins m => m (Type -> PathView)
pathView'
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> PathView
view Type
t0

pathView' :: HasBuiltins m => m (Type -> PathView)
pathView' :: forall (m :: * -> *). HasBuiltins m => m (Type -> PathView)
pathView' = do
 Maybe QName
mpath  <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getBuiltinName' String
builtinPath
 Maybe QName
mpathp <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getBuiltinName' String
builtinPathP
 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \ t0 :: Type
t0@(El Sort
s Term
t) ->
  case Term
t of
    Def QName
path' [ Apply Arg Term
level , Apply Arg Term
typ , Apply Arg Term
lhs , Apply Arg Term
rhs ]
      | forall a. a -> Maybe a
Just QName
path' forall a. Eq a => a -> a -> Bool
== Maybe QName
mpath, Just QName
path <- Maybe QName
mpathp -> Sort
-> QName
-> Arg Term
-> Arg Term
-> Arg Term
-> Arg Term
-> PathView
PathType Sort
s QName
path Arg Term
level (Term -> Term
lam_i forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term
typ) Arg Term
lhs Arg Term
rhs
      where lam_i :: Term -> Term
lam_i = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. String -> a -> Abs a
NoAbs String
"_"
    Def QName
path' [ Apply Arg Term
level , Apply Arg Term
typ , Apply Arg Term
lhs , Apply Arg Term
rhs ]
      | forall a. a -> Maybe a
Just QName
path' forall a. Eq a => a -> a -> Bool
== Maybe QName
mpathp, Just QName
path <- Maybe QName
mpathp -> Sort
-> QName
-> Arg Term
-> Arg Term
-> Arg Term
-> Arg Term
-> PathView
PathType Sort
s QName
path Arg Term
level Arg Term
typ Arg Term
lhs Arg Term
rhs
    Term
_ -> Type -> PathView
OType Type
t0

-- | Non dependent Path
idViewAsPath :: HasBuiltins m => Type -> m PathView
idViewAsPath :: forall (m :: * -> *). HasBuiltins m => Type -> m PathView
idViewAsPath t0 :: Type
t0@(El Sort
s Term
t) = do
  Maybe QName
mid <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> QName
getPrimName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinId
  Maybe QName
mpath <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> QName
getPrimName forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getBuiltin' String
builtinPath
  case Maybe QName
mid of
   Just QName
path | forall a. Maybe a -> Bool
isJust Maybe QName
mpath -> case Term
t of
    Def QName
path' [ Apply Arg Term
level , Apply Arg Term
typ , Apply Arg Term
lhs , Apply Arg Term
rhs ]
      | QName
path' forall a. Eq a => a -> a -> Bool
== QName
path -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort
-> QName
-> Arg Term
-> Arg Term
-> Arg Term
-> Arg Term
-> PathView
PathType Sort
s (forall a. HasCallStack => Maybe a -> a
fromJust Maybe QName
mpath) Arg Term
level Arg Term
typ Arg Term
lhs Arg Term
rhs
    Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> PathView
OType Type
t0
   Maybe QName
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> PathView
OType Type
t0

boldPathView :: Type -> PathView
boldPathView :: Type -> PathView
boldPathView t0 :: Type
t0@(El Sort
s Term
t) = do
  case Term
t of
    Def QName
path' [ Apply Arg Term
level , Apply Arg Term
typ , Apply Arg Term
lhs , Apply Arg Term
rhs ]
      -> Sort
-> QName
-> Arg Term
-> Arg Term
-> Arg Term
-> Arg Term
-> PathView
PathType Sort
s QName
path' Arg Term
level Arg Term
typ Arg Term
lhs Arg Term
rhs
    Term
_ -> Type -> PathView
OType Type
t0

-- | Revert the 'PathView'.
--
--   Postcondition: type is reduced.

pathUnview :: PathView -> Type
pathUnview :: PathView -> Type
pathUnview (OType Type
t) = Type
t
pathUnview (PathType Sort
s QName
path Arg Term
l Arg Term
t Arg Term
lhs Arg Term
rhs) =
  forall t a. Sort' t -> a -> Type'' t a
El Sort
s forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
path forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply [Arg Term
l, Arg Term
t, Arg Term
lhs, Arg Term
rhs]

------------------------------------------------------------------------
-- * Swan's Id Equality
------------------------------------------------------------------------

-- f x (< phi , p > : Id A x _) = Just (phi,p)
conidView' :: HasBuiltins m => m (Term -> Term -> Maybe (Arg Term,Arg Term))
conidView' :: forall (m :: * -> *).
HasBuiltins m =>
m (Term -> Term -> Maybe (Arg Term, Arg Term))
conidView' = do
  Maybe [QName]
mn <- forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getName' [String
builtinReflId, String
builtinConId]
  Maybe Term
mio <- forall (m :: * -> *). HasBuiltins m => String -> m (Maybe Term)
getTerm' String
builtinIOne
  let fallback :: m (p -> p -> Maybe a)
fallback = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \ p
_ p
_ -> forall a. Maybe a
Nothing
  forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe [QName]
mn forall {p} {p} {a}. m (p -> p -> Maybe a)
fallback forall a b. (a -> b) -> a -> b
$ \ [QName
refl,QName
conid] ->
   forall a b. Maybe a -> b -> (a -> b) -> b
caseMaybe Maybe Term
mio forall {p} {p} {a}. m (p -> p -> Maybe a)
fallback forall a b. (a -> b) -> a -> b
$ \ Term
io -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ \ Term
x Term
t ->
    case Term
t of
      Con ConHead
h ConInfo
_ [] | ConHead -> QName
conName ConHead
h forall a. Eq a => a -> a -> Bool
== QName
refl -> forall a. a -> Maybe a
Just (forall a. a -> Arg a
defaultArg Term
io,forall a. a -> Arg a
defaultArg (ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo forall a b. (a -> b) -> a -> b
$ forall a. String -> a -> Abs a
NoAbs String
"_" forall a b. (a -> b) -> a -> b
$ Term
x))
      Def QName
d Elims
es | Just [Arg Term
l,Arg Term
a,Arg Term
x,Arg Term
y,Arg Term
phi,Arg Term
p] <- forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es, QName
d forall a. Eq a => a -> a -> Bool
== QName
conid -> forall a. a -> Maybe a
Just (Arg Term
phi, Arg Term
p)
      Term
_ -> forall a. Maybe a
Nothing

------------------------------------------------------------------------
-- * Builtin equality
------------------------------------------------------------------------

-- | Get the name of the equality type.
primEqualityName :: TCM QName
-- primEqualityName = getDef =<< primEquality  -- LEADS TO IMPORT CYCLE
primEqualityName :: TCM QName
primEqualityName = do
  Term
eq <- forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquality
  -- Andreas, 2014-05-17 moved this here from TC.Rules.Def
  -- Don't know why up to 2 hidden lambdas need to be stripped,
  -- but I left the code in place.
  -- Maybe it was intended that equality could be declared
  -- in three different ways:
  -- 1. universe and type polymorphic
  -- 2. type polymorphic only
  -- 3. monomorphic.
  let lamV :: Term -> ([Hiding], Term)
lamV (Lam ArgInfo
i Abs Term
b)  = forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst (forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
i forall a. a -> [a] -> [a]
:) forall a b. (a -> b) -> a -> b
$ Term -> ([Hiding], Term)
lamV (forall a. Abs a -> a
unAbs Abs Term
b)
      lamV Term
v          = ([], Term
v)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ case Term -> ([Hiding], Term)
lamV Term
eq of
    ([Hiding]
_, Def QName
equality Elims
_) -> QName
equality
    ([Hiding], Term)
_                   -> forall a. HasCallStack => a
__IMPOSSIBLE__

-- | Check whether the type is actually an equality (lhs ≡ rhs)
--   and extract lhs, rhs, and their type.
--
--   Precondition: type is reduced.

equalityView :: Type -> TCM EqualityView
equalityView :: Type -> TCM EqualityView
equalityView t0 :: Type
t0@(El Sort
s Term
t) = do
  QName
equality <- TCM QName
primEqualityName
  case Term
t of
    Def QName
equality' Elims
es | QName
equality' forall a. Eq a => a -> a -> Bool
== QName
equality -> do
      let vs :: Args
vs = forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
__IMPOSSIBLE__ forall a b. (a -> b) -> a -> b
$ forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
      let n :: Int
n = forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
vs
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Int
n forall a. Ord a => a -> a -> Bool
>= Int
3) forall a. HasCallStack => a
__IMPOSSIBLE__
      let (Args
pars, [ Arg Term
typ , Arg Term
lhs, Arg Term
rhs ]) = forall a. Int -> [a] -> ([a], [a])
splitAt (Int
nforall a. Num a => a -> a -> a
-Int
3) Args
vs
      forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Sort
-> QName
-> Args
-> Arg Term
-> Arg Term
-> Arg Term
-> EqualityView
EqualityType Sort
s QName
equality Args
pars Arg Term
typ Arg Term
lhs Arg Term
rhs
    Term
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Type -> EqualityView
OtherType Type
t0

-- | Revert the 'EqualityView'.
--
--   Postcondition: type is reduced.

class EqualityUnview a where
  equalityUnview :: a -> Type

instance EqualityUnview EqualityView where
  equalityUnview :: EqualityView -> Type
equalityUnview = \case
    OtherType Type
t -> Type
t
    IdiomType Type
t -> Type
t
    EqualityViewType EqualityTypeData
eqt -> forall a. EqualityUnview a => a -> Type
equalityUnview EqualityTypeData
eqt

instance EqualityUnview EqualityTypeData where
  equalityUnview :: EqualityTypeData -> Type
equalityUnview (EqualityTypeData Sort
s QName
equality Args
l Arg Term
t Arg Term
lhs Arg Term
rhs) =
    forall t a. Sort' t -> a -> Type'' t a
El Sort
s forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
equality forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Arg a -> Elim' a
Apply (Args
l forall a. [a] -> [a] -> [a]
++ [Arg Term
t, Arg Term
lhs, Arg Term
rhs])

-- | Primitives with typechecking constrants.
constrainedPrims :: [String]
constrainedPrims :: [String]
constrainedPrims =
  [ String
builtinConId
  , String
builtinPOr
  , String
builtinComp
  , String
builtinHComp
  , String
builtinTrans
  , String
builtin_glue
  , String
builtin_glueU
  ]

getNameOfConstrained :: HasBuiltins m => String -> m (Maybe QName)
getNameOfConstrained :: forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getNameOfConstrained String
s = do
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (String
s forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
constrainedPrims) forall a. HasCallStack => a
__IMPOSSIBLE__
  forall (m :: * -> *). HasBuiltins m => String -> m (Maybe QName)
getName' String
s