1signature tttSearch =
2sig
3
4  include Abbrev
5
6  type lbl_t = (string * real * goal * goal list)
7  type fea_t = int list
8  type feav_t = (lbl_t * fea_t)
9
10  val last_stac : string ref (* for debugging purpose *)
11
12  val add_metis : string list -> string list
13  val stac_to_tac :
14    (int -> goal -> string list) ->
15    (string, tactic) Redblackmap.dict ref *
16    (string * goal, string * tactic * real) Redblackmap.dict ref *
17    (goal * int, string list) Redblackmap.dict ref ->
18    string -> goal ->
19    string * tactic * real
20
21
22  datatype proof_status_t =
23    ProofError | ProofSaturated | ProofTimeOut | Proof of string
24
25  val search :
26    (int -> goal -> string list) ->
27    (goal -> string list) ->
28    (goal list -> real) ->
29    (int -> goal -> string option) ->
30    goal -> proof_status_t
31
32end
33