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