src/Pure/Concurrent/lazy.ML
changeset 68868 5f44ad150ed8
parent 68867 a8728e3f9822
child 68918 3a0db30e5d87
     1.1 --- a/src/Pure/Concurrent/lazy.ML	Sat Sep 01 14:25:03 2018 +0200
     1.2 +++ b/src/Pure/Concurrent/lazy.ML	Sat Sep 01 16:08:54 2018 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4    val is_running: 'a lazy -> bool
     1.5    val is_finished: 'a lazy -> bool
     1.6    val finished_result: 'a lazy -> 'a Exn.result
     1.7 -  val force_result: 'a lazy -> 'a Exn.result
     1.8 +  val force_result: {strict: bool} -> 'a lazy -> 'a Exn.result
     1.9    val force: 'a lazy -> 'a
    1.10    val force_value: 'a lazy -> 'a lazy
    1.11    val map: ('a -> 'b) -> 'a lazy -> 'b lazy
    1.12 @@ -80,8 +80,8 @@
    1.13  
    1.14  (* force result *)
    1.15  
    1.16 -fun force_result (Value a) = Exn.Res a
    1.17 -  | force_result (Lazy var) =
    1.18 +fun force_result _ (Value a) = Exn.Res a
    1.19 +  | force_result {strict} (Lazy var) =
    1.20        (case peek (Lazy var) of
    1.21          SOME res => res
    1.22        | NONE =>
    1.23 @@ -104,19 +104,22 @@
    1.24                      val res0 = Exn.capture (restore_attributes e) ();
    1.25                      val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
    1.26                      val res = Future.join_result x;
    1.27 -                    (*semantic race: some other threads might see the same
    1.28 -                      interrupt, until there is a fresh start*)
    1.29                      val _ =
    1.30 -                      if Exn.is_interrupt_exn res
    1.31 -                      then Synchronized.change var (fn _ => Expr (name, e))
    1.32 -                      else Synchronized.assign var (Result (Future.value_result res));
    1.33 +                      if not (Exn.is_interrupt_exn res) then
    1.34 +                        Synchronized.assign var (Result (Future.value_result res))
    1.35 +                      else if strict then
    1.36 +                        Synchronized.assign var
    1.37 +                          (Result (Future.value_result (Exn.Exn (Fail "Interrupt"))))
    1.38 +                      (*semantic race: some other threads might see the same
    1.39 +                        interrupt, until there is a fresh start*)
    1.40 +                      else Synchronized.change var (fn _ => Expr (name, e));
    1.41                    in res end
    1.42                | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
    1.43              end) ());
    1.44  
    1.45  end;
    1.46  
    1.47 -fun force x = Exn.release (force_result x);
    1.48 +fun force x = Exn.release (force_result {strict = false} x);
    1.49  
    1.50  fun force_value x = if is_value x then x else value (force x);
    1.51  
    1.52 @@ -133,7 +136,8 @@
    1.53  fun consolidate xs =
    1.54    let
    1.55      val unfinished =
    1.56 -      xs |> map_filter (fn x => if is_finished x then NONE else SOME (fn () => force_result x));
    1.57 +      xs |> map_filter (fn x =>
    1.58 +        if is_finished x then NONE else SOME (fn () => force_result {strict = false} x));
    1.59      val _ =
    1.60        if Future.relevant unfinished then
    1.61          ignore (Future.forked_results {name = "Lazy.consolidate", deps = []} unfinished)
    1.62 @@ -144,7 +148,7 @@
    1.63  (* future evaluation *)
    1.64  
    1.65  fun future params x =
    1.66 -  if is_finished x then Future.value_result (force_result x)
    1.67 +  if is_finished x then Future.value_result (force_result {strict = false} x)
    1.68    else (singleton o Future.forks) params (fn () => force x);
    1.69  
    1.70