# HG changeset patch # User wenzelm # Date 1254413441 -7200 # Node ID 1a5e364584ae5525db115aa763b1e72b2d06df11 # Parent 81897d30b97feb62c5440990e9c36dce71e24e3b separate concurrent/sequential versions of lazy evaluation; lazy based on future avoids wasted evaluations; diff -r 81897d30b97f -r 1a5e364584ae src/Pure/Concurrent/lazy.ML --- /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; + diff -r 81897d30b97f -r 1a5e364584ae src/Pure/General/lazy.ML --- 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; - diff -r 81897d30b97f -r 1a5e364584ae src/Pure/IsaMakefile --- 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 \ diff -r 81897d30b97f -r 1a5e364584ae src/Pure/ROOT.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 *)