display derivation status of thms;
authorwenzelm
Tue Mar 24 21:24:53 2009 +0100 (2009-03-24)
changeset 30711952fdbee1b48
parent 30710 77d4b1284d4c
child 30712 fc9d8b1bf1e0
display derivation status of thms;
src/Pure/display.ML
src/Pure/proofterm.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/display.ML	Tue Mar 24 19:37:50 2009 +0100
     1.2 +++ b/src/Pure/display.ML	Tue Mar 24 21:24:53 2009 +0100
     1.3 @@ -57,6 +57,18 @@
     1.4  fun pretty_flexpair pp (t, u) = Pretty.block
     1.5    [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
     1.6  
     1.7 +fun display_status th =
     1.8 +  let
     1.9 +    val {oracle = oracle0, unfinished, failed} = Thm.status_of th;
    1.10 +    val oracle = oracle0 andalso (not (! quick_and_dirty) orelse ! show_hyps);
    1.11 +  in
    1.12 +    if failed then "!!"
    1.13 +    else if oracle andalso unfinished then "!?"
    1.14 +    else if oracle then "!"
    1.15 +    else if unfinished then "?"
    1.16 +    else ""
    1.17 +  end;
    1.18 +
    1.19  fun pretty_thm_aux pp quote show_hyps' asms raw_th =
    1.20    let
    1.21      val th = Thm.strip_shyps raw_th;
    1.22 @@ -68,20 +80,17 @@
    1.23      val prt_term = q o Pretty.term pp;
    1.24  
    1.25      val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
    1.26 -(* FIXME
    1.27 -    val ora' = Thm.oracle_of th andalso (! show_hyps orelse not (! quick_and_dirty)); *)
    1.28 -    val ora' = false;
    1.29 +    val status = display_status th;
    1.30  
    1.31      val hlen = length xshyps + length hyps' + length tpairs;
    1.32      val hsymbs =
    1.33 -      if hlen = 0 andalso not ora' then []
    1.34 +      if hlen = 0 andalso status = "" then []
    1.35        else if ! show_hyps orelse show_hyps' then
    1.36          [Pretty.brk 2, Pretty.list "[" "]"
    1.37            (map (q o pretty_flexpair pp) tpairs @ map prt_term hyps' @
    1.38             map (Pretty.sort pp) xshyps @
    1.39 -            (if ora' then [Pretty.str "!"] else []))]
    1.40 -      else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^
    1.41 -        (if ora' then "!" else "") ^ "]")];
    1.42 +            (if status = "" then [] else [Pretty.str status]))]
    1.43 +      else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
    1.44      val tsymbs =
    1.45        if null tags orelse not (! show_tags) then []
    1.46        else [Pretty.brk 1, pretty_tags tags];
     2.1 --- a/src/Pure/proofterm.ML	Tue Mar 24 19:37:50 2009 +0100
     2.2 +++ b/src/Pure/proofterm.ML	Tue Mar 24 21:24:53 2009 +0100
     2.3 @@ -40,8 +40,9 @@
     2.4      {oracles: oracle OrdList.T, thms: pthm OrdList.T, proof: proof}
     2.5    val join_proof: proof_body future -> proof
     2.6    val proof_of: proof_body -> proof
     2.7 +  val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
     2.8    val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
     2.9 -  val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
    2.10 +  val status_of: proof_body -> {failed: bool, oracle: bool, unfinished: bool}
    2.11  
    2.12    val oracle_ord: oracle * oracle -> order
    2.13    val thm_ord: pthm * pthm -> order
    2.14 @@ -159,17 +160,6 @@
    2.15  
    2.16  (***** proof atoms *****)
    2.17  
    2.18 -fun fold_body_thms f =
    2.19 -  let
    2.20 -    fun app (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
    2.21 -      if Inttab.defined seen i then (x, seen)
    2.22 -      else
    2.23 -        let
    2.24 -          val body' = Future.join body;
    2.25 -          val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
    2.26 -        in (f (name, prop, body') x', seen') end);
    2.27 -  in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
    2.28 -
    2.29  fun fold_proof_atoms all f =
    2.30    let
    2.31      fun app (Abst (_, _, prf)) = app prf
    2.32 @@ -185,6 +175,39 @@
    2.33        | app prf = (fn (x, seen) => (f prf x, seen));
    2.34    in fn prfs => fn x => #1 (fold app prfs (x, Inttab.empty)) end;
    2.35  
    2.36 +fun fold_body_thms f =
    2.37 +  let
    2.38 +    fun app (PBody {thms, ...}) = thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
    2.39 +      if Inttab.defined seen i then (x, seen)
    2.40 +      else
    2.41 +        let
    2.42 +          val body' = Future.join body;
    2.43 +          val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
    2.44 +        in (f (name, prop, body') x', seen') end);
    2.45 +  in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
    2.46 +
    2.47 +fun status_of proof_body =
    2.48 +  let
    2.49 +    fun status (PBody {oracles, thms, ...}) x =
    2.50 +      let
    2.51 +        val ((oracle, unfinished, failed), seen) =
    2.52 +          (thms, x) |-> fold (fn (i, (_, _, body)) => fn (st, seen) =>
    2.53 +            if Inttab.defined seen i then (st, seen)
    2.54 +            else
    2.55 +              let val seen' = Inttab.update (i, ()) seen in
    2.56 +                (case Future.peek body of
    2.57 +                  SOME (Exn.Result body') => status body' (st, seen')
    2.58 +                | SOME (Exn.Exn _) =>
    2.59 +                    let val (oracle, unfinished, _) = st
    2.60 +                    in ((oracle, unfinished, true), seen') end
    2.61 +                | NONE =>
    2.62 +                    let val (oracle, _, failed) = st
    2.63 +                    in ((oracle, true, failed), seen') end)
    2.64 +              end);
    2.65 +      in ((oracle orelse not (null oracles), unfinished, failed), seen) end;
    2.66 +    val (oracle, unfinished, failed) = #1 (status proof_body ((false, false, false), Inttab.empty));
    2.67 +  in {oracle = oracle, unfinished = unfinished, failed = failed} end;
    2.68 +
    2.69  
    2.70  (* proof body *)
    2.71  
     3.1 --- a/src/Pure/thm.ML	Tue Mar 24 19:37:50 2009 +0100
     3.2 +++ b/src/Pure/thm.ML	Tue Mar 24 21:24:53 2009 +0100
     3.3 @@ -60,6 +60,7 @@
     3.4    val theory_of_thm: thm -> theory
     3.5    val prop_of: thm -> term
     3.6    val tpairs_of: thm -> (term * term) list
     3.7 +  val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
     3.8    val concl_of: thm -> term
     3.9    val prems_of: thm -> term list
    3.10    val nprems_of: thm -> int
    3.11 @@ -399,6 +400,7 @@
    3.12  val hyps_of = #hyps o rep_thm;
    3.13  val prop_of = #prop o rep_thm;
    3.14  val tpairs_of = #tpairs o rep_thm;
    3.15 +fun status_of (Thm (Deriv {body, ...}, _)) = Pt.status_of body;
    3.16  
    3.17  val concl_of = Logic.strip_imp_concl o prop_of;
    3.18  val prems_of = Logic.strip_imp_prems o prop_of;