# HG changeset patch # User wenzelm # Date 1005087143 -3600 # Node ID f9735aad76dca03c032f0c98d24c0460b618670a # Parent 4c1e3a2a87c3ef4f6d4c8b74cc4b4eac59643c27 added goals_limit (from tctical.ML); added pretty_goals_aux, removed excessive variants of print_goals; diff -r 4c1e3a2a87c3 -r f9735aad76dc src/Pure/display.ML --- a/src/Pure/display.ML Tue Nov 06 23:51:16 2001 +0100 +++ b/src/Pure/display.ML Tue Nov 06 23:52:23 2001 +0100 @@ -8,6 +8,7 @@ signature BASIC_DISPLAY = sig + val goals_limit: int ref val show_hyps: bool ref val show_tags: bool ref val string_of_thm: thm -> string @@ -27,7 +28,7 @@ signature DISPLAY = sig include BASIC_DISPLAY - val pretty_thm_aux: (sort -> Pretty.T) -> (term -> Pretty.T) -> bool -> thm -> Pretty.T + val pretty_thm_aux: (sort -> Pretty.T) * (term -> Pretty.T) -> bool -> thm -> Pretty.T val pretty_thm_no_quote: thm -> Pretty.T val pretty_thm: thm -> Pretty.T val pretty_thms: thm list -> Pretty.T @@ -42,10 +43,9 @@ 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 pretty_goals_marker: string -> int -> thm -> Pretty.T list + val pretty_goals_aux: (sort -> Pretty.T) * (typ -> Pretty.T) * (term -> Pretty.T) + -> string -> bool * bool -> 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) @@ -58,13 +58,14 @@ (** print thm **) +val goals_limit = ref 10; (*max number of goals to print -- set by user*) val show_hyps = ref true; (*false: print meta-hypotheses as dots*) val show_tags = ref false; (*false: suppress tags*) fun pretty_tag (name, args) = Pretty.strs (name :: map quote args); val pretty_tags = Pretty.list "[" "]" o map pretty_tag; -fun pretty_thm_aux pretty_sort pretty_term quote th = +fun pretty_thm_aux (pretty_sort, pretty_term) quote th = let val {hyps, prop, der = (ora, _), ...} = rep_thm th; val xshyps = Thm.extra_shyps th; @@ -88,7 +89,7 @@ fun gen_pretty_thm quote th = let val sg = Thm.sign_of_thm th - in pretty_thm_aux (Sign.pretty_sort sg) (Sign.pretty_term sg) quote th end; + in pretty_thm_aux (Sign.pretty_sort sg, Sign.pretty_term sg) quote th end; val pretty_thm = gen_pretty_thm true; val pretty_thm_no_quote = gen_pretty_thm false; @@ -252,105 +253,99 @@ 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 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_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_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_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 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 sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs; +fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs; + +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, []))); + +in - 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 pretty_goals_aux (prt_sort, prt_typ, prt_term) begin_goal (msg, main) maxgoals state = + let + fun prt_atoms prt prtT (X, xs) = Pretty.block + [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::", + Pretty.brk 1, prtT X]; - fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs; - fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs; + 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; - (* 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 pretty_list _ _ [] = [] + | pretty_list name prt lst = [Pretty.big_list name (map prt lst)]; - 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 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); - fun prt_varT (x, ~1) = prt_typ (TFree (x, [])) - | prt_varT xi = prt_typ (TVar (xi, [])); + val pretty_ffpairs = pretty_list "flex-flex pairs:" (prt_term o Logic.mk_flexpair); - 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; + 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; - 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; + 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) + fun pretty_gs (types, sorts) = + (if main then [prt_term B] else []) @ + (if ngoals = 0 then [Pretty.str "No subgoals!"] + else if ngoals > maxgoals then + pretty_subgoals (take (maxgoals, As)) @ + (if 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 ""; +fun pretty_goals_marker bg n th = + let val sg = Thm.sign_of_thm th in + pretty_goals_aux (Sign.pretty_sort sg, Sign.pretty_typ sg, Sign.pretty_term sg) + bg (true, true) n th + end; + +val pretty_goals = pretty_goals_marker ""; +val print_goals_marker = (Pretty.writeln o Pretty.chunks) ooo pretty_goals_marker; +val print_goals = print_goals_marker ""; + end;