75 val maximals = flat (find_max_subsets multiples) |
75 val maximals = flat (find_max_subsets multiples) |
76 in |
76 in |
77 (s, SOME maximals) |
77 (s, SOME maximals) |
78 end) |
78 end) |
79 in |
79 in |
80 rev (map check all_thms) |
80 rev (Par_List.map check all_thms) |
81 end |
81 end |
82 |
82 |
83 |
83 |
84 (* printing results *) |
84 (* printing results *) |
85 |
85 |
86 local |
86 local |
87 |
87 |
88 fun pretty_indexes is = |
88 fun pretty_indexes is = |
89 Pretty.block (separate (Pretty.str " and ") |
89 Pretty.block |
90 (map (fn i => Pretty.str (string_of_int (i + 1))) (sort int_ord is)) |
90 (flat (separate [Pretty.str " and", Pretty.brk 1] |
91 @ [Pretty.brk 1]) |
91 (map (fn i => [Pretty.str (string_of_int (i + 1))]) (sort int_ord is)))) |
92 |
92 |
93 fun pretty_thm (s, set_of_indexes) = |
93 fun pretty_thm (s, set_of_indexes) = |
94 Pretty.block (Pretty.str s :: Pretty.str ":" :: Pretty.brk 1 :: |
94 Pretty.block (Pretty.str s :: Pretty.str ":" :: Pretty.brk 1 :: |
95 Pretty.str "unnecessary assumption(s) " :: |
95 Pretty.str "unnecessary assumption(s) " :: |
96 separate (Pretty.str ", or ") (map pretty_indexes set_of_indexes)) |
96 separate (Pretty.str " or ") (map pretty_indexes set_of_indexes)) |
97 |
97 |
98 in |
98 in |
99 |
99 |
100 fun print_unused_assms ctxt opt_thy_name = |
100 fun print_unused_assms ctxt opt_thy_name = |
101 let |
101 let |
104 val total = length results |
104 val total = length results |
105 val with_assumptions = length (filter (is_some o snd) results) |
105 val with_assumptions = length (filter (is_some o snd) results) |
106 val with_superfluous_assumptions = |
106 val with_superfluous_assumptions = |
107 map_filter (fn (_, NONE) => NONE | (_, SOME []) => NONE | (s, SOME r) => SOME (s, r)) results |
107 map_filter (fn (_, NONE) => NONE | (_, SOME []) => NONE | (s, SOME r) => SOME (s, r)) results |
108 |
108 |
109 val msg = "Found " ^ string_of_int (length with_superfluous_assumptions) |
109 val msg = |
110 ^ " theorem(s) with (potentially) superfluous assumptions" |
110 "Found " ^ string_of_int (length with_superfluous_assumptions) ^ |
111 val end_msg = "Checked " ^ string_of_int with_assumptions ^ " theorem(s) with assumptions" |
111 " theorems with (potentially) superfluous assumptions" |
112 ^ " in the theory " ^ quote thy_name |
112 val end_msg = |
113 ^ " with a total of " ^ string_of_int total ^ " theorem(s)" |
113 "Checked " ^ string_of_int with_assumptions ^ " theorems with assumptions (" ^ |
|
114 string_of_int total ^ " total) in the theory " ^ quote thy_name |
114 in |
115 in |
115 [Pretty.str (msg ^ ":"), Pretty.str ""] @ |
116 [Pretty.str (msg ^ ":"), Pretty.str ""] @ |
116 map pretty_thm with_superfluous_assumptions @ |
117 map pretty_thm with_superfluous_assumptions @ |
117 [Pretty.str "", Pretty.str end_msg] |
118 [Pretty.str "", Pretty.str end_msg] |
118 end |> Pretty.chunks |> Pretty.writeln |
119 end |> Pretty.chunks |> Pretty.writeln |
119 |
120 |
120 end |
121 end |
121 |
122 |
122 val _ = |
123 val _ = |
123 Outer_Syntax.improper_command @{command_spec "find_unused_assms"} |
124 Outer_Syntax.improper_command @{command_spec "find_unused_assms"} |
124 "find theorems with superfluous assumptions" |
125 "find theorems with (potentially) superfluous assumptions" |
125 (Scan.option Parse.name |
126 (Scan.option Parse.name |
126 >> (fn opt_thy_name => |
127 >> (fn opt_thy_name => |
127 Toplevel.no_timing o Toplevel.keep (fn state => |
128 Toplevel.no_timing o Toplevel.keep (fn state => |
128 print_unused_assms (Toplevel.context_of state) opt_thy_name))) |
129 print_unused_assms (Toplevel.context_of state) opt_thy_name))) |
129 |
130 |