proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
authorwenzelm
Tue Jan 27 00:29:37 2009 +0100 (2009-01-27)
changeset 2963531d14e9fa0da
parent 29634 2baf1b2f6655
child 29636 d01bada1df33
proof_body: turned lazy into future -- ensures that body is fulfilled eventually, without explicit force;
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Proof/reconstruct.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Tools/xml_syntax.ML
src/Pure/proofterm.ML
     1.1 --- a/src/Pure/Proof/extraction.ML	Mon Jan 26 22:15:35 2009 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Tue Jan 27 00:29:37 2009 +0100
     1.3 @@ -546,7 +546,7 @@
     1.4  
     1.5        | corr d defs vs ts Ts hs (prf0 as PThm (_, ((name, prop, SOME Ts'), body))) _ _ =
     1.6            let
     1.7 -            val prf = force_proof body;
     1.8 +            val prf = join_proof body;
     1.9              val (vs', tye) = find_inst prop Ts ts vs;
    1.10              val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye;
    1.11              val T = etype_of thy' vs' [] prop;
    1.12 @@ -570,7 +570,7 @@
    1.13                        (proof_combt
    1.14                           (PThm (serial (),
    1.15                            ((corr_name name vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
    1.16 -                            Lazy.value (make_proof_body corr_prf))), vfs_of corr_prop))
    1.17 +                            Future.value (make_proof_body corr_prf))), vfs_of corr_prop))
    1.18                        (map (get_var_type corr_prop) (vfs_of prop))
    1.19                    in
    1.20                      ((name, (vs', ((nullt, nullt), (corr_prf, corr_prf')))) :: defs'',
    1.21 @@ -636,7 +636,7 @@
    1.22  
    1.23        | extr d defs vs ts Ts hs (prf0 as PThm (_, ((s, prop, SOME Ts'), body))) =
    1.24            let
    1.25 -            val prf = force_proof body;
    1.26 +            val prf = join_proof body;
    1.27              val (vs', tye) = find_inst prop Ts ts vs;
    1.28              val tye' = (map fst (OldTerm.term_tvars prop) ~~ Ts') @ tye
    1.29            in
    1.30 @@ -681,7 +681,7 @@
    1.31                        (proof_combt
    1.32                          (PThm (serial (),
    1.33                           ((corr_name s vs', corr_prop, SOME (map TVar (OldTerm.term_tvars corr_prop))),
    1.34 -                           Lazy.value (make_proof_body corr_prf'))), vfs_of corr_prop))
    1.35 +                           Future.value (make_proof_body corr_prf'))), vfs_of corr_prop))
    1.36                        (map (get_var_type corr_prop) (vfs_of prop));
    1.37                    in
    1.38                      ((s, (vs', ((t', u), (corr_prf', corr_prf'')))) :: defs'',
     2.1 --- a/src/Pure/Proof/proof_syntax.ML	Mon Jan 26 22:15:35 2009 +0100
     2.2 +++ b/src/Pure/Proof/proof_syntax.ML	Tue Jan 27 00:29:37 2009 +0100
     2.3 @@ -228,7 +228,7 @@
     2.4      val prop = Thm.full_prop_of thm;
     2.5      val prf = Thm.proof_of thm;
     2.6      val prf' = (case strip_combt (fst (strip_combP prf)) of
     2.7 -        (PThm (_, ((_, prop', _), body)), _) => if prop = prop' then force_proof body else prf
     2.8 +        (PThm (_, ((_, prop', _), body)), _) => if prop = prop' then join_proof body else prf
     2.9        | _ => prf)
    2.10    in if full then Reconstruct.reconstruct_proof thy prop prf' else prf' end;
    2.11  
     3.1 --- a/src/Pure/Proof/reconstruct.ML	Mon Jan 26 22:15:35 2009 +0100
     3.2 +++ b/src/Pure/Proof/reconstruct.ML	Tue Jan 27 00:29:37 2009 +0100
     3.3 @@ -358,7 +358,7 @@
     3.4                      val _ = message ("Reconstructing proof of " ^ a);
     3.5                      val _ = message (Syntax.string_of_term_global thy prop);
     3.6                      val prf' = forall_intr_vfs_prf prop
     3.7 -                      (reconstruct_proof thy prop (force_proof body));
     3.8 +                      (reconstruct_proof thy prop (join_proof body));
     3.9                      val (maxidx', prfs', prf) = expand
    3.10                        (maxidx_proof prf' ~1) prfs prf'
    3.11                    in (maxidx' + maxidx + 1, inc (maxidx + 1) prf,
     4.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Jan 26 22:15:35 2009 +0100
     4.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jan 27 00:29:37 2009 +0100
     4.3 @@ -256,7 +256,7 @@
     4.4    (case Thm.proof_body_of th of 
     4.5      PBody {proof = PThm (_, ((name, _, _), body)), ...} =>
     4.6        if Thm.has_name_hint th andalso Thm.get_name_hint th = name
     4.7 -      then add_proof_body (Lazy.force body)
     4.8 +      then add_proof_body (Future.join body)
     4.9        else I
    4.10    | body => add_proof_body body);
    4.11  
     5.1 --- a/src/Pure/Tools/xml_syntax.ML	Mon Jan 26 22:15:35 2009 +0100
     5.2 +++ b/src/Pure/Tools/xml_syntax.ML	Tue Jan 27 00:29:37 2009 +0100
     5.3 @@ -158,7 +158,7 @@
     5.4    | proof_of_xml (XML.Elem ("PThm", [("name", s)], term :: opttypes)) =
     5.5        (* FIXME? *)
     5.6        PThm (serial (), ((s, term_of_xml term, opttypes_of_xml opttypes),
     5.7 -        Lazy.value (Proofterm.make_proof_body MinProof)))
     5.8 +        Future.value (Proofterm.make_proof_body MinProof)))
     5.9    | proof_of_xml (XML.Elem ("PAxm", [("name", s)], term :: opttypes)) =
    5.10        PAxm (s, term_of_xml term, opttypes_of_xml opttypes)
    5.11    | proof_of_xml (XML.Elem ("Oracle", [("name", s)], term :: opttypes)) =
     6.1 --- a/src/Pure/proofterm.ML	Mon Jan 26 22:15:35 2009 +0100
     6.2 +++ b/src/Pure/proofterm.ML	Tue Jan 27 00:29:37 2009 +0100
     6.3 @@ -21,10 +21,10 @@
     6.4     | PAxm of string * term * typ list option
     6.5     | Oracle of string * term * typ list option
     6.6     | Promise of serial * term * typ list
     6.7 -   | PThm of serial * ((string * term * typ list option) * proof_body lazy)
     6.8 +   | PThm of serial * ((string * term * typ list option) * proof_body future)
     6.9    and proof_body = PBody of
    6.10      {oracles: (string * term) OrdList.T,
    6.11 -     thms: (serial * (string * term * proof_body lazy)) OrdList.T,
    6.12 +     thms: (serial * (string * term * proof_body future)) OrdList.T,
    6.13       proof: proof}
    6.14  
    6.15    val %> : proof * term -> proof
    6.16 @@ -35,10 +35,10 @@
    6.17    include BASIC_PROOFTERM
    6.18  
    6.19    type oracle = string * term
    6.20 -  type pthm = serial * (string * term * proof_body lazy)
    6.21 -  val force_body: proof_body lazy ->
    6.22 +  type pthm = serial * (string * term * proof_body future)
    6.23 +  val join_body: proof_body future ->
    6.24      {oracles: oracle OrdList.T, thms: pthm OrdList.T, proof: proof}
    6.25 -  val force_proof: proof_body lazy -> proof
    6.26 +  val join_proof: proof_body future -> proof
    6.27    val proof_of: proof_body -> proof
    6.28    val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
    6.29    val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
    6.30 @@ -142,17 +142,17 @@
    6.31   | PAxm of string * term * typ list option
    6.32   | Oracle of string * term * typ list option
    6.33   | Promise of serial * term * typ list
    6.34 - | PThm of serial * ((string * term * typ list option) * proof_body lazy)
    6.35 + | PThm of serial * ((string * term * typ list option) * proof_body future)
    6.36  and proof_body = PBody of
    6.37    {oracles: (string * term) OrdList.T,
    6.38 -   thms: (serial * (string * term * proof_body lazy)) OrdList.T,
    6.39 +   thms: (serial * (string * term * proof_body future)) OrdList.T,
    6.40     proof: proof};
    6.41  
    6.42  type oracle = string * term;
    6.43 -type pthm = serial * (string * term * proof_body lazy);
    6.44 +type pthm = serial * (string * term * proof_body future);
    6.45  
    6.46 -val force_body = Lazy.force #> (fn PBody args => args);
    6.47 -val force_proof = #proof o force_body;
    6.48 +val join_body = Future.join #> (fn PBody args => args);
    6.49 +val join_proof = #proof o join_body;
    6.50  
    6.51  fun proof_of (PBody {proof, ...}) = proof;
    6.52  
    6.53 @@ -165,7 +165,7 @@
    6.54        if Inttab.defined seen i then (x, seen)
    6.55        else
    6.56          let
    6.57 -          val body' = Lazy.force body;
    6.58 +          val body' = Future.join body;
    6.59            val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
    6.60          in (f (name, prop, body') x', seen') end);
    6.61    in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
    6.62 @@ -180,7 +180,7 @@
    6.63            if Inttab.defined seen i then (x, seen)
    6.64            else
    6.65              let val (x', seen') =
    6.66 -              (if all then app (force_proof body) else I) (x, Inttab.update (i, ()) seen)
    6.67 +              (if all then app (join_proof body) else I) (x, Inttab.update (i, ()) seen)
    6.68              in (f prf x', seen') end)
    6.69        | app prf = (fn (x, seen) => (f prf x, seen));
    6.70    in fn prfs => fn x => #1 (fold app prfs (x, Inttab.empty)) end;
    6.71 @@ -233,7 +233,7 @@
    6.72  
    6.73  fun strip_thm (body as PBody {proof, ...}) =
    6.74    (case strip_combt (fst (strip_combP proof)) of
    6.75 -    (PThm (_, (_, body')), _) => Lazy.force body'
    6.76 +    (PThm (_, (_, body')), _) => Future.join body'
    6.77    | _ => body);
    6.78  
    6.79  val mk_Abst = fold_rev (fn (s, T:typ) => fn prf => Abst (s, NONE, prf));
    6.80 @@ -1245,7 +1245,7 @@
    6.81        else MinProof;
    6.82  
    6.83      fun new_prf () = (serial (), name, prop,
    6.84 -      Lazy.lazy (fn () => fulfill_proof thy (Lazy.force promises)
    6.85 +      Future.fork_pri ~2 (fn () => fulfill_proof thy (Lazy.force promises)
    6.86          (PBody {oracles = oracles0, thms = thms0, proof = proof0})));
    6.87  
    6.88      val (i, name, prop, body') =