hashtbl.mlw 1.03 KB
Newer Older
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:
*)