src/Pure/thm.ML
changeset 28996 01918abaa9e7
parent 28992 c4ae153d78ab
child 29003 d8d3cbbb6fcc
     1.1 --- a/src/Pure/thm.ML	Fri Dec 05 18:15:52 2008 +0100
     1.2 +++ b/src/Pure/thm.ML	Fri Dec 05 20:38:40 2008 +0100
     1.3 @@ -346,7 +346,8 @@
     1.4    tpairs: (term * term) list,                   (*flex-flex pairs*)
     1.5    prop: term}                                   (*conclusion*)
     1.6  and deriv = Deriv of
     1.7 - {all_promises: (serial * thm future) OrdList.T,
     1.8 + {max_promise: serial,
     1.9 +  open_promises: (serial * thm future) OrdList.T,
    1.10    promises: (serial * thm future) OrdList.T,
    1.11    body: Pt.proof_body};
    1.12  
    1.13 @@ -501,12 +502,11 @@
    1.14  
    1.15  (** derivations **)
    1.16  
    1.17 -fun make_deriv all_promises promises oracles thms proof =
    1.18 -  Deriv {all_promises = all_promises, promises = promises,
    1.19 +fun make_deriv max_promise open_promises promises oracles thms proof =
    1.20 +  Deriv {max_promise = max_promise, open_promises = open_promises, promises = promises,
    1.21      body = PBody {oracles = oracles, thms = thms, proof = proof}};
    1.22  
    1.23 -val closed_deriv = make_deriv [] [] [] [];
    1.24 -val empty_deriv = closed_deriv Pt.MinProof;
    1.25 +val empty_deriv = make_deriv ~1 [] [] [] [] Pt.MinProof;
    1.26  
    1.27  
    1.28  (* inference rules *)
    1.29 @@ -514,12 +514,13 @@
    1.30  fun promise_ord ((i, _), (j, _)) = int_ord (j, i);
    1.31  
    1.32  fun deriv_rule2 f
    1.33 -    (Deriv {all_promises = all_ps1, promises = ps1,
    1.34 +    (Deriv {max_promise = max1, open_promises = open_ps1, promises = ps1,
    1.35        body = PBody {oracles = oras1, thms = thms1, proof = prf1}})
    1.36 -    (Deriv {all_promises = all_ps2, promises = ps2,
    1.37 +    (Deriv {max_promise = max2, open_promises = open_ps2, promises = ps2,
    1.38        body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
    1.39    let
    1.40 -    val all_ps = OrdList.union promise_ord all_ps1 all_ps2;
    1.41 +    val max = Int.max (max1, max2);
    1.42 +    val open_ps = OrdList.union promise_ord open_ps1 open_ps2;
    1.43      val ps = OrdList.union promise_ord ps1 ps2;
    1.44      val oras = Pt.merge_oracles oras1 oras2;
    1.45      val thms = Pt.merge_thms thms1 thms2;
    1.46 @@ -529,10 +530,10 @@
    1.47        | 1 => MinProof
    1.48        | 0 => MinProof
    1.49        | i => error ("Illegal level of detail for proof objects: " ^ string_of_int i));
    1.50 -  in make_deriv all_ps ps oras thms prf end;
    1.51 +  in make_deriv max open_ps ps oras thms prf end;
    1.52  
    1.53  fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
    1.54 -fun deriv_rule0 prf = deriv_rule1 I (closed_deriv prf);
    1.55 +fun deriv_rule0 prf = deriv_rule1 I (make_deriv ~1 [] [] [] [] prf);
    1.56  
    1.57  
    1.58  
    1.59 @@ -1597,12 +1598,12 @@
    1.60      val _ = Theory.check_thy orig_thy;
    1.61      fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
    1.62  
    1.63 -    val Thm (Deriv {all_promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
    1.64 +    val Thm (Deriv {max_promise, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
    1.65      val _ = prop aconv orig_prop orelse err "bad prop";
    1.66      val _ = null tpairs orelse err "bad tpairs";
    1.67      val _ = null hyps orelse err "bad hyps";
    1.68      val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
    1.69 -    val _ = forall (fn (j, _) => j < i) all_promises orelse err "bad dependencies";
    1.70 +    val _ = max_promise < i orelse err "bad dependencies";
    1.71    in thm end;
    1.72  
    1.73  fun future future_thm ct =
    1.74 @@ -1615,7 +1616,7 @@
    1.75      val future = future_thm |> Future.map (future_result i thy sorts prop o norm_proof);
    1.76      val promise = (i, future);
    1.77    in
    1.78 -    Thm (make_deriv [promise] [promise] [] [] (Pt.promise_proof thy i prop),
    1.79 +    Thm (make_deriv i [promise] [promise] [] [] (Pt.promise_proof thy i prop),
    1.80       {thy_ref = thy_ref,
    1.81        tags = [],
    1.82        maxidx = maxidx,
    1.83 @@ -1630,9 +1631,9 @@
    1.84  
    1.85  fun raw_proof_of (Thm (Deriv {body, ...}, _)) = Proofterm.proof_of body;
    1.86  
    1.87 -fun proof_body_of (Thm (Deriv {all_promises, promises, body}, {thy_ref, ...})) =
    1.88 +fun proof_body_of (Thm (Deriv {open_promises, promises, body, ...}, {thy_ref, ...})) =
    1.89    let
    1.90 -    val _ = Exn.release_all (map (Future.join_result o #2) (rev all_promises));
    1.91 +    val _ = Exn.release_all (map (Future.join_result o #2) (rev open_promises));
    1.92      val ps = map (apsnd (raw_proof_of o Future.join)) promises;
    1.93    in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
    1.94  
    1.95 @@ -1647,14 +1648,17 @@
    1.96  
    1.97  fun put_name name (thm as Thm (der, args)) =
    1.98    let
    1.99 -    val Deriv {promises, body, ...} = der;
   1.100 +    val Deriv {max_promise, open_promises, promises, body, ...} = der;
   1.101      val {thy_ref, hyps, prop, tpairs, ...} = args;
   1.102 -    val _ = null tpairs orelse raise THM ("name_thm: unsolved flex-flex constraints", 0, [thm]);
   1.103 +    val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
   1.104  
   1.105      val ps = Lazy.lazy (fn () => map (apsnd (proof_of o Future.join)) promises);
   1.106      val thy = Theory.deref thy_ref;
   1.107      val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
   1.108 -    val der' = make_deriv [] [] [] [pthm] proof;
   1.109 +
   1.110 +    val open_promises' = open_promises |> filter (fn (_, p) =>
   1.111 +      (case Future.peek p of SOME (Exn.Result _) => false | _ => true));
   1.112 +    val der' = make_deriv max_promise open_promises' [] [] [pthm] proof;
   1.113      val _ = Theory.check_thy thy;
   1.114    in Thm (der', args) end;
   1.115  
   1.116 @@ -1670,7 +1674,7 @@
   1.117        raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
   1.118      else
   1.119        let val prf = Pt.oracle_proof name prop in
   1.120 -        Thm (make_deriv [] [] (Pt.make_oracles prf) [] prf,
   1.121 +        Thm (make_deriv ~1 [] [] (Pt.make_oracles prf) [] prf,
   1.122           {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
   1.123            tags = [],
   1.124            maxidx = maxidx,