module Hashtbl

  use import list.List
  use import map.Map

  type key

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

  function ([]) (h: t 'a) (k: key) : list 'a = Map.([]) h.contents 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] /\
      forall k': key. k' <> k -> h[k'] = (old h)[k'] }

  parameter mem (h: t 'a) (k: key) :
    {}
    bool reads h
    { result=True <-> h[k] <> Nil }

  parameter find (h: t 'a) (k: key) :
    { h[k] <> Nil }
    'a reads h
    { match h[k] with Nil -> false | Cons v _ -> result = v end }

  parameter find_all (h: t 'a) (k: key) :
    {}
    list 'a reads h
    { result = h[k] }

  exception NotFound

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

  parameter copy (h: t 'a) :
    {}
    t 'a reads h
    { forall k: key. result[k] = h[k] }

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

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

  parameter length (h: t 'a) :
    {}
    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

  function k1: key
  function k2: key
  function k3: key
  axiom kdiff : k1 <> k2 /\ k1 <> k3 /\ k2 <> k3

  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) }


end

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