Safe Haskell | None |
---|---|
Language | Haskell98 |
Tools for DisplayTerm
and DisplayForm
.
- dtermToTerm :: DisplayTerm -> Term
- displayFormArities :: QName -> TCM [Int]
- displayForm :: QName -> Args -> TCM (Maybe DisplayTerm)
- matchDisplayForm :: DisplayForm -> Args -> MaybeT TCM DisplayTerm
- class Match a where
Documentation
dtermToTerm :: DisplayTerm -> Term Source
Convert a DisplayTerm
into a Term
.
displayFormArities :: QName -> TCM [Int] Source
Get the arities of all display forms for a name.
displayForm :: QName -> Args -> TCM (Maybe DisplayTerm) Source
Find a matching display form for q vs
.
In essence this tries to reqwrite q vs
with any
display form q ps --> dt
and returns the instantiated
dt
if successful. First match wins.
matchDisplayForm :: DisplayForm -> Args -> MaybeT TCM DisplayTerm Source
Match a DisplayForm
q ps = v
against q vs
.
Return the DisplayTerm
v[us]
if the match was successful,
i.e., vs / 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).