Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
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.