Get some files to build using developers/fix_scripts.sml

There are still many that don't build.
CakeML · Jan 22, 2021 · 73252d5 · 73252d5
1 parent 4762e6f
commit 73252d5
Show file tree

Hide file tree

Showing 33 changed files with 61 additions and 1 deletion.
diff --git a/characteristic/cfScript.sml b/characteristic/cfScript.sml
@@ -9,6 +9,8 @@ open cfHeapsBaseTheory cfHeapsTheory cfHeapsBaseLib cfStoreTheory
 open cfNormaliseTheory cfAppTheory
 open cfTacticsBaseLib
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory "cf"
 
 val _ = set_grammar_ancestry

diff --git a/characteristic/cfStoreScript.sml b/characteristic/cfStoreScript.sml
@@ -6,6 +6,8 @@ open set_sepTheory helperLib ConseqConv
 open semanticPrimitivesTheory ml_translatorTheory
 open cfHeapsTheory cfHeapsBaseLib
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory "cfStore"
 
 

diff --git a/compiler/backend/gc/copying_gcScript.sml b/compiler/backend/gc/copying_gcScript.sml
@@ -3,6 +3,8 @@
 *)
 open preamble gc_sharedTheory wordsTheory wordsLib integer_wordTheory;
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory "copying_gc";
 
 val _ = ParseExtras.temp_loose_equality();

diff --git a/compiler/backend/gc/gen_gcScript.sml b/compiler/backend/gc/gen_gcScript.sml
@@ -5,6 +5,8 @@ open preamble wordsTheory wordsLib integer_wordTheory gc_sharedTheory;
 
 val _ = temp_delsimps ["NORMEQ_CONV"]
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory "gen_gc";
 
 val _ = ParseExtras.temp_loose_equality();

diff --git a/compiler/backend/gc/gen_gc_partialScript.sml b/compiler/backend/gc/gen_gc_partialScript.sml
@@ -3,6 +3,8 @@
 *)
 open preamble wordsTheory wordsLib integer_wordTheory gc_sharedTheory gen_gcTheory;
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory "gen_gc_partial";
 
 val _ = ParseExtras.temp_loose_equality();

diff --git a/compiler/backend/proofs/bvl_inlineProofScript.sml b/compiler/backend/proofs/bvl_inlineProofScript.sml
@@ -7,6 +7,8 @@ open preamble backendPropsTheory
      bvl_inlineTheory
 local open bvl_handleProofTheory in end
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory"bvl_inlineProof";
 
 val _ = set_grammar_ancestry [ "bvlSem", "bvlProps", "bvl_inline" ];

diff --git a/compiler/backend/proofs/clos_callProofScript.sml b/compiler/backend/proofs/clos_callProofScript.sml
@@ -6,6 +6,8 @@ open preamble backendPropsTheory match_goal
      closSemTheory closPropsTheory
      clos_callTheory db_varsTheory
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory"clos_callProof";
 
 val _ = temp_delsimps ["NORMEQ_CONV"]

diff --git a/compiler/backend/proofs/clos_knownProofScript.sml b/compiler/backend/proofs/clos_knownProofScript.sml
@@ -7,6 +7,8 @@ open closPropsTheory clos_knownTheory clos_knownPropsTheory closSemTheory
      closLangTheory db_varsTheory backendPropsTheory
 local open clos_letopProofTheory clos_ticksProofTheory clos_fvsProofTheory in end
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory "clos_knownProof";
 val _ = diminish_srw_ss ["ABBREV"]
 val _ = set_trace "BasicProvers.var_eq_old" 1

diff --git a/compiler/backend/proofs/clos_to_bvlProofScript.sml b/compiler/backend/proofs/clos_to_bvlProofScript.sml
@@ -23,6 +23,7 @@ val _ = new_theory"clos_to_bvlProof";
 
 val _ = temp_delsimps ["NORMEQ_CONV"]
 val _ = diminish_srw_ss ["ABBREV"]
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
 val _ = set_trace "BasicProvers.var_eq_old" 1
 
 val _ = set_grammar_ancestry

diff --git a/compiler/backend/proofs/data_liveProofScript.sml b/compiler/backend/proofs/data_liveProofScript.sml
@@ -3,6 +3,8 @@
 *)
 open preamble data_liveTheory dataSemTheory dataPropsTheory;
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory"data_liveProof";
 
 val _ = temp_bring_to_front_overload"get_vars"{Name="get_vars",Thy="dataSem"};

diff --git a/compiler/backend/proofs/flat_elimProofScript.sml b/compiler/backend/proofs/flat_elimProofScript.sml
@@ -5,6 +5,8 @@ open preamble sptreeTheory flatLangTheory flat_elimTheory
      flatSemTheory flatPropsTheory reachable_sptTheory
      reachable_sptProofTheory
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory "flat_elimProof";
 
 val grammar_ancestry =

diff --git a/compiler/backend/proofs/flat_patternProofScript.sml b/compiler/backend/proofs/flat_patternProofScript.sml
@@ -8,6 +8,8 @@ open preamble flat_patternTheory
      pattern_semanticsTheory
 local open bagSimps in end
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory "flat_patternProof"
 
 val _ = set_grammar_ancestry ["flat_pattern",

diff --git a/compiler/backend/proofs/lab_filterProofScript.sml b/compiler/backend/proofs/lab_filterProofScript.sml
@@ -3,6 +3,8 @@
 *)
 open preamble labSemTheory labPropsTheory lab_filterTheory;
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = temp_delsimps ["NORMEQ_CONV"]
 
 val _ = new_theory "lab_filterProof";

diff --git a/compiler/backend/proofs/source_to_flatProofScript.sml b/compiler/backend/proofs/source_to_flatProofScript.sml
@@ -12,6 +12,7 @@ local open flat_elimProofTheory flat_patternProofTheory in end
 val _ = new_theory "source_to_flatProof";
 val _ = temp_delsimps ["NORMEQ_CONV"]
 val _ = diminish_srw_ss ["ABBREV"]
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
 val _ = set_trace "BasicProvers.var_eq_old" 1
 
 val grammar_ancestry =

diff --git a/compiler/backend/proofs/stack_removeProofScript.sml b/compiler/backend/proofs/stack_removeProofScript.sml
@@ -15,6 +15,7 @@ val _ = new_theory"stack_removeProof";
 
 val _ = temp_delsimps ["NORMEQ_CONV"]
 val _ = diminish_srw_ss ["ABBREV"]
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
 val _ = set_trace "BasicProvers.var_eq_old" 1
 
 val word_shift_def = backend_commonTheory.word_shift_def

diff --git a/compiler/backend/proofs/word_gcFunctionsScript.sml b/compiler/backend/proofs/word_gcFunctionsScript.sml
@@ -5,6 +5,8 @@ open preamble
 
 open wordSemTheory data_to_wordTheory gc_sharedTheory
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory "word_gcFunctions"
 
 val shift_def = backend_commonTheory.word_shift_def;

diff --git a/compiler/backend/proofs/word_instProofScript.sml b/compiler/backend/proofs/word_instProofScript.sml
@@ -7,6 +7,8 @@ open preamble
 
 val _ = temp_delsimps ["NORMEQ_CONV"]
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory "word_instProof";
 
 val _ = set_grammar_ancestry ["wordLang", "wordProps", "word_inst", "wordSem"];

diff --git a/compiler/backend/proofs/word_to_stackProofScript.sml b/compiler/backend/proofs/word_to_stackProofScript.sml
@@ -11,6 +11,7 @@ val _ = new_theory "word_to_stackProof";
 
 val _ = temp_delsimps ["NORMEQ_CONV"]
 val _ = diminish_srw_ss ["ABBREV"]
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
 val _ = set_trace "BasicProvers.var_eq_old" 1
 
 val _ = set_grammar_ancestry [

diff --git a/compiler/backend/reg_alloc/proofs/linear_scanProofScript.sml b/compiler/backend/reg_alloc/proofs/linear_scanProofScript.sml
@@ -4,6 +4,8 @@
 open preamble sptreeTheory reg_allocTheory linear_scanTheory reg_allocProofTheory libTheory
 open ml_monadBaseTheory ml_monadBaseLib;
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory "linear_scanProof"
 
 val _ = disable_tyabbrev_printing "type_ident"

diff --git a/compiler/backend/reg_alloc/proofs/reg_allocProofScript.sml b/compiler/backend/reg_alloc/proofs/reg_allocProofScript.sml
@@ -5,6 +5,8 @@ open preamble state_transformerTheory reg_allocTheory
 open sortingTheory;
 open ml_monadBaseTheory ml_monadBaseLib;
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory "reg_allocProof"
 
 val _ = ParseExtras.temp_tight_equality();

diff --git a/compiler/backend/semantics/bviPropsScript.sml b/compiler/backend/semantics/bviPropsScript.sml
@@ -4,6 +4,8 @@
 open preamble bviSemTheory;
 local open bvlPropsTheory in end;
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory"bviProps";
 
 Theorem initial_state_simp[simp]:

diff --git a/compiler/backend/semantics/bviSemScript.sml b/compiler/backend/semantics/bviSemScript.sml
@@ -4,6 +4,8 @@
 open preamble bviTheory;
 local open backend_commonTheory bvlSemTheory in end;
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory"bviSem";
 
 Overload num_stubs[local] = ``bvl_num_stubs``

diff --git a/compiler/backend/semantics/bvlPropsScript.sml b/compiler/backend/semantics/bvlPropsScript.sml
@@ -6,6 +6,8 @@ open closPropsTheory backend_commonTheory;
 
 val _ = temp_delsimps ["NORMEQ_CONV"]
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory"bvlProps";
 
 val s = ``(s:('c,'ffi) bvlSem$state)``

diff --git a/compiler/backend/semantics/closPropsScript.sml b/compiler/backend/semantics/closPropsScript.sml
@@ -3,6 +3,8 @@
 *)
 open preamble closLangTheory closSemTheory backendPropsTheory
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory"closProps"
 
 Theorem with_same_clock[simp]:

diff --git a/compiler/backend/semantics/flatPropsScript.sml b/compiler/backend/semantics/flatPropsScript.sml
@@ -7,6 +7,8 @@ local
        evaluatePropsTheory
 in end
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory"flatProps"
 val _ = set_grammar_ancestry ["flatLang", "flatSem"];
 val _ = temp_tight_equality ();

diff --git a/compiler/backend/semantics/flatSemScript.sml b/compiler/backend/semantics/flatSemScript.sml
@@ -4,6 +4,8 @@
 open preamble flatLangTheory;
 open semanticPrimitivesPropsTheory;
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory "flatSem";
 
 (* The values of flatLang differ from source semantic values in that

diff --git a/compiler/inference/proofs/infer_eSoundScript.sml b/compiler/inference/proofs/infer_eSoundScript.sml
@@ -11,6 +11,8 @@ open namespacePropsTheory;
 local open typeSoundInvariantsTheory in
 end
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory "infer_eSound";
 
 

diff --git a/compiler/parsing/fromSexpScript.sml b/compiler/parsing/fromSexpScript.sml
@@ -9,6 +9,8 @@
 open preamble match_goal
 open simpleSexpTheory astTheory
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory "fromSexp";
 val _ = set_grammar_ancestry ["simpleSexp", "ast", "location","fpSem"]
 val _ = option_monadsyntax.temp_add_option_monadsyntax()

diff --git a/compiler/parsing/proofs/pegCompleteScript.sml b/compiler/parsing/proofs/pegCompleteScript.sml
@@ -6,6 +6,8 @@ open preamble
      pegTheory grammarTheory pegSoundTheory
      gramTheory gramPropsTheory cmlPEGTheory
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory "pegComplete"
 val _ = set_grammar_ancestry ["pegSound"]
 

diff --git a/developers/fix_scripts.sml b/developers/fix_scripts.sml
@@ -5,7 +5,7 @@
   the dir that needs fixing; it will recurse into INCLUDES dirs.
 *)
 
-val new_str = "val _ = temp_delsimps [\"NORMEQ_CONV\"]\n\n"
+val new_str = "val _ = temp_delsimps [\"lift_disj_eq\", \"lift_imp_disj\"]\n\n"
 
 fun mem x [] = false | mem x (y::ys) = x = y orelse mem x ys;
 fun fst (x,y) = x

diff --git a/semantics/proofs/typeSoundScript.sml b/semantics/proofs/typeSoundScript.sml
@@ -13,6 +13,8 @@ local open primSemEnvTheory in end;
 
 val _ = temp_delsimps ["NORMEQ_CONV"]
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory "typeSound";
 
 val type_num_defs = LIST_CONJ [

diff --git a/semantics/proofs/typeSysPropsScript.sml b/semantics/proofs/typeSysPropsScript.sml
@@ -8,6 +8,8 @@ open astPropsTheory;
 open namespacePropsTheory;
 local open semanticPrimitivesPropsTheory in end
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory "typeSysProps";
 
 val find_recfun_def = semanticPrimitivesTheory.find_recfun_def;

diff --git a/translator/ml_progScript.sml b/translator/ml_progScript.sml
@@ -11,6 +11,8 @@ open terminationTheory;
 open namespaceTheory;
 open alist_treeTheory;
 
+val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
+
 val _ = new_theory "ml_prog";
 
 (* --- env operators --- *)