1signature SharingTables =
2sig
3
4  structure Map : Binarymap
5  type id = {Thy : string, Other : string}
6  datatype shared_type = TYV of string
7                       | TYOP of int list
8  datatype shared_term = TMV of string * int
9                       | TMC of int * int
10                       | TMAp of int * int
11                       | TMAbs of int * int
12
13  type idtable = {idsize : int,
14                  idmap : (id, int) Map.dict,
15                  idlist : id list}
16  type typetable = {tysize : int,
17                    tymap : (Type.hol_type, int)Map.dict,
18                    tylist : shared_type list}
19  type termtable = {termsize : int,
20                    termmap : (Term.term, int)Map.dict,
21                    termlist : shared_term list}
22
23  val empty_idtable : idtable
24  val empty_tytable : typetable
25  val empty_termtable : termtable
26
27  val make_shared_type : Type.hol_type -> idtable -> typetable ->
28                         (int * idtable * typetable)
29
30  val make_shared_term : Term.term -> (idtable * typetable * termtable) ->
31                         int * (idtable * typetable * termtable)
32
33  val output_idtable : string -> idtable -> HOLPP.pretty
34  val theoryout_idtable    : idtable PP.pprinter
35
36  val build_type_vector : id Vector.vector -> shared_type list ->
37                          Type.hol_type Vector.vector
38
39  val output_typetable : {idtable_nm : string, tytable_nm : string} ->
40                         typetable -> PP.pretty
41  val theoryout_typetable    : typetable PP.pprinter
42
43  val build_term_vector : id Vector.vector -> Type.hol_type Vector.vector ->
44                          shared_term list -> Term.term Vector.vector
45
46  val output_termtable : {idtable_nm : string, tytable_nm : string,
47                          termtable_nm : string} ->
48                         termtable -> PP.pretty
49
50  val theoryout_termtable    : termtable PP.pprinter
51
52end
53