-
Notifications
You must be signed in to change notification settings - Fork 125
/
qmlPatternAnalysis.ml
1670 lines (1390 loc) · 59.6 KB
/
qmlPatternAnalysis.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
(*
Copyright © 2011 MLstate
This file is part of OPA.
OPA is free software: you can redistribute it and/or modify it under the
terms of the GNU Affero General Public License, version 3, as published by
the Free Software Foundation.
OPA is distributed in the hope that it will be useful, but WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
FOR A PARTICULAR PURPOSE. See the GNU Affero General Public License for
more details.
You should have received a copy of the GNU Affero General Public License
along with OPA. If not, see <http://www.gnu.org/licenses/>.
*)
(*
NOT UP TO DATE JUNK :
Strict case and non strict case are of different nature (the size is not known in the latter case).
We try to elminate unstrict case when possible
Remaining unstrict case
We do the strict case analysis and non strict separately
Or of And normalisation :
First we regroup all case on the strict together,
for this we need to be able to make them go before non strict case, this is done by duplicating them.
Non strict case are gives a set of strictified version (merge with strict cases) and a the original one
Strict record case (including previously generated one) are regroup (order of group has no importance).
All non strict record case in kept in the original order
e.g. cases are re-organised as follow :
match ...
{ toto=1 } -> case1
{ toto=2 bibi=3 } -> case2
{ bibi=4 ... } -> case3
{ toto=5 ... } -> case4
=>
failure = ...
match ...
{ toto = x } -> match x | 1 -> case1'
| 5 -> case4'
end
{ bibi = x bibi = y } -> match x | 2 -> match y | 3 -> case2'
end
| 4 -> case3'
end
{ bibi=x ... } -> match x | 4 -> case3' end
{ toto=x ... } -> match x | 5 -> case4' end
This help to regroup all complete case, case code can be shared or not depending of the low level implementation
Algorithm
regroup all strict possible cases (fields,bool) keeping intra-order information
strictify non strict case on the basis of existing strict case
Or of const are given a default case with Failure code
*)
(* depends *)
let (|>) = InfixOperator.(|>)
module Format = Base.Format
module List = Base.List
module RecordIndex =
struct
open Loop.Deprecated
module Array = BaseArray
type ('a,'b) index =
{
keys : 'a array;
values : 'b array;
map : IntSet.t StringMap.t;
size : IntSet.t IntMap.t;
}
let (|?) a b = match a with
| Some a -> a
| None -> b
let create entities key value =
let entities = Array.of_list entities in
let keys = Array.map key entities in
let values = Array.map value entities in
let map,size = Array.fold_left_i (fun (map,size) fields id ->
let size = IntMap.update_default (List.length fields) (IntSet.add id) (IntSet.singleton id) size in
let map = l_fold(fields,map)(fun field map ->
StringMap.update_default field (IntSet.add id) (IntSet.singleton id) map
) in map,size
) (StringMap.empty,IntMap.empty) keys
in
(*
StringMap.iter (fun field v ->
Format.printf "Field %s -> {%a}\n" field (Format.pp_list "," Format.pp_print_int) (IntSet.elements v)
) map;
IntMap.iter (fun d v ->
Format.printf "Size %d : {%a}\n" d (Format.pp_list "," Format.pp_print_int) (IntSet.elements v)
) size;*)
{ keys; values; map; size}
(* is ok with slow and stupid intersection but could benefit from better intersection than a fold *)
let get_case strict fields index =
let map = index.map in
let size = index.size in
let to_list index set = IntSet.fold (fun id list -> index.values.(id)::list) set [] in
try match fields with
| [] -> if strict then to_list index (IntMap.find 0 size) else Array.to_list index.values
| hd :: tl ->
let len = List.length tl + 1 in
let set = l_fold(tl,StringMap.find hd map)(fun field set->
IntSet.inter set (StringMap.find field map)
) in
let set = if strict then IntSet.inter set (IntMap.find len size) else set in
to_list index set
with Not_found -> []
end
(* refactoring in progress *)
(* shorthands *)
module Q = QmlAst
open Loop.Deprecated
let debug_flag = false
let debug fmt =
Format.printf "%!";
if debug_flag then Format.printf fmt
else Format.ifprintf Format.std_formatter fmt
(* checking that a list is ordered and with no duplicate *)
let rec ordered l =
match l with
| x :: y :: rl ->
if x<y then ordered rl
else if y>x then failwith "not sorted"
else failwith "duplicate"
| _ -> true
(* same on assoc list *)
let rec ordered2 l =
match l with
| (x,_) :: (y,_) :: rl ->
if x<y then ordered2 rl
else if y>x then failwith "not sorted"
else failwith "duplicate"
| _ -> true
(* a check function returning the list for debug purpose *)
let check l =
if not( ordered2 (List.rev l)) then (
Printf.printf "%s\n%!" (String.concat "," (List.map fst l));
assert false
);
l
(* collect all field of strict not appearing in nonstrict (case A) and
verify that all nonstrict field are in strict (case B) *)
let rec fields_completion (gen:string->'a) (strict:string list) (nonstrict:(string*'a) list) res =
assert(ordered strict);
assert(ordered2 nonstrict);
(* Printf.printf "\n[";
l_iter(strict)(Printf.printf "%s ");
Printf.printf "\n[";
l_iter(nonstrict)(fun (f,_)->Printf.printf "%s "f);
Printf.printf "]\n";
*)
let rec aux strict nonstrict res =
match strict,nonstrict with
(* A *)
| f0::strict, (f1,_)::_ when f0<f1 -> aux strict nonstrict (check((f0,gen f0)::res))
| f0::strict, [] -> aux strict nonstrict (check((f0,gen f0)::res))
| f0::strict, (f1,o)::nonstrict when f0=f1 -> aux strict nonstrict (check((f1,o )::res))
(* terminaison *)
| [], [] -> Some (List.rev res)
(* B *)
| f0::_ , (f1,_)::_ when f0>f1 -> None
| [] , _::_ -> None
(* ocaml [stupid] complain *)
| _::_ , _::_ -> assert false
in
let res = aux strict nonstrict res in
assert(Option.default true (Option.map ordered2 res));
res
module Onion ( Lang : QmlPatternAnalysisSig.ONIONLANG) =
struct
module L = Lang
type field = string
type bind = { ident : L.ident list ; coerce_ty : L.ty list} (* standard binding, support name and coercion *)
(*
type switch = Const | NoField | Immediate IsRecord_0 IsPrt
*)
(** immediate, checkable property *)
type pat =
| Any (* the easy property, equivalent exist for fields, see And *)
| Cst of L.const (* constant property *)
(* | Rec of ('bind) layer_record (* set of field property *) *)
(* | Backend of 'backend_property *)
(** composition of checkable properties *)
type onion =
(** basic algebra *)
| Or of onion_or (* to match sum *)
| And of onion_and (* to match record *)
| Term of onion_term (* terminal *)
(** pattern disjunction *)
and onion_or =
{
cases : onion list ; (* list of patterns *)
default : onion_term option; (* the pattern is useless *)
ty : L.ty option ; (* sadly we have to use type to limits presence of '...' and determines completness *)
}
(** pattern conjunction, each conjunction operand is actually associated to a field, but can be extended to any conjuction kind *)
and onion_and =
{
fields : (field*onion) list ; (* check are associated to field *)
strict : bool ; (* pattern contains ... *)
term : onion_term ; (* binded recursion, the pattern is useless !! *)
}
(** terminal pattern
binding occurs and submatch occurs here
*)
and onion_term =
{
bind : bind; (* bind names and coerce *)
pat : pat ; (* the terminal patern *)
content : recur; (* recursion, can content the final expr or an explicit submatch *)
}
(** expression and submatch *)
and recur =
Expr of L.expr
| Failure of string
(* the latter two should be replaced by Branch x where
x is the number of the branch of the whole pattern matching (i.e. code are numbered)
*)
| End (* to fill holes for parten without expr or submatch *)
(* to nest pattern explicit tree form pattern matching,
during optimisation, normalisation ...
ident is the input value of pattern matchin
or a sentinel value to indicate that joint pattern matching must be continuated
*)
| Recur of L.ident * L.ty option * onion
(* | BranchSet of IntSet.t
| Branch of int (* int > 0 *)
| JointSet of integer list *)
(**
Add a binding to an onion
*)
let add_bind ident bind =
{ bind with
ident = ident :: bind.ident
}
let add_bind_term ident term =
{ term with
bind = add_bind ident term.bind ;
}
let add_bind_onion ident = function
| Or _ ->
(*
TODO
Currently, this is not implemented, even in qml
*)
assert false
| And onion_and ->
let onion_and = {
onion_and with
term = add_bind_term ident onion_and.term ;
} in
And onion_and
| Term term -> Term (add_bind_term ident term)
(** getting and_ in And and_ *)
let get_and =
function And and_ -> and_
| Or _
| Term _ -> raise (Invalid_argument "get_and")
(** getting term in Term term *)
let get_term =
function Term term-> term
| And _ -> assert false
| Or _ -> assert false
(** getting the term in Term term, And { term=term } *)
let get_onion_term =
function Term term | And { term = term } -> term
| Or _ -> assert false
let get_fields =
function And { fields = fields} -> fields
| _ -> []
(** some handy constructors *)
let bind ?(id=[]) ?(ty=[]) () = {ident=id;coerce_ty=ty}
let bind_var i = bind ~id:[i] ()
let no_bind = bind ()
let term_r ?(bind=no_bind) ?(pat=Any) ?(e=End) ()= {bind=bind;pat=pat; content=e}
let term ?(bind=no_bind) ?(pat=Any) ?(e=End) () = Term (term_r ~bind ~pat ~e ())
let term_var i= term ~bind:(bind_var i) ()
let no_term_r = term_r ()
let no_term = term ()
(** A S2 module for basic needs *)
module S2 = struct
type 'p t = onion constraint 'p = (_ * _ * _)
let stable2 a a' b b' = a==a' && b==b'
let snd_fold_map tra acc ((a,b) as c) =
let acc,b' =tra acc b in
acc,if b'==b then c else (a,b')
let fold_map_recur tra acc r =
match r with
| Recur (id,ty,o) ->
let acc, o' = tra acc o in
if o'==o then acc,r else acc,Recur(id,ty,o')
| _ -> acc,r
let foldmap tra acc o =
match o with
| Or { cases=cases ; default=default ; ty = ty} ->
let acc, cases' = List.fold_left_map_stable tra acc cases in
let acc, default' = Option.foldmap_stable (fun acc d->
let acc,c'=fold_map_recur tra acc d.content in
if c'==d.content then acc,d
else acc, {d with content=c'}
) acc default
in
acc, if stable2 cases cases' default default' then o else Or {cases=cases' ; default=default' ; ty = ty }
| And ({ fields= fields ; term = { content=content } as term } as and_) ->
let tra_field = snd_fold_map tra in
let acc, fields' = List.fold_left_map_stable tra_field acc fields in
let acc, content' = fold_map_recur tra acc content in
acc, if stable2 fields fields' content content' then o else And { and_ with fields= fields' ; term = { term with content=content' } }
| Term ({content=content} as term) ->
let acc, content' = fold_map_recur tra acc content in
acc, if content'==content then o else Term {term with content=content'}
let iter x = Traverse.Unoptimized.iter foldmap x
let map x = Traverse.Unoptimized.map foldmap x
let fold x = Traverse.Unoptimized.fold foldmap x
end
module Trav = Traverse.Make2( S2 )
(** printers for external types *)
let print_id = Lang.print_id
let print_ty = Lang.print_ty
let print_expr = Lang.print_expr
let print_const = Lang.print_const
(** printers for internal types *)
let rec print_recur fmt r =
match r with
| End -> ()
(* | JointSet s-> Format.fprintf fmt "@[{%a}@]" (Format.pp_list " , " Format.pp_print_int) s *)
| Failure(str) -> Format.fprintf fmt " Failure : %s" str
| Recur (f,_ty,r) -> Format.fprintf fmt "@\n@[@<2>match @[%a@] @\n @[%a@] @\nend@]@\n" print_id f print r
| Expr e -> Format.fprintf fmt "@[@ %a@]" print_expr e
and print_pat ~show_pat fmt pat =
match pat with
| Any -> Format.pp_print_string fmt (if show_pat then "_" else "")
| Cst c -> print_const fmt c
and print_term ~show_pat fmt t =
let { bind = { ident = il; coerce_ty = tyl }; pat = pat ; content = r } = t
in
Format.fprintf fmt "%a%s%a%s%a%s%a"
(print_pat ~show_pat) pat
(if il = [] || pat<>Any then "" else " as ") (Format.pp_list "," print_id) il
(if tyl= [] then "" else " : " ) (Format.pp_list "," print_ty) tyl
(if r=End then "" else "->") print_recur r
and print_field fmt (field , o ) = Format.fprintf fmt "@[@ %s = %a @]" field print o
and print fmt o =
match o with
| Or {cases=l1 ; default=opt} ->
Format.fprintf fmt "@[@ [ %a %a %a ] @]"
(Format.pp_list "@\n" print) l1
(fun f o-> if o then Format.fprintf f "@\n #") (opt<>None (*&& l1<>[]*))
(fun f o -> Option.iter (print_term ~show_pat:true f) o) opt
| And {fields=fs ; strict=b; term=term} ->
Format.fprintf fmt "AND {@[%a %s@]} %a" (Format.pp_list " ;@ " print_field) fs (if b then "" else "; ... ") (print_term ~show_pat:false) term
| Term t -> Format.fprintf fmt "@[T %a@]" (print_term ~show_pat:true) t
(* short and precise pattern are smaller,
slow because of fields comparison
*)
let compare p1 p2 =
match p1,p2 with
| Or _ , _ -> assert false
| _ , Or _ -> assert false
| Term {pat = Cst x}, Term {pat = Cst y} -> compare x y
| _, Term {pat = Cst _} -> -1
| And { fields = fields1; strict=strict1 }, And { fields = fields2; strict=strict2 }
->
if strict1 = strict2 then (
let len1 = List.length fields1 in
let len2 = List.length fields2 in
if len1 = len2 then
compare (List.map fst fields1) (List.map fst fields2)
else
compare len1 len2
) else
if strict1 then -1 else 1
| _,And _ -> -1
| Term { pat = Any} , Term { pat = Any} -> 0
| _ , Term { pat = Any} -> -1
let update_End new_ =
(* no information loss *)
let aux tra o =
match o with
| And( { term = { content = End} as recur } as and_ ) -> And { and_ with term = { recur with content = new_ }}
| Term( { content=End } as term) -> Term {term with content= new_ }
| And _ -> assert false
| Term _ -> assert false
| _ -> tra o
in Trav.traverse_map aux
(* never traverse term *)
let update_First_Term new_ =
(* accept information loss *)
let aux tra o =
match o with
| And( { term = { content = _ } as recur } as and_ ) -> And { and_ with term = { recur with content = new_ }}
| Term( { content = _ } as term) -> Term {term with content= new_ }
| _ -> tra o
in Trav.traverse_map aux
let add_ty_in_term ty o=
let add_ty_bind ty bind = {bind with coerce_ty = ty::bind.coerce_ty} in
let add_ty_term ty term = {term with bind = add_ty_bind ty term.bind } in
let add_ty_and_ ty and_ = {and_ with term = add_ty_term ty and_.term } in
match o with
| And and_ -> And (add_ty_and_ ty and_)
| Term term -> Term (add_ty_term ty term)
| _ -> assert false
module Normalize = struct
type rpath = field list (* reversed path *)
type public_exception =
| Any_before_last_pattern (* any pattern not in last position, merge with hiding *) (* not used *)
| Missing_const_case of rpath * L.const list (* incomplete disjonction of constant *)
| Missing_record_class of rpath * (field list) list
| Pattern_hidding of recur list
| Pattern_incompletness of onion list (* only possible with types or jointures ?? *) (* not used *)
type private_exception =
| Empty_pattern
| Non_homogenious
type exceptions = Public of public_exception | Private of private_exception
exception Exc of exceptions list
(** exceptions :
public exception are collected, there are actually displayed when flush_exceptions is called,
the purpose is emission of warning messages
private exception means internal error, so you should only call them when you feel like something more specific then assert false
currently they are just raise as other exceptions
*)
let ref_public_exception = ref []
let raise_public e = ref_public_exception := (Public e)::(!ref_public_exception)
let has_public_exceptions () = !ref_public_exception<>[]
let clean_public_exceptions () = ref_public_exception:=[]
let nb_failure = ref 0
let nb_total = ref 0
let raise_private e = raise (Exc[Private e])
let print_record_class fmt l = Format.fprintf fmt "{%a}" (Format.pp_list " ; " Format.pp_print_string) l
let print_rpath fmt rpath =
if rpath = [] then
Format.fprintf fmt "in the whole pattern"
else
Format.fprintf fmt "in the path %a" (Format.pp_list "." Format.pp_print_string) (List.rev rpath)
let print_public_exc fmt = function
| Any_before_last_pattern -> Format.fprintf fmt "Any_before_last_pattern"
| Missing_const_case(rpath,lc) ->
Format.fprintf fmt "Incomplete constant pattern matching : %a, %a %s" print_rpath rpath (Format.pp_list " and " print_const) lc
(if List.length lc = 1 then "constant case is missing"
else "constants case are missing")
| Missing_record_class(rpath,lclass) ->
Format.fprintf fmt "Incomplete record pattern matching : %a, %a %s" print_rpath rpath (Format.pp_list " and " print_record_class) lclass
(if List.length lclass = 1 then "record layout is missing"
else "records layout are missing")
| Pattern_hidding _lr ->
Format.fprintf fmt "Pattern hidding" (*"before expression %a" (Format.pp_list " ;@ " print_recur) lr*)
| Pattern_incompletness _lo -> Format.fprintf fmt "Pattern incompletness TODO" (*(Format.pp_list " ;@ " print_recur) lr*)
let print_private_exc fmt = function
| Empty_pattern -> Format.fprintf fmt "Empty pattern"
| Non_homogenious -> Format.fprintf fmt "Non homogenious pattern"
let print_exc fmt e =
match e with
| Public e -> print_public_exc fmt e
| Private e -> print_private_exc fmt e
let flush_exceptions_fmt fmt () =
Format.pp_list "@\n" print_exc fmt (List.rev !ref_public_exception);
clean_public_exceptions ()
let flush_exceptions_stdout () = flush_exceptions_fmt Format.std_formatter ()
(* usefull to avoid nested Or *)
let rec flatten_or cases =
l_map_flat(cases)(function
| Or { cases = l ; default = None } -> l
| Or { cases = l ; default = Some d} -> (flatten_or l)@[Term d]
| x -> [x]
)
(* this function is really linked to the normalisation !! and should be nearer the normalisation *)
let get_pattern_for_field ty record_name f (and_pattern:onion) =
match and_pattern with
| And ({ fields = fields } as and_) ->
let remainings_fields = List.remove_assoc f fields in
let _recur = if remainings_fields=[] then and_.term.content else Recur(record_name,ty, And {and_ with fields = remainings_fields }) in
(* hack : use the intra-pattern term container to memorise its origin, so that latter the correspondance is not lost *)
begin match List.assoc_opt f fields with
| Some p -> Some (update_End _recur p)
| None ->
Format.printf "get_pattern_for_field %s %a@\n%!" f print and_pattern;
Format.printf "BUG@\n%!";
None
end
| _ -> Format.printf "get_pattern_for_field %s %a@\n%!" f print and_pattern; assert false
let get_patterns_for_field ty record_name f and_patterns = List.filter_map (get_pattern_for_field ty record_name f) (flatten_or(* TODO remove the flatten*) and_patterns)
(* make the pattern only active on the first layer *)
let strip_pattern ?(keep_list=[]) o =
match o with
| And( { fields= fields } as and_ ) -> And { and_ with fields = l_map(fields)(fun (f,o)-> if List.mem_assoc f keep_list then f,o else f, term()) }
| Term term -> Term {term with bind=no_bind; pat = Any }
| _ -> o
let get_names_and_types_1 o (names,tys) =
match o with
| Term { bind = { ident = li ; coerce_ty = lt } }
| And {term = { bind = { ident = li ; coerce_ty = lt } } } -> (li@names, lt@tys)
| _ -> assert false
module PatternClass = struct
(**
pattern classes are a sum-up of the first layer of a pattern
a pattern is said strict (or belongs to a strict class) if its first layer does not contains forms like '_' or '...'
*)
(**
The type of pattern classes
'...' in records are just discarded since classes will always be separate into sets of strict and non strict classes
and non strict record classes always have '...'
*)
type t = CRECORD of string list | CST of L.const | ANY
let print_class fmt t =
match t with
| CRECORD l -> Format.fprintf fmt "CRECORD(%s)" (String.concat ";" l)
| CST c -> Format.fprintf fmt "CST(%a)" print_const c
| ANY -> Format.fprintf fmt "ANY"
(** gives the class of a pattern *)
let from_pattern p =
match p with
| Or _ -> assert false
| Term { pat = Cst c} -> CST c
| And and_ ->
assert(ordered2 and_.fields);
CRECORD(List.map fst and_.fields)
| Term { pat = Any } -> ANY
(** check strictness of a pattern *)
let is_strict p =
match p with
| Or _ -> assert false
| And { strict = strict } -> strict
| Term { pat = Any } -> false
| _ -> true
(** is_instance_of *)
let is_instance_of ~candidate ~class_ =
match candidate,class_ with
| CRECORD candidate, CRECORD class_ -> candidate=class_
| _ -> assert false
(** is_unstrict_instance_of *)
let is_unstrict_instance_of ~candidate ~class_ =
match candidate,class_ with
| CRECORD candidate, CRECORD class_ ->
l_for_all(candidate)(fun f -> List.mem f class_)
| _ -> assert false
(** class comparison *)
let compare p1 p2 = (* most generic pattern are superior to other *)
match p1,p2 with
| ANY, ANY -> 0
| ANY, _ -> 1
| CRECORD l0, CRECORD l1 -> Pervasives.compare l0 l1
| CRECORD _ , CST _ -> 1
| CST c0 , CST c1 -> Pervasives.compare c0 c1
| _ -> -1
(** non typed strictification *)
let strictify_record_class strict nonstrict = fields_completion (fun _ ->term()) strict nonstrict []
(** from fields of a non strict instance pattern, and a strict class
eventually return a strict pattern instanciated from the non strict pattern and belonging to the strict class
if such a pattern exists
new fields in the pattern are associated to an Any pattern
*)
let strictify_pattern_class strict_class p =
match strict_class,p with
| CRECORD cfields, And and_ ->
Option.map (fun fields -> And { and_ with fields = fields})
(strictify_record_class cfields and_.fields)
| CRECORD cfields, Term ({ pat = Any } as term) ->
Option.map (fun fields -> And {fields = fields ; strict = true ; term = term})
(strictify_record_class cfields [])
| CST c, Term ({ pat = Any } as term) -> Some (Term ({term with pat = Cst c}))
| CST _, And _ -> None
| _ , Term { pat = Cst _ } (* Cst cannot be unstrict *)
| ANY , _ (* ANY is not a strict class *)
| _ , Or _
-> assert false
(** typed strictification, superior to the latter but need type information *)
let strictify_record_ty ty field_p_l term_ =
let fields = List.map fst field_p_l in
let ands_ = l_map(L.strictify_record_ty ty fields)(fun (fields,strict)->
let fields_o = l_map(fields)(fun field ->
match List.assoc_opt field field_p_l with
| None ->
debug "strictify_record_ty : missing %s replaced by any @\n" field;
(field,term ())
| Some o -> (field,o)
) in
And {fields = fields_o ; strict= strict = `closed ; term = term_}, CRECORD fields
) in
ands_
(** typed strictification, superior to the latter but need type information *)
let strictify_pattern_ty ty p =
match p with
| And and_ when not(and_.strict) -> strictify_record_ty ty and_.fields and_.term
| Term ({ pat = Any } as term) ->
debug "Strictify Any strictify_pattern_ty @\n";
let r = strictify_record_ty ty [] term in
if r<>[] then r
else (* for the any case with const type *)
[p, from_pattern p]
| _ ->
debug "strictify_pattern_ty: %a @\n" print p;
assert false
let get_class_fields class_ =
match class_ with
| CRECORD cfields -> cfields
| _ -> assert false
(* here start the real stuff, move this outside of PatternClass *)
exception Local_no_recur
(* TODO Document *)
let class_merge new_ident _is_joint strict ty =
let get_field_type = match ty with
| None -> (fun _ _ -> None)
| Some ty ->
let get = L.strict_get_field_type ty in
(fun fields -> let get = get fields in fun field -> Some(get field))
in
fun (c,l) ->
let strip_names_1 o =
match o with
| Term t -> Term { t with bind = {t.bind with ident =[]}}
| _ -> o
in
let get_names_and_types and_patterns f = (* get all existing coercions and names for the field *)
l_fold(and_patterns,([],[]))(fun and_pattern acc ->
let and_ = get_and and_pattern in
get_names_and_types_1 (List.assoc f and_.fields) acc
)
in
let get_recur (l as initl) =
let id,l = l_fold(l,(None,[]))(fun pat (id,l) ->
match pat with
| Term { content = Recur(id',_,o) }
| And { term = { content = Recur(id',_,o) } } ->
assert( Option.default_map true (fun id-> id=id') id );
((Some id'),o::l)
| _ -> debug "ASSERT get_recur: %a\n" (Format.pp_list " |@\n " print) initl; raise Local_no_recur
) in Recur(Option.get id,ty, if List.length l > 1 then Or { cases = List.rev l ; default=None ; ty=ty} else List.hd l)
in
debug "class_merge %a\n" print_class c;
let recurs = try Some(get_recur l) with Local_no_recur -> None in
let ext_ty tys = match ty with None -> tys | Some ty -> ty::tys in
match c with
| CRECORD fields when fields<>[] ->
let get_field_type = get_field_type fields in
let id = new_ident "record_to_recurse" in
let fields_idents_types = l_map(fields)(fun field -> field, new_ident field, get_field_type field) in
let fields = l_map(fields_idents_types)(fun (f,name,ty)->
let names,tys = get_names_and_types l f in
let tys = match ty with None -> tys | Some ty -> ty::tys in
(f,term ~bind:(bind ~id:(name::names) ~ty:tys ()) ())
) in
begin match recurs with
| Some e when false ->
let o = And { fields=fields; strict=strict ; term=term_r ~bind:(bind ~ty:(ext_ty [])()) ~e () } in
debug "\n\nMerging in %a\n\n" print o;
Some(id,fields_idents_types),[], o
| _ ->
(* the first layer of patterns should be cleaned from bindings since we get them in the main pattern *)
let l = l_map(l)(strip_names_1) in
let names,tys = l_fold(l, ([],[]) )(get_names_and_types_1) in
Some(id,fields_idents_types),l,And { fields=fields; strict=strict ; term=term_r ~bind:(bind ~id:names ~ty:(ext_ty tys)()) () }
end
| _ -> (* includes const, any and {} *)
begin match recurs with
| Some e -> (* matching will continue, so we must not discard patterns *)
if List.length l > 1 then debug "\n\nKeeping usefull patterns because joint %a\n\n" (Format.pp_list "|" print) l;
let pat = match List.hd l with Term {pat=pat} -> pat | And { fields = [] } -> Any | _ -> assert false in
let id,tys = l_fold(l,([],[]))(get_names_and_types_1) in
debug "\n\nMerging in %a\n\n" print_recur e;
let o = term ~bind:(bind ~id ~ty:(ext_ty tys) ()) ~pat ~e () in
debug "\n\nFinal %a\n\n" print o;
None,[], o
| _ -> (* no pending pattern, we can safely discard useless pattern *)
let discarded = List.tl l in
if discarded <> [] then debug "\n\nDiscarding B immediate useless patterns %a\n\n" (Format.pp_list "|" print) l;
let case = List.hd l in
let case = match ty with None -> case | Some ty -> add_ty_in_term ty case in
None,[],case
end
end
(* partition any patterns *)
let extract_any ol =
List.partition (function
| _, Term { pat=Any } -> true
| _ -> false
) ol
(* partition unstrict patterns *)
let extract_unstrict ol =
List.partition (function
| _, And { strict=false} -> true
| _ -> false
) ol
let add_i i l = List.map (fun j->i,j) l
let add_i_fst i l = List.map (fun j->i,fst j) l
(*
dispatch pattern by class, no specific order on pattern
should be call on separate pattern group,
strict, unstrict, any
*)
let rec class_layer ol =
let hash_add h (k,v) =
let l = try Hashtbl.find h k with Not_found -> [] in
Hashtbl.replace h k (v::l)
in
let hash_pop h (k,_) =
try
let l = Hashtbl.find h k in
Hashtbl.remove h k;
Some(k,List.rev l)
with Not_found -> None
in
let class_o = l_map(ol)(fun o->PatternClass.from_pattern o,o) in
let classes = Hashtbl.create (List.length class_o) in
l_iter(class_o)(hash_add classes);
let classes_patterns = l_filter_map(class_o)(hash_pop classes) in
classes_patterns
and simplify_recur recur =
debug "\n\n--------------------------------------------------------------------------------------Try to simplify %a \n%!" print_recur recur;
match recur with
| Recur (_,_, And { fields = [] ; term = { bind = { ident = [] ; coerce_ty = [] } ; content = c }} )
| Recur (_,_, Term { pat = Any ; bind = { ident = [] ; coerce_ty = [] } ; content = c } )
-> c
| _ -> recur
and recurse_on new_ident ~path recurse_todo (o:onion) =
match recurse_todo with
| [] -> (
match o with
| Or { cases = [o] ; default = None } -> o
| _ -> o
)
| (_id,[])::rl -> recurse_on new_ident ~path:(List.tl path) rl o
| (id, ((field,field_ident,ty) :: fields ) )::rl ->
debug "Recursion on record %a field %s\n" print_id id field;
let submatches = recurse_on_field_and_recurse new_ident ~path:(List.tl path) rl id field field_ident fields ty o in
let r = update_First_Term (simplify_recur (Recur(field_ident,ty,submatches))) o in
debug "\nA BEFORE %a\nAFTER %a" print o print r;
r
and recurse_on_field_and_recurse new_ident ~path recurse_todo id field field_ident other_fields (ty:'a option) o =
let transform id field _field_ident and_patterns other_fields (ty: 'a option) =
debug "transform: args %s %a\n" field print (Or {cases=and_patterns;default=None;ty=ty});
let (field_patterns:onion list) = get_patterns_for_field ty id field and_patterns in
debug "transform: Patterns %a\n" print (Or {cases=field_patterns;default=None;ty=ty});
debug "transform: Type extraction TODO\n";
(* inject the next recursion *)
let recurse_todo = if other_fields=[] && recurse_todo=[] then [] else (id,other_fields)::recurse_todo in
or_cases ~path:(field::path) ~recurse_todo:recurse_todo ty new_ident field_patterns
in
(* find the recur node to recurse on *)
(* Recur(id,Or { cases } ) *)
let map tra o = match o with
| ( Term { content = Recur( _continue_record_ ,_ty, ands_ ) }
| And { term = { content = Recur( _continue_record_ ,_ty ,ands_) }})
when _continue_record_== id ->
debug "Continue on sub record %a with field %s\n" print_id id field;
let r =
begin match ands_ with
| Or { cases = ands_} -> transform id field field_ident ands_ other_fields ty
| And _ -> transform id field field_ident [ands_] other_fields ty
| _ -> (debug "ASSERT FAILURE %a \n%!"print ands_ ; assert false)
end
in r
| _ -> tra o
in Trav.traverse_map map o
and strictify_record ty nonstrict =
nonstrict
|> List.map (fun (i,pat) -> add_i_fst i (PatternClass.strictify_pattern_ty (Option.get ty) pat))
|> List.flatten
|> List.partition (fun (_,p) -> PatternClass.is_strict p)
and strictify_const const_pats nonstrict =
let class_pats = List.map (fun (_i,pat) -> PatternClass.from_pattern pat ) const_pats in
nonstrict
|> List.map (fun (i,pat) ->
add_i i (List.filter_map (fun class_pat -> PatternClass.strictify_pattern_class class_pat pat) class_pats)
)
|> List.flatten
and or_cases ~path ?(recurse_todo=[]) ty new_ident cases =
let need_to_recurse =
let rec aux r = match r with [] -> false | (_,[])::r -> aux r | _ -> true in aux recurse_todo
in
let cases = flatten_or cases in
(* when well tested 1) and 2) should be merged for speed reason *)
let is_and_cases = List.for_all (function And _ -> true | Term { pat = Any } -> true | _ -> false) cases in
let is_const_cases = List.for_all (function Term { pat = Cst _ }-> true | Term { pat = Any } -> true | _ -> false) cases in
assert(is_const_cases || is_and_cases);
(* 0) we number patterns to have retrieve the right when remerging separated cases *)
let cases = List.mapi (fun i p -> (i,p)) cases in
(* 1) separate patterns in 3 groups, strict, unstrict (contains ...), any *)
let any,mix = extract_any cases in
let unstrict,strict = extract_unstrict mix in
if debug_flag then (
debug "\n\nStrict : %a\n\n" (Format.pp_list "|" print) (List.map snd strict);
debug "\n\nUnstrict : %a\n\n" (Format.pp_list "|" print) (List.map snd unstrict);
debug "\n\nAny : %a\n\n" (Format.pp_list "|" print) (List.map snd any);
);
(* 2) pattern completion
detect incomplete pattern on the first layer 'any's appart,
if complete then any patterns are discarded,
if not a 'any' pattern is introduced
*)
let any =
debug "TODO : I should do completion verification here\n";
(* completion verification *)
let missing() = if is_const_cases then
let missings= if strict = [] then (assert (any<>[]); [] ) else L.get_missing (List.map (function _,Term {pat = Cst c} -> c | _ -> assert false) strict) in
if missings <> [] || strict = [] then (
let exc = Missing_const_case(path,missings) in
Some exc
) else None
else (
let ty_classes = L.strictify_record_ty (Option.get ty) [] in
let ty_classes = l_map(ty_classes)(fun (l,s)->PatternClass.CRECORD l,s) in
let strict_classes = l_map(strict)(fun (_,p)->PatternClass.from_pattern p) in
let unstrict_classes = l_map(unstrict)(fun (_,p)->PatternClass.from_pattern p) in
let remaining_ty_classes = l_fold(ty_classes,[])(fun (class_,_strictness) remainings->
let ty_class_covered_by_pattern_class =
List.exists (fun candidate -> PatternClass.is_instance_of ~candidate ~class_) strict_classes
|| List.exists (fun candidate -> PatternClass.is_unstrict_instance_of ~candidate ~class_) unstrict_classes
in
if ty_class_covered_by_pattern_class
then remainings
else class_::remainings
) in
debug "remaining classes %a" (Format.pp_list " ++ " PatternClass.print_class) remaining_ty_classes;
if remaining_ty_classes <> [] then (
let remaining_ty_classes = List.sort PatternClass.compare remaining_ty_classes in
let exc = Missing_record_class(path,l_map(remaining_ty_classes)(function PatternClass.CRECORD l -> l | _ -> assert false)) in
Some exc)
else None
) in
if any <> [] then any
else match missing() with
| Some exc ->