Merge remote-tracking branch 'origin/master' into zero-byte

CakeML · Jul 26, 2019 · 76201ad · 76201ad
2 parents 8ae81f9 + 6a2bd88
commit 76201ad
Show file tree

Hide file tree

Showing 15 changed files with 2,283 additions and 2,006 deletions.
diff --git a/compiler/backend/flat_elimScript.sml b/compiler/backend/flat_elimScript.sml
@@ -10,6 +10,8 @@ open preamble sptreeTheory flatLangTheory
 
 val _ = new_theory "flat_elim";
 
+val _ = set_grammar_ancestry ["flatLang", "misc"]
+val _ = temp_tight_equality();
 
 (**************************** ANALYSIS FUNCTIONS *****************************)
 

diff --git a/compiler/backend/flat_exh_matchScript.sml b/compiler/backend/flat_exh_matchScript.sml
@@ -3,10 +3,12 @@
 *)
 open preamble flatLangTheory backend_commonTheory
 
-val _ = numLib.prefer_num()
-
 val _ = new_theory"flat_exh_match"
 
+val _ = set_grammar_ancestry ["flatLang", "sptree"];
+val _ = temp_tight_equality ();
+val _ = numLib.prefer_num()
+
 val _ = tDefine "is_unconditional" `
   is_unconditional p ⇔
     case p of

diff --git a/compiler/backend/flat_reorder_matchScript.sml b/compiler/backend/flat_reorder_matchScript.sml
@@ -5,6 +5,8 @@
 open preamble flatLangTheory
 
 val _ = new_theory"flat_reorder_match";
+val _ = set_grammar_ancestry ["flatLang"];
+val _ = temp_tight_equality ();
 
 val is_const_con_def = Define`
   (is_const_con (Pcon (SOME tag) plist) = (plist = [])) /\

diff --git a/compiler/backend/flat_to_patScript.sml b/compiler/backend/flat_to_patScript.sml
@@ -5,6 +5,8 @@ open preamble flatLangTheory patLangTheory
 open backend_commonTheory
 
 val _ = new_theory"flat_to_pat"
+val _ = set_grammar_ancestry ["flatLang", "patLang", "misc"];
+val _ = temp_tight_equality ();
 val _ = patternMatchesLib.ENABLE_PMATCH_CASES();
 
 val Bool_def = Define `

diff --git a/compiler/backend/flat_uncheck_ctorsScript.sml b/compiler/backend/flat_uncheck_ctorsScript.sml
@@ -6,6 +6,8 @@ open preamble astTheory terminationTheory flatLangTheory;
 val _ = numLib.prefer_num();
 
 val _ = new_theory "flat_uncheck_ctors";
+val _ = set_grammar_ancestry ["flatLang", "lib"];
+val _ = temp_tight_equality ();
 
 val compile_pat_def = tDefine "compile_pat" `
   (compile_pat flatLang$Pany = flatLang$Pany) ∧

diff --git a/compiler/backend/proofs/backendProofScript.sml b/compiler/backend/proofs/backendProofScript.sml
@@ -370,7 +370,7 @@ Proof
     (fn g as (asl,w) =>
       let
         val (genv_c,tm) = dest_exists w
-        val tm = tm |> strip_conj |> el 10 |> strip_forall |> #2
+        val tm = tm |> strip_conj |> rev |> first is_forall |> strip_forall |> #2
         val (tms1, tm) = dest_imp tm
         val tms2 = tm |> dest_exists |> #2 |> strip_conj |> el 1
         fun get_data (tm,acc) =
@@ -411,7 +411,6 @@ Proof
   qunabbrev_tac`sem2` >>
 
   qabbrev_tac`TODO_co1 = ARB ** 0 - SUC ZERO` >>
-
   (flat_to_patProofTheory.compile_semantics
    |> Q.GEN`cc`
    |> (
@@ -601,8 +600,6 @@ Proof
         \\ simp[source_to_flatTheory.glob_alloc_def]
         \\ simp[flatPropsTheory.op_gbag_def]
         \\ drule compile_decs_elist_globals
-        \\ impl_tac >- (
-          EVAL_TAC \\ Cases \\ simp[namespaceTheory.nsLookup_def] )
         \\ rw[]
         \\ simp[LIST_TO_BAG_DISTINCT]
         \\ irule ALL_DISTINCT_MAP_INJ