1.1 --- a/src/Pure/display.ML Mon Oct 22 17:58:56 2001 +0200
1.2 +++ b/src/Pure/display.ML Mon Oct 22 17:59:39 2001 +0200
1.3 @@ -6,45 +6,59 @@
1.4 Printing of theories, theorems, etc.
1.5 *)
1.6
1.7 +signature BASIC_DISPLAY =
1.8 +sig
1.9 + val show_hyps: bool ref
1.10 + val show_tags: bool ref
1.11 + val string_of_thm: thm -> string
1.12 + val print_thm: thm -> unit
1.13 + val print_thms: thm list -> unit
1.14 + val prth: thm -> thm
1.15 + val prthq: thm Seq.seq -> thm Seq.seq
1.16 + val prths: thm list -> thm list
1.17 + val string_of_ctyp: ctyp -> string
1.18 + val print_ctyp: ctyp -> unit
1.19 + val string_of_cterm: cterm -> string
1.20 + val print_cterm: cterm -> unit
1.21 + val print_syntax: theory -> unit
1.22 + val show_consts: bool ref
1.23 +end;
1.24 +
1.25 signature DISPLAY =
1.26 sig
1.27 - val show_hyps : bool ref
1.28 - val show_tags : bool ref
1.29 + include BASIC_DISPLAY
1.30 val pretty_thm_no_quote: thm -> Pretty.T
1.31 - val pretty_thm : thm -> Pretty.T
1.32 - val pretty_thms : thm list -> Pretty.T
1.33 - val pretty_thm_sg : Sign.sg -> thm -> Pretty.T
1.34 - val pretty_thms_sg : Sign.sg -> thm list -> Pretty.T
1.35 - val string_of_thm : thm -> string
1.36 - val pprint_thm : thm -> pprint_args -> unit
1.37 - val print_thm : thm -> unit
1.38 - val print_thms : thm list -> unit
1.39 - val prth : thm -> thm
1.40 - val prthq : thm Seq.seq -> thm Seq.seq
1.41 - val prths : thm list -> thm list
1.42 - val pretty_ctyp : ctyp -> Pretty.T
1.43 - val pprint_ctyp : ctyp -> pprint_args -> unit
1.44 - val string_of_ctyp : ctyp -> string
1.45 - val print_ctyp : ctyp -> unit
1.46 - val pretty_cterm : cterm -> Pretty.T
1.47 - val pprint_cterm : cterm -> pprint_args -> unit
1.48 - val string_of_cterm : cterm -> string
1.49 - val print_cterm : cterm -> unit
1.50 - val pretty_theory : theory -> Pretty.T
1.51 - val pprint_theory : theory -> pprint_args -> unit
1.52 - val print_syntax : theory -> unit
1.53 + val pretty_thm: thm -> Pretty.T
1.54 + val pretty_thms: thm list -> Pretty.T
1.55 + val pretty_thm_sg: Sign.sg -> thm -> Pretty.T
1.56 + val pretty_thms_sg: Sign.sg -> thm list -> Pretty.T
1.57 + val pprint_thm: thm -> pprint_args -> unit
1.58 + val pretty_ctyp: ctyp -> Pretty.T
1.59 + val pprint_ctyp: ctyp -> pprint_args -> unit
1.60 + val pretty_cterm: cterm -> Pretty.T
1.61 + val pprint_cterm: cterm -> pprint_args -> unit
1.62 + val pretty_theory: theory -> Pretty.T
1.63 + val pprint_theory: theory -> pprint_args -> unit
1.64 val pretty_full_theory: theory -> Pretty.T list
1.65 - val pretty_name_space : string * NameSpace.T -> Pretty.T
1.66 - val show_consts : bool ref
1.67 + val pretty_name_space: string * NameSpace.T -> Pretty.T
1.68 + val pretty_goals_marker: string -> int -> thm -> Pretty.T list
1.69 + val pretty_goals: int -> thm -> Pretty.T list
1.70 + val pretty_sub_goals: bool -> int -> thm -> Pretty.T list
1.71 + val print_goals_marker: string -> int -> thm -> unit
1.72 + val print_goals: int -> thm -> unit
1.73 + val current_goals_markers: (string * string * string) ref
1.74 + val print_current_goals_default: (int -> int -> thm -> unit)
1.75 + val print_current_goals_fn : (int -> int -> thm -> unit) ref
1.76 end;
1.77
1.78 structure Display: DISPLAY =
1.79 struct
1.80
1.81 +
1.82 (** print thm **)
1.83
1.84 -val show_hyps = ref true; (*false: print meta-hypotheses as dots*)
1.85 -val show_tags = ref false; (*false: suppress tags*)
1.86 +val show_hyps = ref true; (*false: print meta-hypotheses as dots*)
1.87 +val show_tags = ref false; (*false: suppress tags*)
1.88
1.89 local
1.90
1.91 @@ -153,8 +167,7 @@
1.92 end;
1.93
1.94
1.95 -
1.96 -(* print theory *)
1.97 +(* pretty_full_theory *)
1.98
1.99 fun pretty_full_theory thy =
1.100 let
1.101 @@ -227,10 +240,142 @@
1.102 end;
1.103
1.104
1.105 +
1.106 +(** print_goals **)
1.107 +
1.108 +(* print_goals etc. *)
1.109 +
1.110 (*show consts with types in proof state output?*)
1.111 val show_consts = ref false;
1.112
1.113
1.114 +(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
1.115 +
1.116 +local
1.117 +
1.118 + (* utils *)
1.119 +
1.120 + fun ins_entry (x, y) [] = [(x, [y])]
1.121 + | ins_entry (x, y) ((pair as (x', ys')) :: pairs) =
1.122 + if x = x' then (x', y ins ys') :: pairs
1.123 + else pair :: ins_entry (x, y) pairs;
1.124 +
1.125 + fun add_consts (Const (c, T), env) = ins_entry (T, (c, T)) env
1.126 + | add_consts (t $ u, env) = add_consts (u, add_consts (t, env))
1.127 + | add_consts (Abs (_, _, t), env) = add_consts (t, env)
1.128 + | add_consts (_, env) = env;
1.129 +
1.130 + fun add_vars (Free (x, T), env) = ins_entry (T, (x, ~1)) env
1.131 + | add_vars (Var (xi, T), env) = ins_entry (T, xi) env
1.132 + | add_vars (Abs (_, _, t), env) = add_vars (t, env)
1.133 + | add_vars (t $ u, env) = add_vars (u, add_vars (t, env))
1.134 + | add_vars (_, env) = env;
1.135 +
1.136 + fun add_varsT (Type (_, Ts), env) = foldr add_varsT (Ts, env)
1.137 + | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
1.138 + | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
1.139 +
1.140 + fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
1.141 + fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
1.142 +
1.143 +
1.144 + (* prepare atoms *)
1.145 +
1.146 + fun consts_of t = sort_cnsts (add_consts (t, []));
1.147 + fun vars_of t = sort_idxs (add_vars (t, []));
1.148 + fun varsT_of t = rev (sort_idxs (it_term_types add_varsT (t, [])));
1.149 +
1.150 + fun pretty_goals_marker_aux begin_goal print_msg print_goal maxgoals state =
1.151 + let
1.152 + val {sign, ...} = rep_thm state;
1.153 +
1.154 + val prt_term = Sign.pretty_term sign;
1.155 + val prt_typ = Sign.pretty_typ sign;
1.156 + val prt_sort = Sign.pretty_sort sign;
1.157 +
1.158 + fun prt_atoms prt prtT (X, xs) = Pretty.block
1.159 + [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
1.160 + Pretty.brk 1, prtT X];
1.161 +
1.162 + fun prt_var (x, ~1) = prt_term (Syntax.free x)
1.163 + | prt_var xi = prt_term (Syntax.var xi);
1.164 +
1.165 + fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
1.166 + | prt_varT xi = prt_typ (TVar (xi, []));
1.167 +
1.168 + val prt_consts = prt_atoms (prt_term o Const) prt_typ;
1.169 + val prt_vars = prt_atoms prt_var prt_typ;
1.170 + val prt_varsT = prt_atoms prt_varT prt_sort;
1.171 +
1.172 +
1.173 + fun pretty_list _ _ [] = []
1.174 + | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
1.175 +
1.176 + fun pretty_subgoal (n, A) =
1.177 + Pretty.blk (0, [Pretty.str (begin_goal ^ " " ^ string_of_int n ^ ". "), prt_term A]);
1.178 + fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
1.179 +
1.180 + val pretty_ffpairs = pretty_list "flex-flex pairs:" (prt_term o Logic.mk_flexpair);
1.181 +
1.182 + val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
1.183 + val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
1.184 + val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
1.185 +
1.186 +
1.187 + val {prop, ...} = rep_thm state;
1.188 + val (tpairs, As, B) = Logic.strip_horn prop;
1.189 + val ngoals = length As;
1.190 +
1.191 + fun pretty_gs (types, sorts) =
1.192 + (if print_goal then [prt_term B] else []) @
1.193 + (if ngoals = 0 then [Pretty.str "No subgoals!"]
1.194 + else if ngoals > maxgoals then
1.195 + pretty_subgoals (take (maxgoals, As)) @
1.196 + (if print_msg then
1.197 + [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
1.198 + else [])
1.199 + else pretty_subgoals As) @
1.200 + pretty_ffpairs tpairs @
1.201 + (if ! show_consts then pretty_consts prop else []) @
1.202 + (if types then pretty_vars prop else []) @
1.203 + (if sorts then pretty_varsT prop else []);
1.204 + in
1.205 + setmp show_no_free_types true
1.206 + (setmp show_types (! show_types orelse ! show_sorts)
1.207 + (setmp show_sorts false pretty_gs))
1.208 + (! show_types orelse ! show_sorts, ! show_sorts)
1.209 + end;
1.210 +
1.211 +in
1.212 + fun pretty_goals_marker bg = pretty_goals_marker_aux bg true true;
1.213 + val print_goals_marker = (Pretty.writeln o Pretty.chunks) ooo pretty_goals_marker;
1.214 + val pretty_sub_goals = pretty_goals_marker_aux "" false;
1.215 + val pretty_goals = pretty_goals_marker "";
1.216 + val print_goals = print_goals_marker "";
1.217 end;
1.218
1.219 -open Display;
1.220 +
1.221 +(* print_current_goals *)
1.222 +
1.223 +val current_goals_markers = ref ("", "", "");
1.224 +
1.225 +fun print_current_goals_default n max th =
1.226 + let
1.227 + val ref (begin_state, end_state, begin_goal) = current_goals_markers;
1.228 + val ngoals = nprems_of th;
1.229 + in
1.230 + if begin_state = "" then () else writeln begin_state;
1.231 + writeln ("Level " ^ string_of_int n ^
1.232 + (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
1.233 + (if ngoals <> 1 then "s" else "") ^ ")"
1.234 + else ""));
1.235 + print_goals_marker begin_goal max th;
1.236 + if end_state = "" then () else writeln end_state
1.237 + end;
1.238 +
1.239 +val print_current_goals_fn = ref print_current_goals_default;
1.240 +
1.241 +end;
1.242 +
1.243 +structure BasicDisplay: BASIC_DISPLAY = Display;
1.244 +open BasicDisplay;