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