summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorSon HO2024-04-04 14:31:03 +0200
committerGitHub2024-04-04 14:31:03 +0200
commitb4f5719a10427dfc168f1210b05397599e761f9a (patch)
tree55906070f19df2a3185250df2aef36f47669842a /tests
parent88cb18c614819f4abba1e0dfdb80c455d334d595 (diff)
parent0c3be2a82205d2737546c7ce8b15b6ad07f34095 (diff)
Merge pull request #111 from AeneasVerif/son/names
Improve the names used for the variables in the generated code
Diffstat (limited to 'tests')
-rw-r--r--tests/coq/betree/BetreeMain_Funs.v12
-rw-r--r--tests/coq/betree/BetreeMain_FunsExternal_Template.v3
-rw-r--r--tests/coq/demo/Demo.v28
-rw-r--r--tests/coq/hashmap/Hashmap_Funs.v30
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v29
-rw-r--r--tests/coq/misc/External_Funs.v4
-rw-r--r--tests/coq/misc/External_FunsExternal_Template.v9
-rw-r--r--tests/coq/misc/External_TypesExternal_Template.v3
-rw-r--r--tests/coq/misc/Loops.v78
-rw-r--r--tests/coq/misc/NoNestedBorrows.v12
-rw-r--r--tests/coq/misc/Paper.v12
-rw-r--r--tests/coq/misc/PoloniusList.v4
-rw-r--r--tests/coq/traits/Traits.v3
-rw-r--r--tests/fstar/betree/BetreeMain.Funs.fst12
-rw-r--r--tests/fstar/betree/BetreeMain.FunsExternal.fsti3
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.Funs.fst12
-rw-r--r--tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti3
-rw-r--r--tests/fstar/demo/Demo.fst26
-rw-r--r--tests/fstar/hashmap/Hashmap.Funs.fst29
-rw-r--r--tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst29
-rw-r--r--tests/fstar/misc/External.Funs.fst4
-rw-r--r--tests/fstar/misc/External.FunsExternal.fsti9
-rw-r--r--tests/fstar/misc/External.TypesExternal.fsti3
-rw-r--r--tests/fstar/misc/Loops.Funs.fst83
-rw-r--r--tests/fstar/misc/NoNestedBorrows.fst11
-rw-r--r--tests/fstar/misc/Paper.fst11
-rw-r--r--tests/fstar/misc/PoloniusList.fst4
-rw-r--r--tests/fstar/traits/Traits.fst3
-rw-r--r--tests/lean/BetreeMain/Funs.lean12
-rw-r--r--tests/lean/BetreeMain/FunsExternal_Template.lean3
-rw-r--r--tests/lean/Demo/Demo.lean32
-rw-r--r--tests/lean/External/Funs.lean4
-rw-r--r--tests/lean/External/FunsExternal_Template.lean9
-rw-r--r--tests/lean/External/TypesExternal_Template.lean3
-rw-r--r--tests/lean/Hashmap/Funs.lean28
-rw-r--r--tests/lean/HashmapMain/Funs.lean28
-rw-r--r--tests/lean/Loops.lean80
-rw-r--r--tests/lean/NoNestedBorrows.lean16
-rw-r--r--tests/lean/Paper.lean16
-rw-r--r--tests/lean/PoloniusList.lean4
-rw-r--r--tests/lean/Traits.lean3
41 files changed, 358 insertions, 349 deletions
diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v
index c2cca26d..9256b149 100644
--- a/tests/coq/betree/BetreeMain_Funs.v
+++ b/tests/coq/betree/BetreeMain_Funs.v
@@ -240,11 +240,11 @@ Fixpoint betree_Node_lookup_first_message_for_key
else (
p <- betree_Node_lookup_first_message_for_key n1 key next_msgs;
let (l, lookup_first_message_for_key_back) := p in
- let back_'a :=
+ let back :=
fun (ret : betree_List_t (u64 * betree_Message_t)) =>
next_msgs1 <- lookup_first_message_for_key_back ret;
Return (Betree_List_Cons (i, m) next_msgs1) in
- Return (l, back_'a))
+ Return (l, back))
| Betree_List_Nil => Return (Betree_List_Nil, Return)
end
end
@@ -440,11 +440,11 @@ Fixpoint betree_Node_lookup_first_message_after_key
then (
p1 <- betree_Node_lookup_first_message_after_key n1 key next_msgs;
let (l, lookup_first_message_after_key_back) := p1 in
- let back_'a :=
+ let back :=
fun (ret : betree_List_t (u64 * betree_Message_t)) =>
next_msgs1 <- lookup_first_message_after_key_back ret;
Return (Betree_List_Cons (k, m) next_msgs1) in
- Return (l, back_'a))
+ Return (l, back))
else Return (Betree_List_Cons (k, m) next_msgs, Return)
| Betree_List_Nil => Return (Betree_List_Nil, Return)
end
@@ -550,11 +550,11 @@ Fixpoint betree_Node_lookup_mut_in_bindings
else (
p <- betree_Node_lookup_mut_in_bindings n1 key tl;
let (l, lookup_mut_in_bindings_back) := p in
- let back_'a :=
+ let back :=
fun (ret : betree_List_t (u64 * u64)) =>
tl1 <- lookup_mut_in_bindings_back ret;
Return (Betree_List_Cons (i, i1) tl1) in
- Return (l, back_'a))
+ Return (l, back))
| Betree_List_Nil => Return (Betree_List_Nil, Return)
end
end
diff --git a/tests/coq/betree/BetreeMain_FunsExternal_Template.v b/tests/coq/betree/BetreeMain_FunsExternal_Template.v
index a9969448..1367bac2 100644
--- a/tests/coq/betree/BetreeMain_FunsExternal_Template.v
+++ b/tests/coq/betree/BetreeMain_FunsExternal_Template.v
@@ -38,7 +38,8 @@ Axiom betree_utils_store_leaf_node
.
(** [core::option::{core::option::Option<T>}::unwrap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+ Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
Axiom core_option_Option_unwrap :
forall(T : Type), option T -> state -> result (state * T)
.
diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index d5a6e535..abec8e88 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -13,8 +13,8 @@ Module Demo.
Definition choose
(T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) :=
if b
- then let back_'a := fun (ret : T) => Return (ret, y) in Return (x, back_'a)
- else let back_'a := fun (ret : T) => Return (x, ret) in Return (y, back_'a)
+ then let back := fun (ret : T) => Return (ret, y) in Return (x, back)
+ else let back := fun (ret : T) => Return (x, ret) in Return (y, back)
.
(** [demo::mul2_add1]:
@@ -79,16 +79,16 @@ Fixpoint list_nth_mut
| CList_CCons x tl =>
if i s= 0%u32
then
- let back_'a := fun (ret : T) => Return (CList_CCons ret tl) in
- Return (x, back_'a)
+ let back := fun (ret : T) => Return (CList_CCons ret tl) in
+ Return (x, back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut T n1 tl i1;
let (t, list_nth_mut_back) := p in
- let back_'a :=
+ let back :=
fun (ret : T) =>
tl1 <- list_nth_mut_back ret; Return (CList_CCons x tl1) in
- Return (t, back_'a))
+ Return (t, back))
| CList_CNil => Fail_ Failure
end
end
@@ -107,15 +107,15 @@ Fixpoint list_nth_mut1_loop
| CList_CCons x tl =>
if i s= 0%u32
then
- let back_'a := fun (ret : T) => Return (CList_CCons ret tl) in
- Return (x, back_'a)
+ let back := fun (ret : T) => Return (CList_CCons ret tl) in
+ Return (x, back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut1_loop T n1 tl i1;
- let (t, back_'a) := p in
- let back_'a1 :=
- fun (ret : T) => tl1 <- back_'a ret; Return (CList_CCons x tl1) in
- Return (t, back_'a1))
+ let (t, back) := p in
+ let back1 :=
+ fun (ret : T) => tl1 <- back ret; Return (CList_CCons x tl1) in
+ Return (t, back1))
| CList_CNil => Fail_ Failure
end
end
@@ -155,10 +155,10 @@ Fixpoint list_tail
| CList_CCons t tl =>
p <- list_tail T n1 tl;
let (c, list_tail_back) := p in
- let back_'a :=
+ let back :=
fun (ret : CList_t T) =>
tl1 <- list_tail_back ret; Return (CList_CCons t tl1) in
- Return (c, back_'a)
+ Return (c, back)
| CList_CNil => Return (CList_CNil, Return)
end
end
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index d709a8d5..c0cde78d 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -94,13 +94,13 @@ Fixpoint hashMap_clear_loop
Source: 'src/hashmap.rs', lines 80:4-80:27 *)
Definition hashMap_clear
(T : Type) (n : nat) (self : HashMap_t T) : result (HashMap_t T) :=
- back <- hashMap_clear_loop T n self.(hashMap_slots) 0%usize;
+ hm <- hashMap_clear_loop T n self.(hashMap_slots) 0%usize;
Return
{|
hashMap_num_entries := 0%usize;
hashMap_max_load_factor := self.(hashMap_max_load_factor);
hashMap_max_load := self.(hashMap_max_load);
- hashMap_slots := back
+ hashMap_slots := hm
|}
.
@@ -125,8 +125,8 @@ Fixpoint hashMap_insert_in_list_loop
then Return (false, List_Cons ckey value tl)
else (
p <- hashMap_insert_in_list_loop T n1 key value tl;
- let (b, back) := p in
- Return (b, List_Cons ckey cvalue back))
+ let (b, tl1) := p in
+ Return (b, List_Cons ckey cvalue tl1))
| List_Nil => Return (true, List_Cons key value List_Nil)
end
end
@@ -376,15 +376,15 @@ Fixpoint hashMap_get_mut_in_list_loop
| List_Cons ckey cvalue tl =>
if ckey s= key
then
- let back_'a := fun (ret : T) => Return (List_Cons ckey ret tl) in
- Return (cvalue, back_'a)
+ let back := fun (ret : T) => Return (List_Cons ckey ret tl) in
+ Return (cvalue, back)
else (
p <- hashMap_get_mut_in_list_loop T n1 tl key;
- let (t, back_'a) := p in
- let back_'a1 :=
- fun (ret : T) =>
- tl1 <- back_'a ret; Return (List_Cons ckey cvalue tl1) in
- Return (t, back_'a1))
+ let (t, back) := p in
+ let back1 :=
+ fun (ret : T) => tl1 <- back ret; Return (List_Cons ckey cvalue tl1)
+ in
+ Return (t, back1))
| List_Nil => Fail_ Failure
end
end
@@ -415,7 +415,7 @@ Definition hashMap_get_mut
let (l, index_mut_back) := p in
p1 <- hashMap_get_mut_in_list T n l key;
let (t, get_mut_in_list_back) := p1 in
- let back_'a :=
+ let back :=
fun (ret : T) =>
l1 <- get_mut_in_list_back ret;
v <- index_mut_back l1;
@@ -426,7 +426,7 @@ Definition hashMap_get_mut
hashMap_max_load := self.(hashMap_max_load);
hashMap_slots := v
|} in
- Return (t, back_'a)
+ Return (t, back)
.
(** [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
@@ -450,8 +450,8 @@ Fixpoint hashMap_remove_from_list_loop
end
else (
p <- hashMap_remove_from_list_loop T n1 key tl;
- let (o, back) := p in
- Return (o, List_Cons ckey t back))
+ let (o, tl1) := p in
+ Return (o, List_Cons ckey t tl1))
| List_Nil => Return (None, List_Nil)
end
end
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 9fb3c482..8e299800 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -104,13 +104,13 @@ Definition hashmap_HashMap_clear
(T : Type) (n : nat) (self : hashmap_HashMap_t T) :
result (hashmap_HashMap_t T)
:=
- back <- hashmap_HashMap_clear_loop T n self.(hashmap_HashMap_slots) 0%usize;
+ hm <- hashmap_HashMap_clear_loop T n self.(hashmap_HashMap_slots) 0%usize;
Return
{|
hashmap_HashMap_num_entries := 0%usize;
hashmap_HashMap_max_load_factor := self.(hashmap_HashMap_max_load_factor);
hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load);
- hashmap_HashMap_slots := back
+ hashmap_HashMap_slots := hm
|}
.
@@ -136,8 +136,8 @@ Fixpoint hashmap_HashMap_insert_in_list_loop
then Return (false, Hashmap_List_Cons ckey value tl)
else (
p <- hashmap_HashMap_insert_in_list_loop T n1 key value tl;
- let (b, back) := p in
- Return (b, Hashmap_List_Cons ckey cvalue back))
+ let (b, tl1) := p in
+ Return (b, Hashmap_List_Cons ckey cvalue tl1))
| Hashmap_List_Nil =>
Return (true, Hashmap_List_Cons key value Hashmap_List_Nil)
end
@@ -398,16 +398,15 @@ Fixpoint hashmap_HashMap_get_mut_in_list_loop
| Hashmap_List_Cons ckey cvalue tl =>
if ckey s= key
then
- let back_'a := fun (ret : T) => Return (Hashmap_List_Cons ckey ret tl)
- in
- Return (cvalue, back_'a)
+ let back := fun (ret : T) => Return (Hashmap_List_Cons ckey ret tl) in
+ Return (cvalue, back)
else (
p <- hashmap_HashMap_get_mut_in_list_loop T n1 tl key;
- let (t, back_'a) := p in
- let back_'a1 :=
+ let (t, back) := p in
+ let back1 :=
fun (ret : T) =>
- tl1 <- back_'a ret; Return (Hashmap_List_Cons ckey cvalue tl1) in
- Return (t, back_'a1))
+ tl1 <- back ret; Return (Hashmap_List_Cons ckey cvalue tl1) in
+ Return (t, back1))
| Hashmap_List_Nil => Fail_ Failure
end
end
@@ -438,7 +437,7 @@ Definition hashmap_HashMap_get_mut
let (l, index_mut_back) := p in
p1 <- hashmap_HashMap_get_mut_in_list T n l key;
let (t, get_mut_in_list_back) := p1 in
- let back_'a :=
+ let back :=
fun (ret : T) =>
l1 <- get_mut_in_list_back ret;
v <- index_mut_back l1;
@@ -450,7 +449,7 @@ Definition hashmap_HashMap_get_mut
hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load);
hashmap_HashMap_slots := v
|} in
- Return (t, back_'a)
+ Return (t, back)
.
(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0:
@@ -475,8 +474,8 @@ Fixpoint hashmap_HashMap_remove_from_list_loop
end
else (
p <- hashmap_HashMap_remove_from_list_loop T n1 key tl;
- let (o, back) := p in
- Return (o, Hashmap_List_Cons ckey t back))
+ let (o, tl1) := p in
+ Return (o, Hashmap_List_Cons ckey t tl1))
| Hashmap_List_Nil => Return (None, Hashmap_List_Nil)
end
end
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v
index faf91fef..a6832854 100644
--- a/tests/coq/misc/External_Funs.v
+++ b/tests/coq/misc/External_Funs.v
@@ -46,8 +46,8 @@ Definition custom_swap
p <- core_mem_swap T x y st;
let (st1, p1) := p in
let (x1, y1) := p1 in
- let back_'a := fun (ret : T) (st2 : state) => Return (st2, (ret, y1)) in
- Return (st1, (x1, back_'a))
+ let back := fun (ret : T) (st2 : state) => Return (st2, (ret, y1)) in
+ Return (st1, (x1, back))
.
(** [external::test_custom_swap]:
diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v
index 6773ac18..24dd2d47 100644
--- a/tests/coq/misc/External_FunsExternal_Template.v
+++ b/tests/coq/misc/External_FunsExternal_Template.v
@@ -12,19 +12,22 @@ Include External_Types.
Module External_FunsExternal_Template.
(** [core::mem::swap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42
+ Name pattern: core::mem::swap *)
Axiom core_mem_swap :
forall(T : Type), T -> T -> state -> result (state * (T * T))
.
(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57
+ Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new *)
Axiom core_num_nonzero_NonZeroU32_new
: u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t))
.
(** [core::option::{core::option::Option<T>}::unwrap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+ Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
Axiom core_option_Option_unwrap :
forall(T : Type), option T -> state -> result (state * T)
.
diff --git a/tests/coq/misc/External_TypesExternal_Template.v b/tests/coq/misc/External_TypesExternal_Template.v
index 7ba79d8e..7d6af202 100644
--- a/tests/coq/misc/External_TypesExternal_Template.v
+++ b/tests/coq/misc/External_TypesExternal_Template.v
@@ -10,7 +10,8 @@ Local Open Scope Primitives_scope.
Module External_TypesExternal_Template.
(** [core::num::nonzero::NonZeroU32]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33
+ Name pattern: core::num::nonzero::NonZeroU32 *)
Axiom core_num_nonzero_NonZeroU32_t : Type.
(** The state type used in the state-error monad *)
diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v
index 7c83a014..ae529cf8 100644
--- a/tests/coq/misc/Loops.v
+++ b/tests/coq/misc/Loops.v
@@ -375,18 +375,18 @@ Fixpoint list_nth_mut_loop_pair_loop
| List_Cons x1 tl1 =>
if i s= 0%u32
then
- let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in
- let back_'b := fun (ret : T) => Return (List_Cons ret tl1) in
- Return ((x0, x1), back_'a, back_'b)
+ let back'a := fun (ret : T) => Return (List_Cons ret tl0) in
+ let back'b := fun (ret : T) => Return (List_Cons ret tl1) in
+ Return ((x0, x1), back'a, back'b)
else (
i1 <- u32_sub i 1%u32;
t <- list_nth_mut_loop_pair_loop T n1 tl0 tl1 i1;
- let '(p, back_'a, back_'b) := t in
- let back_'a1 :=
- fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in
- let back_'b1 :=
- fun (ret : T) => tl11 <- back_'b ret; Return (List_Cons x1 tl11) in
- Return (p, back_'a1, back_'b1))
+ let '(p, back'a, back'b) := t in
+ let back'a1 :=
+ fun (ret : T) => tl01 <- back'a ret; Return (List_Cons x0 tl01) in
+ let back'b1 :=
+ fun (ret : T) => tl11 <- back'b ret; Return (List_Cons x1 tl11) in
+ Return (p, back'a1, back'b1))
| List_Nil => Fail_ Failure
end
| List_Nil => Fail_ Failure
@@ -451,21 +451,21 @@ Fixpoint list_nth_mut_loop_pair_merge_loop
| List_Cons x1 tl1 =>
if i s= 0%u32
then
- let back_'a :=
+ let back :=
fun (ret : (T * T)) =>
let (t, t1) := ret in Return (List_Cons t tl0, List_Cons t1 tl1)
in
- Return ((x0, x1), back_'a)
+ Return ((x0, x1), back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut_loop_pair_merge_loop T n1 tl0 tl1 i1;
- let (p1, back_'a) := p in
- let back_'a1 :=
+ let (p1, back) := p in
+ let back1 :=
fun (ret : (T * T)) =>
- p2 <- back_'a ret;
+ p2 <- back ret;
let (tl01, tl11) := p2 in
Return (List_Cons x0 tl01, List_Cons x1 tl11) in
- Return (p1, back_'a1))
+ Return (p1, back1))
| List_Nil => Fail_ Failure
end
| List_Nil => Fail_ Failure
@@ -531,15 +531,15 @@ Fixpoint list_nth_mut_shared_loop_pair_loop
| List_Cons x1 tl1 =>
if i s= 0%u32
then
- let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in
- Return ((x0, x1), back_'a)
+ let back := fun (ret : T) => Return (List_Cons ret tl0) in
+ Return ((x0, x1), back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut_shared_loop_pair_loop T n1 tl0 tl1 i1;
- let (p1, back_'a) := p in
- let back_'a1 :=
- fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in
- Return (p1, back_'a1))
+ let (p1, back) := p in
+ let back1 :=
+ fun (ret : T) => tl01 <- back ret; Return (List_Cons x0 tl01) in
+ Return (p1, back1))
| List_Nil => Fail_ Failure
end
| List_Nil => Fail_ Failure
@@ -571,15 +571,15 @@ Fixpoint list_nth_mut_shared_loop_pair_merge_loop
| List_Cons x1 tl1 =>
if i s= 0%u32
then
- let back_'a := fun (ret : T) => Return (List_Cons ret tl0) in
- Return ((x0, x1), back_'a)
+ let back := fun (ret : T) => Return (List_Cons ret tl0) in
+ Return ((x0, x1), back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut_shared_loop_pair_merge_loop T n1 tl0 tl1 i1;
- let (p1, back_'a) := p in
- let back_'a1 :=
- fun (ret : T) => tl01 <- back_'a ret; Return (List_Cons x0 tl01) in
- Return (p1, back_'a1))
+ let (p1, back) := p in
+ let back1 :=
+ fun (ret : T) => tl01 <- back ret; Return (List_Cons x0 tl01) in
+ Return (p1, back1))
| List_Nil => Fail_ Failure
end
| List_Nil => Fail_ Failure
@@ -611,15 +611,15 @@ Fixpoint list_nth_shared_mut_loop_pair_loop
| List_Cons x1 tl1 =>
if i s= 0%u32
then
- let back_'b := fun (ret : T) => Return (List_Cons ret tl1) in
- Return ((x0, x1), back_'b)
+ let back := fun (ret : T) => Return (List_Cons ret tl1) in
+ Return ((x0, x1), back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_shared_mut_loop_pair_loop T n1 tl0 tl1 i1;
- let (p1, back_'b) := p in
- let back_'b1 :=
- fun (ret : T) => tl11 <- back_'b ret; Return (List_Cons x1 tl11) in
- Return (p1, back_'b1))
+ let (p1, back) := p in
+ let back1 :=
+ fun (ret : T) => tl11 <- back ret; Return (List_Cons x1 tl11) in
+ Return (p1, back1))
| List_Nil => Fail_ Failure
end
| List_Nil => Fail_ Failure
@@ -651,15 +651,15 @@ Fixpoint list_nth_shared_mut_loop_pair_merge_loop
| List_Cons x1 tl1 =>
if i s= 0%u32
then
- let back_'a := fun (ret : T) => Return (List_Cons ret tl1) in
- Return ((x0, x1), back_'a)
+ let back := fun (ret : T) => Return (List_Cons ret tl1) in
+ Return ((x0, x1), back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_shared_mut_loop_pair_merge_loop T n1 tl0 tl1 i1;
- let (p1, back_'a) := p in
- let back_'a1 :=
- fun (ret : T) => tl11 <- back_'a ret; Return (List_Cons x1 tl11) in
- Return (p1, back_'a1))
+ let (p1, back) := p in
+ let back1 :=
+ fun (ret : T) => tl11 <- back ret; Return (List_Cons x1 tl11) in
+ Return (p1, back1))
| List_Nil => Fail_ Failure
end
| List_Nil => Fail_ Failure
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index 76dc4cf6..d4035104 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -321,8 +321,8 @@ Check (test_split_list )%return.
Definition choose
(T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) :=
if b
- then let back_'a := fun (ret : T) => Return (ret, y) in Return (x, back_'a)
- else let back_'a := fun (ret : T) => Return (x, ret) in Return (y, back_'a)
+ then let back := fun (ret : T) => Return (ret, y) in Return (x, back)
+ else let back := fun (ret : T) => Return (x, ret) in Return (y, back)
.
(** [no_nested_borrows::choose_test]:
@@ -399,16 +399,16 @@ Fixpoint list_nth_mut
| List_Cons x tl =>
if i s= 0%u32
then
- let back_'a := fun (ret : T) => Return (List_Cons ret tl) in
- Return (x, back_'a)
+ let back := fun (ret : T) => Return (List_Cons ret tl) in
+ Return (x, back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut T tl i1;
let (t, list_nth_mut_back) := p in
- let back_'a :=
+ let back :=
fun (ret : T) => tl1 <- list_nth_mut_back ret; Return (List_Cons x tl1)
in
- Return (t, back_'a))
+ Return (t, back))
| List_Nil => Fail_ Failure
end
.
diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v
index ad77fa2a..77276223 100644
--- a/tests/coq/misc/Paper.v
+++ b/tests/coq/misc/Paper.v
@@ -27,8 +27,8 @@ Check (test_incr )%return.
Definition choose
(T : Type) (b : bool) (x : T) (y : T) : result (T * (T -> result (T * T))) :=
if b
- then let back_'a := fun (ret : T) => Return (ret, y) in Return (x, back_'a)
- else let back_'a := fun (ret : T) => Return (x, ret) in Return (y, back_'a)
+ then let back := fun (ret : T) => Return (ret, y) in Return (x, back)
+ else let back := fun (ret : T) => Return (x, ret) in Return (y, back)
.
(** [paper::test_choose]:
@@ -70,16 +70,16 @@ Fixpoint list_nth_mut
| List_Cons x tl =>
if i s= 0%u32
then
- let back_'a := fun (ret : T) => Return (List_Cons ret tl) in
- Return (x, back_'a)
+ let back := fun (ret : T) => Return (List_Cons ret tl) in
+ Return (x, back)
else (
i1 <- u32_sub i 1%u32;
p <- list_nth_mut T tl i1;
let (t, list_nth_mut_back) := p in
- let back_'a :=
+ let back :=
fun (ret : T) => tl1 <- list_nth_mut_back ret; Return (List_Cons x tl1)
in
- Return (t, back_'a))
+ Return (t, back))
| List_Nil => Fail_ Failure
end
.
diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v
index 8f403a8e..dfa09328 100644
--- a/tests/coq/misc/PoloniusList.v
+++ b/tests/coq/misc/PoloniusList.v
@@ -31,10 +31,10 @@ Fixpoint get_list_at_x
else (
p <- get_list_at_x tl x;
let (l, get_list_at_x_back) := p in
- let back_'a :=
+ let back :=
fun (ret : List_t u32) =>
tl1 <- get_list_at_x_back ret; Return (List_Cons hd tl1) in
- Return (l, back_'a))
+ Return (l, back))
| List_Nil => Return (List_Nil, Return)
end
.
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index a861c114..0e942c7d 100644
--- a/tests/coq/traits/Traits.v
+++ b/tests/coq/traits/Traits.v
@@ -671,7 +671,8 @@ Arguments foo_x { _ _ }.
Arguments foo_y { _ _ }.
(** [core::result::Result]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 *)
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21
+ Name pattern: core::result::Result *)
Inductive core_result_Result_t (T E : Type) :=
| Core_result_Result_Ok : T -> core_result_Result_t T E
| Core_result_Result_Err : E -> core_result_Result_t T E
diff --git a/tests/fstar/betree/BetreeMain.Funs.fst b/tests/fstar/betree/BetreeMain.Funs.fst
index 2469f98c..129e6f7e 100644
--- a/tests/fstar/betree/BetreeMain.Funs.fst
+++ b/tests/fstar/betree/BetreeMain.Funs.fst
@@ -195,11 +195,11 @@ let rec betree_Node_lookup_first_message_for_key
else
let* (l, lookup_first_message_for_key_back) =
betree_Node_lookup_first_message_for_key key next_msgs in
- let back_'a =
+ let back =
fun ret ->
let* next_msgs1 = lookup_first_message_for_key_back ret in
Return (Betree_List_Cons (i, m) next_msgs1) in
- Return (l, back_'a)
+ Return (l, back)
| Betree_List_Nil -> Return (Betree_List_Nil, Return)
end
@@ -352,11 +352,11 @@ let rec betree_Node_lookup_first_message_after_key
then
let* (l, lookup_first_message_after_key_back) =
betree_Node_lookup_first_message_after_key key next_msgs in
- let back_'a =
+ let back =
fun ret ->
let* next_msgs1 = lookup_first_message_after_key_back ret in
Return (Betree_List_Cons (k, m) next_msgs1) in
- Return (l, back_'a)
+ Return (l, back)
else Return (Betree_List_Cons (k, m) next_msgs, Return)
| Betree_List_Nil -> Return (Betree_List_Nil, Return)
end
@@ -453,11 +453,11 @@ let rec betree_Node_lookup_mut_in_bindings
else
let* (l, lookup_mut_in_bindings_back) =
betree_Node_lookup_mut_in_bindings key tl in
- let back_'a =
+ let back =
fun ret ->
let* tl1 = lookup_mut_in_bindings_back ret in
Return (Betree_List_Cons (i, i1) tl1) in
- Return (l, back_'a)
+ Return (l, back)
| Betree_List_Nil -> Return (Betree_List_Nil, Return)
end
diff --git a/tests/fstar/betree/BetreeMain.FunsExternal.fsti b/tests/fstar/betree/BetreeMain.FunsExternal.fsti
index de9b96fd..3aad9390 100644
--- a/tests/fstar/betree/BetreeMain.FunsExternal.fsti
+++ b/tests/fstar/betree/BetreeMain.FunsExternal.fsti
@@ -29,7 +29,8 @@ val betree_utils_store_leaf_node
: u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
(** [core::option::{core::option::Option<T>}::unwrap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+ Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
val core_option_Option_unwrap
(t : Type0) : option t -> state -> result (state & t)
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
index 2469f98c..129e6f7e 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
+++ b/tests/fstar/betree_back_stateful/BetreeMain.Funs.fst
@@ -195,11 +195,11 @@ let rec betree_Node_lookup_first_message_for_key
else
let* (l, lookup_first_message_for_key_back) =
betree_Node_lookup_first_message_for_key key next_msgs in
- let back_'a =
+ let back =
fun ret ->
let* next_msgs1 = lookup_first_message_for_key_back ret in
Return (Betree_List_Cons (i, m) next_msgs1) in
- Return (l, back_'a)
+ Return (l, back)
| Betree_List_Nil -> Return (Betree_List_Nil, Return)
end
@@ -352,11 +352,11 @@ let rec betree_Node_lookup_first_message_after_key
then
let* (l, lookup_first_message_after_key_back) =
betree_Node_lookup_first_message_after_key key next_msgs in
- let back_'a =
+ let back =
fun ret ->
let* next_msgs1 = lookup_first_message_after_key_back ret in
Return (Betree_List_Cons (k, m) next_msgs1) in
- Return (l, back_'a)
+ Return (l, back)
else Return (Betree_List_Cons (k, m) next_msgs, Return)
| Betree_List_Nil -> Return (Betree_List_Nil, Return)
end
@@ -453,11 +453,11 @@ let rec betree_Node_lookup_mut_in_bindings
else
let* (l, lookup_mut_in_bindings_back) =
betree_Node_lookup_mut_in_bindings key tl in
- let back_'a =
+ let back =
fun ret ->
let* tl1 = lookup_mut_in_bindings_back ret in
Return (Betree_List_Cons (i, i1) tl1) in
- Return (l, back_'a)
+ Return (l, back)
| Betree_List_Nil -> Return (Betree_List_Nil, Return)
end
diff --git a/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
index de9b96fd..3aad9390 100644
--- a/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
+++ b/tests/fstar/betree_back_stateful/BetreeMain.FunsExternal.fsti
@@ -29,7 +29,8 @@ val betree_utils_store_leaf_node
: u64 -> betree_List_t (u64 & u64) -> state -> result (state & unit)
(** [core::option::{core::option::Option<T>}::unwrap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+ Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
val core_option_Option_unwrap
(t : Type0) : option t -> state -> result (state & t)
diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
index d93bc847..9c59ab9b 100644
--- a/tests/fstar/demo/Demo.fst
+++ b/tests/fstar/demo/Demo.fst
@@ -10,8 +10,8 @@ open Primitives
let choose
(t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) =
if b
- then let back_'a = fun ret -> Return (ret, y) in Return (x, back_'a)
- else let back_'a = fun ret -> Return (x, ret) in Return (y, back_'a)
+ then let back = fun ret -> Return (ret, y) in Return (x, back)
+ else let back = fun ret -> Return (x, ret) in Return (y, back)
(** [demo::mul2_add1]:
Source: 'src/demo.rs', lines 13:0-13:31 *)
@@ -66,15 +66,14 @@ let rec list_nth_mut
| CList_CCons x tl ->
if i = 0
then
- let back_'a = fun ret -> Return (CList_CCons ret tl) in
- Return (x, back_'a)
+ let back = fun ret -> Return (CList_CCons ret tl) in Return (x, back)
else
let* i1 = u32_sub i 1 in
let* (x1, list_nth_mut_back) = list_nth_mut t n1 tl i1 in
- let back_'a =
+ let back =
fun ret ->
let* tl1 = list_nth_mut_back ret in Return (CList_CCons x tl1) in
- Return (x1, back_'a)
+ Return (x1, back)
| CList_CNil -> Fail Failure
end
@@ -92,14 +91,13 @@ let rec list_nth_mut1_loop
| CList_CCons x tl ->
if i = 0
then
- let back_'a = fun ret -> Return (CList_CCons ret tl) in
- Return (x, back_'a)
+ let back = fun ret -> Return (CList_CCons ret tl) in Return (x, back)
else
let* i1 = u32_sub i 1 in
- let* (x1, back_'a) = list_nth_mut1_loop t n1 tl i1 in
- let back_'a1 =
- fun ret -> let* tl1 = back_'a ret in Return (CList_CCons x tl1) in
- Return (x1, back_'a1)
+ let* (x1, back) = list_nth_mut1_loop t n1 tl i1 in
+ let back1 =
+ fun ret -> let* tl1 = back ret in Return (CList_CCons x tl1) in
+ Return (x1, back1)
| CList_CNil -> Fail Failure
end
@@ -135,10 +133,10 @@ let rec list_tail
begin match l with
| CList_CCons x tl ->
let* (c, list_tail_back) = list_tail t n1 tl in
- let back_'a =
+ let back =
fun ret -> let* tl1 = list_tail_back ret in Return (CList_CCons x tl1)
in
- Return (c, back_'a)
+ Return (c, back)
| CList_CNil -> Return (CList_CNil, Return)
end
diff --git a/tests/fstar/hashmap/Hashmap.Funs.fst b/tests/fstar/hashmap/Hashmap.Funs.fst
index fba711f1..d897933a 100644
--- a/tests/fstar/hashmap/Hashmap.Funs.fst
+++ b/tests/fstar/hashmap/Hashmap.Funs.fst
@@ -79,8 +79,8 @@ let rec hashMap_clear_loop
(** [hashmap::{hashmap::HashMap<T>}::clear]:
Source: 'src/hashmap.rs', lines 80:4-80:27 *)
let hashMap_clear (t : Type0) (self : hashMap_t t) : result (hashMap_t t) =
- let* back = hashMap_clear_loop t self.slots 0 in
- Return { self with num_entries = 0; slots = back }
+ let* hm = hashMap_clear_loop t self.slots 0 in
+ Return { self with num_entries = 0; slots = hm }
(** [hashmap::{hashmap::HashMap<T>}::len]:
Source: 'src/hashmap.rs', lines 90:4-90:30 *)
@@ -99,8 +99,8 @@ let rec hashMap_insert_in_list_loop
if ckey = key
then Return (false, List_Cons ckey value tl)
else
- let* (b, back) = hashMap_insert_in_list_loop t key value tl in
- Return (b, List_Cons ckey cvalue back)
+ let* (b, tl1) = hashMap_insert_in_list_loop t key value tl in
+ Return (b, List_Cons ckey cvalue tl1)
| List_Nil -> Return (true, List_Cons key value List_Nil)
end
@@ -287,14 +287,13 @@ let rec hashMap_get_mut_in_list_loop
| List_Cons ckey cvalue tl ->
if ckey = key
then
- let back_'a = fun ret -> Return (List_Cons ckey ret tl) in
- Return (cvalue, back_'a)
+ let back = fun ret -> Return (List_Cons ckey ret tl) in
+ Return (cvalue, back)
else
- let* (x, back_'a) = hashMap_get_mut_in_list_loop t tl key in
- let back_'a1 =
- fun ret -> let* tl1 = back_'a ret in Return (List_Cons ckey cvalue tl1)
- in
- Return (x, back_'a1)
+ let* (x, back) = hashMap_get_mut_in_list_loop t tl key in
+ let back1 =
+ fun ret -> let* tl1 = back ret in Return (List_Cons ckey cvalue tl1) in
+ Return (x, back1)
| List_Nil -> Fail Failure
end
@@ -320,12 +319,12 @@ let hashMap_get_mut
(core_slice_index_SliceIndexUsizeSliceTInst (list_t t)) self.slots
hash_mod in
let* (x, get_mut_in_list_back) = hashMap_get_mut_in_list t l key in
- let back_'a =
+ let back =
fun ret ->
let* l1 = get_mut_in_list_back ret in
let* v = index_mut_back l1 in
Return { self with slots = v } in
- Return (x, back_'a)
+ Return (x, back)
(** [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
Source: 'src/hashmap.rs', lines 265:4-291:5 *)
@@ -345,8 +344,8 @@ let rec hashMap_remove_from_list_loop
| List_Nil -> Fail Failure
end
else
- let* (o, back) = hashMap_remove_from_list_loop t key tl in
- Return (o, List_Cons ckey x back)
+ let* (o, tl1) = hashMap_remove_from_list_loop t key tl in
+ Return (o, List_Cons ckey x tl1)
| List_Nil -> Return (None, List_Nil)
end
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
index 97f4151f..e0005c81 100644
--- a/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
+++ b/tests/fstar/hashmap_on_disk/HashmapMain.Funs.fst
@@ -84,8 +84,8 @@ let rec hashmap_HashMap_clear_loop
Source: 'src/hashmap.rs', lines 80:4-80:27 *)
let hashmap_HashMap_clear
(t : Type0) (self : hashmap_HashMap_t t) : result (hashmap_HashMap_t t) =
- let* back = hashmap_HashMap_clear_loop t self.slots 0 in
- Return { self with num_entries = 0; slots = back }
+ let* hm = hashmap_HashMap_clear_loop t self.slots 0 in
+ Return { self with num_entries = 0; slots = hm }
(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::len]:
Source: 'src/hashmap.rs', lines 90:4-90:30 *)
@@ -105,8 +105,8 @@ let rec hashmap_HashMap_insert_in_list_loop
if ckey = key
then Return (false, Hashmap_List_Cons ckey value tl)
else
- let* (b, back) = hashmap_HashMap_insert_in_list_loop t key value tl in
- Return (b, Hashmap_List_Cons ckey cvalue back)
+ let* (b, tl1) = hashmap_HashMap_insert_in_list_loop t key value tl in
+ Return (b, Hashmap_List_Cons ckey cvalue tl1)
| Hashmap_List_Nil ->
Return (true, Hashmap_List_Cons key value Hashmap_List_Nil)
end
@@ -305,15 +305,14 @@ let rec hashmap_HashMap_get_mut_in_list_loop
| Hashmap_List_Cons ckey cvalue tl ->
if ckey = key
then
- let back_'a = fun ret -> Return (Hashmap_List_Cons ckey ret tl) in
- Return (cvalue, back_'a)
+ let back = fun ret -> Return (Hashmap_List_Cons ckey ret tl) in
+ Return (cvalue, back)
else
- let* (x, back_'a) = hashmap_HashMap_get_mut_in_list_loop t tl key in
- let back_'a1 =
+ let* (x, back) = hashmap_HashMap_get_mut_in_list_loop t tl key in
+ let back1 =
fun ret ->
- let* tl1 = back_'a ret in Return (Hashmap_List_Cons ckey cvalue tl1)
- in
- Return (x, back_'a1)
+ let* tl1 = back ret in Return (Hashmap_List_Cons ckey cvalue tl1) in
+ Return (x, back1)
| Hashmap_List_Nil -> Fail Failure
end
@@ -339,12 +338,12 @@ let hashmap_HashMap_get_mut
(core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t t))
self.slots hash_mod in
let* (x, get_mut_in_list_back) = hashmap_HashMap_get_mut_in_list t l key in
- let back_'a =
+ let back =
fun ret ->
let* l1 = get_mut_in_list_back ret in
let* v = index_mut_back l1 in
Return { self with slots = v } in
- Return (x, back_'a)
+ Return (x, back)
(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0:
Source: 'src/hashmap.rs', lines 265:4-291:5 *)
@@ -365,8 +364,8 @@ let rec hashmap_HashMap_remove_from_list_loop
| Hashmap_List_Nil -> Fail Failure
end
else
- let* (o, back) = hashmap_HashMap_remove_from_list_loop t key tl in
- Return (o, Hashmap_List_Cons ckey x back)
+ let* (o, tl1) = hashmap_HashMap_remove_from_list_loop t key tl in
+ Return (o, Hashmap_List_Cons ckey x tl1)
| Hashmap_List_Nil -> Return (None, Hashmap_List_Nil)
end
diff --git a/tests/fstar/misc/External.Funs.fst b/tests/fstar/misc/External.Funs.fst
index 3ba20022..78960404 100644
--- a/tests/fstar/misc/External.Funs.fst
+++ b/tests/fstar/misc/External.Funs.fst
@@ -34,8 +34,8 @@ let custom_swap
result (state & (t & (t -> state -> result (state & (t & t)))))
=
let* (st1, (x1, y1)) = core_mem_swap t x y st in
- let back_'a = fun ret st2 -> Return (st2, (ret, y1)) in
- Return (st1, (x1, back_'a))
+ let back = fun ret st2 -> Return (st2, (ret, y1)) in
+ Return (st1, (x1, back))
(** [external::test_custom_swap]:
Source: 'src/external.rs', lines 29:0-29:59 *)
diff --git a/tests/fstar/misc/External.FunsExternal.fsti b/tests/fstar/misc/External.FunsExternal.fsti
index a412aea9..4c1c58b7 100644
--- a/tests/fstar/misc/External.FunsExternal.fsti
+++ b/tests/fstar/misc/External.FunsExternal.fsti
@@ -7,16 +7,19 @@ include External.Types
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
(** [core::mem::swap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *)
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42
+ Name pattern: core::mem::swap *)
val core_mem_swap (t : Type0) : t -> t -> state -> result (state & (t & t))
(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *)
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57
+ Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new *)
val core_num_nonzero_NonZeroU32_new
: u32 -> state -> result (state & (option core_num_nonzero_NonZeroU32_t))
(** [core::option::{core::option::Option<T>}::unwrap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *)
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+ Name pattern: core::option::{core::option::Option<@T>}::unwrap *)
val core_option_Option_unwrap
(t : Type0) : option t -> state -> result (state & t)
diff --git a/tests/fstar/misc/External.TypesExternal.fsti b/tests/fstar/misc/External.TypesExternal.fsti
index 4bfbe0c5..45174c7e 100644
--- a/tests/fstar/misc/External.TypesExternal.fsti
+++ b/tests/fstar/misc/External.TypesExternal.fsti
@@ -6,7 +6,8 @@ open Primitives
#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
(** [core::num::nonzero::NonZeroU32]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 *)
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33
+ Name pattern: core::num::nonzero::NonZeroU32 *)
val core_num_nonzero_NonZeroU32_t : Type0
(** The state type used in the state-error monad *)
diff --git a/tests/fstar/misc/Loops.Funs.fst b/tests/fstar/misc/Loops.Funs.fst
index 7c099da2..93683deb 100644
--- a/tests/fstar/misc/Loops.Funs.fst
+++ b/tests/fstar/misc/Loops.Funs.fst
@@ -289,18 +289,17 @@ let rec list_nth_mut_loop_pair_loop
| List_Cons x1 tl1 ->
if i = 0
then
- let back_'a = fun ret -> Return (List_Cons ret tl0) in
- let back_'b = fun ret -> Return (List_Cons ret tl1) in
- Return ((x0, x1), back_'a, back_'b)
+ let back'a = fun ret -> Return (List_Cons ret tl0) in
+ let back'b = fun ret -> Return (List_Cons ret tl1) in
+ Return ((x0, x1), back'a, back'b)
else
let* i1 = u32_sub i 1 in
- let* (p, back_'a, back_'b) = list_nth_mut_loop_pair_loop t tl0 tl1 i1
- in
- let back_'a1 =
- fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in
- let back_'b1 =
- fun ret -> let* tl11 = back_'b ret in Return (List_Cons x1 tl11) in
- Return (p, back_'a1, back_'b1)
+ let* (p, back'a, back'b) = list_nth_mut_loop_pair_loop t tl0 tl1 i1 in
+ let back'a1 =
+ fun ret -> let* tl01 = back'a ret in Return (List_Cons x0 tl01) in
+ let back'b1 =
+ fun ret -> let* tl11 = back'b ret in Return (List_Cons x1 tl11) in
+ Return (p, back'a1, back'b1)
| List_Nil -> Fail Failure
end
| List_Nil -> Fail Failure
@@ -352,18 +351,18 @@ let rec list_nth_mut_loop_pair_merge_loop
| List_Cons x1 tl1 ->
if i = 0
then
- let back_'a =
+ let back =
fun ret ->
let (x, x2) = ret in Return (List_Cons x tl0, List_Cons x2 tl1) in
- Return ((x0, x1), back_'a)
+ Return ((x0, x1), back)
else
let* i1 = u32_sub i 1 in
- let* (p, back_'a) = list_nth_mut_loop_pair_merge_loop t tl0 tl1 i1 in
- let back_'a1 =
+ let* (p, back) = list_nth_mut_loop_pair_merge_loop t tl0 tl1 i1 in
+ let back1 =
fun ret ->
- let* (tl01, tl11) = back_'a ret in
+ let* (tl01, tl11) = back ret in
Return (List_Cons x0 tl01, List_Cons x1 tl11) in
- Return (p, back_'a1)
+ Return (p, back1)
| List_Nil -> Fail Failure
end
| List_Nil -> Fail Failure
@@ -417,14 +416,14 @@ let rec list_nth_mut_shared_loop_pair_loop
| List_Cons x1 tl1 ->
if i = 0
then
- let back_'a = fun ret -> Return (List_Cons ret tl0) in
- Return ((x0, x1), back_'a)
+ let back = fun ret -> Return (List_Cons ret tl0) in
+ Return ((x0, x1), back)
else
let* i1 = u32_sub i 1 in
- let* (p, back_'a) = list_nth_mut_shared_loop_pair_loop t tl0 tl1 i1 in
- let back_'a1 =
- fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in
- Return (p, back_'a1)
+ let* (p, back) = list_nth_mut_shared_loop_pair_loop t tl0 tl1 i1 in
+ let back1 =
+ fun ret -> let* tl01 = back ret in Return (List_Cons x0 tl01) in
+ Return (p, back1)
| List_Nil -> Fail Failure
end
| List_Nil -> Fail Failure
@@ -451,15 +450,15 @@ let rec list_nth_mut_shared_loop_pair_merge_loop
| List_Cons x1 tl1 ->
if i = 0
then
- let back_'a = fun ret -> Return (List_Cons ret tl0) in
- Return ((x0, x1), back_'a)
+ let back = fun ret -> Return (List_Cons ret tl0) in
+ Return ((x0, x1), back)
else
let* i1 = u32_sub i 1 in
- let* (p, back_'a) =
- list_nth_mut_shared_loop_pair_merge_loop t tl0 tl1 i1 in
- let back_'a1 =
- fun ret -> let* tl01 = back_'a ret in Return (List_Cons x0 tl01) in
- Return (p, back_'a1)
+ let* (p, back) = list_nth_mut_shared_loop_pair_merge_loop t tl0 tl1 i1
+ in
+ let back1 =
+ fun ret -> let* tl01 = back ret in Return (List_Cons x0 tl01) in
+ Return (p, back1)
| List_Nil -> Fail Failure
end
| List_Nil -> Fail Failure
@@ -486,14 +485,14 @@ let rec list_nth_shared_mut_loop_pair_loop
| List_Cons x1 tl1 ->
if i = 0
then
- let back_'b = fun ret -> Return (List_Cons ret tl1) in
- Return ((x0, x1), back_'b)
+ let back = fun ret -> Return (List_Cons ret tl1) in
+ Return ((x0, x1), back)
else
let* i1 = u32_sub i 1 in
- let* (p, back_'b) = list_nth_shared_mut_loop_pair_loop t tl0 tl1 i1 in
- let back_'b1 =
- fun ret -> let* tl11 = back_'b ret in Return (List_Cons x1 tl11) in
- Return (p, back_'b1)
+ let* (p, back) = list_nth_shared_mut_loop_pair_loop t tl0 tl1 i1 in
+ let back1 =
+ fun ret -> let* tl11 = back ret in Return (List_Cons x1 tl11) in
+ Return (p, back1)
| List_Nil -> Fail Failure
end
| List_Nil -> Fail Failure
@@ -520,15 +519,15 @@ let rec list_nth_shared_mut_loop_pair_merge_loop
| List_Cons x1 tl1 ->
if i = 0
then
- let back_'a = fun ret -> Return (List_Cons ret tl1) in
- Return ((x0, x1), back_'a)
+ let back = fun ret -> Return (List_Cons ret tl1) in
+ Return ((x0, x1), back)
else
let* i1 = u32_sub i 1 in
- let* (p, back_'a) =
- list_nth_shared_mut_loop_pair_merge_loop t tl0 tl1 i1 in
- let back_'a1 =
- fun ret -> let* tl11 = back_'a ret in Return (List_Cons x1 tl11) in
- Return (p, back_'a1)
+ let* (p, back) = list_nth_shared_mut_loop_pair_merge_loop t tl0 tl1 i1
+ in
+ let back1 =
+ fun ret -> let* tl11 = back ret in Return (List_Cons x1 tl11) in
+ Return (p, back1)
| List_Nil -> Fail Failure
end
| List_Nil -> Fail Failure
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index db63eb0d..1a93beaa 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -291,8 +291,8 @@ let _ = assert_norm (test_split_list = Return ())
let choose
(t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) =
if b
- then let back_'a = fun ret -> Return (ret, y) in Return (x, back_'a)
- else let back_'a = fun ret -> Return (x, ret) in Return (y, back_'a)
+ then let back = fun ret -> Return (ret, y) in Return (x, back)
+ else let back = fun ret -> Return (x, ret) in Return (y, back)
(** [no_nested_borrows::choose_test]:
Source: 'src/no_nested_borrows.rs', lines 282:0-282:20 *)
@@ -355,15 +355,14 @@ let rec list_nth_mut
begin match l with
| List_Cons x tl ->
if i = 0
- then
- let back_'a = fun ret -> Return (List_Cons ret tl) in Return (x, back_'a)
+ then let back = fun ret -> Return (List_Cons ret tl) in Return (x, back)
else
let* i1 = u32_sub i 1 in
let* (x1, list_nth_mut_back) = list_nth_mut t tl i1 in
- let back_'a =
+ let back =
fun ret -> let* tl1 = list_nth_mut_back ret in Return (List_Cons x tl1)
in
- Return (x1, back_'a)
+ Return (x1, back)
| List_Nil -> Fail Failure
end
diff --git a/tests/fstar/misc/Paper.fst b/tests/fstar/misc/Paper.fst
index ddc5e7a8..c2f47ad1 100644
--- a/tests/fstar/misc/Paper.fst
+++ b/tests/fstar/misc/Paper.fst
@@ -23,8 +23,8 @@ let _ = assert_norm (test_incr = Return ())
let choose
(t : Type0) (b : bool) (x : t) (y : t) : result (t & (t -> result (t & t))) =
if b
- then let back_'a = fun ret -> Return (ret, y) in Return (x, back_'a)
- else let back_'a = fun ret -> Return (x, ret) in Return (y, back_'a)
+ then let back = fun ret -> Return (ret, y) in Return (x, back)
+ else let back = fun ret -> Return (x, ret) in Return (y, back)
(** [paper::test_choose]:
Source: 'src/paper.rs', lines 23:0-23:20 *)
@@ -57,15 +57,14 @@ let rec list_nth_mut
begin match l with
| List_Cons x tl ->
if i = 0
- then
- let back_'a = fun ret -> Return (List_Cons ret tl) in Return (x, back_'a)
+ then let back = fun ret -> Return (List_Cons ret tl) in Return (x, back)
else
let* i1 = u32_sub i 1 in
let* (x1, list_nth_mut_back) = list_nth_mut t tl i1 in
- let back_'a =
+ let back =
fun ret -> let* tl1 = list_nth_mut_back ret in Return (List_Cons x tl1)
in
- Return (x1, back_'a)
+ Return (x1, back)
| List_Nil -> Fail Failure
end
diff --git a/tests/fstar/misc/PoloniusList.fst b/tests/fstar/misc/PoloniusList.fst
index b477802b..4203247e 100644
--- a/tests/fstar/misc/PoloniusList.fst
+++ b/tests/fstar/misc/PoloniusList.fst
@@ -23,10 +23,10 @@ let rec get_list_at_x
then Return (List_Cons hd tl, Return)
else
let* (l, get_list_at_x_back) = get_list_at_x tl x in
- let back_'a =
+ let back =
fun ret ->
let* tl1 = get_list_at_x_back ret in Return (List_Cons hd tl1) in
- Return (l, back_'a)
+ Return (l, back)
| List_Nil -> Return (List_Nil, Return)
end
diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
index fba564a5..199d49bf 100644
--- a/tests/fstar/traits/Traits.fst
+++ b/tests/fstar/traits/Traits.fst
@@ -503,7 +503,8 @@ let use_wrapper_len (t : Type0) (traitInst : trait_t t) : result usize =
type foo_t (t u : Type0) = { x : t; y : u; }
(** [core::result::Result]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 *)
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21
+ Name pattern: core::result::Result *)
type core_result_Result_t (t e : Type0) =
| Core_result_Result_Ok : t -> core_result_Result_t t e
| Core_result_Result_Err : e -> core_result_Result_t t e
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index ca9b48da..2fbcd6a4 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -192,12 +192,12 @@ divergent def betree.Node.lookup_first_message_for_key
do
let (l, lookup_first_message_for_key_back) ←
betree.Node.lookup_first_message_for_key key next_msgs
- let back_'a :=
+ let back :=
fun ret =>
do
let next_msgs1 ← lookup_first_message_for_key_back ret
Result.ret (betree.List.Cons (i, m) next_msgs1)
- Result.ret (l, back_'a)
+ Result.ret (l, back)
| betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]:
@@ -364,12 +364,12 @@ divergent def betree.Node.lookup_first_message_after_key
do
let (l, lookup_first_message_after_key_back) ←
betree.Node.lookup_first_message_after_key key next_msgs
- let back_'a :=
+ let back :=
fun ret =>
do
let next_msgs1 ← lookup_first_message_after_key_back ret
Result.ret (betree.List.Cons (k, m) next_msgs1)
- Result.ret (l, back_'a)
+ Result.ret (l, back)
else Result.ret (betree.List.Cons (k, m) next_msgs, Result.ret)
| betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
@@ -468,12 +468,12 @@ divergent def betree.Node.lookup_mut_in_bindings
do
let (l, lookup_mut_in_bindings_back) ←
betree.Node.lookup_mut_in_bindings key tl
- let back_'a :=
+ let back :=
fun ret =>
do
let tl1 ← lookup_mut_in_bindings_back ret
Result.ret (betree.List.Cons (i, i1) tl1)
- Result.ret (l, back_'a)
+ Result.ret (l, back)
| betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]:
diff --git a/tests/lean/BetreeMain/FunsExternal_Template.lean b/tests/lean/BetreeMain/FunsExternal_Template.lean
index eaa4b6c2..0b3e4ef4 100644
--- a/tests/lean/BetreeMain/FunsExternal_Template.lean
+++ b/tests/lean/BetreeMain/FunsExternal_Template.lean
@@ -29,7 +29,8 @@ axiom betree_utils.store_leaf_node
: U64 → betree.List (U64 × U64) → State → Result (State × Unit)
/- [core::option::{core::option::Option<T>}::unwrap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 -/
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+ Name pattern: core::option::{core::option::Option<@T>}::unwrap -/
axiom core.option.Option.unwrap
(T : Type) : Option T → State → Result (State × T)
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 4acc69c8..6d9fef8e 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -12,10 +12,10 @@ def choose
Result (T × (T → Result (T × T)))
:=
if b
- then let back_'a := fun ret => Result.ret (ret, y)
- Result.ret (x, back_'a)
- else let back_'a := fun ret => Result.ret (x, ret)
- Result.ret (y, back_'a)
+ then let back := fun ret => Result.ret (ret, y)
+ Result.ret (x, back)
+ else let back := fun ret => Result.ret (x, ret)
+ Result.ret (y, back)
/- [demo::mul2_add1]:
Source: 'src/demo.rs', lines 13:0-13:31 -/
@@ -73,18 +73,18 @@ divergent def list_nth_mut
| CList.CCons x tl =>
if i = 0#u32
then
- let back_'a := fun ret => Result.ret (CList.CCons ret tl)
- Result.ret (x, back_'a)
+ let back := fun ret => Result.ret (CList.CCons ret tl)
+ Result.ret (x, back)
else
do
let i1 ← i - 1#u32
let (t, list_nth_mut_back) ← list_nth_mut T tl i1
- let back_'a :=
+ let back :=
fun ret =>
do
let tl1 ← list_nth_mut_back ret
Result.ret (CList.CCons x tl1)
- Result.ret (t, back_'a)
+ Result.ret (t, back)
| CList.CNil => Result.fail .panic
/- [demo::list_nth_mut1]: loop 0:
@@ -97,17 +97,17 @@ divergent def list_nth_mut1_loop
| CList.CCons x tl =>
if i = 0#u32
then
- let back_'a := fun ret => Result.ret (CList.CCons ret tl)
- Result.ret (x, back_'a)
+ let back := fun ret => Result.ret (CList.CCons ret tl)
+ Result.ret (x, back)
else
do
let i1 ← i - 1#u32
- let (t, back_'a) ← list_nth_mut1_loop T tl i1
- let back_'a1 :=
+ let (t, back) ← list_nth_mut1_loop T tl i1
+ let back1 :=
fun ret => do
- let tl1 ← back_'a ret
+ let tl1 ← back ret
Result.ret (CList.CCons x tl1)
- Result.ret (t, back_'a1)
+ Result.ret (t, back1)
| CList.CNil => Result.fail .panic
/- [demo::list_nth_mut1]:
@@ -138,12 +138,12 @@ divergent def list_tail
| CList.CCons t tl =>
do
let (c, list_tail_back) ← list_tail T tl
- let back_'a :=
+ let back :=
fun ret =>
do
let tl1 ← list_tail_back ret
Result.ret (CList.CCons t tl1)
- Result.ret (c, back_'a)
+ Result.ret (c, back)
| CList.CNil => Result.ret (CList.CNil, Result.ret)
/- Trait declaration: [demo::Counter]
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 8b645037..cfb2cb3c 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -39,8 +39,8 @@ def custom_swap
:=
do
let (st1, (x1, y1)) ← core.mem.swap T x y st
- let back_'a := fun ret st2 => Result.ret (st2, (ret, y1))
- Result.ret (st1, (x1, back_'a))
+ let back := fun ret st2 => Result.ret (st2, (ret, y1))
+ Result.ret (st1, (x1, back))
/- [external::test_custom_swap]:
Source: 'src/external.rs', lines 29:0-29:59 -/
diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean
index 7e237369..38151dc9 100644
--- a/tests/lean/External/FunsExternal_Template.lean
+++ b/tests/lean/External/FunsExternal_Template.lean
@@ -7,17 +7,20 @@ open Primitives
open external
/- [core::mem::swap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 -/
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42
+ Name pattern: core::mem::swap -/
axiom core.mem.swap
(T : Type) : T → T → State → Result (State × (T × T))
/- [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 -/
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57
+ Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new -/
axiom core.num.nonzero.NonZeroU32.new
: U32 → State → Result (State × (Option core.num.nonzero.NonZeroU32))
/- [core::option::{core::option::Option<T>}::unwrap]:
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 -/
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
+ Name pattern: core::option::{core::option::Option<@T>}::unwrap -/
axiom core.option.Option.unwrap
(T : Type) : Option T → State → Result (State × T)
diff --git a/tests/lean/External/TypesExternal_Template.lean b/tests/lean/External/TypesExternal_Template.lean
index 85fef236..84245531 100644
--- a/tests/lean/External/TypesExternal_Template.lean
+++ b/tests/lean/External/TypesExternal_Template.lean
@@ -5,7 +5,8 @@ import Base
open Primitives
/- [core::num::nonzero::NonZeroU32]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33
+ Name pattern: core::num::nonzero::NonZeroU32 -/
axiom core.num.nonzero.NonZeroU32 : Type
/- The state type used in the state-error monad -/
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 1c95f7c9..363d751a 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -79,8 +79,8 @@ divergent def HashMap.clear_loop
Source: 'src/hashmap.rs', lines 80:4-80:27 -/
def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) :=
do
- let back ← HashMap.clear_loop T self.slots 0#usize
- Result.ret { self with num_entries := 0#usize, slots := back }
+ let hm ← HashMap.clear_loop T self.slots 0#usize
+ Result.ret { self with num_entries := 0#usize, slots := hm }
/- [hashmap::{hashmap::HashMap<T>}::len]:
Source: 'src/hashmap.rs', lines 90:4-90:30 -/
@@ -99,8 +99,8 @@ divergent def HashMap.insert_in_list_loop
then Result.ret (false, List.Cons ckey value tl)
else
do
- let (b, back) ← HashMap.insert_in_list_loop T key value tl
- Result.ret (b, List.Cons ckey cvalue back)
+ let (b, tl1) ← HashMap.insert_in_list_loop T key value tl
+ Result.ret (b, List.Cons ckey cvalue tl1)
| List.Nil => Result.ret (true, List.Cons key value List.Nil)
/- [hashmap::{hashmap::HashMap<T>}::insert_in_list]:
@@ -287,17 +287,17 @@ divergent def HashMap.get_mut_in_list_loop
| List.Cons ckey cvalue tl =>
if ckey = key
then
- let back_'a := fun ret => Result.ret (List.Cons ckey ret tl)
- Result.ret (cvalue, back_'a)
+ let back := fun ret => Result.ret (List.Cons ckey ret tl)
+ Result.ret (cvalue, back)
else
do
- let (t, back_'a) ← HashMap.get_mut_in_list_loop T tl key
- let back_'a1 :=
+ let (t, back) ← HashMap.get_mut_in_list_loop T tl key
+ let back1 :=
fun ret =>
do
- let tl1 ← back_'a ret
+ let tl1 ← back ret
Result.ret (List.Cons ckey cvalue tl1)
- Result.ret (t, back_'a1)
+ Result.ret (t, back1)
| List.Nil => Result.fail .panic
/- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]:
@@ -322,13 +322,13 @@ def HashMap.get_mut
alloc.vec.Vec.index_mut (List T) Usize
(core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots hash_mod
let (t, get_mut_in_list_back) ← HashMap.get_mut_in_list T l key
- let back_'a :=
+ let back :=
fun ret =>
do
let l1 ← get_mut_in_list_back ret
let v ← index_mut_back l1
Result.ret { self with slots := v }
- Result.ret (t, back_'a)
+ Result.ret (t, back)
/- [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
Source: 'src/hashmap.rs', lines 265:4-291:5 -/
@@ -345,8 +345,8 @@ divergent def HashMap.remove_from_list_loop
| List.Nil => Result.fail .panic
else
do
- let (o, back) ← HashMap.remove_from_list_loop T key tl
- Result.ret (o, List.Cons ckey t back)
+ let (o, tl1) ← HashMap.remove_from_list_loop T key tl
+ Result.ret (o, List.Cons ckey t tl1)
| List.Nil => Result.ret (none, List.Nil)
/- [hashmap::{hashmap::HashMap<T>}::remove_from_list]:
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index 6a6934b8..6fac6940 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -83,8 +83,8 @@ divergent def hashmap.HashMap.clear_loop
def hashmap.HashMap.clear
(T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) :=
do
- let back ← hashmap.HashMap.clear_loop T self.slots 0#usize
- Result.ret { self with num_entries := 0#usize, slots := back }
+ let hm ← hashmap.HashMap.clear_loop T self.slots 0#usize
+ Result.ret { self with num_entries := 0#usize, slots := hm }
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::len]:
Source: 'src/hashmap.rs', lines 90:4-90:30 -/
@@ -103,8 +103,8 @@ divergent def hashmap.HashMap.insert_in_list_loop
then Result.ret (false, hashmap.List.Cons ckey value tl)
else
do
- let (b, back) ← hashmap.HashMap.insert_in_list_loop T key value tl
- Result.ret (b, hashmap.List.Cons ckey cvalue back)
+ let (b, tl1) ← hashmap.HashMap.insert_in_list_loop T key value tl
+ Result.ret (b, hashmap.List.Cons ckey cvalue tl1)
| hashmap.List.Nil =>
Result.ret (true, hashmap.List.Cons key value hashmap.List.Nil)
@@ -302,17 +302,17 @@ divergent def hashmap.HashMap.get_mut_in_list_loop
| hashmap.List.Cons ckey cvalue tl =>
if ckey = key
then
- let back_'a := fun ret => Result.ret (hashmap.List.Cons ckey ret tl)
- Result.ret (cvalue, back_'a)
+ let back := fun ret => Result.ret (hashmap.List.Cons ckey ret tl)
+ Result.ret (cvalue, back)
else
do
- let (t, back_'a) ← hashmap.HashMap.get_mut_in_list_loop T tl key
- let back_'a1 :=
+ let (t, back) ← hashmap.HashMap.get_mut_in_list_loop T tl key
+ let back1 :=
fun ret =>
do
- let tl1 ← back_'a ret
+ let tl1 ← back ret
Result.ret (hashmap.List.Cons ckey cvalue tl1)
- Result.ret (t, back_'a1)
+ Result.ret (t, back1)
| hashmap.List.Nil => Result.fail .panic
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]:
@@ -338,13 +338,13 @@ def hashmap.HashMap.get_mut
(core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T)) self.slots
hash_mod
let (t, get_mut_in_list_back) ← hashmap.HashMap.get_mut_in_list T l key
- let back_'a :=
+ let back :=
fun ret =>
do
let l1 ← get_mut_in_list_back ret
let v ← index_mut_back l1
Result.ret { self with slots := v }
- Result.ret (t, back_'a)
+ Result.ret (t, back)
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0:
Source: 'src/hashmap.rs', lines 265:4-291:5 -/
@@ -364,8 +364,8 @@ divergent def hashmap.HashMap.remove_from_list_loop
| hashmap.List.Nil => Result.fail .panic
else
do
- let (o, back) ← hashmap.HashMap.remove_from_list_loop T key tl
- Result.ret (o, hashmap.List.Cons ckey t back)
+ let (o, tl1) ← hashmap.HashMap.remove_from_list_loop T key tl
+ Result.ret (o, hashmap.List.Cons ckey t tl1)
| hashmap.List.Nil => Result.ret (none, hashmap.List.Nil)
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]:
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index 0f3d77c2..27434db8 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -295,22 +295,22 @@ divergent def list_nth_mut_loop_pair_loop
| List.Cons x1 tl1 =>
if i = 0#u32
then
- let back_'a := fun ret => Result.ret (List.Cons ret tl0)
- let back_'b := fun ret => Result.ret (List.Cons ret tl1)
- Result.ret ((x0, x1), back_'a, back_'b)
+ let back'a := fun ret => Result.ret (List.Cons ret tl0)
+ let back'b := fun ret => Result.ret (List.Cons ret tl1)
+ Result.ret ((x0, x1), back'a, back'b)
else
do
let i1 ← i - 1#u32
- let (p, back_'a, back_'b) ← list_nth_mut_loop_pair_loop T tl0 tl1 i1
- let back_'a1 :=
+ let (p, back'a, back'b) ← list_nth_mut_loop_pair_loop T tl0 tl1 i1
+ let back'a1 :=
fun ret => do
- let tl01 ← back_'a ret
+ let tl01 ← back'a ret
Result.ret (List.Cons x0 tl01)
- let back_'b1 :=
+ let back'b1 :=
fun ret => do
- let tl11 ← back_'b ret
+ let tl11 ← back'b ret
Result.ret (List.Cons x1 tl11)
- Result.ret (p, back_'a1, back_'b1)
+ Result.ret (p, back'a1, back'b1)
| List.Nil => Result.fail .panic
| List.Nil => Result.fail .panic
@@ -356,21 +356,21 @@ divergent def list_nth_mut_loop_pair_merge_loop
| List.Cons x1 tl1 =>
if i = 0#u32
then
- let back_'a :=
+ let back :=
fun ret =>
let (t, t1) := ret
Result.ret (List.Cons t tl0, List.Cons t1 tl1)
- Result.ret ((x0, x1), back_'a)
+ Result.ret ((x0, x1), back)
else
do
let i1 ← i - 1#u32
- let (p, back_'a) ← list_nth_mut_loop_pair_merge_loop T tl0 tl1 i1
- let back_'a1 :=
+ let (p, back) ← list_nth_mut_loop_pair_merge_loop T tl0 tl1 i1
+ let back1 :=
fun ret =>
do
- let (tl01, tl11) ← back_'a ret
+ let (tl01, tl11) ← back ret
Result.ret (List.Cons x0 tl01, List.Cons x1 tl11)
- Result.ret (p, back_'a1)
+ Result.ret (p, back1)
| List.Nil => Result.fail .panic
| List.Nil => Result.fail .panic
@@ -417,17 +417,17 @@ divergent def list_nth_mut_shared_loop_pair_loop
| List.Cons x1 tl1 =>
if i = 0#u32
then
- let back_'a := fun ret => Result.ret (List.Cons ret tl0)
- Result.ret ((x0, x1), back_'a)
+ let back := fun ret => Result.ret (List.Cons ret tl0)
+ Result.ret ((x0, x1), back)
else
do
let i1 ← i - 1#u32
- let (p, back_'a) ← list_nth_mut_shared_loop_pair_loop T tl0 tl1 i1
- let back_'a1 :=
+ let (p, back) ← list_nth_mut_shared_loop_pair_loop T tl0 tl1 i1
+ let back1 :=
fun ret => do
- let tl01 ← back_'a ret
+ let tl01 ← back ret
Result.ret (List.Cons x0 tl01)
- Result.ret (p, back_'a1)
+ Result.ret (p, back1)
| List.Nil => Result.fail .panic
| List.Nil => Result.fail .panic
@@ -451,18 +451,17 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop
| List.Cons x1 tl1 =>
if i = 0#u32
then
- let back_'a := fun ret => Result.ret (List.Cons ret tl0)
- Result.ret ((x0, x1), back_'a)
+ let back := fun ret => Result.ret (List.Cons ret tl0)
+ Result.ret ((x0, x1), back)
else
do
let i1 ← i - 1#u32
- let (p, back_'a) ←
- list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i1
- let back_'a1 :=
+ let (p, back) ← list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i1
+ let back1 :=
fun ret => do
- let tl01 ← back_'a ret
+ let tl01 ← back ret
Result.ret (List.Cons x0 tl01)
- Result.ret (p, back_'a1)
+ Result.ret (p, back1)
| List.Nil => Result.fail .panic
| List.Nil => Result.fail .panic
@@ -486,17 +485,17 @@ divergent def list_nth_shared_mut_loop_pair_loop
| List.Cons x1 tl1 =>
if i = 0#u32
then
- let back_'b := fun ret => Result.ret (List.Cons ret tl1)
- Result.ret ((x0, x1), back_'b)
+ let back := fun ret => Result.ret (List.Cons ret tl1)
+ Result.ret ((x0, x1), back)
else
do
let i1 ← i - 1#u32
- let (p, back_'b) ← list_nth_shared_mut_loop_pair_loop T tl0 tl1 i1
- let back_'b1 :=
+ let (p, back) ← list_nth_shared_mut_loop_pair_loop T tl0 tl1 i1
+ let back1 :=
fun ret => do
- let tl11 ← back_'b ret
+ let tl11 ← back ret
Result.ret (List.Cons x1 tl11)
- Result.ret (p, back_'b1)
+ Result.ret (p, back1)
| List.Nil => Result.fail .panic
| List.Nil => Result.fail .panic
@@ -520,18 +519,17 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop
| List.Cons x1 tl1 =>
if i = 0#u32
then
- let back_'a := fun ret => Result.ret (List.Cons ret tl1)
- Result.ret ((x0, x1), back_'a)
+ let back := fun ret => Result.ret (List.Cons ret tl1)
+ Result.ret ((x0, x1), back)
else
do
let i1 ← i - 1#u32
- let (p, back_'a) ←
- list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i1
- let back_'a1 :=
+ let (p, back) ← list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i1
+ let back1 :=
fun ret => do
- let tl11 ← back_'a ret
+ let tl11 ← back ret
Result.ret (List.Cons x1 tl11)
- Result.ret (p, back_'a1)
+ Result.ret (p, back1)
| List.Nil => Result.fail .panic
| List.Nil => Result.fail .panic
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 5f9ec0f2..b90f6aef 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -331,10 +331,10 @@ def choose
Result (T × (T → Result (T × T)))
:=
if b
- then let back_'a := fun ret => Result.ret (ret, y)
- Result.ret (x, back_'a)
- else let back_'a := fun ret => Result.ret (x, ret)
- Result.ret (y, back_'a)
+ then let back := fun ret => Result.ret (ret, y)
+ Result.ret (x, back)
+ else let back := fun ret => Result.ret (x, ret)
+ Result.ret (y, back)
/- [no_nested_borrows::choose_test]:
Source: 'src/no_nested_borrows.rs', lines 282:0-282:20 -/
@@ -406,18 +406,18 @@ divergent def list_nth_mut
| List.Cons x tl =>
if i = 0#u32
then
- let back_'a := fun ret => Result.ret (List.Cons ret tl)
- Result.ret (x, back_'a)
+ let back := fun ret => Result.ret (List.Cons ret tl)
+ Result.ret (x, back)
else
do
let i1 ← i - 1#u32
let (t, list_nth_mut_back) ← list_nth_mut T tl i1
- let back_'a :=
+ let back :=
fun ret =>
do
let tl1 ← list_nth_mut_back ret
Result.ret (List.Cons x tl1)
- Result.ret (t, back_'a)
+ Result.ret (t, back)
| List.Nil => Result.fail .panic
/- [no_nested_borrows::list_rev_aux]:
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index 924ff36c..5b00aa83 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -29,10 +29,10 @@ def choose
Result (T × (T → Result (T × T)))
:=
if b
- then let back_'a := fun ret => Result.ret (ret, y)
- Result.ret (x, back_'a)
- else let back_'a := fun ret => Result.ret (x, ret)
- Result.ret (y, back_'a)
+ then let back := fun ret => Result.ret (ret, y)
+ Result.ret (x, back)
+ else let back := fun ret => Result.ret (x, ret)
+ Result.ret (y, back)
/- [paper::test_choose]:
Source: 'src/paper.rs', lines 23:0-23:20 -/
@@ -68,18 +68,18 @@ divergent def list_nth_mut
| List.Cons x tl =>
if i = 0#u32
then
- let back_'a := fun ret => Result.ret (List.Cons ret tl)
- Result.ret (x, back_'a)
+ let back := fun ret => Result.ret (List.Cons ret tl)
+ Result.ret (x, back)
else
do
let i1 ← i - 1#u32
let (t, list_nth_mut_back) ← list_nth_mut T tl i1
- let back_'a :=
+ let back :=
fun ret =>
do
let tl1 ← list_nth_mut_back ret
Result.ret (List.Cons x tl1)
- Result.ret (t, back_'a)
+ Result.ret (t, back)
| List.Nil => Result.fail .panic
/- [paper::sum]:
diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index 59c557a0..c657237f 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -24,12 +24,12 @@ divergent def get_list_at_x
else
do
let (l, get_list_at_x_back) ← get_list_at_x tl x
- let back_'a :=
+ let back :=
fun ret =>
do
let tl1 ← get_list_at_x_back ret
Result.ret (List.Cons hd tl1)
- Result.ret (l, back_'a)
+ Result.ret (l, back)
| List.Nil => Result.ret (List.Nil, Result.ret)
end polonius_list
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index acddd1a9..766b109d 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -512,7 +512,8 @@ structure Foo (T U : Type) where
y : U
/- [core::result::Result]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21 -/
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/result.rs', lines 502:0-502:21
+ Name pattern: core::result::Result -/
inductive core.result.Result (T E : Type) :=
| Ok : T → core.result.Result T E
| Err : E → core.result.Result T E