--- a/src/HOL/IsaMakefile Thu Oct 01 18:58:47 2009 +0200
+++ b/src/HOL/IsaMakefile Thu Oct 01 18:59:26 2009 +0200
@@ -192,6 +192,7 @@
Tools/sat_funcs.ML \
Tools/sat_solver.ML \
Tools/split_rule.ML \
+ Tools/transfer.ML \
Tools/typecopy.ML \
Tools/typedef_codegen.ML \
Tools/typedef.ML \
@@ -258,12 +259,12 @@
Tools/Qelim/presburger.ML \
Tools/Qelim/qelim.ML \
Tools/recdef.ML \
+ Tools/choice_specification.ML \
Tools/res_atp.ML \
Tools/res_axioms.ML \
Tools/res_clause.ML \
Tools/res_hol_clause.ML \
Tools/res_reconstruct.ML \
- Tools/choice_specification.ML \
Tools/string_code.ML \
Tools/string_syntax.ML \
Tools/TFL/casesplit.ML \
@@ -308,7 +309,6 @@
Taylor.thy \
Transcendental.thy \
Tools/float_syntax.ML \
- Tools/transfer.ML \
Tools/Qelim/ferrante_rackoff_data.ML \
Tools/Qelim/ferrante_rackoff.ML \
Tools/Qelim/langford_data.ML \
--- a/src/HOL/Tools/transfer.ML Thu Oct 01 18:58:47 2009 +0200
+++ b/src/HOL/Tools/transfer.ML Thu Oct 01 18:59:26 2009 +0200
@@ -1,5 +1,5 @@
(* Author: Amine Chaieb, University of Cambridge, 2009
- Jeremy Avigad, Carnegie Mellon University
+ Author: Jeremy Avigad, Carnegie Mellon University
*)
signature TRANSFER =
@@ -14,10 +14,8 @@
structure Transfer : TRANSFER =
struct
-val eq_thm = Thm.eq_thm;
-
type entry = {inj : thm list, emb : thm list, ret : thm list, cong : thm list,
- guess : bool, hints : string list};
+ guess : bool, hints : string list};
type data = simpset * (thm * entry) list;
structure Data = GenericDataFun
@@ -26,36 +24,34 @@
val empty = (HOL_ss, []);
val extend = I;
fun merge _ ((ss1, e1), (ss2, e2)) =
- (merge_ss (ss1, ss2), AList.merge eq_thm (K true) (e1, e2));
+ (merge_ss (ss1, ss2), AList.merge Thm.eq_thm (K true) (e1, e2));
);
val get = Data.get o Context.Proof;
-fun del_data key = apsnd (remove (eq_fst eq_thm) (key, []));
+fun del_data key = apsnd (remove (eq_fst Thm.eq_thm) (key, []));
val del = Thm.declaration_attribute (Data.map o del_data);
-val add_ss = Thm.declaration_attribute
+val add_ss = Thm.declaration_attribute
(fn th => Data.map (fn (ss,data) => (ss addsimps [th], data)));
-val del_ss = Thm.declaration_attribute
+val del_ss = Thm.declaration_attribute
(fn th => Data.map (fn (ss,data) => (ss delsimps [th], data)));
val transM_pat = (Thm.dest_arg1 o Thm.dest_arg o cprop_of) @{thm TransferMorphism_def};
fun merge_update eq m (k,v) [] = [(k,v)]
- | merge_update eq m (k,v) ((k',v')::al) =
+ | merge_update eq m (k,v) ((k',v')::al) =
if eq (k,k') then (k',m (v,v')):: al else (k',v') :: merge_update eq m (k,v) al
-fun C f x y = f y x
-
-fun simpset_of_entry injonly {inj = inj, emb = emb, ret = ret, cong = cg, guess = g, hints = hints} =
+fun simpset_of_entry injonly {inj = inj, emb = emb, ret = ret, cong = cg, guess = g, hints = hints} =
HOL_ss addsimps inj addsimps (if injonly then [] else emb@ret) addcongs cg;
-fun basic_transfer_rule injonly a0 D0 e leave ctxt0 th =
- let
+fun basic_transfer_rule injonly a0 D0 e leave ctxt0 th =
+ let
val ([a,D], ctxt) = apfst (map Drule.dest_term o snd) (Variable.import true (map Drule.mk_term [a0, D0]) ctxt0)
- val (aT,bT) =
- let val T = typ_of (ctyp_of_term a)
+ val (aT,bT) =
+ let val T = typ_of (ctyp_of_term a)
in (Term.range_type T, Term.domain_type T)
end
val ctxt' = (Variable.declare_term (term_of a) o Variable.declare_term (term_of D) o Variable.declare_thm th) ctxt
@@ -65,60 +61,64 @@
val cfis = map ((cterm_of o ProofContext.theory_of) ctxt'' o (fn n => Free (n, bT))) ins
val cis = map (Thm.capply a) cfis
val (hs,ctxt''') = Assumption.add_assumes (map (fn ct => Thm.capply @{cterm "Trueprop"} (Thm.capply D ct)) cfis) ctxt''
- val th1 = Drule.cterm_instantiate (cns~~ cis) th
- val th2 = fold (C implies_elim) hs (fold_rev implies_intr (map cprop_of hs) th1)
- val th3 = Simplifier.asm_full_simplify (Simplifier.context ctxt''' (simpset_of_entry injonly e))
+ val th1 = Drule.cterm_instantiate (cns ~~ cis) th
+ val th2 = fold Thm.elim_implies hs (fold_rev implies_intr (map cprop_of hs) th1)
+ val th3 = Simplifier.asm_full_simplify (Simplifier.context ctxt''' (simpset_of_entry injonly e))
(fold_rev implies_intr (map cprop_of hs) th2)
in hd (Variable.export ctxt''' ctxt0 [th3]) end;
local
-fun transfer_ruleh a D leave ctxt th =
+fun transfer_ruleh a D leave ctxt th =
let val (ss,al) = get ctxt
val a0 = cterm_of (ProofContext.theory_of ctxt) a
val D0 = cterm_of (ProofContext.theory_of ctxt) D
- fun h (th', e) = let val (a',D') = (Thm.dest_binop o Thm.dest_arg o cprop_of) th'
+ fun h (th', e) = let val (a',D') = (Thm.dest_binop o Thm.dest_arg o cprop_of) th'
in if a0 aconvc a' andalso D0 aconvc D' then SOME e else NONE
end
in case get_first h al of
SOME e => basic_transfer_rule false a0 D0 e leave ctxt th
| NONE => error "Transfer: corresponding instance not found in context-data"
end
-in fun transfer_rule (a,D) leave (gctxt,th) =
+in fun transfer_rule (a,D) leave (gctxt,th) =
(gctxt, transfer_ruleh a D leave (Context.proof_of gctxt) th)
end;
fun splits P [] = []
- | splits P (xxs as (x::xs)) =
+ | splits P (xxs as (x::xs)) =
let val pss = filter (P x) xxs
val qss = filter_out (P x) xxs
in if null pss then [qss] else if null qss then [pss] else pss:: splits P qss
end
-fun all_transfers leave (gctxt,th) =
- let
+fun all_transfers leave (gctxt,th) =
+ let
val ctxt = Context.proof_of gctxt
val tys = map snd (Term.add_vars (prop_of th) [])
val _ = if null tys then error "transfer: Unable to guess instance" else ()
- val tyss = splits (curry Type.could_unify) tys
+ val tyss = splits (curry Type.could_unify) tys
val get_ty = typ_of o ctyp_of_term o fst o Thm.dest_binop o Thm.dest_arg o cprop_of
val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
- val insts =
- map_filter (fn tys =>
- get_first (fn (k,ss) => if Type.could_unify (hd tys, range_type (get_ty k))
- then SOME (get_aD k, ss)
- else NONE) (snd (get ctxt))) tyss
- val _ = if null insts then error "Transfer guesser: there were no possible instances, use direction: in order to provide a direction" else ()
+ val insts =
+ map_filter (fn tys =>
+ get_first (fn (k,ss) =>
+ if Type.could_unify (hd tys, range_type (get_ty k))
+ then SOME (get_aD k, ss)
+ else NONE) (snd (get ctxt))) tyss
+ val _ =
+ if null insts then
+ error "Transfer guesser: there were no possible instances, use direction: in order to provide a direction"
+ else ()
val ths = map (fn ((a,D),e) => basic_transfer_rule false a D e leave ctxt th) insts
val cth = Conjunction.intr_balanced ths
in (gctxt, cth)
end;
-fun transfer_rule_by_hint ls leave (gctxt,th) =
- let
+fun transfer_rule_by_hint ls leave (gctxt,th) =
+ let
val ctxt = Context.proof_of gctxt
val get_aD = Thm.dest_binop o Thm.dest_arg o cprop_of
- val insts =
- map_filter (fn (k,e) => if exists (fn l => l mem_string (#hints e)) ls
+ val insts =
+ map_filter (fn (k,e) => if exists (member (op =) (#hints e)) ls
then SOME (get_aD k, e) else NONE)
(snd (get ctxt))
val _ = if null insts then error "Transfer: No labels provided are stored in the context" else ()
@@ -128,53 +128,58 @@
end;
-fun transferred_attribute ls NONE leave =
+fun transferred_attribute ls NONE leave =
if null ls then all_transfers leave else transfer_rule_by_hint ls leave
| transferred_attribute _ (SOME (a,D)) leave = transfer_rule (a,D) leave
- (* Add data to the context *)
+
+(* Add data to the context *)
+
fun gen_merge_entries {inj = inj0, emb = emb0, ret = ret0, cong = cg0, guess = g0, hints = hints0}
- ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
+ ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
{inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2})
- =
+ =
let fun h xs0 xs ys = subtract Thm.eq_thm xs0 (merge Thm.eq_thm (xs,ys)) in
- {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2,
+ {inj = h inj0 inj1 inj2, emb = h emb0 emb1 emb2,
ret = h ret0 ret1 ret2, cong = h cg0 cg1 cg2, guess = g1 andalso g2,
- hints = subtract (op = : string*string -> bool) hints0
+ hints = subtract (op = : string*string -> bool) hints0
(hints1 union_string hints2)}
end;
local
val h = curry (merge Thm.eq_thm)
in
-fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
- {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) =
+fun merge_entries ({inj = inj1, emb = emb1, ret = ret1, cong = cg1, guess = g1, hints = hints1},
+ {inj = inj2, emb = emb2, ret = ret2, cong = cg2, guess = g2, hints = hints2}) =
{inj = h inj1 inj2, emb = h emb1 emb2, ret = h ret1 ret2, cong = h cg1 cg2, guess = g1 andalso g2, hints = hints1 union_string hints2}
-end;
+end;
fun add ((inja,injd), (emba,embd), (reta,retd), (cga,cgd), g, (hintsa, hintsd)) =
Thm.declaration_attribute (fn key => fn context => context |> Data.map
- (fn (ss, al) =>
+ (fn (ss, al) =>
let
- val _ = ((let val _ = Thm.match (transM_pat, (Thm.dest_arg o cprop_of) key)
- in 0 end)
- handle MATCH => error "Attribute expected Theorem of the form : TransferMorphism A a B b")
+ val _ = Thm.match (transM_pat, Thm.dest_arg (Thm.cprop_of key))
+ handle Pattern.MATCH =>
+ error "Attribute expected Theorem of the form : TransferMorphism A a B b"
val e0 = {inj = inja, emb = emba, ret = reta, cong = cga, guess = g, hints = hintsa}
val ed = {inj = injd, emb = embd, ret = retd, cong = cgd, guess = g, hints = hintsd}
- val entry =
- if g then
+ val entry =
+ if g then
let val (a0,D0) = (Thm.dest_binop o Thm.dest_arg o cprop_of) key
val ctxt0 = ProofContext.init (Thm.theory_of_thm key)
- val inj' = if null inja then #inj (case AList.lookup eq_thm al key of SOME e => e | NONE => error "Transfer: can not generate return rules on the fly, either add injectivity axiom or force manual mode with mode: manual")
- else inja
+ val inj' =
+ if null inja then
+ #inj
+ (case AList.lookup Thm.eq_thm al key of SOME e => e
+ | NONE => error "Transfer: can not generate return rules on the fly, either add injectivity axiom or force manual mode with mode: manual")
+ else inja
val ret' = merge Thm.eq_thm (reta, map (fn th => basic_transfer_rule true a0 D0 {inj = inj', emb = [], ret = [], cong = cga, guess = g, hints = hintsa} [] ctxt0 th RS sym) emba)
- in {inj = inja, emb = emba, ret = ret', cong = cga, guess = g, hints = hintsa} end
+ in {inj = inja, emb = emba, ret = ret', cong = cga, guess = g, hints = hintsa} end
else e0
- in (ss, merge_update eq_thm (gen_merge_entries ed) (key, entry) al)
+ in (ss, merge_update Thm.eq_thm (gen_merge_entries ed) (key, entry) al)
end));
-
(* concrete syntax *)
local
@@ -199,7 +204,7 @@
val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat
val terms = thms >> map Drule.dest_term
-val types = thms >> (Logic.dest_type o HOLogic.dest_Trueprop o prop_of o hd)
+val types = thms >> (Logic.dest_type o HOLogic.dest_Trueprop o prop_of o hd)
val name = Scan.lift Args.name
val names = Scan.repeat (Scan.unless any_keyword name)
fun optional scan = Scan.optional scan []
--- a/src/Pure/Concurrent/future.ML Thu Oct 01 18:58:47 2009 +0200
+++ b/src/Pure/Concurrent/future.ML Thu Oct 01 18:59:26 2009 +0200
@@ -30,6 +30,7 @@
type task = Task_Queue.task
type group = Task_Queue.group
val is_worker: unit -> bool
+ val worker_task: unit -> Task_Queue.task option
val worker_group: unit -> Task_Queue.group option
type 'a future
val task_of: 'a future -> task
@@ -71,6 +72,7 @@
end;
val is_worker = is_some o thread_data;
+val worker_task = Option.map #2 o thread_data;
val worker_group = Option.map #3 o thread_data;
@@ -347,7 +349,8 @@
| SOME res => res);
fun join_wait x =
- Synchronized.guarded_access (result_of x) (fn NONE => NONE | some => SOME ((), some));
+ Synchronized.guarded_access (result_of x)
+ (fn NONE => NONE | some => SOME ((), some));
fun join_next deps = (*requires SYNCHRONIZED*)
if null deps then NONE
@@ -357,10 +360,14 @@
| (NONE, deps') => (worker_wait work_finished; join_next deps')
| (SOME work, deps') => SOME (work, deps'));
-fun join_work deps =
- (case SYNCHRONIZED "join" (fn () => join_next deps) of
- NONE => ()
- | SOME (work, deps') => (execute "join" work; join_work deps'));
+fun execute_work NONE = ()
+ | execute_work (SOME (work, deps')) = (execute "join" work; join_work deps')
+and join_work deps =
+ execute_work (SYNCHRONIZED "join" (fn () => join_next deps));
+
+fun join_depend task deps =
+ execute_work (SYNCHRONIZED "join" (fn () =>
+ (Unsynchronized.change queue (Task_Queue.depend task deps); join_next deps)));
in
@@ -368,11 +375,11 @@
if forall is_finished xs then map get_result xs
else if Multithreading.self_critical () then
error "Cannot join future values within critical section"
- else uninterruptible (fn _ => fn () =>
- (if is_worker ()
- then join_work (map task_of xs)
- else List.app join_wait xs;
- map get_result xs)) ();
+ else
+ (case worker_task () of
+ SOME task => join_depend task (map task_of xs)
+ | NONE => List.app join_wait xs;
+ map get_result xs);
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/lazy.ML Thu Oct 01 18:59:26 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;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/lazy_sequential.ML Thu Oct 01 18:59:26 2009 +0200
@@ -0,0 +1,43 @@
+(* Title: Pure/Concurrent/lazy_sequential.ML
+ Author: Florian Haftmann and Makarius, TU Muenchen
+
+Lazy evaluation with memoing (sequential version).
+*)
+
+structure Lazy: LAZY =
+struct
+
+(* datatype *)
+
+datatype 'a expr =
+ Expr of unit -> 'a |
+ Result of 'a Exn.result;
+
+abstype 'a lazy = Lazy of 'a expr Unsynchronized.ref
+with
+
+fun peek (Lazy r) =
+ (case ! r of
+ Expr _ => NONE
+ | Result x => SOME x);
+
+fun lazy e = Lazy (Unsynchronized.ref (Expr e));
+fun value a = Lazy (Unsynchronized.ref (Result (Exn.Result a)));
+
+
+(* force result *)
+
+fun force_result (Lazy r) =
+ (case ! r of
+ Expr e => Exn.capture e ()
+ | Result res => res);
+
+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;
+
--- a/src/Pure/Concurrent/par_list_dummy.ML Thu Oct 01 18:58:47 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(* Title: Pure/Concurrent/par_list_dummy.ML
- Author: Makarius
-
-Dummy version of parallel list combinators -- plain sequential evaluation.
-*)
-
-structure Par_List: PAR_LIST =
-struct
-
-val map = map;
-val get_some = get_first;
-val find_some = find_first;
-val exists = exists;
-val forall = forall;
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/par_list_sequential.ML Thu Oct 01 18:59:26 2009 +0200
@@ -0,0 +1,16 @@
+(* Title: Pure/Concurrent/par_list_sequential.ML
+ Author: Makarius
+
+Dummy version of parallel list combinators -- plain sequential evaluation.
+*)
+
+structure Par_List: PAR_LIST =
+struct
+
+val map = map;
+val get_some = get_first;
+val find_some = find_first;
+val exists = exists;
+val forall = forall;
+
+end;
--- a/src/Pure/Concurrent/synchronized_dummy.ML Thu Oct 01 18:58:47 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,25 +0,0 @@
-(* Title: Pure/Concurrent/synchronized_dummy.ML
- Author: Makarius
-
-Dummy version of state variables -- plain refs for sequential access.
-*)
-
-structure Synchronized: SYNCHRONIZED =
-struct
-
-datatype 'a var = Var of 'a Unsynchronized.ref;
-
-fun var _ x = Var (Unsynchronized.ref x);
-fun value (Var var) = ! var;
-
-fun timed_access (Var var) _ f =
- (case f (! var) of
- SOME (y, x') => (var := x'; SOME y)
- | NONE => Thread.unavailable ());
-
-fun guarded_access var f = the (timed_access var (K NONE) f);
-
-fun change_result var f = guarded_access var (SOME o f);
-fun change var f = change_result var (fn x => ((), f x));
-
-end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/synchronized_sequential.ML Thu Oct 01 18:59:26 2009 +0200
@@ -0,0 +1,27 @@
+(* Title: Pure/Concurrent/synchronized_sequential.ML
+ Author: Makarius
+
+Sequential version of state variables -- plain refs.
+*)
+
+structure Synchronized: SYNCHRONIZED =
+struct
+
+abstype 'a var = Var of 'a Unsynchronized.ref
+with
+
+fun var _ x = Var (Unsynchronized.ref x);
+fun value (Var var) = ! var;
+
+fun timed_access (Var var) _ f =
+ (case f (! var) of
+ SOME (y, x') => (var := x'; SOME y)
+ | NONE => Thread.unavailable ());
+
+fun guarded_access var f = the (timed_access var (K NONE) f);
+
+fun change_result var f = guarded_access var (SOME o f);
+fun change var f = change_result var (fn x => ((), f x));
+
+end;
+end;
--- a/src/Pure/Concurrent/task_queue.ML Thu Oct 01 18:58:47 2009 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Thu Oct 01 18:59:26 2009 +0200
@@ -27,6 +27,7 @@
val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> (task * bool) * queue
val extend: task -> (bool -> bool) -> queue -> queue option
val dequeue: Thread.thread -> queue -> (task * group * (bool -> bool) list) option * queue
+ val depend: task -> task list -> queue -> queue
val dequeue_towards: Thread.thread -> task list -> queue ->
(((task * group * (bool -> bool) list) option * task list) * queue)
val finish: task -> queue -> bool * queue
@@ -101,6 +102,11 @@
fun add_job task dep (jobs: jobs) =
Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs;
+fun add_dep task dep (jobs: jobs) =
+ if Task_Graph.is_edge jobs (task, dep) then
+ raise Fail "Cyclic dependency of future tasks"
+ else add_job task dep jobs;
+
fun get_deps (jobs: jobs) task =
Task_Graph.imm_preds jobs task handle Task_Graph.UNDEF _ => [];
@@ -205,6 +211,9 @@
(* dequeue_towards -- adhoc dependencies *)
+fun depend task deps (Queue {groups, jobs, ...}) =
+ make_queue groups (fold (add_dep task) deps jobs) Unknown;
+
fun dequeue_towards thread deps (queue as Queue {groups, jobs, ...}) =
let
fun ready task =
--- a/src/Pure/General/lazy.ML Thu Oct 01 18:58:47 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;
-
--- a/src/Pure/IsaMakefile Thu Oct 01 18:58:47 2009 +0200
+++ b/src/Pure/IsaMakefile Thu Oct 01 18:59:26 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/par_list_sequential.ML Concurrent/simple_thread.ML \
+ Concurrent/synchronized.ML Concurrent/synchronized_sequential.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 \
--- a/src/Pure/ROOT.ML Thu Oct 01 18:58:47 2009 +0200
+++ b/src/Pure/ROOT.ML Thu Oct 01 18:59:26 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_sequential.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_sequential.ML";
(* fundamental structures *)
--- a/src/Pure/Thy/thm_deps.ML Thu Oct 01 18:58:47 2009 +0200
+++ b/src/Pure/Thy/thm_deps.ML Thu Oct 01 18:59:26 2009 +0200
@@ -40,7 +40,7 @@
path = "",
parents = parents};
in cons entry end;
- val deps = Proofterm.fold_body_thms (add_dep o #2) (map Thm.proof_body_of thms) [];
+ val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
in Present.display_graph (sort_wrt #ID deps) end;
@@ -55,9 +55,10 @@
fold (Facts.fold_static add_fact o PureThy.facts_of) thys []
|> sort_distinct (string_ord o pairself #1);
- val tab = Proofterm.fold_body_thms
- (fn (_, (name, prop, _)) => name <> "" ? Symtab.insert_list (op =) (name, prop))
- (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty;
+ val tab =
+ Proofterm.fold_body_thms
+ (fn (name, prop, _) => name <> "" ? Symtab.insert_list (op =) (name, prop))
+ (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty;
fun is_unused (name, th) =
not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th));
--- a/src/Pure/Thy/thy_info.ML Thu Oct 01 18:58:47 2009 +0200
+++ b/src/Pure/Thy/thy_info.ML Thu Oct 01 18:59:26 2009 +0200
@@ -364,7 +364,7 @@
local
-fun schedule_futures task_graph =
+fun schedule_futures task_graph = uninterruptible (fn _ => fn () =>
let
val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
(case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
@@ -397,7 +397,7 @@
val _ = after_load ();
in [] end handle exn => (kill_thy name; [exn]));
- in ignore (Exn.release_all (map Exn.Exn (rev exns))) end;
+ in ignore (Exn.release_all (map Exn.Exn (rev exns))) end) ();
fun schedule_seq tasks =
Graph.topological_order tasks
--- a/src/Pure/Thy/thy_load.ML Thu Oct 01 18:58:47 2009 +0200
+++ b/src/Pure/Thy/thy_load.ML Thu Oct 01 18:59:26 2009 +0200
@@ -73,7 +73,7 @@
(* check files *)
-fun check_ext exts paths dir src_path =
+fun check_ext exts paths src_path =
let
val path = Path.expand src_path;
val _ = Path.is_current path andalso error "Bad file specification";
@@ -84,15 +84,15 @@
fun try_prfx prfx = get_first (try_ext (Path.append prfx path)) ("" :: exts);
in get_first try_prfx paths end;
-fun check_file dir path = check_ext [] (search_path dir path) dir path;
-fun check_ml dir path = check_ext ml_exts (search_path dir path) dir path;
+fun check_file dir path = check_ext [] (search_path dir path) path;
+fun check_ml dir path = check_ext ml_exts (search_path dir path) path;
fun check_thy dir name =
let
val thy_file = thy_path name;
val paths = search_path dir thy_file;
in
- (case check_ext [] paths dir thy_file of
+ (case check_ext [] paths thy_file of
NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^
" in " ^ commas_quote (map Path.implode paths))
| SOME thy_id => thy_id)
--- a/src/Pure/proofterm.ML Thu Oct 01 18:58:47 2009 +0200
+++ b/src/Pure/proofterm.ML Thu Oct 01 18:59:26 2009 +0200
@@ -40,8 +40,7 @@
val proof_of: proof_body -> proof
val join_proof: proof_body future -> proof
val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
- val fold_body_thms: (serial * (string * term * proof_body) -> 'a -> 'a) ->
- proof_body list -> 'a -> 'a
+ val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
val join_bodies: proof_body list -> unit
val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
@@ -110,7 +109,7 @@
val axm_proof: string -> term -> proof
val oracle_proof: string -> term -> oracle * proof
val promise_proof: theory -> serial -> term -> proof
- val fulfill_proof: theory -> serial -> (serial * proof_body) list -> proof_body -> proof_body
+ val fulfill_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
val thm_proof: theory -> string -> term list -> term ->
(serial * proof_body future) list -> proof_body -> pthm * proof
val get_name: term list -> term -> proof -> string
@@ -182,7 +181,7 @@
let
val body' = Future.join body;
val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
- in (f (i, (name, prop, body')) x', seen') end));
+ in (f (name, prop, body') x', seen') end));
in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
@@ -1279,16 +1278,12 @@
| _ => false));
in Promise (i, prop, map TVar (Term.add_tvars prop [])) end;
-fun fulfill_proof _ _ [] body0 = body0
- | fulfill_proof thy id ps body0 =
+fun fulfill_proof _ [] body0 = body0
+ | fulfill_proof thy ps body0 =
let
val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
- val bodies = map snd ps;
- val _ = fold_body_thms (fn (i, (name, _, _)) => fn () =>
- if i = id then error ("Cyclic reference to theorem " ^ quote name)
- else ()) bodies ();
- val oracles = fold (fn PBody {oracles, ...} => merge_oracles oracles) bodies oracles0;
- val thms = fold (fn PBody {thms, ...} => merge_thms thms) bodies thms0;
+ val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
+ val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
fun fill (Promise (i, prop, Ts)) =
@@ -1300,18 +1295,18 @@
val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
in PBody {oracles = oracles, thms = thms, proof = proof} end;
-fun fulfill_proof_future _ _ [] body = Future.value body
- | fulfill_proof_future thy id promises body =
+fun fulfill_proof_future _ [] body = Future.value body
+ | fulfill_proof_future thy promises body =
Future.fork_deps (map snd promises) (fn () =>
- fulfill_proof thy id (map (apsnd Future.join) promises) body);
+ fulfill_proof thy (map (apsnd Future.join) promises) body);
(***** theorems *****)
-fun thm_proof thy name hyps prop promises body =
+fun thm_proof thy name hyps concl promises body =
let
val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;
- val prop = Logic.list_implies (hyps, prop);
+ val prop = Logic.list_implies (hyps, concl);
val nvs = needed_vars prop;
val args = map (fn (v as Var (ixn, _)) =>
if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @
@@ -1323,9 +1318,7 @@
else MinProof;
val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
- fun new_prf () =
- let val id = serial ()
- in (id, name, prop, fulfill_proof_future thy id promises body0) end;
+ fun new_prf () = (serial (), name, prop, fulfill_proof_future thy promises body0);
val (i, name, prop, body') =
(case strip_combt (fst (strip_combP prf)) of
(PThm (i, ((old_name, prop', NONE), body')), args') =>
--- a/src/Pure/thm.ML Thu Oct 01 18:58:47 2009 +0200
+++ b/src/Pure/thm.ML Thu Oct 01 18:59:26 2009 +0200
@@ -540,7 +540,7 @@
fun raw_body (Thm (Deriv {body, ...}, _)) = body;
fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
- Pt.fulfill_proof (Theory.deref thy_ref) ~1
+ Pt.fulfill_proof (Theory.deref thy_ref)
(map #1 promises ~~ fulfill_bodies (map #2 promises)) body
and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));