diff options
author | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:37:42 +0000 |
---|---|---|
committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-02 15:37:42 +0000 |
commit | bbe58bc0b1dc9e8ae44a151dfcfa3923a391ce2d (patch) | |
tree | f8f508d7ffb5554daf5f8d861c84ab3d465ef30a /bootstrap/Monads.v | |
parent | 8a226a66871bd99db0a236393082d3dd2a7bc29a (diff) |
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
Diffstat (limited to 'bootstrap/Monads.v')
-rw-r--r-- | bootstrap/Monads.v | 20 |
1 files changed, 11 insertions, 9 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 - )))) + ))) . |