hashtbl.mlw 2.45 KB
Newer Older
1

2 3 4 5
(* 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]. *)

6 7 8 9 10 11 12 13 14
module Hashtbl

  use import list.List
  use import map.Map

  type key

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
17
  val create (n:int) :
18 19
    {} t 'a { forall k: key. result[k] = Nil }

Andrei Paskevich's avatar
Andrei Paskevich committed
20
  val clear (h: t 'a) :
21 22
    {} unit writes h { forall k: key. h[k] = Nil }

Andrei Paskevich's avatar
Andrei Paskevich committed
23
  val add (h: t 'a) (k: key) (v: 'a) :
24 25
    {}
    unit writes h
Andrei Paskevich's avatar
Andrei Paskevich committed
26
    { h[k] = Cons v (old h)[k] /\
27 28
      forall k': key. k' <> k -> h[k'] = (old h)[k'] }

Andrei Paskevich's avatar
Andrei Paskevich committed
29
  val mem (h: t 'a) (k: key) :
30 31 32
    {}
    bool reads h
    { result=True <-> h[k] <> Nil }
33

Andrei Paskevich's avatar
Andrei Paskevich committed
34
  val find (h: t 'a) (k: key) :
35 36 37
    { h[k] <> Nil }
    'a reads h
    { match h[k] with Nil -> false | Cons v _ -> result = v end }
38

Andrei Paskevich's avatar
Andrei Paskevich committed
39
  val find_all (h: t 'a) (k: key) :
40 41 42
    {}
    list 'a reads h
    { result = h[k] }
43

44
  exception NotFound
45

Andrei Paskevich's avatar
Andrei Paskevich committed
46
  val defensive_find (h: t 'a) (k: key) :
47 48 49 50
    {}
    'a reads h raises NotFound
    { match h[k] with Nil -> false | Cons v _ -> result = v end }
    | NotFound -> { h[k] = Nil }
51

Andrei Paskevich's avatar
Andrei Paskevich committed
52
  val copy (h: t 'a) :
53 54 55
    {}
    t 'a reads h
    { forall k: key. result[k] = h[k] }
56

Andrei Paskevich's avatar
Andrei Paskevich committed
57
  val remove (h: t 'a) (k: key) :
58
    {}
59
    unit writes h
60
    { h[k] = match (old h)[k] with Nil -> Nil | Cons _ l -> l end /\
61 62
      forall k': key. k' <> k -> h[k'] = (old h)[k'] }

Andrei Paskevich's avatar
Andrei Paskevich committed
63
  val replace (h: t 'a) (k: key) (v: 'a) :
64 65 66
    {}
    unit writes h
    { (h[k] = Cons v (match (old h)[k] with Nil -> Nil | Cons _ l -> l end))
Andrei Paskevich's avatar
Andrei Paskevich committed
67
      /\
68 69 70
      forall k': key. k' <> k -> h[k'] = (old h)[k'] }

  (* TODO
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
71
     - val length: t 'a -> int (the number of distinct key)
72 73 74 75 76 77 78 79 80 81 82 83
     - 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

Andrei Paskevich's avatar
Andrei Paskevich committed
84 85 86 87
  function k1: key
  function k2: key
  function k3: key
  axiom kdiff : k1 <> k2 /\ k1 <> k3 /\ k2 <> k3
88 89 90 91 92 93 94 95 96 97 98 99

  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) }
100 101 102 103 104 105 106 107 108


end

(*
Local Variables:
compile-command: "unset LANG; make -C .. modules/hashtbl"
End:
*)