lib: support for Haskell Reader monad constructs

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>

lib/HaskellLib_H.thy

@@ -33,6 +33,12 @@ definition
   runState :: "('s, 'a) nondet_monad \<Rightarrow> 's \<Rightarrow> ('a \<times> 's)" where
  "runState f s \<equiv> THE x. x \<in> fst (f s)"
 
+definition
+  "runReaderT \<equiv> id"
+
+abbreviation (input)
+  "getsJust \<equiv> gets_the"
+
 definition
   sassert :: "bool \<Rightarrow> 'a \<Rightarrow> 'a" where
  "sassert P \<equiv> if P then id else (\<lambda>x. undefined)"

lib/Monad_WP/OptionMonad.thy

@@ -91,10 +91,23 @@ definition
 definition
   "oassert P \<equiv> if P then oreturn () else ofail"
 
-definition oapply :: "'a \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option"
-  where
+definition
+  "oassert_opt r \<equiv> case r of None \<Rightarrow> ofail | Some x \<Rightarrow> oreturn x"
+
+definition oapply :: "'a \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> 'b option" where
   "oapply x \<equiv> \<lambda>s. s x"
 
+definition oliftM :: "('a \<Rightarrow> 'b) \<Rightarrow> ('s,'a) lookup \<Rightarrow> ('s,'b) lookup" where
+  "oliftM f m \<equiv> do { x \<leftarrow> m; oreturn (f x) }"
+
+(* Reader monad interface: *)
+abbreviation (input)
+  "ask \<equiv> Some"
+
+definition
+  "asks f = do { v <- ask; oreturn (f v) }"
+
+
 text \<open>
   If the result can be an exception.
   Corresponding bindE would be analogous to lifting in NonDetMonad.