# HG changeset patch # User wenzelm # Date 1248117609 -7200 # Node ID 568a23753e3a8fe150c1c10fd19655282142b0f5 # Parent 2110fcd86efbea48f4ab5bbcc97d620c547d4695 moved pretty_goals etc. to Display_Goal (required by tracing tacticals); load display.ML after assumption.ML, to accomodate proper contextual theorem display; diff -r 2110fcd86efb -r 568a23753e3a src/HOL/Tools/Function/lexicographic_order.ML --- a/src/HOL/Tools/Function/lexicographic_order.ML Mon Jul 20 20:03:19 2009 +0200 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Mon Jul 20 21:20:09 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.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st + Display_Goal.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st |> Pretty.chunks |> Pretty.string_of diff -r 2110fcd86efb -r 568a23753e3a src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Mon Jul 20 20:03:19 2009 +0200 +++ b/src/Pure/IsaMakefile Mon Jul 20 21:20:09 2009 +0200 @@ -90,13 +90,13 @@ 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 \ - drule.ML envir.ML facts.ML goal.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 sign.ML \ - simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML \ - term_ord.ML term_subst.ML theory.ML thm.ML type.ML type_infer.ML \ - unify.ML variable.ML + display_goal.ML drule.ML envir.ML facts.ML goal.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 \ + sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML \ + term.ML term_ord.ML term_subst.ML theory.ML thm.ML type.ML \ + type_infer.ML unify.ML variable.ML @./mk diff -r 2110fcd86efb -r 568a23753e3a src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Mon Jul 20 20:03:19 2009 +0200 +++ b/src/Pure/Isar/proof.ML Mon Jul 20 21:20:09 2009 +0200 @@ -318,7 +318,7 @@ val show_main_goal = ref false; val verbose = ProofContext.verbose; -val pretty_goals_local = Display.pretty_goals_aux o Syntax.pp; +val pretty_goals_local = Display_Goal.pretty_goals_aux o Syntax.pp; fun pretty_facts _ _ NONE = [] | pretty_facts s ctxt (SOME ths) = diff -r 2110fcd86efb -r 568a23753e3a src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Mon Jul 20 20:03:19 2009 +0200 +++ b/src/Pure/Proof/reconstruct.ML Mon Jul 20 21:20:09 2009 +0200 @@ -255,7 +255,7 @@ let fun search env [] = error ("Unsolvable constraints:\n" ^ Pretty.string_of (Pretty.chunks (map (fn (_, p, _) => - Display.pretty_flexpair (Syntax.pp_global thy) (pairself + Display_Goal.pretty_flexpair (Syntax.pp_global thy) (pairself (Envir.norm_term bigenv) p)) cs))) | search env ((u, p as (t1, t2), vs)::ps) = if u then diff -r 2110fcd86efb -r 568a23753e3a src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Mon Jul 20 20:03:19 2009 +0200 +++ b/src/Pure/ROOT.ML Mon Jul 20 21:20:09 2009 +0200 @@ -115,17 +115,18 @@ use "more_thm.ML"; use "facts.ML"; use "pure_thy.ML"; -use "display.ML"; use "drule.ML"; use "morphism.ML"; use "variable.ML"; use "conv.ML"; +use "display_goal.ML"; use "tctical.ML"; use "search.ML"; use "tactic.ML"; use "meta_simplifier.ML"; use "conjunction.ML"; use "assumption.ML"; +use "display.ML"; use "goal.ML"; use "axclass.ML"; diff -r 2110fcd86efb -r 568a23753e3a src/Pure/display.ML --- a/src/Pure/display.ML Mon Jul 20 20:03:19 2009 +0200 +++ b/src/Pure/display.ML Mon Jul 20 21:20:09 2009 +0200 @@ -1,22 +1,21 @@ (* Title: Pure/display.ML Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1993 University of Cambridge + Author: Makarius -Printing of theorems, goals, results etc. +Printing of theorems, results etc. *) signature BASIC_DISPLAY = sig val goals_limit: int ref + val show_consts: bool ref val show_hyps: bool ref val show_tags: bool ref - val show_consts: bool ref end; signature DISPLAY = sig include BASIC_DISPLAY - val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T val pretty_thm_aux: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} -> term list -> thm -> Pretty.T val pretty_thm: thm -> Pretty.T @@ -37,27 +36,26 @@ val print_cterm: cterm -> unit val print_syntax: theory -> unit val pretty_full_theory: bool -> theory -> Pretty.T list - val pretty_goals_aux: Pretty.pp -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list - val pretty_goals: int -> thm -> Pretty.T list - val print_goals: int -> thm -> unit end; structure Display: DISPLAY = struct +(** options **) + +val goals_limit = Display_Goal.goals_limit; +val show_consts = Display_Goal.show_consts; + +val show_hyps = ref false; (*false: print meta-hypotheses as dots*) +val show_tags = ref false; (*false: suppress tags*) + + (** print thm **) -val goals_limit = ref 10; (*max number of goals to print*) -val show_hyps = ref false; (*false: print meta-hypotheses as dots*) -val show_tags = ref false; (*false: suppress tags*) - fun pretty_tag (name, arg) = Pretty.strs [name, quote arg]; val pretty_tags = Pretty.list "[" "]" o map pretty_tag; -fun pretty_flexpair pp (t, u) = Pretty.block - [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u]; - fun display_status false _ = "" | display_status true th = let @@ -89,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 pretty_flexpair pp) tpairs @ map prt_term hyps' @ + (map (q o Display_Goal.pretty_flexpair pp) tpairs @ map prt_term hyps' @ map (Pretty.sort pp) xshyps @ (if status = "" then [] else [Pretty.str status]))] else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")]; @@ -242,109 +240,7 @@ Pretty.big_list "pattern restrictions:" (map pretty_restrict rests)]] end; - - -(** print_goals **) - -(* print_goals etc. *) - -val show_consts = ref false; (*true: show consts with types in proof state output*) - - -(*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_aux pp markup (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 prt_var (x, ~1) = Pretty.term pp (Syntax.free x) - | prt_var xi = Pretty.term pp (Syntax.var xi); - - fun prt_varT (x, ~1) = Pretty.typ pp (TFree (x, [])) - | prt_varT xi = Pretty.typ pp (TVar (xi, [])); - - val prt_consts = prt_atoms (Pretty.term pp o Const) (Pretty.typ pp); - val prt_vars = prt_atoms prt_var (Pretty.typ pp); - val prt_varsT = prt_atoms prt_varT (Pretty.sort pp); - - - fun pretty_list _ _ [] = [] - | pretty_list name prt lst = [Pretty.big_list name (map prt lst)]; - - fun pretty_subgoal (n, A) = Pretty.markup markup - [Pretty.str (" " ^ string_of_int n ^ ". "), Pretty.term pp A]; - fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As); - - val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair pp); - - 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 [Pretty.term pp B] else []) @ - (if ngoals = 0 then [Pretty.str "No subgoals!"] - else if ngoals > maxgoals then - pretty_subgoals (Library.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 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 n th = - pretty_goals_aux (Syntax.pp_global (Thm.theory_of_thm th)) Markup.none (true, true) n th; - -val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals; - end; - -end; - -structure BasicDisplay: BASIC_DISPLAY = Display; -open BasicDisplay; +structure Basic_Display: BASIC_DISPLAY = Display; +open Basic_Display; diff -r 2110fcd86efb -r 568a23753e3a src/Pure/display_goal.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/display_goal.ML Mon Jul 20 21:20:09 2009 +0200 @@ -0,0 +1,121 @@ +(* 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: Pretty.pp -> term * term -> Pretty.T + val pretty_goals_aux: Pretty.pp -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list + val pretty_goals: int -> thm -> Pretty.T list + val print_goals: int -> thm -> unit +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 pp (t, u) = Pretty.block + [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp 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_aux pp markup (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 prt_var (x, ~1) = Pretty.term pp (Syntax.free x) + | prt_var xi = Pretty.term pp (Syntax.var xi); + + fun prt_varT (x, ~1) = Pretty.typ pp (TFree (x, [])) + | prt_varT xi = Pretty.typ pp (TVar (xi, [])); + + val prt_consts = prt_atoms (Pretty.term pp o Const) (Pretty.typ pp); + val prt_vars = prt_atoms prt_var (Pretty.typ pp); + val prt_varsT = prt_atoms prt_varT (Pretty.sort pp); + + + fun pretty_list _ _ [] = [] + | pretty_list name prt lst = [Pretty.big_list name (map prt lst)]; + + fun pretty_subgoal (n, A) = Pretty.markup markup + [Pretty.str (" " ^ string_of_int n ^ ". "), Pretty.term pp A]; + fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As); + + val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair pp); + + 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 [Pretty.term pp B] else []) @ + (if ngoals = 0 then [Pretty.str "No subgoals!"] + else if ngoals > maxgoals then + pretty_subgoals (Library.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 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 n th = + pretty_goals_aux (Syntax.pp_global (Thm.theory_of_thm th)) Markup.none (true, true) n th; + +val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals; + +end; + +end; + diff -r 2110fcd86efb -r 568a23753e3a src/Pure/goal.ML --- a/src/Pure/goal.ML Mon Jul 20 20:03:19 2009 +0200 +++ b/src/Pure/goal.ML Mon Jul 20 21:20:09 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.pretty_goals n th)) ^ + Pretty.string_of (Pretty.chunks (Display_Goal.pretty_goals n th)) ^ ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th])); diff -r 2110fcd86efb -r 568a23753e3a src/Pure/old_goals.ML --- a/src/Pure/old_goals.ML Mon Jul 20 20:03:19 2009 +0200 +++ b/src/Pure/old_goals.ML Mon Jul 20 21:20:09 2009 +0200 @@ -135,7 +135,7 @@ (*Default action is to print an error message; could be suppressed for special applications.*) fun result_error_default state msg : thm = - Pretty.str "Bad final proof state:" :: Display.pretty_goals (!goals_limit) state @ + Pretty.str "Bad final proof state:" :: Display_Goal.pretty_goals (!goals_limit) state @ [Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error; val result_error_fn = ref result_error_default; @@ -277,7 +277,7 @@ (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^ (if ngoals <> 1 then "s" else "") ^ ")" else ""))] @ - Display.pretty_goals m th + Display_Goal.pretty_goals m th end |> Pretty.chunks |> Pretty.writeln; (*Printing can raise exceptions, so the assignment occurs last. diff -r 2110fcd86efb -r 568a23753e3a src/Pure/tctical.ML --- a/src/Pure/tctical.ML Mon Jul 20 20:03:19 2009 +0200 +++ b/src/Pure/tctical.ML Mon Jul 20 21:20:09 2009 +0200 @@ -195,7 +195,7 @@ (fn st => (tracing msg; tracing ((Pretty.string_of o Pretty.chunks o - Display.pretty_goals (! Display.goals_limit)) st); + Display_Goal.pretty_goals (! Display_Goal.goals_limit)) st); Seq.single st)); (*Pause until a line is typed -- if non-empty then fail. *) @@ -233,7 +233,7 @@ (*Extract from a tactic, a thm->thm seq function that handles tracing*) fun tracify flag tac st = if !flag andalso not (!suppress_tracing) - then (Display.print_goals (! Display.goals_limit) st; + then (Display_Goal.print_goals (! Display_Goal.goals_limit) st; tracing "** Press RETURN to continue:"; exec_trace_command flag (tac,st)) else tac st;