summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tests/betree/BetreeMain.Funs.fst113
-rw-r--r--tests/betree/Primitives.fst2
-rw-r--r--tests/hashmap/Hashmap.Funs.fst67
-rw-r--r--tests/hashmap/Primitives.fst2
-rw-r--r--tests/hashmap_on_disk/HashmapMain.Funs.fst70
-rw-r--r--tests/hashmap_on_disk/Primitives.fst2
-rw-r--r--tests/misc/External.Funs.fst3
-rw-r--r--tests/misc/NoNestedBorrows.fst49
-rw-r--r--tests/misc/Paper.fst14
-rw-r--r--tests/misc/Primitives.fst2
10 files changed, 130 insertions, 194 deletions
diff --git a/tests/betree/BetreeMain.Funs.fst b/tests/betree/BetreeMain.Funs.fst
index b11ca399..9b960ce5 100644
--- a/tests/betree/BetreeMain.Funs.fst
+++ b/tests/betree/BetreeMain.Funs.fst
@@ -135,9 +135,9 @@ let rec betree_list_split_at_fwd
Tot (result ((betree_list_t t) & (betree_list_t t)))
(decreases (betree_list_split_at_decreases t self n))
=
- begin match n with
- | 0 -> Return (BetreeListNil, self)
- | _ ->
+ if n = 0
+ then Return (BetreeListNil, self)
+ else
begin match self with
| BetreeListCons hd tl ->
begin match u64_sub n 1 with
@@ -152,7 +152,6 @@ let rec betree_list_split_at_fwd
end
| BetreeListNil -> Fail
end
- end
(** [betree_main::betree::List::{1}::push_front] *)
let betree_list_push_front_fwd_back
@@ -528,10 +527,7 @@ and betree_node_lookup_fwd
let (k, msg) = p in
if k <> key
then
- begin match
- betree_internal_lookup_in_children_fwd (Mkbetree_internal_t
- node.betree_internal_id node.betree_internal_pivot
- node.betree_internal_left node.betree_internal_right) key st0
+ begin match betree_internal_lookup_in_children_fwd node key st0
with
| Fail -> Fail
| Return (st1, opt) ->
@@ -559,10 +555,7 @@ and betree_node_lookup_fwd
| Return _ -> Return (st0, None)
end
| BetreeMessageUpsert ufs ->
- begin match
- betree_internal_lookup_in_children_fwd (Mkbetree_internal_t
- node.betree_internal_id node.betree_internal_pivot
- node.betree_internal_left node.betree_internal_right) key st0
+ begin match betree_internal_lookup_in_children_fwd node key st0
with
| Fail -> Fail
| Return (st1, v) ->
@@ -572,10 +565,7 @@ and betree_node_lookup_fwd
| Fail -> Fail
| Return (st2, v0) ->
begin match
- betree_internal_lookup_in_children_back
- (Mkbetree_internal_t node.betree_internal_id
- node.betree_internal_pivot node.betree_internal_left
- node.betree_internal_right) key st0 with
+ betree_internal_lookup_in_children_back node key st0 with
| Fail -> Fail
| Return node0 ->
begin match
@@ -601,11 +591,7 @@ and betree_node_lookup_fwd
end
end
| BetreeListNil ->
- begin match
- betree_internal_lookup_in_children_fwd (Mkbetree_internal_t
- node.betree_internal_id node.betree_internal_pivot
- node.betree_internal_left node.betree_internal_right) key st0
- with
+ begin match betree_internal_lookup_in_children_fwd node key st0 with
| Fail -> Fail
| Return (st1, opt) ->
begin match
@@ -653,10 +639,7 @@ and betree_node_lookup_back
(BetreeListCons (k, msg) l) with
| Fail -> Fail
| Return _ ->
- begin match
- betree_internal_lookup_in_children_back (Mkbetree_internal_t
- node.betree_internal_id node.betree_internal_pivot
- node.betree_internal_left node.betree_internal_right) key st0
+ begin match betree_internal_lookup_in_children_back node key st0
with
| Fail -> Fail
| Return node0 -> Return (BetreeNodeInternal node0)
@@ -669,26 +652,17 @@ and betree_node_lookup_back
betree_node_lookup_first_message_for_key_back key msgs
(BetreeListCons (k, BetreeMessageInsert v) l) with
| Fail -> Fail
- | Return _ ->
- Return (BetreeNodeInternal (Mkbetree_internal_t
- node.betree_internal_id node.betree_internal_pivot
- node.betree_internal_left node.betree_internal_right))
+ | Return _ -> Return (BetreeNodeInternal node)
end
| BetreeMessageDelete ->
begin match
betree_node_lookup_first_message_for_key_back key msgs
(BetreeListCons (k, BetreeMessageDelete) l) with
| Fail -> Fail
- | Return _ ->
- Return (BetreeNodeInternal (Mkbetree_internal_t
- node.betree_internal_id node.betree_internal_pivot
- node.betree_internal_left node.betree_internal_right))
+ | Return _ -> Return (BetreeNodeInternal node)
end
| BetreeMessageUpsert ufs ->
- begin match
- betree_internal_lookup_in_children_fwd (Mkbetree_internal_t
- node.betree_internal_id node.betree_internal_pivot
- node.betree_internal_left node.betree_internal_right) key st0
+ begin match betree_internal_lookup_in_children_fwd node key st0
with
| Fail -> Fail
| Return (st1, v) ->
@@ -698,10 +672,7 @@ and betree_node_lookup_back
| Fail -> Fail
| Return (st2, _) ->
begin match
- betree_internal_lookup_in_children_back
- (Mkbetree_internal_t node.betree_internal_id
- node.betree_internal_pivot node.betree_internal_left
- node.betree_internal_right) key st0 with
+ betree_internal_lookup_in_children_back node key st0 with
| Fail -> Fail
| Return node0 ->
begin match
@@ -718,12 +689,7 @@ and betree_node_lookup_back
betree_store_internal_node_fwd
node0.betree_internal_id msgs0 st2 with
| Fail -> Fail
- | Return (_, _) ->
- Return (BetreeNodeInternal (Mkbetree_internal_t
- node0.betree_internal_id
- node0.betree_internal_pivot
- node0.betree_internal_left
- node0.betree_internal_right))
+ | Return (_, _) -> Return (BetreeNodeInternal node0)
end
end
end
@@ -737,10 +703,7 @@ and betree_node_lookup_back
BetreeListNil with
| Fail -> Fail
| Return _ ->
- begin match
- betree_internal_lookup_in_children_back (Mkbetree_internal_t
- node.betree_internal_id node.betree_internal_pivot
- node.betree_internal_left node.betree_internal_right) key st0
+ begin match betree_internal_lookup_in_children_back node key st0
with
| Fail -> Fail
| Return node0 -> Return (BetreeNodeInternal node0)
@@ -755,9 +718,7 @@ and betree_node_lookup_back
| Return (_, bindings) ->
begin match betree_node_lookup_in_bindings_fwd key bindings with
| Fail -> Fail
- | Return _ ->
- Return (BetreeNodeLeaf (Mkbetree_leaf_t node.betree_leaf_id
- node.betree_leaf_size))
+ | Return _ -> Return (BetreeNodeLeaf node)
end
end
end
@@ -1323,17 +1284,13 @@ and betree_node_apply_messages_fwd
if num_msgs >= params.betree_params_min_flush_size
then
begin match
- betree_internal_flush_fwd (Mkbetree_internal_t
- node.betree_internal_id node.betree_internal_pivot
- node.betree_internal_left node.betree_internal_right) params
- node_id_cnt content0 st0 with
+ betree_internal_flush_fwd node params node_id_cnt content0 st0
+ with
| Fail -> Fail
| Return (st1, content1) ->
begin match
- betree_internal_flush_back (Mkbetree_internal_t
- node.betree_internal_id node.betree_internal_pivot
- node.betree_internal_left node.betree_internal_right) params
- node_id_cnt content0 st0 with
+ betree_internal_flush_back node params node_id_cnt content0 st0
+ with
| Fail -> Fail
| Return (node0, _) ->
begin match
@@ -1370,8 +1327,7 @@ and betree_node_apply_messages_fwd
if len >= i
then
begin match
- betree_leaf_split_fwd (Mkbetree_leaf_t node.betree_leaf_id
- node.betree_leaf_size) content0 params node_id_cnt st0 with
+ betree_leaf_split_fwd node content0 params node_id_cnt st0 with
| Fail -> Fail
| Return (st1, _) ->
begin match
@@ -1418,17 +1374,13 @@ and betree_node_apply_messages_back
if num_msgs >= params.betree_params_min_flush_size
then
begin match
- betree_internal_flush_fwd (Mkbetree_internal_t
- node.betree_internal_id node.betree_internal_pivot
- node.betree_internal_left node.betree_internal_right) params
- node_id_cnt content0 st0 with
+ betree_internal_flush_fwd node params node_id_cnt content0 st0
+ with
| Fail -> Fail
| Return (st1, content1) ->
begin match
- betree_internal_flush_back (Mkbetree_internal_t
- node.betree_internal_id node.betree_internal_pivot
- node.betree_internal_left node.betree_internal_right) params
- node_id_cnt content0 st0 with
+ betree_internal_flush_back node params node_id_cnt content0 st0
+ with
| Fail -> Fail
| Return (node0, node_id_cnt0) ->
begin match
@@ -1436,10 +1388,7 @@ and betree_node_apply_messages_back
content1 st1 with
| Fail -> Fail
| Return (_, _) ->
- Return (BetreeNodeInternal (Mkbetree_internal_t
- node0.betree_internal_id node0.betree_internal_pivot
- node0.betree_internal_left node0.betree_internal_right),
- node_id_cnt0)
+ Return (BetreeNodeInternal node0, node_id_cnt0)
end
end
end
@@ -1448,11 +1397,7 @@ and betree_node_apply_messages_back
betree_store_internal_node_fwd node.betree_internal_id content0
st0 with
| Fail -> Fail
- | Return (_, _) ->
- Return (BetreeNodeInternal (Mkbetree_internal_t
- node.betree_internal_id node.betree_internal_pivot
- node.betree_internal_left node.betree_internal_right),
- node_id_cnt)
+ | Return (_, _) -> Return (BetreeNodeInternal node, node_id_cnt)
end
end
end
@@ -1473,8 +1418,7 @@ and betree_node_apply_messages_back
if len >= i
then
begin match
- betree_leaf_split_fwd (Mkbetree_leaf_t node.betree_leaf_id
- node.betree_leaf_size) content0 params node_id_cnt st0 with
+ betree_leaf_split_fwd node content0 params node_id_cnt st0 with
| Fail -> Fail
| Return (st1, new_node) ->
begin match
@@ -1483,8 +1427,7 @@ and betree_node_apply_messages_back
| Fail -> Fail
| Return (_, _) ->
begin match
- betree_leaf_split_back (Mkbetree_leaf_t node.betree_leaf_id
- node.betree_leaf_size) content0 params node_id_cnt st0
+ betree_leaf_split_back node content0 params node_id_cnt st0
with
| Fail -> Fail
| Return node_id_cnt0 ->
diff --git a/tests/betree/Primitives.fst b/tests/betree/Primitives.fst
index f73c8c09..fe351f3a 100644
--- a/tests/betree/Primitives.fst
+++ b/tests/betree/Primitives.fst
@@ -146,7 +146,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
mk_scalar ty (x * y)
(** Cast an integer from a [src_ty] to a [tgt_ty] *)
-let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
+let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
mk_scalar tgt_ty x
/// The scalar types
diff --git a/tests/hashmap/Hashmap.Funs.fst b/tests/hashmap/Hashmap.Funs.fst
index a97c52b9..83c245fb 100644
--- a/tests/hashmap/Hashmap.Funs.fst
+++ b/tests/hashmap/Hashmap.Funs.fst
@@ -16,9 +16,9 @@ let rec hash_map_allocate_slots_fwd
Tot (result (vec (list_t t)))
(decreases (hash_map_allocate_slots_decreases t slots n))
=
- begin match n with
- | 0 -> Return slots
- | _ ->
+ if n = 0
+ then Return slots
+ else
begin match vec_push_back (list_t t) slots ListNil with
| Fail -> Fail
| Return slots0 ->
@@ -31,7 +31,6 @@ let rec hash_map_allocate_slots_fwd
end
end
end
- end
(** [hashmap::HashMap::{0}::new_with_capacity] *)
let hash_map_new_with_capacity_fwd
@@ -245,35 +244,39 @@ let rec hash_map_move_elements_fwd_back
(** [hashmap::HashMap::{0}::try_resize] *)
let hash_map_try_resize_fwd_back
(t : Type0) (self : hash_map_t t) : result (hash_map_t t) =
- let capacity = vec_len (list_t t) self.hash_map_slots in
- begin match usize_div 4294967295 2 with
+ begin match scalar_cast U32 Usize 4294967295 with
| Fail -> Fail
- | Return n1 ->
- let (i, i0) = self.hash_map_max_load_factor in
- begin match usize_div n1 i with
+ | Return max_usize ->
+ let capacity = vec_len (list_t t) self.hash_map_slots in
+ begin match usize_div max_usize 2 with
| Fail -> Fail
- | Return i1 ->
- if capacity <= i1
- then
- begin match usize_mul capacity 2 with
- | Fail -> Fail
- | Return i2 ->
- begin match hash_map_new_with_capacity_fwd t i2 i i0 with
+ | Return n1 ->
+ let (i, i0) = self.hash_map_max_load_factor in
+ begin match usize_div n1 i with
+ | Fail -> Fail
+ | Return i1 ->
+ if capacity <= i1
+ then
+ begin match usize_mul capacity 2 with
| Fail -> Fail
- | Return ntable ->
- begin match
- hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0
- with
+ | Return i2 ->
+ begin match hash_map_new_with_capacity_fwd t i2 i i0 with
| Fail -> Fail
- | Return (ntable0, _) ->
- Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
- ntable0.hash_map_max_load ntable0.hash_map_slots)
+ | Return ntable ->
+ begin match
+ hash_map_move_elements_fwd_back t ntable self.hash_map_slots 0
+ with
+ | Fail -> Fail
+ | Return (ntable0, _) ->
+ Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
+ ntable0.hash_map_max_load ntable0.hash_map_slots)
+ end
end
end
- end
- else
- Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
- self.hash_map_max_load self.hash_map_slots)
+ else
+ Return (Mkhash_map_t self.hash_map_num_entries (i, i0)
+ self.hash_map_max_load self.hash_map_slots)
+ end
end
end
@@ -290,17 +293,11 @@ let hash_map_insert_fwd_back
| Return i ->
if i > self0.hash_map_max_load
then
- begin match
- hash_map_try_resize_fwd_back t (Mkhash_map_t
- self0.hash_map_num_entries self0.hash_map_max_load_factor
- self0.hash_map_max_load self0.hash_map_slots) with
+ begin match hash_map_try_resize_fwd_back t self0 with
| Fail -> Fail
| Return self1 -> Return self1
end
- else
- Return (Mkhash_map_t self0.hash_map_num_entries
- self0.hash_map_max_load_factor self0.hash_map_max_load
- self0.hash_map_slots)
+ else Return self0
end
end
diff --git a/tests/hashmap/Primitives.fst b/tests/hashmap/Primitives.fst
index f73c8c09..fe351f3a 100644
--- a/tests/hashmap/Primitives.fst
+++ b/tests/hashmap/Primitives.fst
@@ -146,7 +146,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
mk_scalar ty (x * y)
(** Cast an integer from a [src_ty] to a [tgt_ty] *)
-let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
+let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
mk_scalar tgt_ty x
/// The scalar types
diff --git a/tests/hashmap_on_disk/HashmapMain.Funs.fst b/tests/hashmap_on_disk/HashmapMain.Funs.fst
index 160df880..d01046ec 100644
--- a/tests/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/hashmap_on_disk/HashmapMain.Funs.fst
@@ -17,9 +17,9 @@ let rec hashmap_hash_map_allocate_slots_fwd
Tot (result (vec (hashmap_list_t t)))
(decreases (hashmap_hash_map_allocate_slots_decreases t slots n))
=
- begin match n with
- | 0 -> Return slots
- | _ ->
+ if n = 0
+ then Return slots
+ else
begin match vec_push_back (hashmap_list_t t) slots HashmapListNil with
| Fail -> Fail
| Return slots0 ->
@@ -32,7 +32,6 @@ let rec hashmap_hash_map_allocate_slots_fwd
end
end
end
- end
(** [hashmap_main::hashmap::HashMap::{0}::new_with_capacity] *)
let hashmap_hash_map_new_with_capacity_fwd
@@ -258,36 +257,40 @@ let rec hashmap_hash_map_move_elements_fwd_back
(** [hashmap_main::hashmap::HashMap::{0}::try_resize] *)
let hashmap_hash_map_try_resize_fwd_back
(t : Type0) (self : hashmap_hash_map_t t) : result (hashmap_hash_map_t t) =
- let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
- begin match usize_div 4294967295 2 with
+ begin match scalar_cast U32 Usize 4294967295 with
| Fail -> Fail
- | Return n1 ->
- let (i, i0) = self.hashmap_hash_map_max_load_factor in
- begin match usize_div n1 i with
+ | Return max_usize ->
+ let capacity = vec_len (hashmap_list_t t) self.hashmap_hash_map_slots in
+ begin match usize_div max_usize 2 with
| Fail -> Fail
- | Return i1 ->
- if capacity <= i1
- then
- begin match usize_mul capacity 2 with
- | Fail -> Fail
- | Return i2 ->
- begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 with
+ | Return n1 ->
+ let (i, i0) = self.hashmap_hash_map_max_load_factor in
+ begin match usize_div n1 i with
+ | Fail -> Fail
+ | Return i1 ->
+ if capacity <= i1
+ then
+ begin match usize_mul capacity 2 with
| Fail -> Fail
- | Return ntable ->
- begin match
- hashmap_hash_map_move_elements_fwd_back t ntable
- self.hashmap_hash_map_slots 0 with
+ | Return i2 ->
+ begin match hashmap_hash_map_new_with_capacity_fwd t i2 i i0 with
| Fail -> Fail
- | Return (ntable0, _) ->
- Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
- (i, i0) ntable0.hashmap_hash_map_max_load
- ntable0.hashmap_hash_map_slots)
+ | Return ntable ->
+ begin match
+ hashmap_hash_map_move_elements_fwd_back t ntable
+ self.hashmap_hash_map_slots 0 with
+ | Fail -> Fail
+ | Return (ntable0, _) ->
+ Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries
+ (i, i0) ntable0.hashmap_hash_map_max_load
+ ntable0.hashmap_hash_map_slots)
+ end
end
end
- end
- else
- Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i, i0)
- self.hashmap_hash_map_max_load self.hashmap_hash_map_slots)
+ else
+ Return (Mkhashmap_hash_map_t self.hashmap_hash_map_num_entries (i,
+ i0) self.hashmap_hash_map_max_load self.hashmap_hash_map_slots)
+ end
end
end
@@ -304,18 +307,11 @@ let hashmap_hash_map_insert_fwd_back
| Return i ->
if i > self0.hashmap_hash_map_max_load
then
- begin match
- hashmap_hash_map_try_resize_fwd_back t (Mkhashmap_hash_map_t
- self0.hashmap_hash_map_num_entries
- self0.hashmap_hash_map_max_load_factor
- self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots) with
+ begin match hashmap_hash_map_try_resize_fwd_back t self0 with
| Fail -> Fail
| Return self1 -> Return self1
end
- else
- Return (Mkhashmap_hash_map_t self0.hashmap_hash_map_num_entries
- self0.hashmap_hash_map_max_load_factor
- self0.hashmap_hash_map_max_load self0.hashmap_hash_map_slots)
+ else Return self0
end
end
diff --git a/tests/hashmap_on_disk/Primitives.fst b/tests/hashmap_on_disk/Primitives.fst
index f73c8c09..fe351f3a 100644
--- a/tests/hashmap_on_disk/Primitives.fst
+++ b/tests/hashmap_on_disk/Primitives.fst
@@ -146,7 +146,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
mk_scalar ty (x * y)
(** Cast an integer from a [src_ty] to a [tgt_ty] *)
-let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
+let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
mk_scalar tgt_ty x
/// The scalar types
diff --git a/tests/misc/External.Funs.fst b/tests/misc/External.Funs.fst
index aafc0cf6..874b739c 100644
--- a/tests/misc/External.Funs.fst
+++ b/tests/misc/External.Funs.fst
@@ -109,8 +109,7 @@ let test_swap_non_zero_fwd (x : u32) (st : state) : result (state & u32) =
| Return (st0, _) ->
begin match swap_back u32 x 0 st with
| Fail -> Fail
- | Return (x0, _) ->
- begin match x0 with | 0 -> Fail | _ -> Return (st0, x0) end
+ | Return (x0, _) -> if x0 = 0 then Fail else Return (st0, x0)
end
end
diff --git a/tests/misc/NoNestedBorrows.fst b/tests/misc/NoNestedBorrows.fst
index 97688191..35d32514 100644
--- a/tests/misc/NoNestedBorrows.fst
+++ b/tests/misc/NoNestedBorrows.fst
@@ -56,10 +56,14 @@ let rem_test_fwd (x : u32) (y : u32) : result u32 =
(** [no_nested_borrows::cast_test] *)
let cast_test_fwd (x : u32) : result i32 =
- begin match scalar_cast I32 x with | Fail -> Fail | Return i -> Return i end
+ begin match scalar_cast U32 I32 x with
+ | Fail -> Fail
+ | Return i -> Return i
+ end
(** [no_nested_borrows::test2] *)
-let test2_fwd : result unit = Return ()
+let test2_fwd : result unit =
+ begin match u32_add 23 44 with | Fail -> Fail | Return _ -> Return () end
(** Unit test for [no_nested_borrows::test2] *)
let _ = assert_norm (test2_fwd = Return ())
@@ -87,7 +91,11 @@ let test3_fwd : result unit =
let _ = assert_norm (test3_fwd = Return ())
(** [no_nested_borrows::test_neg1] *)
-let test_neg1_fwd : result unit = Return ()
+let test_neg1_fwd : result unit =
+ begin match i32_neg 3 with
+ | Fail -> Fail
+ | Return y -> if not (y = -3) then Fail else Return ()
+ end
(** Unit test for [no_nested_borrows::test_neg1] *)
let _ = assert_norm (test_neg1_fwd = Return ())
@@ -222,27 +230,25 @@ and node_elem_t (t : Type0) =
(** [no_nested_borrows::even] *)
let rec even_fwd (x : u32) : result bool =
- begin match x with
- | 0 -> Return true
- | _ ->
+ if x = 0
+ then Return true
+ else
begin match u32_sub x 1 with
| Fail -> Fail
| Return i ->
begin match odd_fwd i with | Fail -> Fail | Return b -> Return b end
end
- end
(** [no_nested_borrows::odd] *)
and odd_fwd (x : u32) : result bool =
- begin match x with
- | 0 -> Return false
- | _ ->
+ if x = 0
+ then Return false
+ else
begin match u32_sub x 1 with
| Fail -> Fail
| Return i ->
begin match even_fwd i with | Fail -> Fail | Return b -> Return b end
end
- end
(** [no_nested_borrows::test_even_odd] *)
let test_even_odd_fwd : result unit =
@@ -291,9 +297,9 @@ let rec list_length_fwd (t : Type0) (l : list_t t) : result u32 =
let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
begin match l with
| ListCons x tl ->
- begin match i with
- | 0 -> Return x
- | _ ->
+ if i = 0
+ then Return x
+ else
begin match u32_sub i 1 with
| Fail -> Fail
| Return i0 ->
@@ -302,7 +308,6 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
| Return x0 -> Return x0
end
end
- end
| ListNil -> Fail
end
@@ -310,9 +315,9 @@ let rec list_nth_shared_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
begin match l with
| ListCons x tl ->
- begin match i with
- | 0 -> Return x
- | _ ->
+ if i = 0
+ then Return x
+ else
begin match u32_sub i 1 with
| Fail -> Fail
| Return i0 ->
@@ -321,7 +326,6 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
| Return x0 -> Return x0
end
end
- end
| ListNil -> Fail
end
@@ -330,9 +334,9 @@ let rec list_nth_mut_back
(t : Type0) (l : list_t t) (i : u32) (ret : t) : result (list_t t) =
begin match l with
| ListCons x tl ->
- begin match i with
- | 0 -> Return (ListCons ret tl)
- | _ ->
+ if i = 0
+ then Return (ListCons ret tl)
+ else
begin match u32_sub i 1 with
| Fail -> Fail
| Return i0 ->
@@ -341,7 +345,6 @@ let rec list_nth_mut_back
| Return tl0 -> Return (ListCons x tl0)
end
end
- end
| ListNil -> Fail
end
diff --git a/tests/misc/Paper.fst b/tests/misc/Paper.fst
index d162519a..424889ef 100644
--- a/tests/misc/Paper.fst
+++ b/tests/misc/Paper.fst
@@ -59,9 +59,9 @@ type list_t (t : Type0) =
let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
begin match l with
| ListCons x tl ->
- begin match i with
- | 0 -> Return x
- | _ ->
+ if i = 0
+ then Return x
+ else
begin match u32_sub i 1 with
| Fail -> Fail
| Return i0 ->
@@ -70,7 +70,6 @@ let rec list_nth_mut_fwd (t : Type0) (l : list_t t) (i : u32) : result t =
| Return x0 -> Return x0
end
end
- end
| ListNil -> Fail
end
@@ -79,9 +78,9 @@ let rec list_nth_mut_back
(t : Type0) (l : list_t t) (i : u32) (ret : t) : result (list_t t) =
begin match l with
| ListCons x tl ->
- begin match i with
- | 0 -> Return (ListCons ret tl)
- | _ ->
+ if i = 0
+ then Return (ListCons ret tl)
+ else
begin match u32_sub i 1 with
| Fail -> Fail
| Return i0 ->
@@ -90,7 +89,6 @@ let rec list_nth_mut_back
| Return tl0 -> Return (ListCons x tl0)
end
end
- end
| ListNil -> Fail
end
diff --git a/tests/misc/Primitives.fst b/tests/misc/Primitives.fst
index f73c8c09..fe351f3a 100644
--- a/tests/misc/Primitives.fst
+++ b/tests/misc/Primitives.fst
@@ -146,7 +146,7 @@ let scalar_mul (#ty : scalar_ty) (x : scalar ty) (y : scalar ty) : result (scala
mk_scalar ty (x * y)
(** Cast an integer from a [src_ty] to a [tgt_ty] *)
-let scalar_cast (#src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
+let scalar_cast (src_ty : scalar_ty) (tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) =
mk_scalar tgt_ty x
/// The scalar types
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 03:37:52 +0000