forked from CakeML/cakeml
-
Notifications
You must be signed in to change notification settings - Fork 0
/
ml_translatorLib.sml
4912 lines (4619 loc) · 198 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
(*
The HOL to CakeML translator itself.
The main entry point is the translate function.
*)
structure ml_translatorLib :> ml_translatorLib =
struct
open HolKernel boolLib bossLib BasicProvers;
open astTheory libTheory semanticPrimitivesTheory namespaceTheory;
open evaluateTheory stringLib astSyntax semanticPrimitivesSyntax;
open ml_translatorTheory ml_translatorSyntax intLib;
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 permLib comparisonTheory in end
val ERR = mk_HOL_ERR "ml_translatorLib";
val RW = REWRITE_RULE;
val RW1 = ONCE_REWRITE_RULE;
fun allowing_rebind f = Feedback.trace ("Theory.allow_rebinds", 1) f
local
structure Parse = struct
open Parse
val (Type,Term) =
parse_from_grammars ml_translatorTheory.ml_translator_grammars
end
open Parse
val prim_exn_list = let
val tm = primSemEnvTheory.prim_sem_env_eq |> concl |> rand |> rand |> rand
val (xs,ty) = ``^tm.c`` |> SIMP_CONV (srw_ss()) []
|> concl |> rand |> rator |> rand |> listSyntax.dest_list
val ys = filter (semanticPrimitivesSyntax.is_ExnStamp o rand o rand) xs
in listSyntax.mk_list(ys, ty) end
val term_alist =
[("find_recfun",``find_recfun name funs : ('a # 'b) option``),
("eq type",``EqualityType (a:'a->v->bool)``),
("lookup_cons",``lookup_cons s e = SOME x``),
("nsLookup",``nsLookup (e:('a,'b,v) namespace) s = SOME (x:v)``),
(*TODO: Should this be e or e.v?*)
("eq remove",``!b x. Eq b x = (b:'a->v->bool)``),
("map pat",``MAP (f:'a->'b)``),
("filter pat",``FILTER (f:'a->bool)``),
("every pat",``EVERY (f:'a->bool)``),
("exists pat",``EXISTS (f:'a->bool)``),
("n = 0",``(n = (0:num))``),
("0 = n",``(0 = (n:num))``),
("bind",``(Con(SOME(Short"Bind")) [])``),
("eq arrow",“ml_translator$Arrow (Eq (a:'a->v->bool) x) (b:'b->v->bool)”),
("arrow eq",``Arrow (Eq a (x:'a)) (b:'b->v->bool)``),
("precond = T",``!b. PRECONDITION b = T``),
("WF",``WF:('a -> 'a -> bool) -> bool``),
("COND",``COND:bool -> 'a -> 'a -> 'a``),
("not eq",``~(x = y:'a)``),
("lookup_cons eq",``lookup_cons n env = x``),
("Eval Var",``Eval env (Var n) (a (y:'a))``),
("PMATCH_ROW",``(PMATCH_ROW f1 f2):('a -> 'c) -> 'b -> 'c option``),
("PMATCH_ROW_T",``(PMATCH_ROW (f1:'a->'b) (K T) f3):'b -> 'c option``),
("PMATCH",``PMATCH x (l :('a -> 'b option) list)``),
("evaluate_pat",``evaluate (_ : α semanticPrimitives$state) _ _``),
("PreImp_Eval",``PreImp _ (Eval _ _ _)``),
("nsLookup_pat",``nsLookup (env:(α,β,γ) namespace) name``),
("pmatch_eq_Match_type_error",``pmatch _ _ _ _ _ = Match_type_error``),
("auto eq proof 1",``!x1:α x2:β x3:γ x4:δ. bbb``),
("auto eq proof 2",``!x1:α x2:β. bbb ==> bbbb``),
("remove lookup_cons",``!x1 x2 x3. (lookup_cons x1 x2 = SOME x3) = T``),
("no_closure_pat",``!(x:α) v. p x v ==> no_closures v``),
("types_match_pat",``!x1:α v1 x2:α v2. p x1 v1 /\ p x2 v2 ==> types_match v1 v2``),
("prim_exn_list",prim_exn_list),
("list-type-char",``LIST_TYPE CHAR``),
("OPTION_TYPE_SIMP",``!OPTION_TYPE x. CONTAINER OPTION_TYPE
(\y v. if x = SOME y then p y v else ARB) x =
(OPTION_TYPE (p:('a -> v -> bool)) x):v->bool``)]
in
val get_term = fn s => assoc s term_alist
end (* local *)
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;
(* non-persistent state *)
local
val use_string_type_ref = ref false;
val finalise_function = ref (I:unit -> unit);
in
fun use_string_type b =
(use_string_type_ref := b;
if b then print "Translator now treats `char list` as a CakeML string.\n"
else print "Translator now treats `char list` as a list of characters in CakeML.\n");
fun use_hol_string_type () = !use_string_type_ref
fun add_finalise_function f = let
val old_f = !finalise_function
in (finalise_function := (fn () => (old_f (); f ()))) end
fun run_finalise_function () = (!finalise_function) ()
end
(* / non-persistent state *)
(* code for managing state of certificate theorems *)
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 reraise fname message r = raise (ERR fname (message ^ ": " ^ #message r))
fun auto_prove_asms name ((asms,goal),tac) = let
val (rest,validation) = tac (asms,goal)
handle HOL_ERR r => reraise "auto_prove_asms" "tactic failure" r
in if length rest = 0 then validation [] else let
in failwith ("auto_prove_asms failed for " ^ name) end end
fun auto_prove proof_name (goal,tac:tactic) = let
val (rest,validation) = tac ([],goal)
handle HOL_ERR r => reraise "auto_prove" "tactic failure" r
| Empty => raise (ERR "auto_prove" "tactic raised Empty")
in if length rest = 0 then validation [] else let
in failwith("auto_prove failed for " ^ proof_name) end end
val unknown_loc = prim_mk_const {Name = "unknown_loc" , Thy = "location"}
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
(unknown_loc,
mk_var("x",#1(dom_rng(#2(dom_rng(type_of astSyntax.Dtype_tm))))));
val Dletrec_funs = astSyntax.mk_Dletrec
(unknown_loc,
mk_var("funs",#1(dom_rng(#2(dom_rng(type_of astSyntax.Dletrec_tm))))));
val Dexn_n_l =
let val args = tl(#1(boolSyntax.strip_fun(type_of astSyntax.Dexn_tm))) in
astSyntax.mk_Dexn (unknown_loc,mk_var("n",el 1 args), mk_var("l",el 2 args))
end
val Dlet_v_x =
let val args = tl(#1(boolSyntax.strip_fun(type_of astSyntax.Dlet_tm))) in
astSyntax.mk_Dlet (unknown_loc,mk_var("v",el 1 args), mk_var("x",el 2 args))
end
fun Dtype ls = astSyntax.mk_Dtype
(unknown_loc,
listSyntax.mk_list(ls,listSyntax.dest_list_type
(#1(dom_rng(#2(dom_rng(type_of astSyntax.Dtype_tm)))))))
fun Dtabbrev name ty = astSyntax.mk_Dtabbrev
(unknown_loc,listSyntax.mk_nil string_ty, name, ty)
fun Atapp ls x = astSyntax.mk_Atapp(listSyntax.mk_list(ls,astSyntax.ast_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=TypeBasePure.mk_recordtype_fieldsel {fieldname="refs",tyname="state"},Thy="semanticPrimitives"}
fun mk_tid name =
optionSyntax.mk_some
(astSyntax.mk_Short
(stringSyntax.fromMLstring name))
val true_tid = mk_tid "true"
val false_tid = mk_tid "false"
val true_exp_tm = (Eval_Val_BOOL_TRUE |> concl |> rator |> rand)
val false_exp_tm = (Eval_Val_BOOL_FALSE |> concl |> rator |> rand)
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;
(* make the qualified identifier for some item, where "base" is its base name
(parameter of Short) in its local scope, mods is the module scope it was
defined in, and curr_mods is the current module scope. *)
fun mk_qualified_relative_name curr_mods mods base = let
val base_nm = astSyntax.mk_Short base
fun drop_same (x :: xs) (y :: ys) = if x = y then drop_same xs ys
else (x :: xs)
| drop_same xs _ = xs
val rel_mods = drop_same mods curr_mods
val mks = stringSyntax.fromMLstring
fun mk_name [] b = b
| mk_name (m :: ms) b = astSyntax.mk_Long (mks m, mk_name ms b)
in mk_name rel_mods base_nm end
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 list (* module scope *)) 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;
val cons_name_state = ref ([] : (string * (* %%thy%%type%%ctor *)
(term * (* constructor name *)
string list) (* module scope *)) list);
val type_mod_state = ref ([] : (string * (* type name *)
string list (* module scope *)) list);
in
fun get_ml_name (_:string,nm:string,_:term,_:thm,_:thm,_:string list) = nm
fun get_const (_:string,_:string,tm:term,_:thm,_:thm,_:string list) = tm
fun get_cert (_:string,_:string,_:term,th:thm,_:thm,_:string list) = th
fun get_pre (_:string,_:string,_:term,_:thm,th:thm,_:string list) = 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_modules () = get_open_modules (!prog_state);
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 modules = get_curr_modules ()
val _ = if Teq (concl pre_def) then () else
(print ("\nWARNING: " ^ml_name^" has a precondition.\n\n"))
in (v_thms := (name,ml_name,tm,th,pre_def,modules) :: (!v_thms)) end;
fun filter_v_thms f = let
val xs = (!v_thms)
val ys = filter f xs
val _ = (v_thms := ys)
in length xs - length ys 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,_,_) =>
aconv (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 get_qualified_name mods base = mk_qualified_relative_name
(get_curr_modules ()) mods base
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 iden = get_qualified_name m (stringSyntax.fromMLstring ml_name)
val th = MATCH_MP Eval_Var_general th
|> SPEC iden |> 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 update_precondition new_pre = let
fun update_aux (name,ml_name,tm,th,pre,module) = let
val th1 = D th
val (new_pre,th1) =
(if is_imp (concl (SPEC_ALL new_pre))
then (* case: new_pre is an induction theorem *)
(((MATCH_MP IMP_EQ_T (MP (D new_pre) TRUTH)
handle HOL_ERR _ => new_pre)
|> PURE_REWRITE_RULE [GSYM CONJ_ASSOC]),
PURE_REWRITE_RULE [GSYM CONJ_ASSOC] th1)
else (new_pre,th1))
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 _ = allowing_rebind 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 check_no_ind_assum tm th = let
val hs = th |> DISCH_ALL |> REWRITE_RULE [GSYM AND_IMP_INTRO]
|> UNDISCH_ALL |> hyp
in if can (first is_forall) hs then let
val str = "User must prove skipped induction theorem for " ^
term_to_string tm
in print ("\nERROR: " ^ str ^ "\n\n") ; failwith str end
else ()
end
fun pack_v_thms () = let
fun check_no_ind_assum_in_v (_,_,tm,th,_,_) = check_no_ind_assum tm th
val _ = map check_no_ind_assum_in_v (!v_thms)
val pack_vs = pack_list (pack_6tuple pack_string pack_string pack_term
pack_thm pack_thm (pack_list 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_list 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 pack_cons_names () =
let
val pack_ns =
pack_pair pack_string (pack_pair pack_term (pack_list pack_string))
in
pack_list pack_ns (!cons_name_state)
end
fun pack_type_mods () =
let
val pack_ns = pack_pair pack_string (pack_list pack_string)
in
pack_list pack_ns (!type_mod_state)
end
fun unpack_type_mods th =
let
val unpack_ns = unpack_pair unpack_string (unpack_list unpack_string)
val tyms = unpack_list unpack_ns th
in
type_mod_state := tyms
end
fun unpack_cons_names th =
let
val unpack_ns =
unpack_pair unpack_string
(unpack_pair unpack_term (unpack_list unpack_string))
val tyns = unpack_list unpack_ns th
in
cons_name_state := tyns
end
fun get_names() = map (#2) (!v_thms)
fun get_v_thms_ref() = v_thms (* for the monadic translator *)
fun get_type_mods () = !type_mod_state
fun type_mods_reset () = type_mod_state := []
fun lookup_type_mod tyname =
SOME (Lib.assoc tyname (!type_mod_state))
handle HOL_ERR _ => NONE
(* TODO not sure we'll ever encounter duplicate type names - they should
* be entered with their full name. *)
fun enter_type_mod tyname =
let
val mods = get_curr_modules ()
val _ = lookup_type_mod tyname = NONE orelse
failwith ("duplicate type: " ^ tyname)
in
case mods of
[] => ()
| _ => type_mod_state := (tyname,mods)::(!type_mod_state)
end
fun get_cons_names () = !cons_name_state
fun cons_names_reset () = cons_name_state := []
fun mk_cons_name tm =
let
val (_, ty) = strip_fun (type_of tm)
val info = Option.valOf (TypeBase.fetch ty)
val (thyn, tyn) = TypeBasePure.ty_name_of info
val name = term_to_string tm
in
(* separating with underscores is more prone to name clashes *)
String.concat ["%%", thyn, "%%", tyn, "%%", name, "%%"]
end
fun lookup_cons_name key = Lib.assoc key (!cons_name_state)
fun enter_cons_name (tm, v_tm) =
let
val key = mk_cons_name tm
val mods = get_curr_modules ()
val (v_tm', mods') = lookup_cons_name key
handle HOL_ERR _ => (v_tm, mods)
in
if aconv v_tm' v_tm andalso mods = mods' then
key before cons_name_state := (key, (v_tm, mods)) :: (!cons_name_state)
else
raise ERR "enter_cons_name"
("already entered with different value: " ^ term_to_string v_tm)
end
end
(*
* Returns the 'full' identifier for the type. What this is depends on where the
* type was registered. For types that are not in scope (i.e. outside of the
* current module) we give a Long name, otherwise the name is short.
*)
fun full_id n =
case lookup_type_mod (stringSyntax.fromHOLstring n) of
NONE => astSyntax.mk_Short n
| SOME type_mod => get_qualified_name type_mod 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", "machine_ieee",
"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 mlstring_ty = mlstringTheory.implode_def |> concl |> rand
|> type_of |> dest_type |> snd |> last;
local
val prim_exn_list = get_term "prim_exn_list"
val xs = listSyntax.dest_list prim_exn_list |> fst
val ys = map dest_pair xs |>
map (fn (x,y) => (stringSyntax.fromHOLstring x,
numSyntax.int_of_term (y |> rator |> rand), y))
in
fun get_primitive_exception name = let
val (_,arity,value) = first (fn (n,_,_) => n = name) ys
in (arity,value) end
fun is_primitive_exception name = can get_primitive_exception name
end;
val default_eq_lemmas = CONJUNCTS EqualityType_NUM_BOOL
@ CONJUNCTS IsTypeRep_NUM_BOOL
@ [IsTypeRep_PAIR, IsTypeRep_LIST, IsTypeRep_VECTOR]
local
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 default_eq_lemmas
in
fun type_reset () =
(type_mappings := [];
other_types := [];
preprocessor_rws := [];
type_memory := [];
deferred_dprogs := [];
all_eq_lemmas := default_eq_lemmas)
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 prim_type name = Atapp [] (astSyntax.mk_Short(stringSyntax.fromMLstring name))
val bool_ast_t = prim_type "bool"
val int_ast_t = prim_type "int"
val char_ast_t = prim_type "char"
val word8_ast_t = prim_type "word8"
val word64_ast_t = prim_type "word64"
val string_ast_t = prim_type "string"
val one_ast_t = mk_Attup(listSyntax.mk_list([],ast_t_ty))
fun type2t ty =
if ty = bool then bool_ast_t 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 word8_ast_t else word64_ast_t
end else
if ty = intSyntax.int_ty then int_ast_t else
if ty = numSyntax.num then int_ast_t else
if ty = stringSyntax.char_ty then char_ast_t else
if ty = oneSyntax.one_ty then one_ast_t else
if ty = stringSyntax.string_ty andalso use_hol_string_type() then string_ast_t else
if ty = mlstring_ty then string_ast_t else
if can dest_vartype ty then
astSyntax.mk_Atvar(stringSyntax.fromMLstring (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 mk_Atfun(el 1 tt, el 2 tt) else
if name = "prod" then mk_Attup(listSyntax.mk_list(tt,astSyntax.ast_t_ty)) else
if name = "list" then Atapp tt (astSyntax.mk_Short(name_tm))
else Atapp tt (full_id name_tm) end
val HOL_STRING_TYPE =
HOL_STRING_TYPE_def |> SPEC_ALL |> concl |> dest_eq |> fst |> repeat rator
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 = 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 = stringSyntax.string_ty andalso use_hol_string_type() then HOL_STRING_TYPE 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 Teq (concl eq_lemma) then () else
(all_eq_lemmas := eq_lemma :: (!all_eq_lemmas))
fun add_type_thms (rws1,rws2,res,tr_lemmas) = let
val _ = map (fn (ty,eq_lemma,inv_def,conses,case_lemma,ts) => add_eq_lemma eq_lemma) res
val _ = map add_eq_lemma tr_lemmas
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 ignore_type ty = (type_memory := (ty,TRUTH,[],TRUTH) :: (!type_memory));
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 _ => []
fun allowing_rebind f = Feedback.trace ("Theory.allow_rebinds", 1) f
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) $
allowing_rebind $
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
(* timing output *)
val trace_timing_to = ref (NONE : string option)
fun timing_message msg = case ! trace_timing_to of
SOME fname => let
val f = TextIO.openAppend fname
in TextIO.output (f, " ++ " ^ msg ^ "\n");
TextIO.closeOut f
end | NONE => ()
fun start_timing nm = case ! trace_timing_to of
SOME fname => let
val time = Portable.timestamp ()
val f = TextIO.openAppend fname
val time_s = Portable.time_to_string time
in TextIO.output (f, time_s ^ ": began " ^ nm ^ "\n");
TextIO.closeOut f;
SOME (fname, nm, time)
end | NONE => NONE
fun end_timing t = case t of
SOME (fname, nm, start_time) => let
val time = Portable.timestamp ()
val f = TextIO.openAppend fname
val time_s = Portable.time_to_string time
val dur_s = Portable.time_to_string (time - start_time)
in TextIO.output (f, time_s ^ ": finished " ^ nm ^ "\n");
TextIO.output (f, " -- duration of " ^ nm ^ ": " ^ dur_s ^ "\n");
TextIO.closeOut f
end | NONE => ()
fun do_timing nm f x = let
val start = start_timing nm
val r = f x
in end_timing start; r end
(* code for loading and storing translations into a single thm *)
fun check_uptodate_term t =
if ThyDataSexp.uptodate t 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 () *)
raise mk_HOL_ERR "ml_translatorLib" "pack_state" "Out of date junk"
local
val {export,segment_data,set} = ThyDataSexp.new {
thydataty = "foo",
merge = fn {old, new} => new,
load = fn _ => (), other_tds = fn (t,_) => SOME t}
fun pack_state () = let
val p1 = pack_types()
val p2 = pack_v_thms()
val p3 = pack_cons_names()
val p4 = pack_type_mods()
val p = pack_4tuple I I I I (p1,p2,p3,p4)
val _ = check_uptodate_term p
in export p end
fun unpack_state data = let
val (p1,p2,p3,p4) = unpack_4tuple I I I I data
val _ = unpack_types p1
val _ = unpack_v_thms p2
val _ = unpack_cons_names p3
val _ = unpack_type_mods p4
in () end;
val finalised = ref false
in
fun finalise_reset () = (finalised := false)
fun finalise_translation () =
if !finalised then () else let
val _ = (finalised := true)
val _ = run_finalise_function ()
val _ = pack_state ()
val _ = print_translation_output ()
in () end
fun translation_extends name = let
val _ = print ("Loading translation: " ^ name ^ " ... ")
val _ =
case segment_data {thyname=name} of
NONE => raise mk_HOL_ERR "ml_translatorLib" "translation_extends"
("No translator data in theory " ^ name)
| SOME data => unpack_state data
val _ = init_printer name
val _ = print ("done.\n")
in () end;
val _ = Theory.register_hook(
"CakeML.ml_translator",
(fn TheoryDelta.ExportTheory _ => finalise_translation() | _ => ()))
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 = auto_prove "get_nchotomy_of" (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"
val xs = TypeBase.axiom_of ty |> SPEC_ALL |> concl |> strip_exists |> #1 |> map (#1 o dest_fun_type o type_of) |> (fn ls => filter (fn ty => intersect ((#2 o dest_type) ty) ls = []) ls)
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)
*)
(*
input: ``lookup_cons specific_name env_const = NONE``
output: |- lookup_cons specific_name env_const = NONE <=> T
or: |- lookup_cons specific_name env_const = NONE <=> F
input: ``lookup_cons specific_name env_const = SOME stamp``
output: |- lookup_cons specific_name env_const = SOME stamp <=> T
or: |- lookup_cons specific_name env_const = SOME stamp <=> F