1signature mlTacticData = 2sig 3 4 include Abbrev 5 6 (* datatype *) 7 type stac = string 8 type loc = string * int * int 9 type call = {stac : stac, ogl : int list, fea : mlFeature.fea} 10 val loc_compare : loc * loc -> order 11 val call_compare : call * call -> order 12 type tacdata = 13 { 14 calld : (loc,call) Redblackmap.dict, 15 taccov : (stac,int) Redblackmap.dict, 16 symfreq : (int,int) Redblackmap.dict 17 } 18 val empty_tacdata : tacdata 19 20 (* I/O *) 21 val export_calls : string -> (loc * call) list -> unit 22 val import_calls : string -> (loc * call) list 23 val import_tacdata : string list -> tacdata 24 val export_tacdata : string -> string -> tacdata -> unit 25 26 (* tactictoe database *) 27 val ttt_tacdata_dir : string 28 val exists_tacdata_thy : string -> bool 29 val create_tacdata : unit -> tacdata 30 val ttt_update_tacdata : ((loc * call) * tacdata) -> tacdata 31 val ttt_export_tacdata : string -> tacdata -> unit 32 33end 34