src/Pure/Isar/proof_display.ML
author wenzelm
Thu Sep 24 23:33:29 2015 +0200 (2015-09-24)
changeset 61261 ddb2da7cb2e4
parent 61258 2be9ea29f9ec
child 61266 eb9522a9d997
permissions -rw-r--r--
more explicit Defs.context: use proper name spaces as far as possible;
     1 (*  Title:      Pure/Isar/proof_display.ML
     2     Author:     Makarius
     3 
     4 Printing of theorems, goals, results etc.
     5 *)
     6 
     7 signature PROOF_DISPLAY =
     8 sig
     9   val pp_context: Proof.context -> Pretty.T
    10   val pp_thm: (unit -> theory) -> thm -> Pretty.T
    11   val pp_typ: (unit -> theory) -> typ -> Pretty.T
    12   val pp_term: (unit -> theory) -> term -> Pretty.T
    13   val pp_ctyp: (unit -> theory) -> ctyp -> Pretty.T
    14   val pp_cterm: (unit -> theory) -> cterm -> Pretty.T
    15   val pretty_definitions: bool -> Proof.context -> Pretty.T
    16   val pretty_theorems_diff: bool -> theory list -> theory -> Pretty.T list
    17   val pretty_theorems: bool -> theory -> Pretty.T list
    18   val pretty_full_theory: bool -> theory -> Pretty.T
    19   val string_of_rule: Proof.context -> string -> thm -> string
    20   val pretty_goal_header: thm -> Pretty.T
    21   val string_of_goal: Proof.context -> thm -> string
    22   val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T
    23   val method_error: string -> Position.T ->
    24     {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
    25   val print_results: bool -> Position.T -> Proof.context ->
    26     ((string * string) * (string * thm list) list) -> unit
    27   val print_consts: bool -> Position.T -> Proof.context ->
    28     (string * typ -> bool) -> (string * typ) list -> unit
    29 end
    30 
    31 structure Proof_Display: PROOF_DISPLAY =
    32 struct
    33 
    34 (** toplevel pretty printing **)
    35 
    36 fun pp_context ctxt =
    37  (if Config.get ctxt Proof_Context.debug then
    38     Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt))
    39   else Pretty.str "<context>");
    40 
    41 fun default_context mk_thy =
    42   (case Context.thread_data () of
    43     SOME (Context.Proof ctxt) => ctxt
    44   | SOME (Context.Theory thy) =>
    45       (case try Syntax.init_pretty_global thy of
    46         SOME ctxt => ctxt
    47       | NONE => Syntax.init_pretty_global (mk_thy ()))
    48   | NONE => Syntax.init_pretty_global (mk_thy ()));
    49 
    50 fun pp_thm mk_thy th =
    51   Display.pretty_thm_raw (default_context mk_thy) {quote = true, show_hyps = false} th;
    52 
    53 fun pp_typ mk_thy T = Pretty.quote (Syntax.pretty_typ (default_context mk_thy) T);
    54 fun pp_term mk_thy t = Pretty.quote (Syntax.pretty_term (default_context mk_thy) t);
    55 
    56 fun pp_ctyp mk_thy cT = pp_typ mk_thy (Thm.typ_of cT);
    57 fun pp_cterm mk_thy ct = pp_term mk_thy (Thm.term_of ct);
    58 
    59 
    60 
    61 (** theory content **)
    62 
    63 (* theorems and theory *)
    64 
    65 fun pretty_theorems_diff verbose prev_thys thy =
    66   let
    67     val pretty_fact = Proof_Context.pretty_fact (Proof_Context.init_global thy);
    68     val facts = Global_Theory.facts_of thy;
    69     val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts;
    70     val prts = map #1 (sort_by (#1 o #2) (map (`pretty_fact) thmss));
    71   in if null prts then [] else [Pretty.big_list "theorems:" prts] end;
    72 
    73 fun pretty_theorems verbose thy =
    74   pretty_theorems_diff verbose (Theory.parents_of thy) thy;
    75 
    76 fun pretty_full_theory verbose thy =
    77   Pretty.chunks (Display.pretty_full_theory verbose thy @ pretty_theorems verbose thy);
    78 
    79 
    80 (* definitions *)
    81 
    82 fun pretty_definitions verbose ctxt =
    83   let
    84     val thy = Proof_Context.theory_of ctxt;
    85     val context = Proof_Context.defs_context ctxt;
    86 
    87     val const_space = Proof_Context.const_space ctxt;
    88     val type_space = Proof_Context.type_space ctxt;
    89     val item_space = fn Defs.Const => const_space | Defs.Type => type_space;
    90     fun prune_item (k, c) = not verbose andalso Name_Space.is_concealed (item_space k) c;
    91 
    92     fun extern_item (kind, name) =
    93       let val xname = Name_Space.extern ctxt (item_space kind) name
    94       in (xname, (kind, name)) end;
    95 
    96     fun extern_item_ord ((xname1, (kind1, _)), (xname2, (kind2, _))) =
    97       (case Defs.item_kind_ord (kind1, kind2) of
    98         EQUAL => string_ord (xname1, xname2)
    99       | ord => ord);
   100 
   101     fun sort_items f = sort (extern_item_ord o apply2 f);
   102 
   103     fun pretty_entry ((_: string, item), args) = Defs.pretty_entry context (item, args);
   104 
   105     fun pretty_reduct (lhs, rhs) = Pretty.block
   106       ([pretty_entry lhs, Pretty.str "  ->", Pretty.brk 2] @
   107         Pretty.commas (map pretty_entry (sort_items fst rhs)));
   108 
   109     fun pretty_restrict (entry, name) =
   110       Pretty.block ([pretty_entry entry, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
   111 
   112     val defs = Theory.defs_of thy;
   113     val {restricts, reducts} = Defs.dest defs;
   114 
   115     val (reds1, reds2) =
   116       filter_out (prune_item o #1 o #1) reducts
   117       |> map (fn (lhs, rhs) =>
   118         (apfst extern_item lhs, map (apfst extern_item) (filter_out (prune_item o fst) rhs)))
   119       |> sort_items (#1 o #1)
   120       |> filter_out (null o #2)
   121       |> List.partition (Defs.plain_args o #2 o #1);
   122 
   123     val rests = restricts |> map (apfst (apfst extern_item)) |> sort_items (#1 o #1);
   124   in
   125     Pretty.big_list "definitions:"
   126       (map (Pretty.text_fold o single)
   127         [Pretty.big_list "non-overloaded LHS:" (map pretty_reduct reds1),
   128          Pretty.big_list "overloaded LHS:" (map pretty_reduct reds2),
   129          Pretty.big_list "pattern restrictions due to incomplete LHS:" (map pretty_restrict rests)])
   130   end;
   131 
   132 
   133 
   134 (** proof items **)
   135 
   136 (* refinement rule *)
   137 
   138 fun pretty_rule ctxt s thm =
   139   Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
   140     Pretty.fbrk, Display.pretty_thm ctxt thm];
   141 
   142 val string_of_rule = Pretty.string_of ooo pretty_rule;
   143 
   144 
   145 (* goals *)
   146 
   147 local
   148 
   149 fun subgoals 0 = []
   150   | subgoals 1 = [Pretty.brk 1, Pretty.str "(1 subgoal)"]
   151   | subgoals n = [Pretty.brk 1, Pretty.str ("(" ^ string_of_int n ^ " subgoals)")];
   152 
   153 in
   154 
   155 fun pretty_goal_header goal =
   156   Pretty.block ([Pretty.keyword1 "goal"] @ subgoals (Thm.nprems_of goal) @ [Pretty.str ":"]);
   157 
   158 end;
   159 
   160 fun string_of_goal ctxt goal =
   161   Pretty.string_of (Pretty.chunks [pretty_goal_header goal, Goal_Display.pretty_goal ctxt goal]);
   162 
   163 
   164 (* goal facts *)
   165 
   166 fun pretty_goal_facts ctxt s ths =
   167   (Pretty.block o Pretty.fbreaks)
   168     [if s = "" then Pretty.str "this:"
   169      else Pretty.block [Pretty.keyword1 s, Pretty.brk 1, Pretty.str "this:"],
   170      Proof_Context.pretty_fact ctxt ("", ths)];
   171 
   172 
   173 (* method_error *)
   174 
   175 fun method_error kind pos {context = ctxt, facts, goal} = Seq.Error (fn () =>
   176   let
   177     val pr_header =
   178       "Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^
   179       "proof method" ^ Position.here pos ^ ":\n";
   180     val pr_facts =
   181       if null facts then ""
   182       else Pretty.string_of (pretty_goal_facts ctxt "using" facts) ^ "\n";
   183     val pr_goal = string_of_goal ctxt goal;
   184   in pr_header ^ pr_facts ^ pr_goal end);
   185 
   186 
   187 (* results *)
   188 
   189 fun position_markup pos = Pretty.mark (Position.markup pos Markup.position);
   190 
   191 local
   192 
   193 fun pretty_fact_name pos (kind, "") = position_markup pos (Pretty.keyword1 kind)
   194   | pretty_fact_name pos (kind, name) =
   195       Pretty.block [position_markup pos (Pretty.keyword1 kind), Pretty.brk 1,
   196         Pretty.str (Long_Name.base_name name), Pretty.str ":"];
   197 
   198 fun pretty_facts ctxt =
   199   flat o (separate [Pretty.fbrk, Pretty.keyword2 "and", Pretty.str " "]) o
   200     map (single o Proof_Context.pretty_fact ctxt);
   201 
   202 in
   203 
   204 fun print_results do_print pos ctxt ((kind, name), facts) =
   205   if not do_print orelse kind = "" then ()
   206   else if name = "" then
   207     (Output.state o Pretty.string_of)
   208       (Pretty.block (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
   209         pretty_facts ctxt facts))
   210   else
   211     (Output.state o Pretty.string_of)
   212       (case facts of
   213         [fact] => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
   214           Proof_Context.pretty_fact ctxt fact])
   215       | _ => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
   216           Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
   217 
   218 end;
   219 
   220 
   221 (* consts *)
   222 
   223 local
   224 
   225 fun pretty_var ctxt (x, T) =
   226   Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
   227     Pretty.quote (Syntax.pretty_typ ctxt T)];
   228 
   229 fun pretty_vars pos ctxt kind vs =
   230   Pretty.block (Pretty.fbreaks (position_markup pos (Pretty.str kind) :: map (pretty_var ctxt) vs));
   231 
   232 fun pretty_consts pos ctxt pred cs =
   233   (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of
   234     [] => pretty_vars pos ctxt "constants" cs
   235   | ps => Pretty.chunks [pretty_vars pos ctxt "parameters" ps, pretty_vars pos ctxt "constants" cs]);
   236 
   237 in
   238 
   239 fun print_consts do_print pos ctxt pred cs =
   240   if not do_print orelse null cs then ()
   241   else Output.state (Pretty.string_of (pretty_consts pos ctxt pred cs));
   242 
   243 end;
   244 
   245 end;