Add {get,set,update}_state

MetaCoq · Apr 24, 2023 · b33c544 · b33c544
1 parent de0cc6b
commit b33c544
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/utils/theories/monad_utils.v b/utils/theories/monad_utils.v
@@ -69,13 +69,21 @@ Import MCMonadNotation.
 
 Open Scope monad.
 
+(* state is underneath the other monad *)
 Definition StateT S M T := S -> M (T * S)%type.
 Definition StateT_Monad {S T} {TM : Monad T} : Monad (StateT S T) :=
   {| ret A a st := ret (a, st) ;
      bind A B m f st := '(m, st) <- m st;; f m st
   |}.
 #[export] Hint Extern 1 (Monad (StateT ?S ?T)) => simple apply (@StateT_Monad S T) : typeclass_instances.
 
+Definition get_state {S T} {TM : Monad T} : StateT S T S
+  := fun s => ret (s, s).
+Definition update_state {S T} {TM : Monad T} (f : S -> S) : StateT S T unit
+  := fun s => ret (tt, f s).
+Definition set_state {S T} {TM : Monad T} (s : S) : StateT S T unit
+  := update_state (fun _ => s).
+
 Section MapOpt.
   Context {A} {B} (f : A -> option B).