summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/lean/Array.lean26
-rw-r--r--tests/lean/BetreeMain/Funs.lean42
-rw-r--r--tests/lean/BetreeMain/Types.lean4
-rw-r--r--tests/lean/BetreeMain/TypesExternal.lean7
-rw-r--r--tests/lean/BetreeMain/TypesExternal_Template.lean9
-rw-r--r--tests/lean/External/Funs.lean8
-rw-r--r--tests/lean/External/Types.lean8
-rw-r--r--tests/lean/External/TypesExternal.lean11
-rw-r--r--tests/lean/External/TypesExternal_Template.lean13
-rw-r--r--tests/lean/Hashmap/Funs.lean40
-rw-r--r--tests/lean/HashmapMain/Funs.lean38
-rw-r--r--tests/lean/HashmapMain/Types.lean4
-rw-r--r--tests/lean/HashmapMain/TypesExternal.lean7
-rw-r--r--tests/lean/HashmapMain/TypesExternal_Template.lean9
-rw-r--r--tests/lean/Loops.lean184
-rw-r--r--tests/lean/NoNestedBorrows.lean133
-rw-r--r--tests/lean/Paper.lean32
-rw-r--r--tests/lean/PoloniusList.lean8
-rw-r--r--tests/lean/Traits.lean10
19 files changed, 314 insertions, 279 deletions
diff --git a/tests/lean/Array.lean b/tests/lean/Array.lean
index 4832f469..b49add96 100644
--- a/tests/lean/Array.lean
+++ b/tests/lean/Array.lean
@@ -31,10 +31,10 @@ def array_to_mut_slice_ (T : Type) (s : Array T 32#usize) : Result (Slice T) :=
/- [array::array_to_mut_slice_]: backward function 0
Source: 'src/array.rs', lines 21:0-21:58 -/
def array_to_mut_slice__back
- (T : Type) (s : Array T 32#usize) (ret0 : Slice T) :
+ (T : Type) (s : Array T 32#usize) (ret : Slice T) :
Result (Array T 32#usize)
:=
- Array.from_slice T 32#usize s ret0
+ Array.from_slice T 32#usize s ret
/- [array::array_len]: forward function
Source: 'src/array.rs', lines 25:0-25:40 -/
@@ -82,10 +82,10 @@ def index_mut_array (T : Type) (s : Array T 32#usize) (i : Usize) : Result T :=
/- [array::index_mut_array]: backward function 0
Source: 'src/array.rs', lines 52:0-52:62 -/
def index_mut_array_back
- (T : Type) (s : Array T 32#usize) (i : Usize) (ret0 : T) :
+ (T : Type) (s : Array T 32#usize) (i : Usize) (ret : T) :
Result (Array T 32#usize)
:=
- Array.update_usize T 32#usize s i ret0
+ Array.update_usize T 32#usize s i ret
/- [array::index_slice]: forward function
Source: 'src/array.rs', lines 56:0-56:46 -/
@@ -100,8 +100,8 @@ def index_mut_slice (T : Type) (s : Slice T) (i : Usize) : Result T :=
/- [array::index_mut_slice]: backward function 0
Source: 'src/array.rs', lines 60:0-60:58 -/
def index_mut_slice_back
- (T : Type) (s : Slice T) (i : Usize) (ret0 : T) : Result (Slice T) :=
- Slice.update_usize T s i ret0
+ (T : Type) (s : Slice T) (i : Usize) (ret : T) : Result (Slice T) :=
+ Slice.update_usize T s i ret
/- [array::slice_subslice_shared_]: forward function
Source: 'src/array.rs', lines 64:0-64:70 -/
@@ -122,12 +122,12 @@ def slice_subslice_mut_
/- [array::slice_subslice_mut_]: backward function 0
Source: 'src/array.rs', lines 68:0-68:75 -/
def slice_subslice_mut__back
- (x : Slice U32) (y : Usize) (z : Usize) (ret0 : Slice U32) :
+ (x : Slice U32) (y : Usize) (z : Usize) (ret : Slice U32) :
Result (Slice U32)
:=
core.slice.index.Slice.index_mut_back U32 (core.ops.range.Range Usize)
(core.slice.index.SliceIndexRangeUsizeSliceTInst U32) x
- { start := y, end_ := z } ret0
+ { start := y, end_ := z } ret
/- [array::array_to_slice_shared_]: forward function
Source: 'src/array.rs', lines 72:0-72:54 -/
@@ -142,8 +142,8 @@ def array_to_slice_mut_ (x : Array U32 32#usize) : Result (Slice U32) :=
/- [array::array_to_slice_mut_]: backward function 0
Source: 'src/array.rs', lines 76:0-76:59 -/
def array_to_slice_mut__back
- (x : Array U32 32#usize) (ret0 : Slice U32) : Result (Array U32 32#usize) :=
- Array.from_slice U32 32#usize x ret0
+ (x : Array U32 32#usize) (ret : Slice U32) : Result (Array U32 32#usize) :=
+ Array.from_slice U32 32#usize x ret
/- [array::array_subslice_shared_]: forward function
Source: 'src/array.rs', lines 80:0-80:74 -/
@@ -166,13 +166,13 @@ def array_subslice_mut_
/- [array::array_subslice_mut_]: backward function 0
Source: 'src/array.rs', lines 84:0-84:79 -/
def array_subslice_mut__back
- (x : Array U32 32#usize) (y : Usize) (z : Usize) (ret0 : Slice U32) :
+ (x : Array U32 32#usize) (y : Usize) (z : Usize) (ret : Slice U32) :
Result (Array U32 32#usize)
:=
core.array.Array.index_mut_back U32 (core.ops.range.Range Usize) 32#usize
(core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize)
(core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x
- { start := y, end_ := z } ret0
+ { start := y, end_ := z } ret
/- [array::index_slice_0]: forward function
Source: 'src/array.rs', lines 88:0-88:38 -/
@@ -417,7 +417,7 @@ def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 :=
let i := Slice.len U32 s
let i0 := Slice.len U32 s2
if not (i = i0)
- then Result.fail Error.panic
+ then Result.fail .panic
else sum2_loop s s2 0#u32 0#usize
/- [array::f0]: forward function
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 45548884..4c862225 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -121,7 +121,7 @@ divergent def betree.List.split_at
let (ls0, ls1) := p
let l := ls0
Result.ret (betree.List.Cons hd l, ls1)
- | betree.List.Nil => Result.fail Error.panic
+ | betree.List.Nil => Result.fail .panic
/- [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function
(there is a single backward function, and the forward function returns ())
@@ -138,7 +138,7 @@ def betree.List.pop_front (T : Type) (self : betree.List T) : Result T :=
let ls := core.mem.replace (betree.List T) self betree.List.Nil
match ls with
| betree.List.Cons x tl => Result.ret x
- | betree.List.Nil => Result.fail Error.panic
+ | betree.List.Nil => Result.fail .panic
/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0
Source: 'src/betree.rs', lines 306:4-306:32 -/
@@ -147,14 +147,14 @@ def betree.List.pop_front_back
let ls := core.mem.replace (betree.List T) self betree.List.Nil
match ls with
| betree.List.Cons x tl => Result.ret tl
- | betree.List.Nil => Result.fail Error.panic
+ | betree.List.Nil => Result.fail .panic
/- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function
Source: 'src/betree.rs', lines 318:4-318:22 -/
def betree.List.hd (T : Type) (self : betree.List T) : Result T :=
match self with
| betree.List.Cons hd l => Result.ret hd
- | betree.List.Nil => Result.fail Error.panic
+ | betree.List.Nil => Result.fail .panic
/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function
Source: 'src/betree.rs', lines 327:4-327:44 -/
@@ -241,20 +241,20 @@ divergent def betree.Node.lookup_first_message_for_key
Source: 'src/betree.rs', lines 789:4-792:34 -/
divergent def betree.Node.lookup_first_message_for_key_back
(key : U64) (msgs : betree.List (U64 × betree.Message))
- (ret0 : betree.List (U64 × betree.Message)) :
+ (ret : betree.List (U64 × betree.Message)) :
Result (betree.List (U64 × betree.Message))
:=
match msgs with
| betree.List.Cons x next_msgs =>
let (i, m) := x
if i >= key
- then Result.ret ret0
+ then Result.ret ret
else
do
let next_msgs0 ←
- betree.Node.lookup_first_message_for_key_back key next_msgs ret0
+ betree.Node.lookup_first_message_for_key_back key next_msgs ret
Result.ret (betree.List.Cons (i, m) next_msgs0)
- | betree.List.Nil => Result.ret ret0
+ | betree.List.Nil => Result.ret ret
/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function
Source: 'src/betree.rs', lines 819:4-819:90 -/
@@ -271,8 +271,8 @@ divergent def betree.Node.apply_upserts
let msg ← betree.List.pop_front (U64 × betree.Message) msgs
let (_, m) := msg
match m with
- | betree.Message.Insert i => Result.fail Error.panic
- | betree.Message.Delete => Result.fail Error.panic
+ | betree.Message.Insert i => Result.fail .panic
+ | betree.Message.Delete => Result.fail .panic
| betree.Message.Upsert s =>
do
let v ← betree.upsert_update prev s
@@ -302,8 +302,8 @@ divergent def betree.Node.apply_upserts_back
let msg ← betree.List.pop_front (U64 × betree.Message) msgs
let (_, m) := msg
match m with
- | betree.Message.Insert i => Result.fail Error.panic
- | betree.Message.Delete => Result.fail Error.panic
+ | betree.Message.Insert i => Result.fail .panic
+ | betree.Message.Delete => Result.fail .panic
| betree.Message.Upsert s =>
do
let v ← betree.upsert_update prev s
@@ -542,7 +542,7 @@ divergent def betree.Node.lookup_first_message_after_key
Source: 'src/betree.rs', lines 689:4-692:34 -/
divergent def betree.Node.lookup_first_message_after_key_back
(key : U64) (msgs : betree.List (U64 × betree.Message))
- (ret0 : betree.List (U64 × betree.Message)) :
+ (ret : betree.List (U64 × betree.Message)) :
Result (betree.List (U64 × betree.Message))
:=
match msgs with
@@ -552,10 +552,10 @@ divergent def betree.Node.lookup_first_message_after_key_back
then
do
let next_msgs0 ←
- betree.Node.lookup_first_message_after_key_back key next_msgs ret0
+ betree.Node.lookup_first_message_after_key_back key next_msgs ret
Result.ret (betree.List.Cons (k, m) next_msgs0)
- else Result.ret ret0
- | betree.List.Nil => Result.ret ret0
+ else Result.ret ret
+ | betree.List.Nil => Result.ret ret
/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function
(there is a single backward function, and the forward function returns ())
@@ -658,19 +658,19 @@ divergent def betree.Node.lookup_mut_in_bindings
Source: 'src/betree.rs', lines 653:4-656:32 -/
divergent def betree.Node.lookup_mut_in_bindings_back
(key : U64) (bindings : betree.List (U64 × U64))
- (ret0 : betree.List (U64 × U64)) :
+ (ret : betree.List (U64 × U64)) :
Result (betree.List (U64 × U64))
:=
match bindings with
| betree.List.Cons hd tl =>
let (i, i0) := hd
if i >= key
- then Result.ret ret0
+ then Result.ret ret
else
do
- let tl0 ← betree.Node.lookup_mut_in_bindings_back key tl ret0
+ let tl0 ← betree.Node.lookup_mut_in_bindings_back key tl ret
Result.ret (betree.List.Cons (i, i0) tl0)
- | betree.List.Nil => Result.ret ret0
+ | betree.List.Nil => Result.ret ret
/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function
(there is a single backward function, and the forward function returns ())
@@ -1069,6 +1069,6 @@ def main : Result Unit :=
Result.ret ()
/- Unit test for [betree_main::main] -/
-#assert (main == .ret ())
+#assert (main == Result.ret ())
end betree_main
diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/BetreeMain/Types.lean
index 6e528437..877508f6 100644
--- a/tests/lean/BetreeMain/Types.lean
+++ b/tests/lean/BetreeMain/Types.lean
@@ -1,6 +1,7 @@
-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [betree_main]: type definitions
import Base
+import BetreeMain.TypesExternal
open Primitives
namespace betree_main
@@ -63,7 +64,4 @@ structure betree.BeTree where
node_id_cnt : betree.NodeIdCounter
root : betree.Node
-/- The state type used in the state-error monad -/
-axiom State : Type
-
end betree_main
diff --git a/tests/lean/BetreeMain/TypesExternal.lean b/tests/lean/BetreeMain/TypesExternal.lean
new file mode 100644
index 00000000..1701eaaf
--- /dev/null
+++ b/tests/lean/BetreeMain/TypesExternal.lean
@@ -0,0 +1,7 @@
+-- [betree_main]: external types.
+import Base
+open Primitives
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
diff --git a/tests/lean/BetreeMain/TypesExternal_Template.lean b/tests/lean/BetreeMain/TypesExternal_Template.lean
new file mode 100644
index 00000000..bbac7e99
--- /dev/null
+++ b/tests/lean/BetreeMain/TypesExternal_Template.lean
@@ -0,0 +1,9 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [betree_main]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
+import Base
+open Primitives
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index e5655c7e..48ec6ad5 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -45,7 +45,7 @@ def test_vec : Result Unit :=
Result.ret ()
/- Unit test for [external::test_vec] -/
-#assert (test_vec == .ret ())
+#assert (test_vec == Result.ret ())
/- [external::custom_swap]: forward function
Source: 'src/external.rs', lines 24:0-24:66 -/
@@ -60,14 +60,14 @@ def custom_swap
/- [external::custom_swap]: backward function 0
Source: 'src/external.rs', lines 24:0-24:66 -/
def custom_swap_back
- (T : Type) (x : T) (y : T) (st : State) (ret0 : T) (st0 : State) :
+ (T : Type) (x : T) (y : T) (st : State) (ret : T) (st0 : State) :
Result (State × (T × T))
:=
do
let (st1, _) ← core.mem.swap T x y st
let (st2, _) ← core.mem.swap_back0 T x y st st1
let (_, y0) ← core.mem.swap_back1 T x y st st2
- Result.ret (st0, (ret0, y0))
+ Result.ret (st0, (ret, y0))
/- [external::test_custom_swap]: forward function
Source: 'src/external.rs', lines 29:0-29:59 -/
@@ -92,7 +92,7 @@ def test_swap_non_zero (x : U32) (st : State) : Result (State × U32) :=
let (st0, _) ← swap U32 x 0#u32 st
let (st1, (x0, _)) ← swap_back U32 x 0#u32 st st0
if x0 = 0#u32
- then Result.fail Error.panic
+ then Result.fail .panic
else Result.ret (st1, x0)
end external
diff --git a/tests/lean/External/Types.lean b/tests/lean/External/Types.lean
index 40f20cda..961f3e8a 100644
--- a/tests/lean/External/Types.lean
+++ b/tests/lean/External/Types.lean
@@ -1,15 +1,9 @@
-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [external]: type definitions
import Base
+import External.TypesExternal
open Primitives
namespace external
-/- [core::num::nonzero::NonZeroU32]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/
-axiom core.num.nonzero.NonZeroU32 : Type
-
-/- The state type used in the state-error monad -/
-axiom State : Type
-
end external
diff --git a/tests/lean/External/TypesExternal.lean b/tests/lean/External/TypesExternal.lean
new file mode 100644
index 00000000..7c30f792
--- /dev/null
+++ b/tests/lean/External/TypesExternal.lean
@@ -0,0 +1,11 @@
+-- [external]: external types.
+import Base
+open Primitives
+
+/- [core::num::nonzero::NonZeroU32]
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/
+axiom core.num.nonzero.NonZeroU32 : Type
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
diff --git a/tests/lean/External/TypesExternal_Template.lean b/tests/lean/External/TypesExternal_Template.lean
new file mode 100644
index 00000000..85fef236
--- /dev/null
+++ b/tests/lean/External/TypesExternal_Template.lean
@@ -0,0 +1,13 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [external]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
+import Base
+open Primitives
+
+/- [core::num::nonzero::NonZeroU32]
+ Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/
+axiom core.num.nonzero.NonZeroU32 : Type
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 95c501f6..e03981a2 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -295,7 +295,7 @@ divergent def HashMap.get_in_list_loop
if ckey = key
then Result.ret cvalue
else HashMap.get_in_list_loop T key tl
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
/- [hashmap::{hashmap::HashMap<T>}::get_in_list]: forward function
Source: 'src/hashmap.rs', lines 224:4-224:70 -/
@@ -324,7 +324,7 @@ divergent def HashMap.get_mut_in_list_loop
if ckey = key
then Result.ret cvalue
else HashMap.get_mut_in_list_loop T tl key
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
/- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: forward function
Source: 'src/hashmap.rs', lines 245:4-245:86 -/
@@ -335,22 +335,22 @@ def HashMap.get_mut_in_list
/- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: loop 0: backward function 0
Source: 'src/hashmap.rs', lines 245:4-254:5 -/
divergent def HashMap.get_mut_in_list_loop_back
- (T : Type) (ls : List T) (key : Usize) (ret0 : T) : Result (List T) :=
+ (T : Type) (ls : List T) (key : Usize) (ret : T) : Result (List T) :=
match ls with
| List.Cons ckey cvalue tl =>
if ckey = key
- then Result.ret (List.Cons ckey ret0 tl)
+ then Result.ret (List.Cons ckey ret tl)
else
do
- let tl0 ← HashMap.get_mut_in_list_loop_back T tl key ret0
+ let tl0 ← HashMap.get_mut_in_list_loop_back T tl key ret
Result.ret (List.Cons ckey cvalue tl0)
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
/- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]: backward function 0
Source: 'src/hashmap.rs', lines 245:4-245:86 -/
def HashMap.get_mut_in_list_back
- (T : Type) (ls : List T) (key : Usize) (ret0 : T) : Result (List T) :=
- HashMap.get_mut_in_list_loop_back T ls key ret0
+ (T : Type) (ls : List T) (key : Usize) (ret : T) : Result (List T) :=
+ HashMap.get_mut_in_list_loop_back T ls key ret
/- [hashmap::{hashmap::HashMap<T>}::get_mut]: forward function
Source: 'src/hashmap.rs', lines 257:4-257:67 -/
@@ -368,9 +368,7 @@ def HashMap.get_mut (T : Type) (self : HashMap T) (key : Usize) : Result T :=
/- [hashmap::{hashmap::HashMap<T>}::get_mut]: backward function 0
Source: 'src/hashmap.rs', lines 257:4-257:67 -/
def HashMap.get_mut_back
- (T : Type) (self : HashMap T) (key : Usize) (ret0 : T) :
- Result (HashMap T)
- :=
+ (T : Type) (self : HashMap T) (key : Usize) (ret : T) : Result (HashMap T) :=
do
let hash ← hash_key key
let i := alloc.vec.Vec.len (List T) self.slots
@@ -379,7 +377,7 @@ def HashMap.get_mut_back
alloc.vec.Vec.index_mut (List T) Usize
(core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots
hash_mod
- let l0 ← HashMap.get_mut_in_list_back T l key ret0
+ let l0 ← HashMap.get_mut_in_list_back T l key ret
let v ←
alloc.vec.Vec.index_mut_back (List T) Usize
(core.slice.index.SliceIndexUsizeSliceTInst (List T)) self.slots
@@ -397,7 +395,7 @@ divergent def HashMap.remove_from_list_loop
let mv_ls := core.mem.replace (List T) (List.Cons ckey t tl) List.Nil
match mv_ls with
| List.Cons i cvalue tl0 => Result.ret (some cvalue)
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
else HashMap.remove_from_list_loop T key tl
| List.Nil => Result.ret none
@@ -418,7 +416,7 @@ divergent def HashMap.remove_from_list_loop_back
let mv_ls := core.mem.replace (List T) (List.Cons ckey t tl) List.Nil
match mv_ls with
| List.Cons i cvalue tl0 => Result.ret tl0
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
else
do
let tl0 ← HashMap.remove_from_list_loop_back T key tl
@@ -493,37 +491,37 @@ def test1 : Result Unit :=
let hm3 ← HashMap.insert U64 hm2 1056#usize 256#u64
let i ← HashMap.get U64 hm3 128#usize
if not (i = 18#u64)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let hm4 ← HashMap.get_mut_back U64 hm3 1024#usize 56#u64
let i0 ← HashMap.get U64 hm4 1024#usize
if not (i0 = 56#u64)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let x ← HashMap.remove U64 hm4 1024#usize
match x with
- | none => Result.fail Error.panic
+ | none => Result.fail .panic
| some x0 =>
if not (x0 = 56#u64)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let hm5 ← HashMap.remove_back U64 hm4 1024#usize
let i1 ← HashMap.get U64 hm5 0#usize
if not (i1 = 42#u64)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let i2 ← HashMap.get U64 hm5 128#usize
if not (i2 = 18#u64)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let i3 ← HashMap.get U64 hm5 1056#usize
if not (i3 = 256#u64)
- then Result.fail Error.panic
+ then Result.fail .panic
else Result.ret ()
end hashmap
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index abe84bbf..f87ad355 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -309,7 +309,7 @@ divergent def hashmap.HashMap.get_in_list_loop
if ckey = key
then Result.ret cvalue
else hashmap.HashMap.get_in_list_loop T key tl
- | hashmap.List.Nil => Result.fail Error.panic
+ | hashmap.List.Nil => Result.fail .panic
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_in_list]: forward function
Source: 'src/hashmap.rs', lines 224:4-224:70 -/
@@ -340,7 +340,7 @@ divergent def hashmap.HashMap.get_mut_in_list_loop
if ckey = key
then Result.ret cvalue
else hashmap.HashMap.get_mut_in_list_loop T tl key
- | hashmap.List.Nil => Result.fail Error.panic
+ | hashmap.List.Nil => Result.fail .panic
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: forward function
Source: 'src/hashmap.rs', lines 245:4-245:86 -/
@@ -351,26 +351,26 @@ def hashmap.HashMap.get_mut_in_list
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: loop 0: backward function 0
Source: 'src/hashmap.rs', lines 245:4-254:5 -/
divergent def hashmap.HashMap.get_mut_in_list_loop_back
- (T : Type) (ls : hashmap.List T) (key : Usize) (ret0 : T) :
+ (T : Type) (ls : hashmap.List T) (key : Usize) (ret : T) :
Result (hashmap.List T)
:=
match ls with
| hashmap.List.Cons ckey cvalue tl =>
if ckey = key
- then Result.ret (hashmap.List.Cons ckey ret0 tl)
+ then Result.ret (hashmap.List.Cons ckey ret tl)
else
do
- let tl0 ← hashmap.HashMap.get_mut_in_list_loop_back T tl key ret0
+ let tl0 ← hashmap.HashMap.get_mut_in_list_loop_back T tl key ret
Result.ret (hashmap.List.Cons ckey cvalue tl0)
- | hashmap.List.Nil => Result.fail Error.panic
+ | hashmap.List.Nil => Result.fail .panic
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]: backward function 0
Source: 'src/hashmap.rs', lines 245:4-245:86 -/
def hashmap.HashMap.get_mut_in_list_back
- (T : Type) (ls : hashmap.List T) (key : Usize) (ret0 : T) :
+ (T : Type) (ls : hashmap.List T) (key : Usize) (ret : T) :
Result (hashmap.List T)
:=
- hashmap.HashMap.get_mut_in_list_loop_back T ls key ret0
+ hashmap.HashMap.get_mut_in_list_loop_back T ls key ret
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]: forward function
Source: 'src/hashmap.rs', lines 257:4-257:67 -/
@@ -389,7 +389,7 @@ def hashmap.HashMap.get_mut
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut]: backward function 0
Source: 'src/hashmap.rs', lines 257:4-257:67 -/
def hashmap.HashMap.get_mut_back
- (T : Type) (self : hashmap.HashMap T) (key : Usize) (ret0 : T) :
+ (T : Type) (self : hashmap.HashMap T) (key : Usize) (ret : T) :
Result (hashmap.HashMap T)
:=
do
@@ -400,7 +400,7 @@ def hashmap.HashMap.get_mut_back
alloc.vec.Vec.index_mut (hashmap.List T) Usize
(core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T))
self.slots hash_mod
- let l0 ← hashmap.HashMap.get_mut_in_list_back T l key ret0
+ let l0 ← hashmap.HashMap.get_mut_in_list_back T l key ret
let v ←
alloc.vec.Vec.index_mut_back (hashmap.List T) Usize
(core.slice.index.SliceIndexUsizeSliceTInst (hashmap.List T))
@@ -420,7 +420,7 @@ divergent def hashmap.HashMap.remove_from_list_loop
hashmap.List.Nil
match mv_ls with
| hashmap.List.Cons i cvalue tl0 => Result.ret (some cvalue)
- | hashmap.List.Nil => Result.fail Error.panic
+ | hashmap.List.Nil => Result.fail .panic
else hashmap.HashMap.remove_from_list_loop T key tl
| hashmap.List.Nil => Result.ret none
@@ -443,7 +443,7 @@ divergent def hashmap.HashMap.remove_from_list_loop_back
hashmap.List.Nil
match mv_ls with
| hashmap.List.Cons i cvalue tl0 => Result.ret tl0
- | hashmap.List.Nil => Result.fail Error.panic
+ | hashmap.List.Nil => Result.fail .panic
else
do
let tl0 ← hashmap.HashMap.remove_from_list_loop_back T key tl
@@ -520,37 +520,37 @@ def hashmap.test1 : Result Unit :=
let hm3 ← hashmap.HashMap.insert U64 hm2 1056#usize 256#u64
let i ← hashmap.HashMap.get U64 hm3 128#usize
if not (i = 18#u64)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let hm4 ← hashmap.HashMap.get_mut_back U64 hm3 1024#usize 56#u64
let i0 ← hashmap.HashMap.get U64 hm4 1024#usize
if not (i0 = 56#u64)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let x ← hashmap.HashMap.remove U64 hm4 1024#usize
match x with
- | none => Result.fail Error.panic
+ | none => Result.fail .panic
| some x0 =>
if not (x0 = 56#u64)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let hm5 ← hashmap.HashMap.remove_back U64 hm4 1024#usize
let i1 ← hashmap.HashMap.get U64 hm5 0#usize
if not (i1 = 42#u64)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let i2 ← hashmap.HashMap.get U64 hm5 128#usize
if not (i2 = 18#u64)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let i3 ← hashmap.HashMap.get U64 hm5 1056#usize
if not (i3 = 256#u64)
- then Result.fail Error.panic
+ then Result.fail .panic
else Result.ret ()
/- [hashmap_main::insert_on_disk]: forward function
diff --git a/tests/lean/HashmapMain/Types.lean b/tests/lean/HashmapMain/Types.lean
index f7be6719..ae9ac999 100644
--- a/tests/lean/HashmapMain/Types.lean
+++ b/tests/lean/HashmapMain/Types.lean
@@ -1,6 +1,7 @@
-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [hashmap_main]: type definitions
import Base
+import HashmapMain.TypesExternal
open Primitives
namespace hashmap_main
@@ -19,7 +20,4 @@ structure hashmap.HashMap (T : Type) where
max_load : Usize
slots : alloc.vec.Vec (hashmap.List T)
-/- The state type used in the state-error monad -/
-axiom State : Type
-
end hashmap_main
diff --git a/tests/lean/HashmapMain/TypesExternal.lean b/tests/lean/HashmapMain/TypesExternal.lean
new file mode 100644
index 00000000..4e1cdbe9
--- /dev/null
+++ b/tests/lean/HashmapMain/TypesExternal.lean
@@ -0,0 +1,7 @@
+-- [hashmap_main]: external types.
+import Base
+open Primitives
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
diff --git a/tests/lean/HashmapMain/TypesExternal_Template.lean b/tests/lean/HashmapMain/TypesExternal_Template.lean
new file mode 100644
index 00000000..cfa8bbb1
--- /dev/null
+++ b/tests/lean/HashmapMain/TypesExternal_Template.lean
@@ -0,0 +1,9 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [hashmap_main]: external types.
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
+import Base
+open Primitives
+
+/- The state type used in the state-error monad -/
+axiom State : Type
+
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index ae1d87aa..08aa08a5 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -107,7 +107,7 @@ divergent def list_nth_mut_loop_loop
else do
let i0 ← i - 1#u32
list_nth_mut_loop_loop T tl i0
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_mut_loop]: forward function
Source: 'src/loops.rs', lines 78:0-78:71 -/
@@ -117,23 +117,23 @@ def list_nth_mut_loop (T : Type) (ls : List T) (i : U32) : Result T :=
/- [loops::list_nth_mut_loop]: loop 0: backward function 0
Source: 'src/loops.rs', lines 78:0-88:1 -/
divergent def list_nth_mut_loop_loop_back
- (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) :=
+ (T : Type) (ls : List T) (i : U32) (ret : T) : Result (List T) :=
match ls with
| List.Cons x tl =>
if i = 0#u32
- then Result.ret (List.Cons ret0 tl)
+ then Result.ret (List.Cons ret tl)
else
do
let i0 ← i - 1#u32
- let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret0
+ let tl0 ← list_nth_mut_loop_loop_back T tl i0 ret
Result.ret (List.Cons x tl0)
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_mut_loop]: backward function 0
Source: 'src/loops.rs', lines 78:0-78:71 -/
def list_nth_mut_loop_back
- (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) :=
- list_nth_mut_loop_loop_back T ls i ret0
+ (T : Type) (ls : List T) (i : U32) (ret : T) : Result (List T) :=
+ list_nth_mut_loop_loop_back T ls i ret
/- [loops::list_nth_shared_loop]: loop 0: forward function
Source: 'src/loops.rs', lines 91:0-101:1 -/
@@ -146,7 +146,7 @@ divergent def list_nth_shared_loop_loop
else do
let i0 ← i - 1#u32
list_nth_shared_loop_loop T tl i0
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_shared_loop]: forward function
Source: 'src/loops.rs', lines 91:0-91:66 -/
@@ -160,7 +160,7 @@ divergent def get_elem_mut_loop (x : Usize) (ls : List Usize) : Result Usize :=
| List.Cons y tl => if y = x
then Result.ret y
else get_elem_mut_loop x tl
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
/- [loops::get_elem_mut]: forward function
Source: 'src/loops.rs', lines 103:0-103:73 -/
@@ -175,28 +175,28 @@ def get_elem_mut
/- [loops::get_elem_mut]: loop 0: backward function 0
Source: 'src/loops.rs', lines 103:0-117:1 -/
divergent def get_elem_mut_loop_back
- (x : Usize) (ls : List Usize) (ret0 : Usize) : Result (List Usize) :=
+ (x : Usize) (ls : List Usize) (ret : Usize) : Result (List Usize) :=
match ls with
| List.Cons y tl =>
if y = x
- then Result.ret (List.Cons ret0 tl)
+ then Result.ret (List.Cons ret tl)
else
do
- let tl0 ← get_elem_mut_loop_back x tl ret0
+ let tl0 ← get_elem_mut_loop_back x tl ret
Result.ret (List.Cons y tl0)
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
/- [loops::get_elem_mut]: backward function 0
Source: 'src/loops.rs', lines 103:0-103:73 -/
def get_elem_mut_back
- (slots : alloc.vec.Vec (List Usize)) (x : Usize) (ret0 : Usize) :
+ (slots : alloc.vec.Vec (List Usize)) (x : Usize) (ret : Usize) :
Result (alloc.vec.Vec (List Usize))
:=
do
let l ←
alloc.vec.Vec.index_mut (List Usize) Usize
(core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize
- let l0 ← get_elem_mut_loop_back x l ret0
+ let l0 ← get_elem_mut_loop_back x l ret
alloc.vec.Vec.index_mut_back (List Usize) Usize
(core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize
l0
@@ -209,7 +209,7 @@ divergent def get_elem_shared_loop
| List.Cons y tl => if y = x
then Result.ret y
else get_elem_shared_loop x tl
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
/- [loops::get_elem_shared]: forward function
Source: 'src/loops.rs', lines 119:0-119:68 -/
@@ -228,8 +228,8 @@ def id_mut (T : Type) (ls : List T) : Result (List T) :=
/- [loops::id_mut]: backward function 0
Source: 'src/loops.rs', lines 135:0-135:50 -/
-def id_mut_back (T : Type) (ls : List T) (ret0 : List T) : Result (List T) :=
- Result.ret ret0
+def id_mut_back (T : Type) (ls : List T) (ret : List T) : Result (List T) :=
+ Result.ret ret
/- [loops::id_shared]: forward function
Source: 'src/loops.rs', lines 139:0-139:45 -/
@@ -247,7 +247,7 @@ divergent def list_nth_mut_loop_with_id_loop
else do
let i0 ← i - 1#u32
list_nth_mut_loop_with_id_loop T i0 tl
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_mut_loop_with_id]: forward function
Source: 'src/loops.rs', lines 144:0-144:75 -/
@@ -259,25 +259,25 @@ def list_nth_mut_loop_with_id (T : Type) (ls : List T) (i : U32) : Result T :=
/- [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0
Source: 'src/loops.rs', lines 144:0-155:1 -/
divergent def list_nth_mut_loop_with_id_loop_back
- (T : Type) (i : U32) (ls : List T) (ret0 : T) : Result (List T) :=
+ (T : Type) (i : U32) (ls : List T) (ret : T) : Result (List T) :=
match ls with
| List.Cons x tl =>
if i = 0#u32
- then Result.ret (List.Cons ret0 tl)
+ then Result.ret (List.Cons ret tl)
else
do
let i0 ← i - 1#u32
- let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret0
+ let tl0 ← list_nth_mut_loop_with_id_loop_back T i0 tl ret
Result.ret (List.Cons x tl0)
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_mut_loop_with_id]: backward function 0
Source: 'src/loops.rs', lines 144:0-144:75 -/
def list_nth_mut_loop_with_id_back
- (T : Type) (ls : List T) (i : U32) (ret0 : T) : Result (List T) :=
+ (T : Type) (ls : List T) (i : U32) (ret : T) : Result (List T) :=
do
let ls0 ← id_mut T ls
- let l ← list_nth_mut_loop_with_id_loop_back T i ls0 ret0
+ let l ← list_nth_mut_loop_with_id_loop_back T i ls0 ret
id_mut_back T ls l
/- [loops::list_nth_shared_loop_with_id]: loop 0: forward function
@@ -291,7 +291,7 @@ divergent def list_nth_shared_loop_with_id_loop
else do
let i0 ← i - 1#u32
list_nth_shared_loop_with_id_loop T i0 tl
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_shared_loop_with_id]: forward function
Source: 'src/loops.rs', lines 158:0-158:70 -/
@@ -314,8 +314,8 @@ divergent def list_nth_mut_loop_pair_loop
else do
let i0 ← i - 1#u32
list_nth_mut_loop_pair_loop T tl0 tl1 i0
- | List.Nil => Result.fail Error.panic
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_mut_loop_pair]: forward function
Source: 'src/loops.rs', lines 174:0-178:27 -/
@@ -326,7 +326,7 @@ def list_nth_mut_loop_pair
/- [loops::list_nth_mut_loop_pair]: loop 0: backward function 0
Source: 'src/loops.rs', lines 174:0-195:1 -/
divergent def list_nth_mut_loop_pair_loop_back'a
- (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+ (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
Result (List T)
:=
match ls0 with
@@ -334,27 +334,27 @@ divergent def list_nth_mut_loop_pair_loop_back'a
match ls1 with
| List.Cons x1 tl1 =>
if i = 0#u32
- then Result.ret (List.Cons ret0 tl0)
+ then Result.ret (List.Cons ret tl0)
else
do
let i0 ← i - 1#u32
- let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret0
+ let tl00 ← list_nth_mut_loop_pair_loop_back'a T tl0 tl1 i0 ret
Result.ret (List.Cons x0 tl00)
- | List.Nil => Result.fail Error.panic
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_mut_loop_pair]: backward function 0
Source: 'src/loops.rs', lines 174:0-178:27 -/
def list_nth_mut_loop_pair_back'a
- (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+ (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
Result (List T)
:=
- list_nth_mut_loop_pair_loop_back'a T ls0 ls1 i ret0
+ list_nth_mut_loop_pair_loop_back'a T ls0 ls1 i ret
/- [loops::list_nth_mut_loop_pair]: loop 0: backward function 1
Source: 'src/loops.rs', lines 174:0-195:1 -/
divergent def list_nth_mut_loop_pair_loop_back'b
- (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+ (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
Result (List T)
:=
match ls0 with
@@ -362,22 +362,22 @@ divergent def list_nth_mut_loop_pair_loop_back'b
match ls1 with
| List.Cons x1 tl1 =>
if i = 0#u32
- then Result.ret (List.Cons ret0 tl1)
+ then Result.ret (List.Cons ret tl1)
else
do
let i0 ← i - 1#u32
- let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret0
+ let tl10 ← list_nth_mut_loop_pair_loop_back'b T tl0 tl1 i0 ret
Result.ret (List.Cons x1 tl10)
- | List.Nil => Result.fail Error.panic
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_mut_loop_pair]: backward function 1
Source: 'src/loops.rs', lines 174:0-178:27 -/
def list_nth_mut_loop_pair_back'b
- (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+ (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
Result (List T)
:=
- list_nth_mut_loop_pair_loop_back'b T ls0 ls1 i ret0
+ list_nth_mut_loop_pair_loop_back'b T ls0 ls1 i ret
/- [loops::list_nth_shared_loop_pair]: loop 0: forward function
Source: 'src/loops.rs', lines 198:0-219:1 -/
@@ -392,8 +392,8 @@ divergent def list_nth_shared_loop_pair_loop
else do
let i0 ← i - 1#u32
list_nth_shared_loop_pair_loop T tl0 tl1 i0
- | List.Nil => Result.fail Error.panic
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_shared_loop_pair]: forward function
Source: 'src/loops.rs', lines 198:0-202:19 -/
@@ -415,8 +415,8 @@ divergent def list_nth_mut_loop_pair_merge_loop
do
let i0 ← i - 1#u32
list_nth_mut_loop_pair_merge_loop T tl0 tl1 i0
- | List.Nil => Result.fail Error.panic
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_mut_loop_pair_merge]: forward function
Source: 'src/loops.rs', lines 223:0-227:27 -/
@@ -427,7 +427,7 @@ def list_nth_mut_loop_pair_merge
/- [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0
Source: 'src/loops.rs', lines 223:0-238:1 -/
divergent def list_nth_mut_loop_pair_merge_loop_back
- (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) :
+ (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : (T × T)) :
Result ((List T) × (List T))
:=
match ls0 with
@@ -435,24 +435,24 @@ divergent def list_nth_mut_loop_pair_merge_loop_back
match ls1 with
| List.Cons x1 tl1 =>
if i = 0#u32
- then let (t, t0) := ret0
+ then let (t, t0) := ret
Result.ret (List.Cons t tl0, List.Cons t0 tl1)
else
do
let i0 ← i - 1#u32
let (tl00, tl10) ←
- list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
+ list_nth_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret
Result.ret (List.Cons x0 tl00, List.Cons x1 tl10)
- | List.Nil => Result.fail Error.panic
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_mut_loop_pair_merge]: backward function 0
Source: 'src/loops.rs', lines 223:0-227:27 -/
def list_nth_mut_loop_pair_merge_back
- (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : (T × T)) :
+ (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : (T × T)) :
Result ((List T) × (List T))
:=
- list_nth_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0
+ list_nth_mut_loop_pair_merge_loop_back T ls0 ls1 i ret
/- [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function
Source: 'src/loops.rs', lines 241:0-256:1 -/
@@ -468,8 +468,8 @@ divergent def list_nth_shared_loop_pair_merge_loop
do
let i0 ← i - 1#u32
list_nth_shared_loop_pair_merge_loop T tl0 tl1 i0
- | List.Nil => Result.fail Error.panic
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_shared_loop_pair_merge]: forward function
Source: 'src/loops.rs', lines 241:0-245:19 -/
@@ -491,8 +491,8 @@ divergent def list_nth_mut_shared_loop_pair_loop
do
let i0 ← i - 1#u32
list_nth_mut_shared_loop_pair_loop T tl0 tl1 i0
- | List.Nil => Result.fail Error.panic
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_mut_shared_loop_pair]: forward function
Source: 'src/loops.rs', lines 259:0-263:23 -/
@@ -503,7 +503,7 @@ def list_nth_mut_shared_loop_pair
/- [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0
Source: 'src/loops.rs', lines 259:0-274:1 -/
divergent def list_nth_mut_shared_loop_pair_loop_back
- (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+ (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
Result (List T)
:=
match ls0 with
@@ -511,23 +511,22 @@ divergent def list_nth_mut_shared_loop_pair_loop_back
match ls1 with
| List.Cons x1 tl1 =>
if i = 0#u32
- then Result.ret (List.Cons ret0 tl0)
+ then Result.ret (List.Cons ret tl0)
else
do
let i0 ← i - 1#u32
- let tl00 ←
- list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret0
+ let tl00 ← list_nth_mut_shared_loop_pair_loop_back T tl0 tl1 i0 ret
Result.ret (List.Cons x0 tl00)
- | List.Nil => Result.fail Error.panic
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_mut_shared_loop_pair]: backward function 0
Source: 'src/loops.rs', lines 259:0-263:23 -/
def list_nth_mut_shared_loop_pair_back
- (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+ (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
Result (List T)
:=
- list_nth_mut_shared_loop_pair_loop_back T ls0 ls1 i ret0
+ list_nth_mut_shared_loop_pair_loop_back T ls0 ls1 i ret
/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function
Source: 'src/loops.rs', lines 278:0-293:1 -/
@@ -543,8 +542,8 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop
do
let i0 ← i - 1#u32
list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i0
- | List.Nil => Result.fail Error.panic
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_mut_shared_loop_pair_merge]: forward function
Source: 'src/loops.rs', lines 278:0-282:23 -/
@@ -555,7 +554,7 @@ def list_nth_mut_shared_loop_pair_merge
/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0
Source: 'src/loops.rs', lines 278:0-293:1 -/
divergent def list_nth_mut_shared_loop_pair_merge_loop_back
- (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+ (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
Result (List T)
:=
match ls0 with
@@ -563,23 +562,23 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop_back
match ls1 with
| List.Cons x1 tl1 =>
if i = 0#u32
- then Result.ret (List.Cons ret0 tl0)
+ then Result.ret (List.Cons ret tl0)
else
do
let i0 ← i - 1#u32
let tl00 ←
- list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
+ list_nth_mut_shared_loop_pair_merge_loop_back T tl0 tl1 i0 ret
Result.ret (List.Cons x0 tl00)
- | List.Nil => Result.fail Error.panic
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0
Source: 'src/loops.rs', lines 278:0-282:23 -/
def list_nth_mut_shared_loop_pair_merge_back
- (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+ (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
Result (List T)
:=
- list_nth_mut_shared_loop_pair_merge_loop_back T ls0 ls1 i ret0
+ list_nth_mut_shared_loop_pair_merge_loop_back T ls0 ls1 i ret
/- [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function
Source: 'src/loops.rs', lines 297:0-312:1 -/
@@ -595,8 +594,8 @@ divergent def list_nth_shared_mut_loop_pair_loop
do
let i0 ← i - 1#u32
list_nth_shared_mut_loop_pair_loop T tl0 tl1 i0
- | List.Nil => Result.fail Error.panic
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_shared_mut_loop_pair]: forward function
Source: 'src/loops.rs', lines 297:0-301:23 -/
@@ -607,7 +606,7 @@ def list_nth_shared_mut_loop_pair
/- [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1
Source: 'src/loops.rs', lines 297:0-312:1 -/
divergent def list_nth_shared_mut_loop_pair_loop_back
- (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+ (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
Result (List T)
:=
match ls0 with
@@ -615,23 +614,22 @@ divergent def list_nth_shared_mut_loop_pair_loop_back
match ls1 with
| List.Cons x1 tl1 =>
if i = 0#u32
- then Result.ret (List.Cons ret0 tl1)
+ then Result.ret (List.Cons ret tl1)
else
do
let i0 ← i - 1#u32
- let tl10 ←
- list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret0
+ let tl10 ← list_nth_shared_mut_loop_pair_loop_back T tl0 tl1 i0 ret
Result.ret (List.Cons x1 tl10)
- | List.Nil => Result.fail Error.panic
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_shared_mut_loop_pair]: backward function 1
Source: 'src/loops.rs', lines 297:0-301:23 -/
def list_nth_shared_mut_loop_pair_back
- (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+ (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
Result (List T)
:=
- list_nth_shared_mut_loop_pair_loop_back T ls0 ls1 i ret0
+ list_nth_shared_mut_loop_pair_loop_back T ls0 ls1 i ret
/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function
Source: 'src/loops.rs', lines 316:0-331:1 -/
@@ -647,8 +645,8 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop
do
let i0 ← i - 1#u32
list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i0
- | List.Nil => Result.fail Error.panic
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_shared_mut_loop_pair_merge]: forward function
Source: 'src/loops.rs', lines 316:0-320:23 -/
@@ -659,7 +657,7 @@ def list_nth_shared_mut_loop_pair_merge
/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0
Source: 'src/loops.rs', lines 316:0-331:1 -/
divergent def list_nth_shared_mut_loop_pair_merge_loop_back
- (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+ (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
Result (List T)
:=
match ls0 with
@@ -667,22 +665,22 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop_back
match ls1 with
| List.Cons x1 tl1 =>
if i = 0#u32
- then Result.ret (List.Cons ret0 tl1)
+ then Result.ret (List.Cons ret tl1)
else
do
let i0 ← i - 1#u32
let tl10 ←
- list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret0
+ list_nth_shared_mut_loop_pair_merge_loop_back T tl0 tl1 i0 ret
Result.ret (List.Cons x1 tl10)
- | List.Nil => Result.fail Error.panic
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
+ | List.Nil => Result.fail .panic
/- [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0
Source: 'src/loops.rs', lines 316:0-320:23 -/
def list_nth_shared_mut_loop_pair_merge_back
- (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret0 : T) :
+ (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) (ret : T) :
Result (List T)
:=
- list_nth_shared_mut_loop_pair_merge_loop_back T ls0 ls1 i ret0
+ list_nth_shared_mut_loop_pair_merge_loop_back T ls0 ls1 i ret
end loops
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 3b1c3f9f..ca66c628 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -101,7 +101,7 @@ def test2 : Result Unit :=
Result.ret ()
/- Unit test for [no_nested_borrows::test2] -/
-#assert (test2 == .ret ())
+#assert (test2 == Result.ret ())
/- [no_nested_borrows::get_max]: forward function
Source: 'src/no_nested_borrows.rs', lines 111:0-111:37 -/
@@ -118,11 +118,11 @@ def test3 : Result Unit :=
let y ← get_max 10#u32 11#u32
let z ← x + y
if not (z = 15#u32)
- then Result.fail Error.panic
+ then Result.fail .panic
else Result.ret ()
/- Unit test for [no_nested_borrows::test3] -/
-#assert (test3 == .ret ())
+#assert (test3 == Result.ret ())
/- [no_nested_borrows::test_neg1]: forward function
Source: 'src/no_nested_borrows.rs', lines 126:0-126:18 -/
@@ -130,40 +130,39 @@ def test_neg1 : Result Unit :=
do
let y ← - 3#i32
if not (y = (-(3:Int))#i32)
- then Result.fail Error.panic
+ then Result.fail .panic
else Result.ret ()
/- Unit test for [no_nested_borrows::test_neg1] -/
-#assert (test_neg1 == .ret ())
+#assert (test_neg1 == Result.ret ())
/- [no_nested_borrows::refs_test1]: forward function
Source: 'src/no_nested_borrows.rs', lines 133:0-133:19 -/
def refs_test1 : Result Unit :=
if not (1#i32 = 1#i32)
- then Result.fail Error.panic
+ then Result.fail .panic
else Result.ret ()
/- Unit test for [no_nested_borrows::refs_test1] -/
-#assert (refs_test1 == .ret ())
+#assert (refs_test1 == Result.ret ())
/- [no_nested_borrows::refs_test2]: forward function
Source: 'src/no_nested_borrows.rs', lines 144:0-144:19 -/
def refs_test2 : Result Unit :=
if not (2#i32 = 2#i32)
- then Result.fail Error.panic
+ then Result.fail .panic
else
if not (0#i32 = 0#i32)
- then Result.fail Error.panic
+ then Result.fail .panic
else
if not (2#i32 = 2#i32)
- then Result.fail Error.panic
- else
- if not (2#i32 = 2#i32)
- then Result.fail Error.panic
- else Result.ret ()
+ then Result.fail .panic
+ else if not (2#i32 = 2#i32)
+ then Result.fail .panic
+ else Result.ret ()
/- Unit test for [no_nested_borrows::refs_test2] -/
-#assert (refs_test2 == .ret ())
+#assert (refs_test2 == Result.ret ())
/- [no_nested_borrows::test_list1]: forward function
Source: 'src/no_nested_borrows.rs', lines 160:0-160:19 -/
@@ -171,7 +170,7 @@ def test_list1 : Result Unit :=
Result.ret ()
/- Unit test for [no_nested_borrows::test_list1] -/
-#assert (test_list1 == .ret ())
+#assert (test_list1 == Result.ret ())
/- [no_nested_borrows::test_box1]: forward function
Source: 'src/no_nested_borrows.rs', lines 165:0-165:18 -/
@@ -181,11 +180,11 @@ def test_box1 : Result Unit :=
let b0 ← alloc.boxed.Box.deref_mut_back I32 b 1#i32
let x ← alloc.boxed.Box.deref I32 b0
if not (x = 1#i32)
- then Result.fail Error.panic
+ then Result.fail .panic
else Result.ret ()
/- Unit test for [no_nested_borrows::test_box1] -/
-#assert (test_box1 == .ret ())
+#assert (test_box1 == Result.ret ())
/- [no_nested_borrows::copy_int]: forward function
Source: 'src/no_nested_borrows.rs', lines 175:0-175:30 -/
@@ -196,14 +195,14 @@ def copy_int (x : I32) : Result I32 :=
Source: 'src/no_nested_borrows.rs', lines 181:0-181:32 -/
def test_unreachable (b : Bool) : Result Unit :=
if b
- then Result.fail Error.panic
+ then Result.fail .panic
else Result.ret ()
/- [no_nested_borrows::test_panic]: forward function
Source: 'src/no_nested_borrows.rs', lines 189:0-189:26 -/
def test_panic (b : Bool) : Result Unit :=
if b
- then Result.fail Error.panic
+ then Result.fail .panic
else Result.ret ()
/- [no_nested_borrows::test_copy_int]: forward function
@@ -212,11 +211,11 @@ def test_copy_int : Result Unit :=
do
let y ← copy_int 0#i32
if not (0#i32 = y)
- then Result.fail Error.panic
+ then Result.fail .panic
else Result.ret ()
/- Unit test for [no_nested_borrows::test_copy_int] -/
-#assert (test_copy_int == .ret ())
+#assert (test_copy_int == Result.ret ())
/- [no_nested_borrows::is_cons]: forward function
Source: 'src/no_nested_borrows.rs', lines 203:0-203:38 -/
@@ -232,18 +231,18 @@ def test_is_cons : Result Unit :=
let l := List.Nil
let b ← is_cons I32 (List.Cons 0#i32 l)
if not b
- then Result.fail Error.panic
+ then Result.fail .panic
else Result.ret ()
/- Unit test for [no_nested_borrows::test_is_cons] -/
-#assert (test_is_cons == .ret ())
+#assert (test_is_cons == Result.ret ())
/- [no_nested_borrows::split_list]: forward function
Source: 'src/no_nested_borrows.rs', lines 216:0-216:48 -/
def split_list (T : Type) (l : List T) : Result (T × (List T)) :=
match l with
| List.Cons hd tl => Result.ret (hd, tl)
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
/- [no_nested_borrows::test_split_list]: forward function
Source: 'src/no_nested_borrows.rs', lines 224:0-224:24 -/
@@ -253,11 +252,11 @@ def test_split_list : Result Unit :=
let p ← split_list I32 (List.Cons 0#i32 l)
let (hd, _) := p
if not (hd = 0#i32)
- then Result.fail Error.panic
+ then Result.fail .panic
else Result.ret ()
/- Unit test for [no_nested_borrows::test_split_list] -/
-#assert (test_split_list == .ret ())
+#assert (test_split_list == Result.ret ())
/- [no_nested_borrows::choose]: forward function
Source: 'src/no_nested_borrows.rs', lines 231:0-231:70 -/
@@ -269,10 +268,10 @@ def choose (T : Type) (b : Bool) (x : T) (y : T) : Result T :=
/- [no_nested_borrows::choose]: backward function 0
Source: 'src/no_nested_borrows.rs', lines 231:0-231:70 -/
def choose_back
- (T : Type) (b : Bool) (x : T) (y : T) (ret0 : T) : Result (T × T) :=
+ (T : Type) (b : Bool) (x : T) (y : T) (ret : T) : Result (T × T) :=
if b
- then Result.ret (ret0, y)
- else Result.ret (x, ret0)
+ then Result.ret (ret, y)
+ else Result.ret (x, ret)
/- [no_nested_borrows::choose_test]: forward function
Source: 'src/no_nested_borrows.rs', lines 239:0-239:20 -/
@@ -281,18 +280,18 @@ def choose_test : Result Unit :=
let z ← choose I32 true 0#i32 0#i32
let z0 ← z + 1#i32
if not (z0 = 1#i32)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let (x, y) ← choose_back I32 true 0#i32 0#i32 z0
if not (x = 1#i32)
- then Result.fail Error.panic
+ then Result.fail .panic
else if not (y = 0#i32)
- then Result.fail Error.panic
+ then Result.fail .panic
else Result.ret ()
/- Unit test for [no_nested_borrows::choose_test] -/
-#assert (choose_test == .ret ())
+#assert (choose_test == Result.ret ())
/- [no_nested_borrows::test_char]: forward function
Source: 'src/no_nested_borrows.rs', lines 251:0-251:26 -/
@@ -334,7 +333,7 @@ divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T :=
else do
let i0 ← i - 1#u32
list_nth_shared T tl i0
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
/- [no_nested_borrows::list_nth_mut]: forward function
Source: 'src/no_nested_borrows.rs', lines 320:0-320:67 -/
@@ -346,22 +345,22 @@ divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result T :=
else do
let i0 ← i - 1#u32
list_nth_mut T tl i0
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
/- [no_nested_borrows::list_nth_mut]: backward function 0
Source: 'src/no_nested_borrows.rs', lines 320:0-320:67 -/
divergent def list_nth_mut_back
- (T : Type) (l : List T) (i : U32) (ret0 : T) : Result (List T) :=
+ (T : Type) (l : List T) (i : U32) (ret : T) : Result (List T) :=
match l with
| List.Cons x tl =>
if i = 0#u32
- then Result.ret (List.Cons ret0 tl)
+ then Result.ret (List.Cons ret tl)
else
do
let i0 ← i - 1#u32
- let tl0 ← list_nth_mut_back T tl i0 ret0
+ let tl0 ← list_nth_mut_back T tl i0 ret
Result.ret (List.Cons x tl0)
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
/- [no_nested_borrows::list_rev_aux]: forward function
Source: 'src/no_nested_borrows.rs', lines 336:0-336:63 -/
@@ -387,43 +386,43 @@ def test_list_functions : Result Unit :=
let l1 := List.Cons 1#i32 l0
let i ← list_length I32 (List.Cons 0#i32 l1)
if not (i = 3#u32)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let i0 ← list_nth_shared I32 (List.Cons 0#i32 l1) 0#u32
if not (i0 = 0#i32)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let i1 ← list_nth_shared I32 (List.Cons 0#i32 l1) 1#u32
if not (i1 = 1#i32)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let i2 ← list_nth_shared I32 (List.Cons 0#i32 l1) 2#u32
if not (i2 = 2#i32)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let ls ←
list_nth_mut_back I32 (List.Cons 0#i32 l1) 1#u32 3#i32
let i3 ← list_nth_shared I32 ls 0#u32
if not (i3 = 0#i32)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let i4 ← list_nth_shared I32 ls 1#u32
if not (i4 = 3#i32)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let i5 ← list_nth_shared I32 ls 2#u32
if not (i5 = 2#i32)
- then Result.fail Error.panic
+ then Result.fail .panic
else Result.ret ()
/- Unit test for [no_nested_borrows::test_list_functions] -/
-#assert (test_list_functions == .ret ())
+#assert (test_list_functions == Result.ret ())
/- [no_nested_borrows::id_mut_pair1]: forward function
Source: 'src/no_nested_borrows.rs', lines 371:0-371:89 -/
@@ -433,8 +432,8 @@ def id_mut_pair1 (T1 T2 : Type) (x : T1) (y : T2) : Result (T1 × T2) :=
/- [no_nested_borrows::id_mut_pair1]: backward function 0
Source: 'src/no_nested_borrows.rs', lines 371:0-371:89 -/
def id_mut_pair1_back
- (T1 T2 : Type) (x : T1) (y : T2) (ret0 : (T1 × T2)) : Result (T1 × T2) :=
- let (t, t0) := ret0
+ (T1 T2 : Type) (x : T1) (y : T2) (ret : (T1 × T2)) : Result (T1 × T2) :=
+ let (t, t0) := ret
Result.ret (t, t0)
/- [no_nested_borrows::id_mut_pair2]: forward function
@@ -446,8 +445,8 @@ def id_mut_pair2 (T1 T2 : Type) (p : (T1 × T2)) : Result (T1 × T2) :=
/- [no_nested_borrows::id_mut_pair2]: backward function 0
Source: 'src/no_nested_borrows.rs', lines 375:0-375:88 -/
def id_mut_pair2_back
- (T1 T2 : Type) (p : (T1 × T2)) (ret0 : (T1 × T2)) : Result (T1 × T2) :=
- let (t, t0) := ret0
+ (T1 T2 : Type) (p : (T1 × T2)) (ret : (T1 × T2)) : Result (T1 × T2) :=
+ let (t, t0) := ret
Result.ret (t, t0)
/- [no_nested_borrows::id_mut_pair3]: forward function
@@ -458,14 +457,14 @@ def id_mut_pair3 (T1 T2 : Type) (x : T1) (y : T2) : Result (T1 × T2) :=
/- [no_nested_borrows::id_mut_pair3]: backward function 0
Source: 'src/no_nested_borrows.rs', lines 379:0-379:93 -/
def id_mut_pair3_back'a
- (T1 T2 : Type) (x : T1) (y : T2) (ret0 : T1) : Result T1 :=
- Result.ret ret0
+ (T1 T2 : Type) (x : T1) (y : T2) (ret : T1) : Result T1 :=
+ Result.ret ret
/- [no_nested_borrows::id_mut_pair3]: backward function 1
Source: 'src/no_nested_borrows.rs', lines 379:0-379:93 -/
def id_mut_pair3_back'b
- (T1 T2 : Type) (x : T1) (y : T2) (ret0 : T2) : Result T2 :=
- Result.ret ret0
+ (T1 T2 : Type) (x : T1) (y : T2) (ret : T2) : Result T2 :=
+ Result.ret ret
/- [no_nested_borrows::id_mut_pair4]: forward function
Source: 'src/no_nested_borrows.rs', lines 383:0-383:92 -/
@@ -476,14 +475,14 @@ def id_mut_pair4 (T1 T2 : Type) (p : (T1 × T2)) : Result (T1 × T2) :=
/- [no_nested_borrows::id_mut_pair4]: backward function 0
Source: 'src/no_nested_borrows.rs', lines 383:0-383:92 -/
def id_mut_pair4_back'a
- (T1 T2 : Type) (p : (T1 × T2)) (ret0 : T1) : Result T1 :=
- Result.ret ret0
+ (T1 T2 : Type) (p : (T1 × T2)) (ret : T1) : Result T1 :=
+ Result.ret ret
/- [no_nested_borrows::id_mut_pair4]: backward function 1
Source: 'src/no_nested_borrows.rs', lines 383:0-383:92 -/
def id_mut_pair4_back'b
- (T1 T2 : Type) (p : (T1 × T2)) (ret0 : T2) : Result T2 :=
- Result.ret ret0
+ (T1 T2 : Type) (p : (T1 × T2)) (ret : T2) : Result T2 :=
+ Result.ret ret
/- [no_nested_borrows::StructWithTuple]
Source: 'src/no_nested_borrows.rs', lines 390:0-390:34 -/
@@ -522,28 +521,28 @@ def test_constants : Result Unit :=
let swt ← new_tuple1
let (i, _) := swt.p
if not (i = 1#u32)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let swt0 ← new_tuple2
let (i0, _) := swt0.p
if not (i0 = 1#i16)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let swt1 ← new_tuple3
let (i1, _) := swt1.p
if not (i1 = 1#u64)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let swp ← new_pair1
if not (swp.p.x = 1#u32)
- then Result.fail Error.panic
+ then Result.fail .panic
else Result.ret ()
/- Unit test for [no_nested_borrows::test_constants] -/
-#assert (test_constants == .ret ())
+#assert (test_constants == Result.ret ())
/- [no_nested_borrows::test_weird_borrows1]: forward function
Source: 'src/no_nested_borrows.rs', lines 428:0-428:28 -/
@@ -551,7 +550,7 @@ def test_weird_borrows1 : Result Unit :=
Result.ret ()
/- Unit test for [no_nested_borrows::test_weird_borrows1] -/
-#assert (test_weird_borrows1 == .ret ())
+#assert (test_weird_borrows1 == Result.ret ())
/- [no_nested_borrows::test_mem_replace]: merged forward/backward function
(there is a single backward function, and the forward function returns ())
@@ -559,7 +558,7 @@ def test_weird_borrows1 : Result Unit :=
def test_mem_replace (px : U32) : Result U32 :=
let y := core.mem.replace U32 px 1#u32
if not (y = 0#u32)
- then Result.fail Error.panic
+ then Result.fail .panic
else Result.ret 2#u32
/- [no_nested_borrows::test_shared_borrow_bool1]: forward function
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index 37e0e70e..08386bb7 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -17,11 +17,11 @@ def test_incr : Result Unit :=
do
let x ← ref_incr 0#i32
if not (x = 1#i32)
- then Result.fail Error.panic
+ then Result.fail .panic
else Result.ret ()
/- Unit test for [paper::test_incr] -/
-#assert (test_incr == .ret ())
+#assert (test_incr == Result.ret ())
/- [paper::choose]: forward function
Source: 'src/paper.rs', lines 15:0-15:70 -/
@@ -33,10 +33,10 @@ def choose (T : Type) (b : Bool) (x : T) (y : T) : Result T :=
/- [paper::choose]: backward function 0
Source: 'src/paper.rs', lines 15:0-15:70 -/
def choose_back
- (T : Type) (b : Bool) (x : T) (y : T) (ret0 : T) : Result (T × T) :=
+ (T : Type) (b : Bool) (x : T) (y : T) (ret : T) : Result (T × T) :=
if b
- then Result.ret (ret0, y)
- else Result.ret (x, ret0)
+ then Result.ret (ret, y)
+ else Result.ret (x, ret)
/- [paper::test_choose]: forward function
Source: 'src/paper.rs', lines 23:0-23:20 -/
@@ -45,18 +45,18 @@ def test_choose : Result Unit :=
let z ← choose I32 true 0#i32 0#i32
let z0 ← z + 1#i32
if not (z0 = 1#i32)
- then Result.fail Error.panic
+ then Result.fail .panic
else
do
let (x, y) ← choose_back I32 true 0#i32 0#i32 z0
if not (x = 1#i32)
- then Result.fail Error.panic
+ then Result.fail .panic
else if not (y = 0#i32)
- then Result.fail Error.panic
+ then Result.fail .panic
else Result.ret ()
/- Unit test for [paper::test_choose] -/
-#assert (test_choose == .ret ())
+#assert (test_choose == Result.ret ())
/- [paper::List]
Source: 'src/paper.rs', lines 35:0-35:16 -/
@@ -74,22 +74,22 @@ divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result T :=
else do
let i0 ← i - 1#u32
list_nth_mut T tl i0
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
/- [paper::list_nth_mut]: backward function 0
Source: 'src/paper.rs', lines 42:0-42:67 -/
divergent def list_nth_mut_back
- (T : Type) (l : List T) (i : U32) (ret0 : T) : Result (List T) :=
+ (T : Type) (l : List T) (i : U32) (ret : T) : Result (List T) :=
match l with
| List.Cons x tl =>
if i = 0#u32
- then Result.ret (List.Cons ret0 tl)
+ then Result.ret (List.Cons ret tl)
else
do
let i0 ← i - 1#u32
- let tl0 ← list_nth_mut_back T tl i0 ret0
+ let tl0 ← list_nth_mut_back T tl i0 ret
Result.ret (List.Cons x tl0)
- | List.Nil => Result.fail Error.panic
+ | List.Nil => Result.fail .panic
/- [paper::sum]: forward function
Source: 'src/paper.rs', lines 57:0-57:32 -/
@@ -112,11 +112,11 @@ def test_nth : Result Unit :=
let l2 ← list_nth_mut_back I32 (List.Cons 1#i32 l1) 2#u32 x0
let i ← sum l2
if not (i = 7#i32)
- then Result.fail Error.panic
+ then Result.fail .panic
else Result.ret ()
/- Unit test for [paper::test_nth] -/
-#assert (test_nth == .ret ())
+#assert (test_nth == Result.ret ())
/- [paper::call_choose]: forward function
Source: 'src/paper.rs', lines 76:0-76:44 -/
diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index 0ef71791..37f0dffb 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -24,15 +24,15 @@ divergent def get_list_at_x (ls : List U32) (x : U32) : Result (List U32) :=
/- [polonius_list::get_list_at_x]: backward function 0
Source: 'src/polonius_list.rs', lines 13:0-13:76 -/
divergent def get_list_at_x_back
- (ls : List U32) (x : U32) (ret0 : List U32) : Result (List U32) :=
+ (ls : List U32) (x : U32) (ret : List U32) : Result (List U32) :=
match ls with
| List.Cons hd tl =>
if hd = x
- then Result.ret ret0
+ then Result.ret ret
else
do
- let tl0 ← get_list_at_x_back tl x ret0
+ let tl0 ← get_list_at_x_back tl x ret
Result.ret (List.Cons hd tl0)
- | List.Nil => Result.ret ret0
+ | List.Nil => Result.ret ret
end polonius_list
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index 9ac4736c..e7795d9c 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -326,15 +326,11 @@ def test_where2
:=
Result.ret ()
-/- [alloc::string::String]
- Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/alloc/src/string.rs', lines 365:0-365:17 -/
-axiom alloc.string.String : Type
-
/- Trait declaration: [traits::ParentTrait0]
Source: 'src/traits.rs', lines 200:0-200:22 -/
structure ParentTrait0 (Self : Type) where
W : Type
- get_name : Self → Result alloc.string.String
+ get_name : Self → Result String
get_w : Self → Result W
/- Trait declaration: [traits::ParentTrait1]
@@ -350,9 +346,7 @@ structure ChildTrait (Self : Type) where
/- [traits::test_child_trait1]: forward function
Source: 'src/traits.rs', lines 209:0-209:56 -/
def test_child_trait1
- (T : Type) (ChildTraitTInst : ChildTrait T) (x : T) :
- Result alloc.string.String
- :=
+ (T : Type) (ChildTraitTInst : ChildTrait T) (x : T) : Result String :=
ChildTraitTInst.ParentTrait0SelfInst.get_name x
/- [traits::test_child_trait2]: forward function
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 15:10:00 +0000