src/Pure/Concurrent/lazy.ML

more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;

(*  Title:      Pure/Concurrent/lazy.ML
    Author:     Makarius

Lazy evaluation with memoing of results and regular exceptions.
Parallel version based on (passive) futures, to avoid critical or
multiple evaluation (unless interrupted).
*)

signature LAZY =
sig
  type 'a lazy
  val peek: 'a lazy -> 'a Exn.result option
  val is_finished: 'a lazy -> bool
  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: ('a -> 'b) -> 'a lazy -> 'b lazy
  val future: Future.params -> 'a lazy -> 'a future
end;

structure Lazy: LAZY =
struct

(* datatype *)

datatype 'a expr =
  Expr of unit -> 'a |
  Result of 'a future;

abstype 'a lazy = Lazy of 'a expr Synchronized.var
with

fun peek (Lazy var) =
  (case Synchronized.value var of
    Expr _ => NONE
  | Result res => Future.peek res);

fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a)));

fun is_finished x = is_some (peek x);


(* force result *)

fun force_result (Lazy var) =
  (case peek (Lazy var) of
    SOME res => res
  | NONE =>
      uninterruptible (fn restore_attributes => fn () =>
        let
          val (expr, x) =
            Synchronized.change_result var
              (fn Expr e =>
                    let val x = Future.promise I
                    in ((SOME e, x), Result x) end
                | Result x => ((NONE, x), Result x));
        in
          (case expr of
            SOME 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 e)
                  else ();
              in res end
          | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
        end) ());


end;

fun force r = Exn.release (force_result r);
fun map f x = lazy (fn () => f (force x));


(* future evaluation *)

fun future params x =
  if is_finished x then Future.value_result (force_result x)
  else (singleton o Future.forks) params (fn () => force x);

end;

type 'a lazy = 'a Lazy.lazy;