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 = MonadConversion m
checkType :: MonadCheckInternal m => Type -> m ()
checkType' :: MonadCheckInternal m => Type -> m Sort
checkSort :: MonadCheckInternal m => Action m -> Sort -> m Sort
checkInternal :: MonadCheckInternal m => Term -> Comparison -> Type -> m ()
checkInternal' :: MonadCheckInternal m => Action m -> Term -> Comparison -> Type -> m Term
checkInternalType' :: MonadCheckInternal m => Action m -> Type -> m Type
data Action m = Action {
- preAction :: Type -> Term -> m Term
- postAction :: Type -> Term -> m Term
- modalityAction :: Modality -> Modality -> Modality
- elimViewAction :: Term -> m Term
}
defaultAction :: PureTCM m => Action m
eraseUnusedAction :: Action TCM
infer :: MonadCheckInternal m => Term -> m Type
inferSpine' :: MonadCheckInternal m => Action m -> Type -> Term -> Term -> Elims -> m ((Term, Term), Type)
shouldBeSort :: (PureTCM m, MonadBlock m, MonadError TCErr m) => Type -> m Sort

Documentation

type MonadCheckInternal m = MonadConversion m Source #

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

Entry point for e.g. checking WithFunctionType.

checkType' :: MonadCheckInternal m => Type -> m Sort Source #

Check a type and infer its sort.

Necessary because of PTS rule (SizeUniv, Set i, Set i) but SizeUniv is not included in any Set i.

This algorithm follows Abel, Coquand, Dybjer, MPC 08, Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory

checkSort :: MonadCheckInternal m => Action m -> Sort -> m Sort Source #

Check if sort is well-formed.

checkInternal :: MonadCheckInternal m => Term -> Comparison -> Type -> m () Source #

Entry point for term checking.

checkInternal' :: MonadCheckInternal m => Action m -> Term -> Comparison -> Type -> m Term Source #

checkInternalType' :: MonadCheckInternal m => Action m -> Type -> m Type Source #

data Action m 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 :: PureTCM m => Action m Source #

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

eraseUnusedAction :: Action TCM Source #

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

Infer type of a neutral term.

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

Returns both the real term (first) and the transformed term (second). The transformed term is not necessarily a valid term, so it must not be used in types.

shouldBeSort :: (PureTCM m, MonadBlock m, MonadError TCErr m) => Type -> m Sort Source #

Result is in reduced form.