Updates after moving sptree closure/reachability theories to HOL

In particular, HOL-Theorem-Prover/HOL@10ce9d0.
CakeML · Feb 15, 2021 · ea2e296 · ea2e296
1 parent b39b4fb
commit ea2e296
Show file tree

Hide file tree

Showing 15 changed files with 9 additions and 387 deletions.
diff --git a/compiler/backend/Holmakefile b/compiler/backend/Holmakefile
@@ -2,7 +2,7 @@ INCLUDES = $(HOLDIR)/examples/machine-code/multiword\
 					 $(CAKEMLDIR)/misc $(CAKEMLDIR)/semantics $(CAKEMLDIR)/semantics/proofs\
 					 $(CAKEMLDIR)/basis/pure\
 					 pattern_matching\
-					 ../encoders/asm reg_alloc reachability
+					 ../encoders/asm reg_alloc $(HOLDIR)/examples/algorithms
 
 all: $(DEFAULT_TARGETS) README.md
 .PHONY: all

diff --git a/compiler/backend/flat_elimScript.sml b/compiler/backend/flat_elimScript.sml
@@ -6,11 +6,11 @@
   Removes unreachable globals from the code.
 *)
 
-open preamble sptreeTheory flatLangTheory reachable_sptTheory
+open preamble sptreeTheory flatLangTheory spt_closureTheory
 
 val _ = new_theory "flat_elim";
 
-val _ = set_grammar_ancestry ["reachable_spt", "flatLang", "misc"]
+val _ = set_grammar_ancestry ["spt_closure", "flatLang", "misc"]
 val _ = temp_tight_equality();
 
 (**************************** ANALYSIS FUNCTIONS *****************************)

diff --git a/compiler/backend/proofs/Holmakefile b/compiler/backend/proofs/Holmakefile
@@ -3,7 +3,7 @@ INCLUDES = $(HOLDIR)/examples/machine-code/multiword\
 					 $(CAKEMLDIR)/misc $(CAKEMLDIR)/semantics $(CAKEMLDIR)/semantics/proofs\
 					 ..  ../semantics ../../encoders/asm ../gc\
 					 ../reg_alloc ../reg_alloc/proofs\
-					 ../reachability ../reachability/proofs
+					 $(HOLDIR)/examples/algorithms
 
 all: $(DEFAULT_TARGETS) README.md
 .PHONY: all

diff --git a/compiler/backend/proofs/flat_elimProofScript.sml b/compiler/backend/proofs/flat_elimProofScript.sml
@@ -2,16 +2,15 @@
   Correctness proof for flatLang dead code elimination
 *)
 open preamble sptreeTheory flatLangTheory flat_elimTheory
-     flatSemTheory flatPropsTheory reachable_sptTheory
-     reachable_sptProofTheory
+     flatSemTheory flatPropsTheory spt_closureTheory
 
 val _ = temp_delsimps ["lift_disj_eq", "lift_imp_disj"]
 
 val _ = new_theory "flat_elimProof";
 
 val grammar_ancestry =
   ["flat_elim", "flatSem", "flatLang", "flatProps",
-   "reachable_spt",  "misc", "ffi", "sptree"];
+   "spt_closure",  "misc", "ffi", "sptree"];
 
 val _ = set_grammar_ancestry grammar_ancestry;
 

diff --git a/compiler/backend/proofs/word_elimProofScript.sml b/compiler/backend/proofs/word_elimProofScript.sml
@@ -3,12 +3,11 @@
 *)
 
 open preamble wordLangTheory
-     word_elimTheory wordSemTheory wordPropsTheory
-     reachable_sptTheory reachable_sptProofTheory
+     word_elimTheory wordSemTheory wordPropsTheory spt_closureTheory
 
 val _ = new_theory "word_elimProof";
 val _ = set_grammar_ancestry
-  ["wordLang", "word_elim", "wordSem", "wordProps", "reachable_spt"];
+  ["wordLang", "word_elim", "wordSem", "wordProps", "spt_closure"];
 val _ = Parse.hide"mem";
 val _ = Parse.bring_to_front_overload"domain"{Thy="sptree",Name="domain"};
 

diff --git a/compiler/backend/reachability/Holmakefile b/compiler/backend/reachability/Holmakefile
diff --git a/compiler/backend/reachability/README.md b/compiler/backend/reachability/README.md
diff --git a/compiler/backend/reachability/proofs/Holmakefile b/compiler/backend/reachability/proofs/Holmakefile
diff --git a/compiler/backend/reachability/proofs/README.md b/compiler/backend/reachability/proofs/README.md
diff --git a/compiler/backend/reachability/proofs/reachable_sptProofScript.sml b/compiler/backend/reachability/proofs/reachable_sptProofScript.sml
diff --git a/compiler/backend/reachability/proofs/readmePrefix b/compiler/backend/reachability/proofs/readmePrefix
diff --git a/compiler/backend/reachability/reachable_sptScript.sml b/compiler/backend/reachability/reachable_sptScript.sml
diff --git a/compiler/backend/reachability/readmePrefix b/compiler/backend/reachability/readmePrefix
diff --git a/compiler/backend/word_elimScript.sml b/compiler/backend/word_elimScript.sml
@@ -7,7 +7,7 @@
   Removes unreachable functions from the code.
 *)
 
-open preamble sptreeTheory reachable_sptTheory wordLangTheory
+open preamble sptreeTheory spt_closureTheory wordLangTheory
 
 val _ = new_theory "word_elim";