# HG changeset patch # User wenzelm # Date 1254166557 -7200 # Node ID d5de73f4bcb80f2e6709cc2851f6d1efe3cca10b # Parent f7ed14d60818256362ea24b26828c5bd4a7c1d25# Parent a900d3cd47ccb68753b576b9ffa7b74d065ca9a2 merged diff -r f7ed14d60818 -r d5de73f4bcb8 src/Pure/Concurrent/future.ML --- 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 *) diff -r f7ed14d60818 -r d5de73f4bcb8 src/Pure/Thy/thm_deps.ML --- 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)); diff -r f7ed14d60818 -r d5de73f4bcb8 src/Pure/proofterm.ML --- 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') => diff -r f7ed14d60818 -r d5de73f4bcb8 src/Pure/thm.ML --- 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 *)