hashtbl.mlw 1.91 KB
Newer Older
1

MARCHE Claude's avatar
MARCHE Claude committed
2 3
(** {1 Hash tables}

4
This module provides Hash tables à la OCaml. Each key is mapped to a {h <b>stack</b>} of values,
5
   with [add h k v] pushing a new value [v] for key [k],
6
   and [remove h k] popping a value for key [k].
MARCHE Claude's avatar
MARCHE Claude committed
7 8

*)
9

10 11 12 13 14 15 16
module Hashtbl

  use import list.List
  use import map.Map

  type key

17
  type t 'a model { mutable contents: map key (list 'a) }
18

Andrei Paskevich's avatar
Andrei Paskevich committed
19
  function ([]) (h: t 'a) (k: key) : list 'a = Map.([]) h.contents k
20

21
  val create (n:int) : t 'a ensures { forall k: key. result[k] = Nil }
22

23
  val clear (h: t 'a) : unit writes {h} ensures { forall k: key. h[k] = Nil }
24

25 26 27
  val add (h: t 'a) (k: key) (v: 'a) : unit writes {h}
    ensures { h[k] = Cons v (old h)[k] }
    ensures { forall k': key. k' <> k -> h[k'] = (old h)[k'] }
28

29 30
  val mem (h: t 'a) (k: key) : bool reads {h}
    ensures { result=True <-> h[k] <> Nil }
31

32 33 34
  val find (h: t 'a) (k: key) : 'a reads {h}
    requires { h[k] <> Nil }
    ensures  { match h[k] with Nil -> false | Cons v _ -> result = v end }
35

36 37
  val find_all (h: t 'a) (k: key) : list 'a reads {h}
    ensures { result = h[k] }
38

39
  exception NotFound
40

41 42 43
  val defensive_find (h: t 'a) (k: key) : 'a reads {h}
    ensures { match h[k] with Nil -> false | Cons v _ -> result = v end }
    raises  { NotFound -> h[k] = Nil }
44

45 46 47 48 49 50 51 52 53 54 55
  val copy (h: t 'a) : t 'a reads {h}
    ensures { forall k: key. result[k] = h[k] }

  val remove (h: t 'a) (k: key) : unit writes {h}
    ensures { h[k] = match (old h)[k] with Nil -> Nil | Cons _ l -> l end }
    ensures { forall k': key. k' <> k -> h[k'] = (old h)[k'] }

  val replace (h: t 'a) (k: key) (v: 'a) : unit writes {h}
    ensures {
      h[k] = Cons v (match (old h)[k] with Nil -> Nil | Cons _ l -> l end) }
    ensures { forall k': key. k' <> k -> h[k'] = (old h)[k'] }
56

MARCHE Claude's avatar
MARCHE Claude committed
57
  (*** TODO
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
58
     - val length: t 'a -> int (the number of distinct key)
59 60 61 62 63
     - val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit
     - val fold : ('a -> 'b -> 'c -> 'c) -> ('a, 'b) t -> 'c -> 'c
  *)

end