author  wenzelm 
Fri, 03 Sep 2010 11:21:58 +0200  
changeset 39050  600de0485859 
parent 33957  e9afca2118d4 
child 39115  a00da1674c1c 
permissions  rwrr 
32187  1 
(* Title: Pure/goal_display.ML 
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

3 
Author: Makarius 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

4 

568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

5 
Display tactical goal state. 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

6 
*) 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

7 

32187  8 
signature GOAL_DISPLAY = 
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

9 
sig 
32738  10 
val goals_limit: int Unsynchronized.ref 
39050
600de0485859
turned show_consts into proper configuration option;
wenzelm
parents:
33957
diff
changeset

11 
val show_consts_default: bool Unsynchronized.ref 
600de0485859
turned show_consts into proper configuration option;
wenzelm
parents:
33957
diff
changeset

12 
val show_consts_value: Config.value Config.T 
600de0485859
turned show_consts into proper configuration option;
wenzelm
parents:
33957
diff
changeset

13 
val show_consts: bool Config.T 
32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset

14 
val pretty_flexpair: Proof.context > term * term > Pretty.T 
32167
d32817dda0e6
Display_Goal.pretty_goals: always Markup.subgoal, clarified options;
wenzelm
parents:
32145
diff
changeset

15 
val pretty_goals: Proof.context > {total: bool, main: bool, maxgoals: int} > 
d32817dda0e6
Display_Goal.pretty_goals: always Markup.subgoal, clarified options;
wenzelm
parents:
32145
diff
changeset

16 
thm > Pretty.T list 
32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset

17 
val pretty_goals_without_context: int > thm > Pretty.T list 
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

18 
end; 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

19 

32187  20 
structure Goal_Display: GOAL_DISPLAY = 
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

21 
struct 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

22 

32738  23 
val goals_limit = Unsynchronized.ref 10; (*max number of goals to print*) 
39050
600de0485859
turned show_consts into proper configuration option;
wenzelm
parents:
33957
diff
changeset

24 

600de0485859
turned show_consts into proper configuration option;
wenzelm
parents:
33957
diff
changeset

25 
(*true: show consts with types in proof state output*) 
600de0485859
turned show_consts into proper configuration option;
wenzelm
parents:
33957
diff
changeset

26 
val show_consts_default = Unsynchronized.ref false; 
600de0485859
turned show_consts into proper configuration option;
wenzelm
parents:
33957
diff
changeset

27 
val show_consts_value = 
600de0485859
turned show_consts into proper configuration option;
wenzelm
parents:
33957
diff
changeset

28 
Config.declare false "show_consts" (fn _ => Config.Bool (! show_consts_default)); 
600de0485859
turned show_consts into proper configuration option;
wenzelm
parents:
33957
diff
changeset

29 
val show_consts = Config.bool show_consts_value; 
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

30 

32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset

31 
fun pretty_flexpair ctxt (t, u) = Pretty.block 
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset

32 
[Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u]; 
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

33 

568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

34 

568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

35 
(*print thm A1,...,An/B in "goal style"  premises as numbered subgoals*) 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

36 

568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

37 
local 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

38 

568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

39 
fun ins_entry (x, y) = 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

40 
AList.default (op =) (x, []) #> 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

41 
AList.map_entry (op =) x (insert (op =) y); 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

42 

568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

43 
val add_consts = Term.fold_aterms 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

44 
(fn Const (c, T) => ins_entry (T, (c, T)) 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

45 
 _ => I); 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

46 

568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

47 
val add_vars = Term.fold_aterms 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

48 
(fn Free (x, T) => ins_entry (T, (x, ~1)) 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

49 
 Var (xi, T) => ins_entry (T, xi) 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

50 
 _ => I); 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

51 

568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

52 
val add_varsT = Term.fold_atyps 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

53 
(fn TFree (x, S) => ins_entry (S, (x, ~1)) 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

54 
 TVar (xi, S) => ins_entry (S, xi) 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

55 
 _ => I); 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

56 

568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

57 
fun sort_idxs vs = map (apsnd (sort (prod_ord string_ord int_ord))) vs; 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

58 
fun sort_cnsts cs = map (apsnd (sort_wrt fst)) cs; 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

59 

568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

60 
fun consts_of t = sort_cnsts (add_consts t []); 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

61 
fun vars_of t = sort_idxs (add_vars t []); 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

62 
fun varsT_of t = rev (sort_idxs (Term.fold_types add_varsT t [])); 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

63 

568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

64 
in 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

65 

32167
d32817dda0e6
Display_Goal.pretty_goals: always Markup.subgoal, clarified options;
wenzelm
parents:
32145
diff
changeset

66 
fun pretty_goals ctxt {total, main, maxgoals} state = 
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

67 
let 
32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset

68 
val prt_sort = Syntax.pretty_sort ctxt; 
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset

69 
val prt_typ = Syntax.pretty_typ ctxt; 
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset

70 
val prt_term = Syntax.pretty_term ctxt; 
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset

71 

32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

72 
fun prt_atoms prt prtT (X, xs) = Pretty.block 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

73 
[Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::", 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

74 
Pretty.brk 1, prtT X]; 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

75 

32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset

76 
fun prt_var (x, ~1) = prt_term (Syntax.free x) 
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset

77 
 prt_var xi = prt_term (Syntax.var xi); 
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

78 

32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset

79 
fun prt_varT (x, ~1) = prt_typ (TFree (x, [])) 
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset

80 
 prt_varT xi = prt_typ (TVar (xi, [])); 
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

81 

32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset

82 
val prt_consts = prt_atoms (prt_term o Const) prt_typ; 
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset

83 
val prt_vars = prt_atoms prt_var prt_typ; 
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset

84 
val prt_varsT = prt_atoms prt_varT prt_sort; 
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

85 

568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

86 

568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

87 
fun pretty_list _ _ [] = [] 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

88 
 pretty_list name prt lst = [Pretty.big_list name (map prt lst)]; 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

89 

32167
d32817dda0e6
Display_Goal.pretty_goals: always Markup.subgoal, clarified options;
wenzelm
parents:
32145
diff
changeset

90 
fun pretty_subgoal (n, A) = Pretty.markup Markup.subgoal 
32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset

91 
[Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A]; 
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

92 
fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As); 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

93 

32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset

94 
val pretty_ffpairs = pretty_list "flexflex pairs:" (pretty_flexpair ctxt); 
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

95 

568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

96 
val pretty_consts = pretty_list "constants:" prt_consts o consts_of; 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

97 
val pretty_vars = pretty_list "variables:" prt_vars o vars_of; 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

98 
val pretty_varsT = pretty_list "type variables:" prt_varsT o varsT_of; 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

99 

568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

100 

568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

101 
val {prop, tpairs, ...} = Thm.rep_thm state; 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

102 
val (As, B) = Logic.strip_horn prop; 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

103 
val ngoals = length As; 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

104 

568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

105 
fun pretty_gs (types, sorts) = 
32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset

106 
(if main then [prt_term B] else []) @ 
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

107 
(if ngoals = 0 then [Pretty.str "No subgoals!"] 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

108 
else if ngoals > maxgoals then 
33957  109 
pretty_subgoals (take maxgoals As) @ 
32167
d32817dda0e6
Display_Goal.pretty_goals: always Markup.subgoal, clarified options;
wenzelm
parents:
32145
diff
changeset

110 
(if total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")] 
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

111 
else []) 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

112 
else pretty_subgoals As) @ 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

113 
pretty_ffpairs tpairs @ 
39050
600de0485859
turned show_consts into proper configuration option;
wenzelm
parents:
33957
diff
changeset

114 
(if Config.get ctxt show_consts then pretty_consts prop else []) @ 
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

115 
(if types then pretty_vars prop else []) @ 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

116 
(if sorts then pretty_varsT prop else []); 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

117 
in 
32966
5b21661fe618
indicate CRITICAL nature of various setmp combinators;
wenzelm
parents:
32738
diff
changeset

118 
setmp_CRITICAL show_no_free_types true 
5b21661fe618
indicate CRITICAL nature of various setmp combinators;
wenzelm
parents:
32738
diff
changeset

119 
(setmp_CRITICAL show_types (! show_types orelse ! show_sorts orelse ! show_all_types) 
5b21661fe618
indicate CRITICAL nature of various setmp combinators;
wenzelm
parents:
32738
diff
changeset

120 
(setmp_CRITICAL show_sorts false pretty_gs)) 
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

121 
(! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts) 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

122 
end; 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

123 

32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset

124 
fun pretty_goals_without_context n th = 
32167
d32817dda0e6
Display_Goal.pretty_goals: always Markup.subgoal, clarified options;
wenzelm
parents:
32145
diff
changeset

125 
pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th)) 
d32817dda0e6
Display_Goal.pretty_goals: always Markup.subgoal, clarified options;
wenzelm
parents:
32145
diff
changeset

126 
{total = true, main = true, maxgoals = n} th; 
32089
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

127 

568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

128 
end; 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

129 

568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

130 
end; 
568a23753e3a
moved pretty_goals etc. to Display_Goal (required by tracing tacticals);
wenzelm
parents:
diff
changeset

131 