Safe Haskell  None 

Language  Haskell2010 
A bidirectional type checker for internal syntax.
Performs checking on unreduced terms. With the exception that projectionlike 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
 data Action m = Action {}
 defaultAction :: Monad m => Action m
 eraseUnusedAction :: Action TCM
 infer :: MonadCheckInternal m => Term > m Type
 inferSort :: MonadCheckInternal m => Term > m Sort
 shouldBeSort :: (MonadReduce m, MonadTCEnv m, ReadTCState 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 MartinLöf Type Theory
checkSort :: MonadCheckInternal m => Action m > Sort > m Sort Source #
Check if sort is wellformed.
checkInternal :: MonadCheckInternal m => Term > Comparison > Type > m () Source #
Entry point for term checking.
checkInternal' :: MonadCheckInternal m => Action m > Term > Comparison > Type > m Term Source #
checkInternal
traverses the whole Term
, and we can use this
traversal to modify the term.
Action  

shouldBeSort :: (MonadReduce m, MonadTCEnv m, ReadTCState m, MonadError TCErr m) => Type > m Sort Source #
Result is in reduced form.