-
Notifications
You must be signed in to change notification settings - Fork 81
/
decodeProgScript.sml
253 lines (211 loc) · 9.36 KB
/
decodeProgScript.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
(*
Translate the compiler's state decoder.
*)
open preamble basisFunctionsLib
num_list_enc_decTheory num_tree_enc_decTheory backend_enc_decTheory
explorerProgTheory ml_translatorLib ml_translatorTheory cfLib
val _ = new_theory "decodeProg"
val _ = translation_extends "explorerProg";
val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "decodeProg");
(* translator setup *)
val RW = REWRITE_RULE
val RW1 = ONCE_REWRITE_RULE
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 dest_fun_type = dom_rng
val mk_fun_type = curry op -->;
fun list_mk_fun_type [ty] = ty
| list_mk_fun_type (ty1::tys) =
mk_fun_type ty1 (list_mk_fun_type tys)
| list_mk_fun_type _ = fail()
val _ = add_preferred_thy "-";
val _ = add_preferred_thy "termination";
Theorem NOT_NIL_AND_LEMMA:
(b <> [] /\ x) = if b = [] then F else x
Proof
Cases_on `b` THEN FULL_SIMP_TAC std_ss []
QED
val extra_preprocessing = ref [MEMBER_INTRO,MAP];
fun def_of_const tm = let
val res = dest_thy_const tm handle HOL_ERR _ =>
failwith ("Unable to translate: " ^ term_to_string tm)
val name = (#Name res)
fun def_from_thy thy name =
DB.fetch thy (name ^ "_pmatch") handle HOL_ERR _ =>
DB.fetch thy (name ^ "_def") handle HOL_ERR _ =>
DB.fetch thy (name ^ "_DEF") handle HOL_ERR _ =>
DB.fetch thy name
val def = def_from_thy "termination" name handle HOL_ERR _ =>
def_from_thy (#Thy res) name handle HOL_ERR _ =>
failwith ("Unable to find definition of " ^ name)
val def = def |> RW (!extra_preprocessing)
|> CONV_RULE (DEPTH_CONV BETA_CONV)
|> SIMP_RULE bool_ss [IN_INSERT,NOT_IN_EMPTY]
|> REWRITE_RULE [NOT_NIL_AND_LEMMA]
in def end
val _ = (find_def_for_const := def_of_const);
(* --- *)
val _ = ml_translatorLib.use_string_type true;
val _ = register_type “:lab_to_target$inc_config”
val _ = ml_translatorLib.use_string_type false;
val _ = register_type “:backend$inc_config”
Theorem IsTypeRep_BACKEND_INC_CONFIG_v:
IsTypeRep BACKEND_INC_CONFIG_v BACKEND_INC_CONFIG_TYPE
Proof
irule_at Any (fetch_v_fun “:backend$inc_config” |> snd |> hd) \\ fs []
\\ irule_at Any (fetch_v_fun “:bvl_to_bvi$config” |> snd |> hd) \\ fs []
\\ irule_at Any (fetch_v_fun “:clos_to_bvl$config” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:'a num_map” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:'a # 'b” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:'a option” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:'a list” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:'a num_map” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:'a # 'b” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:clos_known$config” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:'a list” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:closLang$exp” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:bvl$exp” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:closLang$op” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:'a list” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:'a num_map” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:clos_known$val_approx” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:closLang$exp” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:closLang$op” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:'a list” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:unit” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:num” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:closLang$const_part” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:closLang$const” |> snd |> hd) \\ fs []
\\ rpt $ irule_at Any (fetch_v_fun “:word64” |> snd |> hd) \\ fs []
QED
Theorem EqualityType_BACKEND_INC_CONFIG_TYPE =
EqualityType_rule [] “:backend$inc_config”;
Theorem INJ_BACKEND_INC_CONFIG_v[simp]:
INJ BACKEND_INC_CONFIG_v UNIV UNIV
Proof
irule ml_translatorTheory.IsTypeRep_EqualityType_INJ
\\ irule_at Any IsTypeRep_BACKEND_INC_CONFIG_v
\\ fs [EqualityType_BACKEND_INC_CONFIG_TYPE]
QED
(* --- *)
val res = translate dec_next_def;
val res = translate chars_to_nums_def;
val res = translate num_list_enc_decTheory.mlstring_dec_def;
val res = translate (mlstring_dec'_def |> REWRITE_RULE [GSYM mlstringTheory.implode_def]);
Theorem list_dec'_eq_MAP:
∀f t. list_dec' f t = MAP f (list_dec' I t)
Proof
Cases_on ‘t’ \\ fs [list_dec'_def]
QED
val res = translate num_list_enc_decTheory.list_dec'_def;
val res = translate (const_dec'_def |> DefnBase.one_line_ify NONE
|> ONCE_REWRITE_RULE [list_dec'_eq_MAP]);
val res = translate const_dec_def;
val res = translate unit_dec_def;
val res = translate num_dec_def;
val res = translate list_dec_def;
val res = translate bool_dec_def;
val res = translate int_dec_def;
val _ = next_ml_names := ["word8_dec"];
val res = translate (word_dec_def |> INST_TYPE [alpha|->“:8”]);
val _ = next_ml_names := ["word64_dec"];
val res = translate (word_dec_def |> INST_TYPE [alpha|->“:64”]);
val res = translate char_dec_def;
val res = translate prod_dec_def;
val res = translate option_dec_def;
val res = translate sum_dec_def;
val res = translate spt_dec'_def;
val res = translate spt_dec''_def;
val res = translate spt_dec_def;
val res = translate namespace_dec'_def;
val res = translate namespace_dec_def;
(* --- *)
val res = translate num_tree_dec'_def;
val res = translate num_tree_dec_def;
val res = translate nth_def;
val res = translate int_dec'_def;
val res = translate bool_dec'_def;
val res = translate chr_dec'_def;
val res = translate list_dec'_def;
val res = translate pair_dec'_def;
val res = translate option_dec'_def;
(* --- *)
val _ = ml_translatorLib.use_string_type false;
val res = translate (tra_dec'_def |> DefnBase.one_line_ify NONE);
val res = translate safe_chr_list_def;
val res = translate list_chr_dec'_def;
val _ = ml_translatorLib.use_string_type true;
val res = translate string_dec_def;
val res = translate next_indices_dec_def;
val res = translate flat_pattern_config_dec_def;
val res = translate namespace_dec'_def;
val res = translate namespace_dec_def;
val res = translate (var_name_dec'_def |> REWRITE_RULE [string_dec'_intro]);
val res = translate var_name_dec_def;
val res = translate environment_dec_def;
val res = translate environment_store_dec_def;
val res = translate source_to_flat_config_dec_def;
val _ = ml_translatorLib.use_string_type false;
val res = translate data_to_word_config_dec_def;
val res = translate word_to_word_config_dec_def;
val res = translate (word_to_stack_config_dec_def |> INST_TYPE [alpha|->“:64”]);
val res = translate stack_to_lab_config_dec_def;
val res = translate tap_config_dec'_def;
val res = translate tap_config_dec_def;
val res = translate (closLang_op_dec'_def |> DefnBase.one_line_ify NONE);
val def = bvl_exp_dec'_def |> DefnBase.one_line_ify NONE
|> ONCE_REWRITE_RULE [list_dec'_eq_MAP]
val res = translate def;
val res = translate bvl_to_bvi_config_dec_def;
Theorem pair_dec'_eq:
pair_dec' d1 d2 = λt. (d1 (nth 0 (list_dec' I t)), d2 (nth 1 (list_dec' I t)))
Proof
fs [FUN_EQ_THM,FORALL_PROD]
\\ Cases \\ fs [pair_dec'_def,list_dec'_def]
QED
val def = closLang_exp_dec'_def |> DefnBase.one_line_ify NONE
|> ONCE_REWRITE_RULE [list_dec'_eq_MAP]
|> ONCE_REWRITE_RULE [pair_dec'_eq]
|> CONV_RULE (DEPTH_CONV BETA_CONV)
val res = translate_no_ind def;
val ind_lemma = Q.prove(
`^(first is_forall (hyp res))`,
rpt gen_tac
\\ rpt (disch_then strip_assume_tac)
\\ match_mp_tac (latest_ind ())
\\ rpt strip_tac
\\ last_x_assum irule
\\ rewrite_tac [num_tree_11]
\\ rpt gen_tac \\ strip_tac
\\ rpt var_eq_tac
\\ gen_tac \\ disch_then (assume_tac o SYM)
\\ Cases_on ‘x6 = 0’ \\ asm_rewrite_tac [] THEN1 (gvs [ADD1])
\\ ‘n ≠ 1 ∧ n ≠ 0’ by decide_tac
\\ Cases_on ‘x6 = 1’ \\ asm_rewrite_tac [] THEN1 (gvs [ADD1])
\\ ‘n ≠ 2’ by decide_tac
\\ Cases_on ‘n = 3’ \\ asm_rewrite_tac [] THEN1 (gvs [ADD1])
\\ Cases_on ‘n = 4’ \\ asm_rewrite_tac [] THEN1 (gvs [ADD1])
\\ Cases_on ‘n = 5’ \\ asm_rewrite_tac [] THEN1 (gvs [ADD1])
\\ Cases_on ‘n = 6’ \\ asm_rewrite_tac [] THEN1 (gvs [ADD1])
\\ Cases_on ‘n = 7’ \\ asm_rewrite_tac [] THEN1 (gvs [ADD1])
\\ Cases_on ‘n = 8’ \\ asm_rewrite_tac [] THEN1 (gvs [ADD1])
\\ Cases_on ‘n = 9’ \\ asm_rewrite_tac []
\\ rpt var_eq_tac \\ gvs [ADD1])
|> update_precondition;
val def = val_approx_dec'_def |> DefnBase.one_line_ify NONE
|> ONCE_REWRITE_RULE [list_dec'_eq_MAP]
val res = translate def;
val def = clos_to_bvl_config_dec_def
val res = translate def;
val _ = ml_translatorLib.use_string_type true;
val def = lab_to_target_inc_config_dec_def
|> REWRITE_RULE [GSYM string_dec_thm]
val res = translate def;
val _ = ml_translatorLib.use_string_type false;
val res = translate inc_config_dec_def;
val res = translate decode_backend_config_def;
val () = Feedback.set_trace "TheoryPP.include_docs" 0;
val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
val _ = (ml_translatorLib.clean_on_exit := true);
val _ = export_theory();