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