1signature tttPredict = 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 (* tfidf *) 11 val learn_tfidf : ('a * int list) list -> (int, real) Redblackmap.dict 12 13 (* term *) 14 val termknn: int -> goal -> term -> term list 15 val tmknn : int -> 16 (int, real) Redblackmap.dict * ('a * int list) list -> 17 int list -> 'a list 18 19 (* tactic *) 20 val stacknn: 21 (int, real) Redblackmap.dict -> int -> feav_t list -> fea_t -> lbl_t list 22 23 val stacknn_uniq: 24 (int, real) Redblackmap.dict -> int -> feav_t list -> fea_t -> lbl_t list 25 26 val add_stacdesc: 27 (goal, lbl_t list) Redblackmap.dict -> int -> lbl_t list -> lbl_t list 28 29 (* thm (should be sthm) *) 30 val all_thmfeav : unit -> 31 (int, real) Redblackmap.dict * 32 (string * fea_t) list * 33 (string, goal * fea_t) Redblackmap.dict 34 35 val thmknn: 36 (int, real) Redblackmap.dict * (string * fea_t) list -> int -> fea_t -> string list 37 38 val thmknn_std: int -> goal -> string list 39 40 val thmknn_wdep: 41 (int, real) Redblackmap.dict * 42 (string * fea_t) list * 43 (string, goal * fea_t) Redblackmap.dict -> 44 int -> fea_t -> string list 45 46 (* goal *) 47 val mcknn : 48 (int, real) Redblackmap.dict -> int -> ((bool * int) * int list) list -> 49 int list -> real 50 51end 52