--- a/src/Pure/Concurrent/future.ML Mon Sep 28 15:25:43 2009 +0200
+++ b/src/Pure/Concurrent/future.ML Mon Sep 28 21:35:57 2009 +0200
@@ -37,10 +37,11 @@
val peek: 'a future -> 'a Exn.result option
val is_finished: 'a future -> bool
val value: 'a -> 'a future
- val fork: (unit -> 'a) -> 'a future
val fork_group: group -> (unit -> 'a) -> 'a future
+ val fork_deps_pri: 'b future list -> int -> (unit -> 'a) -> 'a future
val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
val fork_pri: int -> (unit -> 'a) -> 'a future
+ val fork: (unit -> 'a) -> 'a future
val join_results: 'a future list -> 'a Exn.result list
val join_result: 'a future -> 'a Exn.result
val join: 'a future -> 'a
@@ -322,10 +323,11 @@
in task end);
in Future {task = task, group = group, result = result} end;
-fun fork e = fork_future NONE [] 0 e;
fun fork_group group e = fork_future (SOME group) [] 0 e;
-fun fork_deps deps e = fork_future NONE (map task_of deps) 0 e;
-fun fork_pri pri e = fork_future NONE [] pri e;
+fun fork_deps_pri deps pri e = fork_future NONE (map task_of deps) pri e;
+fun fork_deps deps e = fork_deps_pri deps 0 e;
+fun fork_pri pri e = fork_deps_pri [] pri e;
+fun fork e = fork_deps [] e;
(* join *)
--- a/src/Pure/Thy/thm_deps.ML Mon Sep 28 15:25:43 2009 +0200
+++ b/src/Pure/Thy/thm_deps.ML Mon Sep 28 21:35:57 2009 +0200
@@ -40,7 +40,7 @@
path = "",
parents = parents};
in cons entry end;
- val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
+ val deps = Proofterm.fold_body_thms (add_dep o #2) (map Thm.proof_body_of thms) [];
in Present.display_graph (sort_wrt #ID deps) end;
@@ -56,7 +56,7 @@
|> sort_distinct (string_ord o pairself #1);
val tab = Proofterm.fold_body_thms
- (fn (name, prop, _) => name <> "" ? Symtab.insert_list (op =) (name, prop))
+ (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/proofterm.ML Mon Sep 28 15:25:43 2009 +0200
+++ b/src/Pure/proofterm.ML Mon Sep 28 21:35:57 2009 +0200
@@ -40,7 +40,8 @@
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: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
+ val fold_body_thms: (serial * (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}
@@ -109,7 +110,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 * proof_body) list -> proof_body -> proof_body
+ val fulfill_proof: theory -> serial -> (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
@@ -173,19 +174,16 @@
fun fold_body_thms f =
let
- fun app path (PBody {thms, ...}) =
+ fun app (PBody {thms, ...}) =
(Future.join_results (map (#3 o #2) thms);
thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
- if Inttab.defined path i then
- error ("Cyclic reference to theorem " ^ quote name)
- else if Inttab.defined seen i then (x, seen)
+ if Inttab.defined seen i then (x, seen)
else
let
val body' = Future.join body;
- val path' = Inttab.update (i, ()) path;
- val (x', seen') = app path' body' (x, Inttab.update (i, ()) seen);
- in (f (name, prop, body') x', seen') end));
- in fn bodies => fn x => #1 (fold (app Inttab.empty) bodies (x, Inttab.empty)) end;
+ val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
+ in (f (i, (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 ();
@@ -1281,12 +1279,16 @@
| _ => false));
in Promise (i, prop, map TVar (Term.add_tvars prop [])) end;
-fun fulfill_proof _ [] body0 = body0
- | fulfill_proof thy ps body0 =
+fun fulfill_proof _ _ [] body0 = body0
+ | fulfill_proof thy id ps body0 =
let
val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
- val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
- val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
+ 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 proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
fun fill (Promise (i, prop, Ts)) =
@@ -1298,10 +1300,10 @@
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 promises body =
+fun fulfill_proof_future _ _ [] body = Future.value body
+ | fulfill_proof_future thy id promises body =
Future.fork_deps (map snd promises) (fn () =>
- fulfill_proof thy (map (apsnd Future.join) promises) body);
+ fulfill_proof thy id (map (apsnd Future.join) promises) body);
(***** theorems *****)
@@ -1321,7 +1323,9 @@
else MinProof;
val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
- fun new_prf () = (serial (), name, prop, fulfill_proof_future thy promises body0);
+ fun new_prf () =
+ let val id = serial ()
+ in (id, name, prop, fulfill_proof_future thy id promises body0) end;
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 Mon Sep 28 15:25:43 2009 +0200
+++ b/src/Pure/thm.ML Mon Sep 28 21:35:57 2009 +0200
@@ -124,6 +124,13 @@
val hyps_of: thm -> term list
val no_prems: thm -> bool
val major_prem_of: thm -> term
+ val join_proofs: thm list -> unit
+ val proof_body_of: thm -> proof_body
+ val proof_of: thm -> proof
+ val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
+ val future: thm future -> cterm -> thm
+ val get_name: thm -> string
+ val put_name: string -> thm -> thm
val axiom: theory -> string -> thm
val axioms_of: theory -> (string * thm) list
val get_tags: thm -> Properties.T
@@ -142,13 +149,6 @@
val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
val rename_boundvars: term -> term -> thm -> thm
- val join_proofs: thm list -> unit
- val proof_body_of: thm -> proof_body
- val proof_of: thm -> proof
- val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
- val future: thm future -> cterm -> thm
- val get_name: thm -> string
- val put_name: string -> thm -> thm
val extern_oracles: theory -> xstring list
val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
end;
@@ -505,7 +505,7 @@
-(** derivations **)
+(** derivations and promised proofs **)
fun make_deriv promises oracles thms proof =
Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}};
@@ -536,6 +536,93 @@
fun deriv_rule0 prf = deriv_rule1 I (make_deriv [] [] [] prf);
+(* fulfilled proofs *)
+
+fun raw_body (Thm (Deriv {body, ...}, _)) = body;
+
+fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
+ Pt.fulfill_proof (Theory.deref thy_ref) ~1
+ (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
+and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
+
+val join_proofs = Pt.join_bodies o map fulfill_body;
+
+fun proof_body_of thm = (Pt.join_bodies [raw_body thm]; fulfill_body thm);
+val proof_of = Pt.proof_of o proof_body_of;
+
+
+(* derivation status *)
+
+fun status_of (Thm (Deriv {promises, body}, _)) =
+ let
+ val ps = map (Future.peek o snd) promises;
+ val bodies = body ::
+ map_filter (fn SOME (Exn.Result th) => SOME (raw_body th) | _ => NONE) ps;
+ val {oracle, unfinished, failed} = Pt.status_of bodies;
+ in
+ {oracle = oracle,
+ unfinished = unfinished orelse exists is_none ps,
+ failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps}
+ end;
+
+
+(* future rule *)
+
+fun future_result i orig_thy orig_shyps orig_prop raw_thm =
+ let
+ val _ = Theory.check_thy orig_thy;
+ val thm = strip_shyps (transfer orig_thy raw_thm);
+ val _ = Theory.check_thy orig_thy;
+ fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
+
+ val Thm (Deriv {promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
+ val _ = prop aconv orig_prop orelse err "bad prop";
+ val _ = null tpairs orelse err "bad tpairs";
+ val _ = null hyps orelse err "bad hyps";
+ val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
+ val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
+ val _ = fulfill_bodies (map #2 promises);
+ in thm end;
+
+fun future future_thm ct =
+ let
+ val Cterm {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = ct;
+ val thy = Context.reject_draft (Theory.deref thy_ref);
+ val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
+
+ val i = serial ();
+ val future = future_thm |> Future.map (future_result i thy sorts prop);
+ in
+ Thm (make_deriv [(i, future)] [] [] (Pt.promise_proof thy i prop),
+ {thy_ref = thy_ref,
+ tags = [],
+ maxidx = maxidx,
+ shyps = sorts,
+ hyps = [],
+ tpairs = [],
+ prop = prop})
+ end;
+
+
+(* closed derivations with official name *)
+
+fun get_name thm =
+ Pt.get_name (hyps_of thm) (prop_of thm) (Pt.proof_of (raw_body thm));
+
+fun put_name name (thm as Thm (der, args)) =
+ let
+ val Deriv {promises, body} = der;
+ val {thy_ref, hyps, prop, tpairs, ...} = args;
+ val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
+
+ val ps = map (apsnd (Future.map proof_body_of)) promises;
+ val thy = Theory.deref thy_ref;
+ val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
+ val der' = make_deriv [] [] [pthm] proof;
+ val _ = Theory.check_thy thy;
+ in Thm (der', args) end;
+
+
(** Axioms **)
@@ -1610,96 +1697,6 @@
-(*** Future theorems -- proofs with promises ***)
-
-(* fulfilled proofs *)
-
-fun raw_body (Thm (Deriv {body, ...}, _)) = body;
-
-fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
- 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));
-
-val join_proofs = Pt.join_bodies o map fulfill_body;
-
-fun proof_body_of thm = (Pt.join_bodies [raw_body thm]; fulfill_body thm);
-val proof_of = Pt.proof_of o proof_body_of;
-
-
-(* derivation status *)
-
-fun status_of (Thm (Deriv {promises, body}, _)) =
- let
- val ps = map (Future.peek o snd) promises;
- val bodies = body ::
- map_filter (fn SOME (Exn.Result th) => SOME (raw_body th) | _ => NONE) ps;
- val {oracle, unfinished, failed} = Pt.status_of bodies;
- in
- {oracle = oracle,
- unfinished = unfinished orelse exists is_none ps,
- failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps}
- end;
-
-
-(* future rule *)
-
-fun future_result i orig_thy orig_shyps orig_prop raw_thm =
- let
- val _ = Theory.check_thy orig_thy;
- val thm = strip_shyps (transfer orig_thy raw_thm);
- val _ = Theory.check_thy orig_thy;
- fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
-
- val Thm (Deriv {promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
- val _ = prop aconv orig_prop orelse err "bad prop";
- val _ = null tpairs orelse err "bad tpairs";
- val _ = null hyps orelse err "bad hyps";
- val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
- val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
- val _ = fulfill_bodies (map #2 promises);
- in thm end;
-
-fun future future_thm ct =
- let
- val Cterm {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = ct;
- val thy = Context.reject_draft (Theory.deref thy_ref);
- val _ = T <> propT andalso raise CTERM ("future: prop expected", [ct]);
-
- val i = serial ();
- val future = future_thm |> Future.map (future_result i thy sorts prop);
- in
- Thm (make_deriv [(i, future)] [] [] (Pt.promise_proof thy i prop),
- {thy_ref = thy_ref,
- tags = [],
- maxidx = maxidx,
- shyps = sorts,
- hyps = [],
- tpairs = [],
- prop = prop})
- end;
-
-
-(* closed derivations with official name *)
-
-fun get_name thm =
- Pt.get_name (hyps_of thm) (prop_of thm) (Pt.proof_of (raw_body thm));
-
-fun put_name name (thm as Thm (der, args)) =
- let
- val Deriv {promises, body} = der;
- val {thy_ref, hyps, prop, tpairs, ...} = args;
- val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
-
- val ps = map (apsnd (Future.map proof_body_of)) promises;
- val thy = Theory.deref thy_ref;
- val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
- val der' = make_deriv [] [] [pthm] proof;
- val _ = Theory.check_thy thy;
- in Thm (der', args) end;
-
-
-
(*** Oracles ***)
(* oracle rule *)