bootstrap/Monads.v: A more efficient split.

Exchanges a IO.bind for a Logic.bind. The latter is better inlined.

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

2 files changed, 51 insertions, 52 deletions

diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index 2403dde9a..bff4e5e5f 100644
--- a/bootstrap/Monads.v
+++ b/bootstrap/Monads.v
@@ -469,9 +469,8 @@ Section Common.
    x _ sk (fun e => y e _ sk fk)
  .
 
- (* For [reflect] and [reify] see the "Backtracking, Interleaving, and
-    Terminating Monad Transformers" paper (where [reify] must be seen
-    as the body of [msplit]).  *)
+ (* For [reflect] and [split] see the "Backtracking, Interleaving, and
+    Terminating Monad Transformers" paper.  *)
  Definition reflect {A:Set} (x:(A*(Exception -> T A)) + Exception) : T A :=
    match x with
    | inr e => _zero e
@@ -485,6 +484,10 @@ Section Common.
    x _ sk fk
  .
 
+ Definition split {A:Set} (x:T A) : T ((A*(Exception -> T A)) + Exception) :=
+   lift (reify x)
+ .
+
  Definition Logic : Logic T := {|
    zero := @_zero;
    plus := @_plus
@@ -548,20 +551,19 @@ Definition split0 {a:Set} (x:LogicalType a) : LogicalType ((a*(Exception -> Logi
   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 _ _ LogicalMonadEnv x s) e)) in
+    do LogicalMonadBase x' :=
+        Logic.split _ 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)
+    | inr exc => ret _ LogicalMonadBase ((inr exc),s, Monoid.zero _ LogicalMessage)
     | inl (a',s',m',y) =>
       let y' exc :=
           State.reflect _ _ LogicalMonadEnv (fun _ =>
           Environment.reflect _ _ (fun _ =>
           Writer.reflect _ _ (y exc)))
       in
-      ret _ NonLogicalMonad (inl (a',y'),s',m')
+      ret _ LogicalMonadBase (inl (a',y'),s',m')
     end
-  ))))
+  )))
 .
 
 
diff --git a/proofs/proofview_gen.ml b/proofs/proofview_gen.ml
index 48201d39e..ad87b7328 100644
--- a/proofs/proofview_gen.ml
+++ b/proofs/proofview_gen.ml
@@ -369,50 +369,47 @@ module Logical =
   let split x =
     (); (fun _ k s e _ sk fk ->
       IOBase.bind
-        (IOBase.bind
-          (Obj.magic x __
-            (fun a s' e0 _ sk0 fk0 ->
-            sk0 ((a,s'),true) fk0) s e __
+        (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 ->
+              match x0 with
+              | Util.Inl p ->
+                let a0,x1 = p in
+                sk0 a0 (fun e1 ->
+                  x1 e1 __ sk0 fk1)
+              | Util.Inr e1 -> fk1 e1)))))
+          (fun e0 ->
+          IOBase.ret (Util.Inr e0)))
+        (fun x0 ->
+        match x0 with
+        | Util.Inl p ->
+          let p0,y = p in
+          let p1,m' = p0 in
+          let a',s' = p1 in
+          Obj.magic k (Util.Inl
+            (a',(fun exc _ k0 s0 e0 _ sk0 fk0 ->
+            y exc __ (fun a fk1 ->
+              let x1,c = a in
+              let a0,s'0 = x1 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' e __ (fun a fk0 ->
+            let y0,c' = a in
+            sk
+              (y0,(if m' then c' else false))
+              fk0) fk
+        | Util.Inr exc ->
+          Obj.magic k (Util.Inr exc) s e __
             (fun a fk0 ->
-            IOBase.ret (Util.Inl
-              (a,(fun e0 _ sk0 fk1 ->
-              IOBase.bind (fk0 e0) (fun x0 ->
-                match x0 with
-                | Util.Inl p ->
-                  let a0,x1 = p in
-                  sk0 a0 (fun e1 ->
-                    x1 e1 __ sk0 fk1)
-                | Util.Inr e1 -> fk1 e1)))))
-            (fun e0 ->
-            IOBase.ret (Util.Inr e0)))
-          (fun x' ->
-          match x' with
-          | Util.Inl p ->
-            let p0,y = p in
-            let p1,m' = p0 in
-            let a',s' = p1 in
-            IOBase.ret (((Util.Inl
-              (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 ->
-        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))
+            let y,c' = a in sk (y,c') fk0) fk))
   
   (** val lift :
       'a1 NonLogical.t -> __ -> ('a1 ->