# HG changeset patch
# User paulson
# Date 1134730284 -3600
# Node ID 30f4b1eda7cd593945849d9c0b8bf5403d00d2b1
# Parent  bf448d999b7e5a02501057250d60a383ef4ad64d
hash tables from SML/NJ

diff -r bf448d999b7e -r 30f4b1eda7cd src/Pure/General/hashtable.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/hashtable.ML	Fri Dec 16 11:51:24 2005 +0100
@@ -0,0 +1,133 @@
+(*Hash tables. Taken from SML/NJ version 110.57.
+  Copyright (c) 1989-2002 by Lucent Technologies*)
+signature HASHTABLE =
+sig
+   type ('a,'b) table
+
+   val create : { hash : 'a -> word, 
+                  ==   : 'a * 'a -> bool,
+                  exn  : exn,
+                  size : int 
+                } -> ('a,'b) table 
+
+   val size         : ('a,'b) table -> int
+   val clear        : ('a,'b) table -> unit
+   val insert       : ('a,'b) table -> 'a * 'b -> unit
+   val remove       : ('a,'b) table -> 'a -> unit
+   val lookup       : ('a,'b) table -> 'a -> 'b 
+   val copy         : ('a,'b) table -> ('a,'b) table
+   val app          : ('a * 'b -> unit) -> ('a,'b) table -> unit
+   val map          : ('a * 'b -> 'c) -> ('a,'b) table -> 'c list
+   val fold         : ('a * 'b * 'c -> 'c) -> 'c -> ('a,'b) table -> 'c
+
+   (*Additions due to L. C. Paulson and Jia Meng*)
+   val hash_word : word * word -> word
+   val hash_char : Char.char * word -> word
+   val hash_vector : word Vector.vector * word -> word
+   val hash_string : string * word -> word
+   val hash_strings : string list * word -> word
+end
+
+structure Hashtable :> HASHTABLE =
+struct
+
+   structure A = Array
+
+   type ('a,'b) table = ('a -> word) * 
+                        ('a * 'a -> bool) *
+                        exn *
+                        ('a * 'b) list A.array ref * 
+                        int ref
+
+   infix ==
+
+   fun create{hash,==,exn,size} = (hash,op==,exn,ref(A.array(size,[])),ref 0)
+   fun copy(hash,op==,exn,ref a,ref c) = 
+         (hash,op==,exn,ref(A.tabulate(A.length a,fn i => A.sub(a,i))), ref c)
+   fun size (_,_,_,_,ref n) = n
+   fun clear (_,_,_,ref a,c) =
+       let fun f ~1 = ()
+             | f i  = (A.update(a,i,[]); f(i-1))
+       in  f(A.length a - 1); c := 0 end
+   fun insert (hash,op==,exn,A as ref a,c) (k,v) =
+   let val N  = A.length a
+       val h  = Word.toIntX(hash k) mod N
+       val es = A.sub(a,h)
+       fun insrt ([],es') = (A.update(a,h,(k,v)::es'); 
+			     c := !c + 1;
+			     if !c >= N then grow(hash,A,N) else ())
+         | insrt ((e as (k',_))::es,es') = 
+            if k == k' then A.update(a,h,(k,v)::es'@es) 
+            else insrt(es,e::es')
+   in  insrt (es,[])
+   end
+
+   and grow(hash,A as ref a,N) =
+       let val M = N + N
+           val M = if M < 13 then 13 else M
+           val a' = A.array(M,[])
+           fun insrt (k,v) = let val h = Word.toIntX(hash k) mod M
+                             in  A.update(a',h,(k,v)::A.sub(a',h)) end
+       in  A.app (fn es => app insrt es) a;
+           A := a'
+       end
+
+   fun remove (hash,op==,exn,ref a,c) k =
+   let val N  = A.length a
+       val h  = Word.toIntX(hash k) mod N
+       val es = A.sub(a,h)
+       fun del ([],es') = ()
+         | del ((e as (k',_))::es,es') = 
+            if k == k' then (A.update(a,h,es'@es); c := !c - 1)
+            else del(es,e::es')
+   in  del (es,[])
+   end
+ 
+   fun lookup(hash,op==,exn,ref a,_) k =
+   let val N  = A.length a
+       val h  = Word.toIntX(hash k) mod N
+       fun find [] = raise exn
+         | find ((k',v)::es) = if k == k' then v else find es
+   in  find(A.sub(a,h))
+   end
+
+   fun app f (_,_,_,ref A,_) = A.app (List.app f) A
+
+   fun map f (_,_,_,ref A,_) =
+   let fun fl([],x) = x
+         | fl((k,v)::es,x) = f(k,v)::fl(es,x)
+   in  A.foldr fl [] A end
+
+   fun fold f x (_,_,_,ref A,_) = 
+   let fun fl([],x) = x
+         | fl((k,v)::es,x) = f(k,v,fl(es,x))
+   in  A.foldr fl x A end
+
+
+   (*Additions due to L. C. Paulson and Jia Meng*)
+
+   val myw = ref 0w0;
+   val () = myw := 0wx70000000;  (*workaround for Poly/ML bug*)
+
+   local open Word
+	 infix << >>
+   in
+   fun hash_word (u,w) =
+     let val w' = (w << 0w4) + u
+	 val g = Word.andb(w', !myw)    (*I hope this hex constant is correct!*)
+     in  
+	 if g = 0w0 then Word.xorb(w', Word.xorb(g, g >> 0w24))
+	 else w'
+     end;
+   end;
+   
+   fun hash_char (c,w) = hash_word (Word.fromInt (Char.ord c), w);
+   
+   fun hash_vector (v,w) = Vector.foldl hash_word w v;
+   
+   fun hash_string (s:string, w) = CharVector.foldl hash_char w s;
+   
+   fun hash_strings (ss, w) = List.foldl hash_string w ss;
+
+end
+