Safe Haskell | None |
---|---|
Language | Haskell2010 |
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 :: Type -> Type) = MonadConversion m
- checkType :: MonadCheckInternal m => Type -> m ()
- infer :: MonadCheckInternal m => Term -> m Type
- inferSpine :: MonadCheckInternal m => Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims)
- class CheckInternal a where
- checkInternal' :: MonadCheckInternal m => Action m -> a -> Comparison -> TypeOf a -> m a
- checkInternal :: MonadCheckInternal m => a -> Comparison -> TypeOf a -> m ()
- inferInternal' :: (MonadCheckInternal m, TypeOf a ~ ()) => Action m -> a -> m a
- inferInternal :: (MonadCheckInternal m, TypeOf a ~ ()) => a -> m ()
- data Action (m :: Type -> Type) = Action {
- preAction :: Type -> Term -> m Term
- postAction :: Type -> Term -> m Term
- modalityAction :: Modality -> Modality -> Modality
- elimViewAction :: Term -> m Term
- defaultAction :: forall (m :: Type -> Type). PureTCM m => Action m
- eraseUnusedAction :: Action TCM
Documentation
type MonadCheckInternal (m :: Type -> Type) = MonadConversion m Source #
checkType :: MonadCheckInternal m => Type -> m () Source #
Entry point for e.g. checking WithFunctionType.
inferSpine :: MonadCheckInternal m => Action m -> Type -> (Elims -> Term) -> Elims -> m (Type, Elims) Source #
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.
class CheckInternal a where Source #
checkInternal' :: MonadCheckInternal m => Action m -> a -> Comparison -> TypeOf a -> m a Source #
checkInternal :: MonadCheckInternal m => a -> Comparison -> TypeOf a -> m () Source #
inferInternal' :: (MonadCheckInternal m, TypeOf a ~ ()) => Action m -> a -> m a Source #
inferInternal :: (MonadCheckInternal m, TypeOf a ~ ()) => a -> m () Source #
Instances
data Action (m :: Type -> Type) Source #
checkInternal
traverses the whole Term
, and we can use this
traversal to modify the term.
Action | |
|