1signature holyHammer =
2sig
3
4  include Abbrev
5  datatype prover = Eprover | Z3 | Vampire
6
7  type lbl_t = (string * real * goal * goal list)
8  type fea_t = int list
9  type feav_t = (lbl_t * fea_t)
10
11  (* Directories *)
12  val hh_dir : string
13  val hh_eval_dir : string
14
15  (* Settings *)
16  val set_timeout        : int -> unit
17  val all_atps           : prover list ref
18    (* atps called by holyhammer if their binary exists *)
19
20  (* Read theorems from their string representataion *)
21  val thml_of_namel : string list -> (string * thm) list
22
23  (* Caching features of goals *)
24  val clean_goalfea_cache : unit -> unit
25
26  (* Updating the database of theorems *)
27  val update_thmdata : unit ->
28    (int, real) Redblackmap.dict *
29    (string * fea_t) list *
30    (string, (goal * int list)) Redblackmap.dict
31
32  (* Calling an automated theorem prover such as "eprover" *)
33  val launch_atp        : string -> prover -> int -> string list option
34
35  (* Reconstruct and minimize the proof using Metis *)
36  val hh_reconstruct    : string list -> goal -> (string * tactic)
37
38  (* Main functions *)
39  val hh_pb             : prover list -> string list -> goal -> tactic
40  val clean_goaltac_cache : unit -> unit
41    (* saving results of the next functions in goaltac_cache *)
42  val hh_goal           : goal -> tactic
43  val hh_fork           : goal -> Thread.thread
44  val holyhammer        : term -> tactic
45  val hh                : tactic
46
47  (* Other functions *)
48  val metis_auto        : real -> int -> goal -> string option
49
50  (* For tttSyntEval.sml *)
51  val export_pb :
52    string -> int -> term list * term ->
53    int * (term * (string, term) Redblackmap.dict)
54  val eprover_parallel:
55    string -> int -> int list -> int ->
56    (int * string list option) list
57
58
59
60  (* HolyHammer for TacTicToe parallel calls *)
61  val hh_stac           :
62    string ->
63      (int, real) Redblackmap.dict *
64      (string * fea_t) list *
65      (string, (goal * int list)) Redblackmap.dict
66    -> int -> goal -> string option
67
68  (* Evaluation *)
69  val hh_eval_thm : prover list -> bool -> (string * thm) -> unit
70  val hh_eval_thy : prover list -> bool -> string -> unit
71
72  (* Export HOL4 library to Holyhammer infrastructure in HOL/Light *)
73  val export_problem  : string -> string list -> term -> unit
74  val export_theories : string -> string list -> unit
75
76end
77