Safe Haskell | None |
---|---|

Language | Haskell2010 |

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
- match :: a -> a -> MaybeT TCM [WithOrigin Term]

- class SubstWithOrigin a where
- substWithOrigin :: Substitution -> [WithOrigin Term] -> a -> a

# 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 (throwImpossible (Impossible "src*full*Agda*TypeChecking*DisplayForm.hs" 126)) which corresponds to
a raise by -1).

## 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 | |

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.

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