Safe Haskell | None |
---|---|
Language | Haskell2010 |
Tools for DisplayTerm
and DisplayForm
.
- dtermToTerm :: DisplayTerm -> Term
- displayFormArities :: QName -> TCM [Int]
- displayForm :: QName -> Elims -> TCM (Maybe DisplayTerm)
- matchDisplayForm :: DisplayForm -> Elims -> MaybeT TCM (DisplayForm, DisplayTerm)
- class Match a where
Documentation
dtermToTerm :: DisplayTerm -> Term Source #
Convert a DisplayTerm
into a Term
.
displayForm :: QName -> Elims -> TCM (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 :: DisplayForm -> Elims -> MaybeT TCM (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).