module Agda.TypeChecking.Monad.Builtin
( module Agda.TypeChecking.Monad.Builtin
, module Agda.Syntax.Builtin
) 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.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)) #-}
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)
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
litType
:: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
=> Literal -> m Type
litType :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Literal -> m Type
litType = \case
LitNat Integer
n -> do
_ <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primZero
when (n > 0) $ void $ primSuc
el <$> primNat
LitWord64 Word64
_ -> Term -> Type
forall {a}. a -> Type'' Term a
el (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primWord64
LitFloat Double
_ -> Term -> Type
forall {a}. a -> Type'' Term a
el (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFloat
LitChar Char
_ -> Term -> Type
forall {a}. a -> Type'' Term a
el (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primChar
LitString Text
_ -> Term -> Type
forall {a}. a -> Type'' Term a
el (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primString
LitQName QName
_ -> Term -> Type
forall {a}. a -> Type'' Term a
el (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQName
LitMeta TopLevelModuleName' Range
_ MetaId
_ -> Term -> Type
forall {a}. a -> Type'' Term a
el (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaMeta
where
el :: a -> Type'' Term a
el a
t = Sort' Term -> a -> Type'' Term a
forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort' Term
mkType Integer
0) a
t
setBuiltinThings :: BuiltinThings 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
builtin <- SomeBuiltin -> TCMT IO (Maybe (Builtin PrimFun))
forall (m :: * -> *).
HasBuiltins m =>
SomeBuiltin -> m (Maybe (Builtin PrimFun))
getBuiltinThing SomeBuiltin
b'
case builtin of
Just (Builtin Term
y) -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ BuiltinId -> Term -> Term -> TypeError
DuplicateBuiltinBinding BuiltinId
b Term
y Term
x
Just Prim{} -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ TypeError
forall a. HasCallStack => a
__IMPOSSIBLE__
Just BuiltinRewriteRelations{} -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
Maybe (Builtin PrimFun)
Nothing -> (Map SomeBuiltin (Builtin PrimFun)
-> f (Map SomeBuiltin (Builtin PrimFun)))
-> TCState -> f TCState
Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
stLocalBuiltins Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
-> (Map SomeBuiltin (Builtin PrimFun)
-> Map SomeBuiltin (Builtin PrimFun))
-> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` SomeBuiltin
-> Builtin PrimFun
-> Map SomeBuiltin (Builtin PrimFun)
-> Map SomeBuiltin (Builtin PrimFun)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SomeBuiltin
b' (Term -> Builtin PrimFun
forall pf. Term -> Builtin pf
Builtin Term
x)
where b' :: SomeBuiltin
b' = BuiltinId -> SomeBuiltin
BuiltinName BuiltinId
b
bindPrimitive :: PrimitiveId -> PrimFun -> TCM ()
bindPrimitive :: PrimitiveId -> PrimFun -> TCM ()
bindPrimitive PrimitiveId
b PrimFun
pf = do
builtin <- SomeBuiltin -> TCMT IO (Maybe (Builtin PrimFun))
forall (m :: * -> *).
HasBuiltins m =>
SomeBuiltin -> m (Maybe (Builtin PrimFun))
getBuiltinThing SomeBuiltin
b'
case builtin of
Just (Builtin Term
_) -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ String -> TypeError
NoSuchPrimitiveFunction (PrimitiveId -> String
forall a. IsBuiltin a => a -> String
getBuiltinId PrimitiveId
b)
Just (Prim PrimFun
x) -> TypeError -> TCM ()
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ (PrimitiveId -> QName -> QName -> TypeError
DuplicatePrimitiveBinding PrimitiveId
b (QName -> QName -> TypeError)
-> (PrimFun -> QName) -> PrimFun -> PrimFun -> TypeError
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` PrimFun -> QName
primFunName) PrimFun
x PrimFun
pf
Just BuiltinRewriteRelations{} -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
Maybe (Builtin PrimFun)
Nothing -> (Map SomeBuiltin (Builtin PrimFun)
-> f (Map SomeBuiltin (Builtin PrimFun)))
-> TCState -> f TCState
Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
stLocalBuiltins Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
-> (Map SomeBuiltin (Builtin PrimFun)
-> Map SomeBuiltin (Builtin PrimFun))
-> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
Lens' TCState a -> (a -> a) -> m ()
`modifyTCLens` SomeBuiltin
-> Builtin PrimFun
-> Map SomeBuiltin (Builtin PrimFun)
-> Map SomeBuiltin (Builtin PrimFun)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert SomeBuiltin
b' (PrimFun -> Builtin PrimFun
forall pf. pf -> Builtin pf
Prim PrimFun
pf)
where b' :: SomeBuiltin
b' = PrimitiveId -> SomeBuiltin
PrimitiveName PrimitiveId
b
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)
getBuiltinRewriteRelations :: (HasBuiltins m, MonadTCError m) => m (Set QName)
getBuiltinRewriteRelations :: forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
m (Set QName)
getBuiltinRewriteRelations =
m (Set QName) -> m (Maybe (Set QName)) -> m (Set QName)
forall (m :: * -> *) a. Monad m => m a -> m (Maybe a) -> m a
fromMaybeM (TypeError -> m (Set QName)
forall (m :: * -> *) a.
(HasCallStack, MonadTCError m) =>
TypeError -> m a
typeError (TypeError -> m (Set QName)) -> TypeError -> m (Set QName)
forall a b. (a -> b) -> a -> b
$ BuiltinId -> TypeError
NoBindingForBuiltin BuiltinId
builtinRewrite) m (Maybe (Set QName))
forall (m :: * -> *). HasBuiltins m => m (Maybe (Set QName))
getBuiltinRewriteRelations'
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 :: (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)
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
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,
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,
primQName, primArgInfo, primArgArgInfo, primArg, primArgArg, primAbs, primAbsAbs, primAgdaTerm, primAgdaTermVar,
primAgdaTermLam, primAgdaTermExtLam, primAgdaTermDef, primAgdaTermCon, primAgdaTermPi,
primAgdaTermSort, primAgdaTermLit, primAgdaTermUnsupported, primAgdaTermMeta,
primAgdaErrorPart, primAgdaErrorPartString, primAgdaErrorPartTerm, primAgdaErrorPartPatt, primAgdaErrorPartName,
primHiding, primHidden, primInstance, primVisible,
primRelevance, primRelevant, primIrrelevant,
primQuantity, primQuantity0, primQuantityω,
primModality, primModalityConstructor,
primAssoc, primAssocLeft, primAssocRight, primAssocNon,
primPrecedence, primPrecRelated, primPrecUnrelated,
primFixity, primFixityFixity,
primAgdaLiteral, primAgdaLitNat, primAgdaLitWord64, primAgdaLitFloat, primAgdaLitString, primAgdaLitChar, primAgdaLitQName, primAgdaLitMeta,
primAgdaSort, primAgdaSortSet, primAgdaSortLit, primAgdaSortProp, primAgdaSortPropLit, primAgdaSortInf, primAgdaSortUnsupported,
primAgdaDefinition, primAgdaDefinitionFunDef, primAgdaDefinitionDataDef, primAgdaDefinitionRecordDef,
primAgdaDefinitionPostulate, primAgdaDefinitionPrimitive, primAgdaDefinitionDataConstructor,
primAgdaClause, primAgdaClauseClause, primAgdaClauseAbsurd,
primAgdaPattern, primAgdaPatCon, primAgdaPatVar, primAgdaPatDot,
primAgdaPatLit, primAgdaPatProj,
primAgdaPatAbsurd,
primAgdaMeta,
primAgdaBlocker, primAgdaBlockerAny, primAgdaBlockerAll, primAgdaBlockerMeta,
primAgdaTCM, primAgdaTCMReturn, primAgdaTCMBind, primAgdaTCMUnify,
primAgdaTCMTypeError, primAgdaTCMInferType, primAgdaTCMCheckType,
primAgdaTCMNormalise, primAgdaTCMReduce,
primAgdaTCMCatchError, primAgdaTCMGetContext, primAgdaTCMExtendContext, primAgdaTCMInContext,
primAgdaTCMFreshName, primAgdaTCMDeclareDef, primAgdaTCMDeclarePostulate, primAgdaTCMDeclareData, primAgdaTCMDefineData, primAgdaTCMDefineFun,
primAgdaTCMGetType, primAgdaTCMGetDefinition,
primAgdaTCMQuoteTerm, primAgdaTCMUnquoteTerm, primAgdaTCMQuoteOmegaTerm,
primAgdaTCMCommit, primAgdaTCMIsMacro, primAgdaTCMBlock,
primAgdaTCMFormatErrorParts, primAgdaTCMDebugPrint,
primAgdaTCMWithNormalisation, primAgdaTCMWithReconstructed,
primAgdaTCMWithExpandLast, primAgdaTCMWithReduceDefs,
primAgdaTCMAskNormalisation, primAgdaTCMAskReconstructed,
primAgdaTCMAskExpandLast, primAgdaTCMAskReduceDefs,
primAgdaTCMNoConstraints,
primAgdaTCMWorkOnTypes,
primAgdaTCMRunSpeculative,
primAgdaTCMExec,
primAgdaTCMGetInstances,
primAgdaTCMSolveInstances,
primAgdaTCMPragmaForeign,
primAgdaTCMPragmaCompile
:: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term
primInteger :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInteger = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinInteger
primIntegerPos :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIntegerPos = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinIntegerPos
primIntegerNegSuc :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIntegerNegSuc = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinIntegerNegSuc
primFloat :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFloat = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinFloat
primChar :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primChar = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinChar
primString :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primString = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinString
primBool :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primBool = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinBool
primSigma :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSigma = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinSigma
primUnit :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinUnit
primUnitUnit :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnitUnit = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinUnitUnit
primTrue :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrue = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinTrue
primFalse :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFalse = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinFalse
primList :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primList = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinList
primNil :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNil = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinNil
primCons :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primCons = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinCons
primMaybe :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primMaybe = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinMaybe
primNothing :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNothing = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinNothing
primJust :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primJust = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinJust
primIO :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIO = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinIO
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
primAgdaTCMWorkOnTypes :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMWorkOnTypes = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMWorkOnTypes
primAgdaTCMRunSpeculative :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMRunSpeculative = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMRunSpeculative
primAgdaTCMExec :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMExec = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMExec
primAgdaTCMGetInstances :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMGetInstances = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMGetInstances
primAgdaTCMSolveInstances :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMSolveInstances = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMSolveInstances
primAgdaTCMPragmaForeign :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMPragmaForeign = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMPragmaForeign
primAgdaTCMPragmaCompile :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMPragmaCompile = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMPragmaCompile
data CoinductionKit = CoinductionKit
{ CoinductionKit -> QName
nameOfInf :: QName
, CoinductionKit -> QName
nameOfSharp :: QName
, CoinductionKit -> QName
nameOfFlat :: QName
}
coinductionKit' :: TCM CoinductionKit
coinductionKit' :: TCM CoinductionKit
coinductionKit' = do
Def inf _ <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInf
Def sharp _ <- primSharp
Def flat _ <- primFlat
return $ CoinductionKit
{ nameOfInf = inf
, nameOfSharp = sharp
, nameOfFlat = flat
}
coinductionKit :: TCM (Maybe CoinductionKit)
coinductionKit :: TCM (Maybe CoinductionKit)
coinductionKit = TCM CoinductionKit -> TCM (Maybe CoinductionKit)
forall e (m :: * -> *) a.
(MonadError e m, Functor m) =>
m a -> m (Maybe a)
tryMaybe TCM CoinductionKit
coinductionKit'
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
}
sortKit :: (HasBuiltins m, MonadTCError m, HasOptions m) => m SortKit
sortKit :: forall (m :: * -> *).
(HasBuiltins m, MonadTCError m, HasOptions m) =>
m SortKit
sortKit = do
Def prop _ <- BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinProp
Def set _ <- getBuiltin builtinSet
Def sset _ <- getBuiltin builtinStrictSet
Def propomega _ <- getBuiltin builtinPropOmega
Def setomega _ <- getBuiltin builtinSetOmega
Def ssetomega _ <- getBuiltin builtinSSetOmega
return $ mkSortKit prop set sset propomega setomega ssetomega
infallibleSortKit :: HasBuiltins m => m SortKit
infallibleSortKit :: forall (m :: * -> *). HasBuiltins m => m SortKit
infallibleSortKit = do
Def prop _ <- 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 set _ <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSet
Def sset _ <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinStrictSet
Def propomega _ <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinPropOmega
Def setomega _ <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSetOmega
Def ssetomega _ <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSSetOmega
return $ mkSortKit prop set sset propomega setomega ssetomega
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
iz <- BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinIZero
io <- getBuiltinName' builtinIOne
imax <- getPrimitiveName' builtinIMax
imin <- getPrimitiveName' builtinIMin
ineg <- getPrimitiveName' builtinINeg
return $ \ Term
t ->
case Term
t of
Def QName
q Elims
es ->
case Elims
es of
[Apply Arg Term
x,Apply Arg Term
y] | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
imin -> Arg Term -> Arg Term -> IntervalView
IMin Arg Term
x Arg Term
y
[Apply Arg Term
x,Apply Arg Term
y] | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
imax -> Arg Term -> Arg Term -> IntervalView
IMax Arg Term
x Arg Term
y
[Apply Arg Term
x] | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
q Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
ineg -> Arg Term -> IntervalView
INeg Arg Term
x
Elims
_ -> Term -> IntervalView
OTerm Term
t
Con ConHead
q ConInfo
_ [] | QName -> Maybe QName
forall a. a -> Maybe a
Just (ConHead -> QName
conName ConHead
q) Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
iz -> IntervalView
IZero
| QName -> Maybe QName
forall a. a -> Maybe a
Just (ConHead -> QName
conName ConHead
q) Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
io -> IntervalView
IOne
Term
_ -> Term -> IntervalView
OTerm Term
t
{-# INLINE intervalView #-}
intervalView :: HasBuiltins m => Term -> m IntervalView
intervalView :: forall (m :: * -> *). HasBuiltins m => Term -> m IntervalView
intervalView Term
t = do
f <- m (Term -> IntervalView)
forall (m :: * -> *). HasBuiltins m => m (Term -> IntervalView)
intervalView'
return (f t)
intervalUnview :: HasBuiltins m => IntervalView -> m Term
intervalUnview :: forall (m :: * -> *). HasBuiltins m => IntervalView -> m Term
intervalUnview IntervalView
t = do
f <- m (IntervalView -> Term)
forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview'
return (f t)
{-# SPECIALIZE intervalUnview' :: TCM (IntervalView -> Term) #-}
intervalUnview' :: HasBuiltins m => m (IntervalView -> Term)
intervalUnview' :: forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview' = do
iz <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinIZero
io <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinIOne
imin <- (`Def` []) . fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' builtinIMin
imax <- (`Def` []) . fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' builtinIMax
ineg <- (`Def` []) . fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' builtinINeg
return $ \ IntervalView
v -> case IntervalView
v of
IntervalView
IZero -> Term
iz
IntervalView
IOne -> Term
io
IMin Arg Term
x Arg Term
y -> Term -> Args -> Term
forall t. Apply t => t -> Args -> t
apply Term
imin [Arg Term
x,Arg Term
y]
IMax Arg Term
x Arg Term
y -> Term -> Args -> Term
forall t. Apply t => t -> Args -> t
apply Term
imax [Arg Term
x,Arg Term
y]
INeg Arg Term
x -> Term -> Args -> Term
forall t. Apply t => t -> Args -> t
apply Term
ineg [Arg Term
x]
OTerm Term
t -> Term
t
{-# INLINE pathView #-}
pathView :: HasBuiltins m => Type -> m PathView
pathView :: forall (m :: * -> *). HasBuiltins m => Type -> m PathView
pathView Type
t0 = do
view <- m (Type -> PathView)
forall (m :: * -> *). HasBuiltins m => m (Type -> PathView)
pathView'
return $ view t0
{-# SPECIALIZE pathView' :: TCM (Type -> PathView) #-}
pathView' :: HasBuiltins m => m (Type -> PathView)
pathView' :: forall (m :: * -> *). HasBuiltins m => m (Type -> PathView)
pathView' = do
mpath <- BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinPath
mpathp <- getBuiltinName' builtinPathP
return $ \ t0 :: Type
t0@(El Sort' Term
s Term
t) ->
case Term
t of
Def QName
path' [ Apply Arg Term
level , Apply Arg Term
typ , Apply Arg Term
lhs , Apply Arg Term
rhs ]
| QName -> Maybe QName
forall a. a -> Maybe a
Just QName
path' Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mpath, Just QName
path <- Maybe QName
mpathp -> Sort' Term
-> QName
-> Arg Term
-> Arg Term
-> Arg Term
-> Arg Term
-> PathView
PathType Sort' Term
s QName
path Arg Term
level (KillRangeT Term
lam_i KillRangeT Term -> Arg Term -> Arg Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Arg Term
typ) Arg Term
lhs Arg Term
rhs
where lam_i :: KillRangeT Term
lam_i = ArgInfo -> Abs Term -> Term
Lam ArgInfo
defaultArgInfo (Abs Term -> Term) -> (Term -> Abs Term) -> KillRangeT Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Term -> Abs Term
forall a. String -> a -> Abs a
NoAbs String
"_"
Def QName
path' [ Apply Arg Term
level , Apply Arg Term
typ , Apply Arg Term
lhs , Apply Arg Term
rhs ]
| QName -> Maybe QName
forall a. a -> Maybe a
Just QName
path' Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
mpathp, Just QName
path <- Maybe QName
mpathp -> Sort' Term
-> QName
-> Arg Term
-> Arg Term
-> Arg Term
-> Arg Term
-> PathView
PathType Sort' Term
s QName
path Arg Term
level Arg Term
typ Arg Term
lhs Arg Term
rhs
Term
_ -> Type -> PathView
OType Type
t0
{-# SPECIALIZE idViewAsPath :: Type -> TCM PathView #-}
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
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
mpath <- fmap getPrimName <$> getBuiltin' builtinPath
case 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
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]
{-# INLINABLE conidView' #-}
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
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]
mio <- getTerm' builtinIOne
let fallback = (t -> t -> Maybe a) -> m (t -> t -> Maybe a)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((t -> t -> Maybe a) -> m (t -> t -> Maybe a))
-> (t -> t -> Maybe a) -> m (t -> t -> Maybe a)
forall a b. (a -> b) -> a -> b
$ \ t
_ t
_ -> Maybe a
forall a. Maybe a
Nothing
caseMaybe mn fallback $ \ [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 {t} {t} {a}. m (t -> t -> 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
primEqualityName :: TCM QName
primEqualityName :: TCM QName
primEqualityName = do
eq <- TCMT IO Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primEquality
let 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)
return $ case lamV eq of
([Hiding]
_, Def QName
equality Elims
_) -> QName
equality
([Hiding], Term)
_ -> QName
forall a. HasCallStack => a
__IMPOSSIBLE__
equalityView :: Type -> TCM EqualityView
equalityView :: Type -> TCM EqualityView
equalityView t0 :: Type
t0@(El Sort' Term
s Term
t) = do
equality <- TCM QName
primEqualityName
case t of
Def QName
equality' Elims
es | QName
equality' QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
equality -> do
let vs :: Args
vs = Args -> Maybe Args -> Args
forall a. a -> Maybe a -> a
fromMaybe Args
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Args -> Args) -> Maybe Args -> Args
forall a b. (a -> b) -> a -> b
$ Elims -> Maybe Args
forall a. [Elim' a] -> Maybe [Arg a]
allApplyElims Elims
es
let n :: Int
n = Args -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Args
vs
Bool -> TCM () -> TCM ()
forall (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
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])
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