State monad implemented in CPS.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16995 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 201 insertions, 129 deletions

diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index 7164c5e69..2403dde9a 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -261,49 +261,49 @@ Module IO.
 End IO.
 
 Module State.
-(** State monad transformer, adapted from Haskell' StateT *)
+(** The impredicative encoding of the usual State predicate
+    transformer (StateT in Haskell). The impredicative encoding allows
+    to avoid creating blocks (val,state) at each bind. *)
 
 Section Common.
 
  Variables (S:Set) (T₀:Set->Set) (M:Monad T₀).
 
- Definition T (A:Set):= S -> T₀ (A*S)%type.
+ Definition T (A:Set):= forall R:Set, (A -> S -> T₀ R) -> S -> T₀ R.
 
  Definition F : Monad T := {|
-   ret A x s := ret _ M (x,s);
-   bind A B x k s :=
-            do M x := x s in
-            let '(x,s) := x in
-            k x s;
-   ignore A x s :=
-              do M x := x s in
-              let '(_,s) := x in
-              ret _ M ((),s);
-   seq A x k s :=
-           do M x := x s in
-           let '((),s) := x in
-           k s
+   ret A x := fun R k s => k x s ;
+   bind A B x f := fun R k s =>
+            x R (fun a s' => f a R k s') s ;
+   ignore A x := fun R k s =>
+            x R (fun _ s' => k tt s') s ;
+   seq A x y := fun R k s =>
+           x R (fun _ s' => y R k s') s
  |}.
 
  Definition State : State S T := {|
-   set := (fun (x s:S) => ret _ M ((),x)) : S -> T unit ;
-   get := fun (s:S) => ret _ M (s,s)
+   set s := (fun R k _ => k () s) : T unit  ;
+   get := fun R k s => k s s
  |}.
 
- Definition lift : forall {A}, T₀ A -> T A :=  fun _ x s =>
+ Definition lift {A} (x:T₀ A) : T A := fun R k s =>
    do M x := x in
-   ret _ M (x,s)
+   k x s
  .
 
- Definition run : forall {A}, T A -> S -> T₀ (A*S) := fun _ x => x.
- Definition reflect : forall {A:Set}, (S -> T₀ (A*S)) -> T A := fun _ x => x.
+ Definition run {A} (x:T A) (s:S) : T₀ (A*S) := x _ (fun a s' => ret _ M (a,s')) s.
+ Definition reflect {A:Set} (x:S -> T₀ (A*S)) : T A := fun R k s =>
+   do M x' := x s in
+   let '(a,s') := x' in
+   k a s'
+ .
 
  Variable (L:Logic T₀).
 
 
  Definition Logic : Logic T := {|
    zero A e := lift (zero _ L e);
-   plus A x y s := plus _ L (x s) (fun e => y e s)
+   plus A x y := fun R k s => plus _ L (x R k s) (fun e => y e R k s)
  |}.
 
 End Common.
@@ -534,8 +534,8 @@ Definition LogicalType := State.T LogicalState (Environment.T LogicalEnvironment
 Definition LogicalMonadBase := Logic.F NonLogicalType.
 Definition LogicalMonadWriter := Writer.F _ LogicalMessage _ LogicalMonadBase.
 Definition LogicalMonadEnv := Environment.F LogicalEnvironment _ LogicalMonadWriter.
-Definition LogicalMonad : Monad LogicalType := State.F LogicalState _ LogicalMonadEnv.
-Definition LogicalStateM : State LogicalState LogicalType := State.State LogicalState _ LogicalMonadEnv.
+Definition LogicalMonad : Monad LogicalType := State.F LogicalState _.
+Definition LogicalStateM : State LogicalState LogicalType := State.State LogicalState _.
 Definition LogicalReader : Environment LogicalEnvironment _ := Environment.Environment LogicalEnvironment _ LogicalMonadWriter.
 Definition LogicalWriter : Writer LogicalMessageType  _ := Writer.Writer LogicalMessageType _ (Logic.F NonLogicalType).
 Definition LogicalLogic : Logic LogicalType := State.Logic _ _ LogicalMonadEnv (Environment.Logic _ _ (Writer.Logic _ LogicalMessage _ LogicalMonadBase (Logic.Logic _))).
@@ -545,16 +545,20 @@ Definition LogicalLogic : Logic LogicalType := State.Logic _ _ LogicalMonadEnv (
    [split0]. It reifies the monad transformer stack until we can read
    back a more syntactic form, then reflects the result back. *)
 Definition split0 {a:Set} (x:LogicalType a) : LogicalType ((a*(Exception -> LogicalType a))+Exception) :=
-  State.reflect _ _ (fun s =>
+  State.reflect _ _ LogicalMonadEnv (fun s =>
   Environment.reflect _ _ (fun e =>
   Writer.reflect _ _ (
   Logic.lift _ NonLogicalMonad (
     do NonLogicalMonad x' :=
-        Logic.reify _ NonLogicalMonad (Writer.run _ _ (Environment.run _ _ (State.run _ _ x s) e)) in
+        Logic.reify _ NonLogicalMonad (Writer.run _ _ (Environment.run _ _ (State.run _ _ LogicalMonadEnv x s) e)) in
     match x' with
     | inr exc => ret _ NonLogicalMonad ((inr exc),s, Monoid.zero _ LogicalMessage)
     | inl (a',s',m',y) =>
-      let y' exc _ _ := y exc in
+      let y' exc :=
+          State.reflect _ _ LogicalMonadEnv (fun _ =>
+          Environment.reflect _ _ (fun _ =>
+          Writer.reflect _ _ (y exc)))
+      in
       ret _ NonLogicalMonad (inl (a',y'),s',m')
     end
   ))))
@@ -645,7 +649,7 @@ split _ LogicalLogic x).
  Extraction Implicit lift [a].
 
  Definition run {a:Set} (x:t a) (e:LogicalEnvironment) (s:LogicalState) : NonLogical.t ((a*LogicalState)*LogicalMessageType) := Eval compute in
-  Logic.run _ NonLogicalMonad _ NonLogicalIO (Writer.run _ _ (Environment.run _ _ (State.run _ _ x s) e))
+  Logic.run _ NonLogicalMonad _ NonLogicalIO (Writer.run _ _ (Environment.run _ _ (State.run _ _ LogicalMonadEnv x s) e))
  .
  Extraction Implicit run [a].
 
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index 7d19f5ad2..48201d39e 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -182,151 +182,198 @@ module NonLogical =
 module Logical = 
  struct 
   type 'a t =
-    proofview -> Environ.env -> __ ->
-    ((('a*proofview)*bool) -> (exn -> __
+    __ -> ('a -> proofview -> Environ.env ->
+    __ -> ((__*bool) -> (exn -> __
     IOBase.coq_T) -> __ IOBase.coq_T) -> (exn
-    -> __ IOBase.coq_T) -> __ IOBase.coq_T
+    -> __ IOBase.coq_T) -> __ IOBase.coq_T)
+    -> proofview -> Environ.env -> __ ->
+    ((__*bool) -> (exn -> __ IOBase.coq_T) ->
+    __ IOBase.coq_T) -> (exn -> __
+    IOBase.coq_T) -> __ IOBase.coq_T
   
   (** val ret :
-      'a1 -> proofview -> Environ.env -> __
-      -> ((('a1*proofview)*bool) -> (exn ->
-      'a2 IOBase.coq_T) -> 'a2 IOBase.coq_T)
-      -> (exn -> 'a2 IOBase.coq_T) -> 'a2
+      'a1 -> __ -> ('a1 -> proofview ->
+      Environ.env -> __ -> (('a2*bool) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      proofview -> Environ.env -> __ ->
+      (('a2*bool) -> (exn -> 'a3
+      IOBase.coq_T) -> 'a3 IOBase.coq_T) ->
+      (exn -> 'a3 IOBase.coq_T) -> 'a3
       IOBase.coq_T **)
   
   let ret x =
-    (); (fun s e _ sk fk ->
-      sk ((x,s),true) fk)
+    (); (fun _ k s -> Obj.magic k x s)
   
   (** val bind :
-      'a1 t -> ('a1 -> 'a2 t) -> proofview ->
-      Environ.env -> __ ->
-      ((('a2*proofview)*bool) -> (exn -> 'a3
-      IOBase.coq_T) -> 'a3 IOBase.coq_T) ->
-      (exn -> 'a3 IOBase.coq_T) -> 'a3
+      'a1 t -> ('a1 -> 'a2 t) -> __ -> ('a2
+      -> proofview -> Environ.env -> __ ->
+      (('a3*bool) -> (exn -> __ IOBase.coq_T)
+      -> __ IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      proofview -> Environ.env -> __ ->
+      (('a3*bool) -> (exn -> 'a4
+      IOBase.coq_T) -> 'a4 IOBase.coq_T) ->
+      (exn -> 'a4 IOBase.coq_T) -> 'a4
       IOBase.coq_T **)
   
   let bind x k =
-    (); (fun s e _ sk fk ->
-      Obj.magic x s e __ (fun a fk0 ->
-        let x0,c = a in
-        let x1,s0 = x0 in
-        Obj.magic k x1 s0 e __ (fun a0 fk1 ->
-          let y,c' = a0 in
-          sk (y,(if c then c' else false))
-            fk1) fk0) fk)
+    (); (fun _ k0 s ->
+      Obj.magic x __ (fun a s' ->
+        Obj.magic k a __ k0 s') s)
   
   (** val ignore :
-      'a1 t -> proofview -> Environ.env -> __
-      -> (((unit*proofview)*bool) -> (exn ->
-      'a2 IOBase.coq_T) -> 'a2 IOBase.coq_T)
-      -> (exn -> 'a2 IOBase.coq_T) -> 'a2
+      'a1 t -> __ -> (unit -> proofview ->
+      Environ.env -> __ -> (('a2*bool) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      proofview -> Environ.env -> __ ->
+      (('a2*bool) -> (exn -> 'a3
+      IOBase.coq_T) -> 'a3 IOBase.coq_T) ->
+      (exn -> 'a3 IOBase.coq_T) -> 'a3
       IOBase.coq_T **)
   
   let ignore x =
-    (); (fun s e _ sk fk ->
-      Obj.magic x s e __ (fun a fk0 ->
-        let x0,c = a in
-        let a0,s0 = x0 in sk (((),s0),c) fk0)
-        fk)
+    (); (fun _ k s ->
+      Obj.magic x __ (fun x1 s' -> k () s') s)
   
   (** val seq :
-      unit t -> 'a1 t -> proofview ->
-      Environ.env -> __ ->
-      ((('a1*proofview)*bool) -> (exn -> 'a2
-      IOBase.coq_T) -> 'a2 IOBase.coq_T) ->
-      (exn -> 'a2 IOBase.coq_T) -> 'a2
+      unit t -> 'a1 t -> __ -> ('a1 ->
+      proofview -> Environ.env -> __ ->
+      (('a2*bool) -> (exn -> __ IOBase.coq_T)
+      -> __ IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      proofview -> Environ.env -> __ ->
+      (('a2*bool) -> (exn -> 'a3
+      IOBase.coq_T) -> 'a3 IOBase.coq_T) ->
+      (exn -> 'a3 IOBase.coq_T) -> 'a3
       IOBase.coq_T **)
   
   let seq x k =
-    (); (fun s e _ sk fk ->
-      Obj.magic x s e __ (fun a fk0 ->
-        let x0,c = a in
-        let u,s0 = x0 in
-        Obj.magic k s0 e __ (fun a0 fk1 ->
-          let y,c' = a0 in
-          sk (y,(if c then c' else false))
-            fk1) fk0) fk)
+    (); (fun _ k0 s ->
+      Obj.magic x __ (fun x1 s' ->
+        Obj.magic k __ k0 s') s)
   
   (** val set :
-      logicalState -> proofview ->
-      Environ.env -> __ ->
-      (((unit*proofview)*bool) -> (exn -> 'a1
-      IOBase.coq_T) -> 'a1 IOBase.coq_T) ->
-      (exn -> 'a1 IOBase.coq_T) -> 'a1
+      logicalState -> __ -> (unit ->
+      proofview -> Environ.env -> __ ->
+      (('a1*bool) -> (exn -> __ IOBase.coq_T)
+      -> __ IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      proofview -> Environ.env -> __ ->
+      (('a1*bool) -> (exn -> 'a2
+      IOBase.coq_T) -> 'a2 IOBase.coq_T) ->
+      (exn -> 'a2 IOBase.coq_T) -> 'a2
       IOBase.coq_T **)
   
   let set s =
-    (); (fun s0 e _ sk fk ->
-      sk (((),s),true) fk)
+    (); (fun _ k x -> Obj.magic k () s)
   
   (** val get :
+      __ -> (logicalState -> proofview ->
+      Environ.env -> __ -> (('a1*bool) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
       proofview -> Environ.env -> __ ->
-      (((logicalState*proofview)*bool) ->
-      (exn -> 'a1 IOBase.coq_T) -> 'a1
-      IOBase.coq_T) -> (exn -> 'a1
-      IOBase.coq_T) -> 'a1 IOBase.coq_T **)
+      (('a1*bool) -> (exn -> 'a2
+      IOBase.coq_T) -> 'a2 IOBase.coq_T) ->
+      (exn -> 'a2 IOBase.coq_T) -> 'a2
+      IOBase.coq_T **)
   
-  let get s e r sk fk =
-    sk ((s,s),true) fk
+  let get r k s =
+    Obj.magic k s s
   
   (** val put :
-      logicalMessageType -> proofview ->
-      Environ.env -> __ ->
-      (((unit*proofview)*bool) -> (exn -> 'a1
-      IOBase.coq_T) -> 'a1 IOBase.coq_T) ->
-      (exn -> 'a1 IOBase.coq_T) -> 'a1
+      logicalMessageType -> __ -> (unit ->
+      proofview -> Environ.env -> __ ->
+      (('a1*bool) -> (exn -> __ IOBase.coq_T)
+      -> __ IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      proofview -> Environ.env -> __ ->
+      (('a1*bool) -> (exn -> 'a2
+      IOBase.coq_T) -> 'a2 IOBase.coq_T) ->
+      (exn -> 'a2 IOBase.coq_T) -> 'a2
       IOBase.coq_T **)
   
   let put m =
-    (); (fun s e _ sk fk -> sk (((),s),m) fk)
+    (); (fun _ k s e _ sk fk ->
+      Obj.magic k () s e __ (fun a fk0 ->
+        let y,c' = a in
+        sk (y,(if m then c' else false)) fk0)
+        fk)
   
   (** val current :
+      __ -> (logicalEnvironment -> proofview
+      -> Environ.env -> __ -> (('a1*bool) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
       proofview -> Environ.env -> __ ->
-      (((logicalEnvironment*proofview)*bool)
-      -> (exn -> 'a1 IOBase.coq_T) -> 'a1
-      IOBase.coq_T) -> (exn -> 'a1
-      IOBase.coq_T) -> 'a1 IOBase.coq_T **)
+      (('a1*bool) -> (exn -> 'a2
+      IOBase.coq_T) -> 'a2 IOBase.coq_T) ->
+      (exn -> 'a2 IOBase.coq_T) -> 'a2
+      IOBase.coq_T **)
   
-  let current s e r sk fk =
-    sk ((e,s),true) fk
+  let current r k s e r0 sk fk =
+    Obj.magic k e s e __ (fun a fk0 ->
+      let y,c' = a in sk (y,c') fk0) fk
   
   (** val zero :
-      exn -> proofview -> Environ.env -> __
-      -> ((('a1*proofview)*bool) -> (exn ->
-      'a2 IOBase.coq_T) -> 'a2 IOBase.coq_T)
-      -> (exn -> 'a2 IOBase.coq_T) -> 'a2
+      exn -> __ -> ('a1 -> proofview ->
+      Environ.env -> __ -> (('a2*bool) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      proofview -> Environ.env -> __ ->
+      (('a2*bool) -> (exn -> 'a3
+      IOBase.coq_T) -> 'a3 IOBase.coq_T) ->
+      (exn -> 'a3 IOBase.coq_T) -> 'a3
       IOBase.coq_T **)
   
   let zero e =
-    (); (fun s e0 _ sk fk -> fk e)
+    (); (fun _ k s e0 _ sk fk -> fk e)
   
   (** val plus :
-      'a1 t -> (exn -> 'a1 t) -> proofview ->
-      Environ.env -> __ ->
-      ((('a1*proofview)*bool) -> (exn -> 'a2
-      IOBase.coq_T) -> 'a2 IOBase.coq_T) ->
-      (exn -> 'a2 IOBase.coq_T) -> 'a2
+      'a1 t -> (exn -> 'a1 t) -> __ -> ('a1
+      -> proofview -> Environ.env -> __ ->
+      (('a2*bool) -> (exn -> __ IOBase.coq_T)
+      -> __ IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      proofview -> Environ.env -> __ ->
+      (('a2*bool) -> (exn -> 'a3
+      IOBase.coq_T) -> 'a3 IOBase.coq_T) ->
+      (exn -> 'a3 IOBase.coq_T) -> 'a3
       IOBase.coq_T **)
   
   let plus x y =
-    (); (fun s env _ sk fk ->
-      Obj.magic x s env __ sk (fun e ->
-        Obj.magic y e s env __ sk fk))
+    (); (fun _ k s env _ sk fk ->
+      Obj.magic x __ k s env __ sk (fun e ->
+        Obj.magic y e __ k s env __ sk fk))
   
   (** val split :
-      'a1 t -> proofview -> Environ.env -> __
-      -> (((('a1*(exn -> 'a1 t), exn)
-      Util.union*proofview)*bool) -> (exn ->
-      'a2 IOBase.coq_T) -> 'a2 IOBase.coq_T)
-      -> (exn -> 'a2 IOBase.coq_T) -> 'a2
+      'a1 t -> __ -> (('a1*(exn -> 'a1 t),
+      exn) Util.union -> proofview ->
+      Environ.env -> __ -> (('a2*bool) ->
+      (exn -> __ IOBase.coq_T) -> __
+      IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      proofview -> Environ.env -> __ ->
+      (('a2*bool) -> (exn -> 'a3
+      IOBase.coq_T) -> 'a3 IOBase.coq_T) ->
+      (exn -> 'a3 IOBase.coq_T) -> 'a3
       IOBase.coq_T **)
   
   let split x =
-    (); (fun s e _ sk fk ->
+    (); (fun _ k s e _ sk fk ->
       IOBase.bind
         (IOBase.bind
-          (Obj.magic x s e __ (fun a fk0 ->
+          (Obj.magic x __
+            (fun a s' e0 _ sk0 fk0 ->
+            sk0 ((a,s'),true) fk0) s e __
+            (fun a fk0 ->
             IOBase.ret (Util.Inl
               (a,(fun e0 _ sk0 fk1 ->
               IOBase.bind (fk0 e0) (fun x0 ->
@@ -345,25 +392,45 @@ module Logical =
             let p1,m' = p0 in
             let a',s' = p1 in
             IOBase.ret (((Util.Inl
-              (a',(fun exc x0 x1 ->
-              y exc))),s'),m')
+              (a',(fun exc _ k0 s0 e0 _ sk0 fk0 ->
+              y exc __ (fun a fk1 ->
+                let x0,c = a in
+                let a0,s'0 = x0 in
+                k0 a0 s'0 e0 __
+                  (fun a1 fk2 ->
+                  let y0,c' = a1 in
+                  sk0
+                    (y0,(if c
+                         then c'
+                         else false)) fk2)
+                  fk1) fk0))),s'),m')
           | Util.Inr exc ->
             IOBase.ret (((Util.Inr
               exc),s),true))) (fun x0 ->
-        sk x0 fk))
+        let x1,c = x0 in
+        let a,s' = x1 in
+        Obj.magic k a s' e __ (fun a0 fk0 ->
+          let y,c' = a0 in
+          sk (y,(if c then c' else false))
+            fk0) fk))
   
   (** val lift :
-      'a1 NonLogical.t -> proofview ->
-      Environ.env -> __ ->
-      ((('a1*proofview)*bool) -> (exn -> 'a2
-      IOBase.coq_T) -> 'a2 IOBase.coq_T) ->
-      (exn -> 'a2 IOBase.coq_T) -> 'a2
+      'a1 NonLogical.t -> __ -> ('a1 ->
+      proofview -> Environ.env -> __ ->
+      (('a2*bool) -> (exn -> __ IOBase.coq_T)
+      -> __ IOBase.coq_T) -> (exn -> __
+      IOBase.coq_T) -> __ IOBase.coq_T) ->
+      proofview -> Environ.env -> __ ->
+      (('a2*bool) -> (exn -> 'a3
+      IOBase.coq_T) -> 'a3 IOBase.coq_T) ->
+      (exn -> 'a3 IOBase.coq_T) -> 'a3
       IOBase.coq_T **)
   
   let lift x =
-    (); (fun s e _ sk fk ->
+    (); (fun _ k s e _ sk fk ->
       IOBase.bind x (fun x0 ->
-        sk ((x0,s),true) fk))
+        Obj.magic k x0 s e __ (fun a fk0 ->
+          let y,c' = a in sk (y,c') fk0) fk))
   
   (** val run :
       'a1 t -> logicalEnvironment ->
@@ -372,8 +439,9 @@ module Logical =
       NonLogical.t **)
   
   let run x e s =
-    Obj.magic x s e __ (fun a x0 ->
-      IOBase.ret a) (fun e0 ->
+    Obj.magic x __ (fun a s' e0 _ sk fk ->
+      sk ((a,s'),true) fk) s e __
+      (fun a x0 -> IOBase.ret a) (fun e0 ->
       IOBase.raise
         ((fun e -> Proof_errors.TacticFailure e)
           e0))