Previous  Up  Next

Module Matcher

module Matcher: sig .. end

Standalone module containing the algorithm for matching modulo associativity and associativity and commutativity (AAC). Additionnaly, some A or AC operators can have units (U).

This module could be reused outside of the Coq plugin.

Matching a pattern p against a term t modulo AACU boils down to finding a substitution env such that the pattern p instantiated with env is equal to t modulo AACU.

We proceed by structural decomposition of the pattern, trying all possible non-deterministic splittings of the subject, when needed. The function Matcher.matcher is limited to top-level matching, that is, the subject must make a perfect match against the pattern (x+x does not match a+a+b ).

We use a search monad Search_monad to perform non-deterministic choices in an almost transparent way.

We also provide a function Matcher.subterm for finding a match that is a subterm of the subject modulo AACU. In particular, this function gives a solution to the aforementioned case (x+x against a+b+a).

On a slightly more involved level :

Utility functions

type symbol = int 
type var = int

Relationship between units and operators. This is a sparse representation of a matrix of couples (op,unit) where op is the index of the operation, and unit the index of the relevant unit. We make the assumption that any operation has 0 or 1 unit, and that operations can share a unit).

type units = (symbol * symbol) list 
type ext_units = {
   unit_for : units;
   is_ac : (symbol * bool) list;
} 
type 'a mset = ('a * int) list

The arguments of sums (or AC operators) are represented using finite multisets. (Typically, a+b+a corresponds to 2.a+b, i.e. Sum[a,2;b,1])

val linear : 'a mset -> 'a list

linear expands a multiset into a simple list

module Terms: sig .. end

Representations of expressions

module Subst: sig .. end

Substitutions (or environments)

Main functions exported by this module

val matcher : ?strict:bool ->
       ext_units ->
       Terms.t -> Terms.t -> Subst.t Search_monad.m

matcher p t computes the set of solutions to the given top-level matching problem (p is the pattern, t is the term). If the strict flag is set, solutions where units are used to instantiate some variables are excluded, unless this unit appears directly under a function symbol (e.g., f(x) still matches f(1), while x+x+y does not match a+b+c, since this would require to assign 1 to x).

val subterm : ?strict:bool ->
       ext_units ->
       Terms.t ->
       Terms.t ->
       (int * Terms.t * Subst.t Search_monad.m) Search_monad.m

subterm p t computes a set of solutions to the given subterm-matching problem.

Return a collection of possible solutions (each with the associated depth, the context, and the solutions of the matching problem). The context is actually a Matcher.Terms.t where the variables are yet to be instantiated by one of the associated substitutions