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

Language | Haskell2010 |

Tools for `DisplayTerm`

and `DisplayForm`

.

## Synopsis

- dtermToTerm :: DisplayTerm -> Term
- displayFormArities :: (HasConstInfo m, ReadTCState m) => QName -> m [Int]
- type MonadDisplayForm m = (MonadReduce m, ReadTCState m, HasConstInfo m, HasBuiltins m, MonadDebug m)
- displayForm :: MonadDisplayForm m => QName -> Elims -> m (Maybe DisplayTerm)
- matchDisplayForm :: MonadDisplayForm m => DisplayForm -> Elims -> MaybeT m (DisplayForm, DisplayTerm)
- class Match a where
- match :: MonadDisplayForm m => a -> a -> MaybeT m [WithOrigin Term]

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

# Documentation

dtermToTerm :: DisplayTerm -> Term Source #

Convert a `DisplayTerm`

into a `Term`

.

displayFormArities :: (HasConstInfo m, ReadTCState m) => QName -> m [Int] Source #

Get the arities of all display forms for a name.

type MonadDisplayForm m = (MonadReduce m, ReadTCState m, HasConstInfo m, HasBuiltins m, MonadDebug m) Source #

displayForm :: MonadDisplayForm m => QName -> Elims -> m (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 :: MonadDisplayForm m => DisplayForm -> Elims -> MaybeT m (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 **IMPOSSIBLE** which corresponds to
a raise by -1).

match :: MonadDisplayForm m => a -> a -> MaybeT m [WithOrigin Term] Source #

## Instances

Match Level Source # | |

Defined in Agda.TypeChecking.DisplayForm match :: MonadDisplayForm m => Level -> Level -> MaybeT m [WithOrigin Term] Source # | |

Match Sort Source # | |

Defined in Agda.TypeChecking.DisplayForm match :: MonadDisplayForm m => Sort -> Sort -> MaybeT m [WithOrigin Term] Source # | |

Match Term Source # | |

Defined in Agda.TypeChecking.DisplayForm match :: MonadDisplayForm m => Term -> Term -> MaybeT m [WithOrigin Term] Source # | |

Match a => Match [a] Source # | |

Defined in Agda.TypeChecking.DisplayForm match :: MonadDisplayForm m => [a] -> [a] -> MaybeT m [WithOrigin Term] Source # | |

Match a => Match (Arg a) Source # | |

Defined in Agda.TypeChecking.DisplayForm match :: MonadDisplayForm m => Arg a -> Arg a -> MaybeT m [WithOrigin Term] Source # | |

Match a => Match (Elim' a) Source # | |

Defined in Agda.TypeChecking.DisplayForm match :: MonadDisplayForm m => Elim' a -> Elim' a -> MaybeT m [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.

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