Agda-2.6.2.2.20230105: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Monad.Builtin

Synopsis

Documentation

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

Minimal complete definition

Nothing

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 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 (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

data CoinductionKit Source #

The coinductive primitives.

data SortKit Source #

Sort primitives.

class EqualityUnview a where Source #

Revert the EqualityView.

Postcondition: type is reduced.

Methods

equalityUnview :: a -> Type Source #

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

Rewrite a literal to constructor form if possible.

primEqualityName :: TCM QName Source #

Get the name of the equality type.

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 => String -> String -> 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.

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. TCMT), 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.

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.

constrainedPrims :: [String] Source #

Primitives with typechecking constrants.