src/Pure/General/hashtable.ML
changeset 18419 30f4b1eda7cd
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/hashtable.ML	Fri Dec 16 11:51:24 2005 +0100
     1.3 @@ -0,0 +1,133 @@
     1.4 +(*Hash tables. Taken from SML/NJ version 110.57.
     1.5 +  Copyright (c) 1989-2002 by Lucent Technologies*)
     1.6 +signature HASHTABLE =
     1.7 +sig
     1.8 +   type ('a,'b) table
     1.9 +
    1.10 +   val create : { hash : 'a -> word, 
    1.11 +                  ==   : 'a * 'a -> bool,
    1.12 +                  exn  : exn,
    1.13 +                  size : int 
    1.14 +                } -> ('a,'b) table 
    1.15 +
    1.16 +   val size         : ('a,'b) table -> int
    1.17 +   val clear        : ('a,'b) table -> unit
    1.18 +   val insert       : ('a,'b) table -> 'a * 'b -> unit
    1.19 +   val remove       : ('a,'b) table -> 'a -> unit
    1.20 +   val lookup       : ('a,'b) table -> 'a -> 'b 
    1.21 +   val copy         : ('a,'b) table -> ('a,'b) table
    1.22 +   val app          : ('a * 'b -> unit) -> ('a,'b) table -> unit
    1.23 +   val map          : ('a * 'b -> 'c) -> ('a,'b) table -> 'c list
    1.24 +   val fold         : ('a * 'b * 'c -> 'c) -> 'c -> ('a,'b) table -> 'c
    1.25 +
    1.26 +   (*Additions due to L. C. Paulson and Jia Meng*)
    1.27 +   val hash_word : word * word -> word
    1.28 +   val hash_char : Char.char * word -> word
    1.29 +   val hash_vector : word Vector.vector * word -> word
    1.30 +   val hash_string : string * word -> word
    1.31 +   val hash_strings : string list * word -> word
    1.32 +end
    1.33 +
    1.34 +structure Hashtable :> HASHTABLE =
    1.35 +struct
    1.36 +
    1.37 +   structure A = Array
    1.38 +
    1.39 +   type ('a,'b) table = ('a -> word) * 
    1.40 +                        ('a * 'a -> bool) *
    1.41 +                        exn *
    1.42 +                        ('a * 'b) list A.array ref * 
    1.43 +                        int ref
    1.44 +
    1.45 +   infix ==
    1.46 +
    1.47 +   fun create{hash,==,exn,size} = (hash,op==,exn,ref(A.array(size,[])),ref 0)
    1.48 +   fun copy(hash,op==,exn,ref a,ref c) = 
    1.49 +         (hash,op==,exn,ref(A.tabulate(A.length a,fn i => A.sub(a,i))), ref c)
    1.50 +   fun size (_,_,_,_,ref n) = n
    1.51 +   fun clear (_,_,_,ref a,c) =
    1.52 +       let fun f ~1 = ()
    1.53 +             | f i  = (A.update(a,i,[]); f(i-1))
    1.54 +       in  f(A.length a - 1); c := 0 end
    1.55 +   fun insert (hash,op==,exn,A as ref a,c) (k,v) =
    1.56 +   let val N  = A.length a
    1.57 +       val h  = Word.toIntX(hash k) mod N
    1.58 +       val es = A.sub(a,h)
    1.59 +       fun insrt ([],es') = (A.update(a,h,(k,v)::es'); 
    1.60 +			     c := !c + 1;
    1.61 +			     if !c >= N then grow(hash,A,N) else ())
    1.62 +         | insrt ((e as (k',_))::es,es') = 
    1.63 +            if k == k' then A.update(a,h,(k,v)::es'@es) 
    1.64 +            else insrt(es,e::es')
    1.65 +   in  insrt (es,[])
    1.66 +   end
    1.67 +
    1.68 +   and grow(hash,A as ref a,N) =
    1.69 +       let val M = N + N
    1.70 +           val M = if M < 13 then 13 else M
    1.71 +           val a' = A.array(M,[])
    1.72 +           fun insrt (k,v) = let val h = Word.toIntX(hash k) mod M
    1.73 +                             in  A.update(a',h,(k,v)::A.sub(a',h)) end
    1.74 +       in  A.app (fn es => app insrt es) a;
    1.75 +           A := a'
    1.76 +       end
    1.77 +
    1.78 +   fun remove (hash,op==,exn,ref a,c) k =
    1.79 +   let val N  = A.length a
    1.80 +       val h  = Word.toIntX(hash k) mod N
    1.81 +       val es = A.sub(a,h)
    1.82 +       fun del ([],es') = ()
    1.83 +         | del ((e as (k',_))::es,es') = 
    1.84 +            if k == k' then (A.update(a,h,es'@es); c := !c - 1)
    1.85 +            else del(es,e::es')
    1.86 +   in  del (es,[])
    1.87 +   end
    1.88 + 
    1.89 +   fun lookup(hash,op==,exn,ref a,_) k =
    1.90 +   let val N  = A.length a
    1.91 +       val h  = Word.toIntX(hash k) mod N
    1.92 +       fun find [] = raise exn
    1.93 +         | find ((k',v)::es) = if k == k' then v else find es
    1.94 +   in  find(A.sub(a,h))
    1.95 +   end
    1.96 +
    1.97 +   fun app f (_,_,_,ref A,_) = A.app (List.app f) A
    1.98 +
    1.99 +   fun map f (_,_,_,ref A,_) =
   1.100 +   let fun fl([],x) = x
   1.101 +         | fl((k,v)::es,x) = f(k,v)::fl(es,x)
   1.102 +   in  A.foldr fl [] A end
   1.103 +
   1.104 +   fun fold f x (_,_,_,ref A,_) = 
   1.105 +   let fun fl([],x) = x
   1.106 +         | fl((k,v)::es,x) = f(k,v,fl(es,x))
   1.107 +   in  A.foldr fl x A end
   1.108 +
   1.109 +
   1.110 +   (*Additions due to L. C. Paulson and Jia Meng*)
   1.111 +
   1.112 +   val myw = ref 0w0;
   1.113 +   val () = myw := 0wx70000000;  (*workaround for Poly/ML bug*)
   1.114 +
   1.115 +   local open Word
   1.116 +	 infix << >>
   1.117 +   in
   1.118 +   fun hash_word (u,w) =
   1.119 +     let val w' = (w << 0w4) + u
   1.120 +	 val g = Word.andb(w', !myw)    (*I hope this hex constant is correct!*)
   1.121 +     in  
   1.122 +	 if g = 0w0 then Word.xorb(w', Word.xorb(g, g >> 0w24))
   1.123 +	 else w'
   1.124 +     end;
   1.125 +   end;
   1.126 +   
   1.127 +   fun hash_char (c,w) = hash_word (Word.fromInt (Char.ord c), w);
   1.128 +   
   1.129 +   fun hash_vector (v,w) = Vector.foldl hash_word w v;
   1.130 +   
   1.131 +   fun hash_string (s:string, w) = CharVector.foldl hash_char w s;
   1.132 +   
   1.133 +   fun hash_strings (ss, w) = List.foldl hash_string w ss;
   1.134 +
   1.135 +end
   1.136 +