status_of: need to include local promises as well!
authorwenzelm
Tue Mar 24 22:56:17 2009 +0100 (2009-03-24)
changeset 30713b1a87e3971a3
parent 30712 fc9d8b1bf1e0
child 30714 88bc86d7dec3
status_of: need to include local promises as well!
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Tue Mar 24 22:55:49 2009 +0100
     1.2 +++ b/src/Pure/thm.ML	Tue Mar 24 22:56:17 2009 +0100
     1.3 @@ -60,7 +60,6 @@
     1.4    val theory_of_thm: thm -> theory
     1.5    val prop_of: thm -> term
     1.6    val tpairs_of: thm -> (term * term) list
     1.7 -  val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
     1.8    val concl_of: thm -> term
     1.9    val prems_of: thm -> term list
    1.10    val nprems_of: thm -> int
    1.11 @@ -145,6 +144,7 @@
    1.12    val freezeT: thm -> thm
    1.13    val future: thm future -> cterm -> thm
    1.14    val pending_groups: thm -> Task_Queue.group list -> Task_Queue.group list
    1.15 +  val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
    1.16    val proof_body_of: thm -> proof_body
    1.17    val proof_of: thm -> proof
    1.18    val join_proof: thm -> unit
    1.19 @@ -400,7 +400,6 @@
    1.20  val hyps_of = #hyps o rep_thm;
    1.21  val prop_of = #prop o rep_thm;
    1.22  val tpairs_of = #tpairs o rep_thm;
    1.23 -fun status_of (Thm (Deriv {body, ...}, _)) = Pt.status_of body;
    1.24  
    1.25  val concl_of = Logic.strip_imp_concl o prop_of;
    1.26  val prems_of = Logic.strip_imp_prems o prop_of;
    1.27 @@ -1637,16 +1636,29 @@
    1.28    end;
    1.29  
    1.30  
    1.31 -(* pending task groups *)
    1.32 +(* derivation status *)
    1.33 +
    1.34 +fun raw_proof_body_of (Thm (Deriv {body, ...}, _)) = body;
    1.35 +val raw_proof_of = Proofterm.proof_of o raw_proof_body_of;
    1.36  
    1.37  fun pending_groups (Thm (Deriv {open_promises, ...}, _)) =
    1.38    fold (insert Task_Queue.eq_group o Future.group_of o #2) open_promises;
    1.39  
    1.40 +fun status_of (Thm (Deriv {promises, body, ...}, _)) =
    1.41 +  let
    1.42 +    val ps = map (Future.peek o snd) promises;
    1.43 +    val bodies = body ::
    1.44 +      map_filter (fn SOME (Exn.Result th) => SOME (raw_proof_body_of th) | _ => NONE) ps;
    1.45 +    val {oracle, unfinished, failed} = Pt.status_of bodies;
    1.46 +  in
    1.47 +   {oracle = oracle,
    1.48 +    unfinished = unfinished orelse exists is_none ps,
    1.49 +    failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps}
    1.50 +  end;
    1.51 +
    1.52  
    1.53  (* fulfilled proofs *)
    1.54  
    1.55 -fun raw_proof_of (Thm (Deriv {body, ...}, _)) = Proofterm.proof_of body;
    1.56 -
    1.57  fun proof_body_of (Thm (Deriv {open_promises, promises, body, ...}, {thy_ref, ...})) =
    1.58    let
    1.59      val _ = Exn.release_all (map (Future.join_result o #2) (rev open_promises));