| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.DisplayForm
Description
Tools for DisplayTerm and DisplayForm.
Synopsis
- dtermToTerm :: DisplayTerm -> Term
- displayFormArities :: (HasConstInfo m, ReadTCState m) => QName -> m [Int]
- type MonadDisplayForm m = (MonadReduce m, ReadTCState m, HasConstInfo m, HasBuiltins m, MonadDebug m)
- displayForm :: MonadDisplayForm m => QName -> Elims -> m (Maybe DisplayTerm)
- matchDisplayForm :: MonadDisplayForm m => DisplayForm -> Elims -> MaybeT m (DisplayForm, DisplayTerm)
- class Match a where
- match :: MonadDisplayForm m => a -> a -> MaybeT m [WithOrigin Term]
- class SubstWithOrigin a where
- substWithOrigin :: Substitution -> [WithOrigin Term] -> a -> a
Documentation
dtermToTerm :: DisplayTerm -> Term Source #
Convert a DisplayTerm into a Term.
displayFormArities :: (HasConstInfo m, ReadTCState m) => QName -> m [Int] Source #
Get the arities of all display forms for a name.
type MonadDisplayForm m = (MonadReduce m, ReadTCState m, HasConstInfo m, HasBuiltins m, MonadDebug m) Source #
displayForm :: MonadDisplayForm m => QName -> Elims -> m (Maybe DisplayTerm) Source #
Find a matching display form for q es.
In essence this tries to rewrite q es with any
display form q ps --> dt and returns the instantiated
dt if successful. First match wins.
matchDisplayForm :: MonadDisplayForm m => DisplayForm -> Elims -> MaybeT m (DisplayForm, DisplayTerm) Source #
Match a DisplayForm q ps = v against q es.
Return the DisplayTerm v[us] if the match was successful,
i.e., es / ps = Just us.
Class Match for matching a term p in the role of a pattern
against a term v.
The 0th variable in p plays the role
of a place holder (pattern variable). Each occurrence of
var 0 in p stands for a different pattern variable.
The result of matching, if successful, is a list of solutions for the pattern variables, in left-to-right order.
The 0th variable is in scope in the input v, but should not
actually occur!
In the output solution, the 0th variable is no longer in scope.
(It has been substituted by IMPOSSIBLE which corresponds to
a raise by -1).
Methods
match :: MonadDisplayForm m => a -> a -> MaybeT m [WithOrigin Term] Source #
Instances
| Match Level Source # | |
Defined in Agda.TypeChecking.DisplayForm | |
| Match Sort Source # | |
Defined in Agda.TypeChecking.DisplayForm | |
| Match Term Source # | |
Defined in Agda.TypeChecking.DisplayForm | |
| Match a => Match [a] Source # | |
Defined in Agda.TypeChecking.DisplayForm Methods match :: forall (m :: Type -> Type). MonadDisplayForm m => [a] -> [a] -> MaybeT m [WithOrigin Term] Source # | |
| Match a => Match (Arg a) Source # | |
Defined in Agda.TypeChecking.DisplayForm | |
| Match a => Match (Elim' a) Source # | |
Defined in Agda.TypeChecking.DisplayForm | |
class SubstWithOrigin a where Source #
Substitute terms with origin into display terms, replacing variables along with their origins.
The purpose is to replace the pattern variables in a with-display form, and only on the top level of the lhs. Thus, we are happy to fall back to ordinary substitution where it does not matter. This fixes issue #2590.
Methods
substWithOrigin :: Substitution -> [WithOrigin Term] -> a -> a Source #