lib+spec+proof+tools: update for reader_option refactor

Signed-off-by: Corey Lewis <[email protected]>
seL4 · Feb 29, 2024 · cf75dfb · cf75dfb
1 parent d08f849
commit cf75dfb
Show file tree

Hide file tree

Showing 11 changed files with 11 additions and 18 deletions.
diff --git a/lib/HaskellLib_H.thy b/lib/HaskellLib_H.thy
@@ -14,8 +14,7 @@ imports
   Lib
   More_Numeral_Type
   Monads.Nondet_VCG
-  Monads.Reader_Option_Monad
-  Monads.Reader_Option_VCG
+  Monads.Nondet_Reader_Option
 begin
 
 abbreviation (input) "flip \<equiv> swp"

diff --git a/lib/NonDetMonadLemmaBucket.thy b/lib/NonDetMonadLemmaBucket.thy
@@ -19,7 +19,7 @@ imports
   Injection_Handler
   Monads.Nondet_While_Loop_Rules_Completeness
   "Word_Lib.Distinct_Prop" (* for distinct_tuple_helper *)
-  Monads.Reader_Option_VCG
+  Monads.Nondet_Reader_Option
 begin
 
 lemma distinct_tuple_helper:

diff --git a/lib/clib/Corres_UL_C.thy b/lib/clib/Corres_UL_C.thy
@@ -14,7 +14,7 @@ imports
   CParser.LemmaBucket_C
   Lib.LemmaBucket
   SIMPL_Lemmas
-  Monads.Reader_Option_VCG
+  Monads.Nondet_Reader_Option
 begin
 
 declare word_neq_0_conv [simp del]

diff --git a/proof/sep-capDL/Lookups_D.thy b/proof/sep-capDL/Lookups_D.thy
@@ -7,7 +7,7 @@
 theory Lookups_D
 imports
   "DSpec.Syscall_D"
-  "Monads.Reader_Option_ND"
+  "Monads.Nondet_Reader_Option"
 begin
 
 type_synonym 'a lookup = "cdl_state \<Rightarrow> 'a option"

diff --git a/spec/design/m-skel/AARCH64/MachineTypes.thy b/spec/design/m-skel/AARCH64/MachineTypes.thy
@@ -9,8 +9,7 @@ theory MachineTypes
 imports
   Word_Lib.WordSetup
   Monads.Nondet_Empty_Fail
-  Monads.Nondet_No_Fail
-  Monads.Reader_Option_ND
+  Monads.Nondet_Reader_Option
   Lib.HaskellLib_H
   Platform
 begin

diff --git a/spec/design/m-skel/ARM/MachineTypes.thy b/spec/design/m-skel/ARM/MachineTypes.thy
@@ -10,8 +10,7 @@ theory MachineTypes
 imports
   Word_Lib.WordSetup
   Monads.Nondet_Empty_Fail
-  Monads.Nondet_No_Fail
-  Monads.Reader_Option_ND
+  Monads.Nondet_Reader_Option
   Setup_Locale
   Platform
 begin

diff --git a/spec/design/m-skel/ARM_HYP/MachineTypes.thy b/spec/design/m-skel/ARM_HYP/MachineTypes.thy
@@ -10,8 +10,7 @@ theory MachineTypes
 imports
   Word_Lib.WordSetup
   Monads.Nondet_Empty_Fail
-  Monads.Nondet_No_Fail
-  Monads.Reader_Option_ND
+  Monads.Nondet_Reader_Option
   Setup_Locale
   Platform
 begin

diff --git a/spec/design/m-skel/RISCV64/MachineTypes.thy b/spec/design/m-skel/RISCV64/MachineTypes.thy
@@ -10,8 +10,7 @@ theory MachineTypes
 imports
   Word_Lib.WordSetup
   Monads.Nondet_Empty_Fail
-  Monads.Nondet_No_Fail
-  Monads.Reader_Option_ND
+  Monads.Nondet_Reader_Option
   Lib.HaskellLib_H
   Platform
 begin

diff --git a/spec/design/m-skel/X64/MachineTypes.thy b/spec/design/m-skel/X64/MachineTypes.thy
@@ -10,8 +10,7 @@ theory MachineTypes
 imports
   Word_Lib.WordSetup
   Monads.Nondet_Empty_Fail
-  Monads.Nondet_No_Fail
-  Monads.Reader_Option_ND
+  Monads.Nondet_Reader_Option
   Lib.HaskellLib_H
   Platform
 begin

diff --git a/tools/autocorres/NonDetMonadEx.thy b/tools/autocorres/NonDetMonadEx.thy
@@ -16,7 +16,7 @@ imports
   "Monads.Nondet_More_VCG"
   "Monads.Nondet_No_Throw"
   "Monads.Nondet_No_Fail"
-  "Monads.Reader_Option_ND"
+  "Monads.Nondet_Reader_Option"
 begin
 
 (*
@@ -276,7 +276,7 @@ lemma whileLoop_to_fold:
            (\<lambda>r. return (Q r))
            i s) = return (if P i \<le> x then fold (\<lambda>i r. (Q r)) [unat (P i) ..< unat x] i else i) s"
     (is "?LHS s = return (?RHS x) s")
-  apply (subst Reader_Option_ND.gets_the_return [symmetric])
+  apply (subst gets_the_return [symmetric])
   apply (subst gets_the_whileLoop)
   apply (rule gets_the_to_return)
   apply (subst owhile_to_fold)

diff --git a/tools/autocorres/TypeStrengthen.thy b/tools/autocorres/TypeStrengthen.thy
@@ -14,7 +14,6 @@
 theory TypeStrengthen
 imports
   L2Defs
-  "Monads.Reader_Option_ND"
   ExecConcrete
 begin