(* Hash tables à la OCaml: each key is mapped to a *stack* of values, with [add h k v] pushing a new value [v] for key [k], and [remove h k] popping a value for key [key]. *) module Hashtbl use import list.List use import map.Map type key type t 'a model {| mutable contents: map key (list 'a) |} function ([]) (h: t 'a) (k: key) : list 'a = Map.([]) h.contents k val create (n:int) : {} t 'a { forall k: key. result[k] = Nil } val clear (h: t 'a) : {} unit writes h { forall k: key. h[k] = Nil } val add (h: t 'a) (k: key) (v: 'a) : {} unit writes h { h[k] = Cons v (old h)[k] /\ forall k': key. k' <> k -> h[k'] = (old h)[k'] } val mem (h: t 'a) (k: key) : {} bool reads h { result=True <-> h[k] <> Nil } val find (h: t 'a) (k: key) : { h[k] <> Nil } 'a reads h { match h[k] with Nil -> false | Cons v _ -> result = v end } val find_all (h: t 'a) (k: key) : {} list 'a reads h { result = h[k] } exception NotFound val defensive_find (h: t 'a) (k: key) : {} 'a reads h raises NotFound { match h[k] with Nil -> false | Cons v _ -> result = v end } | NotFound -> { h[k] = Nil } val copy (h: t 'a) : {} t 'a reads h { forall k: key. result[k] = h[k] } val remove (h: t 'a) (k: key) : {} unit writes h { h[k] = match (old h)[k] with Nil -> Nil | Cons _ l -> l end /\ forall k': key. k' <> k -> h[k'] = (old h)[k'] } val replace (h: t 'a) (k: key) (v: 'a) : {} unit writes h { (h[k] = Cons v (match (old h)[k] with Nil -> Nil | Cons _ l -> l end)) /\ forall k': key. k' <> k -> h[k'] = (old h)[k'] } (* TODO - val length: t 'a -> int (the number of distinct key) - val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit - val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c *) end module TestHashtbl use import int.Int use import list.List use import module Hashtbl function k1: key function k2: key function k3: key axiom kdiff : k1 <> k2 /\ k1 <> k3 /\ k2 <> k3 let test1 () = let h = create 17 in add h k1 True; assert { h[k1] = Cons True Nil }; assert { h[k2] = Nil }; let v1 = find h k1 in assert { v1 = True }; add h k1 False; assert { h[k1] = Cons False (Cons True Nil) }; replace h k1 True; assert { h[k1] = Cons True (Cons True Nil) } end (* Local Variables: compile-command: "unset LANG; make -C .. modules/hashtbl" End: *)