-
Notifications
You must be signed in to change notification settings - Fork 79
/
Copy pathmatching.ml
4521 lines (4037 loc) · 153 KB
/
matching.ml
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
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(**************************************************************************)
(* *)
(* OCaml *)
(* *)
(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
(* *)
(* Copyright 1996 Institut National de Recherche en Informatique et *)
(* en Automatique. *)
(* *)
(* All rights reserved. This file is distributed under the terms of *)
(* the GNU Lesser General Public License version 2.1, with the *)
(* special exception on linking described in the file LICENSE. *)
(* *)
(**************************************************************************)
(* Compilation of pattern matching
Based upon Lefessant-Maranget ``Optimizing Pattern-Matching'' ICFP'2001.
A previous version was based on Peyton-Jones, ``The Implementation of
functional programming languages'', chapter 5.
Overview of the implementation
==============================
1. Precompilation
-----------------
(split_and_precompile)
We first split the initial pattern matching (or "pm") along its first column
-- simplifying pattern heads in the process --, so that we obtain an ordered
list of pms.
For every pm in this list, and any two patterns in its first column, either
the patterns have the same head, or their heads match disjoint sets of
values. (In particular, two extension constructors that may or may not be
equal due to hidden rebinding cannot occur in the same simple pm.)
2. Compilation
--------------
The compilation of one of these pms obtained after precompiling is done as
follows:
(divide)
We split the match along the first column again, this time grouping rows
which start with the same head, and removing the first column.
As a result we get a "division", which is a list a "cells" of the form:
discriminating pattern head * specialized pm
(compile_list + compile_match)
We then map over the division to compile each cell: we simply restart the
whole process on the second element of each cell.
Each cell is now of the form:
discriminating pattern head * lambda
(combine_constant, combine_construct, combine_array, ...)
We recombine the cells using a switch or some ifs, and if the matching can
fail, introduce a jump to the next pm that could potentially match the
scrutiny.
3. Chaining of pms
------------------
(comp_match_handlers)
Once the pms have been compiled, we stitch them back together in the order
produced by precompilation, resulting in the following structure:
{v
catch
catch
<first body>
with <exit i> ->
<second body>
with <exit j> ->
<third body>
v}
Additionally, bodies whose corresponding exit-number is never used are
discarded. So for instance, if in the pseudo-example above we know that exit
[i] is never taken, we would actually generate:
{v
catch
<first body>
with <exit j> ->
<third body>
v}
*)
open Misc
open Asttypes
open Types
open Typedtree
open Lambda
open Parmatch
open Printpat
module Scoped_location = Debuginfo.Scoped_location
type error =
| Void_layout
exception Error of Location.t * error
let dbg = false
let sort_check_not_void loc sort =
let rec contains_void : Jkind.Sort.Const.t -> bool = function
| Base Void -> true
| Base (Value | Float64 | Float32 | Word | Bits32 | Bits64 | Vec128) -> false
| Product [] ->
Misc.fatal_error "nil in sort_check_not_void"
| Product ss -> List.exists contains_void ss
in
if contains_void sort then
raise (Error (loc, Void_layout))
;;
let debugf fmt =
if dbg
then Format.eprintf fmt
else Format.ifprintf Format.err_formatter fmt
let pp_partial ppf = function
| Total -> Format.fprintf ppf "Total"
| Partial -> Format.fprintf ppf "Partial"
(*
Compatibility predicate that considers potential rebindings of constructors
of an extension type.
"may_compat p q" returns false when p and q never admit a common instance;
returns true when they may have a common instance.
*)
module MayCompat = Parmatch.Compat (struct
let equal = Types.may_equal_constr
end)
let may_compat = MayCompat.compat
and may_compats = MayCompat.compats
(*
Many functions on the various data structures of the algorithm :
- Pattern matrices.
- Default environments: mapping from exit numbers to matrices.
- Contexts: matrices whose column are partitioned into
left (prefix of the input that we have already matched) and
right (what remains to be matched).
- Jump summaries: mapping from exit numbers to contexts
*)
let all_record_args lbls =
match lbls with
| [] -> fatal_error "Matching.all_record_args"
| (_, { lbl_all }, _) :: _ ->
let t =
Array.map
(fun lbl ->
(mknoloc (Longident.Lident "?temp?"), lbl, Patterns.omega))
lbl_all
in
List.iter (fun ((_, lbl, _) as x) -> t.(lbl.lbl_num) <- x) lbls;
Array.to_list t
let expand_record_head h =
let open Patterns.Head in
match h.pat_desc with
| Record [] -> fatal_error "Matching.expand_record_head"
| Record ({ lbl_all } :: _) ->
{ h with pat_desc = Record (Array.to_list lbl_all) }
| _ -> h
let expand_record_unboxed_product_head h =
let open Patterns.Head in
match h.pat_desc with
| Record_unboxed_product [] ->
fatal_error "Matching.expand_record_unboxed_product_head"
| Record_unboxed_product ({ lbl_all } :: _) ->
{ h with pat_desc = Record_unboxed_product (Array.to_list lbl_all) }
| _ -> h
let bind_alias p id ~arg ~arg_sort ~action =
let k = Typeopt.layout p.pat_env p.pat_loc arg_sort p.pat_type in
bind_with_layout Alias (id, k) arg action
let head_loc ~scopes head =
Scoped_location.of_location ~scopes head.pat_loc
type 'a clause = 'a * lambda
let map_on_row f (row, action) = (f row, action)
let map_on_rows f = List.map (map_on_row f)
module Non_empty_row = Patterns.Non_empty_row
module General = struct
include Patterns.General
type nonrec clause = pattern Non_empty_row.t clause
end
module Half_simple : sig
include module type of Patterns.Half_simple
(** Half-simplified patterns are patterns where:
- records are expanded so that they possess all fields
- aliases are removed and replaced by bindings in actions.
Or-patterns are not removed, they are only "half-simplified":
- aliases under or-patterns are kept
- or-patterns whose right-hand-side is subsumed by their lhs
are simplified to their lhs.
For instance: [(_ :: _ | 1 :: _)] is changed into [_ :: _]
- or-patterns whose left-hand-side is not simplified
are preserved: (p|q) is changed into (simpl(p)|simpl(q))
{v
# match lazy (print_int 3; 3) with _ | lazy 2 -> ();;
- : unit = ()
# match lazy (print_int 3; 3) with lazy 2 | _ -> ();;
3- : unit = ()
v}
In particular, or-patterns may still occur in the leading column,
so this is only a "half-simplification". *)
type nonrec clause = pattern Non_empty_row.t clause
val of_clause :
arg:lambda -> arg_sort:Jkind.Sort.Const.t -> General.clause -> clause
end = struct
include Patterns.Half_simple
type nonrec clause = pattern Non_empty_row.t clause
let rec simpl_under_orpat p =
match p.pat_desc with
| Tpat_any
| Tpat_var _ ->
p
| Tpat_alias (q, id, s, uid, mode, ty) ->
{ p with pat_desc =
Tpat_alias (simpl_under_orpat q, id, s, uid, mode, ty) }
| Tpat_or (p1, p2, o) ->
let p1, p2 = (simpl_under_orpat p1, simpl_under_orpat p2) in
if le_pat p1 p2 then
p1
else
{ p with pat_desc = Tpat_or (p1, p2, o) }
| Tpat_record (lbls, closed) ->
let all_lbls = all_record_args lbls in
{ p with pat_desc = Tpat_record (all_lbls, closed) }
| Tpat_record_unboxed_product (lbls, closed) ->
let all_lbls = all_record_args lbls in
{ p with pat_desc = Tpat_record_unboxed_product (all_lbls, closed) }
| _ -> p
(* Explode or-patterns and turn aliases into bindings in actions *)
let of_clause ~arg ~arg_sort cl =
let rec aux (((p, patl), action) : General.clause) : clause =
let continue p (view : General.view) : clause =
aux (({ p with pat_desc = view }, patl), action)
in
let stop p (view : view) : clause =
(({ p with pat_desc = view }, patl), action)
in
match p.pat_desc with
| `Any -> stop p `Any
| `Var (id, s, uid, mode) ->
continue p (`Alias (Patterns.omega, id, s, uid, mode, p.pat_type))
| `Alias (p, id, _, _, _, _) ->
aux
( (General.view p, patl),
bind_alias p id ~arg ~arg_sort ~action )
| `Record ([], _) as view -> stop p view
| `Record (lbls, closed) ->
let full_view = `Record (all_record_args lbls, closed) in
stop p full_view
| `Record_unboxed_product ([], _) as view -> stop p view
| `Record_unboxed_product (lbls, closed) ->
let full_view =
`Record_unboxed_product (all_record_args lbls, closed) in
stop p full_view
| `Or _ -> (
let orpat = General.view (simpl_under_orpat (General.erase p)) in
match orpat.pat_desc with
| `Or _ as or_view -> stop orpat or_view
| other_view -> continue orpat other_view
)
| ( `Constant _ | `Tuple _ | `Unboxed_tuple _ | `Construct _ | `Variant _
| `Array _ | `Lazy _ ) as view ->
stop p view
in
aux cl
end
exception Cannot_flatten
module Simple : sig
include module type of Patterns.Simple
type nonrec clause = pattern Non_empty_row.t clause
val head : pattern -> Patterns.Head.t
val explode_or_pat :
arg:lambda ->
arg_sort:Jkind.Sort.Const.t ->
Half_simple.pattern ->
mk_action:(vars:Ident.t list -> lambda) ->
patbound_action_vars:Ident.t list ->
(pattern * lambda) list
end = struct
include Patterns.Simple
type nonrec clause = pattern Non_empty_row.t clause
let head p = fst (Patterns.Head.deconstruct p)
let alpha env (p : pattern) : pattern =
let alpha_pat env p = Typedtree.alpha_pat env p in
let pat_desc =
match p.pat_desc with
| `Any -> `Any
| `Constant cst -> `Constant cst
| `Tuple ps ->
`Tuple (List.map (fun (label, p) -> label, alpha_pat env p) ps)
| `Unboxed_tuple ps ->
`Unboxed_tuple
(List.map (fun (label, p, sort) -> label, alpha_pat env p, sort) ps)
| `Construct (cstr, cst_descr, args) ->
`Construct (cstr, cst_descr, List.map (alpha_pat env) args)
| `Variant (cstr, argo, row_desc) ->
`Variant (cstr, Option.map (alpha_pat env) argo, row_desc)
| `Record (fields, closed) ->
let alpha_field env (lid, l, p) = (lid, l, alpha_pat env p) in
`Record (List.map (alpha_field env) fields, closed)
| `Record_unboxed_product (fields, closed) ->
let alpha_field env (lid, l, p) = (lid, l, alpha_pat env p) in
`Record_unboxed_product (List.map (alpha_field env) fields, closed)
| `Array (am, arg_sort, ps) -> `Array (am, arg_sort, List.map (alpha_pat env) ps)
| `Lazy p -> `Lazy (alpha_pat env p)
in
{ p with pat_desc }
(* Consider the following matching problem involving a half-simple pattern,
with an or-pattern and as-patterns below it:
match arg, other-args with
| (Foo(y, z) as x | Bar(x, y) as z), other-pats -> action[x,y,z]
(action[x,y,z] is some right-hand-side expression using x, y and z,
but we assume that it uses no variables from [other-pats]).
[explode_or_pat] explodes this into the following:
match arg, other-args with
| Foo(y1, z1), other-pats -> let x1 = arg in action[x1,y1,z1]
| Bar(x2, y2), other-pats -> let z2 = arg in action[x2,y2,z2]
notice that the binding occurrences of x,y,z are alpha-renamed with
fresh variables x1,y1,z1 and x2,y2,z2.
We assume that it is fine to duplicate the argument [arg] in each
exploded branch; in most cases it is a variable (in which case
the bindings [let x1 = arg] are inlined on the fly), except when
compiling in [do_for_multiple_match] where it is a tuple of
variables.
*)
let explode_or_pat ~arg ~arg_sort (p : Half_simple.pattern)
~mk_action ~patbound_action_vars
: (pattern * lambda) list =
let rec explode p aliases rem =
let split_explode p aliases rem = explode (General.view p) aliases rem in
match p.pat_desc with
| `Or (p1, p2, _) ->
split_explode p1 aliases (split_explode p2 aliases rem)
| `Alias (p, id, _, _, _, _) -> split_explode p (id :: aliases) rem
| `Var (id, str, uid, mode) ->
explode
{ p with pat_desc =
`Alias (Patterns.omega, id, str, uid, mode, p.pat_type) }
aliases rem
| #view as view ->
(* We are doing two things here:
- we freshen the variables of the pattern, to
avoid reusing the same identifier in distinct exploded
branches
- we bind the variables in [aliases] to the argument [arg]
(the other variables are bound by [view]); to avoid
code duplication if [arg] is itself not a variable, we
generate a binding for it, but only if the binding is
needed.
We are careful to avoid binding [arg] if not needed due
to the {!do_for_multiple_match} usage, which tries to
compile a tuple pattern [match e1, .. en with ...]
without allocating the tuple [(e1, .., en)].
*)
let rec fresh_clause arg_id action_vars renaming_env = function
| [] ->
let fresh_pat = alpha renaming_env { p with pat_desc = view } in
let fresh_action = mk_action ~vars:(List.rev action_vars) in
(fresh_pat, fresh_action)
| pat_id :: rem_vars ->
if not (List.mem pat_id aliases) then begin
let fresh_id = Ident.rename pat_id in
let action_vars = fresh_id :: action_vars in
let renaming_env = ((pat_id, fresh_id) :: renaming_env) in
fresh_clause arg_id action_vars renaming_env rem_vars
end else begin match arg_id, arg with
| Some id, _
| None, Lvar id ->
let action_vars = id :: action_vars in
fresh_clause arg_id action_vars renaming_env rem_vars
| None, _ ->
(* [pat_id] is a name used locally to refer to the argument,
so it makes sense to reuse it (refreshed) *)
let id = Ident.rename pat_id in
let action_vars = (id :: action_vars) in
let pat, action =
fresh_clause (Some id) action_vars renaming_env rem_vars
in
pat, bind_alias pat id ~arg ~arg_sort ~action
end
in
fresh_clause None [] [] patbound_action_vars :: rem
in
explode (p : Half_simple.pattern :> General.pattern) [] []
end
let expand_record_simple : Simple.pattern -> Simple.pattern =
fun p ->
match p.pat_desc with
| `Record (l, _) -> { p with pat_desc = `Record (all_record_args l, Closed) }
| _ -> p
let expand_record_unboxed_product_simple : Simple.pattern -> Simple.pattern =
fun p ->
match p.pat_desc with
| `Record_unboxed_product (l, _) ->
{ p with pat_desc = `Record_unboxed_product (all_record_args l, Closed) }
| _ -> p
type initial_clause = pattern list clause
type matrix = pattern list list
let add_omega_column pss = List.map (fun ps -> Patterns.omega :: ps) pss
let rec rev_split_at n ps =
if n <= 0 then
([], ps)
else
match ps with
| p :: rem ->
let left, right = rev_split_at (n - 1) rem in
(p :: left, right)
| _ -> assert false
exception NoMatch
let matcher discr (p : Simple.pattern) rem =
let discr = expand_record_head discr in
let discr = expand_record_unboxed_product_head discr in
let p = expand_record_simple p in
let p = expand_record_unboxed_product_simple p in
let omegas = Patterns.(omegas (Head.arity discr)) in
let ph, args = Patterns.Head.deconstruct p in
let yes () = args @ rem in
let no () = raise NoMatch in
let yesif b =
if b then
yes ()
else
no ()
in
let open Patterns.Head in
match (discr.pat_desc, ph.pat_desc) with
| Any, _ -> rem
| ( ( Constant _ | Construct _ | Variant _ | Lazy | Array _ | Record _
| Record_unboxed_product _ | Tuple _ | Unboxed_tuple _ ),
Any ) ->
omegas @ rem
| Constant cst, Constant cst' -> yesif (const_compare cst cst' = 0)
| Construct cstr, Construct cstr' ->
(* NB: may_equal_constr considers (potential) constructor rebinding;
Types.may_equal_constr does check that the arities are the same,
preserving row-size coherence. *)
yesif (Types.may_equal_constr cstr cstr')
| Variant { tag; has_arg }, Variant { tag = tag'; has_arg = has_arg' } ->
yesif (tag = tag' && has_arg = has_arg')
| Array (am1, _, n1), Array (am2, _, n2) -> yesif (am1 = am2 && n1 = n2)
| Tuple n1, Tuple n2 -> yesif (n1 = n2)
| Unboxed_tuple l1, Unboxed_tuple l2 ->
yesif (List.for_all2 (fun (lbl1, _) (lbl2, _) -> lbl1 = lbl2) l1 l2)
| Record l, Record l' ->
(* we already expanded the record fully *)
yesif (List.length l = List.length l')
| Record_unboxed_product l, Record_unboxed_product l' ->
(* we already expanded the record fully *)
yesif (List.length l = List.length l')
| Lazy, Lazy -> yes ()
| ( Constant _ | Construct _ | Variant _ | Lazy | Array _ | Record _
| Record_unboxed_product _ | Tuple _ | Unboxed_tuple _), _
->
no ()
let ncols = function
| [] -> 0
| ps :: _ -> List.length ps
module Context : sig
type t
val empty : t
val is_empty : t -> bool
val start : int -> t
val pp : Format.formatter -> t -> unit
val specialize : Patterns.Head.t -> t -> t
val lshift : t -> t
val rshift : t -> t
val rshift_num : int -> t -> t
val lub : pattern -> t -> t
val matches : t -> matrix -> bool
val combine : t -> t
val select_columns : matrix -> t -> t
val union : t -> t -> t
end = struct
module Row = struct
type t = { left : pattern list; right : pattern list }
(* Static knowledge on a frontier of nodes (subtrees) in the matched values.
Left: what we know about what is above us, towards the root.
Right: what we know about whas is below us, towards the leaves. *)
let pp ppf { left; right } =
Format.fprintf ppf
"@[LEFT@ %aRIGHT@ %a@]"
pretty_line left
pretty_line right
let le c1 c2 = le_pats c1.left c2.left && le_pats c1.right c2.right
let lshift { left; right } =
match right with
| x :: xs -> { left = x :: left; right = xs }
| _ -> assert false
let lforget { left; right } =
match right with
| _ :: xs -> { left = Patterns.omega :: left; right = xs }
| _ -> assert false
let rshift { left; right } =
match left with
| p :: ps -> { left = ps; right = p :: right }
| _ -> assert false
let rshift_num n { left; right } =
let shifted, left = rev_split_at n left in
{ left; right = shifted @ right }
(** Recombination of contexts.
For example:
{ (_,_)::left; p1::p2::right } -> { left; (p1,p2)::right }
All mutable fields are replaced by '_', since side-effects in
guards can alter these fields. *)
let combine { left; right } =
match left with
| p :: ps -> { left = ps; right = set_args_erase_mutable p right }
| _ -> assert false
end
type t = Row.t list
(* A union/disjunction of possible context "rows". What we know is that
the matching situation is described by one of the rows. *)
let empty = []
let start n : t = [ { left = []; right = Patterns.omegas n } ]
let is_empty = function
| [] -> true
| _ -> false
let pp ppf ctx =
Format.pp_print_list ~pp_sep:Format.pp_print_cut
Row.pp ppf ctx
let lshift ctx =
if List.length ctx < !Clflags.match_context_rows then
List.map Row.lshift ctx
else
(* Context pruning *)
get_mins Row.le (List.map Row.lforget ctx)
let rshift ctx = List.map Row.rshift ctx
let rshift_num n ctx = List.map (Row.rshift_num n) ctx
let combine ctx = List.map Row.combine ctx
let specialize head ctx =
let non_empty = function
| { Row.left = _; right = [] } ->
fatal_error "Matching.Context.specialize"
| { Row.left; right = p :: ps } -> (left, p, ps)
in
let ctx = List.map non_empty ctx in
let rec filter_rec = function
| [] -> []
| (left, p, right) :: rem -> (
let p = General.view p in
match p.pat_desc with
| `Or (p1, p2, _) ->
filter_rec ((left, p1, right) :: (left, p2, right) :: rem)
| `Alias (p, _, _, _, _, _) -> filter_rec ((left, p, right) :: rem)
| `Var _ -> filter_rec ((left, Patterns.omega, right) :: rem)
| #Simple.view as view -> (
let p = { p with pat_desc = view } in
match matcher head p right with
| exception NoMatch -> filter_rec rem
| right ->
let left = Patterns.Head.to_omega_pattern head :: left in
{ Row.left; right }
:: filter_rec rem
)
)
in
filter_rec ctx
let select_columns pss ctx =
let n = ncols pss in
let lub_row ps { Row.left; right } =
let transfer, right = rev_split_at n right in
match lubs transfer ps with
| exception Empty -> None
| inter -> Some { Row.left = inter @ left; right }
in
let lub_with_ctx ps = List.filter_map (lub_row ps) ctx in
List.flatten (List.map lub_with_ctx pss)
let lub p ctx =
List.filter_map
(fun { Row.left; right } ->
match right with
| q :: rem -> (
try Some { Row.left; right = lub p q :: rem } with Empty -> None
)
| _ -> fatal_error "Matching.Context.lub")
ctx
let matches ctx pss =
List.exists
(fun { Row.right = qs } -> List.exists (fun ps -> may_compats qs ps) pss)
ctx
let union pss qss = get_mins Row.le (pss @ qss)
end
let rec flatten_pat_line size p k =
match p.pat_desc with
| Tpat_any | Tpat_var _ -> Patterns.omegas size :: k
| Tpat_tuple args -> (List.map snd args) :: k
| Tpat_or (p1, p2, _) ->
flatten_pat_line size p1 (flatten_pat_line size p2 k)
| Tpat_alias (p, _, _, _, _, _) ->
(* Note: we are only called from flatten_matrix,
which is itself only ever used in places
where variables do not matter (default environments,
"provenance", etc.). *)
flatten_pat_line size p k
| _ -> fatal_error "Matching.flatten_pat_line"
let flatten_matrix size pss =
List.fold_right
(fun ps r ->
match ps with
| [ p ] -> flatten_pat_line size p r
| _ -> fatal_error "Matching.flatten_matrix")
pss []
(** A default environment (referred to as "reachable trap handlers" in the
paper) is an ordered list of [raise_num * matrix] pairs, mapping reachable
exit numbers to the matrices of the corresponding exit handler.
It is used to decide where to jump next if none of the rows in a given
matrix match the input.
In such situations, one thing you can do is to jump to the first (leftmost)
[raise_num] in that list (by doing a raise to the static-cach handler number
[raise_num]); and you can assume that if the associated pm doesn't match
either, it will do the same thing, etc.
This is what [mk_failaction_neg] (and its callers) does.
But in fact there is no point in jumping to a matrix if you can tell
statically that it cannot match your current input. Default environments
provide static information on what happens "after" each jump, which we use
to optimize our exit choices.
This is what [mk_failaction_pos] (and its callers) does.
*)
module Default_environment : sig
type t
val is_empty : t -> bool
val pop : t -> ((int * matrix) * t) option
val empty : t
val cons : matrix -> int -> t -> t
val specialize : Patterns.Head.t -> t -> t
val pop_column : t -> t
val pop_compat : pattern -> t -> t
val flatten : int -> t -> t
val pp : Format.formatter -> t -> unit
end = struct
type t = (int * matrix) list
(** All matrices in the list should have the same arity -- their rows should
have the same number of columns -- as it should match the arity of the
current scrutiny vector. *)
let empty = []
let is_empty = function
| [] -> true
| _ -> false
let cons matrix raise_num default =
match matrix with
| [] -> default
| _ -> (raise_num, matrix) :: default
let specialize_matrix arity matcher pss =
let rec filter_rec = function
| [] -> []
| (p, ps) :: rem -> (
let p = General.view p in
match p.pat_desc with
| `Alias (p, _, _, _, _, _) -> filter_rec ((p, ps) :: rem)
| `Var _ -> filter_rec ((Patterns.omega, ps) :: rem)
| `Or (p1, p2, _) -> filter_rec_or p1 p2 ps rem
| #Simple.view as view -> (
let p = { p with pat_desc = view } in
match matcher p ps with
| exception NoMatch -> filter_rec rem
| specialized ->
assert (List.length specialized = List.length ps + arity);
specialized :: filter_rec rem
)
)
(* Filter just one row, without a `rem` accumulator
of further rows to process.
The following equality holds:
filter_rec ((p :: ps) :: rem)
= filter_one p ps @ filter_rec rem
*)
and filter_one p ps =
filter_rec [ (p, ps) ]
and filter_rec_or p1 p2 ps rem =
match arity with
| 0 -> (
(* if K has arity 0, specializing ((K|K)::rem) returns just (rem):
if either sides works (filters into a non-empty list),
no need to keep the other. *)
match filter_one p1 ps with
| [] -> filter_rec ((p2, ps) :: rem)
| matches -> matches @ filter_rec rem
)
| 1 -> (
(* if K has arity 1, ((K p | K q) :: rem) can be expressed
as ((p | q) :: rem): even if both sides of an or-pattern
match, we can compress the output in a single row,
instead of duplicating the row.
In particular, filtering a single row (the filter_one calls)
returns a result that respects the following properties:
- "row count": the result is either an empty list or a single row
- "row shape": if there is a row in the result, it contains one
pattern consed to the tail [ps] of our input row; in particular
the row is not empty. *)
match (filter_one p1 ps, filter_one p2 ps) with
| [], row
| row, [] ->
row @ filter_rec rem
| [ (arg1 :: _) ], [ (arg2 :: _) ] ->
(* By the row shape property,
the wildcard patterns can only be ps. *)
(* The output below is a single row,
respecting the row count property. *)
({ arg1 with
pat_desc = Tpat_or (arg1, arg2, None);
pat_loc = Location.none
}
:: ps
)
:: filter_rec rem
| (_ :: _ :: _), _
| _, (_ :: _ :: _) ->
(* Cannot happen from the row count property. *)
assert false
| [ [] ], _
| _, [ [] ] ->
(* Cannot happen from the row shape property. *)
assert false
)
| _ ->
(* we cannot preserve the or-pattern as in the arity-1 case,
because we cannot express
(K (p1, .., pn) | K (q1, .. qn))
as (p1 .. pn | q1 .. qn) *)
filter_rec ((p1, ps) :: (p2, ps) :: rem)
in
filter_rec pss
let specialize_ arity matcher env =
let rec make_rec = function
| [] -> []
| (i, ([] :: _)) :: _ -> [ (i, [ [] ]) ]
| (i, pss) :: rem -> (
(* we already handled the empty-row case
so we know that all rows in pss are non-empty *)
let non_empty = function
| [] -> assert false
| p :: ps -> (p, ps)
in
let pss = List.map non_empty pss in
match specialize_matrix arity matcher pss with
| [] -> make_rec rem
| [] :: _ -> [ (i, [ [] ]) ]
| pss -> (i, pss) :: make_rec rem
)
in
make_rec env
let specialize head def =
specialize_ (Patterns.Head.arity head) (matcher head) def
let pop_column def = specialize_ 0 (fun _p rem -> rem) def
let pop_compat p def =
let compat_matcher q rem =
if may_compat p (General.erase q) then
rem
else
raise NoMatch
in
specialize_ 0 compat_matcher def
let pop = function
| [] -> None
| def :: defs -> Some (def, defs)
let pp ppf def =
Format.fprintf ppf
"@[<v 2>Default environment:@,\
%a@]"
(fun ppf li ->
if li = [] then Format.fprintf ppf "empty"
else
Format.pp_print_list ~pp_sep:Format.pp_print_cut
(fun ppf (i, pss) ->
Format.fprintf ppf
"Matrix for %d:@,\
%a"
i
pretty_matrix pss
) ppf li
) def
let flatten size def =
List.map (fun (i, pss) -> (i, flatten_matrix size pss)) def
end
(** For a given code fragment, we call "external" exits the exit numbers that
are raised within the code but not handled in the code fragment itself.
The jump summary of a code fragment is an ordered list of
[raise_num * Context.t] pairs, mapping all its external exit numbers to
context information valid for all its raise points within the code fragment.
*)
module Jumps : sig
type t
val is_empty : t -> bool
val empty : t
val singleton : int -> Context.t -> t
val add : int -> Context.t -> t -> t
val union : t -> t -> t
val unions : t list -> t
val map : (Context.t -> Context.t) -> t -> t
val remove : int -> t -> t
(** [extract exit jumps] returns the context at the given exit
and the rest of the jump summary. *)
val extract : int -> t -> Context.t * t
val pp : Format.formatter -> t -> unit
end = struct
type t = (int * Context.t) list
let pp ppf (env : t) =
if env = [] then Format.fprintf ppf "empty" else
Format.pp_print_list ~pp_sep:Format.pp_print_cut (fun ppf (i, ctx) ->
Format.fprintf ppf
"jump for %d@,\
%a"
i
Context.pp ctx
) ppf env
let rec extract i = function
| [] -> (Context.empty, [])
| ((j, pss) as x) :: rem as all ->
if i = j then
(pss, rem)
else if j < i then
(Context.empty, all)
else
let r, rem = extract i rem in
(r, x :: rem)
let rec remove i = function
| [] -> []
| (j, _) :: rem when i = j -> rem
| x :: rem -> x :: remove i rem
let empty = []
and is_empty = function
| [] -> true
| _ -> false
let singleton i ctx =
if Context.is_empty ctx then
[]
else
[ (i, ctx) ]
let add i ctx jumps =
let rec add = function
| [] -> [ (i, ctx) ]
| ((j, qss) as x) :: rem as all ->
if j > i then
x :: add rem
else if j < i then
(i, ctx) :: all
else
(i, Context.union ctx qss) :: rem
in
if Context.is_empty ctx then
jumps
else
add jumps
let rec union (env1 : t) env2 =
match (env1, env2) with
| [], _ -> env2
| _, [] -> env1
| ((i1, pss1) as x1) :: rem1, ((i2, pss2) as x2) :: rem2 ->
if i1 = i2 then
(i1, Context.union pss1 pss2) :: union rem1 rem2
else if i1 > i2 then
x1 :: union rem1 env2
else
x2 :: union env1 rem2
let rec merge = function
| env1 :: env2 :: rem -> union env1 env2 :: merge rem
| envs -> envs
let rec unions envs =