src/Pure/goal_display.ML
author wenzelm
Tue Sep 26 20:54:40 2017 +0200 (22 months ago)
changeset 66695 91500c024c7f
parent 64556 851ae0e7b09c
child 69575 f77cc54f6d47
permissions -rw-r--r--
tuned;
     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_raw: Config.raw
    11   val goals_limit: int Config.T
    12   val show_main_goal_raw: Config.raw
    13   val show_main_goal: bool Config.T
    14   val pretty_goals: Proof.context -> thm -> Pretty.T list
    15   val pretty_goal: Proof.context -> thm -> Pretty.T
    16   val string_of_goal: Proof.context -> thm -> string
    17 end;
    18 
    19 structure Goal_Display: GOAL_DISPLAY =
    20 struct
    21 
    22 val goals_limit_raw = Config.declare_option ("goals_limit", \<^here>);
    23 val goals_limit = Config.int goals_limit_raw;
    24 
    25 val show_main_goal_raw = Config.declare_option ("show_main_goal", \<^here>);
    26 val show_main_goal = Config.bool show_main_goal_raw;
    27 
    28 
    29 (*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*)
    30 
    31 local
    32 
    33 fun ins_entry (x, y) =
    34   AList.default (op =) (x, []) #>
    35   AList.map_entry (op =) x (insert (op =) y);
    36 
    37 val add_consts = Term.fold_aterms
    38   (fn Const (c, T) => ins_entry (T, (c, T))
    39     | _ => I);
    40 
    41 val add_vars = Term.fold_aterms
    42   (fn Free (x, T) => ins_entry (T, (x, ~1))
    43     | Var (xi, T) => ins_entry (T, xi)
    44     | _ => I);
    45 
    46 val add_varsT = Term.fold_atyps
    47   (fn TFree (x, S) => ins_entry (S, (x, ~1))
    48     | TVar (xi, S) => ins_entry (S, xi)
    49     | _ => I);
    50 
    51 fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs;
    52 fun sort_cnsts cs = map (apsnd (sort_by fst)) cs;
    53 
    54 fun consts_of t = sort_cnsts (add_consts t []);
    55 fun vars_of t = sort_idxs (add_vars t []);
    56 fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t []));
    57 
    58 in
    59 
    60 fun pretty_goals ctxt0 state =
    61   let
    62     val ctxt = ctxt0
    63       |> Config.put show_types (Config.get ctxt0 show_types orelse Config.get ctxt0 show_sorts)
    64       |> Config.put show_sorts false;
    65 
    66     val show_sorts0 = Config.get ctxt0 show_sorts;
    67     val show_types = Config.get ctxt show_types;
    68     val show_consts = Config.get ctxt show_consts
    69     val show_main_goal = Config.get ctxt show_main_goal;
    70     val goals_limit = Config.get ctxt goals_limit;
    71 
    72     val prt_sort = Syntax.pretty_sort ctxt;
    73     val prt_typ = Syntax.pretty_typ ctxt;
    74     val prt_term =
    75       singleton (Syntax.uncheck_terms ctxt) #>
    76       Type_Annotation.ignore_free_types #>
    77       Syntax.unparse_term ctxt;
    78 
    79     fun prt_atoms prt prtT (X, xs) = Pretty.block
    80       [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
    81         Pretty.brk 1, prtT X];
    82 
    83     fun prt_var (x, ~1) = prt_term (Syntax.free x)
    84       | prt_var xi = prt_term (Syntax.var xi);
    85 
    86     fun prt_varT (x, ~1) = prt_typ (TFree (x, []))
    87       | prt_varT xi = prt_typ (TVar (xi, []));
    88 
    89     val prt_consts = prt_atoms (prt_term o Const) prt_typ;
    90     val prt_vars = prt_atoms prt_var prt_typ;
    91     val prt_varsT = prt_atoms prt_varT prt_sort;
    92 
    93 
    94     fun pretty_list _ _ [] = []
    95       | pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
    96 
    97     fun pretty_subgoal s A =
    98       Pretty.markup (Markup.subgoal s) [Pretty.str (" " ^ s ^ ". "), prt_term A];
    99     val pretty_subgoals = map_index (fn (i, A) => pretty_subgoal (string_of_int (i + 1)) A);
   100 
   101     val pretty_ffpairs = pretty_list "flex-flex pairs:" (Thm.pretty_flexpair ctxt);
   102 
   103     val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
   104     val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
   105     val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of;
   106 
   107 
   108     val prop = Thm.prop_of state;
   109     val (As, B) = Logic.strip_horn prop;
   110     val ngoals = length As;
   111   in
   112     (if show_main_goal then [Pretty.mark Markup.goal (prt_term B)] else []) @
   113      (if ngoals = 0 then [Pretty.str "No subgoals!"]
   114       else if ngoals > goals_limit then
   115         pretty_subgoals (take goals_limit As) @
   116         [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
   117       else pretty_subgoals As) @
   118     pretty_ffpairs (Thm.tpairs_of state) @
   119     (if show_consts then pretty_consts prop else []) @
   120     (if show_types then pretty_vars prop else []) @
   121     (if show_sorts0 then pretty_varsT prop else [])
   122   end;
   123 
   124 val pretty_goal = Pretty.chunks oo pretty_goals;
   125 val string_of_goal = Pretty.string_of oo pretty_goal;
   126 
   127 end;
   128 
   129 end;
   130