separate concurrent/sequential versions of lazy evaluation;
authorwenzelm
Thu Oct 01 18:10:41 2009 +0200 (2009-10-01)
changeset 328151a5e364584ae
parent 32814 81897d30b97f
child 32816 5db89f8d44f3
separate concurrent/sequential versions of lazy evaluation;
lazy based on future avoids wasted evaluations;
src/Pure/Concurrent/lazy.ML
src/Pure/General/lazy.ML
src/Pure/IsaMakefile
src/Pure/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Concurrent/lazy.ML	Thu Oct 01 18:10:41 2009 +0200
     1.3 @@ -0,0 +1,58 @@
     1.4 +(*  Title:      Pure/Concurrent/lazy.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Lazy evaluation based on futures.
     1.8 +*)
     1.9 +
    1.10 +signature LAZY =
    1.11 +sig
    1.12 +  type 'a lazy
    1.13 +  val peek: 'a lazy -> 'a Exn.result option
    1.14 +  val lazy: (unit -> 'a) -> 'a lazy
    1.15 +  val value: 'a -> 'a lazy
    1.16 +  val force_result: 'a lazy -> 'a Exn.result
    1.17 +  val force: 'a lazy -> 'a
    1.18 +  val map_force: ('a -> 'b) -> 'a lazy -> 'b lazy
    1.19 +end;
    1.20 +
    1.21 +structure Lazy: LAZY =
    1.22 +struct
    1.23 +
    1.24 +(* datatype *)
    1.25 +
    1.26 +datatype 'a expr =
    1.27 +  Expr of unit -> 'a |
    1.28 +  Future of 'a future;
    1.29 +
    1.30 +abstype 'a lazy = Lazy of 'a expr Synchronized.var
    1.31 +with
    1.32 +
    1.33 +fun peek (Lazy var) =
    1.34 +  (case Synchronized.value var of
    1.35 +    Expr _ => NONE
    1.36 +  | Future x => Future.peek x);
    1.37 +
    1.38 +fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
    1.39 +fun value a = Lazy (Synchronized.var "lazy" (Future (Future.value a)));
    1.40 +
    1.41 +
    1.42 +(* force result *)
    1.43 +
    1.44 +fun force_result (Lazy var) =
    1.45 +  (case peek (Lazy var) of
    1.46 +    SOME res => res
    1.47 +  | NONE =>
    1.48 +      Synchronized.guarded_access var
    1.49 +        (fn Expr e => let val x = Future.fork e in SOME (x, Future x) end
    1.50 +          | Future x => SOME (x, Future x))
    1.51 +      |> Future.join_result);
    1.52 +
    1.53 +fun force r = Exn.release (force_result r);
    1.54 +
    1.55 +fun map_force f = value o f o force;
    1.56 +
    1.57 +end;
    1.58 +end;
    1.59 +
    1.60 +type 'a lazy = 'a Lazy.lazy;
    1.61 +
     2.1 --- a/src/Pure/General/lazy.ML	Thu Oct 01 16:27:13 2009 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,65 +0,0 @@
     2.4 -(*  Title:      Pure/General/lazy.ML
     2.5 -    Author:     Florian Haftmann and Makarius, TU Muenchen
     2.6 -
     2.7 -Lazy evaluation with memoing.  Concurrency may lead to multiple
     2.8 -attempts of evaluation -- the first result persists.
     2.9 -*)
    2.10 -
    2.11 -signature LAZY =
    2.12 -sig
    2.13 -  type 'a lazy
    2.14 -  val same: 'a lazy * 'a lazy -> bool
    2.15 -  val lazy: (unit -> 'a) -> 'a lazy
    2.16 -  val value: 'a -> 'a lazy
    2.17 -  val peek: 'a lazy -> 'a Exn.result option
    2.18 -  val force_result: 'a lazy -> 'a Exn.result
    2.19 -  val force: 'a lazy -> 'a
    2.20 -  val map_force: ('a -> 'a) -> 'a lazy -> 'a lazy
    2.21 -end
    2.22 -
    2.23 -structure Lazy :> LAZY =
    2.24 -struct
    2.25 -
    2.26 -(* datatype *)
    2.27 -
    2.28 -datatype 'a T =
    2.29 -  Lazy of unit -> 'a |
    2.30 -  Result of 'a Exn.result;
    2.31 -
    2.32 -type 'a lazy = 'a T Unsynchronized.ref;
    2.33 -
    2.34 -fun same (r1: 'a lazy, r2) = r1 = r2;
    2.35 -
    2.36 -fun lazy e = Unsynchronized.ref (Lazy e);
    2.37 -fun value x = Unsynchronized.ref (Result (Exn.Result x));
    2.38 -
    2.39 -fun peek r =
    2.40 -  (case ! r of
    2.41 -    Lazy _ => NONE
    2.42 -  | Result res => SOME res);
    2.43 -
    2.44 -
    2.45 -(* force result *)
    2.46 -
    2.47 -fun force_result r =
    2.48 -  let
    2.49 -    (*potentially concurrent evaluation*)
    2.50 -    val res =
    2.51 -      (case ! r of
    2.52 -        Lazy e => Exn.capture e ()
    2.53 -      | Result res => res);
    2.54 -    (*assign result -- first one persists*)
    2.55 -    val res' = NAMED_CRITICAL "lazy" (fn () =>
    2.56 -      (case ! r of
    2.57 -        Lazy _ => (r := Result res; res)
    2.58 -      | Result res' => res'));
    2.59 -  in res' end;
    2.60 -
    2.61 -fun force r = Exn.release (force_result r);
    2.62 -
    2.63 -fun map_force f = value o f o force;
    2.64 -
    2.65 -end;
    2.66 -
    2.67 -type 'a lazy = 'a Lazy.lazy;
    2.68 -
     3.1 --- a/src/Pure/IsaMakefile	Thu Oct 01 16:27:13 2009 +0200
     3.2 +++ b/src/Pure/IsaMakefile	Thu Oct 01 18:10:41 2009 +0200
     3.3 @@ -43,18 +43,19 @@
     3.4  Pure: $(OUT)/Pure
     3.5  
     3.6  $(OUT)/Pure: $(BOOTSTRAP_FILES) Concurrent/future.ML			\
     3.7 +  Concurrent/lazy.ML Concurrent/lazy_sequential.ML			\
     3.8    Concurrent/mailbox.ML Concurrent/par_list.ML				\
     3.9    Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML		\
    3.10    Concurrent/synchronized.ML Concurrent/synchronized_dummy.ML		\
    3.11    Concurrent/task_queue.ML General/alist.ML General/antiquote.ML	\
    3.12    General/balanced_tree.ML General/basics.ML General/binding.ML		\
    3.13    General/buffer.ML General/file.ML General/graph.ML General/heap.ML	\
    3.14 -  General/integer.ML General/lazy.ML General/long_name.ML		\
    3.15 -  General/markup.ML General/name_space.ML General/ord_list.ML		\
    3.16 -  General/output.ML General/path.ML General/position.ML			\
    3.17 -  General/pretty.ML General/print_mode.ML General/properties.ML		\
    3.18 -  General/queue.ML General/same.ML General/scan.ML General/secure.ML	\
    3.19 -  General/seq.ML General/source.ML General/stack.ML General/symbol.ML	\
    3.20 +  General/integer.ML General/long_name.ML General/markup.ML		\
    3.21 +  General/name_space.ML General/ord_list.ML General/output.ML		\
    3.22 +  General/path.ML General/position.ML General/pretty.ML			\
    3.23 +  General/print_mode.ML General/properties.ML General/queue.ML		\
    3.24 +  General/same.ML General/scan.ML General/secure.ML General/seq.ML	\
    3.25 +  General/source.ML General/stack.ML General/symbol.ML			\
    3.26    General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML	\
    3.27    General/yxml.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML		\
    3.28    Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML	\
     4.1 --- a/src/Pure/ROOT.ML	Thu Oct 01 16:27:13 2009 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Thu Oct 01 18:10:41 2009 +0200
     4.3 @@ -45,7 +45,6 @@
     4.4  use "General/long_name.ML";
     4.5  use "General/binding.ML";
     4.6  use "General/name_space.ML";
     4.7 -use "General/lazy.ML";
     4.8  use "General/path.ML";
     4.9  use "General/url.ML";
    4.10  use "General/buffer.ML";
    4.11 @@ -58,12 +57,17 @@
    4.12  
    4.13  use "Concurrent/simple_thread.ML";
    4.14  use "Concurrent/synchronized.ML";
    4.15 -if Multithreading.available then () else use "Concurrent/synchronized_dummy.ML";
    4.16 +if Multithreading.available then () else
    4.17 +use "Concurrent/synchronized_dummy.ML";
    4.18  use "Concurrent/mailbox.ML";
    4.19  use "Concurrent/task_queue.ML";
    4.20  use "Concurrent/future.ML";
    4.21 +use "Concurrent/lazy.ML";
    4.22 +if Multithreading.available then ()
    4.23 +else use "Concurrent/lazy_sequential.ML";
    4.24  use "Concurrent/par_list.ML";
    4.25 -if Multithreading.available then () else use "Concurrent/par_list_dummy.ML";
    4.26 +if Multithreading.available then ()
    4.27 +else use "Concurrent/par_list_dummy.ML";
    4.28  
    4.29  
    4.30  (* fundamental structures *)