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