--- a/src/Pure/display.ML Mon Oct 22 17:58:56 2001 +0200
+++ b/src/Pure/display.ML Mon Oct 22 17:59:39 2001 +0200
@@ -6,45 +6,59 @@
Printing of theories, theorems, etc.
*)
+signature BASIC_DISPLAY =
+sig
+ val show_hyps: bool ref
+ val show_tags: bool ref
+ val string_of_thm: thm -> string
+ val print_thm: thm -> unit
+ val print_thms: thm list -> unit
+ val prth: thm -> thm
+ val prthq: thm Seq.seq -> thm Seq.seq
+ val prths: thm list -> thm list
+ val string_of_ctyp: ctyp -> string
+ val print_ctyp: ctyp -> unit
+ val string_of_cterm: cterm -> string
+ val print_cterm: cterm -> unit
+ val print_syntax: theory -> unit
+ val show_consts: bool ref
+end;
+
signature DISPLAY =
sig
- val show_hyps : bool ref
- val show_tags : bool ref
+ include BASIC_DISPLAY
val pretty_thm_no_quote: thm -> Pretty.T
- val pretty_thm : thm -> Pretty.T
- val pretty_thms : thm list -> Pretty.T
- val pretty_thm_sg : Sign.sg -> thm -> Pretty.T
- val pretty_thms_sg : Sign.sg -> thm list -> Pretty.T
- val string_of_thm : thm -> string
- val pprint_thm : thm -> pprint_args -> unit
- val print_thm : thm -> unit
- val print_thms : thm list -> unit
- val prth : thm -> thm
- val prthq : thm Seq.seq -> thm Seq.seq
- val prths : thm list -> thm list
- val pretty_ctyp : ctyp -> Pretty.T
- val pprint_ctyp : ctyp -> pprint_args -> unit
- val string_of_ctyp : ctyp -> string
- val print_ctyp : ctyp -> unit
- val pretty_cterm : cterm -> Pretty.T
- val pprint_cterm : cterm -> pprint_args -> unit
- val string_of_cterm : cterm -> string
- val print_cterm : cterm -> unit
- val pretty_theory : theory -> Pretty.T
- val pprint_theory : theory -> pprint_args -> unit
- val print_syntax : theory -> unit
+ val pretty_thm: thm -> Pretty.T
+ val pretty_thms: thm list -> Pretty.T
+ val pretty_thm_sg: Sign.sg -> thm -> Pretty.T
+ val pretty_thms_sg: Sign.sg -> thm list -> Pretty.T
+ val pprint_thm: thm -> pprint_args -> unit
+ val pretty_ctyp: ctyp -> Pretty.T
+ val pprint_ctyp: ctyp -> pprint_args -> unit
+ val pretty_cterm: cterm -> Pretty.T
+ val pprint_cterm: cterm -> pprint_args -> unit
+ val pretty_theory: theory -> Pretty.T
+ val pprint_theory: theory -> pprint_args -> unit
val pretty_full_theory: theory -> Pretty.T list
- val pretty_name_space : string * NameSpace.T -> Pretty.T
- val show_consts : bool ref
+ val pretty_name_space: string * NameSpace.T -> Pretty.T
+ val pretty_goals_marker: string -> int -> thm -> Pretty.T list
+ val pretty_goals: int -> thm -> Pretty.T list
+ val pretty_sub_goals: bool -> int -> thm -> Pretty.T list
+ val print_goals_marker: string -> int -> thm -> unit
+ val print_goals: int -> thm -> unit
+ val current_goals_markers: (string * string * string) ref
+ val print_current_goals_default: (int -> int -> thm -> unit)
+ val print_current_goals_fn : (int -> int -> thm -> unit) ref
end;
structure Display: DISPLAY =
struct
+
(** print thm **)
-val show_hyps = ref true; (*false: print meta-hypotheses as dots*)
-val show_tags = ref false; (*false: suppress tags*)
+val show_hyps = ref true; (*false: print meta-hypotheses as dots*)
+val show_tags = ref false; (*false: suppress tags*)
local
@@ -153,8 +167,7 @@
end;
-
-(* print theory *)
+(* pretty_full_theory *)
fun pretty_full_theory thy =
let
@@ -227,10 +240,142 @@
end;
+
+(** print_goals **)
+
+(* print_goals etc. *)
+
(*show consts with types in proof state output?*)
val show_consts = ref false;
+(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
+
+local
+
+ (* utils *)
+
+ fun ins_entry (x, y) [] = [(x, [y])]
+ | ins_entry (x, y) ((pair as (x', ys')) :: pairs) =
+ if x = x' then (x', y ins ys') :: pairs
+ else pair :: ins_entry (x, y) pairs;
+
+ fun add_consts (Const (c, T), env) = ins_entry (T, (c, T)) env
+ | add_consts (t $ u, env) = add_consts (u, add_consts (t, env))
+ | add_consts (Abs (_, _, t), env) = add_consts (t, env)
+ | add_consts (_, env) = env;
+
+ fun add_vars (Free (x, T), env) = ins_entry (T, (x, ~1)) env
+ | add_vars (Var (xi, T), env) = ins_entry (T, xi) env
+ | add_vars (Abs (_, _, t), env) = add_vars (t, env)
+ | add_vars (t $ u, env) = add_vars (u, add_vars (t, env))
+ | add_vars (_, env) = env;
+
+ fun add_varsT (Type (_, Ts), env) = foldr add_varsT (Ts, env)
+ | add_varsT (TFree (x, S), env) = ins_entry (S, (x, ~1)) env
+ | add_varsT (TVar (xi, S), env) = ins_entry (S, xi) env;
+
+ fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
+ fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
+
+
+ (* prepare atoms *)
+
+ fun consts_of t = sort_cnsts (add_consts (t, []));
+ fun vars_of t = sort_idxs (add_vars (t, []));
+ fun varsT_of t = rev (sort_idxs (it_term_types add_varsT (t, [])));
+
+ fun pretty_goals_marker_aux begin_goal print_msg print_goal maxgoals state =
+ let
+ val {sign, ...} = rep_thm state;
+
+ val prt_term = Sign.pretty_term sign;
+ val prt_typ = Sign.pretty_typ sign;
+ val prt_sort = Sign.pretty_sort sign;
+
+ fun prt_atoms prt prtT (X, xs) = Pretty.block
+ [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
+ Pretty.brk 1, prtT X];
+
+ fun prt_var (x, ~1) = prt_term (Syntax.free x)
+ | prt_var xi = prt_term (Syntax.var xi);
+
+ fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
+ | prt_varT xi = prt_typ (TVar (xi, []));
+
+ val prt_consts = prt_atoms (prt_term o Const) prt_typ;
+ val prt_vars = prt_atoms prt_var prt_typ;
+ val prt_varsT = prt_atoms prt_varT prt_sort;
+
+
+ fun pretty_list _ _ [] = []
+ | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
+
+ fun pretty_subgoal (n, A) =
+ Pretty.blk (0, [Pretty.str (begin_goal ^ " " ^ string_of_int n ^ ". "), prt_term A]);
+ fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
+
+ val pretty_ffpairs = pretty_list "flex-flex pairs:" (prt_term o Logic.mk_flexpair);
+
+ val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
+ val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
+ val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
+
+
+ val {prop, ...} = rep_thm state;
+ val (tpairs, As, B) = Logic.strip_horn prop;
+ val ngoals = length As;
+
+ fun pretty_gs (types, sorts) =
+ (if print_goal then [prt_term B] else []) @
+ (if ngoals = 0 then [Pretty.str "No subgoals!"]
+ else if ngoals > maxgoals then
+ pretty_subgoals (take (maxgoals, As)) @
+ (if print_msg then
+ [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
+ else [])
+ else pretty_subgoals As) @
+ pretty_ffpairs tpairs @
+ (if ! show_consts then pretty_consts prop else []) @
+ (if types then pretty_vars prop else []) @
+ (if sorts then pretty_varsT prop else []);
+ in
+ setmp show_no_free_types true
+ (setmp show_types (! show_types orelse ! show_sorts)
+ (setmp show_sorts false pretty_gs))
+ (! show_types orelse ! show_sorts, ! show_sorts)
+ end;
+
+in
+ fun pretty_goals_marker bg = pretty_goals_marker_aux bg true true;
+ val print_goals_marker = (Pretty.writeln o Pretty.chunks) ooo pretty_goals_marker;
+ val pretty_sub_goals = pretty_goals_marker_aux "" false;
+ val pretty_goals = pretty_goals_marker "";
+ val print_goals = print_goals_marker "";
end;
-open Display;
+
+(* print_current_goals *)
+
+val current_goals_markers = ref ("", "", "");
+
+fun print_current_goals_default n max th =
+ let
+ val ref (begin_state, end_state, begin_goal) = current_goals_markers;
+ val ngoals = nprems_of th;
+ in
+ if begin_state = "" then () else writeln begin_state;
+ writeln ("Level " ^ string_of_int n ^
+ (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
+ (if ngoals <> 1 then "s" else "") ^ ")"
+ else ""));
+ print_goals_marker begin_goal max th;
+ if end_state = "" then () else writeln end_state
+ end;
+
+val print_current_goals_fn = ref print_current_goals_default;
+
+end;
+
+structure BasicDisplay: BASIC_DISPLAY = Display;
+open BasicDisplay;