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