1(* ------------------------------------------------------------------------- *)
2(*                                                                           *)
3(*   Sanity checks for theorems stored in DB. This is intended to check for  *)
4(*   simple errors like types in quantified variable names etc.              *)
5(*                                                                           *)
6(* ------------------------------------------------------------------------- *)
7
8structure Sanity :> Sanity =
9struct
10
11open HolKernel DB Abbrev Parse boolSyntax;
12type theory = Hol_pp.theory;
13
14
15fun report_sanity_problem___plain thy thm_name warning =
16  HOL_WARNING ("Sanity Check "^thy^"Theory") thm_name
17     warning;
18
19val report_last_thm = ref "";
20fun report_sanity_problem___verbose thy thm_name warning =
21  let
22     open PPBackEnd
23     val thm_s = thy^"Theory."^thm_name;
24     val _ = if not (thm_s = (!report_last_thm)) then
25        let
26          val _ = report_last_thm := thm_s;
27          val _ = print "\n\n";
28          val _ = print_with_style [Bold] thm_s;
29          val _ = print "\n";
30          val size = UTF8.size thm_s
31          fun line 0 l = l
32            | line n l = line (n-1) ("-"^l);
33          val _ = print (line size "\n");
34        in
35          ()
36        end else ()
37
38   val _ = print "  - ";
39   val _ = print warning;
40   val _ = print "\n";
41  in
42     ()
43  end;
44
45fun init_report_sanity_problem () =
46   (report_last_thm := "");
47
48val report_verbose = ref true;
49val _ = Feedback.register_btrace ("Sanity Check Verbose", report_verbose);
50
51
52fun report_sanity_problem thy thm_name warning =
53  (if (!report_verbose) then
54      report_sanity_problem___verbose thy thm_name warning
55   else
56      report_sanity_problem___plain thy thm_name warning);
57
58
59fun map_fail c f [] = c
60  | map_fail c f (x::xs) =
61    let
62       val c' = (f x) handle Interrupt => raise Interrupt
63                           | _ => true;
64    in
65       map_fail (c orelse c') f xs
66    end
67
68
69(******************************************************************************)
70(* Check for assumptions                                                      *)
71(******************************************************************************)
72
73fun check_assumptions ((thy, name), (thm, cl)) =
74let
75  val hL = hyp thm
76in
77  if null hL then false else
78  (report_sanity_problem thy name "Theorem has assumptions";true)
79end;
80
81
82(******************************************************************************)
83(* Check for tags                                                             *)
84(******************************************************************************)
85
86val accepted_axioms = ref ([]:string list);
87val accepted_oracles = ref (["DISK_THM"]:string list);
88
89fun check_tags ((thy, name), (thm, cl)) =
90let
91  val (oL, aL) = Tag.dest_tag (tag thm);
92  val oL' = filter (fn s => not(
93      (mem s (!accepted_oracles)))) oL
94  val aL' = filter (fn s => not(
95      (mem s (!accepted_axioms)))) aL
96  val orac_s = if (null oL') then "" else
97       ("Oracles used: "^(concat (commafy oL')));
98  val axiom_s = if (null aL') then "" else
99       ("Axioms used: "^(concat (commafy aL')));
100  val s = if (null oL') then axiom_s else
101          if (null aL') then orac_s else
102          (orac_s ^ "; "^axiom_s)
103in
104  if (null oL' andalso null aL') then false else
105  ((report_sanity_problem thy name s);true)
106end;
107
108
109(******************************************************************************)
110(* Check for theorem name clashes                                             *)
111(******************************************************************************)
112
113val check_thm_name_flag = ref true;
114val _ = Feedback.register_btrace ("Sanity Check Thm-Name Clash", check_thm_name_flag);
115
116fun check_thm_name ((thy, name), (thm, cl)) =
117if (!check_thm_name_flag) then
118let
119  val dL = DB.listDB ();
120  val dL' = filter (fn ((thy',name'), _) =>
121      ((name = name') andalso (not (thy = thy')))) dL
122  val dL'' = map (fn ((s,_), _) => "'"^s^"'") dL';
123in
124  if (null dL') then false else
125  (report_sanity_problem thy name ("Name-clash with theorems in theories "^
126     (concat (commafy dL''))); true)
127end else false;
128
129
130(******************************************************************************)
131(* Check for problematic variable names                                       *)
132(******************************************************************************)
133
134fun check_var_names___no_ident ((thy, name), (thm, cl)) =
135let
136  val vL = all_varsl ((concl thm)::hyp thm)
137  val vL' = filter (fn v => not (Lexis.ok_identifier (fst (dest_var v)))) vL
138  val vnL = map  (fn v => ("'"^(fst (dest_var v))^"'")) vL'
139in
140  if (null vnL) then false else
141  ((report_sanity_problem thy name ("Dodgy variables names: "^
142     (concat (commafy vnL))));true)
143end;
144
145
146val check_var_names___const_flag = ref true;
147val _ = Feedback.register_btrace ("Sanity Check Var-Const Clash", check_var_names___const_flag);
148
149fun check_var_names___const ((thy, name), (thm, cl)) =
150if (!check_var_names___const_flag) then
151let
152  val vL = all_varsl ((concl thm)::hyp thm)
153  val vL' = filter (fn v => Parse.is_constname (fst (dest_var v))) vL
154  val vnL = map  (fn v => ("'"^(fst (dest_var v))^"'")) vL'
155in
156  if (null vnL) then false else
157  ((report_sanity_problem thy name ("Variables names clash with constants: "^
158     (concat (commafy vnL))));true)
159end else false;
160
161
162
163(******************************************************************************)
164(* Check for free top-level variables                                         *)
165(******************************************************************************)
166
167val check_free_vars_ref = ref 1;
168val _ = Feedback.register_trace ("Sanity Check Free Vars", check_free_vars_ref, 1);
169
170fun varlist_to_string vL =
171  concat (commafy (map (fn v => "'"^(ppstring pp_term v)^"'") vL))
172
173fun check_free_vars ((thy, name), (thm, cl)) =
174let
175   val do_check = if (!check_free_vars_ref = 0) then true
176                  else (if (!check_free_vars_ref = 1) then
177                     exists is_forall (strip_conj (concl thm)) else false)
178in
179if (do_check) then
180let
181  val fv = free_vars (concl thm)
182in
183  if null fv then false else
184  (report_sanity_problem thy name ("Free top_level vars " ^
185    (varlist_to_string fv) ^ "!");true)
186end else false end
187
188(******************************************************************************)
189(* Check for redundant quantors                                               *)
190(******************************************************************************)
191
192fun is_quant t =
193  is_forall t orelse
194  is_exists t orelse
195  is_exists1 t
196
197fun check_redundant_quantors ((thy, name), (thm, cl)) =
198let
199   val tL = find_terms is_quant (concl thm);
200   fun check_term t =
201      let
202        val (v, b) = dest_abs (rand t)
203      in
204        if (free_in v b) then false else
205          (report_sanity_problem thy name ("Redundant quantor: '" ^
206          (ppstring pp_term v) ^ "'!");true)
207      end;
208in
209   (map_fail false check_term tL)
210end;
211
212
213
214(******************************************************************************)
215(* A list of all checks                                                       *)
216(******************************************************************************)
217
218val sanity_checks = [
219   check_tags,
220   check_assumptions,
221   check_thm_name,
222   check_var_names___no_ident,
223   check_var_names___const,
224   check_free_vars,
225   check_redundant_quantors]:(DB.data -> bool) list
226
227fun sanity_check_data (data:DB.data) =
228   (map_fail false (fn ff => ff data) sanity_checks)
229
230fun sanity_check_theory thy =
231  (init_report_sanity_problem ();(map_fail false sanity_check_data (DB.thy thy)))
232
233fun sanity_check () = sanity_check_theory "-";
234
235fun sanity_check_all () =
236  (init_report_sanity_problem ();
237   (map_fail false sanity_check_data (DB.listDB ())))
238
239fun sanity_check_named_thm (name, thm) =
240   sanity_check_data ((Theory.current_theory(), name), (thm, DB.Thm))
241
242fun sanity_check_thm thm = sanity_check_named_thm ("-", thm);
243
244(******************************************************************************)
245(* Apply the checks when saving theorems                                      *)
246(******************************************************************************)
247
248val strict_sanity = ref true;
249val _ = Feedback.register_btrace ("Sanity Check Strict", strict_sanity);
250
251exception sanity_exn;
252fun sanity_check_exn_thm (name, thm) =
253   if (not (sanity_check_named_thm (name, thm)) orelse not (!strict_sanity)) then
254      thm
255   else
256      (print "\n\n";raise sanity_exn);
257
258fun sanity_prove (t, tac) = sanity_check_exn_thm ("-", Tactical.prove (t, tac));
259fun save_thm (name, thm) = Theory.save_thm (name, sanity_check_exn_thm (name, thm));
260fun store_thm (name, t, tac) =
261   sanity_check_exn_thm (name, Tactical.store_thm (name, t, tac));
262
263end
264