--- a/doc-src/IsarAdvanced/Codegen/Thy/ML.thy Thu Oct 23 13:52:28 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/ML.thy Thu Oct 23 14:22:16 2008 +0200
@@ -24,7 +24,7 @@
\begin{mldecls}
@{index_ML Code.add_eqn: "thm -> theory -> theory"} \\
@{index_ML Code.del_eqn: "thm -> theory -> theory"} \\
- @{index_ML Code.add_eqnl: "string * (thm * bool) list Susp.T -> theory -> theory"} \\
+ @{index_ML Code.add_eqnl: "string * (thm * bool) list Lazy.T -> theory -> theory"} \\
@{index_ML Code.map_pre: "(MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory"} \\
@{index_ML Code.map_post: "(MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory"} \\
@{index_ML Code.add_functrans: "string * (theory -> (thm * bool) list -> (thm * bool) list option)
--- a/src/HOL/Import/lazy_seq.ML Thu Oct 23 13:52:28 2008 +0200
+++ b/src/HOL/Import/lazy_seq.ML Thu Oct 23 14:22:16 2008 +0200
@@ -80,13 +80,13 @@
structure LazySeq :> LAZY_SEQ =
struct
-datatype 'a seq = Seq of ('a * 'a seq) option Susp.T
+datatype 'a seq = Seq of ('a * 'a seq) option Lazy.T
exception Empty
-fun getItem (Seq s) = Susp.force s
+fun getItem (Seq s) = Lazy.force s
val pull = getItem
-fun make f = Seq (Susp.delay f)
+fun make f = Seq (Lazy.lazy f)
fun null s = is_none (getItem s)
@@ -137,7 +137,7 @@
local
fun F NONE _ = raise Subscript
| F (SOME(x,s)) n = SOME(x,F' s (n-1))
- and F' s 0 = Seq (Susp.value NONE)
+ and F' s 0 = Seq (Lazy.value NONE)
| F' s n = make (fn () => F (getItem s) n)
in
fun take (s,n) =
@@ -166,14 +166,14 @@
local
fun F s NONE = s
- | F s (SOME(x,s')) = F (SOME(x, Seq (Susp.value s))) (getItem s')
+ | F s (SOME(x,s')) = F (SOME(x, Seq (Lazy.value s))) (getItem s')
in
fun rev s = make (fn () => F NONE (getItem s))
end
local
fun F s NONE = getItem s
- | F s (SOME(x,s')) = F (Seq (Susp.value (SOME(x,s)))) (getItem s')
+ | F s (SOME(x,s')) = F (Seq (Lazy.value (SOME(x,s)))) (getItem s')
in
fun revAppend (s1,s2) = make (fn () => F s2 (getItem s1))
end
@@ -294,13 +294,13 @@
F' s1 s2
end
-fun empty _ = Seq (Susp.value NONE)
-fun single x = Seq(Susp.value (SOME(x,Seq (Susp.value NONE))))
-fun cons a = Seq(Susp.value (SOME a))
+fun empty _ = Seq (Lazy.value NONE)
+fun single x = Seq(Lazy.value (SOME(x,Seq (Lazy.value NONE))))
+fun cons a = Seq(Lazy.value (SOME a))
fun cycle seqfn =
let
- val knot = ref (Seq (Susp.value NONE))
+ val knot = ref (Seq (Lazy.value NONE))
in
knot := seqfn (fn () => !knot);
!knot
@@ -374,7 +374,7 @@
(* Adapted from seq.ML *)
val succeed = single
-fun fail _ = Seq (Susp.value NONE)
+fun fail _ = Seq (Lazy.value NONE)
(* fun op THEN (f, g) x = flat (map g (f x)) *)
@@ -414,7 +414,7 @@
fun TRY f x =
make (fn () =>
case getItem (f x) of
- NONE => SOME(x,Seq (Susp.value NONE))
+ NONE => SOME(x,Seq (Lazy.value NONE))
| some => some)
fun REPEAT f =
@@ -446,13 +446,13 @@
make (fn () =>
case getItem (f x) of
NONE => NONE
- | SOME (x', _) => SOME(x',Seq (Susp.value NONE)))
+ | SOME (x', _) => SOME(x',Seq (Lazy.value NONE)))
(*partial function as procedure*)
fun try f x =
make (fn () =>
case Basics.try f x of
- SOME y => SOME(y,Seq (Susp.value NONE))
+ SOME y => SOME(y,Seq (Lazy.value NONE))
| NONE => NONE)
(*functional to print a sequence, up to "count" elements;
@@ -497,7 +497,7 @@
(*turn a list of sequences into a sequence of lists*)
local
- fun F [] = SOME([],Seq (Susp.value NONE))
+ fun F [] = SOME([],Seq (Lazy.value NONE))
| F (xq :: xqs) =
case getItem xq of
NONE => NONE
--- a/src/HOL/Tools/datatype_codegen.ML Thu Oct 23 13:52:28 2008 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Thu Oct 23 14:22:16 2008 +0200
@@ -464,7 +464,7 @@
fun get_thms () = (eq_refl, false)
:: rev (map (rpair true) (get_eq' (Theory.deref thy_ref) dtco));
in
- Code.add_eqnl (const, Susp.delay get_thms) thy
+ Code.add_eqnl (const, Lazy.lazy get_thms) thy
end;
in
thy
--- a/src/Pure/General/ROOT.ML Thu Oct 23 13:52:28 2008 +0200
+++ b/src/Pure/General/ROOT.ML Thu Oct 23 14:22:16 2008 +0200
@@ -28,7 +28,7 @@
use "balanced_tree.ML";
use "graph.ML";
use "name_space.ML";
-use "susp.ML";
+use "lazy.ML";
use "path.ML";
use "url.ML";
use "buffer.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/lazy.ML Thu Oct 23 14:22:16 2008 +0200
@@ -0,0 +1,60 @@
+(* Title: Pure/General/lazy.ML
+ ID: $Id$
+ 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 T
+ val same: 'a T * 'a T -> bool
+ val lazy: (unit -> 'a) -> 'a T
+ val value: 'a -> 'a T
+ val peek: 'a T -> 'a Exn.result option
+ val force: 'a T -> 'a
+ val map_force: ('a -> 'a) -> 'a T -> 'a T
+end
+
+structure Lazy :> LAZY =
+struct
+
+(* datatype *)
+
+datatype 'a lazy =
+ Lazy of unit -> 'a |
+ Result of 'a Exn.result;
+
+type 'a T = 'a lazy ref;
+
+fun same (r1: 'a T, r2) = r1 = r2;
+
+fun lazy e = ref (Lazy e);
+fun value x = ref (Result (Exn.Result x));
+
+fun peek r =
+ (case ! r of
+ Lazy _ => NONE
+ | Result res => SOME res);
+
+
+(* force result *)
+
+fun force 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 Exn.release res' end;
+
+fun map_force f = value o f o force;
+
+end;
--- a/src/Pure/General/susp.ML Thu Oct 23 13:52:28 2008 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,60 +0,0 @@
-(* Title: Pure/General/susp.ML
- ID: $Id$
- Author: Sebastian Skalberg, Florian Haftmann and Makarius, TU Muenchen
-
-Delayed evaluation with memoing. Concurrency may lead to multiple
-attempts of evaluation -- the first result persists.
-*)
-
-signature SUSP =
-sig
- type 'a T
- val same: 'a T * 'a T -> bool
- val delay: (unit -> 'a) -> 'a T
- val value: 'a -> 'a T
- val peek: 'a T -> 'a Exn.result option
- val force: 'a T -> 'a
- val map_force: ('a -> 'a) -> 'a T -> 'a T
-end
-
-structure Susp :> SUSP =
-struct
-
-(* datatype *)
-
-datatype 'a susp =
- Delay of unit -> 'a |
- Result of 'a Exn.result;
-
-type 'a T = 'a susp ref;
-
-fun same (r1: 'a T, r2) = r1 = r2;
-
-fun delay e = ref (Delay e);
-fun value x = ref (Result (Exn.Result x));
-
-fun peek r =
- (case ! r of
- Delay _ => NONE
- | Result res => SOME res);
-
-
-(* force result *)
-
-fun force r =
- let
- (*potentially concurrent evaluation*)
- val res =
- (case ! r of
- Delay e => Exn.capture e ()
- | Result res => res);
- (*assign result -- first one persists*)
- val res' = NAMED_CRITICAL "susp" (fn () =>
- (case ! r of
- Delay _ => (r := Result res; res)
- | Result res' => res'));
- in Exn.release res' end;
-
-fun map_force f = value o f o force;
-
-end;
--- a/src/Pure/IsaMakefile Thu Oct 23 13:52:28 2008 +0200
+++ b/src/Pure/IsaMakefile Thu Oct 23 14:22:16 2008 +0200
@@ -30,33 +30,34 @@
Concurrent/task_queue.ML General/ROOT.ML General/alist.ML \
General/balanced_tree.ML General/basics.ML General/buffer.ML \
General/file.ML General/graph.ML General/heap.ML General/integer.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/scan.ML General/secure.ML General/seq.ML \
- General/source.ML General/stack.ML General/susp.ML General/symbol.ML \
- General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML \
- General/yxml.ML Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML \
- Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML \
- Isar/code.ML Isar/code_unit.ML Isar/constdefs.ML \
- Isar/context_rules.ML Isar/element.ML Isar/find_theorems.ML \
- Isar/instance.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML \
- Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML \
- Isar/locale.ML Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML \
- Isar/obtain.ML Isar/outer_keyword.ML Isar/outer_lex.ML \
- Isar/outer_parse.ML Isar/outer_syntax.ML Isar/overloading.ML \
- Isar/proof.ML Isar/proof_context.ML Isar/proof_display.ML \
- Isar/proof_node.ML Isar/rule_cases.ML Isar/rule_insts.ML \
- Isar/session.ML Isar/skip_proof.ML Isar/spec_parse.ML \
- Isar/specification.ML Isar/subclass.ML Isar/theory_target.ML \
- Isar/toplevel.ML ML-Systems/alice.ML ML-Systems/exn.ML \
- ML-Systems/install_pp_polyml.ML ML-Systems/ml_name_space.ML \
- ML-Systems/multithreading.ML ML-Systems/mosml.ML \
- ML-Systems/multithreading_polyml.ML ML-Systems/overloading_smlnj.ML \
- ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML \
- ML-Systems/polyml-4.2.0.ML ML-Systems/polyml-5.0.ML \
- ML-Systems/polyml-5.1.ML ML-Systems/polyml_common.ML \
- ML-Systems/polyml.ML ML-Systems/polyml_old_compiler4.ML \
+ General/lazy.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/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/ROOT.ML \
+ Isar/antiquote.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML \
+ Isar/calculation.ML Isar/class.ML Isar/code.ML Isar/code_unit.ML \
+ Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \
+ Isar/find_theorems.ML Isar/instance.ML Isar/isar.ML Isar/isar_cmd.ML \
+ Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML \
+ Isar/local_theory.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML \
+ Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \
+ Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \
+ Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \
+ Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \
+ Isar/rule_insts.ML Isar/session.ML Isar/skip_proof.ML \
+ Isar/spec_parse.ML Isar/specification.ML Isar/subclass.ML \
+ Isar/theory_target.ML Isar/toplevel.ML ML-Systems/alice.ML \
+ ML-Systems/exn.ML ML-Systems/install_pp_polyml.ML \
+ ML-Systems/ml_name_space.ML ML-Systems/multithreading.ML \
+ ML-Systems/mosml.ML ML-Systems/multithreading_polyml.ML \
+ ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML \
+ ML-Systems/polyml-4.1.4.ML ML-Systems/polyml-4.2.0.ML \
+ ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML \
+ ML-Systems/polyml_common.ML ML-Systems/polyml.ML \
+ ML-Systems/polyml_old_compiler4.ML \
ML-Systems/polyml_old_compiler5.ML ML-Systems/proper_int.ML \
ML-Systems/smlnj.ML ML-Systems/system_shell.ML \
ML-Systems/time_limit.ML ML-Systems/thread_dummy.ML \
--- a/src/Pure/Isar/code.ML Thu Oct 23 13:52:28 2008 +0200
+++ b/src/Pure/Isar/code.ML Thu Oct 23 14:22:16 2008 +0200
@@ -15,7 +15,7 @@
val add_default_eqn_attr: Attrib.src
val del_eqn: thm -> theory -> theory
val del_eqns: string -> theory -> theory
- val add_eqnl: string * (thm * bool) list Susp.T -> theory -> theory
+ val add_eqnl: string * (thm * bool) list Lazy.T -> theory -> theory
val map_pre: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
val map_post: (MetaSimplifier.simpset -> MetaSimplifier.simpset) -> theory -> theory
val add_inline: thm -> theory -> theory
@@ -117,16 +117,16 @@
(* defining equations with linear flag, default flag and lazy theorems *)
-fun pretty_lthms ctxt r = case Susp.peek r
+fun pretty_lthms ctxt r = case Lazy.peek r
of SOME thms => map (ProofContext.pretty_thm ctxt o fst) (Exn.release thms)
| NONE => [Pretty.str "[...]"];
fun certificate thy f r =
- case Susp.peek r
- of SOME thms => (Susp.value o f thy) (Exn.release thms)
+ case Lazy.peek r
+ of SOME thms => (Lazy.value o f thy) (Exn.release thms)
| NONE => let
val thy_ref = Theory.check_thy thy;
- in Susp.delay (fn () => (f (Theory.deref thy_ref) o Susp.force) r) end;
+ in Lazy.lazy (fn () => (f (Theory.deref thy_ref) o Lazy.force) r) end;
fun add_drop_redundant thy (thm, linear) thms =
let
@@ -141,13 +141,13 @@
else false;
in (thm, linear) :: filter_out drop thms end;
-fun add_thm thy _ thm (false, thms) = (false, Susp.map_force (add_drop_redundant thy thm) thms)
- | add_thm thy true thm (true, thms) = (true, Susp.map_force (fn thms => thms @ [thm]) thms)
- | add_thm thy false thm (true, thms) = (false, Susp.value [thm]);
+fun add_thm thy _ thm (false, thms) = (false, Lazy.map_force (add_drop_redundant thy thm) thms)
+ | add_thm thy true thm (true, thms) = (true, Lazy.map_force (fn thms => thms @ [thm]) thms)
+ | add_thm thy false thm (true, thms) = (false, Lazy.value [thm]);
fun add_lthms lthms _ = (false, lthms);
-fun del_thm thm = (apsnd o Susp.map_force) (remove (eq_fst Thm.eq_thm_prop) (thm, true));
+fun del_thm thm = (apsnd o Lazy.map_force) (remove (eq_fst Thm.eq_thm_prop) (thm, true));
fun merge_defthms ((true, _), defthms2) = defthms2
| merge_defthms (defthms1 as (false, _), (true, _)) = defthms1
@@ -171,7 +171,7 @@
(* specification data *)
datatype spec = Spec of {
- eqns: (bool * (thm * bool) list Susp.T) Symtab.table,
+ eqns: (bool * (thm * bool) list Lazy.T) Symtab.table,
dtyps: ((string * sort) list * (string * typ list) list) Symtab.table,
cases: (int * string list) Symtab.table * unit Symtab.table
};
@@ -471,7 +471,7 @@
|> maps (map fst o these o try (#params o AxClass.get_info thy))
|> map_filter (fn c => try (AxClass.param_of_inst thy) (c, tyco))
|> map (Symtab.lookup ((the_eqns o the_exec) thy))
- |> (map o Option.map) (map fst o Susp.force o snd)
+ |> (map o Option.map) (map fst o Lazy.force o snd)
|> maps these
|> map (map (snd o dest_TVar) o Sign.const_typargs thy o Code_Unit.const_typ_eqn);
val inter_sorts = map2 (curry (Sorts.inter_sort algebra));
@@ -544,7 +544,7 @@
else ();
in
(map_exec_purge (SOME [c]) o map_eqns) (Symtab.map_default
- (c, (true, Susp.value [])) (add_thm thy default (thm, linear))) thy
+ (c, (true, Lazy.value [])) (add_thm thy default (thm, linear))) thy
end
| NONE => thy;
@@ -559,7 +559,7 @@
| NONE => thy;
fun del_eqns c = map_exec_purge (SOME [c])
- (map_eqns (Symtab.map_entry c (K (false, Susp.value []))));
+ (map_eqns (Symtab.map_entry c (K (false, Lazy.value []))));
fun add_eqnl (c, lthms) thy =
let
@@ -567,7 +567,7 @@
(fn thy => map (Code_Unit.assert_linear) o certify_const thy c) lthms;
in
map_exec_purge (SOME [c])
- (map_eqns (Symtab.map_default (c, (true, Susp.value []))
+ (map_eqns (Symtab.map_default (c, (true, Lazy.value []))
(add_lthms lthms'))) thy
end;
@@ -648,7 +648,7 @@
fun get_eqns thy c =
Symtab.lookup ((the_eqns o the_exec) thy) c
- |> Option.map (Susp.force o snd)
+ |> Option.map (Lazy.force o snd)
|> these
|> (map o apfst) (Thm.transfer thy);
--- a/src/Pure/ML-Systems/install_pp_polyml.ML Thu Oct 23 13:52:28 2008 +0200
+++ b/src/Pure/ML-Systems/install_pp_polyml.ML Thu Oct 23 14:22:16 2008 +0200
@@ -10,9 +10,9 @@
| SOME (Exn.Exn _) => str "<failed>"
| SOME (Exn.Result y) => print (y, depth)));
-install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Susp.T) =>
- (case Susp.peek x of
- NONE => str "<delayed>"
+install_pp (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a Lazy.T) =>
+ (case Lazy.peek x of
+ NONE => str "<lazy>"
| SOME (Exn.Exn _) => str "<failed>"
| SOME (Exn.Result y) => print (y, depth)));
--- a/src/Tools/code/code_ml.ML Thu Oct 23 13:52:28 2008 +0200
+++ b/src/Tools/code/code_ml.ML Thu Oct 23 14:22:16 2008 +0200
@@ -915,8 +915,8 @@
structure CodeAntiqData = ProofDataFun
(
- type T = string list * (bool * (string * (string * (string * string) list) Susp.T));
- fun init _ = ([], (true, ("", Susp.value ("", []))));
+ type T = string list * (bool * (string * (string * (string * string) list) Lazy.T));
+ fun init _ = ([], (true, ("", Lazy.value ("", []))));
);
val is_first_occ = fst o snd o CodeAntiqData.get;
@@ -938,13 +938,13 @@
val (struct_name', ctxt') = if struct_name = ""
then ML_Antiquote.variant "Code" ctxt
else (struct_name, ctxt);
- val acc_code = Susp.delay (delayed_code (ProofContext.theory_of ctxt) consts');
+ val acc_code = Lazy.lazy (delayed_code (ProofContext.theory_of ctxt) consts');
in CodeAntiqData.put (consts', (false, (struct_name', acc_code))) ctxt' end;
fun print_code struct_name is_first const ctxt =
let
val (consts, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
- val (raw_ml_code, consts_map) = Susp.force acc_code;
+ val (raw_ml_code, consts_map) = Lazy.force acc_code;
val const'' = NameSpace.append (NameSpace.append struct_name struct_code_name)
((the o AList.lookup (op =) consts_map) const);
val ml_code = if is_first then "\nstructure " ^ struct_code_name