# HG changeset patch # User wenzelm # Date 1254400070 -7200 # Node ID f3466a5645fa05cdf109169f11dd6b2347002158 # Parent e72347dd3e647538272028b87deeb65b3618f32a back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc) -- the cycle check is implicit in the future computation of join_proofs; diff -r e72347dd3e64 -r f3466a5645fa src/Pure/Thy/thm_deps.ML --- a/src/Pure/Thy/thm_deps.ML Thu Oct 01 14:11:28 2009 +0200 +++ b/src/Pure/Thy/thm_deps.ML Thu Oct 01 14:27:50 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)); diff -r e72347dd3e64 -r f3466a5645fa src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Thu Oct 01 14:11:28 2009 +0200 +++ b/src/Pure/proofterm.ML Thu Oct 01 14:27:50 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') => diff -r e72347dd3e64 -r f3466a5645fa src/Pure/thm.ML --- a/src/Pure/thm.ML Thu Oct 01 14:11:28 2009 +0200 +++ b/src/Pure/thm.ML Thu Oct 01 14:27:50 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));