support for arbitrarity nested future proofs -- replaced crude order by explicit normalization (which might loop for bad dependencies);
authorwenzelm
Sun Jul 19 18:42:05 2009 +0200 (2009-07-19)
changeset 320597991cdf10a54
parent 32058 c76fd93b3b99
child 32060 b54cb3acbbe4
support for arbitrarity nested future proofs -- replaced crude order by explicit normalization (which might loop for bad dependencies);
export promises_of;
removed obsolete pending_groups;
tuned;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Sun Jul 19 18:02:40 2009 +0200
     1.2 +++ b/src/Pure/thm.ML	Sun Jul 19 18:42:05 2009 +0200
     1.3 @@ -141,12 +141,12 @@
     1.4    val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
     1.5    val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
     1.6    val rename_boundvars: term -> term -> thm -> thm
     1.7 -  val future: thm future -> cterm -> thm
     1.8 -  val pending_groups: thm -> Task_Queue.group list -> Task_Queue.group list
     1.9 -  val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
    1.10    val proof_body_of: thm -> proof_body
    1.11    val proof_of: thm -> proof
    1.12    val join_proof: thm -> unit
    1.13 +  val promises_of: thm -> (serial * thm future) list
    1.14 +  val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
    1.15 +  val future: thm future -> cterm -> thm
    1.16    val get_name: thm -> string
    1.17    val put_name: string -> thm -> thm
    1.18    val extern_oracles: theory -> xstring list
    1.19 @@ -345,9 +345,7 @@
    1.20    tpairs: (term * term) list,                   (*flex-flex pairs*)
    1.21    prop: term}                                   (*conclusion*)
    1.22  and deriv = Deriv of
    1.23 - {max_promise: serial,
    1.24 -  open_promises: (serial * thm future) OrdList.T,
    1.25 -  promises: (serial * thm future) OrdList.T,
    1.26 + {promises: (serial * thm future) OrdList.T,
    1.27    body: Pt.proof_body};
    1.28  
    1.29  type conv = cterm -> thm;
    1.30 @@ -504,11 +502,10 @@
    1.31  
    1.32  (** derivations **)
    1.33  
    1.34 -fun make_deriv max_promise open_promises promises oracles thms proof =
    1.35 -  Deriv {max_promise = max_promise, open_promises = open_promises, promises = promises,
    1.36 -    body = PBody {oracles = oracles, thms = thms, proof = proof}};
    1.37 +fun make_deriv promises oracles thms proof =
    1.38 +  Deriv {promises = promises, body = PBody {oracles = oracles, thms = thms, proof = proof}};
    1.39  
    1.40 -val empty_deriv = make_deriv ~1 [] [] [] [] Pt.MinProof;
    1.41 +val empty_deriv = make_deriv [] [] [] Pt.MinProof;
    1.42  
    1.43  
    1.44  (* inference rules *)
    1.45 @@ -516,13 +513,9 @@
    1.46  fun promise_ord ((i, _), (j, _)) = int_ord (j, i);
    1.47  
    1.48  fun deriv_rule2 f
    1.49 -    (Deriv {max_promise = max1, open_promises = open_ps1, promises = ps1,
    1.50 -      body = PBody {oracles = oras1, thms = thms1, proof = prf1}})
    1.51 -    (Deriv {max_promise = max2, open_promises = open_ps2, promises = ps2,
    1.52 -      body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
    1.53 +    (Deriv {promises = ps1, body = PBody {oracles = oras1, thms = thms1, proof = prf1}})
    1.54 +    (Deriv {promises = ps2, body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
    1.55    let
    1.56 -    val max = Int.max (max1, max2);
    1.57 -    val open_ps = OrdList.union promise_ord open_ps1 open_ps2;
    1.58      val ps = OrdList.union promise_ord ps1 ps2;
    1.59      val oras = Pt.merge_oracles oras1 oras2;
    1.60      val thms = Pt.merge_thms thms1 thms2;
    1.61 @@ -532,10 +525,10 @@
    1.62        | 1 => MinProof
    1.63        | 0 => MinProof
    1.64        | i => error ("Illegal level of detail for proof objects: " ^ string_of_int i));
    1.65 -  in make_deriv max open_ps ps oras thms prf end;
    1.66 +  in make_deriv ps oras thms prf end;
    1.67  
    1.68  fun deriv_rule1 f = deriv_rule2 (K f) empty_deriv;
    1.69 -fun deriv_rule0 prf = deriv_rule1 I (make_deriv ~1 [] [] [] [] prf);
    1.70 +fun deriv_rule0 prf = deriv_rule1 I (make_deriv [] [] [] prf);
    1.71  
    1.72  
    1.73  
    1.74 @@ -1614,6 +1607,36 @@
    1.75  
    1.76  (*** Future theorems -- proofs with promises ***)
    1.77  
    1.78 +(* fulfilled proofs *)
    1.79 +
    1.80 +fun raw_body (Thm (Deriv {body, ...}, _)) = body;
    1.81 +
    1.82 +fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
    1.83 +  let val ps = map (apsnd (fulfill_body o Future.join)) promises
    1.84 +  in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
    1.85 +
    1.86 +fun proof_body_of thm = (Pt.join_bodies [raw_body thm]; fulfill_body thm);
    1.87 +val proof_of = Pt.proof_of o proof_body_of;
    1.88 +val join_proof = ignore o proof_body_of;
    1.89 +
    1.90 +
    1.91 +(* derivation status *)
    1.92 +
    1.93 +fun promises_of (Thm (Deriv {promises, ...}, _)) = promises;
    1.94 +
    1.95 +fun status_of (Thm (Deriv {promises, body}, _)) =
    1.96 +  let
    1.97 +    val ps = map (Future.peek o snd) promises;
    1.98 +    val bodies = body ::
    1.99 +      map_filter (fn SOME (Exn.Result th) => SOME (raw_body th) | _ => NONE) ps;
   1.100 +    val {oracle, unfinished, failed} = Pt.status_of bodies;
   1.101 +  in
   1.102 +   {oracle = oracle,
   1.103 +    unfinished = unfinished orelse exists is_none ps,
   1.104 +    failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps}
   1.105 +  end;
   1.106 +
   1.107 +
   1.108  (* future rule *)
   1.109  
   1.110  fun future_result i orig_thy orig_shyps orig_prop raw_thm =
   1.111 @@ -1623,12 +1646,13 @@
   1.112      val _ = Theory.check_thy orig_thy;
   1.113      fun err msg = raise THM ("future_result: " ^ msg, 0, [thm]);
   1.114  
   1.115 -    val Thm (Deriv {max_promise, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
   1.116 +    val Thm (Deriv {promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
   1.117      val _ = prop aconv orig_prop orelse err "bad prop";
   1.118      val _ = null tpairs orelse err "bad tpairs";
   1.119      val _ = null hyps orelse err "bad hyps";
   1.120      val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
   1.121 -    val _ = max_promise < i orelse err "bad dependencies";
   1.122 +    val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
   1.123 +    val _ = List.app (ignore o fulfill_body o Future.join o #2) promises;
   1.124    in thm end;
   1.125  
   1.126  fun future future_thm ct =
   1.127 @@ -1639,9 +1663,8 @@
   1.128  
   1.129      val i = serial ();
   1.130      val future = future_thm |> Future.map (future_result i thy sorts prop);
   1.131 -    val promise = (i, future);
   1.132    in
   1.133 -    Thm (make_deriv i [promise] [promise] [] [] (Pt.promise_proof thy i prop),
   1.134 +    Thm (make_deriv [(i, future)] [] [] (Pt.promise_proof thy i prop),
   1.135       {thy_ref = thy_ref,
   1.136        tags = [],
   1.137        maxidx = maxidx,
   1.138 @@ -1652,57 +1675,21 @@
   1.139    end;
   1.140  
   1.141  
   1.142 -(* derivation status *)
   1.143 -
   1.144 -fun raw_proof_body_of (Thm (Deriv {body, ...}, _)) = body;
   1.145 -val raw_proof_of = Proofterm.proof_of o raw_proof_body_of;
   1.146 -
   1.147 -fun pending_groups (Thm (Deriv {open_promises, ...}, _)) =
   1.148 -  fold (insert Task_Queue.eq_group o Future.group_of o #2) open_promises;
   1.149 -
   1.150 -fun status_of (Thm (Deriv {promises, body, ...}, _)) =
   1.151 -  let
   1.152 -    val ps = map (Future.peek o snd) promises;
   1.153 -    val bodies = body ::
   1.154 -      map_filter (fn SOME (Exn.Result th) => SOME (raw_proof_body_of th) | _ => NONE) ps;
   1.155 -    val {oracle, unfinished, failed} = Pt.status_of bodies;
   1.156 -  in
   1.157 -   {oracle = oracle,
   1.158 -    unfinished = unfinished orelse exists is_none ps,
   1.159 -    failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps}
   1.160 -  end;
   1.161 -
   1.162 -
   1.163 -(* fulfilled proofs *)
   1.164 -
   1.165 -fun proof_body_of (Thm (Deriv {open_promises, promises, body, ...}, {thy_ref, ...})) =
   1.166 -  let
   1.167 -    val _ = Exn.release_all (map (Future.join_result o #2) (rev open_promises));
   1.168 -    val ps = map (apsnd (raw_proof_body_of o Future.join)) promises;
   1.169 -  in Pt.fulfill_proof (Theory.deref thy_ref) ps body end;
   1.170 -
   1.171 -val proof_of = Proofterm.proof_of o proof_body_of;
   1.172 -val join_proof = ignore o proof_body_of;
   1.173 -
   1.174 -
   1.175  (* closed derivations with official name *)
   1.176  
   1.177  fun get_name thm =
   1.178 -  Pt.get_name (hyps_of thm) (prop_of thm) (raw_proof_of thm);
   1.179 +  Pt.get_name (hyps_of thm) (prop_of thm) (Pt.proof_of (raw_body thm));
   1.180  
   1.181  fun put_name name (thm as Thm (der, args)) =
   1.182    let
   1.183 -    val Deriv {max_promise, open_promises, promises, body, ...} = der;
   1.184 +    val Deriv {promises, body} = der;
   1.185      val {thy_ref, hyps, prop, tpairs, ...} = args;
   1.186      val _ = null tpairs orelse raise THM ("put_name: unsolved flex-flex constraints", 0, [thm]);
   1.187  
   1.188      val ps = map (apsnd (Future.map proof_body_of)) promises;
   1.189      val thy = Theory.deref thy_ref;
   1.190      val (pthm, proof) = Pt.thm_proof thy name hyps prop ps body;
   1.191 -
   1.192 -    val open_promises' = open_promises |> filter (fn (_, p) =>
   1.193 -      (case Future.peek p of SOME (Exn.Result _) => false | _ => true));
   1.194 -    val der' = make_deriv max_promise open_promises' [] [] [pthm] proof;
   1.195 +    val der' = make_deriv [] [] [pthm] proof;
   1.196      val _ = Theory.check_thy thy;
   1.197    in Thm (der', args) end;
   1.198  
   1.199 @@ -1718,7 +1705,7 @@
   1.200        raise THM ("Oracle's result must have type prop: " ^ name, 0, [])
   1.201      else
   1.202        let val (ora, prf) = Pt.oracle_proof name prop in
   1.203 -        Thm (make_deriv ~1 [] [] [ora] [] prf,
   1.204 +        Thm (make_deriv [] [ora] [] prf,
   1.205           {thy_ref = Theory.merge_refs (thy_ref1, thy_ref2),
   1.206            tags = [],
   1.207            maxidx = maxidx,