Move def of decs_allowed into own theory for better deps

Author: myreen

compiler/repl/README.md

@@ -6,6 +6,10 @@ The REPL type checks and modifies the decs given as input. This file
 defines the function that implements this and proves that the
 function will only produce type checked and allowed declarations.
 
+[repl_decs_allowedScript.sml](repl_decs_allowedScript.sml):
+The REPL puts some restrictions on what decs are acceptable as user input.
+This file defines what those restrictions are.
+
 [repl_init_envProgScript.sml](repl_init_envProgScript.sml):
 This file partially instantiates the eval_state and inserts a Denv declaration.
 

compiler/repl/repl_check_and_tweakScript.sml

@@ -5,18 +5,12 @@
 *)
 open preamble
 open semanticsPropsTheory evaluateTheory semanticPrimitivesTheory
-open inferTheory compilerTheory candle_prover_invTheory
+open inferTheory compilerTheory repl_decs_allowedTheory
 
 val _ = Parse.hide "types"
 
 val _ = new_theory "repl_check_and_tweak";
 
-val _ = patternMatchesLib.ENABLE_PMATCH_CASES();
-
-Definition decs_allowed_def:
-  decs_allowed (decs:ast$dec list) = EVERY candle_prover_inv$safe_dec decs
-End
-
 val read_next_dec =
   “[Dlet (Locs UNKNOWNpt UNKNOWNpt) Pany
        (App Opapp
@@ -26,7 +20,7 @@ val read_next_dec =
 Definition check_and_tweak_def:
   check_and_tweak (decs, types, input_str) =
     let all_decs = decs ++ ^read_next_dec in
-      dtcase infertype_prog types all_decs of
+      case infertype_prog types all_decs of
       | Success new_types =>
           if decs_allowed all_decs then INR (all_decs, new_types)
           else INL (strlit "ERROR: input contains reserved constructor/FFI names")
@@ -43,28 +37,4 @@ Proof
   \\ fs [decs_allowed_def]
 QED
 
-(* pmatch lemmas *)
-
-Triviality safe_exp_pmatch_lemma:
-  safe_exp =
-     every_exp $ λx. case x of
-                     | Con opt xs => (dtcase opt of
-                                      | SOME id => let n = id_to_n id in n ∉ kernel_ctors
-                                      | NONE => T)
-                     | App op xs' => op ≠ FFI kernel_ffi
-                     | _ => T
-Proof
-  CONV_TAC(ONCE_DEPTH_CONV patternMatchesLib.PMATCH_ELIM_CONV)
-  \\ rw [safe_exp_def,FUN_EQ_THM]
-  \\ AP_THM_TAC \\ AP_TERM_TAC
-  \\ rw [safe_exp_def,FUN_EQ_THM]
-  \\ CASE_TAC \\ fs []
-  \\ CASE_TAC \\ fs []
-QED
-
-Theorem safe_exp_pmatch = safe_exp_pmatch_lemma
-  |> SIMP_RULE std_ss [candle_kernel_valsTheory.kernel_ctors_def,
-                       candle_kernel_valsTheory.kernel_ffi_def,
-                       IN_UNION,IN_INSERT,NOT_IN_EMPTY,GSYM CONJ_ASSOC]
-
 val _ = export_theory();

compiler/repl/repl_decs_allowedScript.sml

@@ -0,0 +1,45 @@
+(*
+  The REPL puts some restrictions on what decs are acceptable as user input.
+  This file defines what those restrictions are.
+*)
+open preamble
+open semanticsPropsTheory evaluateTheory semanticPrimitivesTheory
+open candle_prover_invTheory
+
+val _ = Parse.hide "types"
+
+val _ = new_theory "repl_decs_allowed";
+
+val _ = patternMatchesLib.ENABLE_PMATCH_CASES();
+
+(* definition *)
+
+Definition decs_allowed_def:
+  decs_allowed (decs:ast$dec list) = EVERY candle_prover_inv$safe_dec decs
+End
+
+(* pmatch lemmas *)
+
+Triviality safe_exp_pmatch_lemma:
+  safe_exp =
+     every_exp $ λx. case x of
+                     | Con opt xs => (dtcase opt of
+                                      | SOME id => let n = id_to_n id in n ∉ kernel_ctors
+                                      | NONE => T)
+                     | App op xs' => op ≠ FFI kernel_ffi
+                     | _ => T
+Proof
+  CONV_TAC(ONCE_DEPTH_CONV patternMatchesLib.PMATCH_ELIM_CONV)
+  \\ rw [safe_exp_def,FUN_EQ_THM]
+  \\ AP_THM_TAC \\ AP_TERM_TAC
+  \\ rw [safe_exp_def,FUN_EQ_THM]
+  \\ CASE_TAC \\ fs []
+  \\ CASE_TAC \\ fs []
+QED
+
+Theorem safe_exp_pmatch = safe_exp_pmatch_lemma
+  |> SIMP_RULE std_ss [candle_kernel_valsTheory.kernel_ctors_def,
+                       candle_kernel_valsTheory.kernel_ffi_def,
+                       IN_UNION,IN_INSERT,NOT_IN_EMPTY,GSYM CONJ_ASSOC]
+
+val _ = export_theory();