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

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 ()
- checkType' :: Type -> TCM Sort
- checkSort :: Action -> Sort -> TCM Sort
- checkInternal :: Term -> Type -> TCM ()
- checkInternal' :: Action -> Term -> Type -> TCM Term
- data Action = Action {
  - preAction :: Type -> Term -> TCM Term
  - postAction :: Type -> Term -> TCM Term
  - relevanceAction :: Relevance -> Relevance -> Relevance
  }
- defaultAction :: Action
- eraseUnusedAction :: Action
- infer :: Term -> TCM Type
- inferSort :: Term -> TCM Sort
- shouldBeSort :: Type -> TCM Sort

# Documentation

checkType :: Type -> TCM () Source #

Entry point for e.g. checking WithFunctionType.

checkType' :: Type -> TCM 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 :: Action -> Sort -> TCM Sort Source #

Check if sort is well-formed.

checkInternal :: Term -> Type -> TCM () Source #

Entry point for term checking.

checkInternal' :: Action -> Term -> Type -> TCM Term 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.

- relevanceAction :: Relevance -> Relevance -> Relevance

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

defaultAction :: Action Source #

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

eraseUnusedAction :: Action Source #

infer :: Term -> TCM Type Source #

Infer type of a neutral term.

inferSort :: Term -> TCM Sort Source #

Compute the sort of a type.

shouldBeSort :: Type -> TCM Sort Source #

Result is in reduced form.