1signature mlNearestNeighbor =
2sig
3
4  include Abbrev
5
6  type fea = mlFeature.fea
7  type thmid = mlThmData.thmid
8  type stac = mlTacticData.stac
9  type loc = mlTacticData.loc
10  type call = mlTacticData.call
11
12  type symweight = mlFeature.symweight
13  type 'a afea = ('a * fea) list
14
15  val inter_time : real ref
16  val dfind_time : real ref
17  val sum_time : real ref
18
19  (* nearest neighbor predictors *)
20  val termknn: symweight * term afea -> int -> fea -> term list
21  val thmknn:  symweight * thmid afea -> int -> fea -> thmid list
22  val thmknn_wdep: symweight * thmid afea -> int -> fea -> thmid list
23  val tacknn: symweight * stac afea -> int -> fea -> stac list
24  val callknn: symweight * (loc * call) afea -> int -> fea -> (loc * call) list
25  val add_calldep: (loc,call) Redblackmap.dict -> int ->
26    (loc * call) list -> (loc * call) list
27
28  (* for comparison with tree neural networks *)
29  type 'a knnpred = (symweight * term afea) * (term, 'a) Redblackmap.dict
30  val train_knn: (term * 'a) list -> 'a knnpred
31  val infer_knn : 'a knnpred -> term -> 'a
32  val knn_accuracy: (real list) knnpred -> (term * real list) list -> real
33
34end
35