Permalink
Browse files

Use modules in bootstrap translation.

This should speed up bootstrap translation a bit, since the
number of things in the top-level namespace has an impact on
translator performance. Grouping many things in modules keeps
them out of the top-level namespace.
  • Loading branch information...
Thomas Sewell authored and xrchz committed Oct 9, 2018
1 parent cc95061 commit 2ce1a84a603f5e9acdd2601314dd649077ede745
@@ -9,6 +9,8 @@ val _ = new_theory "arm6Prog"
val _ = translation_extends "to_target32Prog";
val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "arm6Prog");
val _ = add_preferred_thy "-";
val _ = add_preferred_thy "termination";
@@ -204,6 +206,8 @@ val res = translate (arm6_config_def |> SIMP_RULE std_ss[valid_immediate_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();
@@ -9,6 +9,8 @@ val _ = new_theory "arm8Prog"
val _ = translation_extends "x64Prog";
val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "arm8Prog");
val _ = add_preferred_thy "-";
val _ = add_preferred_thy "termination";
@@ -306,6 +308,8 @@ val res = translate (arm8_config_def |> SIMP_RULE bool_ss [IN_INSERT,NOT_IN_EMPT
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();
@@ -8,6 +8,8 @@ val _ = new_theory"compiler32Prog";
val _ = translation_extends "arm6Prog";
val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "compiler32Prog");
val () = Globals.max_print_depth := 15;
val () = use_long_names := true;
@@ -162,6 +164,10 @@ val res = translate
(arm6_configTheory.arm6_backend_config_def
|> SIMP_RULE(srw_ss())[FUNION_FUPDATE_1]);
(* Leave the module now, so that key things are available in the toplevel
namespace for main. *)
val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
(* Rest of the translation *)
val res = translate (extend_conf_def |> spec32 |> SIMP_RULE (srw_ss()) [MEMBER_INTRO]);
val res = translate parse_target_32_def;
@@ -8,6 +8,8 @@ val _ = new_theory"compiler64Prog";
val _ = translation_extends "mipsProg";
val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "compiler64Prog");
val _ = (ml_translatorLib.trace_timing_to
:= SOME "compiler64Prog_translate_timing.txt")
@@ -189,6 +191,10 @@ val res = translate
(arm8_configTheory.arm8_backend_config_def
|> SIMP_RULE(srw_ss())[FUNION_FUPDATE_1]);
(* Leave the module now, so that key things are available in the toplevel
namespace for main. *)
val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
(* Rest of the translation *)
val res = translate (extend_conf_def |> spec64 |> SIMP_RULE (srw_ss()) [MEMBER_INTRO]);
val res = translate parse_target_64_def;
@@ -6,6 +6,8 @@ val _ = new_theory "explorerProg"
val _ = translation_extends "inferProg";
val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "explorerProg");
(* TODO: this is copied in many bootstrap translation files - should be in a lib? *)
fun def_of_const tm = let
val res = dest_thy_const tm handle HOL_ERR _ =>
@@ -103,6 +105,9 @@ val res7 = translate presLangTheory.clos_to_json_table_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();
@@ -7,6 +7,8 @@ val _ = new_theory "inferProg"
val _ = translation_extends "reg_allocProg";
val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "inferProg");
(* translator setup *)
val RW = REWRITE_RULE
@@ -1142,6 +1144,8 @@ val infertype_prog_side_thm = store_thm("infertype_prog_side_thm",
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();
@@ -6,6 +6,8 @@ val _ = new_theory "lexerProg"
val _ = translation_extends "to_dataProg";
val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "lexerProg");
val RW = REWRITE_RULE
val RW1 = ONCE_REWRITE_RULE
fun list_dest f tm =
@@ -108,6 +110,8 @@ val lexer_fun_side = Q.prove(`
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();
@@ -9,6 +9,8 @@ val _ = new_theory "mipsProg"
val _ = translation_extends "riscvProg";
val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "mipsProg");
val _ = add_preferred_thy "-";
val _ = add_preferred_thy "termination";
@@ -161,6 +163,8 @@ val res = translate (mips_config_def |> SIMP_RULE bool_ss [IN_INSERT,NOT_IN_EMPT
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();
@@ -7,6 +7,8 @@ val _ = new_theory "parserProg"
val _ = translation_extends "lexerProg";
val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "parserProg");
(* translator setup *)
val RW = REWRITE_RULE
@@ -226,6 +228,8 @@ val parse_prog_side_lemma = Q.store_thm("parse_prog_side_lemma",
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();
@@ -424,8 +424,6 @@ val res = translate linear_scan_reg_alloc_def;
val () = Feedback.set_trace "TheoryPP.include_docs" 0;
val _ = export_theory();
(*
TODO: update the following code (comes from the non-monadic register allocator
@@ -9,6 +9,8 @@ val _ = new_theory "riscvProg"
val _ = translation_extends "arm8Prog";
val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "riscvProg");
val _ = add_preferred_thy "-";
val _ = add_preferred_thy "termination";
@@ -172,6 +174,8 @@ val res = translate (riscv_config_def |> SIMP_RULE bool_ss [IN_INSERT,NOT_IN_EMP
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();
@@ -5,6 +5,8 @@ open preamble explorerProgTheory
val _ = new_theory"sexp_parserProg";
val _ = translation_extends "explorerProg";
val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "sexp_parserProg");
(* TODO: this is duplicated in parserProgTheory *)
val monad_unitbind_assert = Q.prove(
`!b x. monad_unitbind (assert b) x = if b then x else NONE`,
@@ -257,4 +259,6 @@ val sexpdec_alt_side = Q.prove(
\\ fs[LENGTH_EQ_NUM_compute])
|> update_precondition;
val _ = ml_translatorLib.ml_prog_update (ml_progLib.close_module NONE);
val _ = export_theory();
@@ -6,6 +6,8 @@ open basisProgTheory;
val _ = new_theory "to_dataProg"
val _ = translation_extends "basisProg";
val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "to_dataProg");
(* This is the compiler "preamble" that translates the compile functions down to dataLang *)
val RW = REWRITE_RULE
@@ -1473,6 +1475,8 @@ val bvi_to_data_compile_prog_side = Q.prove(`∀prog. bvi_to_data_compile_prog_s
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();
@@ -7,6 +7,8 @@ val _ = new_theory "to_target32Prog"
val _ = translation_extends "to_word32Prog";
val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "to_target32Prog");
val RW = REWRITE_RULE
val _ = add_preferred_thy "-";
@@ -359,6 +361,8 @@ val _ = translate (spec32 compile_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();
@@ -7,6 +7,8 @@ val _ = new_theory "to_target64Prog"
val _ = translation_extends "to_word64Prog";
val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "to_target64Prog");
val RW = REWRITE_RULE
val _ = add_preferred_thy "-";
@@ -359,6 +361,8 @@ val _ = translate (spec64 compile_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();
@@ -7,6 +7,8 @@ val _ = new_theory "to_word32Prog"
val _ = translation_extends "sexp_parserProg";
val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "to_word32Prog");
val RW = REWRITE_RULE
val _ = add_preferred_thy "-";
@@ -780,6 +782,8 @@ val res = translate (data_to_wordTheory.compile_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();
@@ -7,6 +7,8 @@ val _ = new_theory "to_word64Prog"
val _ = translation_extends "sexp_parserProg";
val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "to_word64Prog");
val RW = REWRITE_RULE
val _ = add_preferred_thy "-";
@@ -780,6 +782,8 @@ val res = translate (data_to_wordTheory.compile_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();
@@ -9,6 +9,8 @@ val _ = new_theory "x64Prog"
val _ = translation_extends "to_target64Prog";
val _ = ml_translatorLib.ml_prog_update (ml_progLib.open_module "x64Prog");
val _ = add_preferred_thy "-";
val _ = add_preferred_thy "termination";
@@ -254,6 +256,8 @@ val _ = translate (x64_config_def |> gconv)
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();

0 comments on commit 2ce1a84

Please sign in to comment.