Agda-2.8.0: 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

- 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.

infer :: MonadCheckInternal m => Term -> m Type Source #

Infer type of a neutral term.

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 #

Minimal complete definition

checkInternal'

Methods

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

Instances details

CheckInternal Elims Source # |

Instance details

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Elims -> Comparison -> TypeOf Elims -> m Elims Source #

checkInternal :: MonadCheckInternal m => Elims -> Comparison -> TypeOf Elims -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf Elims ~ ()) => Action m -> Elims -> m Elims Source #

inferInternal :: (MonadCheckInternal m, TypeOf Elims ~ ()) => Elims -> m () Source #

CheckInternal Level Source # |

Instance details

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Level -> Comparison -> TypeOf Level -> m Level Source #

checkInternal :: MonadCheckInternal m => Level -> Comparison -> TypeOf Level -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf Level ~ ()) => Action m -> Level -> m Level Source #

inferInternal :: (MonadCheckInternal m, TypeOf Level ~ ()) => Level -> m () Source #

CheckInternal PlusLevel Source # |

Instance details

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> PlusLevel -> Comparison -> TypeOf PlusLevel -> m PlusLevel Source #

checkInternal :: MonadCheckInternal m => PlusLevel -> Comparison -> TypeOf PlusLevel -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf PlusLevel ~ ()) => Action m -> PlusLevel -> m PlusLevel Source #

inferInternal :: (MonadCheckInternal m, TypeOf PlusLevel ~ ()) => PlusLevel -> m () Source #

CheckInternal Sort Source # |

Instance details

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Sort -> Comparison -> TypeOf Sort -> m Sort Source #

checkInternal :: MonadCheckInternal m => Sort -> Comparison -> TypeOf Sort -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf Sort ~ ()) => Action m -> Sort -> m Sort Source #

inferInternal :: (MonadCheckInternal m, TypeOf Sort ~ ()) => Sort -> m () Source #

CheckInternal Term Source # |

Instance details

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Term -> Comparison -> TypeOf Term -> m Term Source #

checkInternal :: MonadCheckInternal m => Term -> Comparison -> TypeOf Term -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf Term ~ ()) => Action m -> Term -> m Term Source #

inferInternal :: (MonadCheckInternal m, TypeOf Term ~ ()) => Term -> m () Source #

CheckInternal Type Source # |

Instance details

Defined in Agda.TypeChecking.CheckInternal

Methods

checkInternal' :: MonadCheckInternal m => Action m -> Type -> Comparison -> TypeOf Type -> m Type Source #

checkInternal :: MonadCheckInternal m => Type -> Comparison -> TypeOf Type -> m () Source #

inferInternal' :: (MonadCheckInternal m, TypeOf Type ~ ()) => Action m -> Type -> m Type Source #

inferInternal :: (MonadCheckInternal m, TypeOf Type ~ ()) => Type -> m () Source #

data Action (m :: Type -> Type) 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 :: forall (m :: Type -> Type). PureTCM m => Action m Source #

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

eraseUnusedAction :: Action TCM Source #