summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
Diffstat (limited to 'tests')
-rw-r--r--tests/coq/arrays/Arrays.v21
-rw-r--r--tests/coq/betree/BetreeMain_Funs.v8
-rw-r--r--tests/coq/betree/_CoqProject2
-rw-r--r--tests/coq/demo/Demo.v2
-rw-r--r--tests/coq/hashmap/Hashmap_Funs.v4
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v8
-rw-r--r--tests/coq/hashmap_on_disk/_CoqProject2
-rw-r--r--tests/coq/misc/Loops.v39
-rw-r--r--tests/coq/misc/_CoqProject4
-rw-r--r--tests/fstar/arrays/Arrays.Funs.fst17
-rw-r--r--tests/fstar/betree/BetreeMain.Funs.fst6
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Funs.fst6
-rw-r--r--tests/fstar/demo/Demo.fst2
-rw-r--r--tests/fstar/hashmap/Hashmap.Funs.fst3
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst6
-rw-r--r--tests/fstar/misc/Loops.Funs.fst35
-rw-r--r--tests/lean/Arrays.lean28
-rw-r--r--tests/lean/BetreeMain/Funs.lean8
-rw-r--r--tests/lean/Demo/Demo.lean4
-rw-r--r--tests/lean/Hashmap/Funs.lean4
-rw-r--r--tests/lean/HashmapMain/Funs.lean7
-rw-r--r--tests/lean/Loops.lean52
22 files changed, 80 insertions, 188 deletions
diff --git a/tests/coq/arrays/Arrays.v b/tests/coq/arrays/Arrays.v
index 34d163b7..580e72f0 100644
--- a/tests/coq/arrays/Arrays.v
+++ b/tests/coq/arrays/Arrays.v
@@ -30,9 +30,7 @@ Definition array_to_mut_slice_
(T : Type) (s : array T 32%usize) :
result ((slice T) * (slice T -> result (array T 32%usize)))
:=
- p <- array_to_slice_mut T 32%usize s;
- let (s1, to_slice_mut_back) := p in
- Return (s1, to_slice_mut_back)
+ array_to_slice_mut T 32%usize s
.
(** [arrays::array_len]:
@@ -78,9 +76,7 @@ Definition index_mut_array
(T : Type) (s : array T 32%usize) (i : usize) :
result (T * (T -> result (array T 32%usize)))
:=
- p <- array_index_mut_usize T 32%usize s i;
- let (t, index_mut_back) := p in
- Return (t, index_mut_back)
+ array_index_mut_usize T 32%usize s i
.
(** [arrays::index_slice]:
@@ -95,9 +91,7 @@ Definition index_mut_slice
(T : Type) (s : slice T) (i : usize) :
result (T * (T -> result (slice T)))
:=
- p <- slice_index_mut_usize T s i;
- let (t, index_mut_back) := p in
- Return (t, index_mut_back)
+ slice_index_mut_usize T s i
.
(** [arrays::slice_subslice_shared_]:
@@ -136,9 +130,7 @@ Definition array_to_slice_mut_
(x : array u32 32%usize) :
result ((slice u32) * (slice u32 -> result (array u32 32%usize)))
:=
- p <- array_to_slice_mut u32 32%usize x;
- let (s, to_slice_mut_back) := p in
- Return (s, to_slice_mut_back)
+ array_to_slice_mut u32 32%usize x
.
(** [arrays::array_subslice_shared_]:
@@ -381,7 +373,7 @@ Definition take_array_t (a : array AB_t 2%usize) : result unit :=
(** [arrays::non_copyable_array]:
Source: 'src/arrays.rs', lines 229:0-229:27 *)
Definition non_copyable_array : result unit :=
- _ <- take_array_t (mk_array AB_t 2%usize [ AB_A; AB_B ]); Return tt
+ take_array_t (mk_array AB_t 2%usize [ AB_A; AB_B ])
.
(** [arrays::sum]: loop 0:
@@ -548,8 +540,7 @@ Fixpoint iter_mut_slice_loop
| O => Fail_ OutOfFuel
| S n1 =>
if i s< len
- then (
- i1 <- usize_add i 1%usize; _ <- iter_mut_slice_loop n1 len i1; Return tt)
+ then (i1 <- usize_add i 1%usize; iter_mut_slice_loop n1 len i1)
else Return tt
end
.
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index 3863a90f..a0338557 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -27,9 +27,7 @@ Definition betree_store_internal_node
(id : u64) (content : betree_List_t (u64 * betree_Message_t)) (st : state) :
result (state * unit)
:=
- p <- betree_utils_store_internal_node id content st;
- let (st1, _) := p in
- Return (st1, tt)
+ betree_utils_store_internal_node id content st
.
(** [betree_main::betree::load_leaf_node]:
@@ -45,9 +43,7 @@ Definition betree_store_leaf_node
(id : u64) (content : betree_List_t (u64 * u64)) (st : state) :
result (state * unit)
:=
- p <- betree_utils_store_leaf_node id content st;
- let (st1, _) := p in
- Return (st1, tt)
+ betree_utils_store_leaf_node id content st
.
(** [betree_main::betree::fresh_node_id]:
diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject
index 13e4b9c1..b14bed66 100644
--- a/tests/coq/betree/_CoqProject
+++ b/tests/coq/betree/_CoqProject
@@ -3,8 +3,8 @@
-arg -w
-arg all
-BetreeMain_Types.v
BetreeMain_TypesExternal_Template.v
+BetreeMain_Types.v
Primitives.v
BetreeMain_FunsExternal_Template.v
BetreeMain_Funs.v
diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index 48067c02..2fccf6c0 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -127,7 +127,7 @@ Definition list_nth_mut1
(T : Type) (n : nat) (l : CList_t T) (i : u32) :
result (T * (T -> result (CList_t T)))
:=
- p <- list_nth_mut1_loop T n l i; let (t, back_'a) := p in Return (t, back_'a)
+ list_nth_mut1_loop T n l i
.
(** [demo::i32_id]:
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index 0478edbe..ab424e42 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -398,9 +398,7 @@ Definition hashMap_get_mut_in_list
(T : Type) (n : nat) (ls : List_t T) (key : usize) :
result (T * (T -> result (List_t T)))
:=
- p <- hashMap_get_mut_in_list_loop T n ls key;
- let (t, back_'a) := p in
- Return (t, back_'a)
+ hashMap_get_mut_in_list_loop T n ls key
.
(** [hashmap::{hashmap::HashMap<T>}::get_mut]:
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 6a7eeb2d..aff4995f 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -423,9 +423,7 @@ Definition hashmap_HashMap_get_mut_in_list
(T : Type) (n : nat) (ls : hashmap_List_t T) (key : usize) :
result (T * (T -> result (hashmap_List_t T)))
:=
- p <- hashmap_HashMap_get_mut_in_list_loop T n ls key;
- let (t, back_'a) := p in
- Return (t, back_'a)
+ hashmap_HashMap_get_mut_in_list_loop T n ls key
.
(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]:
@@ -585,9 +583,7 @@ Definition insert_on_disk
p <- hashmap_utils_deserialize st;
let (st1, hm) := p in
hm1 <- hashmap_HashMap_insert u64 n hm key value;
- p1 <- hashmap_utils_serialize hm1 st1;
- let (st2, _) := p1 in
- Return (st2, tt)
+ hashmap_utils_serialize hm1 st1
.
(** [hashmap_main::main]:
diff --git a/tests/coq/hashmap_on_disk/_CoqProject b/tests/coq/hashmap_on_disk/_CoqProject
index 41945494..d73541d9 100644
--- a/tests/coq/hashmap_on_disk/_CoqProject
+++ b/tests/coq/hashmap_on_disk/_CoqProject
@@ -4,9 +4,9 @@
-arg all
HashmapMain_Types.v
+HashmapMain_FunsExternal_Template.v
Primitives.v
HashmapMain_Funs.v
HashmapMain_TypesExternal.v
-HashmapMain_FunsExternal_Template.v
HashmapMain_FunsExternal.v
HashmapMain_TypesExternal_Template.v
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index e235b60d..85b54510 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -183,7 +183,7 @@ Definition list_nth_mut_loop
(T : Type) (n : nat) (ls : List_t T) (i : u32) :
result (T * (T -> result (List_t T)))
:=
- p <- list_nth_mut_loop_loop T n ls i; let (t, back) := p in Return (t, back)
+ list_nth_mut_loop_loop T n ls i
.
(** [loops::list_nth_shared_loop]: loop 0:
@@ -400,9 +400,7 @@ Definition list_nth_mut_loop_pair
(T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
result ((T * T) * (T -> result (List_t T)) * (T -> result (List_t T)))
:=
- t <- list_nth_mut_loop_pair_loop T n ls0 ls1 i;
- let '(p, back_'a, back_'b) := t in
- Return (p, back_'a, back_'b)
+ list_nth_mut_loop_pair_loop T n ls0 ls1 i
.
(** [loops::list_nth_shared_loop_pair]: loop 0:
@@ -481,9 +479,7 @@ Definition list_nth_mut_loop_pair_merge
(T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
result ((T * T) * ((T * T) -> result ((List_t T) * (List_t T))))
:=
- p <- list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i;
- let (p1, back_'a) := p in
- Return (p1, back_'a)
+ list_nth_mut_loop_pair_merge_loop T n ls0 ls1 i
.
(** [loops::list_nth_shared_loop_pair_merge]: loop 0:
@@ -557,9 +553,7 @@ Definition list_nth_mut_shared_loop_pair
(T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
result ((T * T) * (T -> result (List_t T)))
:=
- p <- list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i;
- let (p1, back_'a) := p in
- Return (p1, back_'a)
+ list_nth_mut_shared_loop_pair_loop T n ls0 ls1 i
.
(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
@@ -599,9 +593,7 @@ Definition list_nth_mut_shared_loop_pair_merge
(T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
result ((T * T) * (T -> result (List_t T)))
:=
- p <- list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i;
- let (p1, back_'a) := p in
- Return (p1, back_'a)
+ list_nth_mut_shared_loop_pair_merge_loop T n ls0 ls1 i
.
(** [loops::list_nth_shared_mut_loop_pair]: loop 0:
@@ -641,9 +633,7 @@ Definition list_nth_shared_mut_loop_pair
(T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
result ((T * T) * (T -> result (List_t T)))
:=
- p <- list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i;
- let (p1, back_'b) := p in
- Return (p1, back_'b)
+ list_nth_shared_mut_loop_pair_loop T n ls0 ls1 i
.
(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
@@ -683,9 +673,7 @@ Definition list_nth_shared_mut_loop_pair_merge
(T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
result ((T * T) * (T -> result (List_t T)))
:=
- p <- list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i;
- let (p1, back_'a) := p in
- Return (p1, back_'a)
+ list_nth_shared_mut_loop_pair_merge_loop T n ls0 ls1 i
.
(** [loops::ignore_input_mut_borrow]: loop 0:
@@ -695,8 +683,7 @@ Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
| O => Fail_ OutOfFuel
| S n1 =>
if i s> 0%u32
- then (
- i1 <- u32_sub i 1%u32; _ <- ignore_input_mut_borrow_loop n1 i1; Return tt)
+ then (i1 <- u32_sub i 1%u32; ignore_input_mut_borrow_loop n1 i1)
else Return tt
end
.
@@ -715,10 +702,7 @@ Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
| O => Fail_ OutOfFuel
| S n1 =>
if i s> 0%u32
- then (
- i1 <- u32_sub i 1%u32;
- _ <- incr_ignore_input_mut_borrow_loop n1 i1;
- Return tt)
+ then (i1 <- u32_sub i 1%u32; incr_ignore_input_mut_borrow_loop n1 i1)
else Return tt
end
.
@@ -737,10 +721,7 @@ Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit :=
| O => Fail_ OutOfFuel
| S n1 =>
if i s> 0%u32
- then (
- i1 <- u32_sub i 1%u32;
- _ <- ignore_input_shared_borrow_loop n1 i1;
- Return tt)
+ then (i1 <- u32_sub i 1%u32; ignore_input_shared_borrow_loop n1 i1)
else Return tt
end
.
diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject
index 869cdb4d..308de4f4 100644
--- a/tests/coq/misc/_CoqProject
+++ b/tests/coq/misc/_CoqProject
@@ -3,6 +3,7 @@
-arg -w
-arg all
+External_FunsExternal_Template.v
Loops.v
External_Types.v
Primitives.v
@@ -10,9 +11,8 @@ External_Funs.v
External_TypesExternal.v
Constants.v
PoloniusList.v
-Paper.v
NoNestedBorrows.v
External_FunsExternal.v
Bitwise.v
External_TypesExternal_Template.v
-External_FunsExternal_Template.v
+Paper.v
diff --git a/tests/fstar/arrays/Arrays.Funs.fst b/tests/fstar/arrays/Arrays.Funs.fst
index cf0f4f8b..15c82e93 100644
--- a/tests/fstar/arrays/Arrays.Funs.fst
+++ b/tests/fstar/arrays/Arrays.Funs.fst
@@ -23,8 +23,7 @@ let array_to_mut_slice_
(t : Type0) (s : array t 32) :
result ((slice t) & (slice t -> result (array t 32)))
=
- let* (s1, to_slice_mut_back) = array_to_slice_mut t 32 s in
- Return (s1, to_slice_mut_back)
+ array_to_slice_mut t 32 s
(** [arrays::array_len]:
Source: 'src/arrays.rs', lines 25:0-25:40 *)
@@ -62,8 +61,7 @@ let index_mut_array
(t : Type0) (s : array t 32) (i : usize) :
result (t & (t -> result (array t 32)))
=
- let* (x, index_mut_back) = array_index_mut_usize t 32 s i in
- Return (x, index_mut_back)
+ array_index_mut_usize t 32 s i
(** [arrays::index_slice]:
Source: 'src/arrays.rs', lines 56:0-56:46 *)
@@ -76,8 +74,7 @@ let index_mut_slice
(t : Type0) (s : slice t) (i : usize) :
result (t & (t -> result (slice t)))
=
- let* (x, index_mut_back) = slice_index_mut_usize t s i in
- Return (x, index_mut_back)
+ slice_index_mut_usize t s i
(** [arrays::slice_subslice_shared_]:
Source: 'src/arrays.rs', lines 64:0-64:70 *)
@@ -110,8 +107,7 @@ let array_to_slice_mut_
(x : array u32 32) :
result ((slice u32) & (slice u32 -> result (array u32 32)))
=
- let* (s, to_slice_mut_back) = array_to_slice_mut u32 32 x in
- Return (s, to_slice_mut_back)
+ array_to_slice_mut u32 32 x
(** [arrays::array_subslice_shared_]:
Source: 'src/arrays.rs', lines 80:0-80:74 *)
@@ -308,7 +304,7 @@ let take_array_t (a : array aB_t 2) : result unit =
(** [arrays::non_copyable_array]:
Source: 'src/arrays.rs', lines 229:0-229:27 *)
let non_copyable_array : result unit =
- let* _ = take_array_t (mk_array aB_t 2 [ AB_A; AB_B ]) in Return ()
+ take_array_t (mk_array aB_t 2 [ AB_A; AB_B ])
(** [arrays::sum]: loop 0:
Source: 'src/arrays.rs', lines 242:0-250:1 *)
@@ -444,8 +440,7 @@ let rec iter_mut_slice_loop
Tot (result unit) (decreases (iter_mut_slice_loop_decreases len i))
=
if i < len
- then
- let* i1 = usize_add i 1 in let* _ = iter_mut_slice_loop len i1 in Return ()
+ then let* i1 = usize_add i 1 in iter_mut_slice_loop len i1
else Return ()
(** [arrays::iter_mut_slice]:
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index ec042fb3..74044961 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -22,8 +22,7 @@ let betree_store_internal_node
(id : u64) (content : betree_List_t (u64 & betree_Message_t)) (st : state) :
result (state & unit)
=
- let* (st1, _) = betree_utils_store_internal_node id content st in
- Return (st1, ())
+ betree_utils_store_internal_node id content st
(** [betree_main::betree::load_leaf_node]:
Source: 'src/betree.rs', lines 46:0-46:44 *)
@@ -37,8 +36,7 @@ let betree_store_leaf_node
(id : u64) (content : betree_List_t (u64 & u64)) (st : state) :
result (state & unit)
=
- let* (st1, _) = betree_utils_store_leaf_node id content st in
- Return (st1, ())
+ betree_utils_store_leaf_node id content st
(** [betree_main::betree::fresh_node_id]:
Source: 'src/betree.rs', lines 55:0-55:48 *)
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index ec042fb3..74044961 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -22,8 +22,7 @@ let betree_store_internal_node
(id : u64) (content : betree_List_t (u64 & betree_Message_t)) (st : state) :
result (state & unit)
=
- let* (st1, _) = betree_utils_store_internal_node id content st in
- Return (st1, ())
+ betree_utils_store_internal_node id content st
(** [betree_main::betree::load_leaf_node]:
Source: 'src/betree.rs', lines 46:0-46:44 *)
@@ -37,8 +36,7 @@ let betree_store_leaf_node
(id : u64) (content : betree_List_t (u64 & u64)) (st : state) :
result (state & unit)
=
- let* (st1, _) = betree_utils_store_leaf_node id content st in
- Return (st1, ())
+ betree_utils_store_leaf_node id content st
(** [betree_main::betree::fresh_node_id]:
Source: 'src/betree.rs', lines 55:0-55:48 *)
diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
index 5651b80f..4ad7cb65 100644
--- a/tests/fstar/demo/Demo.fst
+++ b/tests/fstar/demo/Demo.fst
@@ -109,7 +109,7 @@ let list_nth_mut1
(t : Type0) (n : nat) (l : cList_t t) (i : u32) :
result (t & (t -> result (cList_t t)))
=
- let* (x, back_'a) = list_nth_mut1_loop t n l i in Return (x, back_'a)
+ list_nth_mut1_loop t n l i
(** [demo::i32_id]:
Source: 'src/demo.rs', lines 80:0-80:28 *)
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index 447f9b49..7ca8b9c1 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -308,8 +308,7 @@ let hashMap_get_mut_in_list
(t : Type0) (ls : list_t t) (key : usize) :
result (t & (t -> result (list_t t)))
=
- let* (x, back_'a) = hashMap_get_mut_in_list_loop t ls key in
- Return (x, back_'a)
+ hashMap_get_mut_in_list_loop t ls key
(** [hashmap::{hashmap::HashMap<T>}::get_mut]:
Source: 'src/hashmap.rs', lines 257:4-257:67 *)
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index b16dcada..9b5baaeb 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -324,8 +324,7 @@ let hashmap_HashMap_get_mut_in_list
(t : Type0) (ls : hashmap_List_t t) (key : usize) :
result (t & (t -> result (hashmap_List_t t)))
=
- let* (x, back_'a) = hashmap_HashMap_get_mut_in_list_loop t ls key in
- Return (x, back_'a)
+ hashmap_HashMap_get_mut_in_list_loop t ls key
(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]:
Source: 'src/hashmap.rs', lines 257:4-257:67 *)
@@ -446,8 +445,7 @@ let insert_on_disk
(key : usize) (value : u64) (st : state) : result (state & unit) =
let* (st1, hm) = hashmap_utils_deserialize st in
let* hm1 = hashmap_HashMap_insert u64 hm key value in
- let* (st2, _) = hashmap_utils_serialize hm1 st1 in
- Return (st2, ())
+ hashmap_utils_serialize hm1 st1
(** [hashmap_main::main]:
Source: 'src/hashmap_main.rs', lines 16:0-16:13 *)
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index 5f24fe7a..c87f693b 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -140,7 +140,7 @@ let list_nth_mut_loop
(t : Type0) (ls : list_t t) (i : u32) :
result (t & (t -> result (list_t t)))
=
- let* (x, back) = list_nth_mut_loop_loop t ls i in Return (x, back)
+ list_nth_mut_loop_loop t ls i
(** [loops::list_nth_shared_loop]: loop 0:
Source: 'src/loops.rs', lines 101:0-111:1 *)
@@ -312,8 +312,7 @@ let list_nth_mut_loop_pair
(t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
result ((t & t) & (t -> result (list_t t)) & (t -> result (list_t t)))
=
- let* (p, back_'a, back_'b) = list_nth_mut_loop_pair_loop t ls0 ls1 i in
- Return (p, back_'a, back_'b)
+ list_nth_mut_loop_pair_loop t ls0 ls1 i
(** [loops::list_nth_shared_loop_pair]: loop 0:
Source: 'src/loops.rs', lines 208:0-229:1 *)
@@ -376,8 +375,7 @@ let list_nth_mut_loop_pair_merge
(t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
result ((t & t) & ((t & t) -> result ((list_t t) & (list_t t))))
=
- let* (p, back_'a) = list_nth_mut_loop_pair_merge_loop t ls0 ls1 i in
- Return (p, back_'a)
+ list_nth_mut_loop_pair_merge_loop t ls0 ls1 i
(** [loops::list_nth_shared_loop_pair_merge]: loop 0:
Source: 'src/loops.rs', lines 251:0-266:1 *)
@@ -438,8 +436,7 @@ let list_nth_mut_shared_loop_pair
(t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
result ((t & t) & (t -> result (list_t t)))
=
- let* (p, back_'a) = list_nth_mut_shared_loop_pair_loop t ls0 ls1 i in
- Return (p, back_'a)
+ list_nth_mut_shared_loop_pair_loop t ls0 ls1 i
(** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
Source: 'src/loops.rs', lines 288:0-303:1 *)
@@ -474,8 +471,7 @@ let list_nth_mut_shared_loop_pair_merge
(t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
result ((t & t) & (t -> result (list_t t)))
=
- let* (p, back_'a) = list_nth_mut_shared_loop_pair_merge_loop t ls0 ls1 i in
- Return (p, back_'a)
+ list_nth_mut_shared_loop_pair_merge_loop t ls0 ls1 i
(** [loops::list_nth_shared_mut_loop_pair]: loop 0:
Source: 'src/loops.rs', lines 307:0-322:1 *)
@@ -509,8 +505,7 @@ let list_nth_shared_mut_loop_pair
(t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
result ((t & t) & (t -> result (list_t t)))
=
- let* (p, back_'b) = list_nth_shared_mut_loop_pair_loop t ls0 ls1 i in
- Return (p, back_'b)
+ list_nth_shared_mut_loop_pair_loop t ls0 ls1 i
(** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
Source: 'src/loops.rs', lines 326:0-341:1 *)
@@ -545,8 +540,7 @@ let list_nth_shared_mut_loop_pair_merge
(t : Type0) (ls0 : list_t t) (ls1 : list_t t) (i : u32) :
result ((t & t) & (t -> result (list_t t)))
=
- let* (p, back_'a) = list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i in
- Return (p, back_'a)
+ list_nth_shared_mut_loop_pair_merge_loop t ls0 ls1 i
(** [loops::ignore_input_mut_borrow]: loop 0:
Source: 'src/loops.rs', lines 345:0-349:1 *)
@@ -555,10 +549,7 @@ let rec ignore_input_mut_borrow_loop
Tot (result unit) (decreases (ignore_input_mut_borrow_loop_decreases i))
=
if i > 0
- then
- let* i1 = u32_sub i 1 in
- let* _ = ignore_input_mut_borrow_loop i1 in
- Return ()
+ then let* i1 = u32_sub i 1 in ignore_input_mut_borrow_loop i1
else Return ()
(** [loops::ignore_input_mut_borrow]:
@@ -573,10 +564,7 @@ let rec incr_ignore_input_mut_borrow_loop
Tot (result unit) (decreases (incr_ignore_input_mut_borrow_loop_decreases i))
=
if i > 0
- then
- let* i1 = u32_sub i 1 in
- let* _ = incr_ignore_input_mut_borrow_loop i1 in
- Return ()
+ then let* i1 = u32_sub i 1 in incr_ignore_input_mut_borrow_loop i1
else Return ()
(** [loops::incr_ignore_input_mut_borrow]:
@@ -593,10 +581,7 @@ let rec ignore_input_shared_borrow_loop
Tot (result unit) (decreases (ignore_input_shared_borrow_loop_decreases i))
=
if i > 0
- then
- let* i1 = u32_sub i 1 in
- let* _ = ignore_input_shared_borrow_loop i1 in
- Return ()
+ then let* i1 = u32_sub i 1 in ignore_input_shared_borrow_loop i1
else Return ()
(** [loops::ignore_input_shared_borrow]:
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index d637ee13..cd1b6544 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -28,9 +28,7 @@ def array_to_mut_slice_
(T : Type) (s : Array T 32#usize) :
Result ((Slice T) × (Slice T → Result (Array T 32#usize)))
:=
- do
- let (s1, to_slice_mut_back) ← Array.to_slice_mut T 32#usize s
- Result.ret (s1, to_slice_mut_back)
+ Array.to_slice_mut T 32#usize s
/- [arrays::array_len]:
Source: 'src/arrays.rs', lines 25:0-25:40 -/
@@ -76,9 +74,7 @@ def index_mut_array
(T : Type) (s : Array T 32#usize) (i : Usize) :
Result (T × (T → Result (Array T 32#usize)))
:=
- do
- let (t, index_mut_back) ← Array.index_mut_usize T 32#usize s i
- Result.ret (t, index_mut_back)
+ Array.index_mut_usize T 32#usize s i
/- [arrays::index_slice]:
Source: 'src/arrays.rs', lines 56:0-56:46 -/
@@ -91,9 +87,7 @@ def index_mut_slice
(T : Type) (s : Slice T) (i : Usize) :
Result (T × (T → Result (Slice T)))
:=
- do
- let (t, index_mut_back) ← Slice.index_mut_usize T s i
- Result.ret (t, index_mut_back)
+ Slice.index_mut_usize T s i
/- [arrays::slice_subslice_shared_]:
Source: 'src/arrays.rs', lines 64:0-64:70 -/
@@ -127,9 +121,7 @@ def array_to_slice_mut_
(x : Array U32 32#usize) :
Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize)))
:=
- do
- let (s, to_slice_mut_back) ← Array.to_slice_mut U32 32#usize x
- Result.ret (s, to_slice_mut_back)
+ Array.to_slice_mut U32 32#usize x
/- [arrays::array_subslice_shared_]:
Source: 'src/arrays.rs', lines 80:0-80:74 -/
@@ -354,9 +346,7 @@ def take_array_t (a : Array AB 2#usize) : Result Unit :=
/- [arrays::non_copyable_array]:
Source: 'src/arrays.rs', lines 229:0-229:27 -/
def non_copyable_array : Result Unit :=
- do
- let _ ← take_array_t (Array.make AB 2#usize [ AB.A, AB.B ])
- Result.ret ()
+ take_array_t (Array.make AB 2#usize [ AB.A, AB.B ])
/- [arrays::sum]: loop 0:
Source: 'src/arrays.rs', lines 242:0-250:1 -/
@@ -496,11 +486,9 @@ def zero_slice (a : Slice U8) : Result (Slice U8) :=
Source: 'src/arrays.rs', lines 312:0-318:1 -/
divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit :=
if i < len
- then
- do
- let i1 ← i + 1#usize
- let _ ← iter_mut_slice_loop len i1
- Result.ret ()
+ then do
+ let i1 ← i + 1#usize
+ iter_mut_slice_loop len i1
else Result.ret ()
/- [arrays::iter_mut_slice]:
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index d6449b37..bd5921a8 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -21,9 +21,7 @@ def betree.store_internal_node
(id : U64) (content : betree.List (U64 × betree.Message)) (st : State) :
Result (State × Unit)
:=
- do
- let (st1, _) ← betree_utils.store_internal_node id content st
- Result.ret (st1, ())
+ betree_utils.store_internal_node id content st
/- [betree_main::betree::load_leaf_node]:
Source: 'src/betree.rs', lines 46:0-46:44 -/
@@ -37,9 +35,7 @@ def betree.store_leaf_node
(id : U64) (content : betree.List (U64 × U64)) (st : State) :
Result (State × Unit)
:=
- do
- let (st1, _) ← betree_utils.store_leaf_node id content st
- Result.ret (st1, ())
+ betree_utils.store_leaf_node id content st
/- [betree_main::betree::fresh_node_id]:
Source: 'src/betree.rs', lines 55:0-55:48 -/
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index f38b5cd3..09032820 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -116,9 +116,7 @@ def list_nth_mut1
(T : Type) (l : CList T) (i : U32) :
Result (T × (T → Result (CList T)))
:=
- do
- let (t, back_'a) ← list_nth_mut1_loop T l i
- Result.ret (t, back_'a)
+ list_nth_mut1_loop T l i
/- [demo::i32_id]:
Source: 'src/demo.rs', lines 80:0-80:28 -/
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index f0706725..d33b6571 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -311,9 +311,7 @@ def HashMap.get_mut_in_list
(T : Type) (ls : List T) (key : Usize) :
Result (T × (T → Result (List T)))
:=
- do
- let (t, back_'a) ← HashMap.get_mut_in_list_loop T ls key
- Result.ret (t, back_'a)
+ HashMap.get_mut_in_list_loop T ls key
/- [hashmap::{hashmap::HashMap<T>}::get_mut]:
Source: 'src/hashmap.rs', lines 257:4-257:67 -/
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index 31441b4a..8a277700 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -326,9 +326,7 @@ def hashmap.HashMap.get_mut_in_list
(T : Type) (ls : hashmap.List T) (key : Usize) :
Result (T × (T → Result (hashmap.List T)))
:=
- do
- let (t, back_'a) ← hashmap.HashMap.get_mut_in_list_loop T ls key
- Result.ret (t, back_'a)
+ hashmap.HashMap.get_mut_in_list_loop T ls key
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]:
Source: 'src/hashmap.rs', lines 257:4-257:67 -/
@@ -460,8 +458,7 @@ def insert_on_disk
do
let (st1, hm) ← hashmap_utils.deserialize st
let hm1 ← hashmap.HashMap.insert U64 hm key value
- let (st2, _) ← hashmap_utils.serialize hm1 st1
- Result.ret (st2, ())
+ hashmap_utils.serialize hm1 st1
/- [hashmap_main::main]:
Source: 'src/hashmap_main.rs', lines 16:0-16:13 -/
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index 433ca8f0..3f075347 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -138,9 +138,7 @@ divergent def list_nth_mut_loop_loop
Source: 'src/loops.rs', lines 88:0-88:71 -/
def list_nth_mut_loop
(T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
- do
- let (t, back) ← list_nth_mut_loop_loop T ls i
- Result.ret (t, back)
+ list_nth_mut_loop_loop T ls i
/- [loops::list_nth_shared_loop]: loop 0:
Source: 'src/loops.rs', lines 101:0-111:1 -/
@@ -322,9 +320,7 @@ def list_nth_mut_loop_pair
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)) × (T → Result (List T)))
:=
- do
- let (p, back_'a, back_'b) ← list_nth_mut_loop_pair_loop T ls0 ls1 i
- Result.ret (p, back_'a, back_'b)
+ list_nth_mut_loop_pair_loop T ls0 ls1 i
/- [loops::list_nth_shared_loop_pair]: loop 0:
Source: 'src/loops.rs', lines 208:0-229:1 -/
@@ -384,9 +380,7 @@ def list_nth_mut_loop_pair_merge
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × ((T × T) → Result ((List T) × (List T))))
:=
- do
- let (p, back_'a) ← list_nth_mut_loop_pair_merge_loop T ls0 ls1 i
- Result.ret (p, back_'a)
+ list_nth_mut_loop_pair_merge_loop T ls0 ls1 i
/- [loops::list_nth_shared_loop_pair_merge]: loop 0:
Source: 'src/loops.rs', lines 251:0-266:1 -/
@@ -443,9 +437,7 @@ def list_nth_mut_shared_loop_pair
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)))
:=
- do
- let (p, back_'a) ← list_nth_mut_shared_loop_pair_loop T ls0 ls1 i
- Result.ret (p, back_'a)
+ list_nth_mut_shared_loop_pair_loop T ls0 ls1 i
/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
Source: 'src/loops.rs', lines 288:0-303:1 -/
@@ -480,9 +472,7 @@ def list_nth_mut_shared_loop_pair_merge
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)))
:=
- do
- let (p, back_'a) ← list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i
- Result.ret (p, back_'a)
+ list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i
/- [loops::list_nth_shared_mut_loop_pair]: loop 0:
Source: 'src/loops.rs', lines 307:0-322:1 -/
@@ -516,9 +506,7 @@ def list_nth_shared_mut_loop_pair
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)))
:=
- do
- let (p, back_'b) ← list_nth_shared_mut_loop_pair_loop T ls0 ls1 i
- Result.ret (p, back_'b)
+ list_nth_shared_mut_loop_pair_loop T ls0 ls1 i
/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
Source: 'src/loops.rs', lines 326:0-341:1 -/
@@ -553,19 +541,15 @@ def list_nth_shared_mut_loop_pair_merge
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)))
:=
- do
- let (p, back_'a) ← list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i
- Result.ret (p, back_'a)
+ list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i
/- [loops::ignore_input_mut_borrow]: loop 0:
Source: 'src/loops.rs', lines 345:0-349:1 -/
divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
if i > 0#u32
- then
- do
- let i1 ← i - 1#u32
- let _ ← ignore_input_mut_borrow_loop i1
- Result.ret ()
+ then do
+ let i1 ← i - 1#u32
+ ignore_input_mut_borrow_loop i1
else Result.ret ()
/- [loops::ignore_input_mut_borrow]:
@@ -579,11 +563,9 @@ def ignore_input_mut_borrow (_a : U32) (i : U32) : Result U32 :=
Source: 'src/loops.rs', lines 353:0-358:1 -/
divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
if i > 0#u32
- then
- do
- let i1 ← i - 1#u32
- let _ ← incr_ignore_input_mut_borrow_loop i1
- Result.ret ()
+ then do
+ let i1 ← i - 1#u32
+ incr_ignore_input_mut_borrow_loop i1
else Result.ret ()
/- [loops::incr_ignore_input_mut_borrow]:
@@ -598,11 +580,9 @@ def incr_ignore_input_mut_borrow (a : U32) (i : U32) : Result U32 :=
Source: 'src/loops.rs', lines 362:0-366:1 -/
divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit :=
if i > 0#u32
- then
- do
- let i1 ← i - 1#u32
- let _ ← ignore_input_shared_borrow_loop i1
- Result.ret ()
+ then do
+ let i1 ← i - 1#u32
+ ignore_input_shared_borrow_loop i1
else Result.ret ()
/- [loops::ignore_input_shared_borrow]:
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 02:29:40 +0000