forked from rems-project/sail
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathrewrites.ml
4523 lines (4142 loc) · 206 KB
/
rewrites.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
(**************************************************************************)
(* Sail *)
(* *)
(* Copyright (c) 2013-2017 *)
(* Kathyrn Gray *)
(* Shaked Flur *)
(* Stephen Kell *)
(* Gabriel Kerneis *)
(* Robert Norton-Wright *)
(* Christopher Pulte *)
(* Peter Sewell *)
(* Alasdair Armstrong *)
(* Brian Campbell *)
(* Thomas Bauereiss *)
(* Anthony Fox *)
(* Jon French *)
(* Dominic Mulligan *)
(* Stephen Kell *)
(* Mark Wassell *)
(* *)
(* All rights reserved. *)
(* *)
(* This software was developed by the University of Cambridge Computer *)
(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *)
(* (REMS) project, funded by EPSRC grant EP/K008528/1. *)
(* *)
(* Redistribution and use in source and binary forms, with or without *)
(* modification, are permitted provided that the following conditions *)
(* are met: *)
(* 1. Redistributions of source code must retain the above copyright *)
(* notice, this list of conditions and the following disclaimer. *)
(* 2. Redistributions in binary form must reproduce the above copyright *)
(* notice, this list of conditions and the following disclaimer in *)
(* the documentation and/or other materials provided with the *)
(* distribution. *)
(* *)
(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *)
(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *)
(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *)
(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *)
(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *)
(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *)
(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *)
(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *)
(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *)
(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *)
(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *)
(* SUCH DAMAGE. *)
(**************************************************************************)
module Big_int = Nat_big_num
open Ast
open Ast_util
open Type_check
open Spec_analysis
open Rewriter
let (>>) f g = fun x -> g(f(x))
let fresh_name_counter = ref 0
let fresh_name () =
let current = !fresh_name_counter in
let () = fresh_name_counter := (current + 1) in
current
let reset_fresh_name_counter () =
fresh_name_counter := 0
let fresh_id pre l =
let current = fresh_name () in
Id_aux (Id (pre ^ string_of_int current), gen_loc l)
let fresh_id_exp pre ((l,annot)) =
let id = fresh_id pre l in
E_aux (E_id id, (gen_loc l, annot))
let fresh_id_pat pre ((l,annot)) =
let id = fresh_id pre l in
P_aux (P_id id, (gen_loc l, annot))
let get_loc_exp (E_aux (_,(l,_))) = l
let gen_vs (id, spec) = Initial_check.extern_of_string dec_ord (mk_id id) spec
let annot_exp_effect e_aux l env typ effect = E_aux (e_aux, (l, mk_tannot env typ effect))
let annot_exp e_aux l env typ = annot_exp_effect e_aux l env typ no_effect
let annot_pat p_aux l env typ = P_aux (p_aux, (l, mk_tannot env typ no_effect))
let annot_letbind (p_aux, exp) l env typ =
LB_aux (LB_val (annot_pat p_aux l env typ, exp), (l, mk_tannot env typ (effect_of exp)))
let simple_num l n = E_aux (
E_lit (L_aux (L_num n, gen_loc l)),
simple_annot (gen_loc l)
(atom_typ (Nexp_aux (Nexp_constant n, gen_loc l))))
let effectful_effs = function
| Effect_aux (Effect_set effs, _) -> not (effs = [])
(*List.exists
(fun (BE_aux (be,_)) ->
match be with
| BE_nondet | BE_unspec | BE_undef | BE_lset -> false
| _ -> true
) effs*)
let effectful eaux = effectful_effs (effect_of eaux)
let effectful_pexp pexp = effectful_effs (effect_of_pexp pexp)
let rec small (E_aux (exp,_)) = match exp with
| E_id _
| E_lit _ -> true
| E_cast (_,e) -> small e
| E_list es -> List.for_all small es
| E_cons (e1,e2) -> small e1 && small e2
| E_sizeof _ -> true
| _ -> false
let id_is_local_var id env = match Env.lookup_id id env with
| Local _ -> true
| _ -> false
let id_is_unbound id env = match Env.lookup_id id env with
| Unbound -> true
| _ -> false
let rec lexp_is_local (LEXP_aux (lexp, _)) env = match lexp with
| LEXP_memory _ | LEXP_deref _ -> false
| LEXP_id id
| LEXP_cast (_, id) -> id_is_local_var id env
| LEXP_tup lexps | LEXP_vector_concat lexps -> List.for_all (fun lexp -> lexp_is_local lexp env) lexps
| LEXP_vector (lexp,_)
| LEXP_vector_range (lexp,_,_)
| LEXP_field (lexp,_) -> lexp_is_local lexp env
let rec lexp_is_local_intro (LEXP_aux (lexp, _)) env = match lexp with
| LEXP_memory _ | LEXP_deref _ -> false
| LEXP_id id
| LEXP_cast (_, id) -> id_is_unbound id env
| LEXP_tup lexps | LEXP_vector_concat lexps -> List.for_all (fun lexp -> lexp_is_local_intro lexp env) lexps
| LEXP_vector (lexp,_)
| LEXP_vector_range (lexp,_,_)
| LEXP_field (lexp,_) -> lexp_is_local_intro lexp env
let lexp_is_effectful (LEXP_aux (_, (_, annot))) = match destruct_tannot annot with
| Some (_, _, eff) -> effectful_effs eff
| _ -> false
let find_used_vars exp =
(* Overapproximates the set of used identifiers, but for the use cases below
this is acceptable. *)
let e_id id = IdSet.singleton id, E_id id in
fst (fold_exp
{ (compute_exp_alg IdSet.empty IdSet.union) with e_id = e_id } exp)
let find_introduced_vars exp =
let lEXP_aux ((ids, lexp), annot) =
let ids = match lexp with
| LEXP_id id | LEXP_cast (_, id)
when id_is_unbound id (env_of_annot annot) -> IdSet.add id ids
| _ -> ids in
(ids, LEXP_aux (lexp, annot)) in
fst (fold_exp
{ (compute_exp_alg IdSet.empty IdSet.union) with lEXP_aux = lEXP_aux } exp)
let find_updated_vars exp =
let intros = find_introduced_vars exp in
let lEXP_aux ((ids, lexp), annot) =
let ids = match lexp with
| LEXP_id id | LEXP_cast (_, id)
when id_is_local_var id (env_of_annot annot) && not (IdSet.mem id intros) ->
IdSet.add id ids
| _ -> ids in
(ids, LEXP_aux (lexp, annot)) in
fst (fold_exp
{ (compute_exp_alg IdSet.empty IdSet.union) with lEXP_aux = lEXP_aux } exp)
let lookup_equal_kids env =
let get_eq_kids kid eqs = try KBindings.find kid eqs with Not_found -> KidSet.singleton kid in
let add_eq_kids kid1 kid2 eqs =
let kids = KidSet.union (get_eq_kids kid2 eqs) (get_eq_kids kid1 eqs) in
eqs
|> KBindings.add kid1 kids
|> KBindings.add kid2 kids
in
let add_nc eqs = function
| NC_aux (NC_equal (Nexp_aux (Nexp_var kid1, _), Nexp_aux (Nexp_var kid2, _)), _) ->
add_eq_kids kid1 kid2 eqs
| _ -> eqs
in
List.fold_left add_nc KBindings.empty (Env.get_constraints env)
let lookup_constant_kid env kid =
let kids =
match KBindings.find kid (lookup_equal_kids env) with
| kids -> kids
| exception Not_found -> KidSet.singleton kid
in
let check_nc const nc = match const, nc with
| None, NC_aux (NC_equal (Nexp_aux (Nexp_var kid, _), Nexp_aux (Nexp_constant i, _)), _)
when KidSet.mem kid kids ->
Some i
| _, _ -> const
in
List.fold_left check_nc None (Env.get_constraints env)
let rec rewrite_nexp_ids env (Nexp_aux (nexp, l) as nexp_aux) = match nexp with
| Nexp_id id -> rewrite_nexp_ids env (Env.get_num_def id env)
| Nexp_var kid ->
begin
match lookup_constant_kid env kid with
| Some i -> nconstant i
| None -> nexp_aux
end
| Nexp_times (nexp1, nexp2) -> Nexp_aux (Nexp_times (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l)
| Nexp_sum (nexp1, nexp2) -> Nexp_aux (Nexp_sum (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l)
| Nexp_minus (nexp1, nexp2) -> Nexp_aux (Nexp_minus (rewrite_nexp_ids env nexp1, rewrite_nexp_ids env nexp2), l)
| Nexp_exp nexp -> Nexp_aux (Nexp_exp (rewrite_nexp_ids env nexp), l)
| Nexp_neg nexp -> Nexp_aux (Nexp_neg (rewrite_nexp_ids env nexp), l)
| _ -> nexp_aux
let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids =
let rec rewrite_typ env (Typ_aux (typ, l) as typ_aux) = match typ with
| Typ_fn (arg_t, ret_t, eff) ->
Typ_aux (Typ_fn (rewrite_typ env arg_t, rewrite_typ env ret_t, eff), l)
| Typ_tup ts ->
Typ_aux (Typ_tup (List.map (rewrite_typ env) ts), l)
| Typ_exist (kids, c, typ) ->
Typ_aux (Typ_exist (kids, c, rewrite_typ env typ), l)
| Typ_app (id, targs) ->
Typ_aux (Typ_app (id, List.map (rewrite_typ_arg env) targs), l)
| _ -> typ_aux
and rewrite_typ_arg env (Typ_arg_aux (targ, l) as targ_aux) = match targ with
| Typ_arg_nexp nexp ->
Typ_arg_aux (Typ_arg_nexp (rewrite_nexp_ids env nexp), l)
| Typ_arg_typ typ ->
Typ_arg_aux (Typ_arg_typ (rewrite_typ env typ), l)
| Typ_arg_order ord ->
Typ_arg_aux (Typ_arg_order ord, l)
in
let rewrite_annot (l, tannot) =
match destruct_tannot tannot with
| Some (env, typ, eff) -> l, replace_typ (rewrite_typ env typ) tannot
| None -> l, empty_tannot
in
let rewrite_def rewriters = function
| DEF_spec (VS_aux (VS_val_spec (typschm, id, exts, b), (l, tannot))) when not (is_empty_tannot tannot) ->
let env = env_of_annot (l, tannot) in
let typ = typ_of_annot (l, tannot) in
let eff = effect_of_annot tannot in
let typschm = match typschm with
| TypSchm_aux (TypSchm_ts (tq, typ), l) ->
TypSchm_aux (TypSchm_ts (tq, rewrite_typ env typ), l)
in
let a = rewrite_annot (l, mk_tannot env typ eff) in
DEF_spec (VS_aux (VS_val_spec (typschm, id, exts, b), a))
| d -> Rewriter.rewrite_def rewriters d
in
rewrite_defs_base { rewriters_base with
rewrite_exp = (fun _ -> map_exp_annot rewrite_annot); rewrite_def = rewrite_def
},
rewrite_typ
let rewrite_bitvector_exps defs =
let e_aux = function
| (E_vector es, ((l, tannot) as a)) when not (is_empty_tannot tannot) ->
let env = env_of_annot (l, tannot) in
let typ = typ_of_annot (l, tannot) in
let eff = effect_of_annot tannot in
if is_bitvector_typ typ then
try
let len = mk_lit_exp (L_num (Big_int.of_int (List.length es))) in
let es = mk_exp (E_list (List.map strip_exp es)) in
let exp = mk_exp (E_app (mk_id "bitvector_of_bitlist", [len; es])) in
check_exp env exp typ
with
| _ -> E_aux (E_vector es, a)
else
E_aux (E_vector es, a)
| (e_aux, a) -> E_aux (e_aux, a)
in
let rewrite_exp _ = fold_exp { id_exp_alg with e_aux = e_aux } in
if IdSet.mem (mk_id "bitvector_of_bitlist") (Initial_check.val_spec_ids defs) then
rewrite_defs_base { rewriters_base with rewrite_exp = rewrite_exp } defs
else defs
(* Re-write trivial sizeof expressions - trivial meaning that the
value of the sizeof can be directly inferred from the type
variables in scope. *)
let rewrite_trivial_sizeof, rewrite_trivial_sizeof_exp =
let extract_typ_var l env nexp (id, (_, typ)) =
let var = E_aux (E_id id, (l, mk_tannot env typ no_effect)) in
match destruct_atom_nexp env typ with
| Some size when prove env (nc_eq size nexp) -> Some var
(* AA: This next case is a bit of a hack... is there a more
general way to deal with trivial nexps that are offset by
constants? This will resolve a 'n - 1 sizeof when 'n is in
scope. *)
| Some size when prove env (nc_eq (nsum size (nint 1)) nexp) ->
let one_exp = infer_exp env (mk_lit_exp (L_num (Big_int.of_int 1))) in
Some (E_aux (E_app (mk_id "add_atom", [var; one_exp]), (gen_loc l, mk_tannot env (atom_typ (nsum size (nint 1))) no_effect)))
| _ ->
begin
match destruct_vector env typ with
| Some (len, _, _) when prove env (nc_eq len nexp) ->
Some (E_aux (E_app (mk_id "length", [var]), (l, mk_tannot env (atom_typ len) no_effect)))
| _ -> None
end
in
let rec split_nexp (Nexp_aux (nexp_aux, l) as nexp) =
match nexp_aux with
| Nexp_sum (n1, n2) ->
mk_exp (E_app (mk_id "add_atom", [split_nexp n1; split_nexp n2]))
| Nexp_minus (n1, n2) ->
mk_exp (E_app (mk_id "sub_atom", [split_nexp n1; split_nexp n2]))
| Nexp_times (n1, n2) ->
mk_exp (E_app (mk_id "mult_atom", [split_nexp n1; split_nexp n2]))
| Nexp_neg nexp -> mk_exp (E_app (mk_id "negate_atom", [split_nexp nexp]))
| _ -> mk_exp (E_sizeof nexp)
in
let rec rewrite_e_aux split_sizeof (E_aux (e_aux, (l, _)) as orig_exp) =
let env = env_of orig_exp in
match e_aux with
| E_sizeof (Nexp_aux (Nexp_constant c, _) as nexp) ->
E_aux (E_lit (L_aux (L_num c, l)), (l, mk_tannot env (atom_typ nexp) no_effect))
| E_sizeof nexp ->
begin
match nexp_simp (rewrite_nexp_ids (env_of orig_exp) nexp) with
| Nexp_aux (Nexp_constant c, _) ->
E_aux (E_lit (L_aux (L_num c, l)), (l, mk_tannot env (atom_typ nexp) no_effect))
| _ ->
let locals = Env.get_locals env in
let exps = Bindings.bindings locals
|> List.map (extract_typ_var l env nexp)
|> List.map (fun opt -> match opt with Some x -> [x] | None -> [])
|> List.concat
in
match exps with
| (exp :: _) -> check_exp env (strip_exp exp) (typ_of exp)
| [] when split_sizeof ->
fold_exp (rewrite_e_sizeof false) (check_exp env (split_nexp nexp) (typ_of orig_exp))
| [] -> orig_exp
end
| _ -> orig_exp
and rewrite_e_sizeof split_sizeof =
{ id_exp_alg with e_aux = (fun (exp, annot) -> rewrite_e_aux split_sizeof (E_aux (exp, annot))) }
in
rewrite_defs_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp (rewrite_e_sizeof true)) }, rewrite_e_aux true
(* Rewrite sizeof expressions with type-level variables to
term-level expressions
For each type-level variable used in a sizeof expressions whose value cannot
be directly extracted from existing parameters of the surrounding function,
a further parameter is added; calls to the function are rewritten
accordingly (possibly causing further rewriting in the calling function) *)
let rewrite_sizeof (Defs defs) =
let sizeof_frees exp =
fst (fold_exp
{ (compute_exp_alg KidSet.empty KidSet.union) with
e_sizeof = (fun nexp -> (nexp_frees nexp, E_sizeof nexp)) }
exp) in
(* Collect nexps whose values can be obtained directly from a pattern bind *)
let nexps_from_params pat =
fst (fold_pat
{ (compute_pat_alg [] (@)) with
p_aux = (fun ((v,pat),((l,_) as annot)) ->
let v' = match pat with
| P_id id | P_as (_, id) ->
let (Typ_aux (typ,_) as typ_aux) = typ_of_annot annot in
(match typ with
| Typ_app (atom, [Typ_arg_aux (Typ_arg_nexp nexp, _)])
when string_of_id atom = "atom" ->
[nexp, E_id id]
| Typ_app (vector, _) when string_of_id vector = "vector" ->
let id_length = Id_aux (Id "length", gen_loc l) in
(try
(match Env.get_val_spec id_length (env_of_annot annot) with
| _ ->
let (len,_,_) = vector_typ_args_of typ_aux in
let exp = E_app (id_length, [E_aux (E_id id, annot)]) in
[len, exp])
with
| _ -> [])
| _ -> [])
| _ -> [] in
(v @ v', P_aux (pat,annot)))} pat) in
(* Substitute collected values in sizeof expressions *)
let rec e_sizeof nmap (Nexp_aux (nexp, l) as nexp_aux) =
try snd (List.find (fun (nexp,_) -> nexp_identical nexp nexp_aux) nmap)
with
| Not_found ->
let binop nexp1 op nexp2 = E_app_infix (
E_aux (e_sizeof nmap nexp1, simple_annot l (atom_typ nexp1)),
Id_aux (Id op, Parse_ast.Unknown),
E_aux (e_sizeof nmap nexp2, simple_annot l (atom_typ nexp2))
) in
let (Nexp_aux (nexp, l) as nexp_aux) = nexp_simp nexp_aux in
(match nexp with
| Nexp_constant i -> E_lit (L_aux (L_num i, l))
| Nexp_times (nexp1, nexp2) -> binop nexp1 "*" nexp2
| Nexp_sum (nexp1, nexp2) -> binop nexp1 "+" nexp2
| Nexp_minus (nexp1, nexp2) -> binop nexp1 "-" nexp2
| _ -> E_sizeof nexp_aux) in
let ex_regex = Str.regexp "'ex[0-9]+" in
(* Rewrite calls to functions which have had parameters added to pass values
of type-level variables; these are added as sizeof expressions first, and
then further rewritten as above. *)
let e_app_aux param_map ((exp, exp_orig), ((l, _) as annot)) =
let env = env_of_annot annot in
let full_exp = E_aux (exp, annot) in
let orig_exp = E_aux (exp_orig, annot) in
match exp with
| E_app (f, args) ->
if Bindings.mem f param_map then
(* Retrieve instantiation of the type variables of the called function
for the given parameters in the original environment *)
let inst =
try instantiation_of orig_exp with
| Type_error (l, err) ->
raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err)) in
(* Rewrite the inst using orig_kid so that each type variable has it's
original name rather than a mangled typechecker name *)
let inst = KBindings.fold (fun kid uvar b -> KBindings.add (orig_kid kid) uvar b) inst KBindings.empty in
let kid_exp kid = begin
(* We really don't want to see an existential here! *)
assert (not (Str.string_match ex_regex (string_of_kid kid) 0));
let uvar = try Some (KBindings.find (orig_kid kid) inst) with Not_found -> None in
match uvar with
| Some (U_nexp nexp) ->
let sizeof = E_aux (E_sizeof nexp, (l, mk_tannot env (atom_typ nexp) no_effect)) in
(try rewrite_trivial_sizeof_exp sizeof with
| Type_error (l, err) ->
raise (Reporting_basic.err_typ l (Type_error.string_of_type_error err)))
(* If the type variable is Not_found then it was probably
introduced by a P_var pattern, so it likely exists as
a variable in scope. It can't be an existential because the assert rules that out. *)
| None -> annot_exp (E_id (id_of_kid (orig_kid kid))) l env (atom_typ (nvar (orig_kid kid)))
| _ ->
raise (Reporting_basic.err_unreachable l
("failed to infer nexp for type variable " ^ string_of_kid kid ^
" of function " ^ string_of_id f))
end in
let kid_exps = List.map kid_exp (KidSet.elements (Bindings.find f param_map)) in
(E_aux (E_app (f, kid_exps @ args), annot), orig_exp)
else (full_exp, orig_exp)
| _ -> (full_exp, orig_exp) in
(* Plug this into a folding algorithm that also keeps around a copy of the
original expressions, which we use to infer instantiations of type variables
in the original environments *)
let copy_exp_alg =
{ e_block = (fun es -> let (es, es') = List.split es in (E_block es, E_block es'))
; e_nondet = (fun es -> let (es, es') = List.split es in (E_nondet es, E_nondet es'))
; e_id = (fun id -> (E_id id, E_id id))
; e_ref = (fun id -> (E_ref id, E_ref id))
; e_lit = (fun lit -> (E_lit lit, E_lit lit))
; e_cast = (fun (typ,(e,e')) -> (E_cast (typ,e), E_cast (typ,e')))
; e_app = (fun (id,es) -> let (es, es') = List.split es in (E_app (id,es), E_app (id,es')))
; e_app_infix = (fun ((e1,e1'),id,(e2,e2')) -> (E_app_infix (e1,id,e2), E_app_infix (e1',id,e2')))
; e_tuple = (fun es -> let (es, es') = List.split es in (E_tuple es, E_tuple es'))
; e_if = (fun ((e1,e1'),(e2,e2'),(e3,e3')) -> (E_if (e1,e2,e3), E_if (e1',e2',e3')))
; e_for = (fun (id,(e1,e1'),(e2,e2'),(e3,e3'),order,(e4,e4')) -> (E_for (id,e1,e2,e3,order,e4), E_for (id,e1',e2',e3',order,e4')))
; e_loop = (fun (lt, (e1, e1'), (e2, e2')) -> (E_loop (lt, e1, e2), E_loop (lt, e1', e2')))
; e_vector = (fun es -> let (es, es') = List.split es in (E_vector es, E_vector es'))
; e_vector_access = (fun ((e1,e1'),(e2,e2')) -> (E_vector_access (e1,e2), E_vector_access (e1',e2')))
; e_vector_subrange = (fun ((e1,e1'),(e2,e2'),(e3,e3')) -> (E_vector_subrange (e1,e2,e3), E_vector_subrange (e1',e2',e3')))
; e_vector_update = (fun ((e1,e1'),(e2,e2'),(e3,e3')) -> (E_vector_update (e1,e2,e3), E_vector_update (e1',e2',e3')))
; e_vector_update_subrange = (fun ((e1,e1'),(e2,e2'),(e3,e3'),(e4,e4')) -> (E_vector_update_subrange (e1,e2,e3,e4), E_vector_update_subrange (e1',e2',e3',e4')))
; e_vector_append = (fun ((e1,e1'),(e2,e2')) -> (E_vector_append (e1,e2), E_vector_append (e1',e2')))
; e_list = (fun es -> let (es, es') = List.split es in (E_list es, E_list es'))
; e_cons = (fun ((e1,e1'),(e2,e2')) -> (E_cons (e1,e2), E_cons (e1',e2')))
; e_record = (fun (fexps, fexps') -> (E_record fexps, E_record fexps'))
; e_record_update = (fun ((e1,e1'),(fexp,fexp')) -> (E_record_update (e1,fexp), E_record_update (e1',fexp')))
; e_field = (fun ((e1,e1'),id) -> (E_field (e1,id), E_field (e1',id)))
; e_case = (fun ((e1,e1'),pexps) -> let (pexps, pexps') = List.split pexps in (E_case (e1,pexps), E_case (e1',pexps')))
; e_try = (fun ((e1,e1'),pexps) -> let (pexps, pexps') = List.split pexps in (E_try (e1,pexps), E_try (e1',pexps')))
; e_let = (fun ((lb,lb'),(e2,e2')) -> (E_let (lb,e2), E_let (lb',e2')))
; e_assign = (fun ((lexp,lexp'),(e2,e2')) -> (E_assign (lexp,e2), E_assign (lexp',e2')))
; e_sizeof = (fun nexp -> (E_sizeof nexp, E_sizeof nexp))
; e_constraint = (fun nc -> (E_constraint nc, E_constraint nc))
; e_exit = (fun (e1,e1') -> (E_exit (e1), E_exit (e1')))
; e_throw = (fun (e1,e1') -> (E_throw (e1), E_throw (e1')))
; e_return = (fun (e1,e1') -> (E_return e1, E_return e1'))
; e_assert = (fun ((e1,e1'),(e2,e2')) -> (E_assert(e1,e2), E_assert(e1',e2')) )
; e_var = (fun ((lexp,lexp'), (e2,e2'), (e3,e3')) -> (E_var (lexp,e2,e3), E_var (lexp',e2',e3')))
; e_internal_plet = (fun (pat, (e1,e1'), (e2,e2')) -> (E_internal_plet (pat,e1,e2), E_internal_plet (pat,e1',e2')))
; e_internal_return = (fun (e,e') -> (E_internal_return e, E_internal_return e'))
; e_internal_value = (fun v -> (E_internal_value v, E_internal_value v))
; e_aux = (fun ((e,e'),annot) -> (E_aux (e,annot), E_aux (e',annot)))
; lEXP_id = (fun id -> (LEXP_id id, LEXP_id id))
; lEXP_deref = (fun (e, e') -> (LEXP_deref e, LEXP_deref e'))
; lEXP_memory = (fun (id,es) -> let (es, es') = List.split es in (LEXP_memory (id,es), LEXP_memory (id,es')))
; lEXP_cast = (fun (typ,id) -> (LEXP_cast (typ,id), LEXP_cast (typ,id)))
; lEXP_tup = (fun tups -> let (tups,tups') = List.split tups in (LEXP_tup tups, LEXP_tup tups'))
; lEXP_vector = (fun ((lexp,lexp'),(e2,e2')) -> (LEXP_vector (lexp,e2), LEXP_vector (lexp',e2')))
; lEXP_vector_range = (fun ((lexp,lexp'),(e2,e2'),(e3,e3')) -> (LEXP_vector_range (lexp,e2,e3), LEXP_vector_range (lexp',e2',e3')))
; lEXP_vector_concat = (fun lexps -> let (lexps,lexps') = List.split lexps in (LEXP_vector_concat lexps, LEXP_vector_concat lexps'))
; lEXP_field = (fun ((lexp,lexp'),id) -> (LEXP_field (lexp,id), LEXP_field (lexp',id)))
; lEXP_aux = (fun ((lexp,lexp'),annot) -> (LEXP_aux (lexp,annot), LEXP_aux (lexp',annot)))
; fE_Fexp = (fun (id,(e,e')) -> (FE_Fexp (id,e), FE_Fexp (id,e')))
; fE_aux = (fun ((fexp,fexp'),annot) -> (FE_aux (fexp,annot), FE_aux (fexp',annot)))
; fES_Fexps = (fun (fexps,b) -> let (fexps, fexps') = List.split fexps in (FES_Fexps (fexps,b), FES_Fexps (fexps',b)))
; fES_aux = (fun ((fexp,fexp'),annot) -> (FES_aux (fexp,annot), FES_aux (fexp',annot)))
; def_val_empty = (Def_val_empty, Def_val_empty)
; def_val_dec = (fun (e,e') -> (Def_val_dec e, Def_val_dec e'))
; def_val_aux = (fun ((defval,defval'),aux) -> (Def_val_aux (defval,aux), Def_val_aux (defval',aux)))
; pat_exp = (fun (pat,(e,e')) -> (Pat_exp (pat,e), Pat_exp (pat,e')))
; pat_when = (fun (pat,(e1,e1'),(e2,e2')) -> (Pat_when (pat,e1,e2), Pat_when (pat,e1',e2')))
; pat_aux = (fun ((pexp,pexp'),a) -> (Pat_aux (pexp,a), Pat_aux (pexp',a)))
; lB_val = (fun (pat,(e,e')) -> (LB_val (pat,e), LB_val (pat,e')))
; lB_aux = (fun ((lb,lb'),annot) -> (LB_aux (lb,annot), LB_aux (lb',annot)))
; pat_alg = id_pat_alg
} in
let rewrite_sizeof_fun params_map
(FD_aux (FD_function (rec_opt,tannot,eff,funcls),((l,_) as annot))) =
let rewrite_funcl_body (FCL_aux (FCL_Funcl (id,pexp), annot)) (funcls,nvars) =
let pat,guard,exp,pannot = destruct_pexp pexp in
let nmap = nexps_from_params pat in
(* first rewrite calls to other functions... *)
let exp' = fst (fold_exp { copy_exp_alg with e_aux = e_app_aux params_map } exp) in
(* ... then rewrite sizeof expressions in current function body *)
let exp'' = fold_exp { id_exp_alg with e_sizeof = e_sizeof nmap } exp' in
let guard' = match guard with
| Some guard ->
(* As above *)
let guard' = fst (fold_exp { copy_exp_alg with e_aux = e_app_aux params_map } guard) in
Some (fold_exp { id_exp_alg with e_sizeof = e_sizeof nmap } guard')
| None -> None in
let pexp' = construct_pexp (pat,guard',exp'',pannot) in
(FCL_aux (FCL_Funcl (id,pexp'), annot) :: funcls,
KidSet.union nvars (sizeof_frees exp'')) in
let (funcls, nvars) = List.fold_right rewrite_funcl_body funcls ([], KidSet.empty) in
(* Add a parameter for each remaining free type-level variable in a
sizeof expression *)
let kid_typ kid = atom_typ (nvar kid) in
let kid_annot kid = simple_annot l (kid_typ kid) in
let kid_pat kid =
P_aux (P_typ (kid_typ kid,
P_aux (P_id (Id_aux (Id (string_of_id (id_of_kid kid) ^ "__tv"), l)),
kid_annot kid)), kid_annot kid) in
let kid_eaux kid = E_id (Id_aux (Id (string_of_id (id_of_kid kid) ^ "__tv"), l)) in
let kid_typs = List.map kid_typ (KidSet.elements nvars) in
let kid_pats = List.map kid_pat (KidSet.elements nvars) in
let kid_nmap = List.map (fun kid -> (nvar kid, kid_eaux kid)) (KidSet.elements nvars) in
let rewrite_funcl_params (FCL_aux (FCL_Funcl (id, pexp), annot) as funcl) =
let rec rewrite_pat (P_aux (pat, ((l, _) as pannot)) as paux) =
let penv = env_of_annot pannot in
let peff = effect_of_annot (snd pannot) in
if KidSet.is_empty nvars then paux else
match pat_typ_of paux with
| Typ_aux (Typ_tup typs, _) ->
let ptyp' = Typ_aux (Typ_tup (kid_typs @ typs), l) in
(match pat with
| P_tup pats ->
P_aux (P_tup (kid_pats @ pats), (l, mk_tannot penv ptyp' peff))
| P_wild -> P_aux (pat, (l, mk_tannot penv ptyp' peff))
| P_typ (Typ_aux (Typ_tup typs, l), pat) ->
P_aux (P_typ (Typ_aux (Typ_tup (kid_typs @ typs), l),
rewrite_pat pat), (l, mk_tannot penv ptyp' peff))
| P_as (_, id) | P_id id ->
(* adding parameters here would change the type of id;
we should remove the P_as/P_id here and add a let-binding to the body *)
raise (Reporting_basic.err_todo l
"rewriting as- or id-patterns for sizeof expressions not yet implemented")
| _ ->
raise (Reporting_basic.err_unreachable l
"unexpected pattern while rewriting function parameters for sizeof expressions"))
| ptyp ->
let ptyp' = Typ_aux (Typ_tup (kid_typs @ [ptyp]), l) in
P_aux (P_tup (kid_pats @ [paux]), (l, mk_tannot penv ptyp' peff)) in
let pat,guard,exp,pannot = destruct_pexp pexp in
let pat' = rewrite_pat pat in
let guard' = match guard with
| Some guard -> Some (fold_exp { id_exp_alg with e_sizeof = e_sizeof kid_nmap } guard)
| None -> None in
let exp' = fold_exp { id_exp_alg with e_sizeof = e_sizeof kid_nmap } exp in
let pexp' = construct_pexp (pat',guard',exp',pannot) in
FCL_aux (FCL_Funcl (id, pexp'), annot) in
let funcls = List.map rewrite_funcl_params funcls in
let fd = FD_aux (FD_function (rec_opt,tannot,eff,funcls),annot) in
let params_map =
if KidSet.is_empty nvars then params_map else
Bindings.add (id_of_fundef fd) nvars params_map in
(params_map, FD_aux (FD_function (rec_opt,tannot,eff,funcls),annot)) in
let rewrite_sizeof_def (params_map, defs) = function
| DEF_fundef fd ->
let (params_map', fd') = rewrite_sizeof_fun params_map fd in
(params_map', defs @ [DEF_fundef fd'])
| DEF_internal_mutrec fds ->
let rewrite_fd (params_map, fds) fd =
let (params_map', fd') = rewrite_sizeof_fun params_map fd in
(params_map', fds @ [fd']) in
(* TODO Split rewrite_sizeof_fun into an analysis and a rewrite pass,
so that we can call the analysis until a fixpoint is reached and then
rewrite the mutually recursive functions *)
let (params_map', fds') = List.fold_left rewrite_fd (params_map, []) fds in
(params_map', defs @ [DEF_internal_mutrec fds'])
| DEF_val (LB_aux (lb, annot)) ->
begin
let lb' = match lb with
| LB_val (pat, exp) ->
let exp' = fst (fold_exp { copy_exp_alg with e_aux = e_app_aux params_map } exp) in
LB_val (pat, exp') in
(params_map, defs @ [DEF_val (LB_aux (lb', annot))])
end
| def ->
(params_map, defs @ [def]) in
let rewrite_sizeof_valspec params_map def =
let rewrite_typschm (TypSchm_aux (TypSchm_ts (tq, typ), l) as ts) id =
if Bindings.mem id params_map then
let kid_typs = List.map (fun kid -> atom_typ (nvar kid))
(KidSet.elements (Bindings.find id params_map)) in
let typ' = match typ with
| Typ_aux (Typ_fn (vtyp_arg, vtyp_ret, declared_eff), vl) ->
let vtyp_arg' = begin
match vtyp_arg with
| Typ_aux (Typ_tup typs, vl) ->
Typ_aux (Typ_tup (kid_typs @ typs), vl)
| _ -> Typ_aux (Typ_tup (kid_typs @ [vtyp_arg]), vl)
end in
Typ_aux (Typ_fn (vtyp_arg', vtyp_ret, declared_eff), vl)
| _ ->
raise (Reporting_basic.err_typ l "val spec with non-function type") in
TypSchm_aux (TypSchm_ts (tq, typ'), l)
else ts in
match def with
| DEF_spec (VS_aux (VS_val_spec (typschm, id, ext, is_cast), a)) ->
DEF_spec (VS_aux (VS_val_spec (rewrite_typschm typschm id, id, ext, is_cast), a))
| def -> def
in
let (params_map, defs) = List.fold_left rewrite_sizeof_def
(Bindings.empty, []) defs in
let defs = List.map (rewrite_sizeof_valspec params_map) defs in
(* Defs defs *)
fst (Type_error.check initial_env (Defs defs))
let rewrite_defs_remove_assert defs =
let e_assert ((E_aux (eaux, (l, _)) as exp), str) = match eaux with
| E_constraint _ ->
E_assert (exp, str)
| _ ->
E_assert (E_aux (E_lit (mk_lit L_true), simple_annot l bool_typ), str) in
rewrite_defs_base
{ rewriters_base with
rewrite_exp = (fun _ -> fold_exp { id_exp_alg with e_assert = e_assert}) }
defs
let remove_vector_concat_pat pat =
(* ivc: bool that indicates whether the exp is in a vector_concat pattern *)
let remove_typed_patterns =
fold_pat { id_pat_alg with
p_aux = (function
| (P_typ (_,P_aux (p,_)),annot)
| (p,annot) ->
P_aux (p,annot)
)
} in
(* let pat = remove_typed_patterns pat in *)
let fresh_id_v = fresh_id "v__" in
(* expects that P_typ elements have been removed from AST,
that the length of all vectors involved is known,
that we don't have indexed vectors *)
(* introduce names for all patterns of form P_vector_concat *)
let name_vector_concat_roots =
{ p_lit = (fun lit -> P_lit lit)
; p_typ = (fun (typ,p) -> P_typ (typ,p false)) (* cannot happen *)
; p_wild = P_wild
(* ToDo: I have no idea what the boolean parameter means so guessed that
* "true" was a good value to use.
* (Adding a comment explaining the boolean might be useful?)
*)
; p_or = (fun (pat1, pat2) -> P_or (pat1 true, pat2 true))
; p_not = (fun pat -> P_not (pat true))
; p_as = (fun (pat,id) -> P_as (pat true,id))
; p_id = (fun id -> P_id id)
; p_var = (fun (pat,kid) -> P_var (pat true,kid))
; p_app = (fun (id,ps) -> P_app (id, List.map (fun p -> p false) ps))
; p_record = (fun (fpats,b) -> P_record (fpats, b))
; p_vector = (fun ps -> P_vector (List.map (fun p -> p false) ps))
; p_vector_concat = (fun ps -> P_vector_concat (List.map (fun p -> p false) ps))
; p_tup = (fun ps -> P_tup (List.map (fun p -> p false) ps))
; p_list = (fun ps -> P_list (List.map (fun p -> p false) ps))
; p_cons = (fun (p,ps) -> P_cons (p false, ps false))
; p_string_append = (fun (ps) -> P_string_append (List.map (fun p -> p false) ps))
; p_aux =
(fun (pat,((l,_) as annot)) contained_in_p_as ->
match pat with
| P_vector_concat pats ->
(if contained_in_p_as
then P_aux (pat,annot)
else P_aux (P_as (P_aux (pat,annot),fresh_id_v l),annot))
| _ -> P_aux (pat,annot)
)
; fP_aux = (fun (fpat,annot) -> FP_aux (fpat,annot))
; fP_Fpat = (fun (id,p) -> FP_Fpat (id,p false))
} in
let pat = (fold_pat name_vector_concat_roots pat) false in
(* introduce names for all unnamed child nodes of P_vector_concat *)
let name_vector_concat_elements =
let p_vector_concat pats =
let rec aux ((P_aux (p,((l,_) as a))) as pat) = match p with
| P_vector _ -> P_aux (P_as (pat,fresh_id_v l),a)
| P_lit _ -> P_aux (P_as (pat, fresh_id_v l), a)
| P_id id -> P_aux (P_id id,a)
| P_as (p,id) -> P_aux (P_as (p,id),a)
| P_typ (typ, pat) -> P_aux (P_typ (typ, aux pat),a)
| P_wild -> P_aux (P_wild,a)
| P_app (id, pats) when Env.is_mapping id (env_of_annot a) -> P_aux (P_app (id, List.map aux pats), a)
| _ ->
raise
(Reporting_basic.err_unreachable
l "name_vector_concat_elements: Non-vector in vector-concat pattern") in
P_vector_concat (List.map aux pats) in
{id_pat_alg with p_vector_concat = p_vector_concat} in
let pat = fold_pat name_vector_concat_elements pat in
let rec tag_last = function
| x :: xs -> let is_last = xs = [] in (x,is_last) :: tag_last xs
| _ -> [] in
(* remove names from vectors in vector_concat patterns and collect them as declarations for the
function body or expression *)
let unname_vector_concat_elements = (* :
('a,
'a pat * ((tannot exp -> tannot exp) list),
'a pat_aux * ((tannot exp -> tannot exp) list),
'a fpat * ((tannot exp -> tannot exp) list),
'a fpat_aux * ((tannot exp -> tannot exp) list))
pat_alg = *)
(* build a let-expression of the form "let child = root[i..j] in body" *)
let letbind_vec typ_opt (rootid,rannot) (child,cannot) (i,j) =
let (l,_) = cannot in
let env = env_of_annot rannot in
let rootname = string_of_id rootid in
let childname = string_of_id child in
let root = E_aux (E_id rootid, rannot) in
let index_i = simple_num l i in
let index_j = simple_num l j in
(* FIXME *)
let subv = fix_eff_exp (E_aux (E_vector_subrange (root, index_i, index_j), cannot)) in
(* let (_, ord, _) = vector_typ_args_of (Env.base_typ_of (env_of root) (typ_of root)) in
let subrange_id = if is_order_inc ord then "bitvector_subrange_inc" else "bitvector_subrange_dec" in
let subv = fix_eff_exp (E_aux (E_app (mk_id subrange_id, [root; index_i; index_j]), cannot)) in *)
let id_pat =
match typ_opt with
| Some typ -> add_p_typ typ (P_aux (P_id child,cannot))
| None -> P_aux (P_id child,cannot) in
let letbind = fix_eff_lb (LB_aux (LB_val (id_pat,subv),cannot)) in
(letbind,
(fun body ->
if IdSet.mem child (find_used_vars body)
then fix_eff_exp (annot_exp (E_let (letbind,body)) l env (typ_of body))
else body),
(rootname,childname)) in
let p_aux = function
| ((P_as (P_aux (P_vector_concat pats,rannot'),rootid),decls),rannot) ->
let rtyp = Env.base_typ_of (env_of_annot rannot') (typ_of_annot rannot') in
let (start,last_idx) = (match vector_start_index rtyp, vector_typ_args_of rtyp with
| Nexp_aux (Nexp_constant start,_), (Nexp_aux (Nexp_constant length,_), ord, _) ->
(start, if is_order_inc ord
then Big_int.sub (Big_int.add start length) (Big_int.of_int 1)
else Big_int.add (Big_int.sub start length) (Big_int.of_int 1))
| _ ->
raise (Reporting_basic.err_unreachable (fst rannot')
("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern"))) in
let rec aux typ_opt (pos,pat_acc,decl_acc) (P_aux (p,cannot),is_last) =
let ctyp = Env.base_typ_of (env_of_annot cannot) (typ_of_annot cannot) in
let (length,ord,_) = vector_typ_args_of ctyp in
let (pos',index_j) = match length with
| Nexp_aux (Nexp_constant i,_) ->
if is_order_inc ord
then (Big_int.add pos i, Big_int.sub (Big_int.add pos i) (Big_int.of_int 1))
else (Big_int.sub pos i, Big_int.add (Big_int.sub pos i) (Big_int.of_int 1))
| Nexp_aux (_,l) ->
if is_last then (pos,last_idx)
else
raise
(Reporting_basic.err_unreachable
l ("unname_vector_concat_elements: vector of unspecified length in vector-concat pattern")) in
(match p with
(* if we see a named vector pattern, remove the name and remember to
declare it later *)
| P_as (P_aux (p,cannot),cname) ->
let (lb,decl,info) = letbind_vec typ_opt (rootid,rannot) (cname,cannot) (pos,index_j) in
(pos', pat_acc @ [P_aux (p,cannot)], decl_acc @ [((lb,decl),info)])
(* if we see a P_id variable, remember to declare it later *)
| P_id cname ->
let (lb,decl,info) = letbind_vec typ_opt (rootid,rannot) (cname,cannot) (pos,index_j) in
(pos', pat_acc @ [P_aux (P_id cname,cannot)], decl_acc @ [((lb,decl),info)])
| P_typ (typ, pat) -> aux (Some typ) (pos,pat_acc,decl_acc) (pat, is_last)
(* | P_app (cname, pats) if Env.is_mapping cname (en) ->
* let (lb,decl,info) = letbind_vec typ_opt (rootid,rannot) (cname,cannot) (pos,index_j) in
* (pos', pat_acc @ [P_aux (P_app (cname,pats),cannot)], decl_acc @ [((lb,decl),info)]) *)
(* normal vector patterns are fine *)
| _ -> (pos', pat_acc @ [P_aux (p,cannot)],decl_acc)) in
let pats_tagged = tag_last pats in
let (_,pats',decls') = List.fold_left (aux None) (start,[],[]) pats_tagged in
(* abuse P_vector_concat as a P_vector_const pattern: it has the of
patterns as an argument but they're meant to be consed together *)
(P_aux (P_as (P_aux (P_vector_concat pats',rannot'),rootid),rannot), decls @ decls')
| ((p,decls),annot) -> (P_aux (p,annot),decls) in
{ p_lit = (fun lit -> (P_lit lit,[]))
; p_wild = (P_wild,[])
; p_or = (fun ((pat1, ds1), (pat2, ds2)) -> (P_or(pat1, pat2), ds1 @ ds2))
; p_not = (fun (pat, ds) -> (P_not(pat), ds))
; p_as = (fun ((pat,decls),id) -> (P_as (pat,id),decls))
; p_typ = (fun (typ,(pat,decls)) -> (P_typ (typ,pat),decls))
; p_id = (fun id -> (P_id id,[]))
; p_var = (fun ((pat,decls),kid) -> (P_var (pat,kid),decls))
; p_app = (fun (id,ps) -> let (ps,decls) = List.split ps in
(P_app (id,ps),List.flatten decls))
; p_record = (fun (ps,b) -> let (ps,decls) = List.split ps in
(P_record (ps,b),List.flatten decls))
; p_vector = (fun ps -> let (ps,decls) = List.split ps in
(P_vector ps,List.flatten decls))
; p_vector_concat = (fun ps -> let (ps,decls) = List.split ps in
(P_vector_concat ps,List.flatten decls))
; p_tup = (fun ps -> let (ps,decls) = List.split ps in
(P_tup ps,List.flatten decls))
; p_list = (fun ps -> let (ps,decls) = List.split ps in
(P_list ps,List.flatten decls))
; p_string_append = (fun ps -> let (ps,decls) = List.split ps in
(P_string_append ps,List.flatten decls))
; p_cons = (fun ((p,decls),(p',decls')) -> (P_cons (p,p'), decls @ decls'))
; p_aux = (fun ((pat,decls),annot) -> p_aux ((pat,decls),annot))
; fP_aux = (fun ((fpat,decls),annot) -> (FP_aux (fpat,annot),decls))
; fP_Fpat = (fun (id,(pat,decls)) -> (FP_Fpat (id,pat),decls))
} in
let (pat,decls) = fold_pat unname_vector_concat_elements pat in
let decls =
let module S = Set.Make(String) in
let roots_needed =
List.fold_right
(fun (_,(rootid,childid)) roots_needed ->
if S.mem childid roots_needed then
(* let _ = print_endline rootid in *)
S.add rootid roots_needed
else if String.length childid >= 3 && String.sub childid 0 2 = String.sub "v__" 0 2 then
roots_needed
else
S.add rootid roots_needed
) decls S.empty in
List.filter
(fun (_,(_,childid)) ->
S.mem childid roots_needed ||
String.length childid < 3 ||
not (String.sub childid 0 2 = String.sub "v__" 0 2))
decls in
let (letbinds,decls) =
let (decls,_) = List.split decls in
List.split decls in
let decls = List.fold_left (fun f g x -> f (g x)) (fun b -> b) decls in
(* at this point shouldn't have P_as patterns in P_vector_concat patterns any more,
all P_as and P_id vectors should have their declarations in decls.
Now flatten all vector_concat patterns *)
let flatten =
let p_vector_concat ps =
let aux p acc = match p with
| (P_aux (P_vector_concat pats,_)) -> pats @ acc
| pat -> pat :: acc in
P_vector_concat (List.fold_right aux ps []) in
{id_pat_alg with p_vector_concat = p_vector_concat} in
let pat = fold_pat flatten pat in
(* at this point pat should be a flat pattern: no vector_concat patterns
with vector_concats patterns as direct child-nodes anymore *)
let range a b =
let rec aux a b = if Big_int.greater a b then [] else a :: aux (Big_int.add a (Big_int.of_int 1)) b in
if Big_int.greater a b then List.rev (aux b a) else aux a b in
let remove_vector_concats =
let p_vector_concat ps =
let aux acc (P_aux (p,annot),is_last) =
let env = env_of_annot annot in
let typ = Env.base_typ_of env (typ_of_annot annot) in
let eff = effect_of_annot (snd annot) in
let (l,_) = annot in
let wild _ = P_aux (P_wild,(gen_loc l, mk_tannot env bit_typ eff)) in
if is_vector_typ typ then
match p, vector_typ_args_of typ with
| P_vector ps,_ -> acc @ ps
| _, (Nexp_aux (Nexp_constant length,_),_,_) ->
acc @ (List.map wild (range Big_int.zero (Big_int.sub length (Big_int.of_int 1))))
| _, _ ->
(*if is_last then*) acc @ [wild Big_int.zero]
else raise
(Reporting_basic.err_unreachable l
("remove_vector_concats: Non-vector in vector-concat pattern " ^
string_of_typ (typ_of_annot annot))) in
let has_length (P_aux (p,annot)) =
let typ = Env.base_typ_of (env_of_annot annot) (typ_of_annot annot) in
match vector_typ_args_of typ with
| (Nexp_aux (Nexp_constant length,_),_,_) -> true
| _ -> false in
let ps_tagged = tag_last ps in
let ps' = List.fold_left aux [] ps_tagged in
let last_has_length ps = List.exists (fun (p,b) -> b && has_length p) ps_tagged in
if last_has_length ps then
P_vector ps'
else
(* If the last vector pattern in the vector_concat pattern has unknown
length we misuse the P_vector_concat constructor's argument to place in
the following way: P_vector_concat [x;y; ... ;z] should be mapped to the
pattern-match x :: y :: .. z, i.e. if x : 'a, then z : vector 'a. *)
P_vector_concat ps' in
{id_pat_alg with p_vector_concat = p_vector_concat} in
let pat = fold_pat remove_vector_concats pat in
(pat,letbinds,decls)
(* assumes there are no more E_internal expressions *)
let rewrite_exp_remove_vector_concat_pat rewriters (E_aux (exp,(l,annot)) as full_exp) =
let rewrap e = E_aux (e,(l,annot)) in
let rewrite_rec = rewriters.rewrite_exp rewriters in
let rewrite_base = rewrite_exp rewriters in
match exp with
| E_case (e,ps) ->
let aux = function
| (Pat_aux (Pat_exp (pat,body),annot')) ->
let (pat,_,decls) = remove_vector_concat_pat pat in
Pat_aux (Pat_exp (pat, decls (rewrite_rec body)),annot')
| (Pat_aux (Pat_when (pat,guard,body),annot')) ->
let (pat,_,decls) = remove_vector_concat_pat pat in
Pat_aux (Pat_when (pat, decls (rewrite_rec guard), decls (rewrite_rec body)),annot') in
rewrap (E_case (rewrite_rec e, List.map aux ps))
| E_let (LB_aux (LB_val (pat,v),annot'),body) ->
let (pat,_,decls) = remove_vector_concat_pat pat in
rewrap (E_let (LB_aux (LB_val (pat,rewrite_rec v),annot'),
decls (rewrite_rec body)))
| exp -> rewrite_base full_exp
let rewrite_fun_remove_vector_concat_pat
rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))) =
let rewrite_funcl (FCL_aux (FCL_Funcl(id,pexp),(l,annot))) =
let pat,guard,exp,pannot = destruct_pexp pexp in
let (pat',_,decls) = remove_vector_concat_pat pat in
let guard' = match guard with
| Some exp -> Some (decls (rewriters.rewrite_exp rewriters exp))
| None -> None in
let exp' = decls (rewriters.rewrite_exp rewriters exp) in
let pexp' = construct_pexp (pat',guard',exp',pannot) in
(FCL_aux (FCL_Funcl (id,pexp'),(l,annot)))
in FD_aux (FD_function(recopt,tannotopt,effectopt,List.map rewrite_funcl funcls),(l,fdannot))
let rewrite_defs_remove_vector_concat (Defs defs) =
let rewriters =
{rewrite_exp = rewrite_exp_remove_vector_concat_pat;
rewrite_pat = rewrite_pat;
rewrite_let = rewrite_let;
rewrite_lexp = rewrite_lexp;
rewrite_fun = rewrite_fun_remove_vector_concat_pat;
rewrite_def = rewrite_def;
rewrite_defs = rewrite_defs_base} in
let rewrite_def d =
let d = rewriters.rewrite_def rewriters d in