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

import qualified Control.Monad.Fail as Fail

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

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

import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Syntax.Literal
import Agda.Syntax.Builtin
import Agda.Syntax.Internal as I
import Agda.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.Impossible

class ( Functor m
      , Applicative m
      , Fail.MonadFail 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)

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 Fail.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
-> Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
-> Map SomeBuiltin (Builtin PrimFun)
forall o i. o -> Lens' o i -> i
^. (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))
-> Map SomeBuiltin (Builtin PrimFun) -> Maybe (Builtin PrimFun)
forall a b. (a -> b) -> a -> b
$ TCState
state TCState
-> Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
-> Map SomeBuiltin (Builtin PrimFun)
forall o i. o -> Lens' o i -> i
^. (Map SomeBuiltin (Builtin PrimFun)
 -> f (Map SomeBuiltin (Builtin PrimFun)))
-> TCState -> f TCState
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
    Term
_ <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primZero
    Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ m Term -> m ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (m Term -> m ()) -> m Term -> m ()
forall a b. (a -> b) -> a -> b
$ m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSuc
    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
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 PrimFun -> 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
  Maybe (Builtin PrimFun)
builtin <- SomeBuiltin -> TCMT IO (Maybe (Builtin PrimFun))
forall (m :: * -> *).
HasBuiltins m =>
SomeBuiltin -> m (Maybe (Builtin PrimFun))
getBuiltinThing SomeBuiltin
b'
  case Maybe (Builtin PrimFun)
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
  Maybe (Builtin PrimFun)
builtin <- SomeBuiltin -> TCMT IO (Maybe (Builtin PrimFun))
forall (m :: * -> *).
HasBuiltins m =>
SomeBuiltin -> m (Maybe (Builtin PrimFun))
getBuiltinThing SomeBuiltin
b'
  case Maybe (Builtin PrimFun)
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 => 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 getBuiltin #-}
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

{-# INLINABLE getBuiltin' #-}
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 BuiltinRewriteRelations{} = Maybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__
  getBuiltin (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
  getBuiltin Builtin pf
_                         = Maybe Term
forall a. Maybe a
Nothing

{-# INLINABLE getPrimitive' #-}
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 (Prim a
pf) = a -> Maybe a
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return a
pf
    getPrim BuiltinRewriteRelations{} = Maybe a
forall a. HasCallStack => a
__IMPOSSIBLE__
    getPrim Builtin a
_         = Maybe a
forall a. Maybe a
Nothing

{-# 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
  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

{-# INLINABLE constructorForm' #-}
{-# SPECIALIZE constructorForm' :: TCM Term -> TCM Term -> Term -> TCM 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,
    primId, primConId, primIdElim,
    primEquiv, primEquivFun, primEquivProof,
    primTranspProof,
    primGlue, prim_glue, prim_unglue,
    prim_glueU, prim_unglueU,
    primFaceForall,
    primNatPlus, primNatMinus, primNatTimes, primNatDivSucAux, primNatModSucAux,
    primNatEquality, primNatLess,
    -- Machine words
    primWord64,
    primSizeUniv, primSize, primSizeLt, primSizeSuc, primSizeInf, primSizeMax,
    primInf, primSharp, primFlat,
    primEquality, primRefl,
    primLevel, primLevelZero, primLevelSuc, primLevelMax,
    primLockUniv,
    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,
    primAgdaTCMRunSpeculative,
    primAgdaTCMExec,
    primAgdaTCMGetInstances,
    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
primId :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primId                                = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinId
primConId :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primConId                             = PrimitiveId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
PrimitiveId -> m Term
getPrimitiveTerm PrimitiveId
builtinConId
primIdElim :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIdElim                            = PrimitiveId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
PrimitiveId -> m Term
getPrimitiveTerm PrimitiveId
builtinIdElim
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
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
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
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
  Def QName
inf   Elims
_ <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInf
  Def QName
sharp Elims
_ <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSharp
  Def QName
flat  Elims
_ <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFlat
  CoinductionKit -> TCM CoinductionKit
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (CoinductionKit -> TCM CoinductionKit)
-> CoinductionKit -> TCM CoinductionKit
forall a b. (a -> b) -> a -> b
$ CoinductionKit
    { nameOfInf :: QName
nameOfInf   = QName
inf
    , nameOfSharp :: QName
nameOfSharp = QName
sharp
    , nameOfFlat :: QName
nameOfFlat  = QName
flat
    }

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

-- | Sort primitives.

data SortKit = SortKit
  { SortKit -> 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, HasOptions m) => m SortKit
sortKit :: forall (m :: * -> *).
(HasBuiltins m, MonadTCError m, HasOptions m) =>
m SortKit
sortKit = do
  Def QName
prop     Elims
_  <- BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinProp
  Def QName
set      Elims
_  <- BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinSet
  Def QName
sset     Elims
_  <- BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinStrictSet
  Def QName
propomega Elims
_ <- BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinPropOmega
  Def QName
setomega Elims
_  <- BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinSetOmega
  Def QName
ssetomega Elims
_ <- BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinSSetOmega
  SortKit -> m SortKit
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SortKit -> m SortKit) -> SortKit -> m SortKit
forall a b. (a -> b) -> a -> b
$ QName -> QName -> QName -> QName -> QName -> QName -> SortKit
mkSortKit QName
prop QName
set QName
sset QName
propomega QName
setomega QName
ssetomega

-- | Compute a 'SortKit' in contexts that do not support failure (e.g.
-- 'Reify'). This should only be used when we are sure that the
-- primitive sorts have been bound, i.e. because it is "after" type
-- checking.
infallibleSortKit :: HasBuiltins m => m SortKit
infallibleSortKit :: forall (m :: * -> *). HasBuiltins m => m SortKit
infallibleSortKit = do
  Def QName
prop     Elims
_  <- 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
builtinProp
  Def QName
set      Elims
_  <- 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
builtinSet
  Def QName
sset     Elims
_  <- 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
builtinStrictSet
  Def QName
propomega Elims
_ <- 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
builtinPropOmega
  Def QName
setomega Elims
_  <- 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
builtinSetOmega
  Def QName
ssetomega Elims
_ <- 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
builtinSSetOmega
  SortKit -> m SortKit
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (SortKit -> m SortKit) -> SortKit -> m SortKit
forall a b. (a -> b) -> a -> b
$ QName -> QName -> QName -> QName -> QName -> QName -> SortKit
mkSortKit QName
prop QName
set QName
sset QName
propomega QName
setomega QName
ssetomega

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

getPrimName :: Term -> QName
getPrimName :: Term -> QName
getPrimName Term
ty = do
  let lamV :: Term -> ([Hiding], Term)
lamV (Lam ArgInfo
i Abs Term
b)  = ([Hiding] -> [Hiding]) -> ([Hiding], Term) -> ([Hiding], Term)
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst (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
  Maybe QName
iz <- BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinIZero
  Maybe QName
io <- BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinIOne
  Maybe QName
imax <- PrimitiveId -> m (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
PrimitiveId -> m (Maybe QName)
getPrimitiveName' PrimitiveId
builtinIMax
  Maybe QName
imin <- PrimitiveId -> m (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
PrimitiveId -> m (Maybe QName)
getPrimitiveName' PrimitiveId
builtinIMin
  Maybe QName
ineg <- PrimitiveId -> m (Maybe QName)
forall (m :: * -> *).
HasBuiltins m =>
PrimitiveId -> m (Maybe QName)
getPrimitiveName' PrimitiveId
builtinINeg
  (Term -> IntervalView) -> m (Term -> IntervalView)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Term -> IntervalView) -> m (Term -> IntervalView))
-> (Term -> IntervalView) -> m (Term -> IntervalView)
forall a b. (a -> b) -> a -> b
$ \ Term
t ->
    case Term
t of
      Def QName
q Elims
es ->
        case Elims
es of
          [Apply Arg Term
x,Apply Arg Term
y] | 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
  Term -> IntervalView
f <- m (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
  IntervalView -> m IntervalView
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Term -> IntervalView
f Term
t)

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

{-# SPECIALIZE intervalUnview' :: TCM (IntervalView -> Term) #-}
intervalUnview' :: HasBuiltins m => m (IntervalView -> Term)
intervalUnview' :: forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview' = do
  Term
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?
  Term
io <- 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
builtinIOne
  Term
imin <- (QName -> Elims -> Term
`Def` []) (QName -> Term) -> (Maybe QName -> QName) -> Maybe QName -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe QName -> Term) -> m (Maybe QName) -> m 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
builtinIMin
  Term
imax <- (QName -> Elims -> Term
`Def` []) (QName -> Term) -> (Maybe QName -> QName) -> Maybe QName -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe QName -> Term) -> m (Maybe QName) -> m 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
builtinIMax
  Term
ineg <- (QName -> Elims -> Term
`Def` []) (QName -> Term) -> (Maybe QName -> QName) -> Maybe QName -> Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe QName -> Term) -> m (Maybe QName) -> m 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
builtinINeg
  (IntervalView -> Term) -> m (IntervalView -> Term)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((IntervalView -> Term) -> m (IntervalView -> Term))
-> (IntervalView -> Term) -> m (IntervalView -> Term)
forall a b. (a -> b) -> a -> b
$ \ IntervalView
v -> case IntervalView
v of
             IntervalView
IZero -> Term
iz
             IntervalView
IOne  -> Term
io
             IMin Arg Term
x Arg Term
y -> 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
  Type -> PathView
view <- m (Type -> PathView)
forall (m :: * -> *). HasBuiltins m => m (Type -> PathView)
pathView'
  PathView -> m PathView
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (PathView -> m PathView) -> PathView -> m PathView
forall a b. (a -> b) -> a -> b
$ Type -> PathView
view Type
t0

{-# SPECIALIZE pathView' :: TCM (Type -> PathView)  #-}
pathView' :: HasBuiltins m => m (Type -> PathView)
pathView' :: forall (m :: * -> *). HasBuiltins m => m (Type -> PathView)
pathView' = do
 Maybe QName
mpath  <- BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinPath
 Maybe QName
mpathp <- BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinPathP
 (Type -> PathView) -> m (Type -> PathView)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Type -> PathView) -> m (Type -> PathView))
-> (Type -> PathView) -> m (Type -> PathView)
forall a b. (a -> b) -> a -> b
$ \ 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

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

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

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

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

-- | Get the name of the equality type.
primEqualityName :: TCM QName
-- primEqualityName = getDef =<< primEquality  -- LEADS TO IMPORT CYCLE
primEqualityName :: TCM QName
primEqualityName = do
  Term
eq <- 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 :: Term -> ([Hiding], Term)
lamV (Lam ArgInfo
i Abs Term
b)  = ([Hiding] -> [Hiding]) -> ([Hiding], Term) -> ([Hiding], Term)
forall a c b. (a -> c) -> (a, b) -> (c, b)
mapFst (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)
  QName -> TCM QName
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (QName -> TCM QName) -> QName -> TCM QName
forall a b. (a -> b) -> a -> b
$ case Term -> ([Hiding], Term)
lamV Term
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 :: Type -> TCM EqualityView
equalityView :: Type -> TCM EqualityView
equalityView t0 :: Type
t0@(El Sort' Term
s Term
t) = do
  QName
equality <- TCM QName
primEqualityName
  case Term
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 (f :: * -> *). Applicative f => Bool -> f () -> f ()
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
$ Sort' Term
-> QName
-> Args
-> Arg Term
-> Arg Term
-> Arg Term
-> EqualityView
EqualityType 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 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
builtinConId
  , 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 (f :: * -> *). Applicative f => Bool -> f () -> f ()
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