renamed structure Display_Goal to Goal_Display;
authorwenzelm
Sat Jul 25 10:31:27 2009 +0200 (2009-07-25)
changeset 32187cca43ca13f4f
parent 32186 8026b73cd357
child 32188 005f9abae1e3
renamed structure Display_Goal to Goal_Display;
src/HOL/Tools/Function/lexicographic_order.ML
src/Pure/IsaMakefile
src/Pure/Isar/proof.ML
src/Pure/Proof/reconstruct.ML
src/Pure/ROOT.ML
src/Pure/display.ML
src/Pure/display_goal.ML
src/Pure/goal.ML
src/Pure/goal_display.ML
src/Pure/old_goals.ML
src/Pure/tactical.ML
     1.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Sat Jul 25 00:53:47 2009 +0200
     1.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Sat Jul 25 10:31:27 2009 +0200
     1.3 @@ -140,7 +140,7 @@
     1.4  fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table))
     1.5  
     1.6  fun pr_goals ctxt st =
     1.7 -    Display_Goal.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st
     1.8 +    Goal_Display.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st
     1.9       |> Pretty.chunks
    1.10       |> Pretty.string_of
    1.11  
     2.1 --- a/src/Pure/IsaMakefile	Sat Jul 25 00:53:47 2009 +0200
     2.2 +++ b/src/Pure/IsaMakefile	Sat Jul 25 10:31:27 2009 +0200
     2.3 @@ -90,7 +90,7 @@
     2.4    Tools/find_theorems.ML Tools/named_thms.ML Tools/xml_syntax.ML	\
     2.5    assumption.ML axclass.ML codegen.ML config.ML conjunction.ML		\
     2.6    consts.ML context.ML context_position.ML conv.ML defs.ML display.ML	\
     2.7 -  display_goal.ML drule.ML envir.ML facts.ML goal.ML interpretation.ML	\
     2.8 +  drule.ML envir.ML facts.ML goal.ML goal_display.ML interpretation.ML	\
     2.9    item_net.ML library.ML logic.ML meta_simplifier.ML more_thm.ML	\
    2.10    morphism.ML name.ML net.ML old_goals.ML old_term.ML pattern.ML	\
    2.11    primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML search.ML	\
     3.1 --- a/src/Pure/Isar/proof.ML	Sat Jul 25 00:53:47 2009 +0200
     3.2 +++ b/src/Pure/Isar/proof.ML	Sat Jul 25 10:31:27 2009 +0200
     3.3 @@ -344,7 +344,7 @@
     3.4              (if mode <> Backward orelse null using then NONE else SOME using) @
     3.5            [Pretty.str ("goal" ^
     3.6              description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @
     3.7 -          Display_Goal.pretty_goals ctxt
     3.8 +          Goal_Display.pretty_goals ctxt
     3.9              {total = true, main = ! show_main_goal, maxgoals = ! Display.goals_limit} goal @
    3.10            (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
    3.11        | prt_goal NONE = [];
    3.12 @@ -366,7 +366,7 @@
    3.13  
    3.14  fun pretty_goals main state =
    3.15    let val (ctxt, (_, goal)) = get_goal state in
    3.16 -    Display_Goal.pretty_goals ctxt
    3.17 +    Goal_Display.pretty_goals ctxt
    3.18        {total = false, main = main, maxgoals = ! Display.goals_limit} goal
    3.19    end;
    3.20  
    3.21 @@ -474,7 +474,7 @@
    3.22  
    3.23      val ngoals = Thm.nprems_of goal;
    3.24      val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks
    3.25 -      (Display_Goal.pretty_goals ctxt
    3.26 +      (Goal_Display.pretty_goals ctxt
    3.27            {total = true, main = ! show_main_goal, maxgoals = ! Display.goals_limit} goal @
    3.28          [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])));
    3.29  
     4.1 --- a/src/Pure/Proof/reconstruct.ML	Sat Jul 25 00:53:47 2009 +0200
     4.2 +++ b/src/Pure/Proof/reconstruct.ML	Sat Jul 25 10:31:27 2009 +0200
     4.3 @@ -255,7 +255,7 @@
     4.4        let
     4.5          fun search env [] = error ("Unsolvable constraints:\n" ^
     4.6                Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
     4.7 -                Display_Goal.pretty_flexpair (Syntax.init_pretty_global thy) (pairself
     4.8 +                Goal_Display.pretty_flexpair (Syntax.init_pretty_global thy) (pairself
     4.9                    (Envir.norm_term bigenv) p)) cs)))
    4.10            | search env ((u, p as (t1, t2), vs)::ps) =
    4.11                if u then
     5.1 --- a/src/Pure/ROOT.ML	Sat Jul 25 00:53:47 2009 +0200
     5.2 +++ b/src/Pure/ROOT.ML	Sat Jul 25 10:31:27 2009 +0200
     5.3 @@ -119,7 +119,7 @@
     5.4  use "morphism.ML";
     5.5  use "variable.ML";
     5.6  use "conv.ML";
     5.7 -use "display_goal.ML";
     5.8 +use "goal_display.ML";
     5.9  use "tactical.ML";
    5.10  use "search.ML";
    5.11  use "tactic.ML";
     6.1 --- a/src/Pure/display.ML	Sat Jul 25 00:53:47 2009 +0200
     6.2 +++ b/src/Pure/display.ML	Sat Jul 25 10:31:27 2009 +0200
     6.3 @@ -42,8 +42,8 @@
     6.4  
     6.5  (** options **)
     6.6  
     6.7 -val goals_limit = Display_Goal.goals_limit;
     6.8 -val show_consts = Display_Goal.show_consts;
     6.9 +val goals_limit = Goal_Display.goals_limit;
    6.10 +val show_consts = Goal_Display.show_consts;
    6.11  
    6.12  val show_hyps = ref false;      (*false: print meta-hypotheses as dots*)
    6.13  val show_tags = ref false;      (*false: suppress tags*)
    6.14 @@ -87,7 +87,7 @@
    6.15        if hlen = 0 andalso status = "" then []
    6.16        else if ! show_hyps orelse show_hyps' then
    6.17          [Pretty.brk 2, Pretty.list "[" "]"
    6.18 -          (map (q o Display_Goal.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @
    6.19 +          (map (q o Goal_Display.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @
    6.20             map (Syntax.pretty_sort ctxt) xshyps @
    6.21              (if status = "" then [] else [Pretty.str status]))]
    6.22        else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")];
     7.1 --- a/src/Pure/display_goal.ML	Sat Jul 25 00:53:47 2009 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,124 +0,0 @@
     7.4 -(*  Title:      Pure/display_goal.ML
     7.5 -    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     7.6 -    Author:     Makarius
     7.7 -
     7.8 -Display tactical goal state.
     7.9 -*)
    7.10 -
    7.11 -signature DISPLAY_GOAL =
    7.12 -sig
    7.13 -  val goals_limit: int ref
    7.14 -  val show_consts: bool ref
    7.15 -  val pretty_flexpair: Proof.context -> term * term -> Pretty.T
    7.16 -  val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} ->
    7.17 -    thm -> Pretty.T list
    7.18 -  val pretty_goals_without_context: int -> thm -> Pretty.T list
    7.19 -end;
    7.20 -
    7.21 -structure Display_Goal: DISPLAY_GOAL =
    7.22 -struct
    7.23 -
    7.24 -val goals_limit = ref 10;      (*max number of goals to print*)
    7.25 -val show_consts = ref false;   (*true: show consts with types in proof state output*)
    7.26 -
    7.27 -fun pretty_flexpair ctxt (t, u) = Pretty.block
    7.28 -  [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
    7.29 -
    7.30 -
    7.31 -(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
    7.32 -
    7.33 -local
    7.34 -
    7.35 -fun ins_entry (x, y) =
    7.36 -  AList.default (op =) (x, []) #>
    7.37 -  AList.map_entry (op =) x (insert (op =) y);
    7.38 -
    7.39 -val add_consts = Term.fold_aterms
    7.40 -  (fn Const (c, T) => ins_entry (T, (c, T))
    7.41 -    | _ => I);
    7.42 -
    7.43 -val add_vars = Term.fold_aterms
    7.44 -  (fn Free (x, T) => ins_entry (T, (x, ~1))
    7.45 -    | Var (xi, T) => ins_entry (T, xi)
    7.46 -    | _ => I);
    7.47 -
    7.48 -val add_varsT = Term.fold_atyps
    7.49 -  (fn TFree (x, S) => ins_entry (S, (x, ~1))
    7.50 -    | TVar (xi, S) => ins_entry (S, xi)
    7.51 -    | _ => I);
    7.52 -
    7.53 -fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
    7.54 -fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
    7.55 -
    7.56 -fun consts_of t = sort_cnsts (add_consts t []);
    7.57 -fun vars_of t = sort_idxs (add_vars t []);
    7.58 -fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
    7.59 -
    7.60 -in
    7.61 -
    7.62 -fun pretty_goals ctxt {total, main, maxgoals} state =
    7.63 -  let
    7.64 -    val prt_sort = Syntax.pretty_sort ctxt;
    7.65 -    val prt_typ = Syntax.pretty_typ ctxt;
    7.66 -    val prt_term = Syntax.pretty_term ctxt;
    7.67 -
    7.68 -    fun prt_atoms prt prtT (X, xs) = Pretty.block
    7.69 -      [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
    7.70 -        Pretty.brk 1, prtT X];
    7.71 -
    7.72 -    fun prt_var (x, ~1) = prt_term (Syntax.free x)
    7.73 -      | prt_var xi = prt_term (Syntax.var xi);
    7.74 -
    7.75 -    fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
    7.76 -      | prt_varT xi = prt_typ (TVar (xi, []));
    7.77 -
    7.78 -    val prt_consts = prt_atoms (prt_term o Const) prt_typ;
    7.79 -    val prt_vars = prt_atoms prt_var prt_typ;
    7.80 -    val prt_varsT = prt_atoms prt_varT prt_sort;
    7.81 -
    7.82 -
    7.83 -    fun pretty_list _ _ [] = []
    7.84 -      | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
    7.85 -
    7.86 -    fun pretty_subgoal (n, A) = Pretty.markup Markup.subgoal
    7.87 -      [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
    7.88 -    fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
    7.89 -
    7.90 -    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
    7.91 -
    7.92 -    val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
    7.93 -    val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
    7.94 -    val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
    7.95 -
    7.96 -
    7.97 -    val {prop, tpairs, ...} = Thm.rep_thm state;
    7.98 -    val (As, B) = Logic.strip_horn prop;
    7.99 -    val ngoals = length As;
   7.100 -
   7.101 -    fun pretty_gs (types, sorts) =
   7.102 -      (if main then [prt_term B] else []) @
   7.103 -       (if ngoals = 0 then [Pretty.str "No subgoals!"]
   7.104 -        else if ngoals > maxgoals then
   7.105 -          pretty_subgoals (Library.take (maxgoals, As)) @
   7.106 -          (if total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
   7.107 -           else [])
   7.108 -        else pretty_subgoals As) @
   7.109 -      pretty_ffpairs tpairs @
   7.110 -      (if ! show_consts then pretty_consts prop else []) @
   7.111 -      (if types then pretty_vars prop else []) @
   7.112 -      (if sorts then pretty_varsT prop else []);
   7.113 -  in
   7.114 -    setmp show_no_free_types true
   7.115 -      (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
   7.116 -        (setmp show_sorts false pretty_gs))
   7.117 -   (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
   7.118 -  end;
   7.119 -
   7.120 -fun pretty_goals_without_context n th =
   7.121 -  pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th))
   7.122 -    {total = true, main = true, maxgoals = n} th;
   7.123 -
   7.124 -end;
   7.125 -
   7.126 -end;
   7.127 -
     8.1 --- a/src/Pure/goal.ML	Sat Jul 25 00:53:47 2009 +0200
     8.2 +++ b/src/Pure/goal.ML	Sat Jul 25 10:31:27 2009 +0200
     8.3 @@ -78,7 +78,7 @@
     8.4    (case Thm.nprems_of th of
     8.5      0 => conclude th
     8.6    | n => raise THM ("Proof failed.\n" ^
     8.7 -      Pretty.string_of (Pretty.chunks (Display_Goal.pretty_goals_without_context n th)) ^
     8.8 +      Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals_without_context n th)) ^
     8.9        ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th]));
    8.10  
    8.11  
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Pure/goal_display.ML	Sat Jul 25 10:31:27 2009 +0200
     9.3 @@ -0,0 +1,124 @@
     9.4 +(*  Title:      Pure/goal_display.ML
     9.5 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     9.6 +    Author:     Makarius
     9.7 +
     9.8 +Display tactical goal state.
     9.9 +*)
    9.10 +
    9.11 +signature GOAL_DISPLAY =
    9.12 +sig
    9.13 +  val goals_limit: int ref
    9.14 +  val show_consts: bool ref
    9.15 +  val pretty_flexpair: Proof.context -> term * term -> Pretty.T
    9.16 +  val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} ->
    9.17 +    thm -> Pretty.T list
    9.18 +  val pretty_goals_without_context: int -> thm -> Pretty.T list
    9.19 +end;
    9.20 +
    9.21 +structure Goal_Display: GOAL_DISPLAY =
    9.22 +struct
    9.23 +
    9.24 +val goals_limit = ref 10;      (*max number of goals to print*)
    9.25 +val show_consts = ref false;   (*true: show consts with types in proof state output*)
    9.26 +
    9.27 +fun pretty_flexpair ctxt (t, u) = Pretty.block
    9.28 +  [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
    9.29 +
    9.30 +
    9.31 +(*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
    9.32 +
    9.33 +local
    9.34 +
    9.35 +fun ins_entry (x, y) =
    9.36 +  AList.default (op =) (x, []) #>
    9.37 +  AList.map_entry (op =) x (insert (op =) y);
    9.38 +
    9.39 +val add_consts = Term.fold_aterms
    9.40 +  (fn Const (c, T) => ins_entry (T, (c, T))
    9.41 +    | _ => I);
    9.42 +
    9.43 +val add_vars = Term.fold_aterms
    9.44 +  (fn Free (x, T) => ins_entry (T, (x, ~1))
    9.45 +    | Var (xi, T) => ins_entry (T, xi)
    9.46 +    | _ => I);
    9.47 +
    9.48 +val add_varsT = Term.fold_atyps
    9.49 +  (fn TFree (x, S) => ins_entry (S, (x, ~1))
    9.50 +    | TVar (xi, S) => ins_entry (S, xi)
    9.51 +    | _ => I);
    9.52 +
    9.53 +fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
    9.54 +fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
    9.55 +
    9.56 +fun consts_of t = sort_cnsts (add_consts t []);
    9.57 +fun vars_of t = sort_idxs (add_vars t []);
    9.58 +fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
    9.59 +
    9.60 +in
    9.61 +
    9.62 +fun pretty_goals ctxt {total, main, maxgoals} state =
    9.63 +  let
    9.64 +    val prt_sort = Syntax.pretty_sort ctxt;
    9.65 +    val prt_typ = Syntax.pretty_typ ctxt;
    9.66 +    val prt_term = Syntax.pretty_term ctxt;
    9.67 +
    9.68 +    fun prt_atoms prt prtT (X, xs) = Pretty.block
    9.69 +      [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
    9.70 +        Pretty.brk 1, prtT X];
    9.71 +
    9.72 +    fun prt_var (x, ~1) = prt_term (Syntax.free x)
    9.73 +      | prt_var xi = prt_term (Syntax.var xi);
    9.74 +
    9.75 +    fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
    9.76 +      | prt_varT xi = prt_typ (TVar (xi, []));
    9.77 +
    9.78 +    val prt_consts = prt_atoms (prt_term o Const) prt_typ;
    9.79 +    val prt_vars = prt_atoms prt_var prt_typ;
    9.80 +    val prt_varsT = prt_atoms prt_varT prt_sort;
    9.81 +
    9.82 +
    9.83 +    fun pretty_list _ _ [] = []
    9.84 +      | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
    9.85 +
    9.86 +    fun pretty_subgoal (n, A) = Pretty.markup Markup.subgoal
    9.87 +      [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
    9.88 +    fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
    9.89 +
    9.90 +    val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
    9.91 +
    9.92 +    val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
    9.93 +    val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
    9.94 +    val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
    9.95 +
    9.96 +
    9.97 +    val {prop, tpairs, ...} = Thm.rep_thm state;
    9.98 +    val (As, B) = Logic.strip_horn prop;
    9.99 +    val ngoals = length As;
   9.100 +
   9.101 +    fun pretty_gs (types, sorts) =
   9.102 +      (if main then [prt_term B] else []) @
   9.103 +       (if ngoals = 0 then [Pretty.str "No subgoals!"]
   9.104 +        else if ngoals > maxgoals then
   9.105 +          pretty_subgoals (Library.take (maxgoals, As)) @
   9.106 +          (if total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
   9.107 +           else [])
   9.108 +        else pretty_subgoals As) @
   9.109 +      pretty_ffpairs tpairs @
   9.110 +      (if ! show_consts then pretty_consts prop else []) @
   9.111 +      (if types then pretty_vars prop else []) @
   9.112 +      (if sorts then pretty_varsT prop else []);
   9.113 +  in
   9.114 +    setmp show_no_free_types true
   9.115 +      (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
   9.116 +        (setmp show_sorts false pretty_gs))
   9.117 +   (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
   9.118 +  end;
   9.119 +
   9.120 +fun pretty_goals_without_context n th =
   9.121 +  pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th))
   9.122 +    {total = true, main = true, maxgoals = n} th;
   9.123 +
   9.124 +end;
   9.125 +
   9.126 +end;
   9.127 +
    10.1 --- a/src/Pure/old_goals.ML	Sat Jul 25 00:53:47 2009 +0200
    10.2 +++ b/src/Pure/old_goals.ML	Sat Jul 25 10:31:27 2009 +0200
    10.3 @@ -125,7 +125,7 @@
    10.4    special applications.*)
    10.5  fun result_error_default state msg : thm =
    10.6    Pretty.str "Bad final proof state:" ::
    10.7 -      Display_Goal.pretty_goals_without_context (!goals_limit) state @
    10.8 +      Goal_Display.pretty_goals_without_context (!goals_limit) state @
    10.9      [Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error;
   10.10  
   10.11  val result_error_fn = ref result_error_default;
   10.12 @@ -267,7 +267,7 @@
   10.13        (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^
   10.14          (if ngoals <> 1 then "s" else "") ^ ")"
   10.15        else ""))] @
   10.16 -    Display_Goal.pretty_goals_without_context m th
   10.17 +    Goal_Display.pretty_goals_without_context m th
   10.18    end |> Pretty.chunks |> Pretty.writeln;
   10.19  
   10.20  (*Printing can raise exceptions, so the assignment occurs last.
    11.1 --- a/src/Pure/tactical.ML	Sat Jul 25 00:53:47 2009 +0200
    11.2 +++ b/src/Pure/tactical.ML	Sat Jul 25 10:31:27 2009 +0200
    11.3 @@ -194,7 +194,7 @@
    11.4  fun print_tac msg st =
    11.5   (tracing (msg ^ "\n" ^
    11.6      Pretty.string_of (Pretty.chunks
    11.7 -      (Display_Goal.pretty_goals_without_context (! Display_Goal.goals_limit) st)));
    11.8 +      (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st)));
    11.9    Seq.single st);
   11.10  
   11.11  (*Pause until a line is typed -- if non-empty then fail. *)
   11.12 @@ -233,7 +233,7 @@
   11.13  fun tracify flag tac st =
   11.14    if !flag andalso not (!suppress_tracing) then
   11.15      (tracing (Pretty.string_of (Pretty.chunks
   11.16 -        (Display_Goal.pretty_goals_without_context (! Display_Goal.goals_limit) st @
   11.17 +        (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st @
   11.18            [Pretty.str "** Press RETURN to continue:"])));
   11.19       exec_trace_command flag (tac, st))
   11.20    else tac st;