diff options
Diffstat (limited to 'AAC_matcher.mli')
| -rw-r--r-- | AAC_matcher.mli | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/AAC_matcher.mli b/AAC_matcher.mli index 531a2cf..896a2a9 100644 --- a/AAC_matcher.mli +++ b/AAC_matcher.mli @@ -21,7 +21,7 @@ function {!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 {!AAC_search_monad} to perform non-deterministic choices in an almost transparent way. @@ -30,7 +30,7 @@ gives a solution to the aforementioned case ([x+x] against [a+b+a]). - On a slightly more involved level : + On a slightly more involved level : - it must be noted that we allow several AC/A operators to share the same units, but that a given AC/A operator can have at most one unit. @@ -42,7 +42,7 @@ of the term increase (by making neutral elements appear in a layered fashion). Hence, in this case, a warning is issued, and some solutions are omitted. - + *) (** {2 Utility functions} *) @@ -57,9 +57,9 @@ type var = int and that operations can share a unit). *) type units =(symbol * symbol) list (* from AC/A symbols to the unit *) -type ext_units = +type ext_units = { - unit_for : units; (* from AC/A symbols to the unit *) + unit_for : units; (* from AC/A symbols to the unit *) is_ac : (symbol * bool) list } @@ -73,7 +73,7 @@ val linear : 'a mset -> 'a list (** Representations of expressions - The module {!Terms} defines two different types for expressions. + The module {!Terms} defines two different types for expressions. - a public type {!Terms.t} that represents abstract syntax trees of expressions with binary associative and commutative operators - a private type {!Terms.nf_term}, corresponding to a canonical @@ -97,8 +97,8 @@ sig by the following value [Sym(0,[| Dot(1, Sym(2,[||]), Sym(3,[||])); Dot(4, Sym(2,[||]), Sym(5,[|Sym(3,[||])|])) |])] - where the implicit symbol environment associates - [f] to [0], [(^)] to [1], [a] to [2], [b] to [3], [( * )] to [4], and [g] to [5], + where the implicit symbol environment associates + [f] to [0], [(^)] to [1], [a] to [2], [b] to [3], [( * )] to [4], and [g] to [5], Accordingly, the following value, that contains "variables" [Sym(0,[| Dot(1, Var x, Unit (1); Dot(4, Var x, @@ -120,18 +120,18 @@ sig (** {2 Normalised terms (canonical representation) } - + A term in normal form is the canonical representative of the equivalence class of all the terms that are equal modulo AACU. This representation is only used internally; it is exported here for the sake of completeness *) - type nf_term + type nf_term (** {3 Comparisons} *) val nf_term_compare : nf_term -> nf_term -> int - val nf_equal : nf_term -> nf_term -> bool + val nf_equal : nf_term -> nf_term -> bool (** {3 Printing function} *) @@ -141,8 +141,8 @@ sig (** we have the following property: [a] and [b] are equal modulo AACU iif [nf_equal (term_of_t a) (term_of_t b) = true] *) - val term_of_t : units -> t -> nf_term - val t_of_term : nf_term -> t + val term_of_t : units -> t -> nf_term + val t_of_term : nf_term -> t end @@ -152,11 +152,11 @@ end The module {!Subst} contains infrastructure to deal with substitutions, i.e., functions from variables to terms. Only a restricted subsets of these functions need to be exported. - + As expected, a particular substitution can be used to instantiate a pattern. *) -module Subst : +module Subst : sig type t val sprint : t -> string @@ -179,11 +179,11 @@ val matcher : ?strict:bool -> ext_units -> Terms.t -> Terms.t -> Subst.t AAC_sea (** [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 {!Terms.t} where the variables are yet to be instantiated by one of the associated substitutions *) -val subterm : ?strict:bool -> ext_units -> Terms.t -> Terms.t -> (int * Terms.t * Subst.t AAC_search_monad.m) AAC_search_monad.m +val subterm : ?strict:bool -> ext_units -> Terms.t -> Terms.t -> (int * Terms.t * Subst.t AAC_search_monad.m) AAC_search_monad.m |