Agda.TypeChecking.DisplayForm

Tools for DisplayTerm and DisplayForm.

Documentation

dtermToTerm :: DisplayTerm -> Term

Convert a DisplayTerm into a Term.

displayFormArities :: QName -> TCM [Int]

Get the arities of all display forms for a name.

displayForm :: QName -> Elims -> TCM (Maybe DisplayTerm)

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)

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 a where

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

Minimal complete definition

match

Methods

match :: a -> a -> MaybeT TCM [Term]

Instances

Match Level

Methods

match :: Level -> Level -> MaybeT TCM [Term]

Match Sort

Methods

match :: Sort -> Sort -> MaybeT TCM [Term]

Match Term

Methods

match :: Term -> Term -> MaybeT TCM [Term]

Match a => Match [a]

Methods

match :: [a] -> [a] -> MaybeT TCM [Term]

Match a => Match (Arg a)

Methods

match :: Arg a -> Arg a -> MaybeT TCM [Term]

Match a => Match (Elim' a)

Methods

match :: Elim' a -> Elim' a -> MaybeT TCM [Term]