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