File: matcher.mli

package info (click to toggle)
aac-tactics 8.6.1-1
  • links: PTS, VCS
  • area: main
  • in suites: stretch
  • size: 396 kB
  • sloc: ml: 2,604; makefile: 34
file content (189 lines) | stat: -rw-r--r-- 7,353 bytes parent folder | download | duplicates (3)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
(***************************************************************************)
(*  This is part of aac_tactics, it is distributed under the terms of the  *)
(*         GNU Lesser General Public License version 3                     *)
(*              (see file LICENSE for more details)                        *)
(*                                                                         *)
(*       Copyright 2009-2010: Thomas Braibant, Damien Pous.                *)
(***************************************************************************)

(** 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} 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 {!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 :
    - 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.

    - if the pattern does not contain "hard" symbols (like constants,
    function symbols, AC or A symbols without units), there can be
    infinitely many subterms such that the pattern matches: it is
    possible to build "subterms" modulo AAC and U that make the size
    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}  *)

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 (* from AC/A symbols to the unit *)
type ext_units =
    {
      unit_for : units; (* from AC/A symbols to the unit *)     
      is_ac : (symbol * bool) 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]]) *)
type 'a mset = ('a * int) list

(** [linear] expands a multiset into a simple list *)
val linear : 'a mset -> 'a list

(** Representations of 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
    representation for the above terms modulo AACU. The construction
    functions on this type ensure that these terms are in normal form
    (that is, no sum can appear as a subterm of the same sum, no
    trailing units, lists corresponding to multisets are sorted,
    etc...).

*)
module Terms  :
sig

  (** {2 Abstract syntax tree of terms and patterns}

      We represent both terms and patterns using the following datatype.

      Values of type [symbol] are used to index symbols. Typically,
      given two associative operations [(^)] and [( * )], and two
      morphisms [f] and [g], the term [f (a^b) (a*g b)] is represented
      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],

      Accordingly, the following value, that contains "variables"
      [Sym(0,[| Dot(1, Var x, Unit (1); Dot(4, Var x,
      Sym(5,[|Sym(3,[||])|])) |])] represents the pattern [forall x, f
      (x^1) (x*g b)]. The relationship between [1] and [( * )] is only
      mentionned in the units table.  *)

  type t =
      Dot of (symbol * t * t)
    | Plus of (symbol * t * t)
    | Sym of (symbol * t array)
    | Var of var
    | Unit of symbol

  (** Test for equality of terms modulo AACU (relies on the following
      canonical representation of terms).  Note than two different
      units of a same operator are not considered equal.  *)
  val equal_aac : units ->  t -> t -> bool


  (** {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

  (** {3 Comparisons} *)

  val nf_term_compare : nf_term -> nf_term -> int
  val nf_equal : nf_term -> nf_term -> bool   

  (** {3 Printing function}  *)

  val sprint_nf_term : nf_term -> string

  (** {3 Conversion functions}  *)

  (** 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

end


(** Substitutions (or environments)

    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 :
sig
  type t
  val sprint : t -> string
  val instantiate : t -> Terms.t-> Terms.t
  val to_list : t -> (var*Terms.t) list
end


(** {2 Main functions exported by this module}  *)

(** [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 matcher : ?strict:bool -> ext_units -> Terms.t -> Terms.t -> Subst.t 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 {!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 Search_monad.m) Search_monad.m