src/Pure/goal_display.ML
author wenzelm
Fri Sep 03 15:54:03 2010 +0200 (2010-09-03)
changeset 39115 a00da1674c1c
parent 39050 600de0485859
child 39116 f14735a88886
permissions -rw-r--r--
turned show_no_free_types into proper configuration option show_free_types, with flipped polarity;
     1 (*  Title:      Pure/goal_display.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Makarius
     4 
     5 Display tactical goal state.
     6 *)
     7 
     8 signature GOAL_DISPLAY =
     9 sig
    10   val goals_limit: int Unsynchronized.ref
    11   val show_consts_default: bool Unsynchronized.ref
    12   val show_consts_value: Config.value Config.T
    13   val show_consts: bool Config.T
    14   val pretty_flexpair: Proof.context -> term * term -> Pretty.T
    15   val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} ->
    16     thm -> Pretty.T list
    17   val pretty_goals_without_context: int -> thm -> Pretty.T list
    18 end;
    19 
    20 structure Goal_Display: GOAL_DISPLAY =
    21 struct
    22 
    23 val goals_limit = Unsynchronized.ref 10;     (*max number of goals to print*)
    24 
    25 (*true: show consts with types in proof state output*)
    26 val show_consts_default = Unsynchronized.ref false;
    27 val show_consts_value =
    28   Config.declare false "show_consts" (fn _ => Config.Bool (! show_consts_default));
    29 val show_consts = Config.bool show_consts_value;
    30 
    31 fun pretty_flexpair ctxt (t, u) = Pretty.block
    32   [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
    33 
    34 
    35 (*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
    36 
    37 local
    38 
    39 fun ins_entry (x, y) =
    40   AList.default (op =) (x, []) #>
    41   AList.map_entry (op =) x (insert (op =) y);
    42 
    43 val add_consts = Term.fold_aterms
    44   (fn Const (c, T) => ins_entry (T, (c, T))
    45     | _ => I);
    46 
    47 val add_vars = Term.fold_aterms
    48   (fn Free (x, T) => ins_entry (T, (x, ~1))
    49     | Var (xi, T) => ins_entry (T, xi)
    50     | _ => I);
    51 
    52 val add_varsT = Term.fold_atyps
    53   (fn TFree (x, S) => ins_entry (S, (x, ~1))
    54     | TVar (xi, S) => ins_entry (S, xi)
    55     | _ => I);
    56 
    57 fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
    58 fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
    59 
    60 fun consts_of t = sort_cnsts (add_consts t []);
    61 fun vars_of t = sort_idxs (add_vars t []);
    62 fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
    63 
    64 in
    65 
    66 fun pretty_goals ctxt0 {total, main, maxgoals} state =
    67   let
    68     val ctxt = Config.put show_free_types false ctxt0;
    69 
    70     val prt_sort = Syntax.pretty_sort ctxt;
    71     val prt_typ = Syntax.pretty_typ ctxt;
    72     val prt_term = Syntax.pretty_term ctxt;
    73 
    74     fun prt_atoms prt prtT (X, xs) = Pretty.block
    75       [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
    76         Pretty.brk 1, prtT X];
    77 
    78     fun prt_var (x, ~1) = prt_term (Syntax.free x)
    79       | prt_var xi = prt_term (Syntax.var xi);
    80 
    81     fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
    82       | prt_varT xi = prt_typ (TVar (xi, []));
    83 
    84     val prt_consts = prt_atoms (prt_term o Const) prt_typ;
    85     val prt_vars = prt_atoms prt_var prt_typ;
    86     val prt_varsT = prt_atoms prt_varT prt_sort;
    87 
    88 
    89     fun pretty_list _ _ [] = []
    90       | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
    91 
    92     fun pretty_subgoal (n, A) = Pretty.markup Markup.subgoal
    93       [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
    94     fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
    95 
    96     val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
    97 
    98     val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
    99     val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
   100     val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
   101 
   102 
   103     val {prop, tpairs, ...} = Thm.rep_thm state;
   104     val (As, B) = Logic.strip_horn prop;
   105     val ngoals = length As;
   106 
   107     fun pretty_gs (types, sorts) =
   108       (if main then [prt_term B] else []) @
   109        (if ngoals = 0 then [Pretty.str "No subgoals!"]
   110         else if ngoals > maxgoals then
   111           pretty_subgoals (take maxgoals As) @
   112           (if total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
   113            else [])
   114         else pretty_subgoals As) @
   115       pretty_ffpairs tpairs @
   116       (if Config.get ctxt show_consts then pretty_consts prop else []) @
   117       (if types then pretty_vars prop else []) @
   118       (if sorts then pretty_varsT prop else []);
   119   in
   120     setmp_CRITICAL show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
   121       (setmp_CRITICAL show_sorts false pretty_gs)
   122    (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
   123   end;
   124 
   125 fun pretty_goals_without_context n th =
   126   pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th))
   127     {total = true, main = true, maxgoals = n} th;
   128 
   129 end;
   130 
   131 end;
   132