lib/monads: rename OptionMonad to Reader_Option_Monad

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

lib/Monads/README.md

@@ -34,6 +34,6 @@ in weakest-precondition style.
 
 [l4v]: https://github.com/seL4/l4v/
 [nondet]: ./NonDetMonad.thy
-[option]: ./OptionMonad.thy
+[option]: ./Reader_Option_Monad.thy
 [trace]: ./TraceMonad.thy
 [AutoCorres]: ../../tools/autocorres/

lib/Monads/ROOT

@@ -20,15 +20,15 @@ session Monads (lib) = HOL +
   theories
     WhileLoopRules
     TraceMonad
-    OptionMonadND
-    OptionMonadWP
+    Reader_Option_ND
+    Reader_Option_VCG
     Strengthen_Demo
     TraceMonadLemmas
     Datatype_Schematic
     WhileLoopRulesCompleteness
     Strengthen
     Strengthen_Setup
-    OptionMonad
+    Reader_Option_Monad
     TraceMonadVCG
     In_Monad
     NonDetMonadVCG

lib/Monads/Reader_Option_Monad.thy

@@ -11,7 +11,7 @@
  *     Option monad while loop formalisation.
  *)
 
-theory OptionMonad (* FIXME: this is really a Reader_Option_Monad *)
+theory Reader_Option_Monad
   imports
     Monad_Lib
     Fun_Pred_Syntax

lib/Monads/Reader_Option_ND.thy

@@ -4,12 +4,12 @@
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
-(* Option monad syntax plus the connection between the option monad and the nondet monad *)
+(* Reader option monad syntax plus the connection between the reader option monad and the nondet monad *)
 
-theory OptionMonadND
+theory Reader_Option_ND
 imports
   NonDetMonadLemmas
-  OptionMonad
+  Reader_Option_Monad
 begin
 
 (* FIXME: remove this syntax, standardise on do {..} instead *)

lib/Monads/Reader_Option_VCG.thy

@@ -5,14 +5,14 @@
  *)
 
 (*
-Hoare reasoning and WP (weakest-precondition) generator rules for the option monad.
+Hoare reasoning and WP (weakest-precondition) generator rules for the reader option monad.
 
 This list is almost certainly incomplete; add rules here as they are needed.
 *)
 
-theory OptionMonadWP
+theory Reader_Option_VCG
 imports
-  OptionMonadND
+  Reader_Option_ND
   WP
   No_Fail
 begin