forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcfLetAutoLib.sml
1837 lines (1616 loc) · 69.6 KB
/
cfLetAutoLib.sml
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
structure cfLetAutoLib :> cfLetAutoLib =
struct
open preamble ml_progLib cfTacticsLib ml_translatorTheory
eqSolveRewriteLib Satisfy cfLetAutoTheory
(* TODO: move *)
(* set_sep syntax *)
val (sep_imp_tm,mk_sep_imp,dest_sep_imp,is_sep_imp) = syntax_fns2 "set_sep" "SEP_IMP";
(* -- *)
(* semanticPrimitives syntax *)
val (sem_env_c_tm,mk_sem_env_c,dest_sem_env_c,is_sem_env_c) = syntax_fns1 "semanticPrimitives" "sem_env_c";
(* -- *)
val set_sep_cond_hprop_tm =
mk_thy_const{Name="cond",Thy="set_sep",Ty= bool --> cfHeapsBaseSyntax.hprop_ty}
fun mk_cond_hprop tm = mk_comb(set_sep_cond_hprop_tm,tm)
(* TODO: move these to preamble, or Drule? *)
(********************************************************************************************)
(******************** Some conversions used to perform the matching *************************)
(*
MP_ASSUM:
(!a in T'. T |= a) T' |= g
===============================
T |= g
*)
fun MP_ASSUML thl th =
let
val conclList = List.map (fn x => (concl x, x)) thl
val conclMap = Redblackmap.fromList Term.compare conclList
val num_hyps = List.length (hyp th)
val th' = DISCH_ALL th
fun rec_mp th n =
if n > 0 then
let
val h = concl th |> dest_imp |> fst
val hyp_th = (Redblackmap.find (conclMap, h) handle NotFound =>
raise (ERR "MP_ASSUML" ("Could not find the hypothesis: " ^(term_to_string h))))
val th' = MP th hyp_th
in
rec_mp th' (n-1)
end
else th
in
rec_mp th' num_hyps
end;
(*
CONV_ASSUM: use a conversion to rewrite an assumption list so that:
(!a' in T'. T |= a') /\ (!a in T. T' |= a)
Returns the list of theorems: !a' in T'. T |= a'
*)
fun CONV_ASSUM sset rws asl =
let
val tautl = List.map ASSUME asl |> List.map CONJUNCTS |> List.concat
fun try_conv th = (CONV_RULE (SIMP_CONV sset rws) th handle HOL_ERR _ => th)
in
List.map try_conv tautl
end;
(**** INTRO_REWRITE: use rewrite rules of the form h1 ==> ... ==> hn ==> PAT <=> y = z ********)
(* INTRO_REWRITE_CONV *)
fun INTRO_REWRITE_CONV thl asl =
let
val base_thms = (List.map ASSUME asl) @ thl
val disj_thl = List.concat (List.map CONJUNCTS thl)
fun match_on_asl th = mapfilter (MATCH_MP th) base_thms
fun is_rw_th th = SPEC_ALL th |> concl |> is_eq
fun generate_rewrites thl =
let
val (rewrite_thl, thl') = List.partition is_rw_th thl
val thl'' = List.concat (mapfilter match_on_asl thl')
in
case thl'' of
[] => rewrite_thl
| _ => List.revAppend (generate_rewrites thl'', rewrite_thl)
end
val rw_thms = generate_rewrites disj_thl
in
SIMP_CONV bool_ss rw_thms
end;
(* INTRO_REWRITE_TAC *)
fun INTRO_REWRITE_TAC rws (g as (asl, w)) = CONV_TAC (INTRO_REWRITE_CONV rws asl) g;
(* RENAME_SPEC_ALL *)
fun RENAME_SPEC_ALL varsl th =
let
val (v, th') = SPEC_VAR th
val v' = variant varsl v
in
if v !~ v' then
RENAME_SPEC_ALL (v'::varsl) (Thm.INST [v |-> v'] th')
else
RENAME_SPEC_ALL (v::varsl) th'
end
handle HOL_ERR _ => th;
(************************ Functions ************************************************)
val ERR = mk_HOL_ERR "cfLetAutoLib";
(* TODO: move to semanticPrimitivesSyntax *)
val (build_conv_tm, mk_build_conv, dest_build_conv, is_build_conv) = HolKernel.syntax_fns3 "semanticPrimitives" "build_conv";
(* TODO: move to cfcNormaliseSyntax? *)
val (exp2v_tm, mk_exp2v, dest_exp2v, is_exp2v) = HolKernel.syntax_fns2 "cfNormalise" "exp2v";
(* Manipulation of expressions *)
fun get_value env e =
cfTacticsLib.reduce_conv (mk_exp2v (env, e))
|> concl |> rhs |> optionSyntax.dest_some;
(* Rename a variable by adding numbers rather than adding primes - useful for
xlet_auto, which introduces variables (Postv, Poste, Post) *)
fun dest_suffix s =
let
fun is_suffix_char c = Char.isDigit c orelse c = #"'"
fun rec_dest s1 (c::s2) =
if is_suffix_char c then rec_dest (c::s1) s2
else (List.rev (c::s2), s1)
| rec_dest s [] = failwith "dest_suffix"
in
rec_dest [] (List.rev s)
end;
fun ivariant varsl v =
let
val _ = if (not o is_var) v then
raise (ERR "variant" "not a variable") else ()
val varnamesl = (List.map (fst o dest_var) varsl) @
(List.map (fst o dest_const) (Term.all_consts ()))
val varnames_set = HOLset.fromList String.compare varnamesl
val vname = (fst o dest_var) v
in
case HOLset.member (varnames_set, vname) of
true =>
let
val name_pre = (implode o fst o dest_suffix o explode) vname
val filt_names = List.filter
(fn x => String.isPrefix name_pre x) varnamesl
val l = String.size name_pre
fun drop s = String.substring (s, l, String.size s - l)
val suffixes = List.map drop filt_names
val nums = mapfilter string_to_int suffixes
val max_s = List.foldr Int.max 0 nums
val suffix = Int.toString (max_s + 1)
val new_name = String.concat [name_pre, suffix]
in
mk_var (new_name, type_of v)
end
| false => v
end;
(* [rename_dest_postv]
Deconstructs the POSTv of a heap condition and rename the POSTv value
so that it is a fresh variable. *)
fun rename_dest_postv (varsl, c) =
let
val (v, c1) = cfHeapsBaseSyntax.dest_postv c
val v' = variant varsl v
val c2 = Term.subst [v |-> v'] c1
in
(v', c2)
end;
(* [rename_dest_poste]
Deconstructs the POSTe of a heap condition and rename the POSTe value
so that it is a fresh variable. *)
fun rename_dest_poste (varsl, c) =
let
val (v, c1) = cfHeapsBaseSyntax.dest_poste c
val v' = variant varsl v
val c2 = Term.subst [v |-> v'] c1
in
(v', c2)
end;
(* [dest_post_condition] *)
fun dest_post_condition c =
if cfHeapsBaseSyntax.is_postv c then
let
val (postv_v, postv_pred) = cfHeapsBaseSyntax.dest_postv c
in
(SOME postv_v, SOME postv_pred, NONE, NONE) end
else if cfHeapsBaseSyntax.is_poste c then
let
val (poste_v, poste_pred) = cfHeapsBaseSyntax.dest_poste c
in
(NONE, NONE, SOME poste_v, SOME poste_pred) end
else if cfHeapsBaseSyntax.is_post c then
let
val (postv_v, postv_pred, poste_v, poste_pred) = cfHeapsBaseSyntax.dest_post c
in
(SOME postv_v, SOME postv_pred, SOME poste_v, SOME poste_pred) end
else
raise (ERR "rename_dest_post" "Not a heap post-condition");
(* [rename_dest_post] *)
fun rename_dest_post (varsl, c) =
if cfHeapsBaseSyntax.is_postv c then
let
val (postv_v, postv_pred) = cfHeapsBaseSyntax.dest_postv c
val postv_v' = variant varsl postv_v
val postv_pred' = Term.subst [postv_v |-> postv_v'] postv_pred
in
(SOME postv_v', SOME postv_pred', NONE, NONE) end
else if cfHeapsBaseSyntax.is_poste c then
let
val (poste_v, poste_pred) = cfHeapsBaseSyntax.dest_poste c
val poste_v' = variant varsl poste_v
val poste_pred' = Term.subst [poste_v |-> poste_v'] poste_pred
in
(NONE, NONE, SOME poste_v', SOME poste_pred') end
else if cfHeapsBaseSyntax.is_post c then
let
val (postv_v, postv_pred, poste_v, poste_pred) = cfHeapsBaseSyntax.dest_post c
val postv_v' = variant varsl postv_v
val postv_pred' = Term.subst [postv_v |-> postv_v'] postv_pred
val poste_v' = variant (postv_v'::varsl) poste_v
val poste_pred' = Term.subst [poste_v |-> poste_v'] poste_pred
in
(SOME postv_v', SOME postv_pred', SOME poste_v', SOME poste_pred') end
else
raise (ERR "rename_dest_post" "Not a heap post-condition");
(* [rename_dest_exists]
Deconstructs the existential quantifiers of a heap condition,
and rename the previsouly bound variables to prevent name conflicts. *)
fun rename_dest_exists (varsl, c) =
let fun rec_dest varsl lv c =
if is_sep_exists c then
let
val (nv, nc) = dest_sep_exists c
val nv' = variant varsl nv
val nc' = Term.subst [nv |-> nv'] nc
val (nlv, fc) = rec_dest (nv'::varsl) lv nc'
in
(nv'::nlv, fc)
end
else
(([]:term list), c)
in
rec_dest varsl ([]:term list) c
end;
(* [dest_pure_fact]
Deconstructs a pure fact (a heap predicate of the form &P) *)
fun dest_pure_fact p =
case (dest_term p) of
COMB dp =>
(if same_const set_sep_cond_hprop_tm (#1 dp) then (#2 dp)
else raise (ERR "dest_pure_fact" "Not a pure fact"))
| _ => raise (ERR "dest_pure_fact" "Not a pure fact");
(* [sort_heap_pred]
Determines whether a heap predicate is a pure fact or not,
and adds it to the according list. *)
fun sort_heap_pred hp hpl pfl =
let
val pure_pred = dest_pure_fact hp
in
(hpl, pure_pred::pfl)
end
handle HOL_ERR _ => (hp::hpl, pfl);
(* list_dest_star
Deconstructs a (star) conjunction of heap conditions.
Splits the conjuncts between heap conditions and pure facts.
*)
fun list_dest_star c =
let fun rec_dest hpl pfl c =
let
val (nc1, nc2) = dest_star c
val (hpl1, pfl1) = rec_dest hpl pfl nc1
val (hpl2, pfl2) = rec_dest hpl1 pfl1 nc2
in
(hpl2, pfl2)
end
handle HOL_ERR _ => sort_heap_pred c hpl pfl
in
rec_dest ([]:term list) ([]:term list) c
end;
(* [dest_heap_condition]
Deconstructs a heap predicate. Needs to be provided a list of terms
representing variables to avoid name collision
Returns:
- the list of existentially quantified variables
- the list of heap pointers used in the heap predicates
- the list of heap predicates
- the list of pure facts *)
fun dest_heap_condition (varsl, c) =
let
val (ex_vl, c') = rename_dest_exists (varsl, c)
val (hpl, pfl) = list_dest_star c'
in
(ex_vl, hpl, pfl)
end;
(* [mk_heap_condition]
Creates a heap condition of the form:
(SEP_EXISTS x1...xn. H1 * ... Hk * &P1 * ... * &Pl)
Parameters:
- the list of existentially quantified variables
- the list of heap predicates
- the list of pure facts
*)
fun mk_heap_condition (ex_vl, hpl, pfl) =
let
val c1 = list_mk_star hpl cfHeapsBaseSyntax.hprop_ty
val hprop_pfl = List.map (fn x => mk_comb (set_sep_cond_hprop_tm, x)) pfl
val c2 = list_mk_star (c1::hprop_pfl) cfHeapsBaseSyntax.hprop_ty
val c3 = List.foldr mk_sep_exists c2 ex_vl
in
c3
end;
(* [mk_post_condition]
Creates a heap post condition.
Parameters:
- the optional postv value
- the optional postv predicate
- the optional poste value
- the optional poste predicate
*)
fun mk_post_condition (postv_v, postv_pred, poste_v, poste_pred) =
case (postv_v, postv_pred, poste_v, poste_pred) of
(SOME postv_v, SOME postv_pred, NONE, NONE) => cfHeapsBaseSyntax.mk_postv (postv_v, postv_pred)
| (NONE, NONE, SOME poste_v, SOME poste_pred) => cfHeapsBaseSyntax.mk_poste (poste_v, poste_pred)
| (SOME postv_v, SOME postv_pred, SOME poste_v, SOME poste_pred) =>
cfHeapsBaseSyntax.mk_post (postv_v, postv_pred, poste_v, poste_pred)
| _ => raise (ERR "mk_heap_post_condition" "Not valid parameters");
(******** Get the post-condition given by the app specification ***********)
(* [find_spec]
Finds a proper specification for the application in the goal.
The code has been taken from xspec (cfTactics) *)
fun find_spec g =
let
val (asl, w) = (xapp_prepare_goal g) |> #1 |> List.hd
val (ffi_ty, f) = (goal_app_infos w)
in
case xspec_in_asl f asl of
SOME (k, a) =>
(print
("Using a " ^ (spec_kind_toString k) ^
" specification from the assumptions\n");
cf_spec ffi_ty k (ASSUME a))
| NONE =>
case xspec_in_db f of
SOME (thy, name, k, thm) =>
(print ("Using " ^ (spec_kind_toString k) ^
" specification " ^ name ^
" from theory " ^ thy ^ "\n");
cf_spec ffi_ty k thm)
| NONE =>
raise ERR "find_spec" ("Could not find a specification for " ^
fst (dest_const f))
end;
(* [rename_dest_foralls]
Removes the forall operators from a term. Renames the bound
variables so that they are fresh regarding a given list
of assumptions *)
fun rename_dest_foralls (asl, spec) =
let
val fvl = free_varsl asl
fun rec_remove fvl spec =
if not (is_forall spec) then (([]:term list), spec)
else
let
val (x, spec') = dest_forall spec
val x' = variant fvl x
val subst_spec = Term.subst [x |-> x'] spec'
val (xl, fspec) = rec_remove (x'::fvl) subst_spec
in
(x'::xl, fspec)
end
in
rec_remove fvl spec
end;
(* [xlet_find_spec]
Find the app specification to use given a goal to prove *)
fun xlet_find_spec g =
let
(* Find the specification *)
val dummy_spec = `POSTv (v:v). &T`
val g' = xlet dummy_spec g |> #1 |> List.hd
in
SPEC_ALL(find_spec g')
end;
(* [xlet_dest_app_spec] *)
fun xlet_dest_app_spec asl let_pre specH =
let
(* Get the parameters and pre/post-conditions written in the specification *)
val (_, noquant_spec_tm) = rename_dest_foralls ((let_pre::asl), (concl specH))
val impsl_spec = list_dest dest_imp noquant_spec_tm
val app_asl = List.take (impsl_spec, (List.length impsl_spec)-1)
val app_spec = List.last impsl_spec
in
(app_asl, app_spec)
end;
(* [xlet_subst_parameters]
The app specification is supposed to be quantified over all the "unknwn" variables.
*)
fun xlet_subst_parameters env app_info asl let_pre app_spec =
let
(* Retrieve the list of free variables *)
val fvset = FVL ((concl app_spec)::app_info::let_pre::asl) empty_varset
val fvl = HOLset.listItems fvset
(* Retrieve the type variables *)
val asl_atoms = all_atomsl (app_info::let_pre::asl) empty_tmset
val asl_typevars =
HOLset.foldr (fn (a, ts) => HOLset.addList(ts, type_vars (type_of a)))
(HOLset.empty Type.compare) asl_atoms
val spec_atoms = all_atoms (concl (DISCH_ALL app_spec))
val spec_typevars =
HOLset.foldr (fn (a, ts) => HOLset.addList(ts, type_vars (type_of a)))
(HOLset.empty Type.compare) spec_atoms
val redundant_typevars = HOLset.intersection(asl_typevars, spec_typevars)
|> HOLset.listItems
val all_typevars = HOLset.union(asl_typevars, spec_typevars)
|> HOLset.listItems
val all_typevars_names = HOLset.addList (HOLset.empty String.compare,
List.map dest_vartype all_typevars)
val red_typevars_names = List.map dest_vartype redundant_typevars
(* Substitute the redundant type variables *)
fun rename_typevar varnames name i =
let
val name' = name ^(Int.toString i)
in
if HOLset.member(varnames, name') then rename_typevar varnames name (i+1)
else name'
end
fun rename_typevars varnames (vn::vars) =
let
val (varnames', pairs) = rename_typevars varnames vars
val vn' = rename_typevar varnames' vn 0
val varnames'' = HOLset.add(varnames', vn')
in
(varnames'', (vn, vn')::pairs)
end
| rename_typevars varnames [] = (varnames, [])
val (_, new_type_names) = rename_typevars all_typevars_names red_typevars_names
val type_subst = List.map (fn (x, y) => (mk_vartype x |-> mk_vartype y)) new_type_names
val app_spec = Thm.INST_TYPE type_subst app_spec
(* Find the parameters given to the function *)
val (app_info', parameters) = dest_comb app_info
val (params_expr_list, _) = listSyntax.dest_list parameters
val params_tm_list = List.map (get_value env) params_expr_list
(* NOT SURE if proper way: rewrite the values to prevent conflicts with the
parameters found by xapp_spec *)
val asl_thms = List.map ASSUME asl
val params_tm_list = List.map (fn x => QCONV (SIMP_CONV bool_ss asl_thms) x
|> concl |> dest_eq |> snd) params_tm_list
(*************************************************)
(* Find the app variable *)
val (app_info'', app_var) = dest_comb app_info'
val app_value = get_value env app_var
(* TODO: evaluate the app variable *)
(* Find the ffi variable *)
val ffi = dest_comb app_info'' |> snd
(* Get the parameters written in the specification *)
val inst_app_spec = RENAME_SPEC_ALL fvl app_spec
val app_spec1 = concl inst_app_spec |> list_dest dest_imp |> List.last
val app_spec2 = dest_comb app_spec1 |> fst
val app_spec3 = dest_comb app_spec2 |> fst
val (app_spec4, spec_parameters) = dest_comb app_spec3
val (spec_params_tm_list, _) = listSyntax.dest_list spec_parameters
(* Get the app variable written in the specification *)
val (app_spec5, spec_app_var) = dest_comb app_spec4
val (spec_params_tm_list, params_tm_list) =
if is_var spec_app_var then
(spec_app_var::spec_params_tm_list, app_value::params_tm_list)
else (spec_params_tm_list, params_tm_list)
(* And the ffi variable written in the specification *)
val spec_ffi = dest_comb app_spec5 |> snd
(* Match the parameters *)
fun create_subst l1 l2 =
(case (l1, l2) of
(e1::l1', e2::l2') =>
let
val tys1 = match_type (type_of e1) (type_of e2)
val (tms2, tys2) = create_subst l1' l2'
in
((e1, e2)::tms2, List.concat [tys1, tys2])
end
| ([], []) => ([], [])
| _ => failwith "create_subst")
val (tm_pairs, ty_subst) = create_subst (spec_ffi::spec_params_tm_list) (ffi::params_tm_list)
val params_subst = List.map (fn (x, y) => (Term.inst ty_subst x |-> y)) tm_pairs
(* Perform the substitution in the app specification *)
val typed_app_spec = Thm.INST_TYPE ty_subst inst_app_spec
val subst_app_spec = Thm.INST params_subst typed_app_spec
in
subst_app_spec
end;
(*
Analyses a theorem of the form:
HPROP_INJ A B EQ
Returns: (A, B, EQ)
*)
val (hprop_inj_tm,mk_hprop_inj,dest_hprop_inj,is_hprop_inj) = syntax_fns3 "cfLetAuto" "HPROP_INJ"
fun convert_extract_thm th =
let
val c = strip_forall (concl th) |> snd
in
dest_hprop_inj c
end
handle HOL_ERR _ => raise (ERR "hprop_extract_pattern"
("not a valid heap extraction theorem: " ^(thm_to_string th)))
(* Some auxiliary definitions for the match_heap_conditions function *)
fun mk_sep_imp_hprop (t1,t2) =
mk_sep_imp (assert (equal cfHeapsBaseSyntax.hprop_ty o type_of) t1,t2)
(* Convert equations to substitutions *)
fun convert_eqs_to_subs eqs =
let
val eql = list_dest dest_conj eqs |> List.map dest_eq
val tsubst = List.map (fn (x, y) => (x |-> y)) eql
in
tsubst
end;
(*
Rename the variable(s) introduced by POSTv/POSTe/POST.
Use the name of the shallow embedding if it is a variable, or its type if it is
a constant.
*)
val type_to_name =
[
(equal intSyntax.int_ty, "iv"),
(equal numSyntax.num, "nv"),
(equal bool, "bv"),
(equal oneSyntax.one_ty, "uv"),
(listSyntax.is_list_type, "lv"),
(equal stringSyntax.string_ty, "sv"),
(equal mlstringSyntax.mlstring_ty, "sv"),
(can dom_rng, "fv"),
(K true, "v")
];
val x = mk_var("x",alpha);
val RI = mk_var("RI",alpha --> semanticPrimitivesSyntax.v_ty --> bool)
fun rename_post_variables ri_thms asl post_condition =
let
val ri_terms = mapfilter (snd o dest_comb o concl) ri_thms
val ri_set = HOLset.fromList Term.compare ri_terms
val varset = FVL asl empty_varset
val varsl = HOLset.listItems varset
val (v_o, vpred_o, e_o, epred_o) = dest_post_condition post_condition
(* Rename the exception *)
val (e_o', epred_o') =
case (e_o, epred_o) of
(SOME e, SOME pred) =>
let
val n_e = ivariant varsl e
val n_pred = Term.subst [e |-> n_e] pred
in
(SOME n_e, SOME n_pred)
end
| _ => (e_o, epred_o)
(* Rename the ressource *)
val (v_o', vpred_o') =
case (v_o, vpred_o) of
(SOME v, SOME H) =>
(let
(* Find the predicate giving information about the type of v *)
val preds = list_dest dest_star H
val pat = mk_cond_hprop(list_mk_comb(RI,[x,v]))
val sgl = HOLset.add (empty_varset, v)
fun get_shallow p =
let
val (tms, tys) = match_terml [] sgl pat p
val (tms', tys') = norm_subst ((tms, empty_varset), (tys, []))
val apply_subst = (Term.subst tms') o (Term.inst tys')
val RI = apply_subst RI
val shallow = apply_subst x
in
(* Check that RI is a refinement invariant *)
if HOLset.member (ri_set, RI) then shallow else failwith ""
end
val shallow = tryfind get_shallow preds
in
case is_var shallow of
true =>
let
val x_name = (fst o dest_var) shallow
val v_name = String.concat [x_name, "v"]
val n_var = ivariant varsl (mk_var(v_name, semanticPrimitivesSyntax.v_ty))
val n_pred = Term.subst [v |-> n_var] H
in
(SOME n_var, SOME n_pred)
end
| false =>
let
val s_t = type_of shallow
fun name_from_type (t,_) = t s_t
val v_name = #2 (Lib.first name_from_type type_to_name)
val n_var = ivariant varsl (mk_var(v_name, semanticPrimitivesSyntax.v_ty))
val n_pred = Term.subst [v |-> n_var] H
in
(SOME n_var, SOME n_pred)
end
end
handle HOL_ERR _ =>
let
val n_var = ivariant varsl v
val n_pred = Term.subst [v |-> n_var] H
in
(SOME n_var, SOME n_pred)
end)
| _ => (v_o, vpred_o)
in
mk_post_condition (v_o', vpred_o', e_o', epred_o')
end
handle HOL_ERR _ => raise (ERR "rename_post_variables" "");
(*********************************************************************************
*
* Theorems, conversions, solvers used by the xlet_auto tactic
*
*********************************************************************************)
(* Auxiliary function for the exporters *)
fun mk_export_f f (thy_name : string) (named_thms : (string * thm) list) =
f (List.map snd named_thms);
(* Theorems used to compute the frame *)
val FRAME_THMS = ref [REF_HPROP_INJ,
ARRAY_HPROP_INJ,
W8ARRAY_HPROP_INJ
];
fun add_frame_thms thms = FRAME_THMS := (thms @ !FRAME_THMS);
fun get_frame_thms () = !FRAME_THMS;
val {mk,dest,export} = ThmSetData.new_exporter "hprop_inj"
(mk_export_f add_frame_thms);
fun export_frame_thms slist = List.app export slist;
(* Refinement invariants: definitions *)
val RI_DEFSL = ref ([] : thm list);
fun add_RI_defs defs = (RI_DEFSL := defs @ !RI_DEFSL);
fun get_RI_defs uv = !RI_DEFSL;
(* Theorem generation *)
fun generate_expand_retract_thms ri_defs =
let
val ri_l = List.map (fn x => SPEC_ALL x |> concl |> dest_eq |> fst) ri_defs
fun inst_ri ri =
let
val ty = dest_type (type_of ri) |> snd |> List.hd
val v = mk_var ("v", ty)
val v' = variant (free_vars ri) v
in
mk_comb (ri, v')
end
handle HOL_ERR _ => ri
| Empty => ri
val inst_ri_l = List.map inst_ri ri_l
val expandThms = List.map (GEN_ALL o (SIMP_CONV (srw_ss()) (ri_defs @ !RI_DEFSL))) inst_ri_l
val retractThms = List.map GSYM expandThms
in
(expandThms, retractThms)
end;
(* Theorems to expand or retract the definitions of refinement invariants*)
val RI_EXPAND_THMSL = ref ([UNIT_TYPE_EXPAND] : thm list);
val RI_RETRACT_THMSL = ref ([UNIT_TYPE_RETRACT] : thm list);
fun add_expand_retract_thms expandThms retractThms =
(RI_EXPAND_THMSL := expandThms @ !RI_EXPAND_THMSL;
RI_RETRACT_THMSL := retractThms @ !RI_RETRACT_THMSL);
fun get_expand_thms () = !RI_EXPAND_THMSL;
fun get_retract_thms () = !RI_RETRACT_THMSL;
val EXPAND_TAC = FULL_SIMP_TAC (srw_ss()) (get_expand_thms());
val RETRACT_TAC = FULL_SIMP_TAC (srw_ss()) (get_retract_thms());
val REWRITE_RI_TAC = EXPAND_TAC THEN RETRACT_TAC;
(* List of equality types *)
val EQUALITY_TYPE_THMS = ref ([] : thm list);
fun add_equality_type_thms thms =
(EQUALITY_TYPE_THMS := (List.concat (List.map CONJUNCTS thms))
@ !EQUALITY_TYPE_THMS);
fun get_equality_type_thms () = !EQUALITY_TYPE_THMS;
(* Unicity theorems *)
val INTRO_RW_THMS = ref ([NUM_INT_EQ, LIST_REL_UNICITY_RIGHT, LIST_REL_UNICITY_LEFT, EQTYPE_UNICITY_R, EQTYPE_UNICITY_L]);
fun add_intro_rewrite_thms thms = (INTRO_RW_THMS := thms @ !INTRO_RW_THMS);
fun get_intro_rewrite_thms () = !INTRO_RW_THMS;
(* Automatic generation of theorems *)
fun generate_RI_unicity_thms eq_type_thms =
let
fun get_ref_inv th = concl th |> dest_comb |> snd
fun get_types ref_inv =
let
fun two_el [x,y] = (x,y)
| two_el _ = failwith "get_types"
val (t1,t') = type_of ref_inv |> dest_type |> snd |> two_el
val (t2, _) = dest_type t' |> snd |> two_el
in
(t1, t2)
end
fun gen_left_rule eq_type_thm =
let
val ref_inv = get_ref_inv eq_type_thm
val (t1, t2) = get_types ref_inv
val th1 = Thm.INST_TYPE [alpha |-> t1, beta |-> t2] EQTYPE_UNICITY_L
val th2 = SPEC ref_inv th1
val (x1, x2, y) = (mk_var("x1", t1), mk_var("x2", t1), mk_var("y", t2))
val th3 = SPECL [x1, x2, y] th2
val th4 = MP th3 eq_type_thm
val th5 = GEN_ALL th4
in
th5
end
fun gen_right_rule eq_type_thm =
let
val ref_inv = get_ref_inv eq_type_thm
val (t1, t2) = get_types ref_inv
val th1 = Thm.INST_TYPE [alpha |-> t1, beta |-> t2] EQTYPE_UNICITY_R
val th2 = SPEC ref_inv th1
val (x, y1, y2) = (mk_var("x", t1), mk_var("y1", t2), mk_var("y2", t2))
val th3 = SPECL [x, y1, y2] th2
val th4 = MP th3 eq_type_thm
val th5 = GEN_ALL th4
in
th5
end
val eq_type_thms = List.concat(List.map CONJUNCTS eq_type_thms)
val left_rules = List.map gen_left_rule eq_type_thms
val right_rules = List.map gen_right_rule eq_type_thms
in
List.concat [left_rules, right_rules]
end;
fun export_equality_type_thms_aux thms =
let
val thms = List.map (CONV_RULE (PURE_REWRITE_CONV [satTheory.AND_IMP])) thms
(* val unicity_thms = generate_RI_unicity_thms thms *)
in
add_equality_type_thms thms
(* ; add_intro_rewrite_thms unicity_thms *)
end;
val {mk,dest,export} = ThmSetData.new_exporter "equality_types"
(mk_export_f export_equality_type_thms_aux);
fun export_equality_type_thms slist = List.app export slist;
val _ = export_equality_type_thms_aux [EqualityType_NUM_BOOL,
EqualityType_LIST_TYPE,
EqualityType_PAIR_TYPE];
(* Basic rewrite theorems *)
val RW_THMS = ref [(* Handle the int_of_num operator *)
integerTheory.INT_ADD,
INT_OF_NUM_TIMES,
INT_OF_NUM_LE,
INT_OF_NUM_LESS,
INT_OF_NUM_GE,
INT_OF_NUM_GREAT,
INT_OF_NUM_EQ,
INT_OF_NUM_SUBS,
INT_OF_NUM_SUBS_2,
(* Handle lists *)
LENGTH_NIL,
LENGTH_NIL_SYM,
REPLICATE_APPEND_DECOMPOSE,
REPLICATE_APPEND_DECOMPOSE_SYM,
LIST_REL_DECOMPOSE_RIGHT,
LIST_REL_DECOMPOSE_LEFT,
LENGTH_REPLICATE,
TAKE_LENGTH_ID,
DROP_nil,
DROP_LENGTH_TOO_LONG,
NULL_EQ,
(* REPLICATE *)
(* REPLICATE_PLUS_ONE *)
(*mlbasicsProgTheory.not_def*)
(* Arithmetic equations simplification *)
NUM_EQ_SIMP1,
NUM_EQ_SIMP2,
NUM_EQ_SIMP3,
NUM_EQ_SIMP4,
NUM_EQ_SIMP5,
NUM_EQ_SIMP6,
NUM_EQ_SIMP7,
NUM_EQ_SIMP8,
NUM_EQ_SIMP9,
NUM_EQ_SIMP10,
NUM_EQ_SIMP11,
NUM_EQ_SIMP12,
MIN_DEF
];
fun add_rewrite_thms thms = (RW_THMS := thms @ !RW_THMS);
fun get_rewrite_thms () = !RW_THMS;
(* Default simpset *)
val DEF_SIMPSET = ref pure_ss;
val _ = (DEF_SIMPSET := srw_ss());
(* TODO: Find a way to export that - like with ThmSetData.new_exporter *)
fun add_simp_frag sf = (DEF_SIMPSET := ((!DEF_SIMPSET) ++ sf));
fun get_default_simpset () = !DEF_SIMPSET;
fun add_refinement_invariants ri_defs =
let
val (expandThms, retractThms) = generate_expand_retract_thms ri_defs
val invertDefs = List.map GSYM ri_defs
in
add_RI_defs ri_defs;
add_expand_retract_thms (expandThms @ ri_defs) (invertDefs @ retractThms)
end;
val {mk,dest,export} = ThmSetData.new_exporter "refinement_invariants"
(mk_export_f add_refinement_invariants);
fun export_refinement_invariants slist = List.app export slist;
(* Don't put UNIT_TYPE in here and use UNIT_TYPE_EXPAND and UNIT_TYPE_RETRACT instead - because of the nature of the unit type, the automatically generated retract rule for UNIT_TYPE introduces a new variable: !u v. v = Conv NONE [] <=> UNIT_TYPE u v *)
val _ = add_refinement_invariants [NUM_def, INT_def, BOOL_def, STRING_TYPE_def];
fun add_match_thms thms =
let
(* Partition the theorems between the rewrite theorems and the intro rewrite ones *)
fun is_intro_rw t =
let
val (vars, t') = strip_forall t
val (imps, t'') = strip_imp t'
in
case (vars, imps) of
([], []) =>
(let
val (leq, req) = dest_eq t''
val lvars = HOLset.addList (empty_varset, free_vars leq)
val rvars = HOLset.addList (empty_varset, free_vars req)
in
not (HOLset.isSubset (rvars, lvars))
end
handle HOL_ERR _ => false)
| _ => is_intro_rw t''
end
val (intro_rws, rws) = List.partition (is_intro_rw o concl) thms
in
add_intro_rewrite_thms intro_rws;
add_rewrite_thms rws
end;
val {mk,dest,export} = ThmSetData.new_exporter "xlet_auto_match"
(mk_export_f add_match_thms);
fun export_match_thms slist = List.app export slist;
(* Store the last iteration of the manipulated app_spec for debugging purposes, if xlet_auto fails *)
val debug_app_spec = ref (REFL T)
fun debug_get_app_spec () = !debug_app_spec
fun debug_set_app_spec app_spec = (debug_app_spec := app_spec)
(************************************************************************************
*
* Match heap preconditions
*
************************************************************************************)
(* [match_heap_conditions] *)
fun match_heap_conditions hcond sub_hcond =
let
val extract_thms = get_frame_thms ()
(* Retrieve the extraction triplets *)
val extr_triplets = mapfilter convert_extract_thm extract_thms
val extr_pairs = List.map (fn (c, w, r) => (mk_sep_imp_hprop (c, w), r)) extr_triplets
(* Decompose the heap conditions *)
val hc_hpl = list_dest dest_star hcond |> List.filter (fn x => not (same_const cfHeapsBaseSyntax.emp_tm x))
val shc_hpl = list_dest dest_star sub_hcond |>
List.filter (fn x => (not (same_const cfHeapsBaseSyntax.emp_tm x)))
(* Perfom the matching *)
fun try_match obj pat_pair =
let
val tsubst = match_term (fst pat_pair) obj |> fst
val eqs = Term.subst tsubst (snd pat_pair)
in
convert_eqs_to_subs eqs
end
(* Interior loop *)
fun match_loop_int h1 [] = raise ERR "match_loop_int" "Empty"
| match_loop_int h1 (h2::hl2) =
if h1 = h2 then ([], hl2)
else
(let
val result = tryfind (try_match (mk_sep_imp_hprop (h1, h2))) extr_pairs
in
(result, hl2)
end
handle HOL_ERR _ =>
let val (results, hl2') = match_loop_int h1 hl2 in (results, h2::hl2') end)
(* Exterior loop *)
fun match_loop_ext (h1::hl1) hl2 =
(let
val (res1, hl2') = match_loop_int h1 hl2
val (results, hl1', hl2'') = match_loop_ext hl1 hl2'
in
(List.revAppend(res1, results), hl1', hl2'')
end
handle HOL_ERR _ =>
let val (results, hl1', hl2') = match_loop_ext hl1 hl2 in (results, h1::hl1', hl2') end)
| match_loop_ext [] hl2 = ([], [], hl2)
in
match_loop_ext hc_hpl shc_hpl
end;
(* [match_hconds] : match two pre-conditions in order to extract a frame *)
fun match_hconds rewrite_thms avoid_tms let_pre app_spec =
let
val sset = get_default_simpset ()
val app_pre = concl (UNDISCH_ALL app_spec) |> list_dest dest_imp |> List.last |>
dest_comb |> fst |> dest_comb |> snd
val rw_app_pre = (QCONV (SIMP_CONV sset rewrite_thms) app_pre |> concl |> dest_eq |> snd)
val rw_let_pre = (QCONV (SIMP_CONV sset rewrite_thms) let_pre |> concl |> dest_eq |> snd)
val (substsl, _, _) = match_heap_conditions let_pre app_pre
val filt_subst =
List.filter (fn {redex = x, residue = y} => not (HOLset.member (avoid_tms, x))) substsl
val used_subst = List.map (fn {redex = x, residue = y} => x) filt_subst
(* Instantiate the variables *)
val (vars_subst, terms_subst) =
List.partition (fn {redex = x, residue = y} => is_var x) filt_subst
val app_spec1 = Thm.INST vars_subst app_spec
(* And add the other equalities as new hypotheses *)
val terms_eqs = List.map (fn {redex = x, residue = y} => mk_eq(x, y)) terms_subst
val app_spec2 = List.foldr (fn (eq, th) => ADD_ASSUM eq th) app_spec1 terms_eqs
val app_spec3 = List.foldr (fn (eq, th) => DISCH eq th) app_spec2 terms_eqs
val app_spec4 = PURE_REWRITE_RULE [AND_IMP_INTRO] app_spec3
in
(app_spec4, used_subst)
end;
(*************** Heuristics *****************************************)
(* For each hypothesis of the app spec the list of possible substitutions
which make it match with one of the assumptions
*)
fun find_possible_instantiations tmsl0 tmsl1 =
let
(* Retrieve the known variables *)
val knwn_vars = FVL tmsl0 empty_varset
(* Retrieve the type variables present in tmsl0 *)
val atoms = all_atomsl tmsl0 empty_tmset
val knwn_typevarset =
HOLset.foldr (fn (a, ts) => HOLset.addList(ts, type_vars (type_of a)))
(HOLset.empty Type.compare) atoms
val knwn_typevars = HOLset.listItems knwn_typevarset
(* Match every term of tmsl0 against every term of tmsl1 *)
(*val tms_net = List.foldr (fn (x, net) => Net.insert (x, x) net) Net.empty tmsl0 *)
fun find_insts tm =