(* Hash table implementation

   Jean-Christophe Filliâtre (CNRS)
   Andrei Paskevich (Univ Paris Sud) *)

module HashtblImpl

  use import int.Int
  use import int.ComputerDivision
  use import option.Option
  use import list.List
  use import list.Mem
  use import map.Map
  use import map.Const
  use import array.Array

  type key

  val eq (x y : key) : bool
    ensures { result <-> x = y }

  val function hash key : int
    ensures { 0 <= result }

  let function bucket (k: key) (n: int) : int
    requires { 0 < n }
    ensures { 0 <= result < n }
  = mod (hash k) n

  lemma bucket_bounds:
    forall n: int. 0 < n ->
    forall k: key. 0 <= bucket k n < n

  predicate in_data (k: key) (v: 'a) (d: array (list (key, 'a))) =
    mem (k,v) d[bucket k (length d)]

  predicate good_data (k: key) (v: 'a)
      (m: map key (option 'a)) (d: array (list (key, 'a))) =
    Map.get m k = Some v <-> in_data k v d

  predicate good_hash (d: array (list (key, 'a))) (i: int) =
    forall k: key, v: 'a. mem (k,v) d[i] -> bucket k (length d) = i

  type t 'a = { mutable size: int;   (* total number of elements *)
                mutable data: array (list (key, 'a)); (* buckets *)
          ghost mutable view: map key (option 'a); (* pure model *) }

    invariant { 0 < length data }
    invariant {
      forall i: int. 0 <= i < length data -> good_hash data i }
    invariant { forall k: key, v: 'a. good_data k v view data }
    by { size = 0; data = make 1 Nil; view = Const.const None }

  let create (n: int) : t 'a
    requires { 1 <= n }
    ensures  { result.view = Const.const None }
  =
    { size = 0; data = make n Nil; view = Const.const None }

  let clear (h: t 'a) : unit
    writes  { h.size, h.data.elts, h.view }
    ensures { h.view = Const.const None }
  =
    h.size <- 0;
    fill h.data 0 (length h.data) Nil;
    h.view <- Const.const None

  let resize (h: t 'a) : unit
    writes  { h.data }
  =
    let odata = h.data in
    let osize = length odata in
    let nsize = 2 * osize + 1 in
    let ndata = make nsize Nil in
    let rec rehash (ghost i : int) l
      requires { forall k: key, v: 'a. mem (k,v) l -> bucket k osize = i }
      requires { forall j: int. 0 <= j < nsize -> good_hash ndata j }
      requires { forall k: key, v: 'a.
        if 0 <= bucket k osize < i then good_data k v h.view ndata
        else if bucket k osize = i then
          (Map.get h.view k = Some v <-> mem (k,v) l \/ in_data k v ndata)
        else not in_data k v ndata }
      ensures  { forall j: int. 0 <= j < nsize -> good_hash ndata j }
      ensures  { forall k: key, v: 'a.
        if 0 <= bucket k osize <= i then good_data k v h.view ndata
        else not in_data k v ndata }
      variant  { l }
    = match l with
      | Nil -> ()
      | Cons (k, v) r ->
          let b = bucket k nsize in
          ndata[b] <- Cons (k, v) (ndata[b]);
          rehash i r
    end in
    for i = 0 to osize - 1 do
      invariant { forall j: int. 0 <= j < nsize -> good_hash ndata j }
      invariant { forall k: key, v: 'a.
        if 0 <= bucket k osize < i then good_data k v h.view ndata
        else not in_data k v ndata }
      rehash i odata[i]
    done;
    h.data <- ndata

  let rec list_find (k: key) (l: list (key, 'a)) : option 'a
    variant { l }
    ensures { match result with
              | None -> forall v: 'a. not (mem (k, v) l)
              | Some v -> mem (k, v) l
              end }
  = match l with
    | Nil -> None
    | Cons (k', v) r -> if eq k k' then Some v else list_find k r
    end

  let find (h: t 'a) (k: key) : option 'a
    ensures { result = Map.get h.view k }
  =
    let i = bucket k (length h.data) in
    list_find k h.data[i]

  let rec list_remove (k: key) (l: list (key, 'a)) : list (key, 'a)
    variant { l }
    ensures { forall k': key, v: 'a.
                mem (k',v) result <-> mem (k',v) l /\ k' <> k }
  = match l with
    | Nil -> Nil
    | Cons ((k', _) as p) r ->
        if eq k k' then list_remove k r else Cons p (list_remove k r)
    end

  let remove (h: t 'a) (k: key) : unit
    writes  { h.data.elts, h.view, h.size }
    ensures { Map.get h.view k = None }
    ensures { forall k': key. k' <> k ->
                Map.get h.view k' = Map.get (old h.view) k' }
  = let i = bucket k (length h.data) in
    let l = h.data[i] in
    match list_find k l with
    | None ->
        ()
    | Some _ ->
        h.data[i] <- list_remove k l;
        h.size <- h.size - 1;
        h.view <- Map.set h.view k None
    end

  let add (h: t 'a) (k: key) (v: 'a) : unit
    writes  { h, h.data.elts }
    ensures { Map.get h.view k = Some v }
    ensures { forall k': key. k' <> k ->
                Map.get h.view k' = Map.get (old h.view) k' }
  =
    if h.size = length h.data then resize h;
    remove h k;
    let i = bucket k (length h.data) in
    h.data[i] <- Cons (k, v) h.data[i];
    h.size <- h.size + 1;
    h.view <- Map.set h.view k (Some v)

(*
  let alias (h: t int) (k: key) : unit =
    let old_data = h.data in
    add h k 42;
    old_data[0] <- Nil
*)
end