-
Notifications
You must be signed in to change notification settings - Fork 85
/
Copy pathcandle_kernelProgScript.sml
208 lines (165 loc) · 6.47 KB
/
candle_kernelProgScript.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
(*
Adds Candle specific functions to the kernel module from ml_hol_kernel_funsProg
*)
open preamble;
open ml_translatorLib ml_monad_translatorLib ml_progLib ml_hol_kernel_funsProgTheory;
open basisFunctionsLib print_thmTheory;
open (* lisp: *) lisp_parsingTheory lisp_valuesTheory lisp_printingTheory;
open (* compute: *) compute_syntaxTheory compute_evalTheory computeTheory
compute_pmatchTheory;
open runtime_checkTheory runtime_checkLib;
val _ = new_theory "candle_kernelProg";
val _ = set_grammar_ancestry [ "ml_hol_kernel_funsProg", "compute"
];
val _ = m_translation_extends "ml_hol_kernel_funsProg"
val _ = (use_long_names := false);
val _ = ml_prog_update open_local_block;
val r = translate lisp_valuesTheory.name_def;
val r = translate lisp_printingTheory.num2ascii_def;
val r = translate lisp_printingTheory.ascii_name_def;
val lemma = prove(“ascii_name_side v3”,
fs [fetch "-" "ascii_name_side_def"]
\\ fs [Once lisp_printingTheory.num2ascii_def,AllCaseEqs()])
|> update_precondition;
val r = translate num2str_def;
val lemma = prove(“∀n. num2str_side n”,
ho_match_mp_tac lisp_printingTheory.num2str_ind
\\ rw [] \\ simp [Once (fetch "-" "num2str_side_def")]
\\ rw [] \\ gvs [DIV_LT_X]
\\ ‘n MOD 10 < 10’ by fs []
\\ decide_tac)
|> update_precondition;
val r = translate lisp_printingTheory.name2str_def;
val r = translate lisp_valuesTheory.list_def;
val r = translate nil_list_def;
val r = translate str_to_v_def;
val r = translate ty_to_v_def;
val r = translate term_to_v_def;
val r = translate thm_to_v_def;
val r = translate update_to_v_def;
val r = translate dest_quote_def;
val r = translate dest_list_def;
val r = translate newlines_def;
val r = translate v2pretty_def;
val r = translate get_size_def;
val r = translate get_next_size_def;
val r = translate annotate_def;
val r = translate remove_all_def;
val r = translate smart_remove_def;
val r = translate flatten_def;
val r = translate dropWhile_def;
val r = translate is_comment_def;
val r = translate v2str_def;
val r = translate vs2str_def;
val r = translate thm_to_string_def;
val _ = ml_prog_update open_local_in_block;
val _ = (append_prog o process_topdecs) `
val print_thm = fn th => case th of Sequent tms c =>
let
val ctxt = !the_context
val str = thm_to_string ctxt th
val arr = Word8Array.array 0 (Word8.fromInt 0)
in
#(kernel_ffi) str arr
end;
`
(* compute primitive *)
val _ = ml_prog_update open_local_block;
val r = translate dest_num_PMATCH;
val r = m_translate dest_numeral_PMATCH;
val r = translate dest_numeral_opt_PMATCH;
val r = translate list_dest_comb_def;
val r = translate mapOption_def;
val r = translate app_type_def;
val r = translate dest_cexp_def;
Theorem dest_cexp_side[local]:
∀x. dest_cexp_side x
Proof
ho_match_mp_tac dest_cexp_ind \\ rw []
\\ once_rewrite_tac [fetch "-" "dest_cexp_side_def"] \\ rw []
QED
val _ = update_precondition dest_cexp_side;
val r = m_translate option_def;
val r = m_translate check_def;
val r = translate SAFEMOD_def;
val r = translate SAFEDIV_def;
val r = translate num2bit_def;
val r = translate compute_execTheory.cv2term_def
val r = compute_thms_def |> EVAL_RULE |> translate;
val r = m_translate dest_binary_PMATCH;
val r = check [‘ths’] compute_init_def |> translate;
val r = m_translate check_var_def;
val _ = use_mem_intro := true;
val res = translate_no_ind check_cexp_closed_def;
Triviality check_cexp_closed_ind:
check_cexp_closed_ind
Proof
rewrite_tac [fetch "-" "check_cexp_closed_ind_def"]
\\ rpt gen_tac
\\ rpt (disch_then strip_assume_tac)
\\ match_mp_tac (latest_ind ())
\\ rpt strip_tac
\\ last_x_assum match_mp_tac
\\ rpt strip_tac
\\ fs [FORALL_PROD, GSYM ml_translatorTheory.MEMBER_INTRO]
QED
val _ = check_cexp_closed_ind |> update_precondition;
val _ = use_mem_intro := false;
val r = translate var_list_def;
val r = translate const_list_def;
val r = m_translate map_def;
val _ = use_mem_intro := true;
val r = m_translate check_consts_def;
val r = m_translate check_eqn_def;
val _ = use_mem_intro := false;
val r = translate compute_default_clock; (* TODO _def *)
val r = translate indexedListsTheory.findi_def
val r = translate compute_execTheory.monop_fst_def
val r = translate compute_execTheory.monop_snd_def
val r = translate compute_execTheory.monop_ispair_def
val r = translate compute_execTheory.monop_def
val r = translate compute_execTheory.to_num_def
val r = translate compute_execTheory.cv_T_def
val r = translate compute_execTheory.cv_F_def
val r = translate compute_execTheory.binop_add_def
val r = translate (compute_execTheory.binop_sub_def |> REWRITE_RULE [GSYM ml_translatorTheory.sub_check_def]);
val r = translate compute_execTheory.binop_mul_def
val r = translate compute_execTheory.binop_div_def
val r = translate compute_execTheory.binop_mod_def
val r = translate compute_execTheory.binop_eq_def
val r = translate compute_execTheory.binop_less_def
val r = translate compute_execTheory.binop_def
val r = translate compute_execTheory.to_ce_def
val r = translate compute_execTheory.compile_to_ce_def
val r = translate compute_execTheory.build_funs_def
val r = translate compute_execTheory.env_lookup_def
val r = m_translate compute_execTheory.get_code_def
val r = m_translate compute_execTheory.exec_def
val _ = ml_prog_update open_local_in_block;
val r = check [‘ths’,‘tm’] compute_add_def |> m_translate;
val r = compute_def
|> SIMP_RULE(srw_ss()) [combinTheory.C_DEF]
|> check [‘ths’,‘ceqs’,‘tm’]
|> m_translate;
val _ = ml_prog_update close_local_blocks;
val _ = ml_prog_update (close_module NONE);
(* extract the interesting theorem *)
val _ = Globals.max_print_depth := 10;
fun define_abbrev_conv name tm = let
val def = define_abbrev true name tm
in GSYM def |> SPEC_ALL end
Theorem candle_prog_thm =
get_Decls_thm (get_ml_prog_state())
|> CONV_RULE ((RATOR_CONV o RATOR_CONV o RAND_CONV)
(EVAL THENC define_abbrev_conv "candle_code"))
|> CONV_RULE ((RATOR_CONV o RAND_CONV)
(EVAL THENC define_abbrev_conv "candle_init_env"))
|> CONV_RULE ((RAND_CONV)
(EVAL THENC define_abbrev_conv "candle_init_state"));
(* extract some other other theorems *)
Theorem EqualityType_TYPE_TYPE = EqualityType_rule [] “:type”;
Theorem EqualityType_TERM_TYPE = EqualityType_rule [] “:term”;
Theorem EqualityType_THM_TYPE = EqualityType_rule [] “:thm”;
Theorem EqualityType_UPDATE_TYPE = EqualityType_rule [] “:update”;
val _ = (print_asts := true);
val _ = export_theory();