path: root/tests/hashmap/Hashmap.Funs.fst

(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [hashmap]: function definitions *)
module Hashmap.Funs
open Primitives
include Hashmap.Types
include Hashmap.Clauses

#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"

(** [hashmap::hash_key] *)
let hash_key_fwd (k : usize) : result usize = Return k

(** [hashmap::HashMap::allocate_slots] *)
let rec hash_map_allocate_slots_fwd
  (t : Type0) (slots : vec (list_t t)) (n : usize) :
  Tot (result (vec (list_t t)))
  (decreases (hash_map_allocate_slots_decreases t slots n))
  =
  begin match n with
  | 0 -> Return slots
  | _ ->
    begin match vec_push_back (list_t t) slots ListNil with
    | Fail -> Fail
    | Return v ->
      begin match usize_sub n 1 with
      | Fail -> Fail
      | Return i ->
        begin match hash_map_allocate_slots_fwd t v i with
        | Fail -> Fail
        | Return v0 -> Return v0
        end
      end
    end
  end

(** [hashmap::HashMap::new_with_capacity] *)
let hash_map_new_with_capacity_fwd
  (t : Type0) (capacity : usize) (max_load_dividend : usize)
  (max_load_divisor : usize) :
  result (hash_map_t t)
  =
  let v = vec_new (list_t t) in
  begin match hash_map_allocate_slots_fwd t v capacity with
  | Fail -> Fail
  | Return v0 ->
    begin match usize_mul capacity max_load_dividend with
    | Fail -> Fail
    | Return i ->
      begin match usize_div i max_load_divisor with
      | Fail -> Fail
      | Return i0 ->
        Return (Mkhash_map_t 0 (max_load_dividend, max_load_divisor) i0 v0)
      end
    end
  end

(** [hashmap::HashMap::new] *)
let hash_map_new_fwd (t : Type0) : result (hash_map_t t) =
  begin match hash_map_new_with_capacity_fwd t 32 4 5 with
  | Fail -> Fail
  | Return h -> Return h
  end

(** [hashmap::HashMap::clear_slots] *)
let rec hash_map_clear_slots_fwd_back
  (t : Type0) (slots : vec (list_t t)) (i : usize) :
  Tot (result (vec (list_t t)))
  (decreases (hash_map_clear_slots_decreases t slots i))
  =
  let i0 = vec_len (list_t t) slots in
  let b = i < i0 in
  if b
  then
    begin match vec_index_mut_back (list_t t) slots i ListNil with
    | Fail -> Fail
    | Return v ->
      begin match usize_add i 1 with
      | Fail -> Fail
      | Return i1 ->
        begin match hash_map_clear_slots_fwd_back t v i1 with
        | Fail -> Fail
        | Return v0 -> Return v0
        end
      end
    end
  else Return slots

(** [hashmap::HashMap::clear] *)
let hash_map_clear_fwd_back
  (t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
  let p = self.hash_map_max_load_factor in
  let i = self.hash_map_max_load in
  let v = self.hash_map_slots in
  begin match hash_map_clear_slots_fwd_back t v 0 with
  | Fail -> Fail
  | Return v0 -> let self0 = Mkhash_map_t 0 p i v0 in Return self0
  end

(** [hashmap::HashMap::len] *)
let hash_map_len_fwd (t : Type0) (self : hash_map_t t) : result usize =
  let i = self.hash_map_num_entries in Return i

(** [hashmap::HashMap::insert_in_list] *)
let rec hash_map_insert_in_list_fwd
  (t : Type0) (key : usize) (value : t) (ls : list_t t) :
  Tot (result bool)
  (decreases (hash_map_insert_in_list_decreases t key value ls))
  =
  begin match ls with
  | ListCons ckey cvalue ls0 ->
    let b = ckey = key in
    if b
    then Return false
    else
      begin match hash_map_insert_in_list_fwd t key value ls0 with
      | Fail -> Fail
      | Return b0 -> Return b0
      end
  | ListNil -> Return true
  end

(** [hashmap::HashMap::insert_in_list] *)
let rec hash_map_insert_in_list_back
  (t : Type0) (key : usize) (value : t) (ls : list_t t) :
  Tot (result (list_t t))
  (decreases (hash_map_insert_in_list_decreases t key value ls))
  =
  begin match ls with
  | ListCons ckey cvalue ls0 ->
    let b = ckey = key in
    if b
    then let ls1 = ListCons ckey value ls0 in Return ls1
    else
      begin match hash_map_insert_in_list_back t key value ls0 with
      | Fail -> Fail
      | Return l -> let ls1 = ListCons ckey cvalue l in Return ls1
      end
  | ListNil -> let l = ListNil in let ls0 = ListCons key value l in Return ls0
  end

(** [hashmap::HashMap::insert_no_resize] *)
let hash_map_insert_no_resize_fwd_back
  (t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
  result (hash_map_t t)
  =
  begin match hash_key_fwd key with
  | Fail -> Fail
  | Return i ->
    let i0 = self.hash_map_num_entries in
    let p = self.hash_map_max_load_factor in
    let i1 = self.hash_map_max_load in
    let v = self.hash_map_slots in
    let i2 = vec_len (list_t t) v in
    begin match usize_rem i i2 with
    | Fail -> Fail
    | Return hash_mod ->
      begin match vec_index_mut_fwd (list_t t) v hash_mod with
      | Fail -> Fail
      | Return l ->
        begin match hash_map_insert_in_list_fwd t key value l with
        | Fail -> Fail
        | Return b ->
          if b
          then
            begin match usize_add i0 1 with
            | Fail -> Fail
            | Return i3 ->
              begin match hash_map_insert_in_list_back t key value l with
              | Fail -> Fail
              | Return l0 ->
                begin match vec_index_mut_back (list_t t) v hash_mod l0 with
                | Fail -> Fail
                | Return v0 ->
                  let self0 = Mkhash_map_t i3 p i1 v0 in Return self0
                end
              end
            end
          else
            begin match hash_map_insert_in_list_back t key value l with
            | Fail -> Fail
            | Return l0 ->
              begin match vec_index_mut_back (list_t t) v hash_mod l0 with
              | Fail -> Fail
              | Return v0 ->
                let self0 = Mkhash_map_t i0 p i1 v0 in Return self0
              end
            end
        end
      end
    end
  end

(** [hashmap::HashMap::move_elements_from_list] *)
let rec hash_map_move_elements_from_list_fwd_back
  (t : Type0) (ntable : hash_map_t t) (ls : list_t t) :
  Tot (result (hash_map_t t))
  (decreases (hash_map_move_elements_from_list_decreases t ntable ls))
  =
  begin match ls with
  | ListCons k v tl ->
    begin match hash_map_insert_no_resize_fwd_back t ntable k v with
    | Fail -> Fail
    | Return h ->
      begin match hash_map_move_elements_from_list_fwd_back t h tl with
      | Fail -> Fail
      | Return h0 -> Return h0
      end
    end
  | ListNil -> Return ntable
  end

(** [hashmap::HashMap::move_elements] *)
let rec hash_map_move_elements_fwd_back
  (t : Type0) (ntable : hash_map_t t) (slots : vec (list_t t)) (i : usize) :
  Tot (result ((hash_map_t t) & (vec (list_t t))))
  (decreases (hash_map_move_elements_decreases t ntable slots i))
  =
  let i0 = vec_len (list_t t) slots in
  let b = i < i0 in
  if b
  then
    begin match vec_index_mut_fwd (list_t t) slots i with
    | Fail -> Fail
    | Return l ->
      let l0 = mem_replace_fwd (list_t t) l ListNil in
      begin match hash_map_move_elements_from_list_fwd_back t ntable l0 with
      | Fail -> Fail
      | Return h ->
        let l1 = mem_replace_back (list_t t) l ListNil in
        begin match vec_index_mut_back (list_t t) slots i l1 with
        | Fail -> Fail
        | Return v ->
          begin match usize_add i 1 with
          | Fail -> Fail
          | Return i1 ->
            begin match hash_map_move_elements_fwd_back t h v i1 with
            | Fail -> Fail
            | Return (h0, v0) -> Return (h0, v0)
            end
          end
        end
      end
    end
  else Return (ntable, slots)

(** [hashmap::HashMap::try_resize] *)
let hash_map_try_resize_fwd_back
  (t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
  let i = self.hash_map_num_entries in
  let p = self.hash_map_max_load_factor in
  let i0 = self.hash_map_max_load in
  let v = self.hash_map_slots in
  let i1 = vec_len (list_t t) v in
  begin match usize_div 4294967295 2 with
  | Fail -> Fail
  | Return n1 ->
    let (i2, i3) = p in
    begin match usize_div n1 i2 with
    | Fail -> Fail
    | Return i4 ->
      let b = i1 <= i4 in
      if b
      then
        begin match usize_mul i1 2 with
        | Fail -> Fail
        | Return i5 ->
          begin match hash_map_new_with_capacity_fwd t i5 i2 i3 with
          | Fail -> Fail
          | Return h ->
            begin match hash_map_move_elements_fwd_back t h v 0 with
            | Fail -> Fail
            | Return (h0, v0) ->
              let i6 = h0.hash_map_max_load in
              let v1 = h0.hash_map_slots in
              let v2 = mem_replace_back (vec (list_t t)) v0 v1 in
              let self0 = Mkhash_map_t i (i2, i3) i6 v2 in
              Return
              self0
            end
          end
        end
      else let self0 = Mkhash_map_t i (i2, i3) i0 v in Return self0
    end
  end

(** [hashmap::HashMap::insert] *)
let hash_map_insert_fwd_back
  (t : Type0) (self : hash_map_t t) (key : usize) (value : t) :
  result (hash_map_t t)
  =
  begin match hash_map_insert_no_resize_fwd_back t self key value with
  | Fail -> Fail
  | Return h ->
    begin match hash_map_len_fwd t h with
    | Fail -> Fail
    | Return i ->
      let i0 = h.hash_map_num_entries in
      let p = h.hash_map_max_load_factor in
      let i1 = h.hash_map_max_load in
      let v = h.hash_map_slots in
      let b = i > i1 in
      if b
      then
        begin match hash_map_try_resize_fwd_back t (Mkhash_map_t i0 p i1 v)
          with
        | Fail -> Fail
        | Return h0 -> Return h0
        end
      else let self0 = Mkhash_map_t i0 p i1 v in Return self0
    end
  end

(** [hashmap::HashMap::get_in_list] *)
let rec hash_map_get_in_list_fwd
  (t : Type0) (key : usize) (ls : list_t t) :
  Tot (result t) (decreases (hash_map_get_in_list_decreases t key ls))
  =
  begin match ls with
  | ListCons ckey cvalue ls0 ->
    let b = ckey = key in
    if b
    then Return cvalue
    else
      begin match hash_map_get_in_list_fwd t key ls0 with
      | Fail -> Fail
      | Return x -> Return x
      end
  | ListNil -> Fail
  end

(** [hashmap::HashMap::get] *)
let hash_map_get_fwd
  (t : Type0) (self : hash_map_t t) (key : usize) : result t =
  begin match hash_key_fwd key with
  | Fail -> Fail
  | Return i ->
    let v = self.hash_map_slots in
    let i0 = vec_len (list_t t) v in
    begin match usize_rem i i0 with
    | Fail -> Fail
    | Return hash_mod ->
      begin match vec_index_fwd (list_t t) v hash_mod with
      | Fail -> Fail
      | Return l ->
        begin match hash_map_get_in_list_fwd t key l with
        | Fail -> Fail
        | Return x -> Return x
        end
      end
    end
  end

(** [hashmap::HashMap::get_mut_in_list] *)
let rec hash_map_get_mut_in_list_fwd
  (t : Type0) (key : usize) (ls : list_t t) :
  Tot (result t) (decreases (hash_map_get_mut_in_list_decreases t key ls))
  =
  begin match ls with
  | ListCons ckey cvalue ls0 ->
    let b = ckey = key in
    if b
    then Return cvalue
    else
      begin match hash_map_get_mut_in_list_fwd t key ls0 with
      | Fail -> Fail
      | Return x -> Return x
      end
  | ListNil -> Fail
  end

(** [hashmap::HashMap::get_mut_in_list] *)
let rec hash_map_get_mut_in_list_back
  (t : Type0) (key : usize) (ls : list_t t) (ret : t) :
  Tot (result (list_t t))
  (decreases (hash_map_get_mut_in_list_decreases t key ls))
  =
  begin match ls with
  | ListCons ckey cvalue ls0 ->
    let b = ckey = key in
    if b
    then let ls1 = ListCons ckey ret ls0 in Return ls1
    else
      begin match hash_map_get_mut_in_list_back t key ls0 ret with
      | Fail -> Fail
      | Return l -> let ls1 = ListCons ckey cvalue l in Return ls1
      end
  | ListNil -> Fail
  end

(** [hashmap::HashMap::get_mut] *)
let hash_map_get_mut_fwd
  (t : Type0) (self : hash_map_t t) (key : usize) : result t =
  begin match hash_key_fwd key with
  | Fail -> Fail
  | Return i ->
    let v = self.hash_map_slots in
    let i0 = vec_len (list_t t) v in
    begin match usize_rem i i0 with
    | Fail -> Fail
    | Return hash_mod ->
      begin match vec_index_mut_fwd (list_t t) v hash_mod with
      | Fail -> Fail
      | Return l ->
        begin match hash_map_get_mut_in_list_fwd t key l with
        | Fail -> Fail
        | Return x -> Return x
        end
      end
    end
  end

(** [hashmap::HashMap::get_mut] *)
let hash_map_get_mut_back
  (t : Type0) (self : hash_map_t t) (key : usize) (ret : t) :
  result (hash_map_t t)
  =
  begin match hash_key_fwd key with
  | Fail -> Fail
  | Return i ->
    let i0 = self.hash_map_num_entries in
    let p = self.hash_map_max_load_factor in
    let i1 = self.hash_map_max_load in
    let v = self.hash_map_slots in
    let i2 = vec_len (list_t t) v in
    begin match usize_rem i i2 with
    | Fail -> Fail
    | Return hash_mod ->
      begin match vec_index_mut_fwd (list_t t) v hash_mod with
      | Fail -> Fail
      | Return l ->
        begin match hash_map_get_mut_in_list_back t key l ret with
        | Fail -> Fail
        | Return l0 ->
          begin match vec_index_mut_back (list_t t) v hash_mod l0 with
          | Fail -> Fail
          | Return v0 -> let self0 = Mkhash_map_t i0 p i1 v0 in Return self0
          end
        end
      end
    end
  end

(** [hashmap::HashMap::remove_from_list] *)
let rec hash_map_remove_from_list_fwd
  (t : Type0) (key : usize) (ls : list_t t) :
  Tot (result (option t))
  (decreases (hash_map_remove_from_list_decreases t key ls))
  =
  begin match ls with
  | ListCons ckey x tl ->
    let b = ckey = key in
    if b
    then
      let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in
      begin match mv_ls with
      | ListCons i cvalue tl0 -> Return (Some cvalue)
      | ListNil -> Fail
      end
    else
      begin match hash_map_remove_from_list_fwd t key tl with
      | Fail -> Fail
      | Return opt -> Return opt
      end
  | ListNil -> Return None
  end

(** [hashmap::HashMap::remove_from_list] *)
let rec hash_map_remove_from_list_back
  (t : Type0) (key : usize) (ls : list_t t) :
  Tot (result (list_t t))
  (decreases (hash_map_remove_from_list_decreases t key ls))
  =
  begin match ls with
  | ListCons ckey x tl ->
    let b = ckey = key in
    if b
    then
      let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in
      begin match mv_ls with
      | ListCons i cvalue tl0 -> Return tl0
      | ListNil -> Fail
      end
    else
      begin match hash_map_remove_from_list_back t key tl with
      | Fail -> Fail
      | Return l -> let ls0 = ListCons ckey x l in Return ls0
      end
  | ListNil -> let ls0 = ListNil in Return ls0
  end

(** [hashmap::HashMap::remove] *)
let hash_map_remove_fwd
  (t : Type0) (self : hash_map_t t) (key : usize) : result (option t) =
  begin match hash_key_fwd key with
  | Fail -> Fail
  | Return i ->
    let i0 = self.hash_map_num_entries in
    let v = self.hash_map_slots in
    let i1 = vec_len (list_t t) v in
    begin match usize_rem i i1 with
    | Fail -> Fail
    | Return hash_mod ->
      begin match vec_index_mut_fwd (list_t t) v hash_mod with
      | Fail -> Fail
      | Return l ->
        begin match hash_map_remove_from_list_fwd t key l with
        | Fail -> Fail
        | Return x ->
          begin match x with
          | None -> Return None
          | Some x0 ->
            begin match usize_sub i0 1 with
            | Fail -> Fail
            | Return _ -> Return (Some x0)
            end
          end
        end
      end
    end
  end

(** [hashmap::HashMap::remove] *)
let hash_map_remove_back
  (t : Type0) (self : hash_map_t t) (key : usize) : result (hash_map_t t) =
  begin match hash_key_fwd key with
  | Fail -> Fail
  | Return i ->
    let i0 = self.hash_map_num_entries in
    let p = self.hash_map_max_load_factor in
    let i1 = self.hash_map_max_load in
    let v = self.hash_map_slots in
    let i2 = vec_len (list_t t) v in
    begin match usize_rem i i2 with
    | Fail -> Fail
    | Return hash_mod ->
      begin match vec_index_mut_fwd (list_t t) v hash_mod with
      | Fail -> Fail
      | Return l ->
        begin match hash_map_remove_from_list_fwd t key l with
        | Fail -> Fail
        | Return x ->
          begin match x with
          | None ->
            begin match hash_map_remove_from_list_back t key l with
            | Fail -> Fail
            | Return l0 ->
              begin match vec_index_mut_back (list_t t) v hash_mod l0 with
              | Fail -> Fail
              | Return v0 ->
                let self0 = Mkhash_map_t i0 p i1 v0 in Return self0
              end
            end
          | Some x0 ->
            begin match usize_sub i0 1 with
            | Fail -> Fail
            | Return i3 ->
              begin match hash_map_remove_from_list_back t key l with
              | Fail -> Fail
              | Return l0 ->
                begin match vec_index_mut_back (list_t t) v hash_mod l0 with
                | Fail -> Fail
                | Return v0 ->
                  let self0 = Mkhash_map_t i3 p i1 v0 in Return self0
                end
              end
            end
          end
        end
      end
    end
  end

(** [hashmap::test1] *)
let test1_fwd : result unit =
  begin match hash_map_new_fwd u64 with
  | Fail -> Fail
  | Return h ->
    begin match hash_map_insert_fwd_back u64 h 0 42 with
    | Fail -> Fail
    | Return h0 ->
      begin match hash_map_insert_fwd_back u64 h0 128 18 with
      | Fail -> Fail
      | Return h1 ->
        begin match hash_map_insert_fwd_back u64 h1 1024 138 with
        | Fail -> Fail
        | Return h2 ->
          begin match hash_map_insert_fwd_back u64 h2 1056 256 with
          | Fail -> Fail
          | Return h3 ->
            begin match hash_map_get_fwd u64 h3 128 with
            | Fail -> Fail
            | Return i ->
              let b = i = 18 in
              let b0 = not b in
              if b0
              then Fail
              else
                begin match hash_map_get_mut_back u64 h3 1024 56 with
                | Fail -> Fail
                | Return h4 ->
                  begin match hash_map_get_fwd u64 h4 1024 with
                  | Fail -> Fail
                  | Return i0 ->
                    let b1 = i0 = 56 in
                    let b2 = not b1 in
                    if b2
                    then Fail
                    else
                      begin match hash_map_remove_fwd u64 h4 1024 with
                      | Fail -> Fail
                      | Return x ->
                        begin match x with
                        | None -> Fail
                        | Some x0 ->
                          let b3 = x0 = 56 in
                          let b4 = not b3 in
                          if b4
                          then Fail
                          else
                            begin match hash_map_remove_back u64 h4 1024 with
                            | Fail -> Fail
                            | Return h5 ->
                              begin match hash_map_get_fwd u64 h5 0 with
                              | Fail -> Fail
                              | Return i1 ->
                                let b5 = i1 = 42 in
                                let b6 = not b5 in
                                if b6
                                then Fail
                                else
                                  begin match hash_map_get_fwd u64 h5 128 with
                                  | Fail -> Fail
                                  | Return i2 ->
                                    let b7 = i2 = 18 in
                                    let b8 = not b7 in
                                    if b8
                                    then Fail
                                    else
                                      begin match hash_map_get_fwd u64 h5 1056
                                        with
                                      | Fail -> Fail
                                      | Return i3 ->
                                        let b9 = i3 = 256 in
                                        let b10 = not b9 in
                                        if b10 then Fail else Return ()
                                      end
                                  end
                              end
                            end
                        end
                      end
                  end
                end
            end
          end
        end
      end
    end
  end

(** Unit test for [hashmap::test1] *)
let _ = assert_norm (test1_fwd = Return ())