Safe Haskell	None
Language	Haskell2010

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

type MonadCheckInternal (m :: Type -> Type) = MonadConversion m
checkType :: MonadCheckInternal m => Type -> m ()
infer :: MonadCheckInternal m => Term -> m Type
inferSpine :: MonadCheckInternal m => Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
class CheckInternal a where
- 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 ()
data Action (m :: Type -> Type) = Action {
- preAction :: Type -> Term -> m Term
- postAction :: Type -> Term -> m Term
- modalityAction :: Modality -> Modality -> Modality
- elimViewAction :: Term -> m Term
}
defaultAction :: forall (m :: Type -> Type). PureTCM m => Action m
eraseUnusedAction :: Action TCM

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 Methods checkInternal' :: MonadCheckInternal m => Action m -> Elims -> Comparison -> TypeOf Elims -> m Elims Source # checkInternal :: MonadCheckInternal m => Elims -> Comparison -> TypeOf Elims -> m () Source # inferInternal' :: (MonadCheckInternal m, TypeOf Elims ~ ()) => Action m -> Elims -> m Elims Source # inferInternal :: (MonadCheckInternal m, TypeOf Elims ~ ()) => Elims -> m () Source #
CheckInternal Level Source #
Instance details Defined in Agda.TypeChecking.CheckInternal Methods checkInternal' :: MonadCheckInternal m => Action m -> Level -> Comparison -> TypeOf Level -> m Level Source # checkInternal :: MonadCheckInternal m => Level -> Comparison -> TypeOf Level -> m () Source # inferInternal' :: (MonadCheckInternal m, TypeOf Level ~ ()) => Action m -> Level -> m Level Source # inferInternal :: (MonadCheckInternal m, TypeOf Level ~ ()) => Level -> m () Source #
CheckInternal PlusLevel Source #
Instance details Defined in Agda.TypeChecking.CheckInternal Methods checkInternal' :: MonadCheckInternal m => Action m -> PlusLevel -> Comparison -> TypeOf PlusLevel -> m PlusLevel Source # checkInternal :: MonadCheckInternal m => PlusLevel -> Comparison -> TypeOf PlusLevel -> m () Source # inferInternal' :: (MonadCheckInternal m, TypeOf PlusLevel ~ ()) => Action m -> PlusLevel -> m PlusLevel Source # inferInternal :: (MonadCheckInternal m, TypeOf PlusLevel ~ ()) => PlusLevel -> m () Source #
CheckInternal Sort Source #
Instance details Defined in Agda.TypeChecking.CheckInternal Methods checkInternal' :: MonadCheckInternal m => Action m -> Sort -> Comparison -> TypeOf Sort -> m Sort Source # checkInternal :: MonadCheckInternal m => Sort -> Comparison -> TypeOf Sort -> m () Source # inferInternal' :: (MonadCheckInternal m, TypeOf Sort ~ ()) => Action m -> Sort -> m Sort Source # inferInternal :: (MonadCheckInternal m, TypeOf Sort ~ ()) => Sort -> m () Source #
CheckInternal Term Source #
Instance details Defined in Agda.TypeChecking.CheckInternal Methods checkInternal' :: MonadCheckInternal m => Action m -> Term -> Comparison -> TypeOf Term -> m Term Source # checkInternal :: MonadCheckInternal m => Term -> Comparison -> TypeOf Term -> m () Source # inferInternal' :: (MonadCheckInternal m, TypeOf Term ~ ()) => Action m -> Term -> m Term Source # inferInternal :: (MonadCheckInternal m, TypeOf Term ~ ()) => Term -> m () Source #
CheckInternal Type Source #
Instance details Defined in Agda.TypeChecking.CheckInternal Methods checkInternal' :: MonadCheckInternal m => Action m -> Type -> Comparison -> TypeOf Type -> m Type Source # checkInternal :: MonadCheckInternal m => Type -> Comparison -> TypeOf Type -> m () Source # inferInternal' :: (MonadCheckInternal m, TypeOf Type ~ ()) => Action m -> Type -> m Type Source # inferInternal :: (MonadCheckInternal m, TypeOf Type ~ ()) => Type -> m () Source #

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

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 :: forall (m :: Type -> Type). PureTCM m => Action m Source #

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

eraseUnusedAction :: Action TCM Source #