Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

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

displayFormArities :: QName -> TCM [Int] Source #

Get the arities of all display forms for a name.

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

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 "srcfullAgdaTypeCheckingDisplayForm.hs" 126)) which corresponds to a raise by -1).

Methods

match :: a -> a -> MaybeT TCM [WithOrigin Term] Source #

Instances

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

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.

Methods

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

Instances

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