Agda-2.6.4.2: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Monad.Builtin

Synopsis

Documentation

constructorForm :: HasBuiltins m => Term -> m Term Source #

Rewrite a literal to constructor form if possible.

class (Functor m, Applicative m, MonadFail m) => HasBuiltins (m :: Type -> Type) where Source #

Minimal complete definition

Nothing

Methods

getBuiltinThing :: SomeBuiltin -> m (Maybe (Builtin PrimFun)) Source #

default getBuiltinThing :: forall (t :: (Type -> Type) -> Type -> Type) (n :: Type -> Type). (MonadTrans t, HasBuiltins n, t n ~ m) => SomeBuiltin -> m (Maybe (Builtin PrimFun)) Source #

Instances

Instances details
HasBuiltins AbsToCon Source # 
Instance details

Defined in Agda.Syntax.Translation.AbstractToConcrete

HasBuiltins TerM Source # 
Instance details

Defined in Agda.Termination.Monad

HasBuiltins ReduceM Source # 
Instance details

Defined in Agda.TypeChecking.Reduce.Monad

HasBuiltins BuiltinAccess Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

HasBuiltins NLM Source # 
Instance details

Defined in Agda.TypeChecking.Rewriting.NonLinMatch

HasBuiltins m => HasBuiltins (PureConversionT m) Source # 
Instance details

Defined in Agda.TypeChecking.Conversion.Pure

HasBuiltins m => HasBuiltins (BlockT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

MonadIO m => HasBuiltins (TCMT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

HasBuiltins m => HasBuiltins (NamesT m) Source # 
Instance details

Defined in Agda.TypeChecking.Names

HasBuiltins m => HasBuiltins (ListT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

HasBuiltins m => HasBuiltins (ChangeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

HasBuiltins m => HasBuiltins (MaybeT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

HasBuiltins m => HasBuiltins (ExceptT e m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

HasBuiltins m => HasBuiltins (IdentityT m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

HasBuiltins m => HasBuiltins (ReaderT e m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

HasBuiltins m => HasBuiltins (StateT s m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

(HasBuiltins m, Monoid w) => HasBuiltins (WriterT w m) Source # 
Instance details

Defined in Agda.TypeChecking.Monad.Builtin

newtype BuiltinAccess a Source #

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.

Constructors

BuiltinAccess 

Fields

bindBuiltinRewriteRelation :: QName -> TCM () Source #

Add one (more) relation symbol to the rewrite relations.

getBuiltinRewriteRelations :: HasBuiltins m => m (Maybe (Set QName)) Source #

Get the currently registered rewrite relation symbols.

getTerm :: (HasBuiltins m, IsBuiltin a) => String -> a -> m Term Source #

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.

data CoinductionKit Source #

The coinductive primitives.

data SortKit Source #

Sort primitives.

Constructors

SortKit 

sortKit :: (HasBuiltins m, MonadTCError m, HasOptions m) => m SortKit Source #

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.

infallibleSortKit :: HasBuiltins m => m SortKit Source #

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.

pathView :: HasBuiltins m => Type -> m PathView Source #

Check whether the type is actually an path (lhs ≡ rhs) and extract lhs, rhs, and their type.

Precondition: type is reduced.

idViewAsPath :: HasBuiltins m => Type -> m PathView Source #

Non dependent Path

pathUnview :: PathView -> Type Source #

Revert the PathView.

Postcondition: type is reduced.

primEqualityName :: TCM QName Source #

Get the name of the equality type.

equalityView :: Type -> TCM EqualityView Source #

Check whether the type is actually an equality (lhs ≡ rhs) and extract lhs, rhs, and their type.

Precondition: type is reduced.

class EqualityUnview a where Source #

Revert the EqualityView.

Postcondition: type is reduced.

Methods

equalityUnview :: a -> Type Source #

constrainedPrims :: [PrimitiveId] Source #

Primitives with typechecking constrants.