Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.DisplayForm

Description

Tools for DisplayTerm and DisplayForm.

Synopsis

dtermToTerm :: DisplayTerm -> Term
displayFormArities :: QName -> TCM [Int]
displayForm :: QName -> Elims -> TCM (Maybe DisplayTerm)
matchDisplayForm :: DisplayForm -> Elims -> MaybeT TCM (DisplayForm, DisplayTerm)
class Match a where
class SubstWithOrigin a where

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 [WithOrigin Term] #

Instances

Match Level #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods match :: Level -> Level -> MaybeT TCM [WithOrigin Term] #
Match Sort #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods match :: Sort -> Sort -> MaybeT TCM [WithOrigin Term] #
Match Term #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods match :: Term -> Term -> MaybeT TCM [WithOrigin Term] #
Match a => Match [a] #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods match :: [a] -> [a] -> MaybeT TCM [WithOrigin Term] #
Match a => Match (Arg a) #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods match :: Arg a -> Arg a -> MaybeT TCM [WithOrigin Term] #
Match a => Match (Elim' a) #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods match :: Elim' a -> Elim' a -> MaybeT TCM [WithOrigin Term] #

class SubstWithOrigin a where #

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.

Minimal complete definition

substWithOrigin

Methods

substWithOrigin :: Substitution -> [WithOrigin Term] -> a -> a #

Instances

SubstWithOrigin Term #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> Term -> Term #
SubstWithOrigin DisplayTerm #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> DisplayTerm -> DisplayTerm #
SubstWithOrigin a => SubstWithOrigin [a] #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> [a] -> [a] #
SubstWithOrigin (Arg Term) #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> Arg Term -> Arg Term #
SubstWithOrigin (Arg DisplayTerm) #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> Arg DisplayTerm -> Arg DisplayTerm #
SubstWithOrigin (Arg a) => SubstWithOrigin (Elim' a) #
Instance details Defined in Agda.TypeChecking.DisplayForm Methods substWithOrigin :: Substitution -> [WithOrigin Term] -> Elim' a -> Elim' a #