# HG changeset patch # User wenzelm # Date 1248510687 -7200 # Node ID cca43ca13f4fe243ea30fb8aa445853fe9e7aa57 # Parent 8026b73cd3570abc5a5655b89cebfa0376da8bde renamed structure Display_Goal to Goal_Display; diff -r 8026b73cd357 -r cca43ca13f4f src/HOL/Tools/Function/lexicographic_order.ML --- a/src/HOL/Tools/Function/lexicographic_order.ML Sat Jul 25 00:53:47 2009 +0200 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Sat Jul 25 10:31:27 2009 +0200 @@ -140,7 +140,7 @@ fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table)) fun pr_goals ctxt st = - Display_Goal.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st + Goal_Display.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st |> Pretty.chunks |> Pretty.string_of diff -r 8026b73cd357 -r cca43ca13f4f src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Sat Jul 25 00:53:47 2009 +0200 +++ b/src/Pure/IsaMakefile Sat Jul 25 10:31:27 2009 +0200 @@ -90,7 +90,7 @@ Tools/find_theorems.ML Tools/named_thms.ML Tools/xml_syntax.ML \ assumption.ML axclass.ML codegen.ML config.ML conjunction.ML \ consts.ML context.ML context_position.ML conv.ML defs.ML display.ML \ - display_goal.ML drule.ML envir.ML facts.ML goal.ML interpretation.ML \ + drule.ML envir.ML facts.ML goal.ML goal_display.ML interpretation.ML \ item_net.ML library.ML logic.ML meta_simplifier.ML more_thm.ML \ morphism.ML name.ML net.ML old_goals.ML old_term.ML pattern.ML \ primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML search.ML \ diff -r 8026b73cd357 -r cca43ca13f4f src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Sat Jul 25 00:53:47 2009 +0200 +++ b/src/Pure/Isar/proof.ML Sat Jul 25 10:31:27 2009 +0200 @@ -344,7 +344,7 @@ (if mode <> Backward orelse null using then NONE else SOME using) @ [Pretty.str ("goal" ^ description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @ - Display_Goal.pretty_goals ctxt + Goal_Display.pretty_goals ctxt {total = true, main = ! show_main_goal, maxgoals = ! Display.goals_limit} goal @ (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages)) | prt_goal NONE = []; @@ -366,7 +366,7 @@ fun pretty_goals main state = let val (ctxt, (_, goal)) = get_goal state in - Display_Goal.pretty_goals ctxt + Goal_Display.pretty_goals ctxt {total = false, main = main, maxgoals = ! Display.goals_limit} goal end; @@ -474,7 +474,7 @@ val ngoals = Thm.nprems_of goal; val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks - (Display_Goal.pretty_goals ctxt + (Goal_Display.pretty_goals ctxt {total = true, main = ! show_main_goal, maxgoals = ! Display.goals_limit} goal @ [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")]))); diff -r 8026b73cd357 -r cca43ca13f4f src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Sat Jul 25 00:53:47 2009 +0200 +++ b/src/Pure/Proof/reconstruct.ML Sat Jul 25 10:31:27 2009 +0200 @@ -255,7 +255,7 @@ let fun search env [] = error ("Unsolvable constraints:\n" ^ Pretty.string_of (Pretty.chunks (map (fn (_, p, _) => - Display_Goal.pretty_flexpair (Syntax.init_pretty_global thy) (pairself + Goal_Display.pretty_flexpair (Syntax.init_pretty_global thy) (pairself (Envir.norm_term bigenv) p)) cs))) | search env ((u, p as (t1, t2), vs)::ps) = if u then diff -r 8026b73cd357 -r cca43ca13f4f src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sat Jul 25 00:53:47 2009 +0200 +++ b/src/Pure/ROOT.ML Sat Jul 25 10:31:27 2009 +0200 @@ -119,7 +119,7 @@ use "morphism.ML"; use "variable.ML"; use "conv.ML"; -use "display_goal.ML"; +use "goal_display.ML"; use "tactical.ML"; use "search.ML"; use "tactic.ML"; diff -r 8026b73cd357 -r cca43ca13f4f src/Pure/display.ML --- a/src/Pure/display.ML Sat Jul 25 00:53:47 2009 +0200 +++ b/src/Pure/display.ML Sat Jul 25 10:31:27 2009 +0200 @@ -42,8 +42,8 @@ (** options **) -val goals_limit = Display_Goal.goals_limit; -val show_consts = Display_Goal.show_consts; +val goals_limit = Goal_Display.goals_limit; +val show_consts = Goal_Display.show_consts; val show_hyps = ref false; (*false: print meta-hypotheses as dots*) val show_tags = ref false; (*false: suppress tags*) @@ -87,7 +87,7 @@ if hlen = 0 andalso status = "" then [] else if ! show_hyps orelse show_hyps' then [Pretty.brk 2, Pretty.list "[" "]" - (map (q o Display_Goal.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @ + (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @ map (Syntax.pretty_sort ctxt) xshyps @ (if status = "" then [] else [Pretty.str status]))] else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")]; diff -r 8026b73cd357 -r cca43ca13f4f src/Pure/display_goal.ML --- a/src/Pure/display_goal.ML Sat Jul 25 00:53:47 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,124 +0,0 @@ -(* Title: Pure/display_goal.ML - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Author: Makarius - -Display tactical goal state. -*) - -signature DISPLAY_GOAL = -sig - val goals_limit: int ref - val show_consts: bool ref - val pretty_flexpair: Proof.context -> term * term -> Pretty.T - val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} -> - thm -> Pretty.T list - val pretty_goals_without_context: int -> thm -> Pretty.T list -end; - -structure Display_Goal: DISPLAY_GOAL = -struct - -val goals_limit = ref 10; (*max number of goals to print*) -val show_consts = ref false; (*true: show consts with types in proof state output*) - -fun pretty_flexpair ctxt (t, u) = Pretty.block - [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u]; - - -(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*) - -local - -fun ins_entry (x, y) = - AList.default (op =) (x, []) #> - AList.map_entry (op =) x (insert (op =) y); - -val add_consts = Term.fold_aterms - (fn Const (c, T) => ins_entry (T, (c, T)) - | _ => I); - -val add_vars = Term.fold_aterms - (fn Free (x, T) => ins_entry (T, (x, ~1)) - | Var (xi, T) => ins_entry (T, xi) - | _ => I); - -val add_varsT = Term.fold_atyps - (fn TFree (x, S) => ins_entry (S, (x, ~1)) - | TVar (xi, S) => ins_entry (S, xi) - | _ => I); - -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 (Term.fold_types add_varsT t [])); - -in - -fun pretty_goals ctxt {total, main, maxgoals} state = - let - val prt_sort = Syntax.pretty_sort ctxt; - val prt_typ = Syntax.pretty_typ ctxt; - val prt_term = Syntax.pretty_term ctxt; - - 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.markup Markup.subgoal - [Pretty.str (" " ^ 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:" (pretty_flexpair ctxt); - - 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, tpairs, ...} = Thm.rep_thm state; - val (As, B) = Logic.strip_horn prop; - val ngoals = length As; - - 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 (Library.take (maxgoals, As)) @ - (if total 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 orelse ! show_all_types) - (setmp show_sorts false pretty_gs)) - (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts) - end; - -fun pretty_goals_without_context n th = - pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th)) - {total = true, main = true, maxgoals = n} th; - -end; - -end; - diff -r 8026b73cd357 -r cca43ca13f4f src/Pure/goal.ML --- a/src/Pure/goal.ML Sat Jul 25 00:53:47 2009 +0200 +++ b/src/Pure/goal.ML Sat Jul 25 10:31:27 2009 +0200 @@ -78,7 +78,7 @@ (case Thm.nprems_of th of 0 => conclude th | n => raise THM ("Proof failed.\n" ^ - Pretty.string_of (Pretty.chunks (Display_Goal.pretty_goals_without_context n th)) ^ + Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals_without_context n th)) ^ ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th])); diff -r 8026b73cd357 -r cca43ca13f4f src/Pure/goal_display.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/goal_display.ML Sat Jul 25 10:31:27 2009 +0200 @@ -0,0 +1,124 @@ +(* Title: Pure/goal_display.ML + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Author: Makarius + +Display tactical goal state. +*) + +signature GOAL_DISPLAY = +sig + val goals_limit: int ref + val show_consts: bool ref + val pretty_flexpair: Proof.context -> term * term -> Pretty.T + val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} -> + thm -> Pretty.T list + val pretty_goals_without_context: int -> thm -> Pretty.T list +end; + +structure Goal_Display: GOAL_DISPLAY = +struct + +val goals_limit = ref 10; (*max number of goals to print*) +val show_consts = ref false; (*true: show consts with types in proof state output*) + +fun pretty_flexpair ctxt (t, u) = Pretty.block + [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u]; + + +(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*) + +local + +fun ins_entry (x, y) = + AList.default (op =) (x, []) #> + AList.map_entry (op =) x (insert (op =) y); + +val add_consts = Term.fold_aterms + (fn Const (c, T) => ins_entry (T, (c, T)) + | _ => I); + +val add_vars = Term.fold_aterms + (fn Free (x, T) => ins_entry (T, (x, ~1)) + | Var (xi, T) => ins_entry (T, xi) + | _ => I); + +val add_varsT = Term.fold_atyps + (fn TFree (x, S) => ins_entry (S, (x, ~1)) + | TVar (xi, S) => ins_entry (S, xi) + | _ => I); + +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 (Term.fold_types add_varsT t [])); + +in + +fun pretty_goals ctxt {total, main, maxgoals} state = + let + val prt_sort = Syntax.pretty_sort ctxt; + val prt_typ = Syntax.pretty_typ ctxt; + val prt_term = Syntax.pretty_term ctxt; + + 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.markup Markup.subgoal + [Pretty.str (" " ^ 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:" (pretty_flexpair ctxt); + + 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, tpairs, ...} = Thm.rep_thm state; + val (As, B) = Logic.strip_horn prop; + val ngoals = length As; + + 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 (Library.take (maxgoals, As)) @ + (if total 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 orelse ! show_all_types) + (setmp show_sorts false pretty_gs)) + (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts) + end; + +fun pretty_goals_without_context n th = + pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th)) + {total = true, main = true, maxgoals = n} th; + +end; + +end; + diff -r 8026b73cd357 -r cca43ca13f4f src/Pure/old_goals.ML --- a/src/Pure/old_goals.ML Sat Jul 25 00:53:47 2009 +0200 +++ b/src/Pure/old_goals.ML Sat Jul 25 10:31:27 2009 +0200 @@ -125,7 +125,7 @@ special applications.*) fun result_error_default state msg : thm = Pretty.str "Bad final proof state:" :: - Display_Goal.pretty_goals_without_context (!goals_limit) state @ + Goal_Display.pretty_goals_without_context (!goals_limit) state @ [Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error; val result_error_fn = ref result_error_default; @@ -267,7 +267,7 @@ (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^ (if ngoals <> 1 then "s" else "") ^ ")" else ""))] @ - Display_Goal.pretty_goals_without_context m th + Goal_Display.pretty_goals_without_context m th end |> Pretty.chunks |> Pretty.writeln; (*Printing can raise exceptions, so the assignment occurs last. diff -r 8026b73cd357 -r cca43ca13f4f src/Pure/tactical.ML --- a/src/Pure/tactical.ML Sat Jul 25 00:53:47 2009 +0200 +++ b/src/Pure/tactical.ML Sat Jul 25 10:31:27 2009 +0200 @@ -194,7 +194,7 @@ fun print_tac msg st = (tracing (msg ^ "\n" ^ Pretty.string_of (Pretty.chunks - (Display_Goal.pretty_goals_without_context (! Display_Goal.goals_limit) st))); + (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st))); Seq.single st); (*Pause until a line is typed -- if non-empty then fail. *) @@ -233,7 +233,7 @@ fun tracify flag tac st = if !flag andalso not (!suppress_tracing) then (tracing (Pretty.string_of (Pretty.chunks - (Display_Goal.pretty_goals_without_context (! Display_Goal.goals_limit) st @ + (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st @ [Pretty.str "** Press RETURN to continue:"]))); exec_trace_command flag (tac, st)) else tac st;