Agda.TypeChecking.CheckInternal

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.

Documentation

type MonadCheckInternal m = MonadConversion m

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

Entry point for e.g. checking WithFunctionType.

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

Infer type of a neutral term.

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

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

Minimal complete definition

checkInternal'

Methods

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

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

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

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

Instances

CheckInternal Elims

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Elims -> Comparison -> TypeOf Elims -> m Elims

checkInternal :: MonadCheckInternal m => Elims -> Comparison -> TypeOf Elims -> m ()

inferInternal' :: (MonadCheckInternal m, TypeOf Elims ~ ()) => Action m -> Elims -> m Elims

inferInternal :: (MonadCheckInternal m, TypeOf Elims ~ ()) => Elims -> m ()

CheckInternal Level

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Level -> Comparison -> TypeOf Level -> m Level

checkInternal :: MonadCheckInternal m => Level -> Comparison -> TypeOf Level -> m ()

inferInternal' :: (MonadCheckInternal m, TypeOf Level ~ ()) => Action m -> Level -> m Level

inferInternal :: (MonadCheckInternal m, TypeOf Level ~ ()) => Level -> m ()

CheckInternal PlusLevel

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> PlusLevel -> Comparison -> TypeOf PlusLevel -> m PlusLevel

checkInternal :: MonadCheckInternal m => PlusLevel -> Comparison -> TypeOf PlusLevel -> m ()

inferInternal' :: (MonadCheckInternal m, TypeOf PlusLevel ~ ()) => Action m -> PlusLevel -> m PlusLevel

inferInternal :: (MonadCheckInternal m, TypeOf PlusLevel ~ ()) => PlusLevel -> m ()

CheckInternal Sort

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Sort -> Comparison -> TypeOf Sort -> m Sort

checkInternal :: MonadCheckInternal m => Sort -> Comparison -> TypeOf Sort -> m ()

inferInternal' :: (MonadCheckInternal m, TypeOf Sort ~ ()) => Action m -> Sort -> m Sort

inferInternal :: (MonadCheckInternal m, TypeOf Sort ~ ()) => Sort -> m ()

CheckInternal Term

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Term -> Comparison -> TypeOf Term -> m Term

checkInternal :: MonadCheckInternal m => Term -> Comparison -> TypeOf Term -> m ()

inferInternal' :: (MonadCheckInternal m, TypeOf Term ~ ()) => Action m -> Term -> m Term

inferInternal :: (MonadCheckInternal m, TypeOf Term ~ ()) => Term -> m ()

CheckInternal Type

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Type -> Comparison -> TypeOf Type -> m Type

checkInternal :: MonadCheckInternal m => Type -> Comparison -> TypeOf Type -> m ()

inferInternal' :: (MonadCheckInternal m, TypeOf Type ~ ()) => Action m -> Type -> m Type

inferInternal :: (MonadCheckInternal m, TypeOf Type ~ ()) => Type -> m ()

data Action m

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

Constructors

Action

Fields

• preAction :: Type -> Term -> m Term

  Called on each subterm before the checker runs.

• postAction :: Type -> Term -> m Term

  Called on each subterm after the type checking.

• modalityAction :: Modality -> Modality -> Modality

  Called for each ArgInfo. The first Modality is from the type, the second from the term.

• elimViewAction :: Term -> m Term

  Called for bringing projection-like funs in post-fix form

defaultAction :: PureTCM m => Action m

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

eraseUnusedAction :: Action TCM