# HG changeset patch # User wenzelm # Date 1254163925 -7200 # Node ID a900d3cd47ccb68753b576b9ffa7b74d065ca9a2 # Parent 57e29093ecfbf7a6912c7d13ca987d945235ab1b fold_body_thms: pass pthm identifier; fold_body_thms: dismiss path-etic attempt to check for cycles (cf. e24acd21e60e) -- could be masked by "seen"; fulfill_proof/thm_proof: check for thm cycles at the substitution point; diff -r 57e29093ecfb -r a900d3cd47cc src/Pure/Thy/thm_deps.ML --- a/src/Pure/Thy/thm_deps.ML Mon Sep 28 12:09:55 2009 +0200 +++ b/src/Pure/Thy/thm_deps.ML Mon Sep 28 20:52:05 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 57e29093ecfb -r a900d3cd47cc src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Mon Sep 28 12:09:55 2009 +0200 +++ b/src/Pure/proofterm.ML Mon Sep 28 20:52:05 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 57e29093ecfb -r a900d3cd47cc src/Pure/thm.ML --- a/src/Pure/thm.ML Mon Sep 28 12:09:55 2009 +0200 +++ b/src/Pure/thm.ML Mon Sep 28 20:52:05 2009 +0200 @@ -541,7 +541,7 @@ fun raw_body (Thm (Deriv {body, ...}, _)) = body; fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) = - Pt.fulfill_proof (Theory.deref 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));