1(* ===================================================================== *) 2(* FILE : holyHammer.sml *) 3(* DESCRIPTION : Premise selection and external provers *) 4(* AUTHOR : (c) Thibault Gauthier, University of Innsbruck *) 5(* DATE : 2015 *) 6(* ===================================================================== *) 7 8structure holyHammer :> holyHammer = 9struct 10 11open HolKernel boolLib Thread aiLib smlExecute smlRedirect smlParallel 12 mlFeature mlThmData mlTacticData mlNearestNeighbor 13 hhExportFof hhReconstruct hhTranslate hhTptp 14 15val ERR = mk_HOL_ERR "holyHammer" 16 17(* ------------------------------------------------------------------------- 18 Settings 19 ------------------------------------------------------------------------- *) 20 21val timeout_glob = ref 10 22fun set_timeout n = timeout_glob := n 23 24val dep_flag = ref false 25 26(* ------------------------------------------------------------------------- 27 ATPs 28 ------------------------------------------------------------------------- *) 29 30datatype prover = Eprover | Z3 | Vampire 31fun name_of atp = case atp of 32 Eprover => "eprover" 33 | Z3 => "z3" 34 | Vampire => "vampire" 35 36fun npremises_of atp = 37 if !dep_flag then 100000 else 38 case atp of 39 Eprover => 128 40 | Z3 => 32 41 | Vampire => 96 42 43(* ATPs called by holyhammer if their binary exists *) 44val all_atps = ref [Eprover,Z3,Vampire] 45 46(* ------------------------------------------------------------------------- 47 Directories 48 ------------------------------------------------------------------------- *) 49 50val parallel_tag = ref "" 51 52fun pathl sl = case sl of 53 [] => raise ERR "pathl" "empty" 54 | [a] => a 55 | a :: m => OS.Path.concat (a, pathl m) 56 57val hh_dir = pathl [HOLDIR,"src","holyhammer"]; 58val provbin_dir = pathl [hh_dir,"provers"]; 59fun provdir_of atp = pathl [provbin_dir, 60 name_of atp ^ "_files" ^ (!parallel_tag)] 61fun out_of atp = pathl [provdir_of atp,"out"] 62fun status_of atp = pathl [provdir_of atp,"status"] 63 64(* ------------------------------------------------------------------------- 65 Evaluation log 66 ------------------------------------------------------------------------- *) 67 68val hh_eval_dir = pathl [hh_dir,"eval"]; 69val eval_flag = ref false 70val eval_thy = ref "scratch" 71fun log_eval s = 72 if !eval_flag then 73 let val file = hh_eval_dir ^ "/" ^ (!eval_thy) in 74 mkDir_err hh_eval_dir; 75 append_endline file s 76 end 77 else () 78 79(* ------------------------------------------------------------------------- 80 Run functions in parallel and terminate as soon as one returned a 81 positive result in parallel_result. 82 ------------------------------------------------------------------------- *) 83 84val (parallel_result : string list option ref) = ref NONE 85 86val attrib = [Thread.InterruptState Thread.InterruptAsynch, Thread.EnableBroadcastInterrupt true] 87 88fun parallel_call t fl = 89 let 90 val _ = parallel_result := NONE 91 fun rec_fork f = Thread.fork (fn () => f (), attrib) 92 val threadl = map rec_fork fl 93 val rt = Timer.startRealTimer () 94 fun loop () = 95 ( 96 OS.Process.sleep (Time.fromReal 0.01); 97 if isSome (!parallel_result) orelse 98 not (exists Thread.isActive threadl) orelse 99 Timer.checkRealTimer rt > Time.fromReal t 100 then (app interruptkill threadl; !parallel_result) 101 else loop () 102 ) 103 in 104 loop () 105 end 106 107(* ------------------------------------------------------------------------- 108 Launch an ATP 109 ------------------------------------------------------------------------- *) 110 111val atp_ref = ref "" 112 113fun launch_atp dir atp t = 114 let 115 val cmd = "sh " ^ name_of atp ^ ".sh " ^ int_to_string t ^ " " ^ 116 dir ^ " > /dev/null 2> /dev/null" 117 val _ = cmd_in_dir provbin_dir cmd 118 val r = get_lemmas (status_of atp, out_of atp) 119 in 120 if isSome r 121 then 122 ( 123 atp_ref := name_of atp; 124 print_endline ("proof found by " ^ name_of atp ^ ":"); 125 print_endline (" " ^ mk_metis_call (valOf r)); 126 log_eval (" proof found by " ^ name_of atp ^ ":"); 127 log_eval (" " ^ mk_metis_call (valOf r)); 128 parallel_result := r 129 ) 130 else (); 131 r 132 end 133 134(* ------------------------------------------------------------------------- 135 HolyHammer 136 ------------------------------------------------------------------------- *) 137 138fun export_to_atp premises cj atp = 139 let 140 val new_premises = first_n (npremises_of atp) premises 141 val namethml = hidef thml_of_namel new_premises 142 in 143 fof_export_pb (provdir_of atp) (cj,namethml) 144 end 145 146fun exists_atp atp = 147 exists_file (pathl [provbin_dir, name_of atp]) 148 149fun exists_atp_err atp = 150 let val b = exists_file (pathl [provbin_dir, name_of atp]) in 151 if not b then print_endline ("no binary for " ^ name_of atp) else (); 152 b 153 end 154 155fun hh_pb wanted_atpl premises goal = 156 let 157 val _ = app (mkDir_err o provdir_of) wanted_atpl 158 val atpl = filter exists_atp_err wanted_atpl 159 val cj = list_mk_imp goal 160 val _ = app (export_to_atp premises cj) atpl 161 val t1 = !timeout_glob 162 val t2 = Real.fromInt t1 + 2.0 163 fun f x = fn () => ignore (launch_atp (provdir_of x) x t1) 164 val olemmas = parallel_call t2 (map f atpl) 165 in 166 case olemmas of 167 NONE => 168 (log_eval " ATPs could not find a proof"; 169 raise ERR "hh_pb" "ATPs could not find a proof") 170 | SOME lemmas => 171 let 172 val (stac,tac) = hidef (hh_reconstruct lemmas) goal 173 in 174 print_endline ("minimized proof: \n " ^ stac); 175 log_eval (" minimized proof: \n " ^ stac); 176 tac 177 end 178 end 179 180fun main_hh thmdata goal = 181 let 182 val atpl = filter exists_atp (!all_atps) 183 val _ = 184 if null atpl 185 then raise ERR "main_hh" "no ATP binary: see src/holyhammer/README" 186 else () 187 val n = list_imax (map npremises_of atpl) 188 val premises = thmknn_wdep thmdata n (fea_of_goal true goal) 189 in 190 hh_pb atpl premises goal 191 end 192 193fun has_boolty x = type_of x = bool 194fun has_boolty_goal goal = all has_boolty (snd goal :: fst goal) 195 196fun hh_goal goal = 197 if not (has_boolty_goal goal) 198 then raise ERR "hh_goal" "a term is not of type bool" 199 else 200 let val thmdata = hidef create_thmdata () in 201 main_hh thmdata goal 202 end 203 204fun hh_fork goal = Thread.fork (fn () => ignore (hh_goal goal), attrib) 205fun hh goal = let val tac = hh_goal goal in hidef tac goal end 206fun holyhammer tm = hidef TAC_PROOF (([],tm), hh_goal ([],tm)); 207 208(* ------------------------------------------------------------------------- 209 HolyHammer evaluation without premise selection: 210 trying to re-prove theorems from their dependencies 211 ------------------------------------------------------------------------- *) 212 213fun hh_pb_eval_thm atpl (s,thm) = 214 let 215 val _ = print_endline ("\nTheorem: " ^ s) 216 val _ = log_eval ("\nTheorem: " ^ s) 217 val goal = dest_thm thm 218 val (b,premises) = intactdep_of_thm thm 219 val _ = log_eval (" dependencies:\n " ^ 220 (String.concatWith "\n " premises)) 221 in 222 if not b then (print_endline " broken_dependencies (not tested)"; 223 log_eval " broken dependencies (not tested)") 224 else 225 let val (_,t) = add_time (can (hh_pb atpl premises)) goal in 226 log_eval (" time: " ^ Real.toString t) 227 end 228 end 229 230fun hh_pb_eval_thy atpl thy = 231 ( 232 dep_flag := true; eval_flag := true; eval_thy := thy; 233 mkDir_err hh_eval_dir; 234 remove_file (hh_eval_dir ^ "/" ^ thy); 235 app (hh_pb_eval_thm atpl) (DB.theorems thy); 236 dep_flag := false; eval_flag := false; eval_thy := "scratch" 237 ) 238 239(* ------------------------------------------------------------------------- 240 Function called by the tactictoe evaluation framework 241 ------------------------------------------------------------------------- *) 242 243fun hh_eval (thmdata,tacdata) goal = 244 let val b = !hide_flag in 245 hide_flag := false; eval_flag := true; 246 eval_thy := current_theory (); 247 mkDir_err hh_eval_dir; 248 log_eval ("Goal: " ^ string_of_goal goal); 249 ignore (main_hh thmdata goal); 250 eval_flag := false; hide_flag := b; 251 eval_thy := "scratch" 252 end 253 254 255end (* struct *) 256