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