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

Agda.TypeChecking.CheckInternal

Description

A bidirectional type checker for internal syntax.

Performs checking on unreduced terms. With the exception that projection-like function applications have to be reduced since they break bidirectionality.

Synopsis

Documentation

type MonadCheckInternal (m :: Type -> Type) = MonadConversion m Source #

checkType :: MonadCheckInternal m => Type -> m () Source #

Entry point for e.g. checking WithFunctionType.

infer :: MonadCheckInternal m => Term -> m Type Source #

Infer type of a neutral term.

inferSpine :: MonadCheckInternal m => Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims) Source #

inferSpine action t hd es checks that spine es eliminates value hd [] of type t and returns the remaining type (target of elimination) and the transformed eliminations.

class CheckInternal a where Source #

Minimal complete definition

checkInternal'

Methods

checkInternal' :: MonadCheckInternal m => Action m -> a -> Comparison -> TypeOf a -> m a Source #

checkInternal :: MonadCheckInternal m => a -> Comparison -> TypeOf a -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf a ~ ()) => Action m -> a -> m a Source #

inferInternal :: (MonadCheckInternal m, TypeOf a ~ ()) => a -> m () Source #

Instances

Instances details
CheckInternal Elims Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

CheckInternal Level Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

CheckInternal PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

CheckInternal Sort Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

CheckInternal Term Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

CheckInternal Type Source # 
Instance details

Defined in Agda.TypeChecking.CheckInternal

data Action (m :: Type -> Type) Source #

checkInternal traverses the whole Term, and we can use this traversal to modify the term.

Constructors

Action 

Fields

defaultAction :: forall (m :: Type -> Type). PureTCM m => Action m Source #

The default action is to not change the Term at all.