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

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

import Data.Function ( on )
import Data.Map qualified as Map
import Data.Set (Set)
import Data.Text.Short (ShortText)

import Mikan.Syntax.Common
import Mikan.Syntax.Position
import Mikan.Syntax.Literal
import Mikan.Syntax.Builtin
import Mikan.Syntax.Internal.Generic
import Mikan.Syntax.Internal as I

import Mikan.TypeChecking.Monad.Diagnostic
import Mikan.TypeChecking.Free.Generic
import Mikan.TypeChecking.Monad.Base
import Mikan.TypeChecking.Substitute

import Mikan.Utils.ExpandCase
import Mikan.Utils.Functor
import Mikan.Utils.Lens
import Mikan.Utils.ListT
import Mikan.Utils.Monad
import Mikan.Utils.Maybe
import Mikan.Utils.Singleton
import Mikan.Utils.Tuple
import Mikan.Utils.Update

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

import Mikan.Utils.Impossible

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

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

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

deriving instance HasBuiltins m => HasBuiltins (BlockT m)

instance MonadIO m => HasBuiltins (TCMT m) where
  getBuiltinThing :: SomeBuiltin -> TCMT m (Maybe (Builtin PrimFun))
getBuiltinThing SomeBuiltin
b =
    (Maybe (Builtin PrimFun)
 -> Maybe (Builtin PrimFun) -> Maybe (Builtin PrimFun))
-> TCMT m (Maybe (Builtin PrimFun))
-> TCMT m (Maybe (Builtin PrimFun))
-> TCMT m (Maybe (Builtin PrimFun))
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Maybe (Builtin PrimFun)
-> Maybe (Builtin PrimFun) -> Maybe (Builtin PrimFun)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>)
      (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
<$> Getter TCState (Map SomeBuiltin (Builtin PrimFun))
-> TCMT m (Map SomeBuiltin (Builtin PrimFun))
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC (Map SomeBuiltin (Builtin PrimFun)
 -> f (Map SomeBuiltin (Builtin PrimFun)))
-> TCState -> f TCState
Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
Getter 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
<$> Getter TCState (Map SomeBuiltin (Builtin PrimFun))
-> TCMT m (Map SomeBuiltin (Builtin PrimFun))
forall (m :: * -> *) a. ReadTCState m => Getter TCState a -> m a
useTC (Map SomeBuiltin (Builtin PrimFun)
 -> f (Map SomeBuiltin (Builtin PrimFun)))
-> TCState -> f TCState
Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
Getter TCState (Map SomeBuiltin (Builtin PrimFun))
stImportedBuiltins)
{-# SPECIALIZE getBuiltinThing :: SomeBuiltin -> TCM (Maybe (Builtin PrimFun)) #-}


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

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

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

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


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

litType
  :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m)
  => Literal -> m Type
litType :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
Literal -> m Type
litType = \case
  LitNat Integer
n    -> do
    _ <- m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primZero
    when (n > 0) $ void $ primSuc
    el <$> primNat
  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 ShortText
_ -> Term -> Type
forall {a}. a -> Type'' Term a
el (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primString
  LitQName QName
_  -> Term -> Type
forall {a}. a -> Type'' Term a
el (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primQName
  LitMeta TopLevelModuleName' Range
_ MetaId
_ -> Term -> Type
forall {a}. a -> Type'' Term a
el (Term -> Type) -> m Term -> m Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaMeta
  where
    el :: a -> Type'' Term a
el a
t = Sort' Term -> a -> Type'' Term a
forall t a. Sort' t -> a -> Type'' t a
El (Integer -> Sort' Term
mkType Integer
0) a
t

setBuiltinThings :: BuiltinThings -> TCM ()
setBuiltinThings :: Map SomeBuiltin (Builtin PrimFun) -> TCM ()
setBuiltinThings Map SomeBuiltin (Builtin PrimFun)
b = (Map SomeBuiltin (Builtin PrimFun)
 -> Identity (Map SomeBuiltin (Builtin PrimFun)))
-> TCState -> Identity TCState
Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
stLocalBuiltins ((Map SomeBuiltin (Builtin PrimFun)
  -> Identity (Map SomeBuiltin (Builtin PrimFun)))
 -> TCState -> Identity TCState)
-> Map SomeBuiltin (Builtin PrimFun) -> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' 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 :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> 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{}      -> TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
    Maybe (Builtin PrimFun)
Nothing          -> (Map SomeBuiltin (Builtin PrimFun)
 -> Identity (Map SomeBuiltin (Builtin PrimFun)))
-> TCState -> Identity TCState
Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
stLocalBuiltins ((Map SomeBuiltin (Builtin PrimFun)
  -> Identity (Map SomeBuiltin (Builtin PrimFun)))
 -> TCState -> Identity TCState)
-> (Map SomeBuiltin (Builtin PrimFun)
    -> Map SomeBuiltin (Builtin PrimFun))
-> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC` 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 :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> TCM ()) -> TypeError -> TCM ()
forall a b. (a -> b) -> a -> b
$ ShortText -> TypeError
NoSuchPrimitiveFunction (PrimitiveId -> ShortText
forall a. IsBuiltin a => a -> ShortText
getBuiltinId PrimitiveId
b)
    Just (Prim PrimFun
x)    -> TypeError -> TCM ()
forall (m :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> 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
    Maybe (Builtin PrimFun)
Nothing          -> (Map SomeBuiltin (Builtin PrimFun)
 -> Identity (Map SomeBuiltin (Builtin PrimFun)))
-> TCState -> Identity TCState
Lens' TCState (Map SomeBuiltin (Builtin PrimFun))
stLocalBuiltins ((Map SomeBuiltin (Builtin PrimFun)
  -> Identity (Map SomeBuiltin (Builtin PrimFun)))
 -> TCState -> Identity TCState)
-> (Map SomeBuiltin (Builtin PrimFun)
    -> Map SomeBuiltin (Builtin PrimFun))
-> TCM ()
forall (m :: * -> *) a.
MonadTCState m =>
ASetter' TCState a -> (a -> a) -> m ()
`modifyingTC` 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

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

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

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

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

{-# 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 :: * -> *) e a.
(HasCallStack, MonadTCError m, Diagnostic e) =>
e -> m a
typeError (TypeError -> m PrimFun)
-> (ShortText -> TypeError) -> ShortText -> m PrimFun
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShortText -> TypeError
NoSuchPrimitiveFunction (ShortText -> m PrimFun) -> ShortText -> m PrimFun
forall a b. (a -> b) -> a -> b
$ PrimitiveId -> ShortText
forall a. IsBuiltin a => a -> ShortText
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

-- [TODO: Reed M, 23/05/2026] This should probably take lazy text?
-- | @getTerm use name@ looks up @name@ as a primitive or builtin, and
-- throws an error otherwise.
-- The @use@ argument describes how the name is used for the sake of
-- the error message.
getTerm :: (HasBuiltins m, IsBuiltin a) => ShortText -> a -> m Term
getTerm :: forall (m :: * -> *) a.
(HasBuiltins m, IsBuiltin a) =>
ShortText -> a -> m Term
getTerm ShortText
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 ([ShortText] -> ShortText -> Impossible
ImpMissingDefinitions [a -> ShortText
forall a. IsBuiltin a => a -> ShortText
getBuiltinId a
name] ShortText
use)


-- | Rewrite a literal to constructor form if possible.
constructorForm :: HasBuiltins m => Term -> m Term
constructorForm :: forall (m :: * -> *). HasBuiltins m => Term -> m Term
constructorForm Term
v = do
  let pZero :: m Term
pZero = Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinZero
      pSuc :: m Term
pSuc  = Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinSuc
  -- By passing the builtins lazily we do not have to look them up if @v@ is not a 'LitNat'.
  m Term -> m Term -> Term -> m Term
forall (m :: * -> *).
Applicative m =>
m Term -> m Term -> Term -> m Term
constructorForm' m Term
pZero m Term
pSuc Term
v

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

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

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

primInteger, primIntegerPos, primIntegerNegSuc,
    primFloat, primChar, primString, primUnit, primUnitUnit, primBool, primTrue, primFalse,
    primSigma,
    primList, primNil, primCons, primNat, primSuc, primZero, primMaybe, primNothing, primJust,
    primPath, primPathP, primIntervalUniv, primInterval, primIZero, primIOne, primPartial, primPartialP,
    primIMin, primIMax, primINeg,
    primIsOne, primItIsOne, primIsOne1, primIsOne2, primIsOneEmpty,
    primSub, primSubIn, primSubOut,
    primTrans, primHComp,
    primEquiv, primEquivFun, primEquivProof,
    primTranspProof,
    primGlue, prim_glue, prim_unglue,
    prim_glueU, prim_unglueU,
    primFaceForall,
    primNatPlus, primNatMinus, primNatTimes, primNatDivSucAux, primNatModSucAux,
    primNatEquality, primNatLess,
    -- Machine words
    primEquality, primRefl,
    primLevel, primLevelZero, primLevelSuc, primLevelMax,
    primLevelUniv,
    primProp, primType, primStrictSet, primPropOmega, primTypeOmega, primSSetOmega,
    primFromNat, primFromNeg, primFromString,
    -- builtins for reflection:
    primQName, primArgInfo, primArgArgInfo, primArg, primArgArg, primAbs, primAbsAbs, primAgdaTerm, primAgdaTermVar,
    primAgdaTermLam, primAgdaTermExtLam, primAgdaTermDef, primAgdaTermCon, primAgdaTermPi,
    primAgdaTermSort, primAgdaTermLit, primAgdaTermUnsupported, primAgdaTermMeta,
    primAgdaErrorPart, primAgdaErrorPartString, primAgdaErrorPartTerm, primAgdaErrorPartPatt, primAgdaErrorPartName,
    primHiding, primHidden, primInstance, primVisible,
    primAssoc, primAssocLeft, primAssocRight, primAssocNon,
    primPrecedence, primPrecRelated, primPrecUnrelated,
    primFixity, primFixityFixity,
    primAgdaLiteral, primAgdaLitNat, primAgdaLitFloat, primAgdaLitString, primAgdaLitChar, primAgdaLitQName, primAgdaLitMeta,
    primAgdaSort, primAgdaSortType, primAgdaSortLit, primAgdaSortProp, primAgdaSortPropLit, primAgdaSortInf, primAgdaSortUnsupported,
    primAgdaDefinition, primAgdaDefinitionFunDef, primAgdaDefinitionDataDef, primAgdaDefinitionRecordDef,
    primAgdaDefinitionPostulate, primAgdaDefinitionPrimitive, primAgdaDefinitionDataConstructor,
    primAgdaClause, primAgdaClauseClause, primAgdaClauseAbsurd,
    primAgdaPattern, primAgdaPatCon, primAgdaPatVar, primAgdaPatDot,
    primAgdaPatLit, primAgdaPatProj,
    primAgdaPatAbsurd,
    primAgdaMeta,
    primAgdaBlocker, primAgdaBlockerAny, primAgdaBlockerAll, primAgdaBlockerMeta,
    primAgdaTCM, primAgdaTCMReturn, primAgdaTCMBind, primAgdaTCMUnify,
    primAgdaTCMTypeError, primAgdaTCMInferType, primAgdaTCMCheckType,
    primAgdaTCMNormalise, primAgdaTCMReduce,
    primAgdaTCMCatchError, primAgdaTCMGetContext, primAgdaTCMExtendContext, primAgdaTCMInContext,
    primAgdaTCMFreshName, primAgdaTCMDeclareDef, primAgdaTCMDeclarePostulate, primAgdaTCMDeclareData, primAgdaTCMDefineData, primAgdaTCMDefineFun,
    primAgdaTCMGetType, primAgdaTCMGetDefinition,
    primAgdaTCMQuoteTerm, primAgdaTCMUnquoteTerm, primAgdaTCMQuoteOmegaTerm,
    primAgdaTCMCommit, primAgdaTCMIsMacro, primAgdaTCMBlock,
    primAgdaTCMFormatErrorParts, primAgdaTCMDebugPrint,
    primAgdaTCMWithNormalisation, primAgdaTCMWithReconstructed,
    primAgdaTCMWithExpandLast, primAgdaTCMWithReduceDefs,
    primAgdaTCMAskNormalisation, primAgdaTCMAskReconstructed,
    primAgdaTCMAskExpandLast, primAgdaTCMAskReduceDefs,
    primAgdaTCMNoConstraints,
    primAgdaTCMRunSpeculative,
    primAgdaTCMExec,
    primAgdaTCMCheckFromString,
    primAgdaTCMGetInstances,
    primAgdaTCMSolveInstances,
    primAgdaTCMPragmaForeign,
    primAgdaTCMPragmaCompile
    :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m Term

primInteger :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primInteger                           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinInteger
primIntegerPos :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIntegerPos                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinIntegerPos
primIntegerNegSuc :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primIntegerNegSuc                     = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinIntegerNegSuc
primFloat :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFloat                             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinFloat
primChar :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primChar                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinChar
primString :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primString                            = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinString
primBool :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primBool                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinBool
primSigma :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primSigma                             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinSigma
primUnit :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnit                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinUnit
primUnitUnit :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primUnitUnit                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinUnitUnit
primTrue :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTrue                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinTrue
primFalse :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primFalse                             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinFalse
primList :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primList                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinList
primNil :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNil                               = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinNil
primCons :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primCons                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinCons
primMaybe :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primMaybe                             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinMaybe
primNothing :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primNothing                           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinNothing
primJust :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primJust                              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinJust
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                           = KillRangeT Term
dontCare KillRangeT Term -> m Term -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
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
primType :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primType                               = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinType
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
primTypeOmega :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primTypeOmega                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinTypeOmega
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
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
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
primAgdaSortType :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaSortType                      = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaSortType
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
primAgdaLitFloat :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitFloat                      = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaLitFloat
primAgdaLitChar :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitChar                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaLitChar
primAgdaLitString :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitString                     = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaLitString
primAgdaLitQName :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitQName                      = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaLitQName
primAgdaLitMeta :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaLitMeta                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaLitMeta
primAgdaPattern :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPattern                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaPattern
primAgdaPatCon :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatCon                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaPatCon
primAgdaPatVar :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatVar                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaPatVar
primAgdaPatDot :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatDot                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaPatDot
primAgdaPatLit :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatLit                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaPatLit
primAgdaPatProj :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatProj                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaPatProj
primAgdaPatAbsurd :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaPatAbsurd                     = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaPatAbsurd
primAgdaClause :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaClause                        = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaClause
primAgdaClauseClause :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaClauseClause                  = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaClauseClause
primAgdaClauseAbsurd :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaClauseAbsurd                  = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaClauseAbsurd
primAgdaDefinitionFunDef :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionFunDef              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaDefinitionFunDef
primAgdaDefinitionDataDef :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionDataDef             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaDefinitionDataDef
primAgdaDefinitionRecordDef :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionRecordDef           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaDefinitionRecordDef
primAgdaDefinitionDataConstructor :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionDataConstructor     = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaDefinitionDataConstructor
primAgdaDefinitionPostulate :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionPostulate           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaDefinitionPostulate
primAgdaDefinitionPrimitive :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinitionPrimitive           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaDefinitionPrimitive
primAgdaDefinition :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaDefinition                    = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaDefinition
primAgdaMeta :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaMeta                          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaMeta
primAgdaTCM :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCM                           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCM
primAgdaTCMReturn :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMReturn                     = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMReturn
primAgdaTCMBind :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMBind                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMBind
primAgdaTCMUnify :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMUnify                      = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMUnify
primAgdaTCMTypeError :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMTypeError                  = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMTypeError
primAgdaTCMInferType :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMInferType                  = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMInferType
primAgdaTCMCheckType :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMCheckType                  = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMCheckType
primAgdaTCMNormalise :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMNormalise                  = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMNormalise
primAgdaTCMReduce :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMReduce                     = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMReduce
primAgdaTCMCatchError :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMCatchError                 = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMCatchError
primAgdaTCMGetContext :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMGetContext                 = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMGetContext
primAgdaTCMExtendContext :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMExtendContext              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMExtendContext
primAgdaTCMInContext :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMInContext                  = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMInContext
primAgdaTCMFreshName :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMFreshName                  = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMFreshName
primAgdaTCMDeclareDef :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDeclareDef                 = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMDeclareDef
primAgdaTCMDeclarePostulate :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDeclarePostulate           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMDeclarePostulate
primAgdaTCMDeclareData :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDeclareData                = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMDeclareData
primAgdaTCMDefineData :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDefineData                 = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMDefineData
primAgdaTCMDefineFun :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDefineFun                  = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMDefineFun
primAgdaTCMGetType :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMGetType                    = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMGetType
primAgdaTCMGetDefinition :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMGetDefinition              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMGetDefinition
primAgdaTCMQuoteTerm :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMQuoteTerm                  = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMQuoteTerm
primAgdaTCMQuoteOmegaTerm :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMQuoteOmegaTerm             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMQuoteOmegaTerm
primAgdaTCMUnquoteTerm :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMUnquoteTerm                = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMUnquoteTerm
primAgdaTCMBlock :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMBlock                      = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMBlock
primAgdaTCMCommit :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMCommit                     = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMCommit
primAgdaTCMIsMacro :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMIsMacro                    = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMIsMacro
primAgdaTCMWithNormalisation :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMWithNormalisation          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMWithNormalisation
primAgdaTCMWithReconstructed :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMWithReconstructed          = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMWithReconstructed
primAgdaTCMWithExpandLast :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMWithExpandLast             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMWithExpandLast
primAgdaTCMWithReduceDefs :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMWithReduceDefs             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMWithReduceDefs
primAgdaTCMAskNormalisation :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMAskNormalisation           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMAskNormalisation
primAgdaTCMAskReconstructed :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMAskReconstructed           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMAskReconstructed
primAgdaTCMAskExpandLast :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMAskExpandLast              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMAskExpandLast
primAgdaTCMAskReduceDefs :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMAskReduceDefs              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMAskReduceDefs
primAgdaTCMFormatErrorParts :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMFormatErrorParts           = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMFormatErrorParts
primAgdaTCMDebugPrint :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMDebugPrint                 = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMDebugPrint
primAgdaTCMNoConstraints :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMNoConstraints              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMNoConstraints
primAgdaTCMRunSpeculative :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMRunSpeculative             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMRunSpeculative
primAgdaTCMExec :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMExec                       = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMExec
primAgdaTCMCheckFromString :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMCheckFromString            = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMCheckFromString
primAgdaTCMGetInstances :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMGetInstances               = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMGetInstances
primAgdaTCMSolveInstances :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMSolveInstances             = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMSolveInstances
primAgdaTCMPragmaForeign :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMPragmaForeign              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMPragmaForeign
primAgdaTCMPragmaCompile :: forall (m :: * -> *).
(HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) =>
m Term
primAgdaTCMPragmaCompile              = BuiltinId -> m Term
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m Term
getBuiltin BuiltinId
builtinAgdaTCMPragmaCompile

-- | Sort primitives.

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

mkSortKit :: QName -> QName -> QName -> QName -> QName -> QName -> SortKit
mkSortKit :: QName -> QName -> QName -> QName -> QName -> QName -> SortKit
mkSortKit QName
prop QName
type_ QName
sset QName
propomega QName
typeomega 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
type_
      (UnivSize
USmall , Univ
USSet) -> QName
sset
      (UnivSize
ULarge , Univ
UProp) -> QName
propomega
      (UnivSize
ULarge , Univ
UType) -> QName
typeomega
      (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
type_     -> (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
typeomega -> (UnivSize, Univ) -> Maybe (UnivSize, Univ)
forall a. a -> Maybe a
Just (UnivSize
ULarge , Univ
UType)
      | QName
x QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
ssetomega -> (UnivSize, Univ) -> Maybe (UnivSize, Univ)
forall a. a -> Maybe a
Just (UnivSize
ULarge , Univ
USSet)
      | Bool
otherwise -> Maybe (UnivSize, Univ)
forall a. Maybe a
Nothing
  }

-- | Compute a 'SortKit' in an environment that supports failures.
--
-- When 'optLoadPrimitives' is set to 'False', 'sortKit' is a fallible operation,
-- so for the uses of 'sortKit' in fallible contexts (e.g. 'TCM'),
-- we report a type error rather than exploding.
sortKit :: (HasBuiltins m, MonadTCError m) => m SortKit
sortKit :: forall (m :: * -> *). (HasBuiltins m, MonadTCError m) => m SortKit
sortKit = do
  prop      <- BuiltinId -> m QName
forall (m :: * -> *).
(HasBuiltins m, MonadTCError m) =>
BuiltinId -> m QName
getBuiltinName_ BuiltinId
builtinProp
  type_     <- getBuiltinName_ builtinType
  sset      <- getBuiltinName_ builtinStrictSet
  propomega <- getBuiltinName_ builtinPropOmega
  typeomega <- getBuiltinName_ builtinTypeOmega
  ssetomega <- getBuiltinName_ builtinSSetOmega
  return $ mkSortKit prop type_ sset propomega typeomega ssetomega

-- | Compute a 'SortKit' in contexts that do not support failure (e.g.
-- 'Reify'). This should only be used when we are sure that the
-- primitive sorts have been bound, i.e. because it is "after" type
-- checking.
infallibleSortKit :: HasBuiltins m => m SortKit
infallibleSortKit :: forall (m :: * -> *). HasBuiltins m => m SortKit
infallibleSortKit = do
  prop      <- QName -> Maybe QName -> QName
forall a. a -> Maybe a -> a
fromMaybe QName
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe QName -> QName) -> m (Maybe QName) -> m QName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe QName)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe QName)
getBuiltinName' BuiltinId
builtinProp
  type_     <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinType
  sset      <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinStrictSet
  propomega <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinPropOmega
  typeomega <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinTypeOmega
  ssetomega <- fromMaybe __IMPOSSIBLE__ <$> getBuiltinName' builtinSSetOmega
  return $ mkSortKit prop type_ sset propomega typeomega 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 b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
i Hiding -> [Hiding] -> [Hiding]
forall a. a -> [a] -> [a]
:) (([Hiding], Term) -> ([Hiding], Term))
-> ([Hiding], Term) -> ([Hiding], Term)
forall a b. (a -> b) -> a -> b
$ Term -> ([Hiding], Term)
lamV (Abs Term -> Term
forall a. Abs a -> a
unAbs Abs Term
b)
      lamV (Pi Dom Type
_ Abs Type
b)   = Term -> ([Hiding], Term)
lamV (Type -> Term
forall t a. Type'' t a -> a
unEl (Type -> Term) -> Type -> Term
forall a b. (a -> b) -> a -> b
$ Abs Type -> Type
forall a. Abs a -> a
unAbs Abs Type
b)
      lamV Term
v          = ([], Term
v)
  case Term -> ([Hiding], Term)
lamV Term
ty of
            ([Hiding]
_, Def QName
path Elims
_) -> QName
path
            ([Hiding]
_, Con ConHead
nm ConInfo
_ Elims
_)   -> ConHead -> QName
conName ConHead
nm
            ([Hiding]
_, Var Int
0 [Proj ProjOrigin
_ QName
l]) -> QName
l
            ([Hiding]
_, Term
t)          -> QName
forall a. HasCallStack => a
__IMPOSSIBLE__

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

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

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

------------------------------------------------------------------------
-- * Interval expressions
------------------------------------------------------------------------

data IntervalView
  = IZero
  | IOne
  | IMin (Arg Term) (Arg Term)
  | IMax (Arg Term) (Arg Term)
  | INeg (Arg Term)
  | OTerm Term
  deriving Int -> IntervalView -> ShowS
[IntervalView] -> ShowS
IntervalView -> String
(Int -> IntervalView -> ShowS)
-> (IntervalView -> String)
-> ([IntervalView] -> ShowS)
-> Show IntervalView
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IntervalView -> ShowS
showsPrec :: Int -> IntervalView -> ShowS
$cshow :: IntervalView -> String
show :: IntervalView -> String
$cshowList :: [IntervalView] -> ShowS
showList :: [IntervalView] -> ShowS
Show

isIOne :: IntervalView -> Bool
isIOne :: IntervalView -> Bool
isIOne IntervalView
IOne = Bool
True
isIOne IntervalView
_    = Bool
False

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 \case
    Def QName
q [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
      | 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
    Def QName
q [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
    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
t -> Term -> IntervalView
OTerm Term
t

{-# SPECIALIZE intervalUnview' :: TCM (IntervalView -> Term) #-}
{-# INLINABLE intervalUnview' #-}
intervalUnview' :: HasBuiltins m => m (IntervalView -> Term)
intervalUnview' :: forall (m :: * -> *). HasBuiltins m => m (IntervalView -> Term)
intervalUnview' = do
  iz <- Term -> Maybe Term -> Term
forall a. a -> Maybe a -> a
fromMaybe Term
forall a. HasCallStack => a
__IMPOSSIBLE__ (Maybe Term -> Term) -> m (Maybe Term) -> m Term
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> m (Maybe Term)
forall (m :: * -> *). HasBuiltins m => BuiltinId -> m (Maybe Term)
getBuiltin' BuiltinId
builtinIZero -- should it be a type error instead?
  io <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinIOne
  imin <- (`Def` []) . fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' builtinIMin
  imax <- (`Def` []) . fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' builtinIMax
  ineg <- (`Def` []) . fromMaybe __IMPOSSIBLE__ <$> getPrimitiveName' builtinINeg
  return $ \case
    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 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

{-# INLINE intervalUnview #-}
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

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

-- | View type as path type.
data PathView
  = PathType
    { PathView -> Sort' Term
pathSort  :: Sort     -- ^ Sort of this type.
    , PathView -> QName
pathName  :: QName    -- ^ Builtin PATH.
    , PathView -> Arg Term
pathLevel :: Arg Term -- ^ Hidden
    , PathView -> Arg Term
pathType  :: Arg Term -- ^ Hidden
    , PathView -> Arg Term
pathLhs   :: Arg Term -- ^ NotHidden
    , PathView -> Arg Term
pathRhs   :: Arg Term -- ^ NotHidden
    }
  | OType Type -- ^ reduced

isPathType :: PathView -> Bool
isPathType :: PathView -> Bool
isPathType PathType{} = Bool
True
isPathType OType{}    = Bool
False

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

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

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

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

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

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

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

-- | View type as equality type.

data EqualityView
  = EqualityViewType EqualityTypeData
      -- ^ A type of the form @u ≡ v@ decomposed into its parts.
      --   Used as type for the @rewrite@ expression.
  | OtherType Type
      -- ^ A reduced type used as type for a @with@ expression.
  | IdiomType Type
      -- ^ A reduced type used as type for the @with@ inspect idiom.

data EqualityTypeData = EqualityTypeData
    { EqualityTypeData -> Range
_eqtRange  :: Range       -- ^ Range of the @rewrite@ expression, if any.
    , EqualityTypeData -> Sort' Term
_eqtSort   :: Sort        -- ^ Sort of this type.
    , EqualityTypeData -> QName
_eqtName   :: QName       -- ^ Builtin EQUALITY.
    , EqualityTypeData -> Args
_eqtParams :: Args        -- ^ Hidden.  Empty or @Level@.
    , EqualityTypeData -> Arg Term
_eqtType   :: Arg Term    -- ^ Hidden.
    , EqualityTypeData -> Arg Term
_eqtLhs    :: Arg Term    -- ^ NotHidden.
    , EqualityTypeData -> Arg Term
_eqtRhs    :: Arg Term    -- ^ NotHidden.
    }

pattern EqualityType ::
     Range
  -> Sort
  -> QName
  -> Args
  -> Arg Term
  -> Arg Term
  -> Arg Term
  -> EqualityView
pattern $bEqualityType :: Range
-> Sort' Term
-> QName
-> Args
-> Arg Term
-> Arg Term
-> Arg Term
-> EqualityView
$mEqualityType :: forall {r}.
EqualityView
-> (Range
    -> Sort' Term
    -> QName
    -> Args
    -> Arg Term
    -> Arg Term
    -> Arg Term
    -> r)
-> ((# #) -> r)
-> r
EqualityType{ EqualityView -> Range
eqtRange, EqualityView -> Sort' Term
eqtSort, EqualityView -> QName
eqtName, EqualityView -> Args
eqtParams, EqualityView -> Arg Term
eqtType, EqualityView -> Arg Term
eqtLhs, EqualityView -> Arg Term
eqtRhs } =
  EqualityViewType (EqualityTypeData eqtRange eqtSort eqtName eqtParams eqtType eqtLhs eqtRhs)

{-# COMPLETE EqualityType, OtherType, IdiomType #-}

isEqualityType :: EqualityView -> Bool
isEqualityType :: EqualityView -> Bool
isEqualityType EqualityType{} = Bool
True
isEqualityType OtherType{}    = Bool
False
isEqualityType IdiomType{}    = Bool
False

instance TermLike EqualityView where
  traverseTermM :: forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> EqualityView -> m EqualityView
traverseTermM Term -> m Term
f = \case
    OtherType Type
t -> Type -> EqualityView
OtherType
      (Type -> EqualityView) -> m Type -> m EqualityView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> m Term) -> Type -> m Type
forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
forall (m :: * -> *). Monad m => (Term -> m Term) -> Type -> m Type
traverseTermM Term -> m Term
f Type
t
    IdiomType Type
t -> Type -> EqualityView
IdiomType
      (Type -> EqualityView) -> m Type -> m EqualityView
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term -> m Term) -> Type -> m Type
forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
forall (m :: * -> *). Monad m => (Term -> m Term) -> Type -> m Type
traverseTermM Term -> m Term
f Type
t
    EqualityType Range
r Sort' Term
s QName
eq Args
l Arg Term
t Arg Term
a Arg Term
b -> Range
-> Sort' Term
-> QName
-> Args
-> Arg Term
-> Arg Term
-> Arg Term
-> EqualityView
EqualityType Range
r Sort' Term
s QName
eq
      (Args -> Arg Term -> Arg Term -> Arg Term -> EqualityView)
-> m Args -> m (Arg Term -> Arg Term -> Arg Term -> EqualityView)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Arg Term -> m (Arg Term)) -> Args -> m Args
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse ((Term -> m Term) -> Arg Term -> m (Arg Term)
forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Arg Term -> m (Arg Term)
traverseTermM Term -> m Term
f) Args
l
      m (Arg Term -> Arg Term -> Arg Term -> EqualityView)
-> m (Arg Term) -> m (Arg Term -> Arg Term -> EqualityView)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term -> m Term) -> Arg Term -> m (Arg Term)
forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Arg Term -> m (Arg Term)
traverseTermM Term -> m Term
f Arg Term
t
      m (Arg Term -> Arg Term -> EqualityView)
-> m (Arg Term) -> m (Arg Term -> EqualityView)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term -> m Term) -> Arg Term -> m (Arg Term)
forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Arg Term -> m (Arg Term)
traverseTermM Term -> m Term
f Arg Term
a
      m (Arg Term -> EqualityView) -> m (Arg Term) -> m EqualityView
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Term -> m Term) -> Arg Term -> m (Arg Term)
forall a (m :: * -> *).
(TermLike a, Monad m) =>
(Term -> m Term) -> a -> m a
forall (m :: * -> *).
Monad m =>
(Term -> m Term) -> Arg Term -> m (Arg Term)
traverseTermM Term -> m Term
f Arg Term
b

  foldTerm :: forall m. Monoid m => (Term -> m) -> EqualityView -> m
foldTerm Term -> m
f = \case
    OtherType Type
t -> (Term -> m) -> Type -> m
forall m. Monoid m => (Term -> m) -> Type -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Type
t
    IdiomType Type
t -> (Term -> m) -> Type -> m
forall m. Monoid m => (Term -> m) -> Type -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f Type
t
    EqualityType Range
_r Sort' Term
_s QName
_eq Args
l Arg Term
t Arg Term
a Arg Term
b -> (Term -> m) -> Args -> m
forall m. Monoid m => (Term -> m) -> Args -> m
forall a m. (TermLike a, Monoid m) => (Term -> m) -> a -> m
foldTerm Term -> m
f (Args
l Args -> Args -> Args
forall a. [a] -> [a] -> [a]
++ [Arg Term
t, Arg Term
a, Arg Term
b])

instance Free EqualityView where
  freeVars :: forall r. ComputeFree r => EqualityView -> Reader r (Collect r)
freeVars EqualityView
ev = ((Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
 -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r)
forall a.
ExpandCase LiftedRep a =>
((a -> Result LiftedRep a) -> Result LiftedRep a) -> a
expand \Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret -> case EqualityView
ev of
    OtherType Type
t                   -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Type -> Reader r (Collect r)
forall r. ComputeFree r => Type -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars Type
t
    IdiomType Type
t                   -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ Type -> Reader r (Collect r)
forall r. ComputeFree r => Type -> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars Type
t
    EqualityType Range
_r Sort' Term
s QName
_eq Args
l Arg Term
t Arg Term
a Arg Term
b -> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
ret (Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r)))
-> Reader r (Collect r) -> Result LiftedRep (Reader r (Collect r))
forall a b. (a -> b) -> a -> b
$ (Sort' Term, Args, (Arg Term, Arg Term, Arg Term))
-> Reader r (Collect r)
forall r.
ComputeFree r =>
(Sort' Term, Args, (Arg Term, Arg Term, Arg Term))
-> Reader r (Collect r)
forall t r. (Free t, ComputeFree r) => t -> Reader r (Collect r)
freeVars (Sort' Term
s, Args
l, (Arg Term
t, Arg Term
a, Arg Term
b))

instance Subst EqualityView where
  type SubstArg EqualityView = Term
  applySubst :: Substitution' (SubstArg EqualityView)
-> EqualityView -> EqualityView
applySubst Substitution' (SubstArg EqualityView)
rho = \case
    OtherType Type
t          -> Type -> EqualityView
OtherType (Type -> EqualityView) -> Type -> EqualityView
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Type)
Substitution' (SubstArg EqualityView)
rho Type
t
    IdiomType Type
t          -> Type -> EqualityView
IdiomType (Type -> EqualityView) -> Type -> EqualityView
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg Type) -> Type -> Type
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg Type)
Substitution' (SubstArg EqualityView)
rho Type
t
    EqualityViewType EqualityTypeData
eqt -> EqualityTypeData -> EqualityView
EqualityViewType (EqualityTypeData -> EqualityView)
-> EqualityTypeData -> EqualityView
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg EqualityTypeData)
-> EqualityTypeData -> EqualityTypeData
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg EqualityTypeData)
Substitution' (SubstArg EqualityView)
rho EqualityTypeData
eqt

instance Subst EqualityTypeData where
  type SubstArg EqualityTypeData = Term
  applySubst :: Substitution' (SubstArg EqualityTypeData)
-> EqualityTypeData -> EqualityTypeData
applySubst Substitution' (SubstArg EqualityTypeData)
rho (EqualityTypeData Range
r Sort' Term
s QName
eq Args
l Arg Term
t Arg Term
a Arg Term
b) = Range
-> Sort' Term
-> QName
-> Args
-> Arg Term
-> Arg Term
-> Arg Term
-> EqualityTypeData
EqualityTypeData Range
r
    (Substitution' (SubstArg (Sort' Term)) -> Sort' Term -> Sort' Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Sort' Term))
Substitution' (SubstArg EqualityTypeData)
rho Sort' Term
s)
    QName
eq
    ((Arg Term -> Arg Term) -> Args -> Args
forall a b. (a -> b) -> [a] -> [b]
map (Substitution' (SubstArg (Arg Term)) -> Arg Term -> Arg Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Arg Term))
Substitution' (SubstArg EqualityTypeData)
rho) Args
l)
    (Substitution' (SubstArg (Arg Term)) -> Arg Term -> Arg Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Arg Term))
Substitution' (SubstArg EqualityTypeData)
rho Arg Term
t)
    (Substitution' (SubstArg (Arg Term)) -> Arg Term -> Arg Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Arg Term))
Substitution' (SubstArg EqualityTypeData)
rho Arg Term
a)
    (Substitution' (SubstArg (Arg Term)) -> Arg Term -> Arg Term
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg (Arg Term))
Substitution' (SubstArg EqualityTypeData)
rho Arg Term
b)


-- | Get the name of the equality type.
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
  -- Andreas, 2014-05-17 moved this here from TC.Rules.Def
  -- Don't know why up to 2 hidden lambdas need to be stripped,
  -- but I left the code in place.
  -- Maybe it was intended that equality could be declared
  -- in three different ways:
  -- 1. universe and type polymorphic
  -- 2. type polymorphic only
  -- 3. monomorphic.
  let lamV (Lam ArgInfo
i Abs Term
b)  = ([Hiding] -> [Hiding]) -> ([Hiding], Term) -> ([Hiding], Term)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (ArgInfo -> Hiding
forall a. LensHiding a => a -> Hiding
getHiding ArgInfo
i Hiding -> [Hiding] -> [Hiding]
forall a. a -> [a] -> [a]
:) (([Hiding], Term) -> ([Hiding], Term))
-> ([Hiding], Term) -> ([Hiding], Term)
forall a b. (a -> b) -> a -> b
$ Term -> ([Hiding], Term)
lamV (Abs Term -> Term
forall a. Abs a -> a
unAbs Abs Term
b)
      lamV Term
v          = ([], Term
v)
  return $ case lamV eq of
    ([Hiding]
_, Def QName
equality Elims
_) -> QName
equality
    ([Hiding], Term)
_                   -> QName
forall a. HasCallStack => a
__IMPOSSIBLE__

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

equalityView ::
     Range  -- ^ Range of the @rewrite@ expression, if any.
  -> Type   -- ^ Identity type?
  -> TCM EqualityView
equalityView :: Range -> Type -> TCM EqualityView
equalityView Range
r t0 :: Type
t0@(El Sort' Term
s Term
t) = do
  equality <- 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 b (m :: * -> *). (IsBool b, Monad m) => b -> m () -> m ()
unless (Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
3) TCM ()
forall a. HasCallStack => a
__IMPOSSIBLE__
      let (Args
pars, [ Arg Term
typ , Arg Term
lhs, Arg Term
rhs ]) = Int -> Args -> (Args, Args)
forall a. Int -> [a] -> ([a], [a])
splitAt (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
3) Args
vs
      EqualityView -> TCM EqualityView
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (EqualityView -> TCM EqualityView)
-> EqualityView -> TCM EqualityView
forall a b. (a -> b) -> a -> b
$ Range
-> Sort' Term
-> QName
-> Args
-> Arg Term
-> Arg Term
-> Arg Term
-> EqualityView
EqualityType Range
r Sort' Term
s QName
equality Args
pars Arg Term
typ Arg Term
lhs Arg Term
rhs
    Term
_ -> EqualityView -> TCM EqualityView
forall a. a -> TCMT IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (EqualityView -> TCM EqualityView)
-> EqualityView -> TCM EqualityView
forall a b. (a -> b) -> a -> b
$ Type -> EqualityView
OtherType Type
t0

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

class EqualityUnview a where
  equalityUnview :: a -> Type

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

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

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

-- | Identifiers of "primitive" functions which must be given a
-- user-written definition and bound by a BUILTIN pragma, instead of
-- being defined in a @primitive@ block.
builtinPrimitives :: [PrimitiveId]
builtinPrimitives :: [PrimitiveId]
builtinPrimitives =
  [ PrimitiveId
PrimNatPlus
  , PrimitiveId
PrimNatMinus
  , PrimitiveId
PrimNatTimes
  , PrimitiveId
PrimNatDivSucAux
  , PrimitiveId
PrimNatModSucAux
  , PrimitiveId
PrimNatEquality
  , PrimitiveId
PrimNatLess
  , PrimitiveId
PrimLevelZero
  , PrimitiveId
PrimLevelSuc
  , PrimitiveId
PrimLevelMax
  ]

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