src/Pure/Concurrent/lazy.ML

removed unused map_force;

(*  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
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);

end;
end;

type 'a lazy = 'a Lazy.lazy;