1signature KernelSig = 2sig 3 4 type kernelname = {Thy : string, Name : string} 5 val name_compare : kernelname * kernelname -> order 6 val name_toString : kernelname -> string 7 val name_toMLString : kernelname -> string 8 9 eqtype kernelid 10 11 val id_compare : kernelid * kernelid -> order 12 val name_of_id : kernelid -> kernelname 13 val id_toString : kernelid -> string 14 val new_id : kernelname -> kernelid 15 val uptodate_id : kernelid -> bool 16 val retire_id : kernelid -> unit 17 val name_of : kernelid -> string 18 val seg_of : kernelid -> string 19 20 type 'a symboltable 21 exception NotFound 22 val new_table : unit -> 'a symboltable 23 val insert : 'a symboltable * kernelname * 'a -> kernelid 24 val find : 'a symboltable * kernelname -> kernelid * 'a 25 val peek : 'a symboltable * kernelname -> (kernelid * 'a) option 26 27 val numItems : 'a symboltable -> int 28 val listItems : 'a symboltable -> (kernelname * (kernelid * 'a)) list 29 val listThy : 'a symboltable -> string -> (kernelname * (kernelid * 'a)) list 30 val listName : 'a symboltable -> string -> (kernelname * (kernelid * 'a)) list 31 32 val app : (kernelname * (kernelid * 'a) -> unit) -> 'a symboltable -> unit 33 val foldl : (kernelname * (kernelid * 'a) * 'b -> 'b) -> 'b -> 34 'a symboltable -> 'b 35 val retire_name : 'a symboltable * kernelname -> unit 36 val uptodate_name : 'a symboltable * kernelname -> bool 37 val del_segment : 'a symboltable * string -> unit 38 39end 40