ModuleAgda-2.8.0.2Haskell2010
Agda.TypeChecking.CheckInternal
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.
- 2 types
- 1 class
- 5 values
- PackageAgda-2.8.0.2
- Exports8
- LanguageHaskell2010
- LicenceMIT
- SourceCheckInternal.hs
Entry point for e.g. checking WithFunctionType.
Infer type of a neutral term.
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.
Methods
checkInternal' :: MonadCheckInternal m => Action m -> a -> Comparison -> TypeOf a -> m acheckInternal :: MonadCheckInternal m => a -> Comparison -> TypeOf a -> m ()inferInternal' :: (MonadCheckInternal m, TypeOf a ~ ()) => Action m -> a -> m ainferInternal :: (MonadCheckInternal m, TypeOf a ~ ()) => a -> m ()
Instances6CheckInternal
CheckInternal ElimsDefined in Agda-2.8.0.2 · Agda.TypeChecking.CheckInternalCheckInternal LevelDefined in Agda-2.8.0.2 · Agda.TypeChecking.CheckInternalCheckInternal PlusLevelDefined in Agda-2.8.0.2 · Agda.TypeChecking.CheckInternalCheckInternal SortDefined in Agda-2.8.0.2 · Agda.TypeChecking.CheckInternalCheckInternal TermDefined in Agda-2.8.0.2 · Agda.TypeChecking.CheckInternalCheckInternal TypeDefined in Agda-2.8.0.2 · Agda.TypeChecking.CheckInternal
checkInternal traverses the whole Term, and we can use this traversal to modify the term.
Constructors
ActionpreAction :: Type -> Term -> m TermCalled on each subterm before the checker runs.
postAction :: Type -> Term -> m TermCalled on each subterm after the type checking.
modalityAction :: Modality -> Modality -> ModalityCalled for each
ArgInfo. The first Modality is from the type, the second from the term.elimViewAction :: Term -> m TermCalled for bringing projection-like funs in post-fix form
The default action is to not change the Term at all.