separate concurrent/sequential versions of lazy evaluation;
lazy based on future avoids wasted evaluations;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/lazy.ML	Thu Oct 01 18:10:41 2009 +0200
@@ -0,0 +1,58 @@
+(*  Title:      Pure/Concurrent/lazy.ML
+    Author:     Makarius
+
+Lazy evaluation based on futures.
+*)
+
+signature LAZY =
+sig
+  type 'a lazy
+  val peek: 'a lazy -> 'a Exn.result option
+  val lazy: (unit -> 'a) -> 'a lazy
+  val value: 'a -> 'a lazy
+  val force_result: 'a lazy -> 'a Exn.result
+  val force: 'a lazy -> 'a
+  val map_force: ('a -> 'b) -> 'a lazy -> 'b lazy
+end;
+
+structure Lazy: LAZY =
+struct
+
+(* datatype *)
+
+datatype 'a expr =
+  Expr of unit -> 'a |
+  Future of 'a future;
+
+abstype 'a lazy = Lazy of 'a expr Synchronized.var
+with
+
+fun peek (Lazy var) =
+  (case Synchronized.value var of
+    Expr _ => NONE
+  | Future x => Future.peek x);
+
+fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
+fun value a = Lazy (Synchronized.var "lazy" (Future (Future.value a)));
+
+
+(* force result *)
+
+fun force_result (Lazy var) =
+  (case peek (Lazy var) of
+    SOME res => res
+  | NONE =>
+      Synchronized.guarded_access var
+        (fn Expr e => let val x = Future.fork e in SOME (x, Future x) end
+          | Future x => SOME (x, Future x))
+      |> Future.join_result);
+
+fun force r = Exn.release (force_result r);
+
+fun map_force f = value o f o force;
+
+end;
+end;
+
+type 'a lazy = 'a Lazy.lazy;
+

--- a/src/Pure/General/lazy.ML	Thu Oct 01 16:27:13 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,65 +0,0 @@
-(*  Title:      Pure/General/lazy.ML
-    Author:     Florian Haftmann and Makarius, TU Muenchen
-
-Lazy evaluation with memoing.  Concurrency may lead to multiple
-attempts of evaluation -- the first result persists.
-*)
-
-signature LAZY =
-sig
-  type 'a lazy
-  val same: 'a lazy * 'a lazy -> bool
-  val lazy: (unit -> 'a) -> 'a lazy
-  val value: 'a -> 'a lazy
-  val peek: 'a lazy -> 'a Exn.result option
-  val force_result: 'a lazy -> 'a Exn.result
-  val force: 'a lazy -> 'a
-  val map_force: ('a -> 'a) -> 'a lazy -> 'a lazy
-end
-
-structure Lazy :> LAZY =
-struct
-
-(* datatype *)
-
-datatype 'a T =
-  Lazy of unit -> 'a |
-  Result of 'a Exn.result;
-
-type 'a lazy = 'a T Unsynchronized.ref;
-
-fun same (r1: 'a lazy, r2) = r1 = r2;
-
-fun lazy e = Unsynchronized.ref (Lazy e);
-fun value x = Unsynchronized.ref (Result (Exn.Result x));
-
-fun peek r =
-  (case ! r of
-    Lazy _ => NONE
-  | Result res => SOME res);
-
-
-(* force result *)
-
-fun force_result r =
-  let
-    (*potentially concurrent evaluation*)
-    val res =
-      (case ! r of
-        Lazy e => Exn.capture e ()
-      | Result res => res);
-    (*assign result -- first one persists*)
-    val res' = NAMED_CRITICAL "lazy" (fn () =>
-      (case ! r of
-        Lazy _ => (r := Result res; res)
-      | Result res' => res'));
-  in res' end;
-
-fun force r = Exn.release (force_result r);
-
-fun map_force f = value o f o force;
-
-end;
-
-type 'a lazy = 'a Lazy.lazy;
-

--- a/src/Pure/IsaMakefile	Thu Oct 01 16:27:13 2009 +0200
+++ b/src/Pure/IsaMakefile	Thu Oct 01 18:10:41 2009 +0200
@@ -43,18 +43,19 @@
 Pure: $(OUT)/Pure
 
 $(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/future.ML			\
+  Concurrent/lazy.ML Concurrent/lazy_sequential.ML			\
   Concurrent/mailbox.ML Concurrent/par_list.ML				\
   Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML		\
   Concurrent/synchronized.ML Concurrent/synchronized_dummy.ML		\
   Concurrent/task_queue.ML General/alist.ML General/antiquote.ML	\
   General/balanced_tree.ML General/basics.ML General/binding.ML		\
   General/buffer.ML General/file.ML General/graph.ML General/heap.ML	\
-  General/integer.ML General/lazy.ML General/long_name.ML		\
-  General/markup.ML General/name_space.ML General/ord_list.ML		\
-  General/output.ML General/path.ML General/position.ML			\
-  General/pretty.ML General/print_mode.ML General/properties.ML		\
-  General/queue.ML General/same.ML General/scan.ML General/secure.ML	\
-  General/seq.ML General/source.ML General/stack.ML General/symbol.ML	\
+  General/integer.ML General/long_name.ML General/markup.ML		\
+  General/name_space.ML General/ord_list.ML General/output.ML		\
+  General/path.ML General/position.ML General/pretty.ML			\
+  General/print_mode.ML General/properties.ML General/queue.ML		\
+  General/same.ML General/scan.ML General/secure.ML General/seq.ML	\
+  General/source.ML General/stack.ML General/symbol.ML			\
   General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML	\
   General/yxml.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML		\
   Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML	\

--- a/src/Pure/ROOT.ML	Thu Oct 01 16:27:13 2009 +0200
+++ b/src/Pure/ROOT.ML	Thu Oct 01 18:10:41 2009 +0200
@@ -45,7 +45,6 @@
 use "General/long_name.ML";
 use "General/binding.ML";
 use "General/name_space.ML";
-use "General/lazy.ML";
 use "General/path.ML";
 use "General/url.ML";
 use "General/buffer.ML";
@@ -58,12 +57,17 @@
 
 use "Concurrent/simple_thread.ML";
 use "Concurrent/synchronized.ML";
-if Multithreading.available then () else use "Concurrent/synchronized_dummy.ML";
+if Multithreading.available then () else
+use "Concurrent/synchronized_dummy.ML";
 use "Concurrent/mailbox.ML";
 use "Concurrent/task_queue.ML";
 use "Concurrent/future.ML";
+use "Concurrent/lazy.ML";
+if Multithreading.available then ()
+else use "Concurrent/lazy_sequential.ML";
 use "Concurrent/par_list.ML";
-if Multithreading.available then () else use "Concurrent/par_list_dummy.ML";
+if Multithreading.available then ()
+else use "Concurrent/par_list_dummy.ML";
 
 
 (* fundamental structures *)