theorem status about oracles/futures is no longer printed by default;
authorwenzelm
Mon Nov 19 20:23:47 2012 +0100 (2012-11-19)
changeset 501263dec88149176
parent 50125 4319691be975
child 50127 ff0b52a6d72f
theorem status about oracles/futures is no longer printed by default;
renamed Proofterm/Thm.status_of to Proofterm/Thm.peek_status to emphasize its semantics;
NEWS
src/Doc/IsarImplementation/Logic.thy
src/Doc/IsarRef/Proof.thy
src/HOL/SPARK/Tools/spark_vcs.ML
src/HOL/ex/Iff_Oracle.thy
src/Pure/Isar/proof_context.ML
src/Pure/Isar/proof_display.ML
src/Pure/display.ML
src/Pure/proofterm.ML
src/Pure/thm.ML
     1.1 --- a/NEWS	Mon Nov 19 18:01:48 2012 +0100
     1.2 +++ b/NEWS	Mon Nov 19 20:23:47 2012 +0100
     1.3 @@ -6,6 +6,14 @@
     1.4  
     1.5  *** General ***
     1.6  
     1.7 +* Theorem status about oracles and unfinished/failed future proofs is
     1.8 +no longer printed by default, since it is incompatible with
     1.9 +incremental / parallel checking of the persistent document model.  ML
    1.10 +function Thm.peek_status may be used to inspect a snapshot of the
    1.11 +ongoing evaluation process.  Note that in batch mode --- notably
    1.12 +isabelle build --- the system ensures that future proofs of all
    1.13 +accessible theorems in the theory context are finished (as before).
    1.14 +
    1.15  * Configuration option show_markup controls direct inlining of markup
    1.16  into the printed representation of formal entities --- notably type
    1.17  and sort constraints.  This enables Prover IDE users to retrieve that
     2.1 --- a/src/Doc/IsarImplementation/Logic.thy	Mon Nov 19 18:01:48 2012 +0100
     2.2 +++ b/src/Doc/IsarImplementation/Logic.thy	Mon Nov 19 20:23:47 2012 +0100
     2.3 @@ -648,6 +648,7 @@
     2.4    \begin{mldecls}
     2.5    @{index_ML_type thm} \\
     2.6    @{index_ML proofs: "int Unsynchronized.ref"} \\
     2.7 +  @{index_ML Thm.peek_status: "thm -> {oracle: bool, unfinished: bool, failed: bool}"} \\
     2.8    @{index_ML Thm.transfer: "theory -> thm -> thm"} \\
     2.9    @{index_ML Thm.assume: "cterm -> thm"} \\
    2.10    @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
    2.11 @@ -670,6 +671,15 @@
    2.12  
    2.13    \begin{description}
    2.14  
    2.15 +  \item @{ML Thm.peek_status}~@{text "thm"} informs about the current
    2.16 +  status of the derivation object behind the given theorem.  This is a
    2.17 +  snapshot of a potentially ongoing (parallel) evaluation of proofs.
    2.18 +  The three Boolean values indicate the following: @{verbatim oracle}
    2.19 +  if the finished part contains some oracle invocation; @{verbatim
    2.20 +  unfinished} if some future proofs are still pending; @{verbatim
    2.21 +  failed} if some future proof has failed, rendering the theorem
    2.22 +  invalid!
    2.23 +
    2.24    \item @{ML Logic.all}~@{text "a B"} produces a Pure quantification
    2.25    @{text "\<And>a. B"}, where occurrences of the atomic term @{text "a"} in
    2.26    the body proposition @{text "B"} are replaced by bound variables.
     3.1 --- a/src/Doc/IsarRef/Proof.thy	Mon Nov 19 18:01:48 2012 +0100
     3.2 +++ b/src/Doc/IsarRef/Proof.thy	Mon Nov 19 20:23:47 2012 +0100
     3.3 @@ -670,9 +670,9 @@
     3.4    pretending to solve the pending claim without further ado.  This
     3.5    only works in interactive development, or if the @{ML
     3.6    quick_and_dirty} flag is enabled (in ML).  Facts emerging from fake
     3.7 -  proofs are not the real thing.  Internally, each theorem container
     3.8 -  is tainted by an oracle invocation, which is indicated as ``@{text
     3.9 -  "[!]"}'' in the printed result.
    3.10 +  proofs are not the real thing.  Internally, the derivation object is
    3.11 +  tainted by an oracle invocation, which may be inspected via the
    3.12 +  theorem status \cite{isabelle-implementation}.
    3.13    
    3.14    The most important application of @{command "sorry"} is to support
    3.15    experimentation and top-down proof development.
     4.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Nov 19 18:01:48 2012 +0100
     4.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Mon Nov 19 20:23:47 2012 +0100
     4.3 @@ -963,7 +963,7 @@
     4.4            val (proved, unproved) = partition_vcs vcs;
     4.5            val _ = Thm.join_proofs (maps (#2 o snd) proved);
     4.6            val (proved', proved'') = List.partition (fn (_, (_, thms, _, _)) =>
     4.7 -            exists (#oracle o Thm.status_of) thms) proved
     4.8 +            exists (#oracle o Thm.peek_status) thms) proved
     4.9          in
    4.10            (if null unproved then ()
    4.11             else (if incomplete then warning else error)
     5.1 --- a/src/HOL/ex/Iff_Oracle.thy	Mon Nov 19 18:01:48 2012 +0100
     5.2 +++ b/src/HOL/ex/Iff_Oracle.thy	Mon Nov 19 20:23:47 2012 +0100
     5.3 @@ -34,7 +34,7 @@
     5.4  
     5.5  ML {* iff_oracle (@{theory}, 2) *}
     5.6  ML {* iff_oracle (@{theory}, 10) *}
     5.7 -ML {* Thm.status_of (iff_oracle (@{theory}, 10)) *}
     5.8 +ML {* Thm.peek_status (iff_oracle (@{theory}, 10)) *}
     5.9  
    5.10  text {* These oracle calls had better fail. *}
    5.11  
     6.1 --- a/src/Pure/Isar/proof_context.ML	Mon Nov 19 18:01:48 2012 +0100
     6.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Nov 19 20:23:47 2012 +0100
     6.3 @@ -52,7 +52,6 @@
     6.4    val extern_fact: Proof.context -> string -> xstring
     6.5    val pretty_term_abbrev: Proof.context -> term -> Pretty.T
     6.6    val markup_fact: Proof.context -> string -> Markup.T
     6.7 -  val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
     6.8    val pretty_fact: Proof.context -> string * thm list -> Pretty.T
     6.9    val read_class: Proof.context -> xstring -> class
    6.10    val read_typ: Proof.context -> string -> typ
    6.11 @@ -343,14 +342,11 @@
    6.12  fun pretty_fact_name ctxt a =
    6.13    Pretty.block [Pretty.mark_str (markup_fact ctxt a, extern_fact ctxt a), Pretty.str ":"];
    6.14  
    6.15 -fun pretty_fact_aux ctxt flag ("", ths) =
    6.16 -      Display.pretty_thms_aux ctxt flag ths
    6.17 -  | pretty_fact_aux ctxt flag (a, [th]) = Pretty.block
    6.18 -      [pretty_fact_name ctxt a, Pretty.brk 1, Display.pretty_thm_aux ctxt flag th]
    6.19 -  | pretty_fact_aux ctxt flag (a, ths) = Pretty.block
    6.20 -      (Pretty.fbreaks (pretty_fact_name ctxt a :: map (Display.pretty_thm_aux ctxt flag) ths));
    6.21 -
    6.22 -fun pretty_fact ctxt = pretty_fact_aux ctxt true;
    6.23 +fun pretty_fact ctxt ("", ths) = Display.pretty_thms ctxt ths
    6.24 +  | pretty_fact ctxt (a, [th]) = Pretty.block
    6.25 +      [pretty_fact_name ctxt a, Pretty.brk 1, Display.pretty_thm ctxt th]
    6.26 +  | pretty_fact ctxt (a, ths) = Pretty.block
    6.27 +      (Pretty.fbreaks (pretty_fact_name ctxt a :: map (Display.pretty_thm ctxt) ths));
    6.28  
    6.29  
    6.30  
     7.1 --- a/src/Pure/Isar/proof_display.ML	Mon Nov 19 18:01:48 2012 +0100
     7.2 +++ b/src/Pure/Isar/proof_display.ML	Mon Nov 19 20:23:47 2012 +0100
     7.3 @@ -46,10 +46,8 @@
     7.4    | NONE => Syntax.init_pretty_global thy0);
     7.5  
     7.6  fun pp_thm th =
     7.7 -  let
     7.8 -    val ctxt = default_context (Thm.theory_of_thm th);
     7.9 -    val flags = {quote = true, show_hyps = false, show_status = true};
    7.10 -  in Display.pretty_thm_raw ctxt flags th end;
    7.11 +  let val ctxt = default_context (Thm.theory_of_thm th);
    7.12 +  in Display.pretty_thm_raw ctxt {quote = true, show_hyps = false} th end;
    7.13  
    7.14  fun pp_typ thy T = Pretty.quote (Syntax.pretty_typ (default_context thy) T);
    7.15  fun pp_term thy t = Pretty.quote (Syntax.pretty_term (default_context thy) t);
    7.16 @@ -85,7 +83,7 @@
    7.17  
    7.18  fun pretty_rule ctxt s thm =
    7.19    Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
    7.20 -    Pretty.fbrk, Display.pretty_thm_aux ctxt false thm];
    7.21 +    Pretty.fbrk, Display.pretty_thm ctxt thm];
    7.22  
    7.23  val string_of_rule = Pretty.string_of ooo pretty_rule;
    7.24  
    7.25 @@ -138,7 +136,7 @@
    7.26  
    7.27  fun pretty_facts ctxt =
    7.28    flat o (separate [Pretty.fbrk, Pretty.keyword "and", Pretty.str " "]) o
    7.29 -    map (single o Proof_Context.pretty_fact_aux ctxt false);
    7.30 +    map (single o Proof_Context.pretty_fact ctxt);
    7.31  
    7.32  in
    7.33  
    7.34 @@ -151,7 +149,7 @@
    7.35      (Pretty.writeln o Pretty.mark markup)
    7.36        (case facts of
    7.37          [fact] => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
    7.38 -          Proof_Context.pretty_fact_aux ctxt false fact])
    7.39 +          Proof_Context.pretty_fact ctxt fact])
    7.40        | _ => Pretty.blk (1, [pretty_fact_name (kind, name), Pretty.fbrk,
    7.41            Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
    7.42  
     8.1 --- a/src/Pure/display.ML	Mon Nov 19 18:01:48 2012 +0100
     8.2 +++ b/src/Pure/display.ML	Mon Nov 19 20:23:47 2012 +0100
     8.3 @@ -18,16 +18,13 @@
     8.4  signature DISPLAY =
     8.5  sig
     8.6    include BASIC_DISPLAY
     8.7 -  val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool, show_status: bool} ->
     8.8 -    thm -> Pretty.T
     8.9 -  val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T
    8.10 +  val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T
    8.11    val pretty_thm: Proof.context -> thm -> Pretty.T
    8.12    val pretty_thm_global: theory -> thm -> Pretty.T
    8.13    val pretty_thm_without_context: thm -> Pretty.T
    8.14    val string_of_thm: Proof.context -> thm -> string
    8.15    val string_of_thm_global: theory -> thm -> string
    8.16    val string_of_thm_without_context: thm -> string
    8.17 -  val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T
    8.18    val pretty_thms: Proof.context -> thm list -> Pretty.T
    8.19    val print_syntax: theory -> unit
    8.20    val pretty_full_theory: bool -> theory -> Pretty.T list
    8.21 @@ -54,20 +51,7 @@
    8.22  fun pretty_tag (name, arg) = Pretty.strs [name, quote arg];
    8.23  val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    8.24  
    8.25 -fun display_status _ false _ = ""
    8.26 -  | display_status show_hyps true th =
    8.27 -      let
    8.28 -        val {oracle = oracle0, unfinished, failed} = Thm.status_of th;
    8.29 -        val oracle = oracle0 andalso (not (! quick_and_dirty) orelse show_hyps);
    8.30 -      in
    8.31 -        if failed then "!!"
    8.32 -        else if oracle andalso unfinished then "!?"
    8.33 -        else if oracle then "!"
    8.34 -        else if unfinished then "?"
    8.35 -        else ""
    8.36 -      end;
    8.37 -
    8.38 -fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps', show_status} raw_th =
    8.39 +fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps'} raw_th =
    8.40    let
    8.41      val show_tags = Config.get ctxt show_tags;
    8.42      val show_hyps = Config.get ctxt show_hyps;
    8.43 @@ -82,30 +66,24 @@
    8.44  
    8.45      val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
    8.46      val hyps' = if show_hyps then hyps else subtract (op aconv) asms hyps;
    8.47 -    val status = display_status show_hyps show_status th;
    8.48  
    8.49      val hlen = length xshyps + length hyps' + length tpairs;
    8.50      val hsymbs =
    8.51 -      if hlen = 0 andalso status = "" then []
    8.52 +      if hlen = 0 then []
    8.53        else if show_hyps orelse show_hyps' then
    8.54          [Pretty.brk 2, Pretty.list "[" "]"
    8.55            (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @
    8.56 -           map (Syntax.pretty_sort ctxt) xshyps @
    8.57 -            (if status = "" then [] else [Pretty.str status]))]
    8.58 -      else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
    8.59 +           map (Syntax.pretty_sort ctxt) xshyps)]
    8.60 +      else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")];
    8.61      val tsymbs =
    8.62        if null tags orelse not show_tags then []
    8.63        else [Pretty.brk 1, pretty_tags tags];
    8.64    in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
    8.65  
    8.66 -fun pretty_thm_aux ctxt show_status =
    8.67 -  pretty_thm_raw ctxt {quote = false, show_hyps = true, show_status = show_status};
    8.68 -
    8.69 -fun pretty_thm ctxt = pretty_thm_aux ctxt true;
    8.70 +fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true};
    8.71  
    8.72  fun pretty_thm_global thy =
    8.73 -  pretty_thm_raw (Syntax.init_pretty_global thy)
    8.74 -    {quote = false, show_hyps = false, show_status = true};
    8.75 +  pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false};
    8.76  
    8.77  fun pretty_thm_without_context th = pretty_thm_global (Thm.theory_of_thm th) th;
    8.78  
    8.79 @@ -116,11 +94,8 @@
    8.80  
    8.81  (* multiple theorems *)
    8.82  
    8.83 -fun pretty_thms_aux ctxt flag [th] = pretty_thm_aux ctxt flag th
    8.84 -  | pretty_thms_aux ctxt flag ths =
    8.85 -      Pretty.blk (0, Pretty.fbreaks (map (pretty_thm_aux ctxt flag) ths));
    8.86 -
    8.87 -fun pretty_thms ctxt = pretty_thms_aux ctxt true;
    8.88 +fun pretty_thms ctxt [th] = pretty_thm ctxt th
    8.89 +  | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
    8.90  
    8.91  
    8.92  
     9.1 --- a/src/Pure/proofterm.ML	Mon Nov 19 18:01:48 2012 +0100
     9.2 +++ b/src/Pure/proofterm.ML	Mon Nov 19 20:23:47 2012 +0100
     9.3 @@ -42,7 +42,7 @@
     9.4    val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
     9.5    val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
     9.6    val join_bodies: proof_body list -> unit
     9.7 -  val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
     9.8 +  val peek_status: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
     9.9  
    9.10    val oracle_ord: oracle * oracle -> order
    9.11    val thm_ord: pthm * pthm -> order
    9.12 @@ -208,7 +208,7 @@
    9.13  
    9.14  fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
    9.15  
    9.16 -fun status_of bodies =
    9.17 +fun peek_status bodies =
    9.18    let
    9.19      fun status (PBody {oracles, thms, ...}) x =
    9.20        let
    10.1 --- a/src/Pure/thm.ML	Mon Nov 19 18:01:48 2012 +0100
    10.2 +++ b/src/Pure/thm.ML	Mon Nov 19 20:23:47 2012 +0100
    10.3 @@ -99,7 +99,7 @@
    10.4    val proof_body_of: thm -> proof_body
    10.5    val proof_of: thm -> proof
    10.6    val join_proofs: thm list -> unit
    10.7 -  val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
    10.8 +  val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool}
    10.9    val future: thm future -> cterm -> thm
   10.10    val derivation_name: thm -> string
   10.11    val name_derivation: string -> thm -> thm
   10.12 @@ -536,12 +536,12 @@
   10.13  
   10.14  (* derivation status *)
   10.15  
   10.16 -fun status_of (Thm (Deriv {promises, body}, _)) =
   10.17 +fun peek_status (Thm (Deriv {promises, body}, _)) =
   10.18    let
   10.19      val ps = map (Future.peek o snd) promises;
   10.20      val bodies = body ::
   10.21        map_filter (fn SOME (Exn.Res th) => SOME (raw_body_of th) | _ => NONE) ps;
   10.22 -    val {oracle, unfinished, failed} = Proofterm.status_of bodies;
   10.23 +    val {oracle, unfinished, failed} = Proofterm.peek_status bodies;
   10.24    in
   10.25     {oracle = oracle,
   10.26      unfinished = unfinished orelse exists is_none ps,