src/Pure/display_goal.ML
author wenzelm
Mon Jul 20 21:20:09 2009 +0200 (2009-07-20)
changeset 32089 568a23753e3a
child 32145 220c9e439d39
permissions -rw-r--r--
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
load display.ML after assumption.ML, to accomodate proper contextual theorem display;
wenzelm@32089
     1
(*  Title:      Pure/display_goal.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@32089
     8
signature DISPLAY_GOAL =
wenzelm@32089
     9
sig
wenzelm@32089
    10
  val goals_limit: int ref
wenzelm@32089
    11
  val show_consts: bool ref
wenzelm@32089
    12
  val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
wenzelm@32089
    13
  val pretty_goals_aux: Pretty.pp -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list
wenzelm@32089
    14
  val pretty_goals: int -> thm -> Pretty.T list
wenzelm@32089
    15
  val print_goals: int -> thm -> unit
wenzelm@32089
    16
end;
wenzelm@32089
    17
wenzelm@32089
    18
structure Display_Goal: DISPLAY_GOAL =
wenzelm@32089
    19
struct
wenzelm@32089
    20
wenzelm@32089
    21
val goals_limit = ref 10;      (*max number of goals to print*)
wenzelm@32089
    22
val show_consts = ref false;   (*true: show consts with types in proof state output*)
wenzelm@32089
    23
wenzelm@32089
    24
fun pretty_flexpair pp (t, u) = Pretty.block
wenzelm@32089
    25
  [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
wenzelm@32089
    26
wenzelm@32089
    27
wenzelm@32089
    28
(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
wenzelm@32089
    29
wenzelm@32089
    30
local
wenzelm@32089
    31
wenzelm@32089
    32
fun ins_entry (x, y) =
wenzelm@32089
    33
  AList.default (op =) (x, []) #>
wenzelm@32089
    34
  AList.map_entry (op =) x (insert (op =) y);
wenzelm@32089
    35
wenzelm@32089
    36
val add_consts = Term.fold_aterms
wenzelm@32089
    37
  (fn Const (c, T) => ins_entry (T, (c, T))
wenzelm@32089
    38
    | _ => I);
wenzelm@32089
    39
wenzelm@32089
    40
val add_vars = Term.fold_aterms
wenzelm@32089
    41
  (fn Free (x, T) => ins_entry (T, (x, ~1))
wenzelm@32089
    42
    | Var (xi, T) => ins_entry (T, xi)
wenzelm@32089
    43
    | _ => I);
wenzelm@32089
    44
wenzelm@32089
    45
val add_varsT = Term.fold_atyps
wenzelm@32089
    46
  (fn TFree (x, S) => ins_entry (S, (x, ~1))
wenzelm@32089
    47
    | TVar (xi, S) => ins_entry (S, xi)
wenzelm@32089
    48
    | _ => I);
wenzelm@32089
    49
wenzelm@32089
    50
fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
wenzelm@32089
    51
fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
wenzelm@32089
    52
wenzelm@32089
    53
fun consts_of t = sort_cnsts (add_consts t []);
wenzelm@32089
    54
fun vars_of t = sort_idxs (add_vars t []);
wenzelm@32089
    55
fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
wenzelm@32089
    56
wenzelm@32089
    57
in
wenzelm@32089
    58
wenzelm@32089
    59
fun pretty_goals_aux pp markup (msg, main) maxgoals state =
wenzelm@32089
    60
  let
wenzelm@32089
    61
    fun prt_atoms prt prtT (X, xs) = Pretty.block
wenzelm@32089
    62
      [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
wenzelm@32089
    63
        Pretty.brk 1, prtT X];
wenzelm@32089
    64
wenzelm@32089
    65
    fun prt_var (x, ~1) = Pretty.term pp (Syntax.free x)
wenzelm@32089
    66
      | prt_var xi = Pretty.term pp (Syntax.var xi);
wenzelm@32089
    67
wenzelm@32089
    68
    fun prt_varT (x, ~1) = Pretty.typ pp (TFree (x, []))
wenzelm@32089
    69
      | prt_varT xi = Pretty.typ pp (TVar (xi, []));
wenzelm@32089
    70
wenzelm@32089
    71
    val prt_consts = prt_atoms (Pretty.term pp o Const) (Pretty.typ pp);
wenzelm@32089
    72
    val prt_vars = prt_atoms prt_var (Pretty.typ pp);
wenzelm@32089
    73
    val prt_varsT = prt_atoms prt_varT (Pretty.sort pp);
wenzelm@32089
    74
wenzelm@32089
    75
wenzelm@32089
    76
    fun pretty_list _ _ [] = []
wenzelm@32089
    77
      | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
wenzelm@32089
    78
wenzelm@32089
    79
    fun pretty_subgoal (n, A) = Pretty.markup markup
wenzelm@32089
    80
      [Pretty.str (" " ^ string_of_int n ^ ". "), Pretty.term pp A];
wenzelm@32089
    81
    fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
wenzelm@32089
    82
wenzelm@32089
    83
    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair pp);
wenzelm@32089
    84
wenzelm@32089
    85
    val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
wenzelm@32089
    86
    val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
wenzelm@32089
    87
    val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
wenzelm@32089
    88
wenzelm@32089
    89
wenzelm@32089
    90
    val {prop, tpairs, ...} = Thm.rep_thm state;
wenzelm@32089
    91
    val (As, B) = Logic.strip_horn prop;
wenzelm@32089
    92
    val ngoals = length As;
wenzelm@32089
    93
wenzelm@32089
    94
    fun pretty_gs (types, sorts) =
wenzelm@32089
    95
      (if main then [Pretty.term pp B] else []) @
wenzelm@32089
    96
       (if ngoals = 0 then [Pretty.str "No subgoals!"]
wenzelm@32089
    97
        else if ngoals > maxgoals then
wenzelm@32089
    98
          pretty_subgoals (Library.take (maxgoals, As)) @
wenzelm@32089
    99
          (if msg then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
wenzelm@32089
   100
           else [])
wenzelm@32089
   101
        else pretty_subgoals As) @
wenzelm@32089
   102
      pretty_ffpairs tpairs @
wenzelm@32089
   103
      (if ! show_consts then pretty_consts prop else []) @
wenzelm@32089
   104
      (if types then pretty_vars prop else []) @
wenzelm@32089
   105
      (if sorts then pretty_varsT prop else []);
wenzelm@32089
   106
  in
wenzelm@32089
   107
    setmp show_no_free_types true
wenzelm@32089
   108
      (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
wenzelm@32089
   109
        (setmp show_sorts false pretty_gs))
wenzelm@32089
   110
   (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
wenzelm@32089
   111
  end;
wenzelm@32089
   112
wenzelm@32089
   113
fun pretty_goals n th =
wenzelm@32089
   114
  pretty_goals_aux (Syntax.pp_global (Thm.theory_of_thm th)) Markup.none (true, true) n th;
wenzelm@32089
   115
wenzelm@32089
   116
val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals;
wenzelm@32089
   117
wenzelm@32089
   118
end;
wenzelm@32089
   119
wenzelm@32089
   120
end;
wenzelm@32089
   121