# HG changeset patch # User wenzelm # Date 1226781085 -3600 # Node ID 5d3b1df16353721ae2e32e324e40840da4698d3b # Parent d90258bbb18fbab700977db076fa1d42a0a6e03a refined notion of derivation, consiting of promises and proof_body; removed oracle_of (would require detailed check wrt. promises); proof_of returns proof_body; diff -r d90258bbb18f -r 5d3b1df16353 src/Pure/thm.ML --- a/src/Pure/thm.ML Sat Nov 15 21:31:23 2008 +0100 +++ b/src/Pure/thm.ML Sat Nov 15 21:31:25 2008 +0100 @@ -121,11 +121,6 @@ val adjust_maxidx_cterm: int -> cterm -> cterm val capply: cterm -> cterm -> cterm val cabs: cterm -> cterm -> cterm - val rep_deriv: thm -> - {oracle: bool, - proof: Proofterm.proof, - promises: (serial * thm Future.T) OrdList.T} - val oracle_of: thm -> bool val major_prem_of: thm -> term val no_prems: thm -> bool val terms_of_tpairs: (term * term) list -> term list @@ -153,7 +148,7 @@ val freezeT: thm -> thm val join_futures: theory -> unit val future: (unit -> thm) -> cterm -> thm - val proof_of: thm -> Proofterm.proof + val proof_of: thm -> proof_body val extern_oracles: theory -> xstring list val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory end; @@ -350,9 +345,9 @@ tpairs: (term * term) list, (*flex-flex pairs*) prop: term} (*conclusion*) and deriv = Deriv of - {oracle: bool, (*oracle occurrence flag*) - proof: Pt.proof, (*proof term*) - promises: (serial * thm Future.T) OrdList.T}; (*promised derivations*) + {all_promises: (serial * thm Future.T) OrdList.T, + promises: (serial * thm Future.T) OrdList.T, + body: Pt.proof_body}; type conv = cterm -> thm; @@ -399,8 +394,8 @@ (* basic components *) -fun rep_deriv (Thm (Deriv args, _)) = args; -val oracle_of = #oracle o rep_deriv; +fun deriv_of (Thm (Deriv der, _)) = der; +val proof_term_of = Proofterm.proof_of o #body o deriv_of; val theory_of_thm = Theory.deref o #thy_ref o rep_thm; val maxidx_of = #maxidx o rep_thm; @@ -508,10 +503,12 @@ (** derivations **) -fun make_deriv oracle promises proof = - Deriv {oracle = oracle, promises = promises, proof = proof}; +fun make_deriv all_promises promises oracles thms proof = + Deriv {all_promises = all_promises, promises = promises, + body = PBody {oracles = oracles, thms = thms, proof = proof}}; -val empty_deriv = make_deriv false [] Pt.min_proof; +val closed_deriv = make_deriv [] [] [] []; +val empty_deriv = closed_deriv Pt.MinProof; (* inference rules *) @@ -519,23 +516,25 @@ fun promise_ord ((i, _), (j, _)) = int_ord (j, i); fun deriv_rule2 f - (Deriv {oracle = ora1, promises = ps1, proof = prf1}) - (Deriv {oracle = ora2, promises = ps2, proof = prf2}) = + (Deriv {all_promises = all_ps1, promises = ps1, + body = PBody {oracles = oras1, thms = thms1, proof = prf1}}) + (Deriv {all_promises = all_ps2, promises = ps2, + body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) = let - val ora = ora1 orelse ora2; + val all_ps = OrdList.union promise_ord all_ps1 all_ps2; val ps = OrdList.union promise_ord ps1 ps2; + val oras = Pt.merge_oracles oras1 oras2; + val thms = Pt.merge_thms thms1 thms2; val prf = (case ! Pt.proofs of 2 => f prf1 prf2 - | 1 => MinProof (([], [], []) |> Pt.mk_min_proof prf1 |> Pt.mk_min_proof prf2) - | 0 => - if ora then MinProof ([], [], [] |> Pt.add_oracles ora1 prf1 |> Pt.add_oracles ora2 prf2) - else Pt.min_proof + | 1 => MinProof + | 0 => MinProof | i => error ("Illegal level of detail for proof objects: " ^ string_of_int i)); - in make_deriv ora ps prf end; + in make_deriv all_ps ps oras thms prf end; fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv; -fun deriv_rule0 prf = deriv_rule1 I (make_deriv false [] prf); +fun deriv_rule0 prf = deriv_rule1 I (closed_deriv prf); @@ -573,19 +572,7 @@ map (fn s => (s, axiom thy s)) (Symtab.keys (Theory.axiom_table thy)); -(* official name and additional tags *) - -fun get_name (Thm (Deriv {proof, ...}, {hyps, prop, ...})) = Pt.get_name hyps prop proof; - -fun put_name name thm = - let - val Thm (Deriv {oracle, promises, proof}, args as {thy_ref, hyps, prop, tpairs, ...}) = thm; - val _ = null tpairs orelse raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]); - val thy = Theory.deref thy_ref; - val der' = make_deriv oracle promises (Pt.thm_proof thy name hyps prop proof); - val _ = Theory.check_thy thy; - in Thm (der', args) end; - +(* tags *) val get_tags = #tags o rep_thm; @@ -1641,12 +1628,12 @@ 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 Thm (Deriv {all_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, _) => j < i) promises orelse err "bad dependencies"; + val _ = forall (fn (j, _) => j < i) all_promises orelse err "bad dependencies"; in thm end; fun future make_result ct = @@ -1658,8 +1645,9 @@ val i = serial (); val future = Future.fork_background (future_result i thy sorts prop o make_result); val _ = add_future thy future; + val promises = [(i, future)]; in - Thm (make_deriv false [(i, future)] (Pt.promise_proof i prop), + Thm (make_deriv promises promises [] [] (Pt.promise_proof i prop), {thy_ref = thy_ref, tags = [], maxidx = maxidx, @@ -1670,18 +1658,34 @@ end; -(* join_deriv *) +(* fulfilled proof *) -fun join_deriv (thm as Thm (Deriv {oracle, proof, promises}, args)) = +fun proof_of thm = let - val _ = Exn.release_all (Future.join_results (rev (map #2 promises))); - val results = map (apsnd Future.join) promises; - val proofs = fold (fn (i, Thm (Deriv {proof = prf, ...}, _)) => Inttab.update (i, prf)) - results Inttab.empty; - val ora = oracle orelse exists (oracle_of o #2) results; - in Thm (make_deriv ora [] (Pt.fulfill proofs proof), args) end; + val {all_promises, promises, body} = deriv_of thm; + val _ = Exn.release_all (map (Future.join_result o #2) (rev all_promises)); + val ps = map (apsnd (Lazy.value o proof_term_of o Future.join)) promises; + in Pt.fulfill_proof ps body end; + + +(* closed derivations with official name *) + +fun get_name thm = + Pt.get_name (hyps_of thm) (prop_of thm) (proof_term_of thm); -val proof_of = join_deriv #> (fn Thm (Deriv {proof, ...}, _) => proof); +fun put_name name (thm as Thm (der, args)) = + let + val Deriv {all_promises, promises, body} = der; + val {thy_ref, hyps, prop, tpairs, ...} = args; + val _ = null tpairs orelse raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]); + + val ps = + map (apsnd (fn future => Lazy.lazy (fn () => proof_term_of (Future.join future)))) 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; @@ -1694,14 +1698,16 @@ if T <> propT then raise THM ("Oracle's result must have type prop: " ^ name, 0, []) else - Thm (make_deriv true [] (Pt.oracle_proof name prop), - {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2), - tags = [], - maxidx = maxidx, - shyps = sorts, - hyps = [], - tpairs = [], - prop = prop}) + let val prf = Pt.oracle_proof name prop in + Thm (make_deriv [] [] (Pt.make_oracles prf) [] prf, + {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2), + tags = [], + maxidx = maxidx, + shyps = sorts, + hyps = [], + tpairs = [], + prop = prop}) + end end;