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