/
ml_translatorLib.sml
3827 lines (3613 loc) · 154 KB
/
ml_translatorLib.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 ml_translatorLib :> ml_translatorLib =
struct
open HolKernel boolLib bossLib;
open astTheory libTheory semanticPrimitivesTheory bigStepTheory namespaceTheory;
open terminationTheory stringLib astSyntax semanticPrimitivesSyntax;
open ml_translatorTheory ml_translatorSyntax intLib lcsymtacs;
open arithmeticTheory listTheory combinTheory pairTheory pairLib;
open integerTheory intLib ml_optimiseTheory ml_pmatchTheory;
open mlstringLib mlstringSyntax mlvectorSyntax packLib ml_progTheory ml_progLib
local open integer_wordSyntax in end
infix \\ val op \\ = op THEN;
val RW = REWRITE_RULE;
val RW1 = ONCE_REWRITE_RULE;
val get_term = let
val ys = unpack_list (unpack_pair unpack_string unpack_term) translator_terms
in fn s => snd (first (fn (n,_) => n = s) ys) end
fun primCases_on tm = Cases_on [ANTIQUOTE tm]
fun print_time s f x = f x
(*
let
val () = print "Starting "
val () = print s
val () = print "...\n"
val r = time f x
val () = print s
val () = print " done\n"
in r end
*)
exception UnableToTranslate of term;
exception UnsupportedType of hol_type;
exception NotFoundVThm of term;
(* code for managing state of certificate theorems *)
fun take 0 xs = []
| take n [] = []
| take n (x::xs) = x :: take (n-1) xs
fun MY_MP name th1 th2 =
MP th1 th2 handle e =>
let
val _ = print ("\n\n "^name^" MP th1 th2 failed, th1 is:\n\n")
val _ = print_thm th1
val _ = print "\n\nth2 is:\n\n"
val _ = print_thm th2
val _ = print "\n\n"
in raise e end
fun prove (goal,tac) = let
val (rest,validation) = tac ([],goal)
in if length rest = 0 then validation [] else let
in failwith "prove failed" end end
fun auto_prove proof_name (goal,tac) = let
val (rest,validation) = tac ([],goal) handle Empty => fail()
in if length rest = 0 then validation [] else let
in failwith("auto_prove failed for " ^ proof_name) end end
val word8 = wordsSyntax.mk_int_word_type 8
val word = wordsSyntax.mk_word_type alpha
val venvironment = mk_environment v_ty
val empty_dec_list = listSyntax.mk_nil astSyntax.dec_ty;
val Dtype_x = astSyntax.mk_Dtype (mk_var("x",#1(dom_rng(type_of astSyntax.Dtype_tm))));
val Dletrec_funs = astSyntax.mk_Dletrec (mk_var("funs",#1(dom_rng(type_of astSyntax.Dletrec_tm))));
val Dexn_n_l =
let val args = #1(boolSyntax.strip_fun(type_of astSyntax.Dexn_tm)) in
astSyntax.mk_Dexn (mk_var("n",el 1 args), mk_var("l",el 2 args))
end
val Dlet_v_x =
let val args = #1(boolSyntax.strip_fun(type_of astSyntax.Dlet_tm)) in
astSyntax.mk_Dlet (mk_var("v",el 1 args), mk_var("x",el 2 args))
end
fun Dtype ls = astSyntax.mk_Dtype(listSyntax.mk_list(ls,listSyntax.dest_list_type(#1(dom_rng(type_of astSyntax.Dtype_tm)))))
fun Tapp ls x = astSyntax.mk_Tapp(listSyntax.mk_list(ls,astSyntax.t_ty),x)
fun mk_store_v ty = mk_thy_type{Thy="semanticPrimitives",Tyop="store_v",Args=[ty]}
val v_store_v = mk_store_v v_ty
val refs_ty = listSyntax.mk_list_type v_store_v
val refs = mk_var("refs",refs_ty)
val refs' = mk_var("refs'",refs_ty)
val v = mk_var("v",v_ty)
val env_tm = mk_var("env",venvironment)
val cl_env_tm = mk_var("cl_env",venvironment)
val state_refs_tm = prim_mk_const{Name="state_refs",Thy="semanticPrimitives"}
fun D th = let
val th = th |> DISCH_ALL |> PURE_REWRITE_RULE [AND_IMP_INTRO]
in if is_imp (concl th) then th else DISCH T th end
fun is_const_str str = can prim_mk_const {Thy=current_theory(), Name=str};
fun find_const_name str = let
fun aux n = let
val s = str ^ "_" ^ int_to_string n
in if is_const_str s then aux (n+1) else s end
in if is_const_str str then aux 0 else str end
fun remove_Eq_from_v_thm th = let
val pat = get_term "arrow eq"
val tms = find_terms (can (match_term pat)) (concl th)
val vs = tms |> map (rand o rand o rator)
fun try_each f [] th = th
| try_each f (x::xs) th = try_each f xs (f x th handle HOL_ERR _ => th)
fun foo v th = let
val th = th |> GEN v
|> HO_MATCH_MP FUN_FORALL_INTRO
|> SIMP_RULE std_ss [FUN_QUANT_SIMP]
in th end
in try_each foo vs th end
fun normalise_assums th =
th |> DISCH_ALL |> PURE_REWRITE_RULE[GSYM AND_IMP_INTRO] |> UNDISCH_ALL
(* new state *)
val clean_on_exit = ref false;
local
val v_thms = ref ([] : (string (* name: "name" *) *
string (* ML name: "mlname" *) *
term (* HOL term: name *) *
thm (* certificate:
(concrete mode)
|- A name name_v
(abstract mode)
|- Eval env (Var (Short "mlname")) (A name) (inside module, or no module)
|- Eval env (Var (Long "modname" "mlname")) (A name) (after module) *) *
thm (* precond definition: |- T or |- name_side ... = ... or user-provided *) *
string option (* module name: "modname" *)) list);
val eval_thms = ref ([] : (string (* name *) *
term (* HOL term *) *
thm (* certificate: Eval env exp (P tm) *)) list);
val prog_state = ref ml_progLib.init_state;
in
fun get_ml_name (_:string,nm:string,_:term,_:thm,_:thm,_:string option) = nm
fun get_const (_:string,_:string,tm:term,_:thm,_:thm,_:string option) = tm
fun get_cert (_:string,_:string,_:term,th:thm,_:thm,_:string option) = th
fun get_pre (_:string,_:string,_:term,_:thm,th:thm,_:string option) = th
fun get_v_thms () = !v_thms
fun v_thms_reset () =
(v_thms := [];
eval_thms := [];
prog_state := ml_progLib.init_state);
fun ml_prog_update f = (prog_state := f (!prog_state));
fun get_ml_prog_state () = (!prog_state)
fun get_curr_env () = get_env (!prog_state);
fun get_curr_state () = get_state (!prog_state);
fun get_curr_v_defs () = get_v_defs (!prog_state);
fun get_curr_module_name () = let
val th = get_thm (!prog_state)
val tm = th |> concl |> rator |> rator |> rand
in if optionSyntax.is_none tm then NONE else
SOME (tm |> rand |> rator |> rand |> stringSyntax.fromHOLstring)
end
fun add_v_thms (name,ml_name,th,pre_def) = let
val thc = th |> concl
val (tm,th) =
if is_Eval thc then
(thc |> rand |> rand,
normalise_assums th)
else (thc |> rator |> rand,th)
val module_name = get_curr_module_name ()
val _ = if concl pre_def =T then () else
(print ("\nWARNING: " ^ml_name^" has a precondition.\n\n"))
in (v_thms := (name,ml_name,tm,th,pre_def,module_name) :: (!v_thms)) end;
(* if the order didn't matter...
fun replace_v_thm c th = let
val (found_v_thms,left_v_thms) = partition (same_const c o get_const) (!v_thms)
val (name,ml_name,_,_,pre,m) = hd found_v_thms
in v_thms := (name,ml_name,c,th,pre,m) :: left_v_thms end
*)
fun replace_v_thm c th = let
fun f [] = failwith "replace_v_thm: not found"
| f ((name,ml_name,c',th',pre,m)::vths) =
if same_const c c' then ((name,ml_name,c,th,pre,m)::vths)
else (name,ml_name,c',th',pre,m)::f vths
in v_thms := f (!v_thms) end
fun add_user_proved_v_thm th = let
val th = UNDISCH_ALL th
val v = th |> concl |> rand
val _ = (type_of v = v_ty) orelse failwith("add_user_proved_v_thm not a v thm")
val tm = th |> concl |> rator |> rand
val (name,ml_name,_,_,_,module_name) = first (fn (name,ml_name,tm,th,_,_) =>
(th |> concl |> rand) = v) (!v_thms)
in ((v_thms := (name,ml_name,tm,th,TRUTH,module_name) :: (!v_thms)); th) end;
fun get_bare_v_thm const = first (can (C match_term const) o get_const) (!v_thms)
fun lookup_v_thm const = let
val (name,ml_name,c,th,pre,m) = get_bare_v_thm const
val th = th |> SPEC_ALL |> UNDISCH_ALL
val th = (case m of
NONE => MATCH_MP Eval_Var_Short th
| SOME mod_name =>
if m = get_curr_module_name ()
then MATCH_MP Eval_Var_Short th
else (MATCH_MP Eval_Var_Long th
|> SPEC (stringSyntax.fromMLstring mod_name)))
val th = SPEC (stringSyntax.fromMLstring ml_name) th |> SPEC_ALL |> UNDISCH_ALL
in th end
fun lookup_abs_v_thm const =
let
val (name,ml_name,c,th,pre,m) = get_bare_v_thm const
val cth = concl th
val _ = is_Eval cth orelse raise NotFoundVThm const
val tm =
let
val precond = first is_PRECONDITION (hyp th)
in
th |> DISCH precond |> concl
|> curry list_mk_forall (free_vars precond)
end handle HOL_ERR _ => th |> concl
val code = rand(rator cth)
val tm =
if is_Var code then tm else
(* TODO: mk_Long depending on m *)
subst [code |-> mk_Var(mk_Short (stringSyntax.fromMLstring ml_name))] tm
in
ASSUME tm |> SPEC_ALL |> UNDISCH_ALL
end handle HOL_ERR {origin_function="first",...} => raise NotFoundVThm const
fun lookup_eval_thm const = let
val (name,c,th) = (first (fn c => can (match_term (#2 c)) const) (!eval_thms))
in th |> SPEC_ALL |> UNDISCH_ALL end
fun get_current_prog () =
get_thm (!prog_state)
|> CONV_RULE ((RATOR_CONV o RATOR_CONV o RATOR_CONV o RAND_CONV) EVAL);
fun update_precondition new_pre = let
fun update_aux (name,ml_name,tm,th,pre,module)= let
val th1 = D th
val th2 = PURE_REWRITE_RULE [new_pre,PRECONDITION_T] th1
in if aconv (concl th1) (concl th2)
then (name,ml_name,tm,th,pre,module) else let
val th2 = REWRITE_RULE [] th2
val th = remove_Eq_from_v_thm th2
val thm_name = name ^ "_v_thm"
val _ = print ("Updating " ^ thm_name ^ "\n")
val _ = save_thm(thm_name,th)
val new_pre = if can (find_term is_PRECONDITION) (concl (SPEC_ALL th))
then new_pre else TRUTH
val th = th |> UNDISCH_ALL
in (name,ml_name,tm,th,new_pre,module) end end
val _ = (v_thms := map update_aux (!v_thms))
in new_pre end
fun add_eval_thm th = let
val tm = concl (th |> SPEC_ALL |> UNDISCH_ALL)
val const = tm |> rand |> rand
val n = term_to_string const
val _ = (eval_thms := (n,const,th)::(!eval_thms))
in th end;
fun pack_v_thms () = let
val pack_vs = pack_list (pack_6tuple pack_string pack_string pack_term
pack_thm pack_thm (pack_option pack_string))
val pack_evals = pack_list (pack_triple pack_string pack_term pack_thm)
val cleaner = if !clean_on_exit then ml_progLib.clean_state else I
in pack_triple pack_vs pack_evals pack_ml_prog_state
(!v_thms,!eval_thms, cleaner (!prog_state)) end
fun unpack_v_thms th = let
val unpack_vs = unpack_list (unpack_6tuple unpack_string unpack_string unpack_term
unpack_thm unpack_thm (unpack_option unpack_string))
val unpack_evals = unpack_list (unpack_triple
unpack_string unpack_term unpack_thm)
val (x1,x2,x3) = unpack_triple unpack_vs unpack_evals unpack_ml_prog_state th
val _ = v_thms := x1
val _ = eval_thms := x2
val _ = prog_state := x3
in () end
fun get_names() = map (#2) (!v_thms)
end
fun full_id n =
case get_curr_module_name () of
(* Single-level module *)
SOME mn => astSyntax.mk_Long(stringSyntax.fromMLstring mn,astSyntax.mk_Short n)
| NONE => astSyntax.mk_Short n
(* code for managing type information *)
fun get_ty_case_const ty = let
val th = TypeBase.case_def_of ty
val case_const = th |> SPEC_ALL |> CONJUNCTS |> hd |> SPEC_ALL
|> concl |> dest_eq |> fst |> repeat rator
in case_const end
fun name_of_type ty = let
val case_const = get_ty_case_const ty
val name = case_const |> dest_const |> fst |> explode |> rev
|> funpow 5 tl |> rev |> implode
in name end;
val basic_theories =
["alist", "arithmetic", "bag", "bitstring", "bit", "bool",
"combin", "container", "divides", "fcp", "finite_map", "float",
"fmaptree", "frac", "gcdset", "gcd", "ind_type", "integer_word",
"integer", "integral", "list", "llist", "marker", "measure",
"numeral_bit", "numeral", "numpair", "numposrep", "num", "one",
"operator", "option", "pair", "path", "patricia_casts",
"patricia", "poly", "poset", "powser", "pred_set", "prelim",
"prim_rec", "quote", "quotient_list", "quotient_option",
"quotient_pair", "quotient_pred_set", "quotient_sum", "quotient",
"rat", "real_sigma", "realax", "real", "relation", "res_quan",
"rich_list", "ringNorm", "ring", "sat", "semi_ring", "seq",
"set_relation", "sorting", "state_option", "state_transformer",
"string_num", "string", "sum_num", "sum", "topology", "transc",
"update", "util_prob", "while", "words"]
val use_full_type_names = ref true;
fun full_name_of_type ty =
if !use_full_type_names then let
val case_const = get_ty_case_const ty
val thy_name = case_const |> dest_thy_const |> #Thy
val thy_name = if mem thy_name basic_theories then "" else thy_name ^ "_"
in thy_name ^ name_of_type ty end
else name_of_type ty;
(* ty must be a word type and dim ≤ 64 *)
fun word_ty_ok ty =
if wordsSyntax.is_word_type ty then
let val fcp_dim = wordsSyntax.dest_word_type ty in
if fcpSyntax.is_numeric_type fcp_dim then
let val dim = fcpSyntax.dest_int_numeric_type fcp_dim in
dim <= 64
end
else
false
end
else false;
val type_mappings = ref ([]:(hol_type * hol_type) list)
val other_types = ref ([]:(hol_type * term) list)
val preprocessor_rws = ref ([]:thm list)
val type_memory = ref ([]:(hol_type * thm * (term * thm) list * thm) list)
val deferred_dprogs = ref ([]:term list)
val all_eq_lemmas = ref (CONJUNCTS EqualityType_NUM_BOOL)
local
in
fun type_reset () =
(type_mappings := [];
other_types := [];
preprocessor_rws := [];
type_memory := [];
deferred_dprogs := [];
all_eq_lemmas := (CONJUNCTS EqualityType_NUM_BOOL))
fun dest_fun_type ty = let
val (name,args) = dest_type ty
in if name = "fun" then (el 1 args, el 2 args) else failwith("not fun type") end
fun find_type_mapping ty =
first (fn (t,_) => can (match_type t) ty) (!type_mappings)
fun free_typevars ty =
if can dest_vartype ty then [ty] else let
val (name,tt) = dest_type ty
in Lib.flatten (map free_typevars tt) end
handle HOL_ERR _ => []
fun add_new_type_mapping ty target_ty =
(type_mappings := (ty,target_ty) :: (!type_mappings))
fun string_tl s = s |> explode |> tl |> implode
fun type2t ty =
if ty = bool then Tapp [] (astSyntax.mk_TC_name(astSyntax.mk_Short(stringSyntax.fromMLstring"bool"))) else
if word_ty_ok ty then
(*dim ≤ 64 guaranteeed*)
let val dim = (fcpSyntax.dest_int_numeric_type o wordsSyntax.dest_word_type) ty in
if dim <= 8 then Tapp [] astSyntax.TC_word8
else Tapp [] astSyntax.TC_word64
end else
if ty = intSyntax.int_ty then Tapp [] astSyntax.TC_int else
if ty = numSyntax.num then Tapp [] astSyntax.TC_int else
if ty = stringSyntax.char_ty then Tapp [] astSyntax.TC_char else
if can dest_vartype ty then
astSyntax.mk_Tvar(stringSyntax.fromMLstring ((* string_tl *) (dest_vartype ty)))
else let
val (lhs,rhs) = find_type_mapping ty
val i = match_type lhs ty
val xs = free_typevars rhs
val i = filter (fn {redex = a, residue = _} => mem a xs) i
val tm = type2t rhs
val s = map (fn {redex = a, residue = b} => type2t a |-> type2t b) i
in subst s tm end handle HOL_ERR _ =>
let
val (x,tt) = dest_type ty
val name = if x = "fun" then "fun" else
if x = "prod" then "prod" else
full_name_of_type ty
val tt = map type2t tt
val name_tm = stringSyntax.fromMLstring name
in if name = "fun" then Tapp tt astSyntax.TC_fn else
if name = "prod" then Tapp tt astSyntax.TC_tup else
if name = "list" then Tapp tt (astSyntax.mk_TC_name(astSyntax.mk_Short(name_tm))) else
Tapp tt (astSyntax.mk_TC_name(full_id name_tm)) end
fun inst_type_inv (ty,inv) ty0 = let
val i = match_type ty ty0
val ii = map (fn {redex = x, residue = y} => (x,y)) i
val ss = map (fn (x,y) => (inst i (get_type_inv x) |-> get_type_inv y)) ii
in subst ss (inst i inv) end
and list_inst_type_inv ty0 [] = fail()
| list_inst_type_inv ty0 ((ty,inv)::xs) =
inst_type_inv (ty,inv) ty0 handle HOL_ERR _ =>
list_inst_type_inv ty0 xs
and get_type_inv ty =
if is_vartype ty then let
val name = dest_vartype ty |> explode |> tl |> implode
in mk_var(name,ty --> (v_ty --> bool)) end else
if can dest_fun_type ty then let
val (t1,t2) = dest_fun_type ty
in mk_Arrow(get_type_inv t1,get_type_inv t2)
end else
if ty = oneSyntax.one_ty then UNIT_TYPE else
if ty = bool then BOOL else
if wordsSyntax.is_word_type ty andalso word_ty_ok ty then
let val dim = wordsSyntax.dest_word_type ty in
inst [alpha|->dim] WORD
end else
if ty = numSyntax.num then NUM else
if ty = intSyntax.int_ty then ml_translatorSyntax.INT else
if ty = stringSyntax.char_ty then CHAR else
if ty = mlstringSyntax.mlstring_ty then STRING_TYPE else
if is_vector_type ty then let
val inv = get_type_inv (dest_vector_type ty)
in VECTOR_TYPE_def |> ISPEC inv |> SPEC_ALL
|> concl |> dest_eq |> fst |> rator |> rator end
else
list_inst_type_inv ty (!other_types)
handle HOL_ERR _ => raise UnsupportedType ty
fun new_type_inv ty inv = (other_types := (ty,inv) :: (!other_types))
fun add_type_inv tm target_ty = let
val ty = fst (dest_fun_type (type_of tm))
val _ = add_new_type_mapping ty target_ty
in new_type_inv ty tm end
fun add_deferred_dprog dprog =
if listSyntax.is_nil dprog then ()
else deferred_dprogs := dprog::(!deferred_dprogs)
fun pop_deferred_dprogs () =
List.rev (!deferred_dprogs) before deferred_dprogs := []
fun get_user_supplied_types () = map fst (!other_types)
fun add_eq_lemma eq_lemma =
if concl eq_lemma = T then () else
(all_eq_lemmas := eq_lemma :: (!all_eq_lemmas))
fun add_type_thms (rws1,rws2,res) = let
val _ = map (fn (ty,eq_lemma,inv_def,conses,case_lemma,ts) => add_eq_lemma eq_lemma) res
val _ = (type_memory := map (fn (ty,eq_lemma,inv_def,conses,case_lemma,ts) => (ty,inv_def,conses,case_lemma)) res @ (!type_memory))
val _ = (preprocessor_rws := rws2 @ (!preprocessor_rws))
in () end
fun lookup_type_thms ty = first (fn (ty1,_,_,_) => can (match_type ty1) ty) (!type_memory)
fun eq_lemmas () = (!all_eq_lemmas)
fun get_preprocessor_rws () = (!preprocessor_rws)
(* store/load to/from a single thm *)
fun pack_types () =
pack_6tuple
(pack_list (pack_pair pack_type pack_type))
(pack_list (pack_pair pack_type pack_term))
(pack_list pack_thm)
(pack_list (pack_4tuple pack_type pack_thm (pack_list (pack_pair pack_term pack_thm)) pack_thm))
(pack_list pack_term)
(pack_list pack_thm)
((!type_mappings), (!other_types), (!preprocessor_rws),
(!type_memory), (!deferred_dprogs), (!all_eq_lemmas))
fun unpack_types th = let
val (t1,t2,t3,t4,t5,t6) = unpack_6tuple
(unpack_list (unpack_pair unpack_type unpack_type))
(unpack_list (unpack_pair unpack_type unpack_term))
(unpack_list unpack_thm)
(unpack_list (unpack_4tuple unpack_type unpack_thm (unpack_list (unpack_pair unpack_term unpack_thm)) unpack_thm))
(unpack_list unpack_term)
(unpack_list unpack_thm) th
val _ = (type_mappings := t1)
val _ = (other_types := t2)
val _ = (preprocessor_rws := t3)
val _ = (type_memory := t4)
val _ = (deferred_dprogs := t5)
val _ = (all_eq_lemmas := t6)
in () end
end
(* misc *)
fun clean_lowercase s = let
fun f c = if #"a" <= c andalso c <= #"z" then implode [c] else
if #"A" <= c andalso c <= #"Z" then implode [chr (ord c + 32)] else
if #"0" <= c andalso c <= #"9" then implode [c] else
if c = #"," then "pair" else
if mem c [#"_",#"'"] then implode [c] else ""
in String.translate f s end;
fun clean_uppercase s = let
fun f c = if #"a" <= c andalso c <= #"z" then implode [chr (ord c - 32)] else
if #"A" <= c andalso c <= #"Z" then implode [c] else
if #"0" <= c andalso c <= #"9" then implode [c] else
if c = #"," then "PAIR" else
if mem c [#"_",#"'"] then implode [c] else ""
in String.translate f s end;
val sml_keywords_and_predefined = ["o", "+", "-", "*", "div", "mod",
"<", ">", "<=", ">=", "ref", "and", "andalso", "case", "datatype",
"else", "end", "eqtype", "exception", "fn", "fun", "handle", "if",
"in", "include", "let", "local", "of", "op", "open", "orelse",
"raise", "rec", "sharing", "sig", "signature", "struct",
"structure", "then", "type", "val", "where", "while", "with",
"withtype"]
fun get_unique_name str = let
val names = get_names() @ sml_keywords_and_predefined
fun find_name str n = let
val new_name = str ^ "_" ^ (int_to_string n)
in if mem new_name names then find_name str (n+1) else new_name end
fun find_new_name str =
if mem str names then find_name str 1 else str
val initial_name = clean_lowercase str
val initial_name = if size initial_name = 0 then "f" else initial_name
in find_new_name initial_name end
fun dest_args tm =
let val (x,y) = dest_comb tm in dest_args x @ [y] end
handle HOL_ERR _ => []
val quietDefine = (* quiet version of Define -- by Anthony Fox *)
Lib.with_flag (Feedback.emit_WARNING, false)
(Lib.with_flag (Feedback.emit_ERR, false)
(Lib.with_flag (Feedback.emit_MESG, false)
(Feedback.trace ("auto Defn.tgoal", 0) TotalDefn.Define)))
(* printing output e.g. SML syntax *)
val print_asts = ref false;
local
val base_filename = ref "";
val prelude_decl_count = ref 0;
datatype print_item = Translation of string * thm | InvDef of thm
val print_items = ref ([]:print_item list)
val prelude_name = ref (NONE: string option);
in
fun add_print_item i = (print_items := i :: (!print_items))
val files = ["_ml.txt","_hol.txt","_thm.txt","_ast.txt"]
fun check_suffix suffix = mem suffix files orelse failwith("bad file suffix")
fun clear_file suffix = if (!base_filename) = "" then () else let
val _ = check_suffix suffix
val t = TextIO.openOut((!base_filename) ^ suffix)
val _ = TextIO.closeOut(t)
in () end
fun get_filename () =
if not (!print_asts) then "" else
if !base_filename = "" then let
val name = current_theory()
val _ = (base_filename := name)
val _ = map clear_file files
in name end
else !base_filename
fun append_to_file suffix strs = if get_filename() = "" then () else let
val _ = check_suffix suffix
val t = TextIO.openAppend(get_filename() ^ suffix)
val _ = map (fn s => TextIO.output(t,s)) strs
val _ = TextIO.closeOut(t)
in () end
fun print_decls_aux xs suffix f =
map (fn tm => append_to_file suffix (f tm)) xs
fun drop n [] = [] | drop n xs = if n = 0 then xs else drop (n-1) (tl xs)
fun print_str str = str
fun print_prelude_comment suffix =
case !prelude_name of
NONE => ()
| SOME name => append_to_file suffix ["\n(* This code extends '"^name^"'. *)\n"]
fun print_decls () = ();
fun print_item _ = ()
fun print_decl_abbrev () = ()
fun print_prelude_name () = ()
fun print_reset () =
(base_filename := "";
prelude_decl_count := 0;
print_items := [];
prelude_name := NONE)
fun init_printer name = let
val _ = map clear_file files
val _ = (prelude_name := SOME name)
val _ = (prelude_decl_count := (length []))
in () end
fun print_translation_output () =
(print_prelude_name (); map print_item (rev (!print_items));
print_decl_abbrev (); print_decls ());
fun print_fname fname def = add_print_item (Translation (fname,def));
fun print_inv_def inv_def = add_print_item (InvDef inv_def);
end
(* code for loading and storing translations into a single thm *)
fun check_uptodate_term tm =
if Theory.uptodate_term tm then () else let
val t = find_term (fn tm => is_const tm
andalso not (Theory.uptodate_term tm)) tm
val _ = print "\n\nFound out-of-date term: "
val _ = print_term t
val _ = print "\n\n"
in () end
local
val suffix = "_translator_state_thm"
fun pack_state () = let
val name = Theory.current_theory () ^ suffix
val name_tm = stringSyntax.fromMLstring name
val tag_lemma = ISPEC (mk_var("b",bool)) (ISPEC name_tm TAG_def) |> GSYM
val p1 = pack_types()
val p2 = pack_v_thms()
val p = pack_pair I I (p1,p2)
val th = PURE_ONCE_REWRITE_RULE [tag_lemma] p
val _ = check_uptodate_term (concl th)
in save_thm(name,th) end
fun unpack_state name = let
val th = fetch name (name ^ suffix)
val th = PURE_ONCE_REWRITE_RULE [TAG_def] th
val (p1,p2) = unpack_pair I I th
val _ = unpack_types p1
val _ = unpack_v_thms p2
in () end;
val finalised = ref false
in
fun finalise_reset () = (finalised := false)
fun finalise_translation () =
if !finalised then () else let
val _ = (finalised := true)
val _ = pack_state ()
val _ = print_translation_output ()
in () end
val _ = Theory.register_hook(
"cakeML.ml_translator",
(fn TheoryDelta.ExportTheory _ => finalise_translation() | _ => ()))
fun translation_extends name = let
val _ = print ("Loading translation: " ^ name ^ " ... ")
val _ = unpack_state name
val _ = init_printer name
val _ = print ("done.\n")
in () end;
end
(* support for user-defined data-types *)
fun type_of_cases_const ty = let
val th = TypeBase.case_def_of ty
handle HOL_ERR e => raise ERR "type_of_cases_const" (String.concat["For ",Parse.type_to_string ty,"\n",Feedback.format_ERR e])
val ty = th |> SPEC_ALL |> CONJUNCTS |> hd |> SPEC_ALL
|> concl |> dest_eq |> fst |> repeat rator |> type_of
in ty end
fun remove_primes th = let
fun last s = substring(s,size s-1,1)
fun delete_last_prime s = if last s = "'" then substring(s,0,size(s)-1) else fail()
fun foo [] ys i = i
| foo (x::xs) ys i = let
val name = (fst o dest_var) x
val new_name = repeat delete_last_prime name
in if name = new_name then foo xs (x::ys) i else let
val new_var = mk_var(new_name,type_of x)
in foo xs (new_var::ys) ((x |-> new_var) :: i) end end
val i = foo (free_varsl (concl th :: hyp th)) [] []
in INST i th end
fun get_nchotomy_of ty = let (* ensures that good variables names are used *)
val case_th = TypeBase.nchotomy_of ty
val ty0 = type_of (hd (SPEC_ALL case_th |> concl |> free_vars))
val case_th = INST_TYPE (match_type ty0 ty) case_th
val xs = map rand (find_terms is_eq (concl case_th))
val x_var = mk_var("x",ty)
fun mk_lines [] = []
| mk_lines (x::xs) = let
val k = length xs + 1
fun rename [] = []
| rename (x::xs) = let val n = int_to_string k ^ "_" ^
int_to_string (length xs + 1)
in (x,mk_var("x" ^ n, type_of x),
mk_var("v" ^ n,v_ty)) end :: rename xs
val vars = rev (rename (free_vars x))
val new_x = subst (map (fn (x,y,z) => x |-> y) vars) x
val tm = list_mk_exists(rev (free_vars new_x), mk_eq(x_var,new_x))
in tm :: mk_lines xs end
val goal = mk_forall(x_var,list_mk_disj (rev (mk_lines xs)))
val lemma = prove(goal,
STRIP_TAC \\ STRIP_ASSUME_TAC (ISPEC x_var case_th)
\\ FULL_SIMP_TAC (srw_ss()) [])
in lemma end
fun find_mutrec_types ty = let (* e.g. input ``:v`` gives [``:exp``,``:v``] *)
fun is_pair_ty ty = fst (dest_type ty) = "prod"
fun is_list_ty ty = fst (dest_type ty) = "list"
fun is_option_ty ty = fst (dest_type ty) = "option"
fun all_distinct [] = []
| all_distinct (x::xs) = if mem x xs then all_distinct xs else x :: all_distinct xs
val xs = snd (TypeBase.size_of ty) |> CONJUNCTS
|> map (type_of o rand o fst o dest_eq o concl o SPEC_ALL)
|> filter (not o is_pair_ty) |> filter (not o is_list_ty)
|> filter (not o is_option_ty)
|> all_distinct
in if is_pair_ty ty then [ty] else if length xs = 0 then [ty] else xs end
(*
val type_name = name
val const_name = (repeat rator x |> dest_const |> fst)
*)
fun tag_name type_name const_name =
if (type_name = "OPTION_TYPE") andalso (const_name = "NONE") then "NONE" else
if (type_name = "OPTION_TYPE") andalso (const_name = "SOME") then "SOME" else
if (type_name = "LIST_TYPE") andalso (const_name = "NIL") then "nil" else
if (type_name = "LIST_TYPE") andalso (const_name = "CONS") then "::" else let
val x = clean_lowercase type_name
val y = clean_lowercase const_name
fun upper_case_hd s =
clean_uppercase (implode [hd (explode s)]) ^ implode (tl (explode s))
val name = if y = "" then upper_case_hd x else upper_case_hd y
val write_cons_pat =
write_cons_def |> SPEC_ALL |> concl |> dest_eq |> fst |> rator
val taken_names = EVAL (get_curr_env ())
|> concl |> rand |> find_terms (can (match_term write_cons_pat))
|> map (stringSyntax.fromHOLstring o rand o rator)
fun find_unique name n =
if not (mem name taken_names) then name else
if not (mem (name ^ "_" ^ int_to_string n) taken_names) then
name ^ "_" ^ int_to_string n
else find_unique name (n+1)
in find_unique name 1 end;
val last_def_fail = ref T
fun derive_record_specific_thms ty = let
val ty_name = name_of_type ty
val access_funs =
TypeBase.accessors_of ty
|> map (rator o fst o dest_eq o concl o SPEC_ALL)
val update_funs =
TypeBase.updates_of ty
|> map (rator o rator o fst o dest_eq o concl o SPEC_ALL)
val thy_name = access_funs |> hd |>dest_thy_const |> #Thy
val tm =
DB.fetch thy_name (ty_name ^ "_11")
|> SPEC_ALL |> concl |> dest_eq |> fst |> dest_eq |> fst
val xs = dest_args tm
val c = repeat rator tm
val case_tm =
DB.fetch thy_name (ty_name ^ "_case_cong")
|> SPEC_ALL |> UNDISCH_ALL |> concl |> dest_eq |> fst |> repeat rator
fun prove_accessor_eq (a,x) = let
val v = mk_var("v",type_of tm)
val f = foldr (fn (v,tm) => mk_abs(v,tm)) x xs
val ty1 = case_tm |> type_of |> dest_type |> snd |> el 2
|> dest_type |> snd |> hd
val i = match_type ty1 (type_of f)
val rhs = mk_comb(mk_comb(inst i case_tm,v),f)
val lhs = mk_comb(a,v)
val goal = mk_forall(v,mk_eq(lhs,rhs))
val lemma = prove(goal,Cases THEN SRW_TAC [] [])
in lemma end
val a_lemmas = map prove_accessor_eq (zip access_funs xs)
fun prove_updates_eq (a,x) = let
val v = mk_var("v",type_of tm)
val (t,ti) = type_of a |> dom_rng
val ti = dom_rng ti |> #2
val g = mk_var("g",t)
val s = match_type (type_of tm) ti
val tmi = Term.inst s tm
val xi = Term.inst s x
val f = foldr mk_abs (subst [xi|->mk_comb(g,x)] tmi) xs
val ty1 = case_tm |> type_of |> dest_type |> snd |> el 2
|> dest_type |> snd |> hd
val i = match_type ty1 (type_of f)
val rhs = mk_comb(mk_comb(inst i case_tm,v),f)
val lhs = mk_comb(mk_comb(a,g),v)
val goal = mk_forall(v,mk_forall(g,mk_eq(lhs,rhs)))
val tac = Cases THEN SRW_TAC [] [DB.fetch thy_name (ty_name ^ "_fn_updates")]
in prove(goal,tac) end
val b_lemmas = map prove_updates_eq (zip update_funs xs)
val rtype = type_of tm
val {Args,Thy,Tyop} = dest_thy_type rtype
fun new_rtype() = let
val Args = List.tabulate (length Args,fn _ => gen_tyvar())
in mk_thy_type{Args=Args,Thy=Thy,Tyop=Tyop} end
fun foldthis ((fupd,var),(rtype,y)) =
let
val (fty,updty) = fupd |> type_of |> dom_rng
val (r1,r2) = dom_rng updty
val s = match_type updty (rtype --> new_rtype())
handle HOL_ERR _ => match_type updty (rtype --> rtype)
val ifupd = inst s fupd
val (g1,g2) = dom_rng (type_subst s fty)
val (x,_) = dest_var var
val x = mk_var(x,g2)
val k = combinSyntax.mk_K_1 (x,g1)
in (type_subst s r2,mk_comb(mk_comb(ifupd,k),y)) end
val arb = mk_arb (new_rtype())
val (_,tm2) = foldr foldthis (type_of arb,arb) (zip update_funs xs)
val s = match_type (type_of tm2) rtype
val tm2 = inst s tm2
val goal = mk_eq(tm2,tm)
val rw_lemma = prove(goal,SRW_TAC []
[DB.fetch thy_name (ty_name ^ "_component_equality")])
val rw_lemmas =
if length(TypeBase.fields_of ty) > 1
then CONJ (DB.fetch thy_name (ty_name ^ "_fupdcanon")) rw_lemma
else rw_lemma
in (a_lemmas @ b_lemmas, [rw_lemmas]) end;
fun rename_bound_vars_rule prefix th = let
val i = ref 0
fun next_name () = (i:= !i+1; prefix ^ int_to_string (!i))
fun next_var v = mk_var(next_name (), type_of v)
fun next_alpha_conv tm = let
val (v,_) = dest_abs tm
val _ = not (String.isPrefix prefix (fst (dest_var v))) orelse fail()
in ALPHA_CONV (next_var v) tm end handle HOL_ERR _ => NO_CONV tm
in CONV_RULE (DEPTH_CONV next_alpha_conv) th end;
fun list_dest f tm =
let val (x,y) = f tm in list_dest f x @ list_dest f y end
handle HOL_ERR _ => [tm];
(*
val ty = ``:'a # 'b``
val tys = find_mutrec_types ty
val is_exn_type = false
*)
fun define_ref_inv is_exn_type tys = let
val is_pair_type =
(case tys of [ty] => can pairSyntax.dest_prod ty | _ => false)
val is_list_type =
(case tys of [ty] => listSyntax.is_list_type ty | _ => false)
val is_option_type =
(case tys of [ty] => optionSyntax.is_option ty | _ => false)
fun get_name ty = clean_uppercase (full_name_of_type ty) ^ "_TYPE"
val names = map get_name tys
val name = hd names
fun list_mk_type [] ret_ty = ret_ty
| list_mk_type (x::xs) ret_ty = mk_type("fun",[type_of x,list_mk_type xs ret_ty])
val cases_thms = map (SPEC_ALL o get_nchotomy_of) tys |> LIST_CONJ
|> rename_bound_vars_rule "x_" |> CONJUNCTS
val all = zip names (zip tys cases_thms) |> map (fn (x,(y,z)) => (x,y,z))
val tmp_v_var = genvar v_ty
val real_v_var = mk_var("v",v_ty)
fun mk_lhs (name,ty,case_th) = let
val xs = map rand (find_terms is_eq (concl case_th))
val ty = type_of (hd (SPEC_ALL case_th |> concl |> free_vars))
val vars = type_vars ty
val ss = map get_type_inv vars
val input = mk_var("input",ty)
val ml_ty_name = full_name_of_type ty
val def_name = mk_var(name,list_mk_type (ss @ [input]) (v_ty --> bool))
val lhs = foldl (fn (x,y) => mk_comb(y,x)) def_name (ss @ [input,tmp_v_var])
in (ml_ty_name,xs,ty,lhs,input) end
val ys = map mk_lhs all
fun reg_type (_,_,ty,lhs,_) = new_type_inv ty (rator (rator lhs));
val _ = map reg_type ys
val rw_lemmas = LIST_CONJ [LIST_TYPE_SIMP,PAIR_TYPE_SIMP,OPTION_TYPE_SIMP]
val def_tm = let
fun mk_lines ml_ty_name lhs ty [] input = []
| mk_lines ml_ty_name lhs ty (x::xs) input = let
val k = length xs + 1
val tag = tag_name name (repeat rator x |> dest_const |> fst)
fun rename [] = []
| rename (x::xs) = let val n = int_to_string k ^ "_" ^
int_to_string (length xs + 1)
in (x,mk_var("v" ^ n,v_ty)) end :: rename xs
val vars = rev (rename (free_vars x))
val ty_list = mk_type("list",[ty])
val list_ty = (ty --> v_ty --> bool) --> listSyntax.mk_list_type(ty) --> v_ty --> bool
fun find_inv tm =
(mk_comb(get_type_inv (type_of tm),tm))
val ys = map (fn (y,z) => mk_comb(find_inv y,z)) vars
val tm = if ys = [] then T else list_mk_conj ys
val str = stringLib.fromMLstring tag
val str_ty_name = stringLib.fromMLstring
(if is_exn_type then tag else ml_ty_name)
val vs = listSyntax.mk_list(map (fn (_,z) => z) vars,v_ty)
val tyi = if is_exn_type then mk_TypeExn else mk_TypeId
val tag_tm = if is_pair_type then
optionSyntax.mk_none(pairSyntax.mk_prod(
stringSyntax.string_ty, tid_or_exn_ty))
else if is_list_type orelse is_option_type then
optionSyntax.mk_some(pairSyntax.mk_pair(str,
mk_TypeId((astSyntax.mk_Short str_ty_name) )))
else optionSyntax.mk_some(pairSyntax.mk_pair(str, tyi(full_id str_ty_name)))
val tm = mk_conj(mk_eq(tmp_v_var,
mk_Conv(tag_tm, vs)),tm)
val tm = list_mk_exists (map (fn (_,z) => z) vars, tm)
val tm = subst [input |-> x] (mk_eq(lhs,tm))
(* val vs = filter (fn x => x <> def_name) (free_vars tm) *)
val ws = free_vars x
in tm :: mk_lines ml_ty_name lhs ty xs input end
(*
val (ml_ty_name,x::xs,ty,lhs,input) = hd ys
*)
val zs = Lib.flatten (map (fn (ml_ty_name,xs,ty,lhs,input) =>
mk_lines ml_ty_name lhs ty xs input) ys)
val def_tm = list_mk_conj zs
val def_tm = QCONV (REWRITE_CONV [rw_lemmas]) def_tm |> concl |> rand
in def_tm end
val size_def = snd (TypeBase.size_of (hd tys))
fun right_list_dest f tm =
let val (x,y) = f tm
in (right_list_dest f y) @ [x] end handle HOL_ERR _ => [tm]
fun build_measure [] = fail()
| build_measure [ty] = let
val x = fst (TypeBase.size_of ty)
(* Check the number of fcp vars -- not sure if this works for more than one *)
val count_fcp = (length o (filter fcpSyntax.is_numeric_type) o snd o dest_type) ty
val xs = tl (tl (right_list_dest dest_fun_type (type_of x)))
val s = (x |> dest_const |> fst)
val s1 = foldr (fn (_,s) => s ^ " (K 0)") s xs
val s2 = foldr (fn (_,s) => s ^ " o SND") " o FST" (List.drop (xs,count_fcp))
in s1 ^ s2 end
| build_measure (t1::t2::ts) = let
val s1 = build_measure [t1]
val s2 = build_measure (t2::ts)
in "sum_case ("^s1^") ("^s2^")" end
val MEM_pat = MEM |> CONJUNCT2 |> SPEC_ALL |> concl |> rand |> rand
val tac =
(WF_REL_TAC [QUOTE ("measure (" ^ build_measure tys ^ ")")]
\\ REPEAT STRIP_TAC
(*TODO: \\ IMP_RES_TAC v_size_lemmas*)
\\ TRY DECIDE_TAC
\\ TRY (PAT_X_ASSUM MEM_pat (fn th =>
ASSUME_TAC th THEN Induct_on [ANTIQUOTE (rand (rand (concl th)))]))
\\ FULL_SIMP_TAC std_ss [MEM,FORALL_PROD,size_def] \\ REPEAT STRIP_TAC
\\ FULL_SIMP_TAC std_ss [] \\ RES_TAC \\ DECIDE_TAC)
(*
Define [ANTIQUOTE def_tm]
*)
val inv_def = if is_list_type then LIST_TYPE_def else
if is_pair_type then PAIR_TYPE_def else
if is_option_type then OPTION_TYPE_def else
tDefine name [ANTIQUOTE def_tm] tac
val clean_rule = CONV_RULE (DEPTH_CONV (fn tm =>
if not (is_abs tm) then NO_CONV tm else
if fst (dest_abs tm) = tmp_v_var then ALPHA_CONV real_v_var tm
else NO_CONV tm))
val inv_def = inv_def |> clean_rule
val inv_def = CONV_RULE (DEPTH_CONV ETA_CONV) inv_def
val inv_def = REWRITE_RULE [GSYM rw_lemmas] inv_def
val _ = if is_list_type then inv_def else
if is_pair_type then inv_def else
if is_option_type then inv_def else
save_thm(name ^ "_def",inv_def)
val ind = fetch "-" (name ^ "_ind") |> clean_rule
handle HOL_ERR _ => TypeBase.induction_of (hd tys) |> clean_rule
(*
val inv_def = tDefine name [ANTIQUOTE def_tm] ALL_TAC
*)
fun has_arg_with_type ty line =
((line |> SPEC_ALL |> concl |> dest_eq |> fst |> rator |> rand |> type_of) = ty)
val inv_defs = map (fn ty => (ty,LIST_CONJ (filter (has_arg_with_type ty)
(CONJUNCTS inv_def)))) tys
(* register the new type invariants *)
fun sub lhs th = subst [(lhs |> repeat rator) |->
(th |> SPEC_ALL |> CONJUNCTS |> hd |> SPEC_ALL
|> concl |> dest_eq |> fst |> repeat rator)] lhs
val ys2 = map (fn ((_,th),(ml_ty_name,xs,ty,lhs,input)) =>
(ml_ty_name,xs,ty,sub lhs th,input)) (zip inv_defs ys)
val _ = map reg_type ys2
(* equality type -- TODO: make this work for mutrec *)
val eq_lemmas = let
val tm = inv_def |> SPEC_ALL |> CONJUNCTS |> hd |> SPEC_ALL
|> concl |> dest_eq |> fst |> rator |> rator
val xs =
inv_def |> RW [GSYM CONJ_ASSOC] |> SPEC_ALL |> CONJUNCTS
|> map (snd o dest_eq o concl o SPEC_ALL)
|> map (last o list_dest dest_exists)
|> map (tl o list_dest dest_conj) |> Lib.flatten
|> map (rator o rator) |> filter (fn t => t <> tm)
val ys = map mk_EqualityType xs
(* val ys = map (fst o dest_imp o concl o D o SIMP_EqualityType_ASSUMS o ASSUME) ys *)
val tm1 = mk_EqualityType tm
val ys = filter (fn y => not (mem y [tm1,T])) ys
val tm2 = if ys = [] then T else list_mk_conj ys
val goal = mk_imp(tm2,tm1)
val pat1 = get_term "auto eq proof 1"
val pat2 = get_term "auto eq proof 2"
val x2 = mk_var("x2",tm1 |> rand |> type_of |> dest_type |> snd |> hd)
val eq_lemma = auto_prove "EqualityType" (goal,
REPEAT STRIP_TAC
\\ FULL_SIMP_TAC std_ss [EqualityType_def]
\\ STRIP_TAC THEN1
(REPEAT (PAT_X_ASSUM pat1 (K ALL_TAC))
\\ (Induct ORELSE Cases)
\\ SIMP_TAC (srw_ss()) [inv_def,no_closures_def,PULL_EXISTS]
\\ REPEAT STRIP_TAC \\ RES_TAC)
\\ STRIP_TAC
THEN1
(REPEAT (PAT_X_ASSUM pat2 (K ALL_TAC))
\\ (Induct ORELSE Cases)
\\ SIMP_TAC (srw_ss()) [inv_def,no_closures_def,PULL_EXISTS]
\\ primCases_on x2
\\ SIMP_TAC (srw_ss()) [inv_def,no_closures_def,PULL_EXISTS]