compdata-0.5.3: Compositional Data Types

Portabilitynon-portable (GHC Extensions)
Stabilityexperimental
MaintainerPatrick Bahr <paba@diku.dk>
Safe HaskellSafe-Infered

Data.Comp.Matching

Description

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

Synopsis

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), Functor f, Foldable 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.