summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-02-23 18:28:53 +0100
committerSon Ho2022-02-23 18:28:53 +0100
commit1a980555aa7db64af2fb745e696ea595fb142c4a (patch)
tree67eaa979a9e96a8fdca7ddaecdf408c743d8bb29
parent453818ff089f14d4ccf887184ba54b0cb568ffe5 (diff)
Improve the code generation by inlining more let-bindings
Diffstat (limited to '')
-rw-r--r--src/PureMicroPasses.ml129
-rw-r--r--src/PureUtils.ml23
-rw-r--r--tests/hashmap/Hashmap.Funs.fst198
3 files changed, 204 insertions, 146 deletions
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index dd2401b9..9b9107d1 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -327,60 +327,108 @@ let remove_meta (def : fun_def) : fun_def =
let body = obj#visit_texpression () def.body in
{ def with body }
-(** Inline the useless variable reassignments (a lot of variable assignments
- like `let x = y in ...ΓΏ` are introduced through the compilation to MIR
- and by the translation, and the variable used on the left is often unnamed.
+(** Inline the useless variable (re-)assignments:
+
+ A lot of intermediate variable assignments are introduced through the
+ compilation to MIR and by the translation itself (and the variable used
+ on the left is often unnamed).
+
+ Note that many of them are just variable "reassignments": `let x = y in ...`.
+ Some others come from ??
+
+ TODO: how do we call that when we introduce intermediate variable assignments
+ for the arguments of a function call?
[inline_named]: if `true`, inline all the assignments of the form
`let VAR = VAR in ...`, otherwise inline only the ones where the variable
on the left is anonymous.
+
+ [inline_pure]: if `true`, inline all the pure assignments where the variable
+ on the left is anonymous, but the assignments where the r-expression is
+ a non-primitive function call (i.e.: inline the binops, ADT constructions,
+ etc.).
+
+ TODO: we have a smallish issue which is that rvalues should be merged with
+ expressions... For now, this forces us to substitute whenever we can, but
+ leave the let-bindings where they are, and eliminated them in a subsequent
+ pass (if they are useless).
*)
-let inline_useless_var_reassignments (inline_named : bool) (def : fun_def) :
- fun_def =
- (* Register a substitution.
- When registering that we need to substitute v0 with v1, we check
- if v1 is itself substituted by v2, in which case we register:
- `v0 --> v2` instead of `v0 --> v1`
- *)
- let add_subst v0 v1 m =
- match VarId.Map.find_opt v1 m with
- | None -> VarId.Map.add v0 v1 m
- | Some v2 -> VarId.Map.add v0 v2 m
- in
-
+let inline_useless_var_reassignments (inline_named : bool) (inline_pure : bool)
+ (def : fun_def) : fun_def =
let obj =
- object
+ object (self)
inherit [_] map_expression as super
method! visit_Let env monadic lv re e =
(* Check that:
* - the let-binding is not monadic
* - the left-value is a variable
- * - the assigned expression is a value *)
- match (monadic, lv.value, re.e) with
- | false, LvVar (Var (lv_var, _)), Value (rv, _) -> (
- (* Check that:
- * - the left variable is unnamed or that [inline_named] is true
- * - the right-value is a variable
+ *)
+ match (monadic, lv.value) with
+ | false, LvVar (Var (lv_var, _)) ->
+ (* Check that: *)
+ let filter = false in
+ (* 1. Either:
+ * - the left variable is unnamed or [inline_named] is true
+ * - the right-expression is a variable
+ *)
+ let filter =
+ match (inline_named, lv_var.basename) with
+ | true, _ | _, None -> is_var re
+ | _ -> filter
+ in
+ (* 2. Or:
+ * - the left variable is an unnamed variable
+ * - the right-expression is a value or a primitive function call
*)
- match ((inline_named, lv_var.basename), rv.value) with
- | (true, _ | false, None), RvPlace { var; projection = [] } ->
- (* Update the environment and explore the next expression
- * (dropping the currrent let) *)
- let env = add_subst lv_var.id var env in
- super#visit_expression env e.e
- | _ -> super#visit_Let env monadic lv re e)
+ let filter =
+ if inline_pure then
+ match re.e with
+ | Value _ -> true
+ | Call call -> (
+ match call.func with
+ | Regular _ -> false
+ | Unop _ | Binop _ -> true)
+ | _ -> filter
+ else false
+ in
+
+ (* Update the environment and continue the exploration *)
+ let re = self#visit_texpression env re in
+ (* TODO: once rvalues and expressions are merged, filter the
+ * let-binding (note that for now we leave it, expect it to
+ * become useless, and wait for a subsequent pass to filter it) *)
+ (* let env = add_subst lv_var.id re env in *)
+ let env = if filter then VarId.Map.add lv_var.id re env else env in
+ let e = self#visit_texpression env e in
+ Let (monadic, lv, re, e)
| _ -> super#visit_Let env monadic lv re e
(** Visit the let-bindings to filter the useless ones (and update
the substitution map while doing so *)
- method! visit_place env p =
+ method! visit_Value env v mp =
(* Check if we need to substitute *)
- match VarId.Map.find_opt p.var env with
- | None -> (* No substitution *) p
- | Some nv ->
- (* Substitute *)
- { p with var = nv }
+ match v.value with
+ | RvPlace p -> (
+ match VarId.Map.find_opt p.var env with
+ | None -> (* No substitution *) super#visit_Value env v mp
+ | Some ne ->
+ (* Substitute - note that we need to reexplore, because
+ * there may be stacked substitutions, if we have:
+ * var0 --> var1
+ * var1 --> var2.
+ *
+ * Also: we can always substitute if we substitute with
+ * a variable. If we substitute with a value we need to
+ * check the path is empty (TODO: actually do a projection) *)
+ if is_var ne then
+ let var = as_var ne in
+ let p = { p with var } in
+ let nv = { v with value = RvPlace p } in
+ self#visit_Value env nv mp
+ else if p.projection = [] then self#visit_expression env ne.e
+ else super#visit_Value env v mp)
+ | _ -> (* No substitution *) super#visit_Value env v mp
(** Visit the places used as rvalues, to substitute them if necessary *)
end
in
@@ -901,7 +949,9 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) :
(* TODO: reorder the branches of the matches/switches *)
- (* The meta-information is now useless: remove it *)
+ (* The meta-information is now useless: remove it.
+ * Rk.: some passes below use the fact that we removed the meta-data
+ * (otherwise we would have to "unmeta" expressions before matching) *)
let def = remove_meta def in
log#ldebug (lazy ("remove_meta:\n\n" ^ fun_def_to_string ctx def ^ "\n"));
@@ -929,7 +979,10 @@ let apply_passes_to_def (config : config) (ctx : trans_ctx) (def : fun_def) :
(* Inline the useless variable reassignments *)
let inline_named_vars = true in
- let def = inline_useless_var_reassignments inline_named_vars def in
+ let inline_pure = true in
+ let def =
+ inline_useless_var_reassignments inline_named_vars inline_pure def
+ in
log#ldebug
(lazy
("inline_useless_var_assignments:\n\n" ^ fun_def_to_string ctx def
diff --git a/src/PureUtils.ml b/src/PureUtils.ml
index 1ed072e9..f51f9415 100644
--- a/src/PureUtils.ml
+++ b/src/PureUtils.ml
@@ -347,3 +347,26 @@ module TypeCheck = struct
check_typed_rvalue ctx v)
av.variant_id av.field_values v.ty
end
+
+let is_value (e : texpression) : bool =
+ match e.e with Value _ -> true | _ -> false
+
+let is_var (e : texpression) : bool =
+ match e.e with
+ | Value (v, _) -> (
+ match v.value with
+ | RvPlace { var = _; projection = [] } -> true
+ | _ -> false)
+ | _ -> false
+
+let as_var (e : texpression) : VarId.id =
+ match e.e with
+ | Value (v, _) -> (
+ match v.value with
+ | RvPlace { var; projection = [] } -> var
+ | _ -> raise (Failure "Unreachable"))
+ | _ -> raise (Failure "Unreachable")
+
+(** Remove the external occurrences of [Meta] *)
+let rec unmeta (e : texpression) : texpression =
+ match e.e with Meta (_, e) -> unmeta e | _ -> e
diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst
index d3d09765..4aa6f02c 100644
--- a/tests/hashmap/Hashmap.Funs.fst
+++ b/tests/hashmap/Hashmap.Funs.fst
@@ -8,7 +8,7 @@ include Hashmap.Clauses
#set-options "--z3rlimit 50 --fuel 0 --ifuel 1"
(** [hashmap::hash_key] *)
-let hash_key_fwd (k : usize) : result usize = Return k
+let hash_key_fwd (k : usize) : result usize = let i = k in Return i
(** [hashmap::HashMap::allocate_slots] *)
let rec hash_map_allocate_slots_fwd
@@ -68,8 +68,7 @@ let rec hash_map_clear_slots_fwd_back
(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
+ if i < i0
then
begin match vec_index_mut_back (list_t t) slots i ListNil with
| Fail -> Fail
@@ -79,21 +78,20 @@ let rec hash_map_clear_slots_fwd_back
| Return i1 ->
begin match hash_map_clear_slots_fwd_back t v i1 with
| Fail -> Fail
- | Return v0 -> Return v0
+ | Return v0 -> let slots0 = v0 in Return slots0
end
end
end
- else Return slots
+ else let slots0 = slots in Return slots0
(** [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
+ begin match hash_map_clear_slots_fwd_back t self.hash_map_slots 0 with
| Fail -> Fail
- | Return v0 -> let self0 = Mkhash_map_t 0 p i v0 in Return self0
+ | Return v -> let self0 = Mkhash_map_t 0 p i v in Return self0
end
(** [hashmap::HashMap::len] *)
@@ -108,13 +106,12 @@ let rec hash_map_insert_in_list_fwd
=
begin match ls with
| ListCons ckey cvalue ls0 ->
- let b = ckey = key in
- if b
+ if ckey = key
then Return false
else
begin match hash_map_insert_in_list_fwd t key value ls0 with
| Fail -> Fail
- | Return b0 -> Return b0
+ | Return b -> Return b
end
| ListNil -> Return true
end
@@ -127,8 +124,7 @@ let rec hash_map_insert_in_list_back
=
begin match ls with
| ListCons ckey cvalue ls0 ->
- let b = ckey = key in
- if b
+ if ckey = key
then let ls1 = ListCons ckey value ls0 in Return ls1
else
begin match hash_map_insert_in_list_back t key value ls0 with
@@ -149,12 +145,12 @@ let hash_map_insert_no_resize_fwd_back
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
+ let i2 = vec_len (list_t t) self.hash_map_slots 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
+ begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
+ with
| Fail -> Fail
| Return l ->
begin match hash_map_insert_in_list_fwd t key value l with
@@ -162,16 +158,18 @@ let hash_map_insert_no_resize_fwd_back
| Return b ->
if b
then
- begin match usize_add i0 1 with
+ begin match usize_add self.hash_map_num_entries 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
+ begin match
+ vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0
+ with
| Fail -> Fail
- | Return v0 ->
- let self0 = Mkhash_map_t i3 p i1 v0 in Return self0
+ | Return v ->
+ let self0 = Mkhash_map_t i3 p i1 v in Return self0
end
end
end
@@ -179,10 +177,11 @@ let hash_map_insert_no_resize_fwd_back
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
+ begin match
+ vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0
+ with
| Fail -> Fail
- | Return v0 ->
- let self0 = Mkhash_map_t i0 p i1 v0 in Return self0
+ | Return v -> let self0 = Mkhash_map_t i0 p i1 v in Return self0
end
end
end
@@ -203,10 +202,10 @@ let rec hash_map_move_elements_from_list_fwd_back
| Return h ->
begin match hash_map_move_elements_from_list_fwd_back t h tl with
| Fail -> Fail
- | Return h0 -> Return h0
+ | Return h0 -> let ntable0 = h0 in Return ntable0
end
end
- | ListNil -> Return ntable
+ | ListNil -> let ntable0 = ntable in Return ntable0
end
(** [hashmap::HashMap::move_elements] *)
@@ -216,8 +215,7 @@ let rec hash_map_move_elements_fwd_back
(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
+ if i < i0
then
begin match vec_index_mut_fwd (list_t t) slots i with
| Fail -> Fail
@@ -235,31 +233,30 @@ let rec hash_map_move_elements_fwd_back
| Return i1 ->
begin match hash_map_move_elements_fwd_back t h v i1 with
| Fail -> Fail
- | Return (h0, v0) -> Return (h0, v0)
+ | Return (h0, v0) ->
+ let ntable0 = h0 in let slots0 = v0 in Return (ntable0, slots0)
end
end
end
end
end
- else Return (ntable, slots)
+ else let ntable0 = ntable in let slots0 = slots in Return (ntable0, slots0)
(** [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
+ let i1 = vec_len (list_t t) self.hash_map_slots in
begin match usize_div 4294967295 2 with
| Fail -> Fail
| Return n1 ->
- let (i2, i3) = p in
+ let (i2, i3) = self.hash_map_max_load_factor in
begin match usize_div n1 i2 with
| Fail -> Fail
| Return i4 ->
- let b = i1 <= i4 in
- if b
+ if i1 <= i4
then
begin match usize_mul i1 2 with
| Fail -> Fail
@@ -267,13 +264,14 @@ let hash_map_try_resize_fwd_back
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
+ begin match
+ hash_map_move_elements_fwd_back t h self.hash_map_slots 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
+ let v1 = mem_replace_back (vec (list_t t)) v0 h0.hash_map_slots
+ in
+ let self0 = Mkhash_map_t i (i2, i3) i6 v1 in
Return
self0
end
@@ -298,13 +296,12 @@ let hash_map_insert_fwd_back
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
+ if i > h.hash_map_max_load
then
begin match hash_map_try_resize_fwd_back t (Mkhash_map_t i0 p i1 v)
with
| Fail -> Fail
- | Return h0 -> Return h0
+ | Return h0 -> let self0 = h0 in Return self0
end
else let self0 = Mkhash_map_t i0 p i1 v in Return self0
end
@@ -318,13 +315,12 @@ let rec hash_map_contains_key_in_list_fwd
=
begin match ls with
| ListCons ckey x ls0 ->
- let b = ckey = key in
- if b
+ if ckey = key
then Return true
else
begin match hash_map_contains_key_in_list_fwd t key ls0 with
| Fail -> Fail
- | Return b0 -> Return b0
+ | Return b -> Return b
end
| ListNil -> Return false
end
@@ -335,12 +331,11 @@ let hash_map_contains_key_fwd
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
+ let i0 = vec_len (list_t t) self.hash_map_slots 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
+ begin match vec_index_fwd (list_t t) self.hash_map_slots hash_mod with
| Fail -> Fail
| Return l ->
begin match hash_map_contains_key_in_list_fwd t key l with
@@ -358,13 +353,12 @@ let rec hash_map_get_in_list_fwd
=
begin match ls with
| ListCons ckey cvalue ls0 ->
- let b = ckey = key in
- if b
+ if ckey = key
then Return cvalue
else
begin match hash_map_get_in_list_fwd t key ls0 with
| Fail -> Fail
- | Return x -> Return x
+ | Return x -> let x0 = x in Return x0
end
| ListNil -> Fail
end
@@ -375,17 +369,16 @@ let hash_map_get_fwd
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
+ let i0 = vec_len (list_t t) self.hash_map_slots 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
+ begin match vec_index_fwd (list_t t) self.hash_map_slots 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
+ | Return x -> let x0 = x in Return x0
end
end
end
@@ -398,13 +391,12 @@ let rec hash_map_get_mut_in_list_fwd
=
begin match ls with
| ListCons ckey cvalue ls0 ->
- let b = ckey = key in
- if b
+ if ckey = key
then Return cvalue
else
begin match hash_map_get_mut_in_list_fwd t key ls0 with
| Fail -> Fail
- | Return x -> Return x
+ | Return x -> let x0 = x in Return x0
end
| ListNil -> Fail
end
@@ -417,9 +409,8 @@ let rec hash_map_get_mut_in_list_back
=
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
+ if ckey = key
+ then let x = ret in let ls1 = ListCons ckey x ls0 in Return ls1
else
begin match hash_map_get_mut_in_list_back t key ls0 ret with
| Fail -> Fail
@@ -434,17 +425,17 @@ let hash_map_get_mut_fwd
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
+ let i0 = vec_len (list_t t) self.hash_map_slots 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
+ begin match vec_index_mut_fwd (list_t t) self.hash_map_slots 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
+ | Return x -> let x0 = x in Return x0
end
end
end
@@ -461,20 +452,21 @@ let hash_map_get_mut_back
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
+ let i2 = vec_len (list_t t) self.hash_map_slots 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
+ begin match vec_index_mut_fwd (list_t t) self.hash_map_slots 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
+ begin match
+ vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0 with
| Fail -> Fail
- | Return v0 -> let self0 = Mkhash_map_t i0 p i1 v0 in Return self0
+ | Return v -> let self0 = Mkhash_map_t i0 p i1 v in Return self0
end
end
end
@@ -489,8 +481,7 @@ let rec hash_map_remove_from_list_fwd
=
begin match ls with
| ListCons ckey x tl ->
- let b = ckey = key in
- if b
+ if ckey = key
then
let mv_ls = mem_replace_fwd (list_t t) (ListCons ckey x tl) ListNil in
begin match mv_ls with
@@ -513,12 +504,11 @@ let rec hash_map_remove_from_list_back
=
begin match ls with
| ListCons ckey x tl ->
- let b = ckey = key in
- if b
+ if ckey = key
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
+ | ListCons i cvalue tl0 -> let ls0 = tl0 in Return ls0
| ListNil -> Fail
end
else
@@ -535,13 +525,12 @@ let hash_map_remove_fwd
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
+ let i0 = vec_len (list_t t) self.hash_map_slots 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
+ begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
+ with
| Fail -> Fail
| Return l ->
begin match hash_map_remove_from_list_fwd t key l with
@@ -550,7 +539,7 @@ let hash_map_remove_fwd
begin match x with
| None -> Return None
| Some x0 ->
- begin match usize_sub i0 1 with
+ begin match usize_sub self.hash_map_num_entries 1 with
| Fail -> Fail
| Return _ -> Return (Some x0)
end
@@ -569,12 +558,12 @@ let hash_map_remove_back
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
+ let i2 = vec_len (list_t t) self.hash_map_slots 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
+ begin match vec_index_mut_fwd (list_t t) self.hash_map_slots hash_mod
+ with
| Fail -> Fail
| Return l ->
begin match hash_map_remove_from_list_fwd t key l with
@@ -585,23 +574,26 @@ let hash_map_remove_back
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
+ begin match
+ vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0
+ with
| Fail -> Fail
- | Return v0 ->
- let self0 = Mkhash_map_t i0 p i1 v0 in Return self0
+ | Return v -> let self0 = Mkhash_map_t i0 p i1 v in Return self0
end
end
| Some x0 ->
- begin match usize_sub i0 1 with
+ begin match usize_sub self.hash_map_num_entries 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
+ begin match
+ vec_index_mut_back (list_t t) self.hash_map_slots hash_mod l0
+ with
| Fail -> Fail
- | Return v0 ->
- let self0 = Mkhash_map_t i3 p i1 v0 in Return self0
+ | Return v ->
+ let self0 = Mkhash_map_t i3 p i1 v in Return self0
end
end
end
@@ -631,9 +623,7 @@ let test1_fwd : result unit =
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
+ if not (i = 18)
then Fail
else
begin match hash_map_get_mut_back u64 h3 1024 56 with
@@ -642,9 +632,7 @@ let test1_fwd : result unit =
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
+ if not (i0 = 56)
then Fail
else
begin match hash_map_remove_fwd u64 h4 1024 with
@@ -653,9 +641,7 @@ let test1_fwd : result unit =
begin match x with
| None -> Fail
| Some x0 ->
- let b3 = x0 = 56 in
- let b4 = not b3 in
- if b4
+ if not (x0 = 56)
then Fail
else
begin match hash_map_remove_back u64 h4 1024 with
@@ -664,26 +650,22 @@ let test1_fwd : result unit =
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
+ if not (i1 = 42)
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
+ if not (i2 = 18)
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 ()
+ if not (i3 = 256)
+ then Fail
+ else Return ()
end
end
end