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

checkType :: Type -> TCM ()
infer :: Term -> TCM Type
inferSpine :: Action -> Type -> (Elims -> Term) -> Elims -> TCM (Type, Elims)
class CheckInternal a where
- checkInternal' :: Action -> a -> Comparison -> TypeOf a -> TCM a
- checkInternal :: a -> Comparison -> TypeOf a -> TCM ()
- inferInternal' :: Action -> a -> TCM a
- inferInternal :: a -> TCM ()
data Action = Action {
- preAction :: Type -> Term -> TCM Term
- postAction :: Type -> Term -> TCM Term
- modalityAction :: Modality -> Modality -> Modality
- elimViewAction :: Term -> TCM Term
}
defaultAction :: Action
eraseUnusedAction :: Action

Documentation

checkType :: Type -> TCM () Source #

Entry point for e.g. checking WithFunctionType.

infer :: Term -> TCM Type Source #

Infer type of a neutral term.

inferSpine :: Action -> Type -> (Elims -> Term) -> Elims -> TCM (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' :: Action -> a -> Comparison -> TypeOf a -> TCM a Source #

checkInternal :: a -> Comparison -> TypeOf a -> TCM () Source #

inferInternal' :: Action -> a -> TCM a Source #

inferInternal :: a -> TCM () Source #

Instances

Instances details

CheckInternal Elims Source #
Instance details Defined in Agda.TypeChecking.CheckInternal Methods checkInternal' :: Action -> Elims -> Comparison -> TypeOf Elims -> TCM Elims Source # checkInternal :: Elims -> Comparison -> TypeOf Elims -> TCM () Source # inferInternal' :: Action -> Elims -> TCM Elims Source # inferInternal :: Elims -> TCM () Source #
CheckInternal Level Source #
Instance details Defined in Agda.TypeChecking.CheckInternal Methods checkInternal' :: Action -> Level -> Comparison -> TypeOf Level -> TCM Level Source # checkInternal :: Level -> Comparison -> TypeOf Level -> TCM () Source # inferInternal' :: Action -> Level -> TCM Level Source # inferInternal :: Level -> TCM () Source #
CheckInternal PlusLevel Source #
Instance details Defined in Agda.TypeChecking.CheckInternal Methods checkInternal' :: Action -> PlusLevel -> Comparison -> TypeOf PlusLevel -> TCM PlusLevel Source # checkInternal :: PlusLevel -> Comparison -> TypeOf PlusLevel -> TCM () Source # inferInternal' :: Action -> PlusLevel -> TCM PlusLevel Source # inferInternal :: PlusLevel -> TCM () Source #
CheckInternal Sort Source #
Instance details Defined in Agda.TypeChecking.CheckInternal Methods checkInternal' :: Action -> Sort -> Comparison -> TypeOf Sort -> TCM Sort Source # checkInternal :: Sort -> Comparison -> TypeOf Sort -> TCM () Source # inferInternal' :: Action -> Sort -> TCM Sort Source # inferInternal :: Sort -> TCM () Source #
CheckInternal Term Source #
Instance details Defined in Agda.TypeChecking.CheckInternal Methods checkInternal' :: Action -> Term -> Comparison -> TypeOf Term -> TCM Term Source # checkInternal :: Term -> Comparison -> TypeOf Term -> TCM () Source # inferInternal' :: Action -> Term -> TCM Term Source # inferInternal :: Term -> TCM () Source #
CheckInternal Type Source #
Instance details Defined in Agda.TypeChecking.CheckInternal Methods checkInternal' :: Action -> Type -> Comparison -> TypeOf Type -> TCM Type Source # checkInternal :: Type -> Comparison -> TypeOf Type -> TCM () Source # inferInternal' :: Action -> Type -> TCM Type Source # inferInternal :: Type -> TCM () Source #

data Action Source #

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

Constructors

Action

Fields

preAction :: Type -> Term -> TCM Term
Called on each subterm before the checker runs.
postAction :: Type -> Term -> TCM 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 -> TCM Term
Called for bringing projection-like funs in post-fix form

defaultAction :: Action Source #

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

eraseUnusedAction :: Action Source #