src/Pure/goal_display.ML
author wenzelm
Wed Dec 12 23:36:07 2012 +0100 (2012-12-12 ago)
changeset 50499 f496b2b7bafb
parent 50201 c26369c9eda6
child 50537 08ce81aeeacc
permissions -rw-r--r--
rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
     1 (*  Title:      Pure/goal_display.ML
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Author:     Makarius
     4 
     5 Display tactical goal state.
     6 *)
     7 
     8 signature GOAL_DISPLAY =
     9 sig
    10   val goals_limit_default: int Unsynchronized.ref
    11   val goals_limit_raw: Config.raw
    12   val goals_limit: int Config.T
    13   val goals_total: bool Config.T
    14   val show_main_goal_default: bool Unsynchronized.ref
    15   val show_main_goal_raw: Config.raw
    16   val show_main_goal: bool Config.T
    17   val show_consts_default: bool Unsynchronized.ref
    18   val show_consts_raw: Config.raw
    19   val show_consts: bool Config.T
    20   val pretty_flexpair: Proof.context -> term * term -> Pretty.T
    21   val pretty_goals: Proof.context -> thm -> Pretty.T list
    22   val pretty_goals_without_context: thm -> Pretty.T list
    23   val pretty_goal: {main: bool, limit: bool} -> Proof.context -> thm -> Pretty.T
    24 end;
    25 
    26 structure Goal_Display: GOAL_DISPLAY =
    27 struct
    28 
    29 val goals_limit_default = Unsynchronized.ref 10;
    30 val goals_limit_raw = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default));
    31 val goals_limit = Config.int goals_limit_raw;
    32 
    33 val goals_total = Config.bool (Config.declare "goals_total" (fn _ => Config.Bool true));
    34 
    35 val show_main_goal_default = Unsynchronized.ref false;
    36 val show_main_goal_raw =
    37   Config.declare "show_main_goal" (fn _ => Config.Bool (! show_main_goal_default));
    38 val show_main_goal = Config.bool show_main_goal_raw;
    39 
    40 val show_consts_default = Unsynchronized.ref false;
    41 val show_consts_raw = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default));
    42 val show_consts = Config.bool show_consts_raw;
    43 
    44 fun pretty_flexpair ctxt (t, u) = Pretty.block
    45   [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
    46 
    47 
    48 (*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
    49 
    50 local
    51 
    52 fun ins_entry (x, y) =
    53   AList.default (op =) (x, []) #>
    54   AList.map_entry (op =) x (insert (op =) y);
    55 
    56 val add_consts = Term.fold_aterms
    57   (fn Const (c, T) => ins_entry (T, (c, T))
    58     | _ => I);
    59 
    60 val add_vars = Term.fold_aterms
    61   (fn Free (x, T) => ins_entry (T, (x, ~1))
    62     | Var (xi, T) => ins_entry (T, xi)
    63     | _ => I);
    64 
    65 val add_varsT = Term.fold_atyps
    66   (fn TFree (x, S) => ins_entry (S, (x, ~1))
    67     | TVar (xi, S) => ins_entry (S, xi)
    68     | _ => I);
    69 
    70 fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
    71 fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs;
    72 
    73 fun consts_of t = sort_cnsts (add_consts t []);
    74 fun vars_of t = sort_idxs (add_vars t []);
    75 fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
    76 
    77 in
    78 
    79 fun pretty_goals ctxt0 state =
    80   let
    81     val ctxt = ctxt0
    82       |> Config.put show_free_types false
    83       |> Config.put show_types
    84        (Config.get ctxt0 show_types orelse
    85         Config.get ctxt0 show_sorts orelse
    86         Config.get ctxt0 show_all_types)
    87       |> Config.put show_sorts false;
    88 
    89     val show_sorts0 = Config.get ctxt0 show_sorts;
    90     val show_types = Config.get ctxt show_types;
    91     val show_consts = Config.get ctxt show_consts
    92     val show_main_goal = Config.get ctxt show_main_goal;
    93     val goals_limit = Config.get ctxt goals_limit;
    94     val goals_total = Config.get ctxt goals_total;
    95 
    96     val prt_sort = Syntax.pretty_sort ctxt;
    97     val prt_typ = Syntax.pretty_typ ctxt;
    98     val prt_term = Syntax.pretty_term ctxt;
    99 
   100     fun prt_atoms prt prtT (X, xs) = Pretty.block
   101       [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
   102         Pretty.brk 1, prtT X];
   103 
   104     fun prt_var (x, ~1) = prt_term (Syntax.free x)
   105       | prt_var xi = prt_term (Syntax.var xi);
   106 
   107     fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
   108       | prt_varT xi = prt_typ (TVar (xi, []));
   109 
   110     val prt_consts = prt_atoms (prt_term o Const) prt_typ;
   111     val prt_vars = prt_atoms prt_var prt_typ;
   112     val prt_varsT = prt_atoms prt_varT prt_sort;
   113 
   114 
   115     fun pretty_list _ _ [] = []
   116       | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
   117 
   118     fun pretty_subgoal (n, A) =
   119       Pretty.markup Markup.subgoal [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
   120     fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
   121 
   122     val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
   123 
   124     val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
   125     val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
   126     val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
   127 
   128 
   129     val {prop, tpairs, ...} = Thm.rep_thm state;
   130     val (As, B) = Logic.strip_horn prop;
   131     val ngoals = length As;
   132   in
   133     (if show_main_goal then [prt_term B] else []) @
   134      (if ngoals = 0 then [Pretty.str "No subgoals!"]
   135       else if ngoals > goals_limit then
   136         pretty_subgoals (take goals_limit As) @
   137         (if goals_total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
   138          else [])
   139       else pretty_subgoals As) @
   140     pretty_ffpairs tpairs @
   141     (if show_consts then pretty_consts prop else []) @
   142     (if show_types then pretty_vars prop else []) @
   143     (if show_sorts0 then pretty_varsT prop else [])
   144   end;
   145 
   146 fun pretty_goals_without_context th =
   147   let val ctxt =
   148     Config.put show_main_goal true (Syntax.init_pretty_global (Thm.theory_of_thm th))
   149   in pretty_goals ctxt th end;
   150 
   151 fun pretty_goal {main, limit} ctxt th =
   152   Pretty.chunks (pretty_goals
   153     (ctxt
   154       |> Config.put show_main_goal main
   155       |> not limit ? Config.put goals_limit (Thm.nprems_of th)
   156       |> Config.put goals_total false) th);
   157 
   158 end;
   159 
   160 end;
   161