Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Newer
Older
100644 532 lines (434 sloc) 14.884 kB
fccc685 Initial open-source release
MLstate authored
1 (*
2 Copyright © 2011 MLstate
3
4 This file is part of OPA.
5
6 OPA is free software: you can redistribute it and/or modify it under the
7 terms of the GNU Affero General Public License, version 3, as published by
8 the Free Software Foundation.
9
10 OPA is distributed in the hope that it will be useful, but WITHOUT ANY
11 WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
12 FOR A PARTICULAR PURPOSE. See the GNU Affero General Public License for
13 more details.
14
15 You should have received a copy of the GNU Affero General Public License
16 along with OPA. If not, see <http://www.gnu.org/licenses/>.
17 *)
18 (**
19 Finding field for sum case detection
20 @author Mathieu Barbin
21 @author Valentin Gatien-Baron
22 @author Francois Pessaux
23 *)
24
25 (**
26 TODO(maybe): this module may be used by lot's of code.
27 1) clever warning about pattern matching
28 2) javascript optimized pattern compilation
29 3) better server compilation
30
31 Make it a separated lib, no only for JS.
32 *)
33
34 (**
35 In the compilation of closed pattern matching in javascript,
36 we have sequentiel [if] in which some affectations are done under some conditions.
37 If an other pattern needs again to bind or to check for the same value,
38 the question is if we can reuse the same identifier, or if we cannot
39 because the conditions necessary for this identifier to be defined are
40 not true in this case.
41
42 Example:
43 {[
44 if ( c1 ) {
45 a = m.toto
46 }
47 if ( c1 && c2 ) {
48 b = a.tutu // there we can use a, because c1 && c2 => c1
49 }
50 c = m.toto.tata
51 ]}
52
53 The general problem is complex, but there, we need just a very small subset
54 of utilisation, in which the structure of conditions are simple :
55 The structure representing conditions contains just 2 terminal nodes,
56 present, absent, a totologic node [True], and a conjonction node (flatened)
57 *)
58
59 (**
60 The type of record field
61 *)
62 type field = string
63
64 (**
65 The indexation supporting nested dot.
66 Example:
67 The [path] of [a.tl.tl.tl.hd] is [["tl"; "tl"; "tl" ; "hd"]]
68 *)
69 type path = field list
70
71 (**
72 The indexation supporting nested dot, but in reverse order.
73 Example:
74 The field_path of [a.tl.tl.tl.hd] is [["hd"; "tl"; "tl"; "tl"]]
75
76 <!> It is in reverse order for optimization purpose.
77 *)
78 type rev_path = field list
79
80 (**
81 In some places, we manipulate set of field with all the same prefix.
82 Instead of having a redondant parts in [rev_path], we give e.g. a tuple
83 with a [rev_prefix_path] and a field set
84 *)
85 type rev_prefix_path = field list
86
87 (**
88 For the heuristic for choosing the fields used for detecting the sum case,
89 we may want to use a field rather than an other, depending on all the other
90 tests needed on the same field, for sharing tests between guards.
91 The priority is increasing, [0] is the lowest priority.
92 *)
93 type to_dot = int StringMap.t
94
95 (** {6 Conditions} *)
96
97 module SumCondition :
98 sig
99
100 (**
101 The abstract type of conditions.
102 *)
103 type t
104
105 val pp : Format.formatter -> t -> unit
106
107 (**
108 The type of check on a field we can check in a pattern matching.
109 *)
110 type check =
111 | Field of bool
112 (**
113 [true] means present, [false] means absent
114 *)
115
116 | Const of QmlAst.const_expr
117 (**
118 this check will test if a js value is equal to a qml constant
119 *)
120
121 | Size of int
122 (**
123 this check will test if the size of a js object (record) is
124 of the given size.
125 *)
126
127 (**
128 The item composing conditions.
129 [Check] is followed by a bool indicating the presence of the path [true], or
130 its absence [false]
131 *)
132 type decision =
133 | True
134 | Check of check * rev_path
135 | And of decision list
136
137 val pp_decision : Format.formatter -> decision -> unit
138
139 (**
140 The abstract type returned by the negation of a sum case
141 *)
142 type negation
143
144 type implication = t * negation
145
146 val pp_implication : Format.formatter -> implication -> unit
147
148 exception Inconsistency
149
150 (** {6 decision constructors} *)
151
152 (**
153 test the presence of a rev_path
154 *)
155 val present : rev_path -> decision
156
157 (**
158 test the absence of a rev_path
159 *)
160 val absent : rev_path -> decision
161
162 (**
163 test the presence or the absence of a rev_path,
164 according to the bool
165 *)
166 val check_field : bool -> rev_path -> decision
167
168 (**
169 test a constant
170 *)
171 val const : rev_path -> QmlAst.const_expr -> decision
172
173 (**
174 test the size
175 *)
176 val size : rev_path -> int -> decision
177
178 (**
179 tell if a condition is a conjonction
180 *)
181 val is_conjonction : decision -> bool
182
183 (**
184 Regroup and flaten conjonctives decisions.
185 In particular, proceed to simplifications such as :
186 {[
187 flattern And nodes
188 [] => True
189 And [] => True
190 ]}
191 *)
192 val conjonction : decision list -> decision
193
194 (**
195 The empty condition. Equivalent to [true]
196 *)
197 val empty : t
198
199 (**
200 Tell if a condition is empty.
201 Note that if the internal condition is empty,
202 but contains some implications,
203 this test returns false.
204 Implementation in 0(1)
205 *)
206 val is_empty : t -> bool
207
208 (**
209 Add a guard to a pre-existing condition.
210 The resulting condition may not be equivalent to [false],
211 or in this case, it will raise [Inconsistency]
212
213 Note that with the restricted condition we are considering,
214 the logical and is the only operation for composing conditions.
215 *)
216 val add : decision -> t -> t
217
218 (**
219 Build a condition from a decision
220 *)
221 val decision : decision -> t
222
223 (**
224 At some point, you know that if a certain condition is true, then it
225 implies a decision.
226 Exemple:
227 If you know [C], and you know [A => d], you may use:
228 [let C' = add_implication A d C].
229 If at some point you will add a decision in [C'] implying [A], then [d] will
230 be infered as part of the implied decisions by [C']
231 *)
232 val add_implication : implication -> t -> t
233
234 (**
235 [implies a b] returns true if and only if [a => b]
236 <!> Beware, this function will assert failure if [b] contains
237 some implications.
238 *)
239 val implies : t -> t -> bool
240
241 (**
242 Filter the decision already implied by the condition.
243 Return [True] in case the condition implies the decision
244 *)
245 val filter : t -> decision -> decision
246
247 (**
248 This is equivalent than [filter cond decision = True],
249 and the implementation of [implies] can use the implementation
250 of [filter]
251 *)
252 val implies_decision : t -> decision -> bool
253 end
254
255 (** {6 Env} *)
256
257 module SumEnv :
258 sig
259
260 (**
261 The environment of variable definitions, parametrized by the ident stored inside.
262 *)
263 type 'ident t
264
265 (**
266 The empty environment
267 *)
268 val empty : 'ident t
269
270 (**
271 Tell the implementation that this nested dot has been assigned to a new identifier,
272 under a certain condition.
273 Example:
274 An assign has been generated, under the condition [Ci]
275 {[
276 v0 = x.a.b.c
277 ]}
278 So, we will call
279 {[
280 SumEnv.add ~rev_path:["c";"b";"a"] Ci v0 sum_env
281 ]}
282 *)
283 val add_dot : rev_path:rev_path -> SumCondition.t -> 'ident -> 'ident t -> 'ident t
284
285 (**
286 Find the ident already assigned to this [rev_path] under a certain condition.
287 If no such assignment has been done, or if some was, but under a stronger
288 condition which is not implied by the current condition,
289 the function will returns [None]
290 *)
291 val find_dot : rev_path:rev_path -> SumCondition.t -> 'ident t -> 'ident option
292
293 end
294
295 (**
296 This module implements 2 functions related to sum case detection,
297 and condition about presence or absence of fields in a sum case.
298 *)
299
300 (**
301 The function [decide], with notation {[D()[]]} returns the list of
302 possible minimal (suffisant) tests for deciding the case of the sum.
303
304 Some examples:
305 {[
306 D(hd,tl|nil)[hd,tl] = present(hd) / present(tl) / absent(nil)
307 D(hd,tl|nil)[nil] = present(nil) / absent(hd) / absent(tl)
308
309 D(a|a,b)[a] = absent(b)
310 D(a|a,b)[a,b] = present(b)
311
312 D(a|b|a,b)[a] = absent(b)
313 D(a|b|a,b)[b] = absent(a)
314 D(a|b|a,b)[a,b] = present(a) AND present(b)
315 ]}
316
317 It is used for deciding with a number minimal of test in which
318 case of a sum type we are.
319
320 Some invariants about the returned list:
321
322 1) if we note [#(c)] the number of terminal nodes of a condition,
323 we have : it exists an int [i], such as for all [c] in [list], #(c) = i
324
325 2) for all [c1] != [c2] in [list], not (c1 => c2)
326 if we considere 1) verified, this means that order matters
327 *)
328
329 (**
330 The function [condition] with notation {[C()[]]} returns the complete
331 condition corresponding to the sum case.
332
333 Some examples:
334 {[
335 C(hd,tl|nil)[hd,tl] = present(hd) AND present(tl) AND absent(nil)
336 C(hd,tl|nil)[nil] = present(nil) AND absent(hd) AND absent(tl)
337
338 C(a|a,b)[a] = present(a) AND absent(b)
339 C(a|a,b)[a,b] = present(a) AND present(b)
340
341 C(a|b|a,b)[a] = present(a)
342 C(a|b|a,b)[b] = present(b)
343 C(a|b|a,b)[a,b] = present(a) AND present(b)
344 ]}
345
346 It is used for building condition when we add definition of dots
347 in the compilation of closed pattern matching.
348 *)
349
350 module SumAnalysis :
351 sig
352 (**
353 The abstract type of an analysed sum case.
354 An analysed sum case has a notion of [rev_prefix_path], where sum structure
355 are working as they were all at toplevel.
356 *)
357 type t
358
359 (**
360 Pretty printer for value of type [t]
361 For debug only.
362 *)
363 val pp : Format.formatter -> t -> unit
364
365 (**
366 The type of a field list.
367 assert: should be in lexicographic order
368 *)
369 type sum_case = StringSet.t
370 type sum (* equivalent to field list list, with extra cached infos (types) *)
371
372 (**
373 Pretty printer for value of type [sum]
374 For debug only.
375 *)
376 val pp_sum : Format.formatter -> sum -> unit
377
378 (**
379 Compute the fields cases corresponding to a sum or a record type.
380 give the absolute [rev_path] where this sum appear in the pattern
381
382 <!> Currently in closure mode, some matched expression are not annoted.
383 The returned [sum] is then empty, and not any optimization are performed.
384 *)
385 val from_ty : rev_path:rev_path -> QmlTypes.gamma -> QmlAst.ty -> sum
386
387 (**
388 Built an analysed sum case. If the colvar is not the same than the colvar infered by typing
389 in [from_ty], this will cause an internal error.
390 In case we have both rowvar and colvar open, this means that this is just a syntactic rowvar.
391 *)
392 val make :
393 sum ->
394 rowvar:Imp_PatternAnalysis.rowvar ->
395 colvar:Imp_PatternAnalysis.colvar ->
396 rev_prefix_path:rev_prefix_path ->
397 sum_case ->
398 t
399
400 (**
401 Export the cases of the sum. If the sum is unknown, this will return [None]
402 *)
403 val cases : sum -> StringSet.t array option
404
405 (**
406 The condition implied by the sum.
407 is [True] most of the time, but sometime, there are some possible informations,
408 like {[(a|a,b) ==> present(a)]}
409
410 If the sum is open in column, if the sum is undefined, we cannot imply anything. [True]
411 *)
412 val implies : sum -> SumCondition.decision
413
414 (**
415 Important remark:
416 Here this is strongly dependant to the property that same field
417 inside a sum type should necessary be on the same type.
418 The path is for nested fields.
419 Example, if {[ty = list(int)]}, then
420 {[
421 SumAnalysis.ty sum ["hd" ; "tl"; "tl" ; "tl"]
422 ]}
423 will return {[int]},
424 because the type of {[a.tl.tl.tl.hd]} is {[int]}
425
426 It is used combined with [Imp_Common.maybe_js_false]
427 Assume the rev_path is not empty.
428
429 Implementation request:
430 make so that there is a cache in [sum] indexed
431 by rev_path. We assume that the gamma used with
432 a given sum object is the same during all the
433 live of the sum object.
434
435 If the sum is unknown, this will return a fresh [typevar]
436 *)
437 val ty : QmlTypes.gamma -> sum -> rev_path:rev_path -> QmlAst.ty
438
439 (**
440 This is an optimized shorthand for [from_ty (ty sum)] with a cache
441 indexed by the rev_path
442 *)
443 val from_sum : QmlTypes.gamma -> sum -> rev_path:rev_path -> sum
444
445 (**
446 Returns a list of all possible decisions for being sure that this
447 sum case is the correct one.
448 We will use some other heuristic for choosing between this list
449 of equivalent choices.
450
451 Optimization:
452 This function takes a [SumCondition.t] in argument,
453 the current maximal condition, for beeing smarter about the
454 decision to return, if some cases have already been invalidated.
455
456 If the current condition implies the anlalysed case,
457 This function would return [None], indicating than there is nothing to check.
458
459 <!> The function may raises [Inconsistency]
460 *)
461 val decisions : SumCondition.t -> t -> SumCondition.decision list option
462
463 (**
464 Enrich the condition with all property enforced by this sum case.
465 If the analysed case is unknown, this return the same cond
466 *)
467 val add : t -> SumCondition.t -> SumCondition.t
468
469 (**
470 Returns the negation of the sum case.
471 Used for enriching the accumulator condition, for
472 skiping some tests at last patterns.
473
474 If the negation cannot be expressed into the simple
475 decision algebra, the function will return [None].
476
477 In particular, the negation of an open sum case, or an unknown sum
478 is [None].
479 *)
480 val negation : SumCondition.t -> t -> SumCondition.negation option
481
482 module Filter :
483 sig
484
485 (** {6 Choosing between decisions} *)
486 (**
487 For choosing between several decision, we will essentially use 2 heuristic, by priority :
488 + sharing with dot binding variables in this pattern implying sub-checks and other patterns
489 + using not maybe_js_false types for minimizing the size of the test
490 + using presence rather than absence checks
491
d3757ec [fix] typos: various corrections
Arthur Milchior authored
492 This filtering respect the following property:
fccc685 Initial open-source release
MLstate authored
493 if the filter apply make so that the list become empty, the filter is ignored,
494 and return the list received as input.
495 *)
496
497 (**
498 First heuristic.
499 The [to_dot] parameter contains priorities for sorting decisions,
500 [0] is the lowest priority.
501 *)
502 val patvar :
503 rev_prefix_path:rev_prefix_path ->
504 to_dot:to_dot ->
505 SumCondition.decision list -> SumCondition.decision list
506
507 (**
508 Second heuristic
509 *)
510 val non_js_false :
511 gamma:QmlTypes.gamma ->
512 sum:sum ->
513 SumCondition.decision list -> SumCondition.decision list
514
515 (**
516 Last heuristic
517 *)
518 val present : SumCondition.decision list -> SumCondition.decision list
519
520 (**
521 Combine heuristic, and choose the first remaining decision.
522 *)
523 val final_choice :
524 rev_prefix_path:rev_prefix_path ->
525 gamma:QmlTypes.gamma ->
526 sum:sum ->
527 to_dot:to_dot ->
528 SumCondition.decision list -> SumCondition.decision
529
530 end
531 end
Something went wrong with that request. Please try again.