# HG changeset patch # User wenzelm # Date 1233012577 -3600 # Node ID 31d14e9fa0da952c0efa2825e56eb609477a7516 # Parent 2baf1b2f6655151d608182d2b36cc5e9d586c871 proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force; diff -r 2baf1b2f6655 -r 31d14e9fa0da src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Mon Jan 26 22:15:35 2009 +0100 +++ b/src/Pure/Proof/extraction.ML Tue Jan 27 00:29:37 2009 +0100 @@ -546,7 +546,7 @@ | corr d defs vs ts Ts hs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ = let - val prf = force_proof body; + val prf = join_proof body; val (vs', tye) = find_inst prop Ts ts vs; val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye; val T = etype_of thy' vs' [] prop; @@ -570,7 +570,7 @@ (proof_combt (PThm (serial (), ((corr_name name vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))), - Lazy.value (make_proof_body corr_prf))), vfs_of corr_prop)) + Future.value (make_proof_body corr_prf))), vfs_of corr_prop)) (map (get_var_type corr_prop) (vfs_of prop)) in ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'', @@ -636,7 +636,7 @@ | extr d defs vs ts Ts hs (prf0 as PThm (_, ((s, prop, SOME Ts'), body))) = let - val prf = force_proof body; + val prf = join_proof body; val (vs', tye) = find_inst prop Ts ts vs; val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye in @@ -681,7 +681,7 @@ (proof_combt (PThm (serial (), ((corr_name s vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))), - Lazy.value (make_proof_body corr_prf'))), vfs_of corr_prop)) + Future.value (make_proof_body corr_prf'))), vfs_of corr_prop)) (map (get_var_type corr_prop) (vfs_of prop)); in ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'', diff -r 2baf1b2f6655 -r 31d14e9fa0da src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Mon Jan 26 22:15:35 2009 +0100 +++ b/src/Pure/Proof/proof_syntax.ML Tue Jan 27 00:29:37 2009 +0100 @@ -228,7 +228,7 @@ val prop = Thm.full_prop_of thm; val prf = Thm.proof_of thm; val prf' = (case strip_combt (fst (strip_combP prf)) of - (PThm (_, ((_, prop', _), body)), _) => if prop = prop' then force_proof body else prf + (PThm (_, ((_, prop', _), body)), _) => if prop = prop' then join_proof body else prf | _ => prf) in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end; diff -r 2baf1b2f6655 -r 31d14e9fa0da src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Mon Jan 26 22:15:35 2009 +0100 +++ b/src/Pure/Proof/reconstruct.ML Tue Jan 27 00:29:37 2009 +0100 @@ -358,7 +358,7 @@ val _ = message ("Reconstructing proof of " ^ a); val _ = message (Syntax.string_of_term_global thy prop); val prf' = forall_intr_vfs_prf prop - (reconstruct_proof thy prop (force_proof body)); + (reconstruct_proof thy prop (join_proof body)); val (maxidx', prfs', prf) = expand (maxidx_proof prf' ~1) prfs prf' in (maxidx' + maxidx + 1, inc (maxidx + 1) prf, diff -r 2baf1b2f6655 -r 31d14e9fa0da src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Mon Jan 26 22:15:35 2009 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Jan 27 00:29:37 2009 +0100 @@ -256,7 +256,7 @@ (case Thm.proof_body_of th of PBody {proof = PThm (_, ((name, _, _), body)), ...} => if Thm.has_name_hint th andalso Thm.get_name_hint th = name - then add_proof_body (Lazy.force body) + then add_proof_body (Future.join body) else I | body => add_proof_body body); diff -r 2baf1b2f6655 -r 31d14e9fa0da src/Pure/Tools/xml_syntax.ML --- a/src/Pure/Tools/xml_syntax.ML Mon Jan 26 22:15:35 2009 +0100 +++ b/src/Pure/Tools/xml_syntax.ML Tue Jan 27 00:29:37 2009 +0100 @@ -158,7 +158,7 @@ | proof_of_xml (XML.Elem ("PThm", [("name", s)], term :: opttypes)) = (* FIXME? *) PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes), - Lazy.value (Proofterm.make_proof_body MinProof))) + Future.value (Proofterm.make_proof_body MinProof))) | proof_of_xml (XML.Elem ("PAxm", [("name", s)], term :: opttypes)) = PAxm (s, term_of_xml term, opttypes_of_xml opttypes) | proof_of_xml (XML.Elem ("Oracle", [("name", s)], term :: opttypes)) = diff -r 2baf1b2f6655 -r 31d14e9fa0da src/Pure/proofterm.ML --- a/src/Pure/proofterm.ML Mon Jan 26 22:15:35 2009 +0100 +++ b/src/Pure/proofterm.ML Tue Jan 27 00:29:37 2009 +0100 @@ -21,10 +21,10 @@ | PAxm of string * term * typ list option | Oracle of string * term * typ list option | Promise of serial * term * typ list - | PThm of serial * ((string * term * typ list option) * proof_body lazy) + | PThm of serial * ((string * term * typ list option) * proof_body future) and proof_body = PBody of {oracles: (string * term) OrdList.T, - thms: (serial * (string * term * proof_body lazy)) OrdList.T, + thms: (serial * (string * term * proof_body future)) OrdList.T, proof: proof} val %> : proof * term -> proof @@ -35,10 +35,10 @@ include BASIC_PROOFTERM type oracle = string * term - type pthm = serial * (string * term * proof_body lazy) - val force_body: proof_body lazy -> + type pthm = serial * (string * term * proof_body future) + val join_body: proof_body future -> {oracles: oracle OrdList.T, thms: pthm OrdList.T, proof: proof} - val force_proof: proof_body lazy -> proof + val join_proof: proof_body future -> proof val proof_of: proof_body -> proof val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a @@ -142,17 +142,17 @@ | PAxm of string * term * typ list option | Oracle of string * term * typ list option | Promise of serial * term * typ list - | PThm of serial * ((string * term * typ list option) * proof_body lazy) + | PThm of serial * ((string * term * typ list option) * proof_body future) and proof_body = PBody of {oracles: (string * term) OrdList.T, - thms: (serial * (string * term * proof_body lazy)) OrdList.T, + thms: (serial * (string * term * proof_body future)) OrdList.T, proof: proof}; type oracle = string * term; -type pthm = serial * (string * term * proof_body lazy); +type pthm = serial * (string * term * proof_body future); -val force_body = Lazy.force #> (fn PBody args => args); -val force_proof = #proof o force_body; +val join_body = Future.join #> (fn PBody args => args); +val join_proof = #proof o join_body; fun proof_of (PBody {proof, ...}) = proof; @@ -165,7 +165,7 @@ if Inttab.defined seen i then (x, seen) else let - val body' = Lazy.force body; + val body' = Future.join body; val (x', seen') = app body' (x, Inttab.update (i, ()) seen); in (f (name, prop, body') x', seen') end); in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end; @@ -180,7 +180,7 @@ if Inttab.defined seen i then (x, seen) else let val (x', seen') = - (if all then app (force_proof body) else I) (x, Inttab.update (i, ()) seen) + (if all then app (join_proof body) else I) (x, Inttab.update (i, ()) seen) in (f prf x', seen') end) | app prf = (fn (x, seen) => (f prf x, seen)); in fn prfs => fn x => #1 (fold app prfs (x, Inttab.empty)) end; @@ -233,7 +233,7 @@ fun strip_thm (body as PBody {proof, ...}) = (case strip_combt (fst (strip_combP proof)) of - (PThm (_, (_, body')), _) => Lazy.force body' + (PThm (_, (_, body')), _) => Future.join body' | _ => body); val mk_Abst = fold_rev (fn (s, T:typ) => fn prf => Abst (s, NONE, prf)); @@ -1245,7 +1245,7 @@ else MinProof; fun new_prf () = (serial (), name, prop, - Lazy.lazy (fn () => fulfill_proof thy (Lazy.force promises) + Future.fork_pri ~2 (fn () => fulfill_proof thy (Lazy.force promises) (PBody {oracles = oracles0, thms = thms0, proof = proof0}))); val (i, name, prop, body') =