hashtbl.mlw 2.5 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 17 18
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
19
  function ([]) (h: t 'a) (k: key) : list 'a = Map.([]) h.contents k
20

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
33
  val mem (h: t 'a) (k: key) :
34 35 36
    {}
    bool reads h
    { result=True <-> h[k] <> Nil }
37

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

Andrei Paskevich's avatar
Andrei Paskevich committed
43
  val find_all (h: t 'a) (k: key) :
44 45 46
    {}
    list 'a reads h
    { result = h[k] }
47

48
  exception NotFound
49

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

Andrei Paskevich's avatar
Andrei Paskevich committed
56
  val copy (h: t 'a) :
57 58 59
    {}
    t 'a reads h
    { forall k: key. result[k] = h[k] }
60

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

Andrei Paskevich's avatar
Andrei Paskevich committed
67
  val replace (h: t 'a) (k: key) (v: 'a) :
68 69 70
    {}
    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
71
      /\
72 73
      forall k': key. k' <> k -> h[k'] = (old h)[k'] }

MARCHE Claude's avatar
MARCHE Claude committed
74
  (*** TODO
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
75
     - val length: t 'a -> int (the number of distinct key)
76 77 78 79 80 81 82 83 84 85 86 87
     - 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
88 89 90 91
  function k1: key
  function k2: key
  function k3: key
  axiom kdiff : k1 <> k2 /\ k1 <> k3 /\ k2 <> k3
92 93 94 95 96 97 98 99 100 101 102 103

  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) }
104 105 106

end

MARCHE Claude's avatar
MARCHE Claude committed
107
(***
108 109 110 111
Local Variables:
compile-command: "unset LANG; make -C .. modules/hashtbl"
End:
*)