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