hashtbl.mlw 1.03 KB
 Jean-Christophe Filliâtre committed May 17, 2011 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 `````` module Hashtbl use import list.List use import map.Map type key type t 'a model {| mutable contents: map key (list 'a) |} logic ([]) (h: t 'a) (k: key) : list 'a = get h k parameter create: n:int -> {} t 'a { forall k: key. result[k] = Nil } parameter clear: h: t 'a -> {} unit writes h { forall k: key. h[k] = Nil } parameter add: h: t 'a -> k: key -> v: 'a -> {} unit writes h { h[k] = Cons v (old h)[k] and forall k': key. k' <> k -> h[k'] = (old h)[k'] } (* val copy : ('a, 'b) t -> ('a, 'b) t val find : ('a, 'b) t -> 'a -> 'b val find_all : ('a, 'b) t -> 'a -> 'b list val mem : ('a, 'b) t -> 'a -> bool val remove : ('a, 'b) t -> 'a -> unit val replace : ('a, 'b) t -> 'a -> 'b -> unit val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c val length : ('a, 'b) t -> int *) end (* Local Variables: compile-command: "unset LANG; make -C .. modules/hashtbl" End: *)``````