src/Pure/goal_display.ML
changeset 32187 cca43ca13f4f
parent 32168 116461b8fc01
child 32738 15bb09ca0378
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/goal_display.ML	Sat Jul 25 10:31:27 2009 +0200
     1.3 @@ -0,0 +1,124 @@
     1.4 +(*  Title:      Pure/goal_display.ML
     1.5 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Display tactical goal state.
     1.9 +*)
    1.10 +
    1.11 +signature GOAL_DISPLAY =
    1.12 +sig
    1.13 +  val goals_limit: int ref
    1.14 +  val show_consts: bool ref
    1.15 +  val pretty_flexpair: Proof.context -> term * term -> Pretty.T
    1.16 +  val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} ->
    1.17 +    thm -> Pretty.T list
    1.18 +  val pretty_goals_without_context: int -> thm -> Pretty.T list
    1.19 +end;
    1.20 +
    1.21 +structure Goal_Display: GOAL_DISPLAY =
    1.22 +struct
    1.23 +
    1.24 +val goals_limit = ref 10;      (*max number of goals to print*)
    1.25 +val show_consts = ref false;   (*true: show consts with types in proof state output*)
    1.26 +
    1.27 +fun pretty_flexpair ctxt (t, u) = Pretty.block
    1.28 +  [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
    1.29 +
    1.30 +
    1.31 +(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
    1.32 +
    1.33 +local
    1.34 +
    1.35 +fun ins_entry (x, y) =
    1.36 +  AList.default (op =) (x, []) #>
    1.37 +  AList.map_entry (op =) x (insert (op =) y);
    1.38 +
    1.39 +val add_consts = Term.fold_aterms
    1.40 +  (fn Const (c, T) => ins_entry (T, (c, T))
    1.41 +    | _ => I);
    1.42 +
    1.43 +val add_vars = Term.fold_aterms
    1.44 +  (fn Free (x, T) => ins_entry (T, (x, ~1))
    1.45 +    | Var (xi, T) => ins_entry (T, xi)
    1.46 +    | _ => I);
    1.47 +
    1.48 +val add_varsT = Term.fold_atyps
    1.49 +  (fn TFree (x, S) => ins_entry (S, (x, ~1))
    1.50 +    | TVar (xi, S) => ins_entry (S, xi)
    1.51 +    | _ => I);
    1.52 +
    1.53 +fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
    1.54 +fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
    1.55 +
    1.56 +fun consts_of t = sort_cnsts (add_consts t []);
    1.57 +fun vars_of t = sort_idxs (add_vars t []);
    1.58 +fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
    1.59 +
    1.60 +in
    1.61 +
    1.62 +fun pretty_goals ctxt {total, main, maxgoals} state =
    1.63 +  let
    1.64 +    val prt_sort = Syntax.pretty_sort ctxt;
    1.65 +    val prt_typ = Syntax.pretty_typ ctxt;
    1.66 +    val prt_term = Syntax.pretty_term ctxt;
    1.67 +
    1.68 +    fun prt_atoms prt prtT (X, xs) = Pretty.block
    1.69 +      [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
    1.70 +        Pretty.brk 1, prtT X];
    1.71 +
    1.72 +    fun prt_var (x, ~1) = prt_term (Syntax.free x)
    1.73 +      | prt_var xi = prt_term (Syntax.var xi);
    1.74 +
    1.75 +    fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
    1.76 +      | prt_varT xi = prt_typ (TVar (xi, []));
    1.77 +
    1.78 +    val prt_consts = prt_atoms (prt_term o Const) prt_typ;
    1.79 +    val prt_vars = prt_atoms prt_var prt_typ;
    1.80 +    val prt_varsT = prt_atoms prt_varT prt_sort;
    1.81 +
    1.82 +
    1.83 +    fun pretty_list _ _ [] = []
    1.84 +      | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
    1.85 +
    1.86 +    fun pretty_subgoal (n, A) = Pretty.markup Markup.subgoal
    1.87 +      [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
    1.88 +    fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
    1.89 +
    1.90 +    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
    1.91 +
    1.92 +    val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
    1.93 +    val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
    1.94 +    val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
    1.95 +
    1.96 +
    1.97 +    val {prop, tpairs, ...} = Thm.rep_thm state;
    1.98 +    val (As, B) = Logic.strip_horn prop;
    1.99 +    val ngoals = length As;
   1.100 +
   1.101 +    fun pretty_gs (types, sorts) =
   1.102 +      (if main then [prt_term B] else []) @
   1.103 +       (if ngoals = 0 then [Pretty.str "No subgoals!"]
   1.104 +        else if ngoals > maxgoals then
   1.105 +          pretty_subgoals (Library.take (maxgoals, As)) @
   1.106 +          (if total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
   1.107 +           else [])
   1.108 +        else pretty_subgoals As) @
   1.109 +      pretty_ffpairs tpairs @
   1.110 +      (if ! show_consts then pretty_consts prop else []) @
   1.111 +      (if types then pretty_vars prop else []) @
   1.112 +      (if sorts then pretty_varsT prop else []);
   1.113 +  in
   1.114 +    setmp show_no_free_types true
   1.115 +      (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
   1.116 +        (setmp show_sorts false pretty_gs))
   1.117 +   (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
   1.118 +  end;
   1.119 +
   1.120 +fun pretty_goals_without_context n th =
   1.121 +  pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th))
   1.122 +    {total = true, main = true, maxgoals = n} th;
   1.123 +
   1.124 +end;
   1.125 +
   1.126 +end;
   1.127 +