1structure KernelSig :> KernelSig = 2struct 3 4 type kernelname = {Thy : string, Name : string} 5 fun name_compare ({Thy = thy1, Name = n1}, {Thy = thy2, Name = n2}) = 6 case String.compare (n1, n2) of 7 EQUAL => String.compare(thy1,thy2) 8 | x => x 9 10 fun name_toString {Thy,Name} = Thy ^ "$" ^ Name 11 fun name_toMLString {Thy,Name} = 12 "{Thy=\"" ^ String.toString Thy ^ "\",Name=\"" ^ String.toString Name ^ "\"}" 13 14 type kernelid = (kernelname * bool) ref (* bool is uptodate flag *) 15 16 fun name_of_id r = case !r of (n,utd) => n 17 fun uptodate_id r = case !r of (n,utd) => utd 18 fun new_id n = ref (n, true) 19 fun retire_id r = case !r of ({Thy,Name}, _) => 20 r := ({Thy = Thy, Name = Globals.old Name}, false) 21 fun name_of r = case !r of ({Name,Thy},_) => Name 22 fun seg_of r = case !r of ({Thy,Name},_) => Thy 23 fun id_toString id = name_toString (name_of_id id) 24 fun id_compare(i1, i2) = 25 case (!i1, !i2) of ((n1,_), (n2,_)) => 26 if i1 = i2 then EQUAL else name_compare(n1,n2) 27 28 29 type 'a symboltable = (kernelname, kernelid * 'a) Binarymap.dict ref 30 exception NotFound 31 32 fun new_table() = ref (Binarymap.mkDict name_compare) 33 fun find(tab,n) = Binarymap.find(!tab,n) 34 handle Binarymap.NotFound => raise NotFound 35 fun peek(tab,n) = Binarymap.peek(!tab,n) 36 fun remove(r, n) = let 37 val (tab', (id,v)) = Binarymap.remove(!r,n) 38 in 39 r := tab'; 40 SOME (id,v) 41 end handle Binarymap.NotFound => NONE 42 43 fun numItems r = Binarymap.numItems (!r) 44 45 fun app f r = Binarymap.app f (!r) 46 47 fun foldl f acc r = Binarymap.foldl f acc (!r) 48 49 fun retire_name (r, n) = 50 case remove(r, n) of 51 NONE => raise NotFound 52 | SOME (kid, v) => retire_id kid 53 54 fun insert(r,n,v) = let 55 val id = new_id n 56 in 57 retire_name(r,n) handle NotFound => (); 58 r := Binarymap.insert(!r,n,(id, v)); 59 id 60 end 61 62 63 fun uptodate_name (r, n) = let 64 val (kid, _) = find(r, n) 65 in 66 uptodate_id kid 67 end 68 69 fun listItems r = Binarymap.listItems (!r) 70 fun listThy tab thy = let 71 fun foldthis ({Thy,Name},(kid,v),acc) = 72 if Thy = thy then ({Thy = Thy,Name = Name},(kid,v)) :: acc 73 else acc 74 in 75 foldl foldthis [] tab 76 end 77 78 fun listName tab nm = let 79 fun foldthis ({Thy,Name},(kid,v),acc) = 80 if Name = nm then ({Thy = Thy,Name = Name},(kid,v)) :: acc 81 else acc 82 in 83 foldl foldthis [] tab 84 end 85 86 fun del_segment (r, thyname) = let 87 fun appthis (knm as {Name,Thy},(id,v)) = 88 if Thy = thyname then retire_name(r,knm) 89 else () 90 in 91 app appthis r 92 end 93 94 95 96 97end 98