Copyright | (c) 2010-2011 Patrick Bahr |
---|---|

License | BSD3 |

Maintainer | Patrick Bahr <paba@diku.dk> |

Stability | experimental |

Portability | non-portable (GHC Extensions) |

Safe Haskell | None |

Language | Haskell98 |

This module implements matching of contexts or terms with variables againts terms

# Documentation

matchCxt :: (Ord v, EqF f, Eq (Cxt h f a), Functor f, Foldable f) => Context f v -> Cxt h f a -> Maybe (CxtSubst h a f v) Source

This function takes a context `c`

as the first argument and tries
to match it against the term `t`

(or in general a context with holes
in `a`

). The context `c`

matches the term `t`

if there is a
*matching substitution* `s`

that maps holes to terms (resp. contexts in general)
such that if the holes in the context `c`

are replaced according to
the substitution `s`

, the term `t`

is obtained. Note that the context
`c`

might be non-linear, i.e. has multiple holes that are
equal. According to the above definition this means that holes with
equal holes have to be instantiated by equal terms!

matchTerm :: (Ord v, EqF f, Eq (Cxt h f a), Traversable f, HasVars f v) => Term f -> Cxt h f a -> Maybe (CxtSubst h a f v) Source

This function is similar to `matchCxt`

but instead of a context it
matches a term with variables against a context.

module Data.Comp.Variables