Update bootstrap translation for new --explore

CakeML · Aug 6, 2023 · 05f3824 · 05f3824
1 parent 29e25c9
commit 05f3824
Show file tree

Hide file tree

Showing 7 changed files with 208 additions and 113 deletions.
diff --git a/compiler/bootstrap/translation/compiler32ProgScript.sml b/compiler/bootstrap/translation/compiler32ProgScript.sml
@@ -39,26 +39,7 @@ Proof
   rw[FUN_EQ_THM] \\ EVAL_TAC
 QED
 
-(*
-
-val def = spec32 backendTheory.compile_explorer_def
-
-val res = translate def
-
-val backend_compile_explorer_side = Q.prove(`
-  ∀x y. backend_compile_explorer_side x y = T`,
-  simp[definition"backend_compile_explorer_side_def",PULL_FORALL] \\
-  rpt gen_tac \\ ntac 3 strip_tac \\
-  qmatch_goalsub_abbrev_tac`compile c.do_mti c.max_app [z]` \\
-  `∃a. compile c.do_mti c.max_app [z] = [a]` by
-    (Cases_on`c.do_mti`>>fs[clos_mtiTheory.compile_def]>>
-    metis_tac[clos_mtiTheory.intro_multi_sing])>>
-  specl_args_of_then ``renumber_code_locs_list``
-    (clos_numberTheory.renumber_code_locs_length|>CONJUNCT1) assume_tac>>
-  rfs[LENGTH_EQ_NUM_compute] \\
-  strip_tac \\ fs[]) |> update_precondition;
-
-*)
+val r = translate presLangTheory.default_tap_config_def;
 
 val def = spec32
   (backendTheory.attach_bitmaps_def
@@ -67,16 +48,50 @@ val def = spec32
 
 val res = translate def
 
-val def = spec32 backendTheory.compile_tap_def
+val def = spec32 backendTheory.compile_def
   |> REWRITE_RULE[max_heap_limit_32_thm]
 
 val res = translate def
 
-val def = spec32 backendTheory.compile_def
+val _ = register_type “:32 any_prog”
 
-val res = translate def
+val r = backend_passesTheory.to_flat_all_def |> spec32 |> translate;
+val r = backend_passesTheory.to_clos_all_def |> spec32 |> translate;
+val r = backend_passesTheory.to_bvl_all_def |> spec32 |> translate;
+val r = backend_passesTheory.to_bvi_all_def |> spec32 |> translate;
+
+Triviality backend_passes_to_bvi_all_side:
+  backend_passes_to_bvi_all_side c p
+Proof
+  fs [fetch "-" "backend_passes_to_bvi_all_side_def"]
+  \\ rewrite_tac [GSYM LENGTH_NIL,bvl_inlineTheory.LENGTH_remove_ticks]
+  \\ fs []
+QED
+
+val _ = update_precondition backend_passes_to_bvi_all_side
+
+val r = backend_passesTheory.to_data_all_def |> spec32 |> translate;
+
+val r = backend_passesTheory.to_word_all_def |> spec32
+          |> REWRITE_RULE [data_to_wordTheory.stubs_def,APPEND] |> translate;
+
+val r = backend_passesTheory.to_stack_all_def |> spec32
+          |> REWRITE_RULE[max_heap_limit_32_thm] |> translate;
+
+val r = backend_passesTheory.to_lab_all_def |> spec32
+          |> REWRITE_RULE[max_heap_limit_32_thm] |> translate;
+
+val r = backend_passesTheory.to_target_all_def |> spec32 |> translate;
+
+val r = presLangTheory.word_to_strs_def |> spec32 |> translate
+val r = presLangTheory.stack_to_strs_def |> spec32 |> translate
+val r = presLangTheory.lab_to_strs_def |> spec32 |> translate
+
+val r = backend_passesTheory.any_prog_pp_def |> spec32 |> translate;
+val r = backend_passesTheory.any_prog_pp_with_title_def |> spec32 |> translate;
+val r = backend_passesTheory.compile_tap_def |> spec32 |> translate;
 
-val _ = res |> hyp |> null orelse
+val _ = r |> hyp |> null orelse
         failwith "Unproved side condition in the translation of backendTheory.compile_def.";
 
 (* exportTheory *)
@@ -157,7 +172,8 @@ val _ = translate (compilerTheory.parse_sexp_input_def
 val def = spec32 (compilerTheory.compile_def);
 val res = translate def;
 
-val res = translate basisProgTheory.basis_def
+val _ = print "About to translate basis (this takes some time) ";
+val res = translate basisProgTheory.basis_def;
 
 val res = translate (primTypesTheory.prim_tenv_def
                      |> CONV_RULE (RAND_CONV EVAL));

diff --git a/compiler/bootstrap/translation/compiler64ProgScript.sml b/compiler/bootstrap/translation/compiler64ProgScript.sml
@@ -40,26 +40,7 @@ Proof
   rw[FUN_EQ_THM] \\ EVAL_TAC
 QED
 
-(*
-
-val def = spec64 backendTheory.compile_explorer_def
-
-val res = translate def
-
-val backend_compile_explorer_side = Q.prove(`
-  ∀x y. backend_compile_explorer_side x y = T`,
-  simp[definition"backend_compile_explorer_side_def",PULL_FORALL] \\
-  rpt gen_tac \\ ntac 3 strip_tac \\
-  qmatch_goalsub_abbrev_tac`compile c.do_mti c.max_app [z]` \\
-  `∃a. compile c.do_mti c.max_app [z] = [a]` by
-    (Cases_on`c.do_mti`>>fs[clos_mtiTheory.compile_def]>>
-    metis_tac[clos_mtiTheory.intro_multi_sing])>>
-  specl_args_of_then ``renumber_code_locs_list``
-    (clos_numberTheory.renumber_code_locs_length|>CONJUNCT1) assume_tac>>
-  rfs[LENGTH_EQ_NUM_compute] \\
-  strip_tac \\ fs[]) |> update_precondition;
-
-*)
+val r = translate presLangTheory.default_tap_config_def;
 
 val def = spec64
           (backendTheory.attach_bitmaps_def
@@ -68,17 +49,51 @@ val def = spec64
 
 val res = translate def
 
-val def = spec64 backendTheory.compile_tap_def
-            |> REWRITE_RULE[max_heap_limit_64_thm]
+val def = spec64 backendTheory.compile_def
+  |> REWRITE_RULE[max_heap_limit_64_thm]
 
 val res = translate def
 
-val def = spec64 backendTheory.compile_def
+val _ = register_type “:64 any_prog”
 
-val res = translate def
+val r = backend_passesTheory.to_flat_all_def |> spec64 |> translate;
+val r = backend_passesTheory.to_clos_all_def |> spec64 |> translate;
+val r = backend_passesTheory.to_bvl_all_def |> spec64 |> translate;
+val r = backend_passesTheory.to_bvi_all_def |> spec64 |> translate;
+
+Triviality backend_passes_to_bvi_all_side:
+  backend_passes_to_bvi_all_side c p
+Proof
+  fs [fetch "-" "backend_passes_to_bvi_all_side_def"]
+  \\ rewrite_tac [GSYM LENGTH_NIL,bvl_inlineTheory.LENGTH_remove_ticks]
+  \\ fs []
+QED
+
+val _ = update_precondition backend_passes_to_bvi_all_side
+
+val r = backend_passesTheory.to_data_all_def |> spec64 |> translate;
+
+val r = backend_passesTheory.to_word_all_def |> spec64
+          |> REWRITE_RULE [data_to_wordTheory.stubs_def,APPEND] |> translate;
+
+val r = backend_passesTheory.to_stack_all_def |> spec64
+          |> REWRITE_RULE[max_heap_limit_64_thm] |> translate;
+
+val r = backend_passesTheory.to_lab_all_def |> spec64
+          |> REWRITE_RULE[max_heap_limit_64_thm] |> translate;
+
+val r = backend_passesTheory.to_target_all_def |> spec64 |> translate;
+
+val r = presLangTheory.word_to_strs_def |> spec64 |> translate
+val r = presLangTheory.stack_to_strs_def |> spec64 |> translate
+val r = presLangTheory.lab_to_strs_def |> spec64 |> translate
+
+val r = backend_passesTheory.any_prog_pp_def |> spec64 |> translate;
+val r = backend_passesTheory.any_prog_pp_with_title_def |> spec64 |> translate;
+val r = backend_passesTheory.compile_tap_def |> spec64 |> translate;
 
-val _ = res |> hyp |> null orelse
-                           failwith "Unproved side condition in the translation of backendTheory.compile_def.";
+val _ = r |> hyp |> null orelse
+        failwith "Unproved side condition in the translation of backendTheory.compile_def.";
 
 (* exportTheory *)
 (* TODO: exportTheory functions that don't depend on the word size
@@ -158,8 +173,8 @@ val _ = translate (compilerTheory.parse_sexp_input_def
 val def = spec64 (compilerTheory.compile_def);
 val res = translate def;
 
-val _ = print "About to translate basis (this takes some time)";
-val res = translate basisProgTheory.basis_def
+val _ = print "About to translate basis (this takes some time) ";
+val res = translate basisProgTheory.basis_def;
 
 val res = translate (primTypesTheory.prim_tenv_def
                        |> CONV_RULE (RAND_CONV EVAL));

diff --git a/compiler/bootstrap/translation/explorerProgScript.sml b/compiler/bootstrap/translation/explorerProgScript.sml
@@ -56,28 +56,24 @@ QED
 
 val _ = json_to_mlstring_ind |> update_precondition;
 
-val res = translate presLangTheory.num_to_hex_def;
+(* str_tree and displayLang *)
+
+val r = translate str_treeTheory.v2strs_def;
+val r = translate displayLangTheory.display_to_str_tree_def;
 
-val res = translate
-  (presLangTheory.display_word_to_hex_string_def |> INST_TYPE [``:'a``|->``:8``]);
-val res = translate
-  (presLangTheory.display_word_to_hex_string_def |> INST_TYPE [``:'a``|->``:64``]);
+(* presLang *)
 
-val res = translate displayLangTheory.trace_to_json_def;
-val res = translate displayLangTheory.display_to_json_def;
+val res = translate presLangTheory.num_to_hex_def;
+val res = translate (presLangTheory.word_to_display_def |> INST_TYPE [``:'a``|->``:8``]);
+val res = translate (presLangTheory.word_to_display_def |> INST_TYPE [``:'a``|->``:64``]);
 
-(* fixme: flat op datatype has been translated with use_string_type, which
-   for compatibility here needs that switch on, and looks like it results
-   in an unnecessary explode/implode pair *)
 val _ = ml_translatorLib.use_string_type true;
-val res = translate (presLangTheory.flat_op_to_display_def);
+val res = translate presLangTheory.source_to_strs_def;
 val _ = ml_translatorLib.use_string_type false;
 
-val _ = translate presLangTheory.lang_to_json_def
-
-(* again *)
 val _ = ml_translatorLib.use_string_type true;
-val r = translate presLangTheory.lit_to_display_def
+val res = translate presLangTheory.flat_to_strs_def;
+val res = translate presLangTheory.clos_op_to_display_def;
 val _ = ml_translatorLib.use_string_type false;
 
 val r = translate presLangTheory.num_to_varn_def
@@ -88,38 +84,55 @@ val num_to_varn_side = Q.prove(`
   `n MOD 26 < 26` by simp[] \\ decide_tac)
   |> update_precondition;
 
-Theorem string_imp_lam:
-  string_imp = \s. String (implode s)
-Proof
-  fs [FUN_EQ_THM,presLangTheory.string_imp_def]
-QED
+val r = presLangTheory.display_num_as_varn_def
+          |> REWRITE_RULE [presLangTheory.string_imp_def]
+          |> translate;
 
-val string_imp = SIMP_RULE bool_ss [string_imp_lam];
+val r = translate presLangTheory.data_prog_to_display_def;
+val r = translate presLangTheory.data_fun_to_display_def;
+val r = translate presLangTheory.data_to_strs_def;
 
-val r = translate (presLangTheory.display_num_as_varn_def |> string_imp);
-val _ = ml_translatorLib.use_string_type true;
-val res = translate (presLangTheory.flat_to_display_def)
-val _ = ml_translatorLib.use_string_type false;
+val r = translate presLangTheory.bvl_to_display_def;
+val r = translate presLangTheory.bvl_fun_to_display_def;
+val r = translate presLangTheory.bvl_to_strs_def;
 
-val res = translate presLangTheory.tap_flat_def;
+val r = translate presLangTheory.bvi_to_display_def;
+val r = translate presLangTheory.bvi_fun_to_display_def;
+val r = translate presLangTheory.bvi_to_strs_def;
 
-val _ = ml_translatorLib.use_string_type true;
-val r = translate (presLangTheory.clos_op_to_display_def |> string_imp);
-val _ = ml_translatorLib.use_string_type false;
+val r = translate clos_to_bvlTheory.init_code_def;
 
-val r = translate (presLangTheory.clos_to_display_def |> string_imp);
+Triviality bvl_jump_jumplist_side:
+  ∀x y. bvl_jump_jumplist_side x y
+Proof
+  ho_match_mp_tac bvl_jumpTheory.JumpList_ind
+  \\ rw [] \\ simp [Once to_bvlProgTheory.bvl_jump_jumplist_side_def]
+  \\ Cases_on ‘xs’ \\ fs []
+QED
+
+Triviality init_code_side:
+  init_code_side x
+Proof
+  fs [fetch "-" "init_code_side_def",
+      to_bvlProgTheory.clos_to_bvl_generate_generic_app_side_def,
+      to_bvlProgTheory.bvl_jump_jump_side_def,bvl_jump_jumplist_side]
+QED
 
-val res = translate presLangTheory.tap_clos_def;
+Triviality string_imp_thm:
+  string_imp = λs. String (implode s)
+Proof
+  fs [FUN_EQ_THM,presLangTheory.string_imp_def]
+QED
 
-val res = translate presLangTheory.tap_data_lang_def;
+val _ = ml_translatorLib.use_string_type true;
+val r = presLangTheory.clos_to_display_def
+          |> REWRITE_RULE [string_imp_thm]
+          |> translate
 
-(* we can't translate the tap_word bits yet, because that's 32/64 specific.
-   that's done in the to_word* scripts. *)
+val r = translate presLangTheory.clos_dec_to_display_def;
+val r = translate presLangTheory.clos_to_strs_def;
 
-(* more parts of the external interface *)
-val res = translate presLangTheory.default_tap_config_def;
-val res = translate presLangTheory.mk_tap_config_def;
-val res = translate presLangTheory.tap_data_mlstrings_def;
+val _ = update_precondition init_code_side;
 
 val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 

diff --git a/compiler/bootstrap/translation/to_target32ProgScript.sml b/compiler/bootstrap/translation/to_target32ProgScript.sml
@@ -348,6 +348,18 @@ val res = translate compile_lab_thm;
 
 val res = translate (spec32 compile_def)
 
+(* explorer specific functions *)
+
+val res = presLangTheory.asm_cmp_to_display_def |> spec32 |> translate;
+val res = presLangTheory.asm_asm_to_display_def |> spec32 |> translate;
+val res = presLangTheory.lab_asm_to_display_def |> spec32
+          |> REWRITE_RULE [presLangTheory.string_imp_def] |> translate;
+val res = presLangTheory.lab_line_to_display_def |> spec32 |> translate;
+val res = presLangTheory.lab_fun_to_display_def |> spec32 |> translate;
+val res = presLangTheory.stack_prog_to_display_def |> spec32
+          |> REWRITE_RULE [presLangTheory.string_imp_def] |> translate;
+val res = presLangTheory.stack_fun_to_display_def |> spec32 |> translate;
+
 val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);

diff --git a/compiler/bootstrap/translation/to_target64ProgScript.sml b/compiler/bootstrap/translation/to_target64ProgScript.sml
@@ -348,6 +348,18 @@ val res = translate compile_lab_thm;
 
 val res = translate (spec64 compile_def);
 
+(* explorer specific functions *)
+
+val res = presLangTheory.asm_cmp_to_display_def |> spec64 |> translate;
+val res = presLangTheory.asm_asm_to_display_def |> spec64 |> translate;
+val res = presLangTheory.lab_asm_to_display_def |> spec64
+          |> REWRITE_RULE [presLangTheory.string_imp_def] |> translate;
+val res = presLangTheory.lab_line_to_display_def |> spec64 |> translate;
+val res = presLangTheory.lab_fun_to_display_def |> spec64 |> translate;
+val res = presLangTheory.stack_prog_to_display_def |> spec64
+          |> REWRITE_RULE [presLangTheory.string_imp_def] |> translate;
+val res = presLangTheory.stack_fun_to_display_def |> spec64 |> translate;
+
 val () = Feedback.set_trace "TheoryPP.include_docs" 0;
 
 val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);

diff --git a/compiler/bootstrap/translation/to_word32ProgScript.sml b/compiler/bootstrap/translation/to_word32ProgScript.sml
@@ -631,17 +631,30 @@ val _ = translate stack_removeTheory.stub_names_def
 val res = translate (data_to_wordTheory.compile_def
                      |> SIMP_RULE std_ss [data_to_wordTheory.stubs_def] |> conv32_RHS);
 
-(* translate some 32/64 specific parts of the tap/explorer
-   that can't be translated in explorerProgScript *)
-val res = translate (presLangTheory.tap_word_def |> conv32);
-val res = translate (presLangTheory.store_name_to_display_def |> conv32);
-val res = translate (presLangTheory.stack_prog_to_display_def |> conv32);
-val res = translate (presLangTheory.stack_progs_to_display_def |> conv32);
-val res = translate (presLangTheory.tap_stack_def |> conv32);
-val res = translate (presLangTheory.lab_asm_to_display_def |> conv32);
-val res = translate (presLangTheory.lab_line_to_display_def |> conv32);
-val res = translate (presLangTheory.lab_secs_to_display_def |> conv32);
-val res = translate (presLangTheory.tap_lab_def |> conv32);
+(* explorer specific functions *)
+
+val _ = ml_translatorLib.use_string_type false;
+val r = presLangTheory.num_to_hex_def |> translate;
+val r = presLangTheory.word_to_display_def |> conv32 |> translate;
+val r = presLangTheory.item_with_word_def |> conv32 |> translate;
+val r = presLangTheory.asm_binop_to_display_def |> translate;
+val r = presLangTheory.asm_reg_imm_to_display_def |> conv32 |> translate;
+val r = presLangTheory.asm_arith_to_display_def |> conv32 |> translate;
+val r = presLangTheory.word_to_display_def |> INST_TYPE [“:'a”|->“:5”] |> translate
+val r = presLangTheory.item_with_word_def |> INST_TYPE [“:'a”|->“:5”] |> translate
+val r = presLangTheory.store_name_to_display_def |> conv32 |> translate
+val r = presLangTheory.word_exp_to_display_def |> conv32 |> translate
+val r = presLangTheory.asm_inst_to_display_def |> conv32 |> translate;
+val r = presLangTheory.ws_to_display_def |> conv32 |> translate
+val r = presLangTheory.word_seqs_def |> conv32 |> translate
+
+val _ = ml_translatorLib.use_string_type true;
+val r = presLangTheory.word_prog_to_display_def
+          |> conv32
+          |> REWRITE_RULE [presLangTheory.string_imp_def]
+          |> translate
+
+val r = presLangTheory.word_fun_to_display_def |> conv32 |> translate
 
 val () = Feedback.set_trace "TheoryPP.include_docs" 0;