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