src/Pure/goal_display.ML
author wenzelm
Mon May 13 13:23:13 2013 +0200 (2013-05-13)
changeset 51960 61ac1efe02c3
parent 51959 18d758e38d85
child 52043 286629271d65
permissions -rw-r--r--
option "goals_limit", with more uniform description;
wenzelm@32187
     1
(*  Title:      Pure/goal_display.ML
wenzelm@32089
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@32089
     3
    Author:     Makarius
wenzelm@32089
     4
wenzelm@32089
     5
Display tactical goal state.
wenzelm@32089
     6
*)
wenzelm@32089
     7
wenzelm@32187
     8
signature GOAL_DISPLAY =
wenzelm@32089
     9
sig
wenzelm@39163
    10
  val goals_limit_raw: Config.raw
wenzelm@39125
    11
  val goals_limit: int Config.T
wenzelm@39125
    12
  val show_main_goal_default: bool Unsynchronized.ref
wenzelm@39163
    13
  val show_main_goal_raw: Config.raw
wenzelm@39125
    14
  val show_main_goal: bool Config.T
wenzelm@39050
    15
  val show_consts_default: bool Unsynchronized.ref
wenzelm@39163
    16
  val show_consts_raw: Config.raw
wenzelm@39050
    17
  val show_consts: bool Config.T
wenzelm@32145
    18
  val pretty_flexpair: Proof.context -> term * term -> Pretty.T
wenzelm@39125
    19
  val pretty_goals: Proof.context -> thm -> Pretty.T list
wenzelm@39125
    20
  val pretty_goals_without_context: thm -> Pretty.T list
wenzelm@51958
    21
  val pretty_goal: Proof.context -> thm -> Pretty.T
wenzelm@51958
    22
  val string_of_goal: Proof.context -> thm -> string
wenzelm@32089
    23
end;
wenzelm@32089
    24
wenzelm@32187
    25
structure Goal_Display: GOAL_DISPLAY =
wenzelm@32089
    26
struct
wenzelm@32089
    27
wenzelm@51960
    28
val goals_limit_raw = Config.declare_option "goals_limit";
wenzelm@39163
    29
val goals_limit = Config.int goals_limit_raw;
wenzelm@39125
    30
wenzelm@39125
    31
val show_main_goal_default = Unsynchronized.ref false;
wenzelm@39163
    32
val show_main_goal_raw =
wenzelm@39125
    33
  Config.declare "show_main_goal" (fn _ => Config.Bool (! show_main_goal_default));
wenzelm@39163
    34
val show_main_goal = Config.bool show_main_goal_raw;
wenzelm@39125
    35
wenzelm@39050
    36
val show_consts_default = Unsynchronized.ref false;
wenzelm@39163
    37
val show_consts_raw = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default));
wenzelm@39163
    38
val show_consts = Config.bool show_consts_raw;
wenzelm@32089
    39
wenzelm@32145
    40
fun pretty_flexpair ctxt (t, u) = Pretty.block
wenzelm@32145
    41
  [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
wenzelm@32089
    42
wenzelm@32089
    43
wenzelm@32089
    44
(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
wenzelm@32089
    45
wenzelm@32089
    46
local
wenzelm@32089
    47
wenzelm@32089
    48
fun ins_entry (x, y) =
wenzelm@32089
    49
  AList.default (op =) (x, []) #>
wenzelm@32089
    50
  AList.map_entry (op =) x (insert (op =) y);
wenzelm@32089
    51
wenzelm@32089
    52
val add_consts = Term.fold_aterms
wenzelm@32089
    53
  (fn Const (c, T) => ins_entry (T, (c, T))
wenzelm@32089
    54
    | _ => I);
wenzelm@32089
    55
wenzelm@32089
    56
val add_vars = Term.fold_aterms
wenzelm@32089
    57
  (fn Free (x, T) => ins_entry (T, (x, ~1))
wenzelm@32089
    58
    | Var (xi, T) => ins_entry (T, xi)
wenzelm@32089
    59
    | _ => I);
wenzelm@32089
    60
wenzelm@32089
    61
val add_varsT = Term.fold_atyps
wenzelm@32089
    62
  (fn TFree (x, S) => ins_entry (S, (x, ~1))
wenzelm@32089
    63
    | TVar (xi, S) => ins_entry (S, xi)
wenzelm@32089
    64
    | _ => I);
wenzelm@32089
    65
wenzelm@32089
    66
fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
wenzelm@32089
    67
fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
wenzelm@32089
    68
wenzelm@32089
    69
fun consts_of t = sort_cnsts (add_consts t []);
wenzelm@32089
    70
fun vars_of t = sort_idxs (add_vars t []);
wenzelm@32089
    71
fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
wenzelm@32089
    72
wenzelm@32089
    73
in
wenzelm@32089
    74
wenzelm@39125
    75
fun pretty_goals ctxt0 state =
wenzelm@32089
    76
  let
wenzelm@39134
    77
    val ctxt = ctxt0
wenzelm@39134
    78
      |> Config.put show_free_types false
wenzelm@39134
    79
      |> Config.put show_types
wenzelm@39134
    80
       (Config.get ctxt0 show_types orelse
wenzelm@39134
    81
        Config.get ctxt0 show_sorts orelse
wenzelm@39134
    82
        Config.get ctxt0 show_all_types)
wenzelm@39134
    83
      |> Config.put show_sorts false;
wenzelm@39125
    84
wenzelm@39134
    85
    val show_sorts0 = Config.get ctxt0 show_sorts;
wenzelm@39134
    86
    val show_types = Config.get ctxt show_types;
wenzelm@39134
    87
    val show_consts = Config.get ctxt show_consts
wenzelm@39134
    88
    val show_main_goal = Config.get ctxt show_main_goal;
wenzelm@39125
    89
    val goals_limit = Config.get ctxt goals_limit;
wenzelm@39115
    90
wenzelm@32145
    91
    val prt_sort = Syntax.pretty_sort ctxt;
wenzelm@32145
    92
    val prt_typ = Syntax.pretty_typ ctxt;
wenzelm@32145
    93
    val prt_term = Syntax.pretty_term ctxt;
wenzelm@32145
    94
wenzelm@32089
    95
    fun prt_atoms prt prtT (X, xs) = Pretty.block
wenzelm@32089
    96
      [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
wenzelm@32089
    97
        Pretty.brk 1, prtT X];
wenzelm@32089
    98
wenzelm@32145
    99
    fun prt_var (x, ~1) = prt_term (Syntax.free x)
wenzelm@32145
   100
      | prt_var xi = prt_term (Syntax.var xi);
wenzelm@32089
   101
wenzelm@32145
   102
    fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
wenzelm@32145
   103
      | prt_varT xi = prt_typ (TVar (xi, []));
wenzelm@32089
   104
wenzelm@32145
   105
    val prt_consts = prt_atoms (prt_term o Const) prt_typ;
wenzelm@32145
   106
    val prt_vars = prt_atoms prt_var prt_typ;
wenzelm@32145
   107
    val prt_varsT = prt_atoms prt_varT prt_sort;
wenzelm@32089
   108
wenzelm@32089
   109
wenzelm@32089
   110
    fun pretty_list _ _ [] = []
wenzelm@32089
   111
      | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
wenzelm@32089
   112
wenzelm@50537
   113
    fun pretty_subgoal s A =
wenzelm@50537
   114
      Pretty.markup (Markup.subgoal s) [Pretty.str (" " ^ s ^ ". "), prt_term A];
wenzelm@50537
   115
    val pretty_subgoals = map_index (fn (i, A) => pretty_subgoal (string_of_int (i + 1)) A);
wenzelm@32089
   116
wenzelm@32145
   117
    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
wenzelm@32089
   118
wenzelm@32089
   119
    val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
wenzelm@32089
   120
    val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
wenzelm@32089
   121
    val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
wenzelm@32089
   122
wenzelm@32089
   123
wenzelm@32089
   124
    val {prop, tpairs, ...} = Thm.rep_thm state;
wenzelm@32089
   125
    val (As, B) = Logic.strip_horn prop;
wenzelm@32089
   126
    val ngoals = length As;
wenzelm@32089
   127
  in
wenzelm@50543
   128
    (if show_main_goal then [Pretty.mark Markup.goal (prt_term B)] else []) @
wenzelm@39134
   129
     (if ngoals = 0 then [Pretty.str "No subgoals!"]
wenzelm@39134
   130
      else if ngoals > goals_limit then
wenzelm@39134
   131
        pretty_subgoals (take goals_limit As) @
wenzelm@51959
   132
        [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
wenzelm@39134
   133
      else pretty_subgoals As) @
wenzelm@39134
   134
    pretty_ffpairs tpairs @
wenzelm@39134
   135
    (if show_consts then pretty_consts prop else []) @
wenzelm@39134
   136
    (if show_types then pretty_vars prop else []) @
wenzelm@39134
   137
    (if show_sorts0 then pretty_varsT prop else [])
wenzelm@32089
   138
  end;
wenzelm@32089
   139
wenzelm@39125
   140
fun pretty_goals_without_context th =
wenzelm@39125
   141
  let val ctxt =
wenzelm@39125
   142
    Config.put show_main_goal true (Syntax.init_pretty_global (Thm.theory_of_thm th))
wenzelm@39125
   143
  in pretty_goals ctxt th end;
wenzelm@32089
   144
wenzelm@51959
   145
val pretty_goal = Pretty.chunks oo pretty_goals;
wenzelm@51958
   146
val string_of_goal = Pretty.string_of oo pretty_goal;
wenzelm@49847
   147
wenzelm@32089
   148
end;
wenzelm@32089
   149
wenzelm@32089
   150
end;
wenzelm@32089
   151