Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

hashtbl.mlw 2.32 KB
Newer Older
1 2 3 4 5 6 7 8 9 10

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
11
  function ([]) (h: t 'a) (k: key) : list 'a = Map.([]) h.contents k
12

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

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

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

Andrei Paskevich's avatar
Andrei Paskevich committed
25
  val mem (h: t 'a) (k: key) :
26 27 28
    {}
    bool reads h
    { result=True <-> h[k] <> Nil }
29

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

Andrei Paskevich's avatar
Andrei Paskevich committed
35
  val find_all (h: t 'a) (k: key) :
36 37 38
    {}
    list 'a reads h
    { result = h[k] }
39

40
  exception NotFound
41

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

Andrei Paskevich's avatar
Andrei Paskevich committed
48
  val copy (h: t 'a) :
49 50 51
    {}
    t 'a reads h
    { forall k: key. result[k] = h[k] }
52

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

Andrei Paskevich's avatar
Andrei Paskevich committed
59
  val replace (h: t 'a) (k: key) (v: 'a) :
60 61 62
    {}
    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
63
      /\
64 65
      forall k': key. k' <> k -> h[k'] = (old h)[k'] }

Andrei Paskevich's avatar
Andrei Paskevich committed
66
  val length (h: t 'a) :
67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83
    {}
    int reads h
    {} (* = the number of distinct keys *)

  (* TODO
     - 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:
*)