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