# HG changeset patch
# User wenzelm
# Date 1508760729 -7200
# Node ID d9783ea1160c530a7fda22051a7856aa33c15211
# Parent  c078509d460651d016433de54226bf2045c2b663
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;

diff -r c078509d4606 -r d9783ea1160c src/Pure/Concurrent/lazy.ML
--- a/src/Pure/Concurrent/lazy.ML	Sun Oct 22 22:22:19 2017 +0200
+++ b/src/Pure/Concurrent/lazy.ML	Mon Oct 23 14:12:09 2017 +0200
@@ -9,9 +9,9 @@
 signature LAZY =
 sig
   type 'a lazy
+  val value: 'a -> 'a lazy
   val lazy_name: string -> (unit -> 'a) -> 'a lazy
   val lazy: (unit -> 'a) -> 'a lazy
-  val value: 'a -> 'a lazy
   val peek: 'a lazy -> 'a Exn.result option
   val is_running: 'a lazy -> bool
   val is_finished: 'a lazy -> bool
@@ -31,70 +31,75 @@
   Expr of string * (unit -> 'a) |
   Result of 'a future;
 
-abstype 'a lazy = Lazy of 'a expr Synchronized.var
+abstype 'a lazy = Value of 'a | Lazy of 'a expr Synchronized.var
 with
 
+fun value a = Value a;
+
 fun lazy_name name e = Lazy (Synchronized.var "lazy" (Expr (name, e)));
 fun lazy e = lazy_name "lazy" e;
-fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a)));
 
-fun peek (Lazy var) =
-  (case Synchronized.value var of
-    Expr _ => NONE
-  | Result res => Future.peek res);
+fun peek (Value a) = SOME (Exn.Res a)
+  | peek (Lazy var) =
+      (case Synchronized.value var of
+        Expr _ => NONE
+      | Result res => Future.peek res);
 
-fun pending (Lazy var) =
-  (case Synchronized.value var of
-    Expr _ => true
-  | Result _ => false);
+fun pending (Value _) = false
+  | pending (Lazy var) =
+      (case Synchronized.value var of
+        Expr _ => true
+      | Result _ => false);
 
 
 
 (* status *)
 
-fun is_future pred (Lazy var) =
-  (case Synchronized.value var of
-    Expr _ => false
-  | Result res => pred res);
+fun is_running (Value _) = false
+  | is_running (Lazy var) =
+      (case Synchronized.value var of
+        Expr _ => false
+      | Result res => not (Future.is_finished res));
 
-fun is_running x = is_future (not o Future.is_finished) x;
-
-fun is_finished x =
-  is_future (fn res =>
-    Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res))) x;
+fun is_finished (Value _) = true
+  | is_finished (Lazy var) =
+      (case Synchronized.value var of
+        Expr _ => false
+      | Result res =>
+          Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res)));
 
 
 (* force result *)
 
-fun force_result (Lazy var) =
-  (case peek (Lazy var) of
-    SOME res => res
-  | NONE =>
-      Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
-        let
-          val (expr, x) =
-            Synchronized.change_result var
-              (fn Expr (name, e) =>
-                    let val x = Future.promise_name name I
-                    in ((SOME (name, e), x), Result x) end
-                | Result x => ((NONE, x), Result x));
-        in
-          (case expr of
-            SOME (name, e) =>
-              let
-                val res0 = Exn.capture (restore_attributes e) ();
-                val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
-                val res = Future.join_result x;
-                (*semantic race: some other threads might see the same
-                  interrupt, until there is a fresh start*)
-                val _ =
-                  if Exn.is_interrupt_exn res then
-                    Synchronized.change var (fn _ => Expr (name, e))
-                  else ();
-              in res end
-          | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
-        end) ());
-
+fun force_result (Value a) = Exn.Res a
+  | force_result (Lazy var) =
+      (case peek (Lazy var) of
+        SOME res => res
+      | NONE =>
+          Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
+            let
+              val (expr, x) =
+                Synchronized.change_result var
+                  (fn Expr (name, e) =>
+                        let val x = Future.promise_name name I
+                        in ((SOME (name, e), x), Result x) end
+                    | Result x => ((NONE, x), Result x));
+            in
+              (case expr of
+                SOME (name, e) =>
+                  let
+                    val res0 = Exn.capture (restore_attributes e) ();
+                    val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
+                    val res = Future.join_result x;
+                    (*semantic race: some other threads might see the same
+                      interrupt, until there is a fresh start*)
+                    val _ =
+                      if Exn.is_interrupt_exn res then
+                        Synchronized.change var (fn _ => Expr (name, e))
+                      else ();
+                  in res end
+              | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
+            end) ());
 
 end;