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

import Control.Monad.Except         ( MonadError(..), ExceptT )
import Control.Monad.IO.Class       ( MonadIO(..) )
import Control.Monad.Reader         ( ReaderT )
import Control.Monad.State          ( StateT )
import Control.Monad.Trans.Identity ( IdentityT )
import Control.Monad.Trans.Maybe
import Control.Monad.Writer         ( WriterT )

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.TypeChecking.Monad.Base
-- import Agda.TypeChecking.Functions  -- LEADS TO IMPORT CYCLE
import Agda.TypeChecking.Substitute

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

import Agda.Utils.StrictReader qualified as Strict
import Agda.Utils.StrictWriter qualified as Strict
import Agda.Utils.StrictState  qualified as Strict

import Agda.Utils.Impossible

class ( Functor m
      , Applicative m
      , Monad m
      ) => HasBuiltins m where
  getBuiltinThing :: SomeBuiltin -> m (Maybe (Builtin PrimFun))

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

instance HasBuiltins m => HasBuiltins (ChangeT m)
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)
instance HasBuiltins m => HasBuiltins (Strict.ReaderT e m)
instance HasBuiltins m => HasBuiltins (Strict.StateT s m)
instance (HasBuiltins m, Monoid w) => HasBuiltins (Strict.WriterT w m)

deriving instance HasBuiltins m => HasBuiltins (BlockT m)

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


-- | The trivial implementation of 'HasBuiltins', using a constant 'TCState'.
--
-- This may be used instead of 'TCMT'/'ReduceM' where builtins must be accessed
-- in a pure context.
newtype BuiltinAccess a = BuiltinAccess { forall a. BuiltinAccess a -> TCState -> a
unBuiltinAccess :: TCState -> a }
  deriving ((forall a b. (a -> b) -> BuiltinAccess a -> BuiltinAccess b)
-> (forall a b. a -> BuiltinAccess b -> BuiltinAccess a)
-> Functor BuiltinAccess
forall a b. a -> BuiltinAccess b -> BuiltinAccess a
forall a b. (a -> b) -> BuiltinAccess a -> BuiltinAccess b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> BuiltinAccess a -> BuiltinAccess b
fmap :: forall a b. (a -> b) -> BuiltinAccess a -> BuiltinAccess b
$c<$ :: forall a b. a -> BuiltinAccess b -> BuiltinAccess a
<$ :: forall a b. a -> BuiltinAccess b -> BuiltinAccess a
Functor, Functor BuiltinAccess
Functor BuiltinAccess =>
(forall a. a -> BuiltinAccess a)
-> (forall a b.
    BuiltinAccess (a -> b) -> BuiltinAccess a -> BuiltinAccess b)
-> (forall a b c.
    (a -> b -> c)
    -> BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess c)
-> (forall a b.
    BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess b)
-> (forall a b.
    BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess a)
-> Applicative BuiltinAccess
forall a. a -> BuiltinAccess a
forall a b. BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess a
forall a b. BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess b
forall a b.
BuiltinAccess (a -> b) -> BuiltinAccess a -> BuiltinAccess b
forall a b c.
(a -> b -> c)
-> BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
$cpure :: forall a. a -> BuiltinAccess a
pure :: forall a. a -> BuiltinAccess a
$c<*> :: forall a b.
BuiltinAccess (a -> b) -> BuiltinAccess a -> BuiltinAccess b
<*> :: forall a b.
BuiltinAccess (a -> b) -> BuiltinAccess a -> BuiltinAccess b
$cliftA2 :: forall a b c.
(a -> b -> c)
-> BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess c
liftA2 :: forall a b c.
(a -> b -> c)
-> BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess c
$c*> :: forall a b. BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess b
*> :: forall a b. BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess b
$c<* :: forall a b. BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess a
<* :: forall a b. BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess a
Applicative, Applicative BuiltinAccess
Applicative BuiltinAccess =>
(forall a b.
 BuiltinAccess a -> (a -> BuiltinAccess b) -> BuiltinAccess b)
-> (forall a b.
    BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess b)
-> (forall a. a -> BuiltinAccess a)
-> Monad BuiltinAccess
forall a. a -> BuiltinAccess a
forall a b. BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess b
forall a b.
BuiltinAccess a -> (a -> BuiltinAccess b) -> BuiltinAccess b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall a b.
BuiltinAccess a -> (a -> BuiltinAccess b) -> BuiltinAccess b
>>= :: forall a b.
BuiltinAccess a -> (a -> BuiltinAccess b) -> BuiltinAccess b
$c>> :: forall a b. BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess b
>> :: forall a b. BuiltinAccess a -> BuiltinAccess b -> BuiltinAccess b
$creturn :: forall a. a -> BuiltinAccess a
return :: forall a. a -> BuiltinAccess a
Monad)

instance MonadFail BuiltinAccess where
  fail :: forall a. String -> BuiltinAccess a
fail String
msg = (TCState -> a) -> BuiltinAccess a
forall a. (TCState -> a) -> BuiltinAccess a
BuiltinAccess ((TCState -> a) -> BuiltinAccess a)
-> (TCState -> a) -> BuiltinAccess a
forall a b. (a -> b) -> a -> b
$ \TCState
_ -> String -> a
forall a. HasCallStack => String -> a
error String
msg

instance HasBuiltins BuiltinAccess where
  getBuiltinThing :: SomeBuiltin -> BuiltinAccess (Maybe (Builtin PrimFun))
getBuiltinThing SomeBuiltin
b = (TCState -> Maybe (Builtin PrimFun))
-> BuiltinAccess (Maybe (Builtin PrimFun))
forall a. (TCState -> a) -> BuiltinAccess a
BuiltinAccess ((TCState -> Maybe (Builtin PrimFun))
 -> BuiltinAccess (Maybe (Builtin PrimFun)))
-> (TCState -> Maybe (Builtin PrimFun))
-> BuiltinAccess (Maybe (Builtin PrimFun))
forall a b. (a -> b) -> a -> b
$ \TCState
state ->
    (Builtin PrimFun -> Builtin PrimFun -> Builtin PrimFun)
-> Maybe (Builtin PrimFun)
-> Maybe (Builtin PrimFun)
-> Maybe (Builtin PrimFun)
forall a. (a -> a -> a) -> Maybe a -> Maybe a -> Maybe a
unionMaybeWith Builtin PrimFun -> Builtin PrimFun -> Builtin PrimFun
forall a. Builtin a -> Builtin a -> Builtin a
unionBuiltin
      (SomeBuiltin
-> Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SomeBuiltin
b (Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun))
-> Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun)
forall a b. (a -> b) -> a -> b
$ TCState
state TCState
-> Getting
     (Map SomeBuiltin (Builtin PrimFun))
     TCState
     (Map SomeBuiltin (Builtin PrimFun))
-> Map SomeBuiltin (Builtin PrimFun)
forall s a. s -> Getting a s a -> a
^. Getting
  (Map SomeBuiltin (Builtin PrimFun))
  TCState
  (Map SomeBuiltin (Builtin PrimFun))
Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
stLocalBuiltins)
      (SomeBuiltin
-> Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup SomeBuiltin
b (Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun))
-> Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun)
forall a b. (a -> b) -> a -> b
$ TCState
state TCState
-> Getting
     (Map SomeBuiltin (Builtin PrimFun))
     TCState
     (Map SomeBuiltin (Builtin PrimFun))
-> Map SomeBuiltin (Builtin PrimFun)
forall s a. s -> Getting a s a -> a
^. Getting
  (Map SomeBuiltin (Builtin PrimFun))
  TCState
  (Map SomeBuiltin (Builtin PrimFun))
Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
stImportedBuiltins)

-- | Run a 'BuiltinAccess' monad.
runBuiltinAccess :: TCState -> BuiltinAccess a -> a
runBuiltinAccess :: forall a. TCState -> BuiltinAccess a -> a
runBuiltinAccess TCState
s BuiltinAccess a
m = BuiltinAccess a -> TCState -> a
forall a. BuiltinAccess a -> TCState -> a
unBuiltinAccess BuiltinAccess a
m TCState
s


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

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

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

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

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

-- | Get the currently registered rewrite relation symbols.
getBuiltinRewriteRelations :: (HasBuiltins m, MonadTCError m) => m (Set QName)
getBuiltinRewriteRelations :: forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
m (Set QName)
getBuiltinRewriteRelations =
  m (Set QName) -> m (Maybe (Set QName)) -> m (Set QName)
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (TypeError -> m (Set QName)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m (Set QName)) -> TypeError -> m (Set QName)
forall a b. (a -> b) -> a -> b
$ BuiltinId -> TypeError
NoBindingForBuiltin BuiltinId
builtinRewrite) m (Maybe (Set QName))
forall (m :: * -> *). HasBuiltins m => m (Maybe (Set QName))
getBuiltinRewriteRelations'

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

{-# INLINABLE getBuiltinName_ #-}
getBuiltinName_ :: (HasBuiltins m, MonadTCError m)
  => BuiltinId -> m QName
getBuiltinName_ :: forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m QName
getBuiltinName_ BuiltinId
x =
  m QName -> m (Maybe QName) -> m QName
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (TypeError -> m QName
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m QName) -> TypeError -> m QName
forall a b. (a -> b) -> a -> b
$ BuiltinId -> TypeError
NoBindingForBuiltin BuiltinId
x) (m (Maybe QName) -> m QName) -> m (Maybe QName) -> m QName
forall a b. (a -> b) -> a -> b
$ BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
x

-- {-# INLINABLE getBuiltinName' #-}
-- -- | Returns 'Nothing' if built-in is not bound or bound to a 'Prim' or anything other than a 'Def'.
-- getBuiltinName' :: HasBuiltins m => BuiltinId -> m (Maybe Term)
-- getBuiltinName' x = (getBuiltinName =<<) <$> getBuiltin' x
--   where
--     getBuiltinName = \case
--       Def f [] -> Just f
--       _        -> Nothing

{-# SPECIALIZE getBuiltin :: BuiltinId -> TCM Term #-}
getBuiltin :: (HasBuiltins m, MonadTCError m)
           => BuiltinId -> m Term
getBuiltin :: forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
x =
  m Term -> m (Maybe Term) -> m Term
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (TypeError -> m Term
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m Term) -> TypeError -> m Term
forall a b. (a -> b) -> a -> b
$ BuiltinId -> TypeError
NoBindingForBuiltin BuiltinId
x) (m (Maybe Term) -> m Term) -> m (Maybe Term) -> m Term
forall a b. (a -> b) -> a -> b
$ BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
x

{-# SPECIALIZE getBuiltin' :: BuiltinId -> TCM (Maybe Term) #-}
-- | Returns 'Nothing' if built-in is not bound or bound to a 'Prim'.
getBuiltin' :: HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' :: forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
x = (Builtin PrimFun -> Maybe Term
forall {pf}. Builtin pf -> Maybe Term
getBuiltin (Builtin PrimFun -> Maybe Term)
-> Maybe (Builtin PrimFun) -> Maybe Term
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) (Maybe (Builtin PrimFun) -> Maybe Term)
-> m (Maybe (Builtin PrimFun)) -> m (Maybe Term)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SomeBuiltin -> m (Maybe (Builtin PrimFun))
forall (m :: * -> *).
HasBuiltins m =>
SomeBuiltin -> m (Maybe (Builtin PrimFun))
getBuiltinThing (BuiltinId -> SomeBuiltin
BuiltinName BuiltinId
x)
  where
    getBuiltin :: Builtin pf -> Maybe Term
getBuiltin = \case
      Builtin Term
t                 -> Term -> Maybe Term
forall a. a -> Maybe a
Just (Term -> Maybe Term) -> Term -> Maybe Term
forall a b. (a -> b) -> a -> b
$ KillRangeT Term
forall a. KillRange a => KillRangeT a
killRange Term
t
      Prim{}                    -> Maybe Term
forall a. Maybe a
Nothing
      BuiltinRewriteRelations{} -> Maybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__

{-# SPECIALIZE getPrimitive' :: PrimitiveId -> TCM (Maybe PrimFun)  #-}
-- | Returns 'Nothing' if primitive is not bound or bound to a 'Builtin'.
getPrimitive' :: HasBuiltins m => PrimitiveId -> m (Maybe PrimFun)
getPrimitive' :: forall (m :: * -> *).
HasBuiltins m =>
PrimitiveId -> m (Maybe PrimFun)
getPrimitive' PrimitiveId
x = (Builtin PrimFun -> Maybe PrimFun
forall {a}. Builtin a -> Maybe a
getPrim (Builtin PrimFun -> Maybe PrimFun)
-> Maybe (Builtin PrimFun) -> Maybe PrimFun
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<<) (Maybe (Builtin PrimFun) -> Maybe PrimFun)
-> m (Maybe (Builtin PrimFun)) -> m (Maybe PrimFun)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SomeBuiltin -> m (Maybe (Builtin PrimFun))
forall (m :: * -> *).
HasBuiltins m =>
SomeBuiltin -> m (Maybe (Builtin PrimFun))
getBuiltinThing (PrimitiveId -> SomeBuiltin
PrimitiveName PrimitiveId
x)
  where
    getPrim :: Builtin a -> Maybe a
getPrim = \case
      Prim a
pf                   -> a -> Maybe a
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return a
pf
      Builtin{}                 -> Maybe a
forall a. Maybe a
Nothing
      BuiltinRewriteRelations{} -> Maybe a
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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


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

getTerm' :: (HasBuiltins m, IsBuiltin a) => a -> m (Maybe Term)
getTerm' :: forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe Term)
getTerm' = SomeBuiltin -> m (Maybe Term)
forall {m :: * -> *}.
HasBuiltins m =>
SomeBuiltin -> m (Maybe Term)
go (SomeBuiltin -> m (Maybe Term))
-> (a -> SomeBuiltin) -> a -> m (Maybe Term)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin where
  go :: SomeBuiltin -> m (Maybe Term)
go (BuiltinName BuiltinId
x)   = BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
x
  go (PrimitiveName PrimitiveId
x) = PrimitiveId -> m (Maybe Term)
forall (m :: * -> *).
HasBuiltins m =>
PrimitiveId -> m (Maybe Term)
getPrimitiveTerm' PrimitiveId
x

getName' :: (HasBuiltins m, IsBuiltin a) => a -> m (Maybe QName)
getName' :: forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe QName)
getName' = SomeBuiltin -> m (Maybe QName)
forall {m :: * -> *}.
HasBuiltins m =>
SomeBuiltin -> m (Maybe QName)
go (SomeBuiltin -> m (Maybe QName))
-> (a -> SomeBuiltin) -> a -> m (Maybe QName)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> SomeBuiltin
forall a. IsBuiltin a => a -> SomeBuiltin
someBuiltin where
  go :: SomeBuiltin -> m (Maybe QName)
go (BuiltinName BuiltinId
x)   = BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
x
  go (PrimitiveName PrimitiveId
x) = PrimitiveId -> m (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
PrimitiveId -> m (Maybe QName)
getPrimitiveName' PrimitiveId
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, IsBuiltin a) => String -> a -> m Term
getTerm :: forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
String -> a -> m Term
getTerm String
use a
name = (m Term -> m (Maybe Term) -> m Term)
-> m (Maybe Term) -> m Term -> m Term
forall a b c. (a -> b -> c) -> b -> a -> c
flip m Term -> m (Maybe Term) -> m Term
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (a -> m (Maybe Term)
forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
a -> m (Maybe Term)
getTerm' a
name) (m Term -> m Term) -> m Term -> m Term
forall a b. (a -> b) -> a -> b
$
  Term -> m Term
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> m Term) -> Term -> m Term
forall a b. (a -> b) -> a -> b
$! Impossible -> Term
forall a. Impossible -> a
throwImpossible ([String] -> String -> Impossible
ImpMissingDefinitions [a -> String
forall a. IsBuiltin a => a -> String
getBuiltinId a
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 = Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinZero
      pSuc :: m Term
pSuc  = Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinSuc
  -- By passing the builtins lazily we do not have to look them up if @v@ is not a 'LitNat'.
  m Term -> m Term -> Term -> m Term
forall (m :: * -> *).
Applicative m =>
m Term -> m Term -> Term -> m Term
constructorForm' m Term
pZero m Term
pSuc Term
v

-- | Produce a function that rewrites a literal to constructor form if possible.
constructorFormer :: HasBuiltins m => m (Term -> Term)
constructorFormer :: forall (m :: * -> *). HasBuiltins m => m (KillRangeT Term)
constructorFormer = do
  mz <- BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinZero
  ms <- getBuiltin' builtinSuc
  return \ Term
v -> Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
v (Maybe Term -> Maybe Term -> Term -> Maybe Term
forall (m :: * -> *).
Applicative m =>
m Term -> m Term -> Term -> m Term
constructorForm' Maybe Term
mz Maybe Term
ms Term
v)

{-# INLINABLE constructorForm' #-}
{-# SPECIALIZE constructorForm' :: TCM Term -> TCM Term -> Term -> TCM Term #-}
{-# SPECIALIZE constructorForm' :: Maybe Term -> Maybe Term -> Term -> Maybe Term #-}
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 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0    -> m Term
pZero
      | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0     -> (Term -> KillRangeT Term
forall t. Apply t => t -> Term -> t
`apply1` Literal -> Term
Lit (Integer -> Literal
LitNat (Integer -> Literal) -> Integer -> Literal
forall a b. (a -> b) -> a -> b
$ Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)) KillRangeT Term -> m Term -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Term
pSuc
      | Bool
otherwise -> Term -> m Term
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Term
v
    Term
_ -> Term -> m Term
forall a. a -> m a
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,
    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,
    primLevelUniv,
    primProp, primSet, primStrictSet, primPropOmega, primSetOmega, 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,
    primAgdaBlocker, primAgdaBlockerAny, primAgdaBlockerAll, primAgdaBlockerMeta,
    primAgdaTCM, primAgdaTCMReturn, primAgdaTCMBind, primAgdaTCMUnify,
    primAgdaTCMTypeError, primAgdaTCMInferType, primAgdaTCMCheckType,
    primAgdaTCMNormalise, primAgdaTCMReduce,
    primAgdaTCMCatchError, primAgdaTCMGetContext, primAgdaTCMExtendContext, primAgdaTCMInContext,
    primAgdaTCMFreshName, primAgdaTCMDeclareDef, primAgdaTCMDeclarePostulate, primAgdaTCMDeclareData, primAgdaTCMDefineData, primAgdaTCMDefineFun,
    primAgdaTCMGetType, primAgdaTCMGetDefinition,
    primAgdaTCMQuoteTerm, primAgdaTCMUnquoteTerm, primAgdaTCMQuoteOmegaTerm,
    primAgdaTCMCommit, primAgdaTCMIsMacro, primAgdaTCMBlock,
    primAgdaTCMFormatErrorParts, primAgdaTCMDebugPrint,
    primAgdaTCMWithNormalisation, primAgdaTCMWithReconstructed,
    primAgdaTCMWithExpandLast, primAgdaTCMWithReduceDefs,
    primAgdaTCMAskNormalisation, primAgdaTCMAskReconstructed,
    primAgdaTCMAskExpandLast, primAgdaTCMAskReduceDefs,
    primAgdaTCMNoConstraints,
    primAgdaTCMWorkOnTypes,
    primAgdaTCMRunSpeculative,
    primAgdaTCMExec,
    primAgdaTCMCheckFromString,
    primAgdaTCMGetInstances,
    primAgdaTCMSolveInstances,
    primAgdaTCMPragmaForeign,
    primAgdaTCMPragmaCompile
    :: (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                           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinInteger
primIntegerPos :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIntegerPos                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinIntegerPos
primIntegerNegSuc :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIntegerNegSuc                     = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinIntegerNegSuc
primFloat :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFloat                             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinFloat
primChar :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primChar                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinChar
primString :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primString                            = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinString
primBool :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primBool                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinBool
primSigma :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSigma                             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinSigma
primUnit :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinUnit
primUnitUnit :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnitUnit                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinUnitUnit
primTrue :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrue                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinTrue
primFalse :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFalse                             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinFalse
primList :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primList                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinList
primNil :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNil                               = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinNil
primCons :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primCons                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinCons
primMaybe :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primMaybe                             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinMaybe
primNothing :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNothing                           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinNothing
primJust :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primJust                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinJust
primIO :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIO                                = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinIO
primPath :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPath                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinPath
primPathP :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPathP                             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinPathP
primIntervalUniv :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIntervalUniv                      = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinIntervalUniv
primInterval :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInterval                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinInterval
primIZero :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIZero                             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinIZero
primIOne :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIOne                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinIOne
primIMin :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMin                              = PrimitiveId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
PrimitiveId -> m Term
getPrimitiveTerm PrimitiveId
builtinIMin
primIMax :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIMax                              = PrimitiveId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
PrimitiveId -> m Term
getPrimitiveTerm PrimitiveId
builtinIMax
primINeg :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primINeg                              = PrimitiveId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
PrimitiveId -> m Term
getPrimitiveTerm PrimitiveId
builtinINeg
primPartial :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPartial                           = PrimitiveId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
PrimitiveId -> m Term
getPrimitiveTerm PrimitiveId
PrimPartial
primPartialP :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPartialP                          = PrimitiveId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
PrimitiveId -> m Term
getPrimitiveTerm PrimitiveId
PrimPartialP
primIsOne :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne                             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinIsOne
primItIsOne :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primItIsOne                           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinItIsOne
primTrans :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrans                             = PrimitiveId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
PrimitiveId -> m Term
getPrimitiveTerm PrimitiveId
builtinTrans
primHComp :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHComp                             = PrimitiveId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
PrimitiveId -> m Term
getPrimitiveTerm PrimitiveId
builtinHComp
primEquiv :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquiv                             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinEquiv
primEquivFun :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquivFun                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinEquivFun
primEquivProof :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquivProof                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinEquivProof
primTranspProof :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTranspProof                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinTranspProof
prim_glueU :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
prim_glueU                            = PrimitiveId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
PrimitiveId -> m Term
getPrimitiveTerm PrimitiveId
builtin_glueU
prim_unglueU :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
prim_unglueU                          = PrimitiveId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
PrimitiveId -> m Term
getPrimitiveTerm PrimitiveId
builtin_unglueU
primGlue :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primGlue                              = PrimitiveId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
PrimitiveId -> m Term
getPrimitiveTerm PrimitiveId
builtinGlue
prim_glue :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
prim_glue                             = PrimitiveId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
PrimitiveId -> m Term
getPrimitiveTerm PrimitiveId
builtin_glue
prim_unglue :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
prim_unglue                           = PrimitiveId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
PrimitiveId -> m Term
getPrimitiveTerm PrimitiveId
builtin_unglue
primFaceForall :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFaceForall                        = PrimitiveId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
PrimitiveId -> m Term
getPrimitiveTerm PrimitiveId
builtinFaceForall
primIsOne1 :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne1                            = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinIsOne1
primIsOne2 :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOne2                            = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinIsOne2
primIsOneEmpty :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIsOneEmpty                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinIsOneEmpty
primSub :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSub                               = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinSub
primSubIn :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSubIn                             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinSubIn
primSubOut :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSubOut                            = PrimitiveId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
PrimitiveId -> m Term
getPrimitiveTerm PrimitiveId
builtinSubOut
primNat :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNat                               = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinNat
primSuc :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSuc                               = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinSuc
primZero :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primZero                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinZero
primNatPlus :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNatPlus                           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinNatPlus
primNatMinus :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNatMinus                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinNatMinus
primNatTimes :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNatTimes                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinNatTimes
primNatDivSucAux :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNatDivSucAux                      = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinNatDivSucAux
primNatModSucAux :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNatModSucAux                      = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinNatModSucAux
primNatEquality :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNatEquality                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinNatEquals
primNatLess :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNatLess                           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinNatLess
primWord64 :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primWord64                            = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinWord64
primSizeUniv :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeUniv                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinSizeUniv
primSize :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSize                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinSize
primSizeLt :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeLt                            = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinSizeLt
primSizeSuc :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeSuc                           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinSizeSuc
primSizeInf :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeInf                           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinSizeInf
primSizeMax :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSizeMax                           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinSizeMax
primInf :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInf                               = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinInf
primSharp :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSharp                             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinSharp
primFlat :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFlat                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinFlat
primEquality :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquality                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinEquality
primRefl :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRefl                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinRefl
primLevel :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevel                             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinLevel
primLevelZero :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelZero                         = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinLevelZero
primLevelSuc :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelSuc                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinLevelSuc
primLevelMax :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelMax                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinLevelMax
primProp :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primProp                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinProp
primSet :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSet                               = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinSet
primStrictSet :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primStrictSet                         = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinStrictSet
primPropOmega :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPropOmega                         = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinPropOmega
primSetOmega :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSetOmega                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinSetOmega
primSSetOmega :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSSetOmega                         = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinSSetOmega
primLockUniv :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLockUniv                          = PrimitiveId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
PrimitiveId -> m Term
getPrimitiveTerm PrimitiveId
builtinLockUniv
primLevelUniv :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primLevelUniv                         = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinLevelUniv
primFromNat :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFromNat                           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinFromNat
primFromNeg :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFromNeg                           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinFromNeg
primFromString :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFromString                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinFromString
primQName :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQName                             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinQName
primArg :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArg                               = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinArg
primArgArg :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArgArg                            = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinArgArg
primAbs :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAbs                               = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAbs
primAbsAbs :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAbsAbs                            = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAbsAbs
primAgdaSort :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSort                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaSort
primHiding :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHiding                            = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinHiding
primHidden :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primHidden                            = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinHidden
primInstance :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInstance                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinInstance
primVisible :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primVisible                           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinVisible
primRelevance :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRelevance                         = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinRelevance
primRelevant :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primRelevant                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinRelevant
primIrrelevant :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIrrelevant                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinIrrelevant
primQuantity :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQuantity                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinQuantity
primQuantity0 :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQuantity0                         = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinQuantity0
primQuantityω :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQuantityω                         = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinQuantityω
primModality :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primModality                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinModality
primModalityConstructor :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primModalityConstructor               = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinModalityConstructor
primAssoc :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAssoc                             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAssoc
primAssocLeft :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAssocLeft                         = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAssocLeft
primAssocRight :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAssocRight                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAssocRight
primAssocNon :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAssocNon                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAssocNon
primPrecedence :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPrecedence                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinPrecedence
primPrecRelated :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPrecRelated                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinPrecRelated
primPrecUnrelated :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primPrecUnrelated                     = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinPrecUnrelated
primFixity :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFixity                            = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinFixity
primFixityFixity :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFixityFixity                      = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinFixityFixity
primAgdaBlocker :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaBlocker                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaBlocker
primAgdaBlockerAny :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaBlockerAny                    = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaBlockerAny
primAgdaBlockerAll :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaBlockerAll                    = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaBlockerAll
primAgdaBlockerMeta :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaBlockerMeta                   = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaBlockerMeta
primArgInfo :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArgInfo                           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinArgInfo
primArgArgInfo :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primArgArgInfo                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinArgArgInfo
primAgdaSortSet :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortSet                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaSortSet
primAgdaSortLit :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortLit                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaSortLit
primAgdaSortProp :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortProp                      = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaSortProp
primAgdaSortPropLit :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortPropLit                   = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaSortPropLit
primAgdaSortInf :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortInf                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaSortInf
primAgdaSortUnsupported :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortUnsupported               = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaSortUnsupported
primAgdaTerm :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTerm                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTerm
primAgdaTermVar :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermVar                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTermVar
primAgdaTermLam :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermLam                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTermLam
primAgdaTermExtLam :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermExtLam                    = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTermExtLam
primAgdaTermDef :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermDef                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTermDef
primAgdaTermCon :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermCon                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTermCon
primAgdaTermPi :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermPi                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTermPi
primAgdaTermSort :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermSort                      = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTermSort
primAgdaTermLit :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermLit                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTermLit
primAgdaTermUnsupported :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermUnsupported               = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTermUnsupported
primAgdaTermMeta :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTermMeta                      = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTermMeta
primAgdaErrorPart :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaErrorPart                     = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaErrorPart
primAgdaErrorPartString :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaErrorPartString               = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaErrorPartString
primAgdaErrorPartTerm :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaErrorPartTerm                 = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaErrorPartTerm
primAgdaErrorPartPatt :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaErrorPartPatt                 = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaErrorPartPatt
primAgdaErrorPartName :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaErrorPartName                 = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaErrorPartName
primAgdaLiteral :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLiteral                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaLiteral
primAgdaLitNat :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitNat                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaLitNat
primAgdaLitWord64 :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitWord64                     = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaLitWord64
primAgdaLitFloat :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitFloat                      = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaLitFloat
primAgdaLitChar :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitChar                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaLitChar
primAgdaLitString :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitString                     = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaLitString
primAgdaLitQName :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitQName                      = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaLitQName
primAgdaLitMeta :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitMeta                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaLitMeta
primAgdaPattern :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPattern                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaPattern
primAgdaPatCon :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatCon                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaPatCon
primAgdaPatVar :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatVar                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaPatVar
primAgdaPatDot :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatDot                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaPatDot
primAgdaPatLit :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatLit                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaPatLit
primAgdaPatProj :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatProj                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaPatProj
primAgdaPatAbsurd :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatAbsurd                     = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaPatAbsurd
primAgdaClause :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaClause                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaClause
primAgdaClauseClause :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaClauseClause                  = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaClauseClause
primAgdaClauseAbsurd :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaClauseAbsurd                  = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaClauseAbsurd
primAgdaDefinitionFunDef :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionFunDef              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaDefinitionFunDef
primAgdaDefinitionDataDef :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionDataDef             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaDefinitionDataDef
primAgdaDefinitionRecordDef :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionRecordDef           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaDefinitionRecordDef
primAgdaDefinitionDataConstructor :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionDataConstructor     = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaDefinitionDataConstructor
primAgdaDefinitionPostulate :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionPostulate           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaDefinitionPostulate
primAgdaDefinitionPrimitive :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionPrimitive           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaDefinitionPrimitive
primAgdaDefinition :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinition                    = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaDefinition
primAgdaMeta :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaMeta                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaMeta
primAgdaTCM :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCM                           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCM
primAgdaTCMReturn :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMReturn                     = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMReturn
primAgdaTCMBind :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMBind                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMBind
primAgdaTCMUnify :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMUnify                      = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMUnify
primAgdaTCMTypeError :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMTypeError                  = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMTypeError
primAgdaTCMInferType :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMInferType                  = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMInferType
primAgdaTCMCheckType :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMCheckType                  = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMCheckType
primAgdaTCMNormalise :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMNormalise                  = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMNormalise
primAgdaTCMReduce :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMReduce                     = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMReduce
primAgdaTCMCatchError :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMCatchError                 = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMCatchError
primAgdaTCMGetContext :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMGetContext                 = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMGetContext
primAgdaTCMExtendContext :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMExtendContext              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMExtendContext
primAgdaTCMInContext :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMInContext                  = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMInContext
primAgdaTCMFreshName :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMFreshName                  = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMFreshName
primAgdaTCMDeclareDef :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDeclareDef                 = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMDeclareDef
primAgdaTCMDeclarePostulate :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDeclarePostulate           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMDeclarePostulate
primAgdaTCMDeclareData :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDeclareData                = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMDeclareData
primAgdaTCMDefineData :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDefineData                 = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMDefineData
primAgdaTCMDefineFun :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDefineFun                  = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMDefineFun
primAgdaTCMGetType :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMGetType                    = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMGetType
primAgdaTCMGetDefinition :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMGetDefinition              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMGetDefinition
primAgdaTCMQuoteTerm :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMQuoteTerm                  = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMQuoteTerm
primAgdaTCMQuoteOmegaTerm :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMQuoteOmegaTerm             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMQuoteOmegaTerm
primAgdaTCMUnquoteTerm :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMUnquoteTerm                = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMUnquoteTerm
primAgdaTCMBlock :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMBlock                      = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMBlock
primAgdaTCMCommit :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMCommit                     = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMCommit
primAgdaTCMIsMacro :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMIsMacro                    = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMIsMacro
primAgdaTCMWithNormalisation :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMWithNormalisation          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMWithNormalisation
primAgdaTCMWithReconstructed :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMWithReconstructed          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMWithReconstructed
primAgdaTCMWithExpandLast :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMWithExpandLast             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMWithExpandLast
primAgdaTCMWithReduceDefs :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMWithReduceDefs             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMWithReduceDefs
primAgdaTCMAskNormalisation :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMAskNormalisation           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMAskNormalisation
primAgdaTCMAskReconstructed :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMAskReconstructed           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMAskReconstructed
primAgdaTCMAskExpandLast :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMAskExpandLast              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMAskExpandLast
primAgdaTCMAskReduceDefs :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMAskReduceDefs              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMAskReduceDefs
primAgdaTCMFormatErrorParts :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMFormatErrorParts           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMFormatErrorParts
primAgdaTCMDebugPrint :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDebugPrint                 = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMDebugPrint
primAgdaTCMNoConstraints :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMNoConstraints              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMNoConstraints
primAgdaTCMWorkOnTypes :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMWorkOnTypes                = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMWorkOnTypes
primAgdaTCMRunSpeculative :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMRunSpeculative             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMRunSpeculative
primAgdaTCMExec :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMExec                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMExec
primAgdaTCMCheckFromString :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMCheckFromString            = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMCheckFromString
primAgdaTCMGetInstances :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMGetInstances               = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMGetInstances
primAgdaTCMSolveInstances :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMSolveInstances             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMSolveInstances
primAgdaTCMPragmaForeign :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMPragmaForeign              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMPragmaForeign
primAgdaTCMPragmaCompile :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMPragmaCompile              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMPragmaCompile

-- | 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
  inf   <- BuiltinId -> TCMT IO QName
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m QName
getBuiltinName_ BuiltinId
builtinInf
  sharp <- getBuiltinName_ builtinSharp
  flat  <- getBuiltinName_ builtinFlat
  return $ CoinductionKit
    { nameOfInf   = inf
    , nameOfSharp = sharp
    , nameOfFlat  = flat
    }

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

-- | Sort primitives.

data SortKit = SortKit
  { SortKit -> UnivSize -> Univ -> QName
nameOfUniv   :: UnivSize -> Univ -> QName
  , SortKit -> QName -> Maybe (UnivSize, Univ)
isNameOfUniv :: QName -> Maybe (UnivSize, Univ)
  }

mkSortKit :: QName -> QName -> QName -> QName -> QName -> QName -> SortKit
mkSortKit :: QName -> QName -> QName -> QName -> QName -> QName -> SortKit
mkSortKit QName
prop QName
set QName
sset QName
propomega QName
setomega QName
ssetomega = SortKit
  { nameOfUniv :: UnivSize -> Univ -> QName
nameOfUniv = ((UnivSize, Univ) -> QName) -> UnivSize -> Univ -> QName
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((UnivSize, Univ) -> QName) -> UnivSize -> Univ -> QName)
-> ((UnivSize, Univ) -> QName) -> UnivSize -> Univ -> QName
forall a b. (a -> b) -> a -> b
$ \case
      (UnivSize
USmall , Univ
UProp) -> QName
prop
      (UnivSize
USmall , Univ
UType) -> QName
set
      (UnivSize
USmall , Univ
USSet) -> QName
sset
      (UnivSize
ULarge , Univ
UProp) -> QName
propomega
      (UnivSize
ULarge , Univ
UType) -> QName
setomega
      (UnivSize
ULarge , Univ
USSet) -> QName
ssetomega
  , isNameOfUniv :: QName -> Maybe (UnivSize, Univ)
isNameOfUniv = \ QName
x -> if
      | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
prop      -> (UnivSize, Univ) -> Maybe (UnivSize, Univ)
forall a. a -> Maybe a
Just (UnivSize
USmall , Univ
UProp)
      | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
set       -> (UnivSize, Univ) -> Maybe (UnivSize, Univ)
forall a. a -> Maybe a
Just (UnivSize
USmall , Univ
UType)
      | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
sset      -> (UnivSize, Univ) -> Maybe (UnivSize, Univ)
forall a. a -> Maybe a
Just (UnivSize
USmall , Univ
USSet)
      | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
propomega -> (UnivSize, Univ) -> Maybe (UnivSize, Univ)
forall a. a -> Maybe a
Just (UnivSize
ULarge , Univ
UProp)
      | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
setomega  -> (UnivSize, Univ) -> Maybe (UnivSize, Univ)
forall a. a -> Maybe a
Just (UnivSize
ULarge , Univ
UType)
      | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
ssetomega -> (UnivSize, Univ) -> Maybe (UnivSize, Univ)
forall a. a -> Maybe a
Just (UnivSize
ULarge , Univ
USSet)
      | Bool
otherwise -> Maybe (UnivSize, Univ)
forall a. Maybe a
Nothing
  }

-- | 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) => m SortKit
sortKit :: forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m SortKit
sortKit = do
  prop      <- BuiltinId -> m QName
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m QName
getBuiltinName_ BuiltinId
builtinProp
  set       <- getBuiltinName_ builtinSet
  sset      <- getBuiltinName_ builtinStrictSet
  propomega <- getBuiltinName_ builtinPropOmega
  setomega  <- getBuiltinName_ builtinSetOmega
  ssetomega <- getBuiltinName_ builtinSSetOmega
  return $ mkSortKit prop set sset propomega setomega 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
  prop      <- QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinProp
  set       <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSet
  sset      <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinStrictSet
  propomega <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinPropOmega
  setomega  <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSetOmega
  ssetomega <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSSetOmega
  return $ mkSortKit prop set sset propomega setomega 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)  = ([Hiding] -> [Hiding]) -> ([Hiding], Term) -> ([Hiding], Term)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
i Hiding -> [Hiding] -> [Hiding]
forall a. a -> [a] -> [a]
:) (([Hiding], Term) -> ([Hiding], Term))
-> ([Hiding], Term) -> ([Hiding], Term)
forall a b. (a -> b) -> a -> b
$ Term -> ([Hiding], Term)
lamV (Abs Term -> Term
forall a. Abs a -> a
unAbs Abs Term
b)
      lamV (Pi Dom Type
_ Abs Type
b)   = Term -> ([Hiding], Term)
lamV (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Abs Type -> Type
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)          -> QName
forall a. HasCallStack => a
__IMPOSSIBLE__

getBuiltinName' :: HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' :: forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
n = (Term -> QName) -> Maybe Term -> Maybe QName
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term -> QName
getPrimName (Maybe Term -> Maybe QName) -> m (Maybe Term) -> m (Maybe QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
n

getPrimitiveName' :: HasBuiltins m => PrimitiveId -> m (Maybe QName)
getPrimitiveName' :: forall (m :: * -> *).
HasBuiltins m =>
PrimitiveId -> m (Maybe QName)
getPrimitiveName' PrimitiveId
n = (PrimFun -> QName) -> Maybe PrimFun -> Maybe QName
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap PrimFun -> QName
primFunName (Maybe PrimFun -> Maybe QName)
-> m (Maybe PrimFun) -> m (Maybe QName)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PrimitiveId -> m (Maybe PrimFun)
forall (m :: * -> *).
HasBuiltins m =>
PrimitiveId -> m (Maybe PrimFun)
getPrimitive' PrimitiveId
n

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

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

{-# SPECIALIZE intervalView' :: TCM (Term -> IntervalView) #-}
{-# INLINABLE intervalView' #-}
intervalView' :: HasBuiltins m => m (Term -> IntervalView)
intervalView' :: forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView' = do
  iz <- BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinIZero
  io <- getBuiltinName' builtinIOne
  imax <- getPrimitiveName' builtinIMax
  imin <- getPrimitiveName' builtinIMin
  ineg <- getPrimitiveName' builtinINeg
  return $ \ Term
t ->
    case Term
t of
      Def QName
q Elims
es ->
        case Elims
es of
          [Apply Arg Term
x,Apply Arg Term
y] | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
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] | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
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]         | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
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
_ [] | QName -> Maybe QName
forall a. a -> Maybe a
Just (ConHead -> QName
conName ConHead
q) Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
iz -> IntervalView
IZero
                 | QName -> Maybe QName
forall a. a -> Maybe a
Just (ConHead -> QName
conName ConHead
q) Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
io -> IntervalView
IOne
      Term
_ -> Term -> IntervalView
OTerm Term
t

{-# INLINE intervalView #-}
intervalView :: HasBuiltins m => Term -> m IntervalView
intervalView :: forall (m :: * -> *). HasBuiltins m => Term -> m IntervalView
intervalView Term
t = do
  f <- m (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
  return (f t)

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

{-# SPECIALIZE intervalUnview' :: TCM (IntervalView -> Term) #-}
intervalUnview' :: HasBuiltins m => m (IntervalView -> Term)
intervalUnview' :: forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview' = do
  iz <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinIZero -- should it be a type error instead?
  io <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinIOne
  imin <- (`Def` []) . fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' builtinIMin
  imax <- (`Def` []) . fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' builtinIMax
  ineg <- (`Def` []) . fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' builtinINeg
  return $ \ IntervalView
v -> case IntervalView
v of
             IntervalView
IZero -> Term
iz
             IntervalView
IOne  -> Term
io
             IMin Arg Term
x Arg Term
y -> Term -> Args -> Term
forall t. Apply t => t -> Args -> t
apply Term
imin [Arg Term
x,Arg Term
y]
             IMax Arg Term
x Arg Term
y -> Term -> Args -> Term
forall t. Apply t => t -> Args -> t
apply Term
imax [Arg Term
x,Arg Term
y]
             INeg Arg Term
x   -> Term -> Args -> Term
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.

{-# INLINE pathView #-}
pathView :: HasBuiltins m => Type -> m PathView
pathView :: forall (m :: * -> *). HasBuiltins m => Type -> m PathView
pathView Type
t0 = do
  view <- m (Type -> PathView)
forall (m :: * -> *). HasBuiltins m => m (Type -> PathView)
pathView'
  return $ view t0

{-# SPECIALIZE pathView' :: TCM (Type -> PathView)  #-}
pathView' :: HasBuiltins m => m (Type -> PathView)
pathView' :: forall (m :: * -> *). HasBuiltins m => m (Type -> PathView)
pathView' = do
 mpath  <- BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinPath
 mpathp <- getBuiltinName' builtinPathP
 return $ \ t0 :: Type
t0@(El Sort' Term
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 ]
      | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
path' Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mpath, Just QName
path <- Maybe QName
mpathp -> Sort' Term
-> QName
-> Arg Term
-> Arg Term
-> Arg Term
-> Arg Term
-> PathView
PathType Sort' Term
s QName
path Arg Term
level (KillRangeT Term
lam_i KillRangeT Term -> Arg Term -> Arg Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term
typ) Arg Term
lhs Arg Term
rhs
      where lam_i :: KillRangeT Term
lam_i = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo (Abs Term -> Term) -> (Term -> Abs Term) -> KillRangeT Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Term -> Abs Term
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 ]
      | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
path' Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mpathp, Just QName
path <- Maybe QName
mpathp -> Sort' Term
-> QName
-> Arg Term
-> Arg Term
-> Arg Term
-> Arg Term
-> PathView
PathType Sort' Term
s QName
path Arg Term
level Arg Term
typ Arg Term
lhs Arg Term
rhs
    Term
_ -> Type -> PathView
OType Type
t0

boldPathView :: Type -> PathView
boldPathView :: Type -> PathView
boldPathView t0 :: Type
t0@(El Sort' Term
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' Term
-> QName
-> Arg Term
-> Arg Term
-> Arg Term
-> Arg Term
-> PathView
PathType Sort' Term
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' Term
s QName
path Arg Term
l Arg Term
t Arg Term
lhs Arg Term
rhs) =
  Sort' Term -> Term -> Type
forall t a. Sort' t -> a -> Type'' t a
El Sort' Term
s (Term -> Type) -> Term -> Type
forall a b. (a -> b) -> a -> b
$ QName -> Elims -> Term
Def QName
path (Elims -> Term) -> Elims -> Term
forall a b. (a -> b) -> a -> b
$ (Arg Term -> Elim' Term) -> Args -> Elims
forall a b. (a -> b) -> [a] -> [b]
map Arg Term -> Elim' Term
forall a. Arg a -> Elim' a
Apply [Arg Term
l, Arg Term
t, Arg Term
lhs, Arg Term
rhs]

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

-- | Get the name of the equality type.
primEqualityName :: TCM QName
primEqualityName :: TCMT IO QName
primEqualityName = do
  eq <- TCMT IO Term
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 (Lam ArgInfo
i Abs Term
b)  = ([Hiding] -> [Hiding]) -> ([Hiding], Term) -> ([Hiding], Term)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
i Hiding -> [Hiding] -> [Hiding]
forall a. a -> [a] -> [a]
:) (([Hiding], Term) -> ([Hiding], Term))
-> ([Hiding], Term) -> ([Hiding], Term)
forall a b. (a -> b) -> a -> b
$ Term -> ([Hiding], Term)
lamV (Abs Term -> Term
forall a. Abs a -> a
unAbs Abs Term
b)
      lamV Term
v          = ([], Term
v)
  return $ case lamV eq of
    ([Hiding]
_, Def QName
equality Elims
_) -> QName
equality
    ([Hiding], Term)
_                   -> QName
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 ::
     Range  -- ^ Range of the @rewrite@ expression, if any.
  -> Type   -- ^ Identity type?
  -> TCM EqualityView
equalityView :: Range -> Type -> TCM EqualityView
equalityView Range
r t0 :: Type
t0@(El Sort' Term
s Term
t) = do
  equality <- TCMT IO QName
primEqualityName
  case t of
    Def QName
equality' Elims
es | QName
equality' QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
equality -> do
      let vs :: Args
vs = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
      let n :: Int
n = Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
vs
      Bool -> TCM () -> TCM ()
forall b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
3) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      let (Args
pars, [ Arg Term
typ , Arg Term
lhs, Arg Term
rhs ]) = Int -> Args -> (Args, Args)
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
3) Args
vs
      EqualityView -> TCM EqualityView
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (EqualityView -> TCM EqualityView)
-> EqualityView -> TCM EqualityView
forall a b. (a -> b) -> a -> b
$ Range
-> Sort' Term
-> QName
-> Args
-> Arg Term
-> Arg Term
-> Arg Term
-> EqualityView
EqualityType Range
r Sort' Term
s QName
equality Args
pars Arg Term
typ Arg Term
lhs Arg Term
rhs
    Term
_ -> EqualityView -> TCM EqualityView
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (EqualityView -> TCM EqualityView)
-> EqualityView -> TCM EqualityView
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 -> EqualityTypeData -> Type
forall a. EqualityUnview a => a -> Type
equalityUnview EqualityTypeData
eqt

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

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

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