1signature SharingTables =
2sig
3
4  structure Map : Binarymap
5  exception SharingTables of string
6
7  type id = {Thy : string, Other : string}
8  datatype shared_type = TYV of string
9                       | TYOP of int list
10
11  val shared_type_decode : shared_type HOLsexp.decoder
12  val shared_type_encode : shared_type HOLsexp.encoder
13
14  datatype shared_term = TMV of string * int
15                       | TMC of int * int
16                       | TMAp of int * int
17                       | TMAbs of int * int
18  val shared_term_decode : shared_term HOLsexp.decoder
19  val shared_term_encode : shared_term HOLsexp.encoder
20
21  type stringtable =
22       {size : int, map : (string,int) Map.dict, list : string list}
23  type idtable = {idsize : int,
24                  idmap : (id, int) Map.dict,
25                  idlist : (int * int) list}
26  type typetable = {tysize : int,
27                    tymap : (Type.hol_type, int)Map.dict,
28                    tylist : shared_type list}
29  type termtable = {termsize : int,
30                    termmap : (Term.term, int)Map.dict,
31                    termlist : shared_term list}
32
33  val empty_strtable : stringtable
34  val empty_idtable : idtable
35  val empty_tytable : typetable
36  val empty_termtable : termtable
37
38  val enc_strtable : stringtable HOLsexp.encoder
39  val enc_idtable  : idtable HOLsexp.encoder
40  val enc_tytable  : typetable HOLsexp.encoder
41  val enc_tmtable  : termtable HOLsexp.encoder
42
43  val dec_strings  : string Vector.vector HOLsexp.decoder
44  val dec_ids      : string Vector.vector -> id Vector.vector HOLsexp.decoder
45
46  val make_shared_type : Type.hol_type -> stringtable -> idtable -> typetable ->
47                         (int * stringtable * idtable * typetable)
48
49  val make_shared_term : Term.term ->
50                         (stringtable * idtable * typetable * termtable) ->
51                         int * (stringtable * idtable * typetable * termtable)
52
53  val build_id_vector   : string Vector.vector -> (int * int) list ->
54                          id Vector.vector
55  val build_type_vector : id Vector.vector -> shared_type list ->
56                          Type.hol_type Vector.vector
57
58  val build_term_vector : id Vector.vector -> Type.hol_type Vector.vector ->
59                          shared_term list -> Term.term Vector.vector
60
61  type sharing_data_in
62  type sharing_data_out
63  type extract_data = {named_terms : (string * Term.term) list,
64                       unnamed_terms : Term.term list,
65                       named_types : (string * Type.hol_type) list,
66                       unnamed_types : Type.hol_type list,
67                       theorems : (string * Thm.thm) list}
68  val build_sharing_data : extract_data -> sharing_data_in
69  val add_strings : string list -> sharing_data_in -> sharing_data_in
70  val add_types : Type.hol_type list -> sharing_data_in -> sharing_data_in
71  val add_terms : Term.term list -> sharing_data_in -> sharing_data_in
72  val write_string : sharing_data_in -> string -> int
73  val write_type : sharing_data_in -> Type.hol_type -> int
74  val write_term : sharing_data_in -> Term.term -> string
75  val enc_sdata : sharing_data_in HOLsexp.encoder
76
77  val dec_sdata :
78      {with_strings: (int -> string) -> unit,
79       with_stridty:
80         (int -> string) * (int -> id) * Type.hol_type Vector.vector -> unit} ->
81      sharing_data_out HOLsexp.decoder
82  val export_from_sharing_data : sharing_data_out -> extract_data
83  val read_term : sharing_data_out -> string -> Term.term
84  val read_string : sharing_data_out -> int -> string
85
86end
87
88(*
89    [export_from_sharing_data{data,with_strings,with_stridty}] will
90    return the represented data. The functions with_strings and
91    with_stridty give the caller a chance to update the state of the
92    theory context before types and then terms are constructed. This
93    is necessary in the theory-loading situation where the desired
94    values may depend on new type operators and new term constants
95    that have to be defined before the rest of the process can be
96    continued.
97*)
98