From bbe58bc0b1dc9e8ae44a151dfcfa3923a391ce2d Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:37:42 +0000
Subject: 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
---
 bootstrap/Monads.v | 20 +++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

(limited to 'bootstrap')

diff --git a/bootstrap/Monads.v b/bootstrap/Monads.v
index 2403dde9ad..bff4e5e5f0 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
-  ))))
+  )))
 .
 
 
-- 
cgit v1.2.3