src/Pure/Isar/proof_display.ML
author wenzelm
Wed Apr 06 16:33:33 2016 +0200 (2016-04-06)
changeset 62889 99c7f31615c2
parent 62188 74c56f8b68e8
child 64596 51f8e259de50
permissions -rw-r--r--
clarified modules;
tuned signature;
     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_theory: bool -> Proof.context -> Pretty.T
    16   val pretty_definitions: bool -> Proof.context -> Pretty.T
    17   val pretty_theorems_diff: bool -> theory list -> Proof.context -> Pretty.T list
    18   val pretty_theorems: bool -> Proof.context -> Pretty.T list
    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.get_generic_context () 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   Thm.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 fun pretty_theory verbose ctxt =
    64   let
    65     val thy = Proof_Context.theory_of ctxt;
    66 
    67     fun prt_cls c = Syntax.pretty_sort ctxt [c];
    68     fun prt_sort S = Syntax.pretty_sort ctxt S;
    69     fun prt_arity t (c, Ss) = Syntax.pretty_arity ctxt (t, Ss, [c]);
    70     fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty);
    71     val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global;
    72     fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
    73     val prt_term_no_vars = prt_term o Logic.unvarify_global;
    74     fun prt_const (c, ty) = [Pretty.mark_str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
    75 
    76     fun pretty_classrel (c, []) = prt_cls c
    77       | pretty_classrel (c, cs) = Pretty.block
    78           (prt_cls c :: Pretty.str " <" :: Pretty.brk 1 :: Pretty.commas (map prt_cls cs));
    79 
    80     fun pretty_default S = Pretty.block
    81       [Pretty.str "default sort:", Pretty.brk 1, prt_sort S];
    82 
    83     val tfrees = map (fn v => TFree (v, []));
    84     fun pretty_type syn (t, Type.LogicalType n) =
    85           if syn then NONE
    86           else SOME (prt_typ (Type (t, tfrees (Name.invent Name.context Name.aT n))))
    87       | pretty_type syn (t, Type.Abbreviation (vs, U, syn')) =
    88           if syn <> syn' then NONE
    89           else SOME (Pretty.block
    90             [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U])
    91       | pretty_type syn (t, Type.Nonterminal) =
    92           if not syn then NONE
    93           else SOME (prt_typ (Type (t, [])));
    94 
    95     val pretty_arities = maps (fn (t, ars) => map (prt_arity t) ars);
    96 
    97     fun pretty_abbrev (c, (ty, t)) = Pretty.block
    98       (prt_const (c, ty) @ [Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t]);
    99 
   100     fun pretty_axm (a, t) =
   101       Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t];
   102 
   103     val tsig = Sign.tsig_of thy;
   104     val consts = Sign.consts_of thy;
   105     val {const_space, constants, constraints} = Consts.dest consts;
   106     val {classes, default, types, ...} = Type.rep_tsig tsig;
   107     val type_space = Type.type_space tsig;
   108     val (class_space, class_algebra) = classes;
   109     val classes = Sorts.classes_of class_algebra;
   110     val arities = Sorts.arities_of class_algebra;
   111 
   112     val clsses =
   113       Name_Space.extern_entries verbose ctxt class_space
   114         (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes))
   115       |> map (apfst #1);
   116     val tdecls = Name_Space.extern_table verbose ctxt types |> map (apfst #1);
   117     val arties =
   118       Name_Space.extern_entries verbose ctxt type_space (Symtab.dest arities)
   119       |> map (apfst #1);
   120 
   121     val cnsts = Name_Space.markup_entries verbose ctxt const_space constants;
   122     val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
   123     val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
   124     val cnstrs = Name_Space.markup_entries verbose ctxt const_space constraints;
   125 
   126     val axms = Name_Space.markup_table verbose ctxt (Theory.axiom_table thy);
   127   in
   128     Pretty.chunks
   129      [Pretty.big_list "classes:" (map pretty_classrel clsses),
   130       pretty_default default,
   131       Pretty.big_list "syntactic types:" (map_filter (pretty_type true) tdecls),
   132       Pretty.big_list "logical types:" (map_filter (pretty_type false) tdecls),
   133       Pretty.big_list "type arities:" (pretty_arities arties),
   134       Pretty.big_list "logical consts:" (map (Pretty.block o prt_const) log_cnsts),
   135       Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
   136       Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
   137       Pretty.big_list "axioms:" (map pretty_axm axms),
   138       Pretty.block
   139         (Pretty.breaks (Pretty.str "oracles:" ::
   140           map Pretty.mark_str (Thm.extern_oracles verbose ctxt)))]
   141   end;
   142 
   143 
   144 (* theorems *)
   145 
   146 fun pretty_theorems_diff verbose prev_thys ctxt =
   147   let
   148     val pretty_fact = Proof_Context.pretty_fact ctxt;
   149     val facts = Global_Theory.facts_of (Proof_Context.theory_of ctxt);
   150     val thmss = Facts.dest_static verbose (map Global_Theory.facts_of prev_thys) facts;
   151     val prts = map #1 (sort_by (#1 o #2) (map (`pretty_fact) thmss));
   152   in if null prts then [] else [Pretty.big_list "theorems:" prts] end;
   153 
   154 fun pretty_theorems verbose ctxt =
   155   pretty_theorems_diff verbose (Theory.parents_of (Proof_Context.theory_of ctxt)) ctxt;
   156 
   157 
   158 (* definitions *)
   159 
   160 fun pretty_definitions verbose ctxt =
   161   let
   162     val thy = Proof_Context.theory_of ctxt;
   163     val context = Proof_Context.defs_context ctxt;
   164 
   165     val const_space = Proof_Context.const_space ctxt;
   166     val type_space = Proof_Context.type_space ctxt;
   167     val item_space = fn Defs.Const => const_space | Defs.Type => type_space;
   168     fun prune_item (k, c) = not verbose andalso Name_Space.is_concealed (item_space k) c;
   169 
   170     fun extern_item (kind, name) =
   171       let val xname = Name_Space.extern ctxt (item_space kind) name
   172       in (xname, (kind, name)) end;
   173 
   174     fun extern_item_ord ((xname1, (kind1, _)), (xname2, (kind2, _))) =
   175       (case Defs.item_kind_ord (kind1, kind2) of
   176         EQUAL => string_ord (xname1, xname2)
   177       | ord => ord);
   178 
   179     fun sort_items f = sort (extern_item_ord o apply2 f);
   180 
   181     fun pretty_entry ((_: string, item), args) = Defs.pretty_entry context (item, args);
   182 
   183     fun pretty_reduct (lhs, rhs) = Pretty.block
   184       ([pretty_entry lhs, Pretty.str "  ->", Pretty.brk 2] @
   185         Pretty.commas (map pretty_entry (sort_items fst rhs)));
   186 
   187     fun pretty_restrict (entry, name) =
   188       Pretty.block ([pretty_entry entry, Pretty.brk 2, Pretty.str ("(from " ^ quote name ^ ")")]);
   189 
   190     val defs = Theory.defs_of thy;
   191     val {restricts, reducts} = Defs.dest defs;
   192 
   193     val (reds1, reds2) =
   194       filter_out (prune_item o #1 o #1) reducts
   195       |> map (fn (lhs, rhs) =>
   196         (apfst extern_item lhs, map (apfst extern_item) (filter_out (prune_item o fst) rhs)))
   197       |> sort_items (#1 o #1)
   198       |> filter_out (null o #2)
   199       |> List.partition (Defs.plain_args o #2 o #1);
   200 
   201     val rests = restricts |> map (apfst (apfst extern_item)) |> sort_items (#1 o #1);
   202   in
   203     Pretty.big_list "definitions:"
   204       (map (Pretty.text_fold o single)
   205         [Pretty.big_list "non-overloaded LHS:" (map pretty_reduct reds1),
   206          Pretty.big_list "overloaded LHS:" (map pretty_reduct reds2),
   207          Pretty.big_list "pattern restrictions due to incomplete LHS:" (map pretty_restrict rests)])
   208   end;
   209 
   210 
   211 
   212 (** proof items **)
   213 
   214 (* refinement rule *)
   215 
   216 fun pretty_rule ctxt s thm =
   217   Pretty.block [Pretty.str (s ^ " attempt to solve goal by exported rule:"),
   218     Pretty.fbrk, Thm.pretty_thm ctxt thm];
   219 
   220 val string_of_rule = Pretty.string_of ooo pretty_rule;
   221 
   222 
   223 (* goals *)
   224 
   225 local
   226 
   227 fun subgoals 0 = []
   228   | subgoals 1 = [Pretty.brk 1, Pretty.str "(1 subgoal)"]
   229   | subgoals n = [Pretty.brk 1, Pretty.str ("(" ^ string_of_int n ^ " subgoals)")];
   230 
   231 in
   232 
   233 fun pretty_goal_header goal =
   234   Pretty.block ([Pretty.keyword1 "goal"] @ subgoals (Thm.nprems_of goal) @ [Pretty.str ":"]);
   235 
   236 end;
   237 
   238 fun string_of_goal ctxt goal =
   239   Pretty.string_of (Pretty.chunks [pretty_goal_header goal, Goal_Display.pretty_goal ctxt goal]);
   240 
   241 
   242 (* goal facts *)
   243 
   244 fun pretty_goal_facts ctxt s ths =
   245   (Pretty.block o Pretty.fbreaks)
   246     [if s = "" then Pretty.str "this:"
   247      else Pretty.block [Pretty.keyword1 s, Pretty.brk 1, Pretty.str "this:"],
   248      Proof_Context.pretty_fact ctxt ("", ths)];
   249 
   250 
   251 (* method_error *)
   252 
   253 fun method_error kind pos {context = ctxt, facts, goal} = Seq.Error (fn () =>
   254   let
   255     val pr_header =
   256       "Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^
   257       "proof method" ^ Position.here pos ^ ":\n";
   258     val pr_facts =
   259       if null facts then ""
   260       else Pretty.string_of (pretty_goal_facts ctxt "using" facts) ^ "\n";
   261     val pr_goal = string_of_goal ctxt goal;
   262   in pr_header ^ pr_facts ^ pr_goal end);
   263 
   264 
   265 (* results *)
   266 
   267 fun position_markup pos = Pretty.mark (Position.markup pos Markup.position);
   268 
   269 local
   270 
   271 fun pretty_fact_name pos (kind, "") = position_markup pos (Pretty.keyword1 kind)
   272   | pretty_fact_name pos (kind, name) =
   273       Pretty.block [position_markup pos (Pretty.keyword1 kind), Pretty.brk 1,
   274         Pretty.str (Long_Name.base_name name), Pretty.str ":"];
   275 
   276 fun pretty_facts ctxt =
   277   flat o (separate [Pretty.fbrk, Pretty.keyword2 "and", Pretty.str " "]) o
   278     map (single o Proof_Context.pretty_fact ctxt);
   279 
   280 in
   281 
   282 fun print_results do_print pos ctxt ((kind, name), facts) =
   283   if not do_print orelse kind = "" then ()
   284   else if name = "" then
   285     (Output.state o Pretty.string_of)
   286       (Pretty.block (position_markup pos (Pretty.keyword1 kind) :: Pretty.brk 1 ::
   287         pretty_facts ctxt facts))
   288   else
   289     (Output.state o Pretty.string_of)
   290       (case facts of
   291         [fact] => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
   292           Proof_Context.pretty_fact ctxt fact])
   293       | _ => Pretty.blk (1, [pretty_fact_name pos (kind, name), Pretty.fbrk,
   294           Pretty.blk (1, Pretty.str "(" :: pretty_facts ctxt facts @ [Pretty.str ")"])]));
   295 
   296 end;
   297 
   298 
   299 (* consts *)
   300 
   301 local
   302 
   303 fun pretty_var ctxt (x, T) =
   304   Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
   305     Pretty.quote (Syntax.pretty_typ ctxt T)];
   306 
   307 fun pretty_vars pos ctxt kind vs =
   308   Pretty.block
   309     (Pretty.fbreaks (position_markup pos (Pretty.mark_str kind) :: map (pretty_var ctxt) vs));
   310 
   311 val fixes = (Markup.keyword2, "fixes");
   312 val consts = (Markup.keyword1, "consts");
   313 
   314 fun pretty_consts pos ctxt pred cs =
   315   (case filter pred (#1 (Proof_Context.inferred_fixes ctxt)) of
   316     [] => pretty_vars pos ctxt consts cs
   317   | ps => Pretty.chunks [pretty_vars pos ctxt fixes ps, pretty_vars pos ctxt consts cs]);
   318 
   319 in
   320 
   321 fun print_consts do_print pos ctxt pred cs =
   322   if not do_print orelse null cs then ()
   323   else Output.state (Pretty.string_of (pretty_consts pos ctxt pred cs));
   324 
   325 end;
   326 
   327 end;