From 286984487d515cdb9f2e02834d23c65449760ba2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Apr 2014 17:46:26 +0200
Subject: Adding an [modify] function to the tactic monad. It allows to modify
 the current state without having to use both get, bind and set.

---
 bootstrap/Monads.v | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'bootstrap')

diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index a160aaa87e..10defd0f98 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -130,7 +130,8 @@ Notation "'do' M x ':=' e 'in' u" := (bind _ M e (fun x => u)).
 
 Record State (S:Set) (T:Set->Set) := {
   set : S -> T unit;
-  get : T S
+  get : T S ;
+  modify : (S -> S) -> T unit
 }.
 
 (* spiwack: Environment and Writer are given distinct interfaces from
@@ -318,7 +319,8 @@ Section Common.
 
  Definition State : State S T := {|
    set s := (fun R k _ => k () s) : T unit  ;
-   get := fun R k s => k s s
+   get := fun R k s => k s s ;
+   modify := fun f R k s => k () (f s)
  |}.
 
  Definition lift {A} (x:T₀ A) : T A := fun R k s =>
@@ -681,6 +683,7 @@ Module Logical.
 
  Definition set (s:LogicalState) : t unit := Eval compute in freeze _ (set _ _ LogicalStateM s).
  Definition get : t LogicalState := Eval compute in get _ _ LogicalStateM.
+ Definition modify (f : LogicalState -> LogicalState) : t unit := Eval compute in freeze _ (modify _ _ LogicalStateM f).
  Definition put (m:LogicalMessageType) : t unit := Eval compute in freeze _ (put _ _ LogicalWriter m).
  Definition current : t LogicalEnvironment := Eval compute in current _ _ LogicalReader.
 
-- 
cgit v1.2.3