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