Toccata

(* Hash table implementation.

   These are minimal hash tables, without [remove] operation.

   This is suitable to implement memo tables for instance.
   One example of such a use is in max_matrix.mlw *)

(* The signature *)
module HashTable

  use import option.Option
  use import int.Int
  use import map.Map

  type t 'a 'b model { mutable contents: map 'a (option 'b) }

  function ([]) (h: t 'a 'b) (k: 'a) : option 'b = Map.get h.contents k

  val create (n:int) : t 'a 'b
    requires { 0 < n } ensures { forall k: 'a. result[k] = None }

  val clear (h: t 'a 'b) : unit writes {h}
    ensures { forall k: 'a. h[k] = None }

  val add (h: t 'a 'b) (k: 'a) (v: 'b) : unit writes {h}
    ensures { h[k] = Some v /\ forall k': 'a. k' <> k -> h[k'] = (old h)[k'] }

  exception Not_found

  val find (h: t 'a 'b) (k: 'a) : 'b reads {h}
    ensures { h[k] = Some result } raises { Not_found -> h[k] = None }

end

(* the implementation *)
module HashTableImpl

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

  type t 'a 'b = { mutable contents: map 'a (option 'b);
                   data: array (list ('a, 'b)) }
                 invariant { length self.data > 0 }

  function get (h: t 'a 'b) (k: 'a) : option 'b = Map.get h.contents k

  function hash 'a : int

  function idx (h: t 'a 'b) (k: 'a) : int =
    mod (abs (hash k)) (length h.data)

  lemma idx_bounds:
    forall h: t 'a 'b, k: 'a.
      0 < length h.data -> 0 <= idx h k < length h.data

  (* [(k,v)] is the first pair in [l] with key [k] *)
  predicate occurs_first (k: 'a) (v: 'b) (l: list ('a, 'b)) = match l with
    | Nil            -> false
    | Cons (k',v') r -> (k = k' /\ v = v') \/ (k <> k' /\ occurs_first k v r)
  end

  lemma mem_occurs_first:
    forall k: 'a, v: 'b, l: list ('a, 'b).
    occurs_first k v l -> mem (k, v) l

  lemma cons_occurs_first:
    forall k1: 'a, v1: 'b, l: list ('a, 'b). occurs_first k1 v1 l ->
    forall k: 'a, v: 'b. k <> k1 -> occurs_first k1 v1 (Cons (k,v) l)

  type t 'c 'b
    (* h[k]=v iff (k,v) is the first pair for k in the bucket for k *)
    invariant { forall k: 'c, v: 'b.
       get self k = Some v <-> occurs_first k v self.data[idx self k] }
    (* a pair (k,v) is always stored in the right bucket *)
    invariant { forall k: 'c, v: 'b.
       forall i: int. 0 <= i < length self.data ->
         mem (k,v) self.data[i] -> i = idx self k }

  let create (n:int)
    requires { 0 < n }
    ensures  { forall k: 'a. get result k = None }
  = { contents = const None; data = make n (Nil: list ('a, 'b)) }

  let clear (h: t 'a 'b)
    ensures { forall k: 'a. get h k = None }
  = fill h.data 0 (length h.data) Nil;
    h.contents <- const None

  let idx (h: t 'a 'b) (k: 'a)
    ensures { result = idx h k }
  = mod (abs (hash k)) (length h.data)

  let add (h: t 'a 'b) (k: 'a) (v: 'b)
    ensures { get h k = Some v }
    ensures { forall k': 'a. k' <> k -> get h k' = get (old h) k' }
  = let i = idx h k in
    h.data[i] <- Cons (k,v) h.data[i];
    h.contents <- Map.set h.contents k (Some v)

  exception Not_found

  let rec lookup (k: 'a) (l: list ('a, 'b)) : 'b
    ensures { occurs_first k result l }
    raises  { Not_found -> forall v: 'b. not (mem (k, v) l) }
  = match l with
    | Nil -> raise Not_found
    | Cons (k', v) r -> if k = k' then v else lookup k r
    end

  let find (h: t 'a 'b) (k: 'a)
    ensures { get h k = Some result }
    raises  { Not_found -> get h k = None }
  = let i = idx h k in
    lookup k h.data[i]

end