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
190
191
192
|
(***************************************************************************)
(* 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).
This module could be reused ouside of the Coq plugin.
Matching modulo AAC a pattern [p] against a term [t] boils down to
finding a substitution [env] such that the pattern [p] instantiated
with [env] is equal to [t] modulo AAC.
We proceed by structural decomposition of the pattern, trying all
possible non-deterministic split 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} 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 AAC. In particular, this function
gives a solution to the aforementioned case ([x+x] against
[a+b+a]).
*)
(** {2 Utility functions} *)
type symbol = int
type var = int
(** The {!Search} module contains a search monad that allows to
express our non-deterministic and back-tracking algorithm in a
legible maner.
@see <http://spivey.oriel.ox.ac.uk/mike/search-jfp.pdf> the
inspiration of this module
*)
module Search :
sig
(** A data type that represent a collection of ['a] *)
type 'a m
(** bind and return *)
val ( >> ) : 'a m -> ('a -> 'b m) -> 'b m
val return : 'a -> 'a m
(** non-deterministic choice *)
val ( >>| ) : 'a m -> 'a m -> 'a m
(** failure *)
val fail : unit -> 'a m
(** folding through the collection *)
val fold : ('a -> 'b -> 'b) -> 'a m -> 'b -> 'b
(** derived facilities *)
val sprint : ('a -> string) -> 'a m -> string
val count : 'a m -> int
val choose : 'a m -> 'a option
val to_list : 'a m -> 'a list
val sort : ('a -> 'a -> int) -> 'a m -> 'a m
val is_empty: 'a m -> bool
end
(** 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 AAC. 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, Dot(4,[||]));
Dot(4, Var x, Sym(5,[|Sym(3,[||])|])) |])]
represents the pattern [forall x, f (x^1) (x*g b)], where [1] is the
unit associated with [( * )].
*)
type t =
Dot of (symbol * t * t)
| One of symbol
| Plus of (symbol * t * t)
| Zero of symbol
| Sym of (symbol * t array)
| Var of var
(** Test for equality of terms modulo AAC (relies on the following
canonical representation of terms) *)
val equal_aac : 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 AAC
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 AAC
iif [nf_equal (term_of_t a) (term_of_t b) = true] *)
val term_of_t : 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 -> Terms.t -> Terms.t -> Subst.t Search.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 -> Terms.t -> Terms.t -> (int * Terms.t * Subst.t Search.m) Search.m
(** pretty printing of the solutions *)
val pp_all : (Terms.t -> Pp.std_ppcmds) -> (int * Terms.t * Subst.t Search.m) Search.m -> Pp.std_ppcmds
|
