summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean')
-rw-r--r--tests/lean/Arrays.lean66
-rw-r--r--tests/lean/BetreeMain/Funs.lean122
-rw-r--r--tests/lean/Bitwise.lean6
-rw-r--r--tests/lean/Constants.lean34
-rw-r--r--tests/lean/Demo/Demo.lean38
-rw-r--r--tests/lean/External/Funs.lean12
-rw-r--r--tests/lean/Hashmap/Funs.lean62
-rw-r--r--tests/lean/HashmapMain/Funs.lean64
-rw-r--r--tests/lean/Loops.lean114
-rw-r--r--tests/lean/NoNestedBorrows.lean138
-rw-r--r--tests/lean/Paper.lean32
-rw-r--r--tests/lean/PoloniusList.lean8
-rw-r--r--tests/lean/Traits.lean50
13 files changed, 373 insertions, 373 deletions
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index 207f31b9..d606640a 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -35,19 +35,19 @@ def array_to_mut_slice_
def array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
do
let s1 ← Array.to_slice T 32#usize s
- Result.ret (Slice.len T s1)
+ Result.ok (Slice.len T s1)
/- [arrays::shared_array_len]:
Source: 'src/arrays.rs', lines 29:0-29:48 -/
def shared_array_len (T : Type) (s : Array T 32#usize) : Result Usize :=
do
let s1 ← Array.to_slice T 32#usize s
- Result.ret (Slice.len T s1)
+ Result.ok (Slice.len T s1)
/- [arrays::shared_slice_len]:
Source: 'src/arrays.rs', lines 33:0-33:44 -/
def shared_slice_len (T : Type) (s : Slice T) : Result Usize :=
- Result.ret (Slice.len T s)
+ Result.ok (Slice.len T s)
/- [arrays::index_array_shared]:
Source: 'src/arrays.rs', lines 37:0-37:57 -/
@@ -105,7 +105,7 @@ def slice_subslice_mut_
core.slice.index.Slice.index_mut U32 (core.ops.range.Range Usize)
(core.slice.index.SliceIndexRangeUsizeSliceTInst U32) x
{ start := y, end_ := z }
- Result.ret (s, index_mut_back)
+ Result.ok (s, index_mut_back)
/- [arrays::array_to_slice_shared_]:
Source: 'src/arrays.rs', lines 72:0-72:54 -/
@@ -141,7 +141,7 @@ def array_subslice_mut_
(core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize)
(core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x
{ start := y, end_ := z }
- Result.ret (s, index_mut_back)
+ Result.ok (s, index_mut_back)
/- [arrays::index_slice_0]:
Source: 'src/arrays.rs', lines 88:0-88:38 -/
@@ -175,37 +175,37 @@ def update_update_array
let (_, index_mut_back1) ← Array.index_mut_usize U32 32#usize a j
let a1 ← index_mut_back1 0#u32
let _ ← index_mut_back a1
- Result.ret ()
+ Result.ok ()
/- [arrays::array_local_deep_copy]:
Source: 'src/arrays.rs', lines 118:0-118:43 -/
def array_local_deep_copy (x : Array U32 32#usize) : Result Unit :=
- Result.ret ()
+ Result.ok ()
/- [arrays::take_array]:
Source: 'src/arrays.rs', lines 122:0-122:30 -/
def take_array (a : Array U32 2#usize) : Result Unit :=
- Result.ret ()
+ Result.ok ()
/- [arrays::take_array_borrow]:
Source: 'src/arrays.rs', lines 123:0-123:38 -/
def take_array_borrow (a : Array U32 2#usize) : Result Unit :=
- Result.ret ()
+ Result.ok ()
/- [arrays::take_slice]:
Source: 'src/arrays.rs', lines 124:0-124:28 -/
def take_slice (s : Slice U32) : Result Unit :=
- Result.ret ()
+ Result.ok ()
/- [arrays::take_mut_slice]:
Source: 'src/arrays.rs', lines 125:0-125:36 -/
def take_mut_slice (s : Slice U32) : Result (Slice U32) :=
- Result.ret s
+ Result.ok s
/- [arrays::const_array]:
Source: 'src/arrays.rs', lines 127:0-127:32 -/
def const_array : Result (Array U32 2#usize) :=
- Result.ret (Array.make U32 2#usize [ 0#u32, 0#u32 ])
+ Result.ok (Array.make U32 2#usize [ 0#u32, 0#u32 ])
/- [arrays::const_slice]:
Source: 'src/arrays.rs', lines 131:0-131:20 -/
@@ -213,7 +213,7 @@ def const_slice : Result Unit :=
do
let _ ←
Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
- Result.ret ()
+ Result.ok ()
/- [arrays::take_all]:
Source: 'src/arrays.rs', lines 141:0-141:17 -/
@@ -229,7 +229,7 @@ def take_all : Result Unit :=
Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ])
let s2 ← take_mut_slice s1
let _ ← to_slice_mut_back s2
- Result.ret ()
+ Result.ok ()
/- [arrays::index_array]:
Source: 'src/arrays.rs', lines 155:0-155:38 -/
@@ -251,7 +251,7 @@ def index_slice_u32_0 (x : Slice U32) : Result U32 :=
def index_mut_slice_u32_0 (x : Slice U32) : Result (U32 × (Slice U32)) :=
do
let i ← Slice.index_usize U32 x 0#usize
- Result.ret (i, x)
+ Result.ok (i, x)
/- [arrays::index_all]:
Source: 'src/arrays.rs', lines 170:0-170:25 -/
@@ -271,7 +271,7 @@ def index_all : Result U32 :=
let (i7, s2) ← index_mut_slice_u32_0 s1
let i8 ← i6 + i7
let _ ← to_slice_mut_back s2
- Result.ret i8
+ Result.ok i8
/- [arrays::update_array]:
Source: 'src/arrays.rs', lines 184:0-184:36 -/
@@ -279,7 +279,7 @@ def update_array (x : Array U32 2#usize) : Result Unit :=
do
let (_, index_mut_back) ← Array.index_mut_usize U32 2#usize x 0#usize
let _ ← index_mut_back 1#u32
- Result.ret ()
+ Result.ok ()
/- [arrays::update_array_mut_borrow]:
Source: 'src/arrays.rs', lines 187:0-187:48 -/
@@ -306,7 +306,7 @@ def update_all : Result Unit :=
let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2#usize x
let s1 ← update_mut_slice s
let _ ← to_slice_mut_back s1
- Result.ret ()
+ Result.ok ()
/- [arrays::range_all]:
Source: 'src/arrays.rs', lines 205:0-205:18 -/
@@ -320,7 +320,7 @@ def range_all : Result Unit :=
{ start := 1#usize, end_ := 3#usize }
let s1 ← update_mut_slice s
let _ ← index_mut_back s1
- Result.ret ()
+ Result.ok ()
/- [arrays::deref_array_borrow]:
Source: 'src/arrays.rs', lines 214:0-214:46 -/
@@ -333,12 +333,12 @@ def deref_array_mut_borrow
(x : Array U32 2#usize) : Result (U32 × (Array U32 2#usize)) :=
do
let i ← Array.index_usize U32 2#usize x 0#usize
- Result.ret (i, x)
+ Result.ok (i, x)
/- [arrays::take_array_t]:
Source: 'src/arrays.rs', lines 227:0-227:31 -/
def take_array_t (a : Array AB 2#usize) : Result Unit :=
- Result.ret ()
+ Result.ok ()
/- [arrays::non_copyable_array]:
Source: 'src/arrays.rs', lines 229:0-229:27 -/
@@ -356,7 +356,7 @@ divergent def sum_loop (s : Slice U32) (sum1 : U32) (i : Usize) : Result U32 :=
let sum3 ← sum1 + i2
let i3 ← i + 1#usize
sum_loop s sum3 i3
- else Result.ret sum1
+ else Result.ok sum1
/- [arrays::sum]:
Source: 'src/arrays.rs', lines 242:0-242:28 -/
@@ -377,7 +377,7 @@ divergent def sum2_loop
let sum3 ← sum1 + i4
let i5 ← i + 1#usize
sum2_loop s s2 sum3 i5
- else Result.ret sum1
+ else Result.ok sum1
/- [arrays::sum2]:
Source: 'src/arrays.rs', lines 252:0-252:41 -/
@@ -397,7 +397,7 @@ def f0 : Result Unit :=
let (_, index_mut_back) ← Slice.index_mut_usize U32 s 0#usize
let s1 ← index_mut_back 1#u32
let _ ← to_slice_mut_back s1
- Result.ret ()
+ Result.ok ()
/- [arrays::f1]:
Source: 'src/arrays.rs', lines 268:0-268:11 -/
@@ -407,12 +407,12 @@ def f1 : Result Unit :=
Array.index_mut_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ])
0#usize
let _ ← index_mut_back 1#u32
- Result.ret ()
+ Result.ok ()
/- [arrays::f2]:
Source: 'src/arrays.rs', lines 273:0-273:17 -/
def f2 (i : U32) : Result Unit :=
- Result.ret ()
+ Result.ok ()
/- [arrays::f4]:
Source: 'src/arrays.rs', lines 282:0-282:54 -/
@@ -438,7 +438,7 @@ def f3 : Result U32 :=
/- [arrays::SZ]
Source: 'src/arrays.rs', lines 286:0-286:19 -/
-def SZ_body : Result Usize := Result.ret 32#usize
+def SZ_body : Result Usize := Result.ok 32#usize
def SZ : Usize := eval_global SZ_body
/- [arrays::f5]:
@@ -458,7 +458,7 @@ def ite : Result Unit :=
let (_, s3) ← index_mut_slice_u32_0 s2
let _ ← to_slice_mut_back1 s3
let _ ← to_slice_mut_back s1
- Result.ret ()
+ Result.ok ()
/- [arrays::zero_slice]: loop 0:
Source: 'src/arrays.rs', lines 303:0-310:1 -/
@@ -471,7 +471,7 @@ divergent def zero_slice_loop
let i1 ← i + 1#usize
let a1 ← index_mut_back 0#u8
zero_slice_loop a1 i1 len
- else Result.ret a
+ else Result.ok a
/- [arrays::zero_slice]:
Source: 'src/arrays.rs', lines 303:0-303:31 -/
@@ -486,7 +486,7 @@ divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit :=
then do
let i1 ← i + 1#usize
iter_mut_slice_loop len i1
- else Result.ret ()
+ else Result.ok ()
/- [arrays::iter_mut_slice]:
Source: 'src/arrays.rs', lines 312:0-312:35 -/
@@ -494,7 +494,7 @@ def iter_mut_slice (a : Slice U8) : Result (Slice U8) :=
do
let len := Slice.len U8 a
let _ ← iter_mut_slice_loop len 0#usize
- Result.ret a
+ Result.ok a
/- [arrays::sum_mut_slice]: loop 0:
Source: 'src/arrays.rs', lines 320:0-328:1 -/
@@ -508,13 +508,13 @@ divergent def sum_mut_slice_loop
let s1 ← s + i2
let i3 ← i + 1#usize
sum_mut_slice_loop a i3 s1
- else Result.ret s
+ else Result.ok s
/- [arrays::sum_mut_slice]:
Source: 'src/arrays.rs', lines 320:0-320:42 -/
def sum_mut_slice (a : Slice U32) : Result (U32 × (Slice U32)) :=
do
let i ← sum_mut_slice_loop a 0#usize 0#u32
- Result.ret (i, a)
+ Result.ok (i, a)
end arrays
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 2fbcd6a4..0c31b9bc 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -42,12 +42,12 @@ def betree.store_leaf_node
def betree.fresh_node_id (counter : U64) : Result (U64 × U64) :=
do
let counter1 ← counter + 1#u64
- Result.ret (counter, counter1)
+ Result.ok (counter, counter1)
/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]:
Source: 'src/betree.rs', lines 206:4-206:20 -/
def betree.NodeIdCounter.new : Result betree.NodeIdCounter :=
- Result.ret { next_node_id := 0#u64 }
+ Result.ok { next_node_id := 0#u64 }
/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]:
Source: 'src/betree.rs', lines 210:4-210:36 -/
@@ -55,7 +55,7 @@ def betree.NodeIdCounter.fresh_id
(self : betree.NodeIdCounter) : Result (U64 × betree.NodeIdCounter) :=
do
let i ← self.next_node_id + 1#u64
- Result.ret (self.next_node_id, { next_node_id := i })
+ Result.ok (self.next_node_id, { next_node_id := i })
/- [betree_main::betree::upsert_update]:
Source: 'src/betree.rs', lines 234:0-234:70 -/
@@ -64,8 +64,8 @@ def betree.upsert_update
match prev with
| none =>
match st with
- | betree.UpsertFunState.Add v => Result.ret v
- | betree.UpsertFunState.Sub _ => Result.ret 0#u64
+ | betree.UpsertFunState.Add v => Result.ok v
+ | betree.UpsertFunState.Sub _ => Result.ok 0#u64
| some prev1 =>
match st with
| betree.UpsertFunState.Add v =>
@@ -73,11 +73,11 @@ def betree.upsert_update
let margin ← core_u64_max - prev1
if margin >= v
then prev1 + v
- else Result.ret core_u64_max
+ else Result.ok core_u64_max
| betree.UpsertFunState.Sub v =>
if prev1 >= v
then prev1 - v
- else Result.ret 0#u64
+ else Result.ok 0#u64
/- [betree_main::betree::{betree_main::betree::List<T>#1}::len]:
Source: 'src/betree.rs', lines 276:4-276:24 -/
@@ -86,7 +86,7 @@ divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
| betree.List.Cons _ tl => do
let i ← betree.List.len T tl
1#u64 + i
- | betree.List.Nil => Result.ret 0#u64
+ | betree.List.Nil => Result.ok 0#u64
/- [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]:
Source: 'src/betree.rs', lines 284:4-284:51 -/
@@ -95,7 +95,7 @@ divergent def betree.List.split_at
Result ((betree.List T) × (betree.List T))
:=
if n = 0#u64
- then Result.ret (betree.List.Nil, self)
+ then Result.ok (betree.List.Nil, self)
else
match self with
| betree.List.Cons hd tl =>
@@ -103,7 +103,7 @@ divergent def betree.List.split_at
let i ← n - 1#u64
let p ← betree.List.split_at T tl i
let (ls0, ls1) := p
- Result.ret (betree.List.Cons hd ls0, ls1)
+ Result.ok (betree.List.Cons hd ls0, ls1)
| betree.List.Nil => Result.fail .panic
/- [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]:
@@ -111,7 +111,7 @@ divergent def betree.List.split_at
def betree.List.push_front
(T : Type) (self : betree.List T) (x : T) : Result (betree.List T) :=
let (tl, _) := core.mem.replace (betree.List T) self betree.List.Nil
- Result.ret (betree.List.Cons x tl)
+ Result.ok (betree.List.Cons x tl)
/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]:
Source: 'src/betree.rs', lines 306:4-306:32 -/
@@ -119,14 +119,14 @@ def betree.List.pop_front
(T : Type) (self : betree.List T) : Result (T × (betree.List T)) :=
let (ls, _) := core.mem.replace (betree.List T) self betree.List.Nil
match ls with
- | betree.List.Cons x tl => Result.ret (x, tl)
+ | betree.List.Cons x tl => Result.ok (x, tl)
| betree.List.Nil => Result.fail .panic
/- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]:
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 _ => Result.ret hd
+ | betree.List.Cons hd _ => Result.ok hd
| betree.List.Nil => Result.fail .panic
/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]:
@@ -135,8 +135,8 @@ def betree.ListPairU64T.head_has_key
(T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool :=
match self with
| betree.List.Cons hd _ => let (i, _) := hd
- Result.ret (i = key)
- | betree.List.Nil => Result.ret false
+ Result.ok (i = key)
+ | betree.List.Nil => Result.ok false
/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]:
Source: 'src/betree.rs', lines 339:4-339:73 -/
@@ -148,13 +148,13 @@ divergent def betree.ListPairU64T.partition_at_pivot
| betree.List.Cons hd tl =>
let (i, t) := hd
if i >= pivot
- then Result.ret (betree.List.Nil, betree.List.Cons (i, t) tl)
+ then Result.ok (betree.List.Nil, betree.List.Cons (i, t) tl)
else
do
let p ← betree.ListPairU64T.partition_at_pivot T tl pivot
let (ls0, ls1) := p
- Result.ret (betree.List.Cons (i, t) ls0, ls1)
- | betree.List.Nil => Result.ret (betree.List.Nil, betree.List.Nil)
+ Result.ok (betree.List.Cons (i, t) ls0, ls1)
+ | betree.List.Nil => Result.ok (betree.List.Nil, betree.List.Nil)
/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]:
Source: 'src/betree.rs', lines 359:4-364:17 -/
@@ -174,7 +174,7 @@ def betree.Leaf.split
let (st2, _) ← betree.store_leaf_node id1 content1 st1
let n := betree.Node.Leaf { id := id0, size := params.split_size }
let n1 := betree.Node.Leaf { id := id1, size := params.split_size }
- Result.ret (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2))
+ Result.ok (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2))
/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]:
Source: 'src/betree.rs', lines 789:4-792:34 -/
@@ -187,7 +187,7 @@ divergent def betree.Node.lookup_first_message_for_key
| betree.List.Cons x next_msgs =>
let (i, m) := x
if i >= key
- then Result.ret (betree.List.Cons (i, m) next_msgs, Result.ret)
+ then Result.ok (betree.List.Cons (i, m) next_msgs, Result.ok)
else
do
let (l, lookup_first_message_for_key_back) ←
@@ -196,9 +196,9 @@ divergent def betree.Node.lookup_first_message_for_key
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)
- | betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
+ Result.ok (betree.List.Cons (i, m) next_msgs1)
+ Result.ok (l, back)
+ | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]:
Source: 'src/betree.rs', lines 636:4-636:80 -/
@@ -208,12 +208,12 @@ divergent def betree.Node.lookup_in_bindings
| betree.List.Cons hd tl =>
let (i, i1) := hd
if i = key
- then Result.ret (some i1)
+ then Result.ok (some i1)
else
if i > key
- then Result.ret none
+ then Result.ok none
else betree.Node.lookup_in_bindings key tl
- | betree.List.Nil => Result.ret none
+ | betree.List.Nil => Result.ok none
/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]:
Source: 'src/betree.rs', lines 819:4-819:90 -/
@@ -242,7 +242,7 @@ divergent def betree.Node.apply_upserts
let msgs1 ←
betree.List.push_front (U64 × betree.Message) msgs (key,
betree.Message.Insert v)
- Result.ret (st1, (v, msgs1))
+ Result.ok (st1, (v, msgs1))
/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]:
Source: 'src/betree.rs', lines 395:4-395:63 -/
@@ -255,11 +255,11 @@ mutual divergent def betree.Internal.lookup_in_children
then
do
let (st1, (o, n2)) ← betree.Node.lookup n key st
- Result.ret (st1, (o, betree.Internal.mk i i1 n2 n1))
+ Result.ok (st1, (o, betree.Internal.mk i i1 n2 n1))
else
do
let (st1, (o, n2)) ← betree.Node.lookup n1 key st
- Result.ret (st1, (o, betree.Internal.mk i i1 n n2))
+ Result.ok (st1, (o, betree.Internal.mk i i1 n n2))
/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]:
Source: 'src/betree.rs', lines 709:4-709:58 -/
@@ -285,7 +285,7 @@ divergent def betree.Node.lookup
st1
let _ ←
lookup_first_message_for_key_back (betree.List.Cons (k, msg) l)
- Result.ret (st2, (o, betree.Node.Internal node1))
+ Result.ok (st2, (o, betree.Node.Internal node1))
else
match msg with
| betree.Message.Insert v =>
@@ -293,14 +293,14 @@ divergent def betree.Node.lookup
let _ ←
lookup_first_message_for_key_back (betree.List.Cons (k,
betree.Message.Insert v) l)
- Result.ret (st1, (some v, betree.Node.Internal (betree.Internal.mk i
+ Result.ok (st1, (some v, betree.Node.Internal (betree.Internal.mk i
i1 n n1)))
| betree.Message.Delete =>
do
let _ ←
lookup_first_message_for_key_back (betree.List.Cons (k,
betree.Message.Delete) l)
- Result.ret (st1, (none, betree.Node.Internal (betree.Internal.mk i i1
+ Result.ok (st1, (none, betree.Node.Internal (betree.Internal.mk i i1
n n1)))
| betree.Message.Upsert ufs =>
do
@@ -313,20 +313,20 @@ divergent def betree.Node.lookup
let ⟨ i2, i3, n2, n3 ⟩ := node1
let msgs1 ← lookup_first_message_for_key_back pending1
let (st4, _) ← betree.store_internal_node i2 msgs1 st3
- Result.ret (st4, (some v1, betree.Node.Internal (betree.Internal.mk
- i2 i3 n2 n3)))
+ Result.ok (st4, (some v1, betree.Node.Internal (betree.Internal.mk i2
+ i3 n2 n3)))
| betree.List.Nil =>
do
let (st2, (o, node1)) ←
betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key
st1
let _ ← lookup_first_message_for_key_back betree.List.Nil
- Result.ret (st2, (o, betree.Node.Internal node1))
+ Result.ok (st2, (o, betree.Node.Internal node1))
| betree.Node.Leaf node =>
do
let (st1, bindings) ← betree.load_leaf_node node.id st
let o ← betree.Node.lookup_in_bindings key bindings
- Result.ret (st1, (o, betree.Node.Leaf node))
+ Result.ok (st1, (o, betree.Node.Leaf node))
end
@@ -346,8 +346,8 @@ divergent def betree.Node.filter_messages_for_key
betree.List.pop_front (U64 × betree.Message) (betree.List.Cons (k, m)
l)
betree.Node.filter_messages_for_key key msgs1
- else Result.ret (betree.List.Cons (k, m) l)
- | betree.List.Nil => Result.ret betree.List.Nil
+ else Result.ok (betree.List.Cons (k, m) l)
+ | betree.List.Nil => Result.ok betree.List.Nil
/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]:
Source: 'src/betree.rs', lines 689:4-692:34 -/
@@ -368,10 +368,10 @@ divergent def betree.Node.lookup_first_message_after_key
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)
- else Result.ret (betree.List.Cons (k, m) next_msgs, Result.ret)
- | betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
+ Result.ok (betree.List.Cons (k, m) next_msgs1)
+ Result.ok (l, back)
+ else Result.ok (betree.List.Cons (k, m) next_msgs, Result.ok)
+ | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]:
Source: 'src/betree.rs', lines 521:4-521:89 -/
@@ -450,7 +450,7 @@ divergent def betree.Node.apply_messages_to_internal
let (i, m) := new_msg
let msgs1 ← betree.Node.apply_to_internal msgs i m
betree.Node.apply_messages_to_internal msgs1 new_msgs_tl
- | betree.List.Nil => Result.ret msgs
+ | betree.List.Nil => Result.ok msgs
/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]:
Source: 'src/betree.rs', lines 653:4-656:32 -/
@@ -463,7 +463,7 @@ divergent def betree.Node.lookup_mut_in_bindings
| betree.List.Cons hd tl =>
let (i, i1) := hd
if i >= key
- then Result.ret (betree.List.Cons (i, i1) tl, Result.ret)
+ then Result.ok (betree.List.Cons (i, i1) tl, Result.ok)
else
do
let (l, lookup_mut_in_bindings_back) ←
@@ -472,9 +472,9 @@ divergent def betree.Node.lookup_mut_in_bindings
fun ret =>
do
let tl1 ← lookup_mut_in_bindings_back ret
- Result.ret (betree.List.Cons (i, i1) tl1)
- Result.ret (l, back)
- | betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
+ Result.ok (betree.List.Cons (i, i1) tl1)
+ Result.ok (l, back)
+ | betree.List.Nil => Result.ok (betree.List.Nil, Result.ok)
/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]:
Source: 'src/betree.rs', lines 460:4-460:87 -/
@@ -529,7 +529,7 @@ divergent def betree.Node.apply_messages_to_leaf
let (i, m) := new_msg
let bindings1 ← betree.Node.apply_to_leaf bindings i m
betree.Node.apply_messages_to_leaf bindings1 new_msgs_tl
- | betree.List.Nil => Result.ret bindings
+ | betree.List.Nil => Result.ok bindings
/- [betree_main::betree::{betree_main::betree::Internal#4}::flush]:
Source: 'src/betree.rs', lines 410:4-415:26 -/
@@ -558,17 +558,17 @@ mutual divergent def betree.Internal.flush
let (st2, p2) ←
betree.Node.apply_messages n1 params node_id_cnt1 msgs_right st1
let (n3, node_id_cnt2) := p2
- Result.ret (st2, (betree.List.Nil, (betree.Internal.mk i i1 n2 n3,
+ Result.ok (st2, (betree.List.Nil, (betree.Internal.mk i i1 n2 n3,
node_id_cnt2)))
else
- Result.ret (st1, (msgs_right, (betree.Internal.mk i i1 n2 n1,
+ Result.ok (st1, (msgs_right, (betree.Internal.mk i i1 n2 n1,
node_id_cnt1)))
else
do
let (st1, p1) ←
betree.Node.apply_messages n1 params node_id_cnt msgs_right st
let (n2, node_id_cnt1) := p1
- Result.ret (st1, (msgs_left, (betree.Internal.mk i i1 n n2, node_id_cnt1)))
+ Result.ok (st1, (msgs_left, (betree.Internal.mk i i1 n n2, node_id_cnt1)))
/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]:
Source: 'src/betree.rs', lines 588:4-593:5 -/
@@ -594,12 +594,12 @@ divergent def betree.Node.apply_messages
let (node1, node_id_cnt1) := p
let ⟨ i2, i3, n2, n3 ⟩ := node1
let (st3, _) ← betree.store_internal_node i2 content2 st2
- Result.ret (st3, (betree.Node.Internal (betree.Internal.mk i2 i3 n2 n3),
+ Result.ok (st3, (betree.Node.Internal (betree.Internal.mk i2 i3 n2 n3),
node_id_cnt1))
else
do
let (st2, _) ← betree.store_internal_node i content1 st1
- Result.ret (st2, (betree.Node.Internal (betree.Internal.mk i i1 n n1),
+ Result.ok (st2, (betree.Node.Internal (betree.Internal.mk i i1 n n1),
node_id_cnt))
| betree.Node.Leaf node =>
do
@@ -613,11 +613,11 @@ divergent def betree.Node.apply_messages
let (st2, (new_node, node_id_cnt1)) ←
betree.Leaf.split node content1 params node_id_cnt st1
let (st3, _) ← betree.store_leaf_node node.id betree.List.Nil st2
- Result.ret (st3, (betree.Node.Internal new_node, node_id_cnt1))
+ Result.ok (st3, (betree.Node.Internal new_node, node_id_cnt1))
else
do
let (st2, _) ← betree.store_leaf_node node.id content1 st1
- Result.ret (st2, (betree.Node.Leaf { node with size := len },
+ Result.ok (st2, (betree.Node.Leaf { node with size := len },
node_id_cnt))
end
@@ -635,7 +635,7 @@ def betree.Node.apply
betree.Node.apply_messages self params node_id_cnt (betree.List.Cons (key,
new_msg) betree.List.Nil) st
let (self1, node_id_cnt1) := p
- Result.ret (st1, (self1, node_id_cnt1))
+ Result.ok (st1, (self1, node_id_cnt1))
/- [betree_main::betree::{betree_main::betree::BeTree#6}::new]:
Source: 'src/betree.rs', lines 849:4-849:60 -/
@@ -647,7 +647,7 @@ def betree.BeTree.new
let node_id_cnt ← betree.NodeIdCounter.new
let (id, node_id_cnt1) ← betree.NodeIdCounter.fresh_id node_id_cnt
let (st1, _) ← betree.store_leaf_node id betree.List.Nil st
- Result.ret (st1,
+ Result.ok (st1,
{
params := { min_flush_size := min_flush_size, split_size := split_size },
node_id_cnt := node_id_cnt1,
@@ -664,7 +664,7 @@ def betree.BeTree.apply
let (st1, p) ←
betree.Node.apply self.root self.params self.node_id_cnt key msg st
let (n, nic) := p
- Result.ret (st1, { self with node_id_cnt := nic, root := n })
+ Result.ok (st1, { self with node_id_cnt := nic, root := n })
/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]:
Source: 'src/betree.rs', lines 874:4-874:52 -/
@@ -699,14 +699,14 @@ def betree.BeTree.lookup
:=
do
let (st1, (o, n)) ← betree.Node.lookup self.root key st
- Result.ret (st1, (o, { self with root := n }))
+ Result.ok (st1, (o, { self with root := n }))
/- [betree_main::main]:
Source: 'src/betree_main.rs', lines 5:0-5:9 -/
def main : Result Unit :=
- Result.ret ()
+ Result.ok ()
/- Unit test for [betree_main::main] -/
-#assert (main == Result.ret ())
+#assert (main == Result.ok ())
end betree_main
diff --git a/tests/lean/Bitwise.lean b/tests/lean/Bitwise.lean
index 7c47e3dd..c13129f1 100644
--- a/tests/lean/Bitwise.lean
+++ b/tests/lean/Bitwise.lean
@@ -22,16 +22,16 @@ def shift_i32 (a : I32) : Result I32 :=
/- [bitwise::xor_u32]:
Source: 'src/bitwise.rs', lines 17:0-17:37 -/
def xor_u32 (a : U32) (b : U32) : Result U32 :=
- Result.ret (a ^^^ b)
+ Result.ok (a ^^^ b)
/- [bitwise::or_u32]:
Source: 'src/bitwise.rs', lines 21:0-21:36 -/
def or_u32 (a : U32) (b : U32) : Result U32 :=
- Result.ret (a ||| b)
+ Result.ok (a ||| b)
/- [bitwise::and_u32]:
Source: 'src/bitwise.rs', lines 25:0-25:37 -/
def and_u32 (a : U32) (b : U32) : Result U32 :=
- Result.ret (a &&& b)
+ Result.ok (a &&& b)
end bitwise
diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean
index 40f590d4..3cc3ca40 100644
--- a/tests/lean/Constants.lean
+++ b/tests/lean/Constants.lean
@@ -7,17 +7,17 @@ namespace constants
/- [constants::X0]
Source: 'src/constants.rs', lines 5:0-5:17 -/
-def X0_body : Result U32 := Result.ret 0#u32
+def X0_body : Result U32 := Result.ok 0#u32
def X0 : U32 := eval_global X0_body
/- [constants::X1]
Source: 'src/constants.rs', lines 7:0-7:17 -/
-def X1_body : Result U32 := Result.ret core_u32_max
+def X1_body : Result U32 := Result.ok core_u32_max
def X1 : U32 := eval_global X1_body
/- [constants::X2]
Source: 'src/constants.rs', lines 10:0-10:17 -/
-def X2_body : Result U32 := Result.ret 3#u32
+def X2_body : Result U32 := Result.ok 3#u32
def X2 : U32 := eval_global X2_body
/- [constants::incr]:
@@ -33,7 +33,7 @@ def X3 : U32 := eval_global X3_body
/- [constants::mk_pair0]:
Source: 'src/constants.rs', lines 23:0-23:51 -/
def mk_pair0 (x : U32) (y : U32) : Result (U32 × U32) :=
- Result.ret (x, y)
+ Result.ok (x, y)
/- [constants::Pair]
Source: 'src/constants.rs', lines 36:0-36:23 -/
@@ -44,7 +44,7 @@ structure Pair (T1 T2 : Type) where
/- [constants::mk_pair1]:
Source: 'src/constants.rs', lines 27:0-27:55 -/
def mk_pair1 (x : U32) (y : U32) : Result (Pair U32 U32) :=
- Result.ret { x := x, y := y }
+ Result.ok { x := x, y := y }
/- [constants::P0]
Source: 'src/constants.rs', lines 31:0-31:24 -/
@@ -58,12 +58,12 @@ def P1 : Pair U32 U32 := eval_global P1_body
/- [constants::P2]
Source: 'src/constants.rs', lines 33:0-33:24 -/
-def P2_body : Result (U32 × U32) := Result.ret (0#u32, 1#u32)
+def P2_body : Result (U32 × U32) := Result.ok (0#u32, 1#u32)
def P2 : (U32 × U32) := eval_global P2_body
/- [constants::P3]
Source: 'src/constants.rs', lines 34:0-34:28 -/
-def P3_body : Result (Pair U32 U32) := Result.ret { x := 0#u32, y := 1#u32 }
+def P3_body : Result (Pair U32 U32) := Result.ok { x := 0#u32, y := 1#u32 }
def P3 : Pair U32 U32 := eval_global P3_body
/- [constants::Wrap]
@@ -74,7 +74,7 @@ structure Wrap (T : Type) where
/- [constants::{constants::Wrap<T>}::new]:
Source: 'src/constants.rs', lines 54:4-54:41 -/
def Wrap.new (T : Type) (value : T) : Result (Wrap T) :=
- Result.ret { value := value }
+ Result.ok { value := value }
/- [constants::Y]
Source: 'src/constants.rs', lines 41:0-41:22 -/
@@ -84,7 +84,7 @@ def Y : Wrap I32 := eval_global Y_body
/- [constants::unwrap_y]:
Source: 'src/constants.rs', lines 43:0-43:30 -/
def unwrap_y : Result I32 :=
- Result.ret Y.value
+ Result.ok Y.value
/- [constants::YVAL]
Source: 'src/constants.rs', lines 47:0-47:19 -/
@@ -93,13 +93,13 @@ def YVAL : I32 := eval_global YVAL_body
/- [constants::get_z1::Z1]
Source: 'src/constants.rs', lines 62:4-62:17 -/
-def get_z1.Z1_body : Result I32 := Result.ret 3#i32
+def get_z1.Z1_body : Result I32 := Result.ok 3#i32
def get_z1.Z1 : I32 := eval_global get_z1.Z1_body
/- [constants::get_z1]:
Source: 'src/constants.rs', lines 61:0-61:28 -/
def get_z1 : Result I32 :=
- Result.ret get_z1.Z1
+ Result.ok get_z1.Z1
/- [constants::add]:
Source: 'src/constants.rs', lines 66:0-66:39 -/
@@ -108,12 +108,12 @@ def add (a : I32) (b : I32) : Result I32 :=
/- [constants::Q1]
Source: 'src/constants.rs', lines 74:0-74:17 -/
-def Q1_body : Result I32 := Result.ret 5#i32
+def Q1_body : Result I32 := Result.ok 5#i32
def Q1 : I32 := eval_global Q1_body
/- [constants::Q2]
Source: 'src/constants.rs', lines 75:0-75:17 -/
-def Q2_body : Result I32 := Result.ret Q1
+def Q2_body : Result I32 := Result.ok Q1
def Q2 : I32 := eval_global Q2_body
/- [constants::Q3]
@@ -131,7 +131,7 @@ def get_z2 : Result I32 :=
/- [constants::S1]
Source: 'src/constants.rs', lines 80:0-80:18 -/
-def S1_body : Result U32 := Result.ret 6#u32
+def S1_body : Result U32 := Result.ok 6#u32
def S1 : U32 := eval_global S1_body
/- [constants::S2]
@@ -141,7 +141,7 @@ def S2 : U32 := eval_global S2_body
/- [constants::S3]
Source: 'src/constants.rs', lines 82:0-82:29 -/
-def S3_body : Result (Pair U32 U32) := Result.ret P3
+def S3_body : Result (Pair U32 U32) := Result.ok P3
def S3 : Pair U32 U32 := eval_global S3_body
/- [constants::S4]
@@ -156,12 +156,12 @@ structure V (T : Type) (N : Usize) where
/- [constants::{constants::V<T, N>#1}::LEN]
Source: 'src/constants.rs', lines 91:4-91:24 -/
-def V.LEN_body (T : Type) (N : Usize) : Result Usize := Result.ret N
+def V.LEN_body (T : Type) (N : Usize) : Result Usize := Result.ok N
def V.LEN (T : Type) (N : Usize) : Usize := eval_global (V.LEN_body T N)
/- [constants::use_v]:
Source: 'src/constants.rs', lines 94:0-94:42 -/
def use_v (T : Type) (N : Usize) : Result Usize :=
- Result.ret (V.LEN T N)
+ Result.ok (V.LEN T N)
end constants
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 6d9fef8e..3a3aeb96 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 := fun ret => Result.ret (ret, y)
- Result.ret (x, back)
- else let back := fun ret => Result.ret (x, ret)
- Result.ret (y, back)
+ then let back := fun ret => Result.ok (ret, y)
+ Result.ok (x, back)
+ else let back := fun ret => Result.ok (x, ret)
+ Result.ok (y, back)
/- [demo::mul2_add1]:
Source: 'src/demo.rs', lines 13:0-13:31 -/
@@ -43,7 +43,7 @@ def use_incr : Result Unit :=
let x ← incr 0#u32
let x1 ← incr x
let _ ← incr x1
- Result.ret ()
+ Result.ok ()
/- [demo::CList]
Source: 'src/demo.rs', lines 34:0-34:17 -/
@@ -57,7 +57,7 @@ divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
match l with
| CList.CCons x tl =>
if i = 0#u32
- then Result.ret x
+ then Result.ok x
else do
let i1 ← i - 1#u32
list_nth T tl i1
@@ -73,8 +73,8 @@ divergent def list_nth_mut
| CList.CCons x tl =>
if i = 0#u32
then
- let back := fun ret => Result.ret (CList.CCons ret tl)
- Result.ret (x, back)
+ let back := fun ret => Result.ok (CList.CCons ret tl)
+ Result.ok (x, back)
else
do
let i1 ← i - 1#u32
@@ -83,8 +83,8 @@ divergent def list_nth_mut
fun ret =>
do
let tl1 ← list_nth_mut_back ret
- Result.ret (CList.CCons x tl1)
- Result.ret (t, back)
+ Result.ok (CList.CCons x tl1)
+ Result.ok (t, back)
| CList.CNil => Result.fail .panic
/- [demo::list_nth_mut1]: loop 0:
@@ -97,8 +97,8 @@ divergent def list_nth_mut1_loop
| CList.CCons x tl =>
if i = 0#u32
then
- let back := fun ret => Result.ret (CList.CCons ret tl)
- Result.ret (x, back)
+ let back := fun ret => Result.ok (CList.CCons ret tl)
+ Result.ok (x, back)
else
do
let i1 ← i - 1#u32
@@ -106,8 +106,8 @@ divergent def list_nth_mut1_loop
let back1 :=
fun ret => do
let tl1 ← back ret
- Result.ret (CList.CCons x tl1)
- Result.ret (t, back1)
+ Result.ok (CList.CCons x tl1)
+ Result.ok (t, back1)
| CList.CNil => Result.fail .panic
/- [demo::list_nth_mut1]:
@@ -122,7 +122,7 @@ def list_nth_mut1
Source: 'src/demo.rs', lines 80:0-80:28 -/
divergent def i32_id (i : I32) : Result I32 :=
if i = 0#i32
- then Result.ret 0#i32
+ then Result.ok 0#i32
else do
let i1 ← i - 1#i32
let i2 ← i32_id i1
@@ -142,9 +142,9 @@ divergent def list_tail
fun ret =>
do
let tl1 ← list_tail_back ret
- Result.ret (CList.CCons t tl1)
- Result.ret (c, back)
- | CList.CNil => Result.ret (CList.CNil, Result.ret)
+ Result.ok (CList.CCons t tl1)
+ Result.ok (c, back)
+ | CList.CNil => Result.ok (CList.CNil, Result.ok)
/- Trait declaration: [demo::Counter]
Source: 'src/demo.rs', lines 97:0-97:17 -/
@@ -156,7 +156,7 @@ structure Counter (Self : Type) where
def CounterUsize.incr (self : Usize) : Result (Usize × Usize) :=
do
let self1 ← self + 1#usize
- Result.ret (self, self1)
+ Result.ok (self, self1)
/- Trait implementation: [demo::{(demo::Counter for usize)}]
Source: 'src/demo.rs', lines 101:0-101:22 -/
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index cfb2cb3c..78e0f95c 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -26,10 +26,10 @@ def test_new_non_zero_u32
def test_vec : Result Unit :=
do
let _ ← alloc.vec.Vec.push U32 (alloc.vec.Vec.new U32) 0#u32
- Result.ret ()
+ Result.ok ()
/- Unit test for [external::test_vec] -/
-#assert (test_vec == Result.ret ())
+#assert (test_vec == Result.ok ())
/- [external::custom_swap]:
Source: 'src/external.rs', lines 24:0-24:66 -/
@@ -39,8 +39,8 @@ def custom_swap
:=
do
let (st1, (x1, y1)) ← core.mem.swap T x y st
- let back := fun ret st2 => Result.ret (st2, (ret, y1))
- Result.ret (st1, (x1, back))
+ let back := fun ret st2 => Result.ok (st2, (ret, y1))
+ Result.ok (st1, (x1, back))
/- [external::test_custom_swap]:
Source: 'src/external.rs', lines 29:0-29:59 -/
@@ -49,7 +49,7 @@ def test_custom_swap
do
let (st1, (_, custom_swap_back)) ← custom_swap U32 x y st
let (_, (x1, y1)) ← custom_swap_back 1#u32 st1
- Result.ret (st1, (x1, y1))
+ Result.ok (st1, (x1, y1))
/- [external::test_swap_non_zero]:
Source: 'src/external.rs', lines 35:0-35:44 -/
@@ -59,6 +59,6 @@ def test_swap_non_zero (x : U32) (st : State) : Result (State × U32) :=
let (x1, _) := p
if x1 = 0#u32
then Result.fail .panic
- else Result.ret (st1, x1)
+ else Result.ok (st1, x1)
end external
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 363d751a..9cbd958c 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -9,7 +9,7 @@ namespace hashmap
/- [hashmap::hash_key]:
Source: 'src/hashmap.rs', lines 27:0-27:32 -/
def hash_key (k : Usize) : Result Usize :=
- Result.ret k
+ Result.ok k
/- [hashmap::{hashmap::HashMap<T>}::allocate_slots]: loop 0:
Source: 'src/hashmap.rs', lines 50:4-56:5 -/
@@ -23,7 +23,7 @@ divergent def HashMap.allocate_slots_loop
let slots1 ← alloc.vec.Vec.push (List T) slots List.Nil
let n1 ← n - 1#usize
HashMap.allocate_slots_loop T slots1 n1
- else Result.ret slots
+ else Result.ok slots
/- [hashmap::{hashmap::HashMap<T>}::allocate_slots]:
Source: 'src/hashmap.rs', lines 50:4-50:76 -/
@@ -44,7 +44,7 @@ def HashMap.new_with_capacity
let slots ← HashMap.allocate_slots T (alloc.vec.Vec.new (List T)) capacity
let i ← capacity * max_load_dividend
let i1 ← i / max_load_divisor
- Result.ret
+ Result.ok
{
num_entries := 0#usize,
max_load_factor := (max_load_dividend, max_load_divisor),
@@ -73,19 +73,19 @@ divergent def HashMap.clear_loop
let i2 ← i + 1#usize
let slots1 ← index_mut_back List.Nil
HashMap.clear_loop T slots1 i2
- else Result.ret slots
+ else Result.ok slots
/- [hashmap::{hashmap::HashMap<T>}::clear]:
Source: 'src/hashmap.rs', lines 80:4-80:27 -/
def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) :=
do
let hm ← HashMap.clear_loop T self.slots 0#usize
- Result.ret { self with num_entries := 0#usize, slots := hm }
+ Result.ok { self with num_entries := 0#usize, slots := hm }
/- [hashmap::{hashmap::HashMap<T>}::len]:
Source: 'src/hashmap.rs', lines 90:4-90:30 -/
def HashMap.len (T : Type) (self : HashMap T) : Result Usize :=
- Result.ret self.num_entries
+ Result.ok self.num_entries
/- [hashmap::{hashmap::HashMap<T>}::insert_in_list]: loop 0:
Source: 'src/hashmap.rs', lines 97:4-114:5 -/
@@ -96,12 +96,12 @@ divergent def HashMap.insert_in_list_loop
match ls with
| List.Cons ckey cvalue tl =>
if ckey = key
- then Result.ret (false, List.Cons ckey value tl)
+ then Result.ok (false, List.Cons ckey value tl)
else
do
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)
+ Result.ok (b, List.Cons ckey cvalue tl1)
+ | List.Nil => Result.ok (true, List.Cons key value List.Nil)
/- [hashmap::{hashmap::HashMap<T>}::insert_in_list]:
Source: 'src/hashmap.rs', lines 97:4-97:71 -/
@@ -130,10 +130,10 @@ def HashMap.insert_no_resize
do
let i1 ← self.num_entries + 1#usize
let v ← index_mut_back l1
- Result.ret { self with num_entries := i1, slots := v }
+ Result.ok { self with num_entries := i1, slots := v }
else do
let v ← index_mut_back l1
- Result.ret { self with slots := v }
+ Result.ok { self with slots := v }
/- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]: loop 0:
Source: 'src/hashmap.rs', lines 183:4-196:5 -/
@@ -144,7 +144,7 @@ divergent def HashMap.move_elements_from_list_loop
do
let ntable1 ← HashMap.insert_no_resize T ntable k v
HashMap.move_elements_from_list_loop T ntable1 tl
- | List.Nil => Result.ret ntable
+ | List.Nil => Result.ok ntable
/- [hashmap::{hashmap::HashMap<T>}::move_elements_from_list]:
Source: 'src/hashmap.rs', lines 183:4-183:72 -/
@@ -171,7 +171,7 @@ divergent def HashMap.move_elements_loop
let i2 ← i + 1#usize
let slots1 ← index_mut_back l1
HashMap.move_elements_loop T ntable1 slots1 i2
- else Result.ret (ntable, slots)
+ else Result.ok (ntable, slots)
/- [hashmap::{hashmap::HashMap<T>}::move_elements]:
Source: 'src/hashmap.rs', lines 171:4-171:95 -/
@@ -198,13 +198,13 @@ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) :=
let ntable ← HashMap.new_with_capacity T i3 i i1
let p ← HashMap.move_elements T ntable self.slots 0#usize
let (ntable1, _) := p
- Result.ret
+ Result.ok
{
ntable1
with
num_entries := self.num_entries, max_load_factor := (i, i1)
}
- else Result.ret { self with max_load_factor := (i, i1) }
+ else Result.ok { self with max_load_factor := (i, i1) }
/- [hashmap::{hashmap::HashMap<T>}::insert]:
Source: 'src/hashmap.rs', lines 129:4-129:48 -/
@@ -217,7 +217,7 @@ def HashMap.insert
let i ← HashMap.len T self1
if i > self1.max_load
then HashMap.try_resize T self1
- else Result.ret self1
+ else Result.ok self1
/- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
Source: 'src/hashmap.rs', lines 206:4-219:5 -/
@@ -226,9 +226,9 @@ divergent def HashMap.contains_key_in_list_loop
match ls with
| List.Cons ckey _ tl =>
if ckey = key
- then Result.ret true
+ then Result.ok true
else HashMap.contains_key_in_list_loop T key tl
- | List.Nil => Result.ret false
+ | List.Nil => Result.ok false
/- [hashmap::{hashmap::HashMap<T>}::contains_key_in_list]:
Source: 'src/hashmap.rs', lines 206:4-206:68 -/
@@ -256,7 +256,7 @@ divergent def HashMap.get_in_list_loop
match ls with
| List.Cons ckey cvalue tl =>
if ckey = key
- then Result.ret cvalue
+ then Result.ok cvalue
else HashMap.get_in_list_loop T key tl
| List.Nil => Result.fail .panic
@@ -287,8 +287,8 @@ divergent def HashMap.get_mut_in_list_loop
| List.Cons ckey cvalue tl =>
if ckey = key
then
- let back := fun ret => Result.ret (List.Cons ckey ret tl)
- Result.ret (cvalue, back)
+ let back := fun ret => Result.ok (List.Cons ckey ret tl)
+ Result.ok (cvalue, back)
else
do
let (t, back) ← HashMap.get_mut_in_list_loop T tl key
@@ -296,8 +296,8 @@ divergent def HashMap.get_mut_in_list_loop
fun ret =>
do
let tl1 ← back ret
- Result.ret (List.Cons ckey cvalue tl1)
- Result.ret (t, back1)
+ Result.ok (List.Cons ckey cvalue tl1)
+ Result.ok (t, back1)
| List.Nil => Result.fail .panic
/- [hashmap::{hashmap::HashMap<T>}::get_mut_in_list]:
@@ -327,8 +327,8 @@ def HashMap.get_mut
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)
+ Result.ok { self with slots := v }
+ Result.ok (t, back)
/- [hashmap::{hashmap::HashMap<T>}::remove_from_list]: loop 0:
Source: 'src/hashmap.rs', lines 265:4-291:5 -/
@@ -341,13 +341,13 @@ 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 _ cvalue tl1 => Result.ret (some cvalue, tl1)
+ | List.Cons _ cvalue tl1 => Result.ok (some cvalue, tl1)
| List.Nil => Result.fail .panic
else
do
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)
+ Result.ok (o, List.Cons ckey t tl1)
+ | List.Nil => Result.ok (none, List.Nil)
/- [hashmap::{hashmap::HashMap<T>}::remove_from_list]:
Source: 'src/hashmap.rs', lines 265:4-265:69 -/
@@ -373,12 +373,12 @@ def HashMap.remove
| none =>
do
let v ← index_mut_back l1
- Result.ret (none, { self with slots := v })
+ Result.ok (none, { self with slots := v })
| some x1 =>
do
let i1 ← self.num_entries - 1#usize
let v ← index_mut_back l1
- Result.ret (some x1, { self with num_entries := i1, slots := v })
+ Result.ok (some x1, { self with num_entries := i1, slots := v })
/- [hashmap::test1]:
Source: 'src/hashmap.rs', lines 315:0-315:10 -/
@@ -422,6 +422,6 @@ def test1 : Result Unit :=
let i4 ← HashMap.get U64 hm6 1056#usize
if ¬ (i4 = 256#u64)
then Result.fail .panic
- else Result.ret ()
+ else Result.ok ()
end hashmap
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index 6fac6940..e985ec6a 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -10,7 +10,7 @@ namespace hashmap_main
/- [hashmap_main::hashmap::hash_key]:
Source: 'src/hashmap.rs', lines 27:0-27:32 -/
def hashmap.hash_key (k : Usize) : Result Usize :=
- Result.ret k
+ Result.ok k
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]: loop 0:
Source: 'src/hashmap.rs', lines 50:4-56:5 -/
@@ -24,7 +24,7 @@ divergent def hashmap.HashMap.allocate_slots_loop
let slots1 ← alloc.vec.Vec.push (hashmap.List T) slots hashmap.List.Nil
let n1 ← n - 1#usize
hashmap.HashMap.allocate_slots_loop T slots1 n1
- else Result.ret slots
+ else Result.ok slots
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::allocate_slots]:
Source: 'src/hashmap.rs', lines 50:4-50:76 -/
@@ -47,7 +47,7 @@ def hashmap.HashMap.new_with_capacity
capacity
let i ← capacity * max_load_dividend
let i1 ← i / max_load_divisor
- Result.ret
+ Result.ok
{
num_entries := 0#usize,
max_load_factor := (max_load_dividend, max_load_divisor),
@@ -76,7 +76,7 @@ divergent def hashmap.HashMap.clear_loop
let i2 ← i + 1#usize
let slots1 ← index_mut_back hashmap.List.Nil
hashmap.HashMap.clear_loop T slots1 i2
- else Result.ret slots
+ else Result.ok slots
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::clear]:
Source: 'src/hashmap.rs', lines 80:4-80:27 -/
@@ -84,12 +84,12 @@ def hashmap.HashMap.clear
(T : Type) (self : hashmap.HashMap T) : Result (hashmap.HashMap T) :=
do
let hm ← hashmap.HashMap.clear_loop T self.slots 0#usize
- Result.ret { self with num_entries := 0#usize, slots := hm }
+ Result.ok { 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 -/
def hashmap.HashMap.len (T : Type) (self : hashmap.HashMap T) : Result Usize :=
- Result.ret self.num_entries
+ Result.ok self.num_entries
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]: loop 0:
Source: 'src/hashmap.rs', lines 97:4-114:5 -/
@@ -100,13 +100,13 @@ divergent def hashmap.HashMap.insert_in_list_loop
match ls with
| hashmap.List.Cons ckey cvalue tl =>
if ckey = key
- then Result.ret (false, hashmap.List.Cons ckey value tl)
+ then Result.ok (false, hashmap.List.Cons ckey value tl)
else
do
let (b, tl1) ← hashmap.HashMap.insert_in_list_loop T key value tl
- Result.ret (b, hashmap.List.Cons ckey cvalue tl1)
+ Result.ok (b, hashmap.List.Cons ckey cvalue tl1)
| hashmap.List.Nil =>
- Result.ret (true, hashmap.List.Cons key value hashmap.List.Nil)
+ Result.ok (true, hashmap.List.Cons key value hashmap.List.Nil)
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert_in_list]:
Source: 'src/hashmap.rs', lines 97:4-97:71 -/
@@ -136,10 +136,10 @@ def hashmap.HashMap.insert_no_resize
do
let i1 ← self.num_entries + 1#usize
let v ← index_mut_back l1
- Result.ret { self with num_entries := i1, slots := v }
+ Result.ok { self with num_entries := i1, slots := v }
else do
let v ← index_mut_back l1
- Result.ret { self with slots := v }
+ Result.ok { self with slots := v }
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]: loop 0:
Source: 'src/hashmap.rs', lines 183:4-196:5 -/
@@ -152,7 +152,7 @@ divergent def hashmap.HashMap.move_elements_from_list_loop
do
let ntable1 ← hashmap.HashMap.insert_no_resize T ntable k v
hashmap.HashMap.move_elements_from_list_loop T ntable1 tl
- | hashmap.List.Nil => Result.ret ntable
+ | hashmap.List.Nil => Result.ok ntable
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements_from_list]:
Source: 'src/hashmap.rs', lines 183:4-183:72 -/
@@ -181,7 +181,7 @@ divergent def hashmap.HashMap.move_elements_loop
let i2 ← i + 1#usize
let slots1 ← index_mut_back l1
hashmap.HashMap.move_elements_loop T ntable1 slots1 i2
- else Result.ret (ntable, slots)
+ else Result.ok (ntable, slots)
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::move_elements]:
Source: 'src/hashmap.rs', lines 171:4-171:95 -/
@@ -209,13 +209,13 @@ def hashmap.HashMap.try_resize
let ntable ← hashmap.HashMap.new_with_capacity T i3 i i1
let p ← hashmap.HashMap.move_elements T ntable self.slots 0#usize
let (ntable1, _) := p
- Result.ret
+ Result.ok
{
ntable1
with
num_entries := self.num_entries, max_load_factor := (i, i1)
}
- else Result.ret { self with max_load_factor := (i, i1) }
+ else Result.ok { self with max_load_factor := (i, i1) }
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::insert]:
Source: 'src/hashmap.rs', lines 129:4-129:48 -/
@@ -228,7 +228,7 @@ def hashmap.HashMap.insert
let i ← hashmap.HashMap.len T self1
if i > self1.max_load
then hashmap.HashMap.try_resize T self1
- else Result.ret self1
+ else Result.ok self1
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]: loop 0:
Source: 'src/hashmap.rs', lines 206:4-219:5 -/
@@ -237,9 +237,9 @@ divergent def hashmap.HashMap.contains_key_in_list_loop
match ls with
| hashmap.List.Cons ckey _ tl =>
if ckey = key
- then Result.ret true
+ then Result.ok true
else hashmap.HashMap.contains_key_in_list_loop T key tl
- | hashmap.List.Nil => Result.ret false
+ | hashmap.List.Nil => Result.ok false
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::contains_key_in_list]:
Source: 'src/hashmap.rs', lines 206:4-206:68 -/
@@ -268,7 +268,7 @@ divergent def hashmap.HashMap.get_in_list_loop
match ls with
| hashmap.List.Cons ckey cvalue tl =>
if ckey = key
- then Result.ret cvalue
+ then Result.ok cvalue
else hashmap.HashMap.get_in_list_loop T key tl
| hashmap.List.Nil => Result.fail .panic
@@ -302,8 +302,8 @@ divergent def hashmap.HashMap.get_mut_in_list_loop
| hashmap.List.Cons ckey cvalue tl =>
if ckey = key
then
- let back := fun ret => Result.ret (hashmap.List.Cons ckey ret tl)
- Result.ret (cvalue, back)
+ let back := fun ret => Result.ok (hashmap.List.Cons ckey ret tl)
+ Result.ok (cvalue, back)
else
do
let (t, back) ← hashmap.HashMap.get_mut_in_list_loop T tl key
@@ -311,8 +311,8 @@ divergent def hashmap.HashMap.get_mut_in_list_loop
fun ret =>
do
let tl1 ← back ret
- Result.ret (hashmap.List.Cons ckey cvalue tl1)
- Result.ret (t, back1)
+ Result.ok (hashmap.List.Cons ckey cvalue tl1)
+ Result.ok (t, back1)
| hashmap.List.Nil => Result.fail .panic
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::get_mut_in_list]:
@@ -343,8 +343,8 @@ def hashmap.HashMap.get_mut
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)
+ Result.ok { self with slots := v }
+ Result.ok (t, back)
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]: loop 0:
Source: 'src/hashmap.rs', lines 265:4-291:5 -/
@@ -360,13 +360,13 @@ divergent def hashmap.HashMap.remove_from_list_loop
core.mem.replace (hashmap.List T) (hashmap.List.Cons ckey t tl)
hashmap.List.Nil
match mv_ls with
- | hashmap.List.Cons _ cvalue tl1 => Result.ret (some cvalue, tl1)
+ | hashmap.List.Cons _ cvalue tl1 => Result.ok (some cvalue, tl1)
| hashmap.List.Nil => Result.fail .panic
else
do
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)
+ Result.ok (o, hashmap.List.Cons ckey t tl1)
+ | hashmap.List.Nil => Result.ok (none, hashmap.List.Nil)
/- [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap<T>}::remove_from_list]:
Source: 'src/hashmap.rs', lines 265:4-265:69 -/
@@ -395,12 +395,12 @@ def hashmap.HashMap.remove
| none =>
do
let v ← index_mut_back l1
- Result.ret (none, { self with slots := v })
+ Result.ok (none, { self with slots := v })
| some x1 =>
do
let i1 ← self.num_entries - 1#usize
let v ← index_mut_back l1
- Result.ret (some x1, { self with num_entries := i1, slots := v })
+ Result.ok (some x1, { self with num_entries := i1, slots := v })
/- [hashmap_main::hashmap::test1]:
Source: 'src/hashmap.rs', lines 315:0-315:10 -/
@@ -444,7 +444,7 @@ def hashmap.test1 : Result Unit :=
let i4 ← hashmap.HashMap.get U64 hm6 1056#usize
if ¬ (i4 = 256#u64)
then Result.fail .panic
- else Result.ret ()
+ else Result.ok ()
/- [hashmap_main::insert_on_disk]:
Source: 'src/hashmap_main.rs', lines 7:0-7:43 -/
@@ -458,6 +458,6 @@ def insert_on_disk
/- [hashmap_main::main]:
Source: 'src/hashmap_main.rs', lines 16:0-16:13 -/
def main : Result Unit :=
- Result.ret ()
+ Result.ok ()
end hashmap_main
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index 27434db8..eeba1add 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -65,7 +65,7 @@ divergent def sum_array_loop
let s1 ← s + i1
let i2 ← i + 1#usize
sum_array_loop N a i2 s1
- else Result.ret s
+ else Result.ok s
/- [loops::sum_array]:
Source: 'src/loops.rs', lines 50:0-50:52 -/
@@ -86,7 +86,7 @@ divergent def clear_loop
let i2 ← i + 1#usize
let v1 ← index_mut_back 0#u32
clear_loop v1 i2
- else Result.ret v
+ else Result.ok v
/- [loops::clear]:
Source: 'src/loops.rs', lines 62:0-62:30 -/
@@ -104,9 +104,9 @@ inductive List (T : Type) :=
divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool :=
match ls with
| List.Cons y tl => if y = x
- then Result.ret true
+ then Result.ok true
else list_mem_loop x tl
- | List.Nil => Result.ret false
+ | List.Nil => Result.ok false
/- [loops::list_mem]:
Source: 'src/loops.rs', lines 76:0-76:52 -/
@@ -121,8 +121,8 @@ divergent def list_nth_mut_loop_loop
| List.Cons x tl =>
if i = 0#u32
then
- let back := fun ret => Result.ret (List.Cons ret tl)
- Result.ret (x, back)
+ let back := fun ret => Result.ok (List.Cons ret tl)
+ Result.ok (x, back)
else
do
let i1 ← i - 1#u32
@@ -130,8 +130,8 @@ divergent def list_nth_mut_loop_loop
let back1 :=
fun ret => do
let tl1 ← back ret
- Result.ret (List.Cons x tl1)
- Result.ret (t, back1)
+ Result.ok (List.Cons x tl1)
+ Result.ok (t, back1)
| List.Nil => Result.fail .panic
/- [loops::list_nth_mut_loop]:
@@ -147,7 +147,7 @@ divergent def list_nth_shared_loop_loop
match ls with
| List.Cons x tl =>
if i = 0#u32
- then Result.ret x
+ then Result.ok x
else do
let i1 ← i - 1#u32
list_nth_shared_loop_loop T tl i1
@@ -168,16 +168,16 @@ divergent def get_elem_mut_loop
| List.Cons y tl =>
if y = x
then
- let back := fun ret => Result.ret (List.Cons ret tl)
- Result.ret (y, back)
+ let back := fun ret => Result.ok (List.Cons ret tl)
+ Result.ok (y, back)
else
do
let (i, back) ← get_elem_mut_loop x tl
let back1 :=
fun ret => do
let tl1 ← back ret
- Result.ret (List.Cons y tl1)
- Result.ret (i, back1)
+ Result.ok (List.Cons y tl1)
+ Result.ok (i, back1)
| List.Nil => Result.fail .panic
/- [loops::get_elem_mut]:
@@ -194,7 +194,7 @@ def get_elem_mut
let back1 := fun ret => do
let l ← back ret
index_mut_back l
- Result.ret (i, back1)
+ Result.ok (i, back1)
/- [loops::get_elem_shared]: loop 0:
Source: 'src/loops.rs', lines 129:0-143:1 -/
@@ -202,7 +202,7 @@ divergent def get_elem_shared_loop
(x : Usize) (ls : List Usize) : Result Usize :=
match ls with
| List.Cons y tl => if y = x
- then Result.ret y
+ then Result.ok y
else get_elem_shared_loop x tl
| List.Nil => Result.fail .panic
@@ -222,12 +222,12 @@ def id_mut
(T : Type) (ls : List T) :
Result ((List T) × (List T → Result (List T)))
:=
- Result.ret (ls, Result.ret)
+ Result.ok (ls, Result.ok)
/- [loops::id_shared]:
Source: 'src/loops.rs', lines 149:0-149:45 -/
def id_shared (T : Type) (ls : List T) : Result (List T) :=
- Result.ret ls
+ Result.ok ls
/- [loops::list_nth_mut_loop_with_id]: loop 0:
Source: 'src/loops.rs', lines 154:0-165:1 -/
@@ -237,8 +237,8 @@ divergent def list_nth_mut_loop_with_id_loop
| List.Cons x tl =>
if i = 0#u32
then
- let back := fun ret => Result.ret (List.Cons ret tl)
- Result.ret (x, back)
+ let back := fun ret => Result.ok (List.Cons ret tl)
+ Result.ok (x, back)
else
do
let i1 ← i - 1#u32
@@ -246,8 +246,8 @@ divergent def list_nth_mut_loop_with_id_loop
let back1 :=
fun ret => do
let tl1 ← back ret
- Result.ret (List.Cons x tl1)
- Result.ret (t, back1)
+ Result.ok (List.Cons x tl1)
+ Result.ok (t, back1)
| List.Nil => Result.fail .panic
/- [loops::list_nth_mut_loop_with_id]:
@@ -260,7 +260,7 @@ def list_nth_mut_loop_with_id
let back1 := fun ret => do
let l ← back ret
id_mut_back l
- Result.ret (t, back1)
+ Result.ok (t, back1)
/- [loops::list_nth_shared_loop_with_id]: loop 0:
Source: 'src/loops.rs', lines 168:0-179:1 -/
@@ -269,7 +269,7 @@ divergent def list_nth_shared_loop_with_id_loop
match ls with
| List.Cons x tl =>
if i = 0#u32
- then Result.ret x
+ then Result.ok x
else do
let i1 ← i - 1#u32
list_nth_shared_loop_with_id_loop T i1 tl
@@ -295,9 +295,9 @@ 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.ok (List.Cons ret tl0)
+ let back'b := fun ret => Result.ok (List.Cons ret tl1)
+ Result.ok ((x0, x1), back'a, back'b)
else
do
let i1 ← i - 1#u32
@@ -305,12 +305,12 @@ divergent def list_nth_mut_loop_pair_loop
let back'a1 :=
fun ret => do
let tl01 ← back'a ret
- Result.ret (List.Cons x0 tl01)
+ Result.ok (List.Cons x0 tl01)
let back'b1 :=
fun ret => do
let tl11 ← back'b ret
- Result.ret (List.Cons x1 tl11)
- Result.ret (p, back'a1, back'b1)
+ Result.ok (List.Cons x1 tl11)
+ Result.ok (p, back'a1, back'b1)
| List.Nil => Result.fail .panic
| List.Nil => Result.fail .panic
@@ -331,7 +331,7 @@ divergent def list_nth_shared_loop_pair_loop
match ls1 with
| List.Cons x1 tl1 =>
if i = 0#u32
- then Result.ret (x0, x1)
+ then Result.ok (x0, x1)
else do
let i1 ← i - 1#u32
list_nth_shared_loop_pair_loop T tl0 tl1 i1
@@ -359,8 +359,8 @@ divergent def list_nth_mut_loop_pair_merge_loop
let back :=
fun ret =>
let (t, t1) := ret
- Result.ret (List.Cons t tl0, List.Cons t1 tl1)
- Result.ret ((x0, x1), back)
+ Result.ok (List.Cons t tl0, List.Cons t1 tl1)
+ Result.ok ((x0, x1), back)
else
do
let i1 ← i - 1#u32
@@ -369,8 +369,8 @@ divergent def list_nth_mut_loop_pair_merge_loop
fun ret =>
do
let (tl01, tl11) ← back ret
- Result.ret (List.Cons x0 tl01, List.Cons x1 tl11)
- Result.ret (p, back1)
+ Result.ok (List.Cons x0 tl01, List.Cons x1 tl11)
+ Result.ok (p, back1)
| List.Nil => Result.fail .panic
| List.Nil => Result.fail .panic
@@ -391,7 +391,7 @@ divergent def list_nth_shared_loop_pair_merge_loop
match ls1 with
| List.Cons x1 tl1 =>
if i = 0#u32
- then Result.ret (x0, x1)
+ then Result.ok (x0, x1)
else
do
let i1 ← i - 1#u32
@@ -417,8 +417,8 @@ divergent def list_nth_mut_shared_loop_pair_loop
| List.Cons x1 tl1 =>
if i = 0#u32
then
- let back := fun ret => Result.ret (List.Cons ret tl0)
- Result.ret ((x0, x1), back)
+ let back := fun ret => Result.ok (List.Cons ret tl0)
+ Result.ok ((x0, x1), back)
else
do
let i1 ← i - 1#u32
@@ -426,8 +426,8 @@ divergent def list_nth_mut_shared_loop_pair_loop
let back1 :=
fun ret => do
let tl01 ← back ret
- Result.ret (List.Cons x0 tl01)
- Result.ret (p, back1)
+ Result.ok (List.Cons x0 tl01)
+ Result.ok (p, back1)
| List.Nil => Result.fail .panic
| List.Nil => Result.fail .panic
@@ -451,8 +451,8 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop
| List.Cons x1 tl1 =>
if i = 0#u32
then
- let back := fun ret => Result.ret (List.Cons ret tl0)
- Result.ret ((x0, x1), back)
+ let back := fun ret => Result.ok (List.Cons ret tl0)
+ Result.ok ((x0, x1), back)
else
do
let i1 ← i - 1#u32
@@ -460,8 +460,8 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop
let back1 :=
fun ret => do
let tl01 ← back ret
- Result.ret (List.Cons x0 tl01)
- Result.ret (p, back1)
+ Result.ok (List.Cons x0 tl01)
+ Result.ok (p, back1)
| List.Nil => Result.fail .panic
| List.Nil => Result.fail .panic
@@ -485,8 +485,8 @@ divergent def list_nth_shared_mut_loop_pair_loop
| List.Cons x1 tl1 =>
if i = 0#u32
then
- let back := fun ret => Result.ret (List.Cons ret tl1)
- Result.ret ((x0, x1), back)
+ let back := fun ret => Result.ok (List.Cons ret tl1)
+ Result.ok ((x0, x1), back)
else
do
let i1 ← i - 1#u32
@@ -494,8 +494,8 @@ divergent def list_nth_shared_mut_loop_pair_loop
let back1 :=
fun ret => do
let tl11 ← back ret
- Result.ret (List.Cons x1 tl11)
- Result.ret (p, back1)
+ Result.ok (List.Cons x1 tl11)
+ Result.ok (p, back1)
| List.Nil => Result.fail .panic
| List.Nil => Result.fail .panic
@@ -519,8 +519,8 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop
| List.Cons x1 tl1 =>
if i = 0#u32
then
- let back := fun ret => Result.ret (List.Cons ret tl1)
- Result.ret ((x0, x1), back)
+ let back := fun ret => Result.ok (List.Cons ret tl1)
+ Result.ok ((x0, x1), back)
else
do
let i1 ← i - 1#u32
@@ -528,8 +528,8 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop
let back1 :=
fun ret => do
let tl11 ← back ret
- Result.ret (List.Cons x1 tl11)
- Result.ret (p, back1)
+ Result.ok (List.Cons x1 tl11)
+ Result.ok (p, back1)
| List.Nil => Result.fail .panic
| List.Nil => Result.fail .panic
@@ -548,14 +548,14 @@ divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
then do
let i1 ← i - 1#u32
ignore_input_mut_borrow_loop i1
- else Result.ret ()
+ else Result.ok ()
/- [loops::ignore_input_mut_borrow]:
Source: 'src/loops.rs', lines 345:0-345:56 -/
def ignore_input_mut_borrow (_a : U32) (i : U32) : Result U32 :=
do
let _ ← ignore_input_mut_borrow_loop i
- Result.ret _a
+ Result.ok _a
/- [loops::incr_ignore_input_mut_borrow]: loop 0:
Source: 'src/loops.rs', lines 353:0-358:1 -/
@@ -564,7 +564,7 @@ divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
then do
let i1 ← i - 1#u32
incr_ignore_input_mut_borrow_loop i1
- else Result.ret ()
+ else Result.ok ()
/- [loops::incr_ignore_input_mut_borrow]:
Source: 'src/loops.rs', lines 353:0-353:60 -/
@@ -572,7 +572,7 @@ def incr_ignore_input_mut_borrow (a : U32) (i : U32) : Result U32 :=
do
let a1 ← a + 1#u32
let _ ← incr_ignore_input_mut_borrow_loop i
- Result.ret a1
+ Result.ok a1
/- [loops::ignore_input_shared_borrow]: loop 0:
Source: 'src/loops.rs', lines 362:0-366:1 -/
@@ -581,13 +581,13 @@ divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit :=
then do
let i1 ← i - 1#u32
ignore_input_shared_borrow_loop i1
- else Result.ret ()
+ else Result.ok ()
/- [loops::ignore_input_shared_borrow]:
Source: 'src/loops.rs', lines 362:0-362:59 -/
def ignore_input_shared_borrow (_a : U32) (i : U32) : Result U32 :=
do
let _ ← ignore_input_shared_borrow_loop i
- Result.ret _a
+ Result.ok _a
end loops
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index b90f6aef..7d28f7f9 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -159,24 +159,24 @@ def cast_bool_to_i32 (x : Bool) : Result I32 :=
/- [no_nested_borrows::cast_bool_to_bool]:
Source: 'src/no_nested_borrows.rs', lines 137:0-137:41 -/
def cast_bool_to_bool (x : Bool) : Result Bool :=
- Result.ret x
+ Result.ok x
/- [no_nested_borrows::test2]:
Source: 'src/no_nested_borrows.rs', lines 142:0-142:14 -/
def test2 : Result Unit :=
do
let _ ← 23#u32 + 44#u32
- Result.ret ()
+ Result.ok ()
/- Unit test for [no_nested_borrows::test2] -/
-#assert (test2 == Result.ret ())
+#assert (test2 == Result.ok ())
/- [no_nested_borrows::get_max]:
Source: 'src/no_nested_borrows.rs', lines 154:0-154:37 -/
def get_max (x : U32) (y : U32) : Result U32 :=
if x >= y
- then Result.ret x
- else Result.ret y
+ then Result.ok x
+ else Result.ok y
/- [no_nested_borrows::test3]:
Source: 'src/no_nested_borrows.rs', lines 162:0-162:14 -/
@@ -187,10 +187,10 @@ def test3 : Result Unit :=
let z ← x + y
if ¬ (z = 15#u32)
then Result.fail .panic
- else Result.ret ()
+ else Result.ok ()
/- Unit test for [no_nested_borrows::test3] -/
-#assert (test3 == Result.ret ())
+#assert (test3 == Result.ok ())
/- [no_nested_borrows::test_neg1]:
Source: 'src/no_nested_borrows.rs', lines 169:0-169:18 -/
@@ -199,20 +199,20 @@ def test_neg1 : Result Unit :=
let y ← -. 3#i32
if ¬ (y = (-3)#i32)
then Result.fail .panic
- else Result.ret ()
+ else Result.ok ()
/- Unit test for [no_nested_borrows::test_neg1] -/
-#assert (test_neg1 == Result.ret ())
+#assert (test_neg1 == Result.ok ())
/- [no_nested_borrows::refs_test1]:
Source: 'src/no_nested_borrows.rs', lines 176:0-176:19 -/
def refs_test1 : Result Unit :=
if ¬ (1#i32 = 1#i32)
then Result.fail .panic
- else Result.ret ()
+ else Result.ok ()
/- Unit test for [no_nested_borrows::refs_test1] -/
-#assert (refs_test1 == Result.ret ())
+#assert (refs_test1 == Result.ok ())
/- [no_nested_borrows::refs_test2]:
Source: 'src/no_nested_borrows.rs', lines 187:0-187:19 -/
@@ -227,18 +227,18 @@ def refs_test2 : Result Unit :=
then Result.fail .panic
else if ¬ (2#i32 = 2#i32)
then Result.fail .panic
- else Result.ret ()
+ else Result.ok ()
/- Unit test for [no_nested_borrows::refs_test2] -/
-#assert (refs_test2 == Result.ret ())
+#assert (refs_test2 == Result.ok ())
/- [no_nested_borrows::test_list1]:
Source: 'src/no_nested_borrows.rs', lines 203:0-203:19 -/
def test_list1 : Result Unit :=
- Result.ret ()
+ Result.ok ()
/- Unit test for [no_nested_borrows::test_list1] -/
-#assert (test_list1 == Result.ret ())
+#assert (test_list1 == Result.ok ())
/- [no_nested_borrows::test_box1]:
Source: 'src/no_nested_borrows.rs', lines 208:0-208:18 -/
@@ -249,29 +249,29 @@ def test_box1 : Result Unit :=
let x ← alloc.boxed.Box.deref I32 b
if ¬ (x = 1#i32)
then Result.fail .panic
- else Result.ret ()
+ else Result.ok ()
/- Unit test for [no_nested_borrows::test_box1] -/
-#assert (test_box1 == Result.ret ())
+#assert (test_box1 == Result.ok ())
/- [no_nested_borrows::copy_int]:
Source: 'src/no_nested_borrows.rs', lines 218:0-218:30 -/
def copy_int (x : I32) : Result I32 :=
- Result.ret x
+ Result.ok x
/- [no_nested_borrows::test_unreachable]:
Source: 'src/no_nested_borrows.rs', lines 224:0-224:32 -/
def test_unreachable (b : Bool) : Result Unit :=
if b
then Result.fail .panic
- else Result.ret ()
+ else Result.ok ()
/- [no_nested_borrows::test_panic]:
Source: 'src/no_nested_borrows.rs', lines 232:0-232:26 -/
def test_panic (b : Bool) : Result Unit :=
if b
then Result.fail .panic
- else Result.ret ()
+ else Result.ok ()
/- [no_nested_borrows::test_copy_int]:
Source: 'src/no_nested_borrows.rs', lines 239:0-239:22 -/
@@ -280,17 +280,17 @@ def test_copy_int : Result Unit :=
let y ← copy_int 0#i32
if ¬ (0#i32 = y)
then Result.fail .panic
- else Result.ret ()
+ else Result.ok ()
/- Unit test for [no_nested_borrows::test_copy_int] -/
-#assert (test_copy_int == Result.ret ())
+#assert (test_copy_int == Result.ok ())
/- [no_nested_borrows::is_cons]:
Source: 'src/no_nested_borrows.rs', lines 246:0-246:38 -/
def is_cons (T : Type) (l : List T) : Result Bool :=
match l with
- | List.Cons _ _ => Result.ret true
- | List.Nil => Result.ret false
+ | List.Cons _ _ => Result.ok true
+ | List.Nil => Result.ok false
/- [no_nested_borrows::test_is_cons]:
Source: 'src/no_nested_borrows.rs', lines 253:0-253:21 -/
@@ -299,16 +299,16 @@ def test_is_cons : Result Unit :=
let b ← is_cons I32 (List.Cons 0#i32 List.Nil)
if ¬ b
then Result.fail .panic
- else Result.ret ()
+ else Result.ok ()
/- Unit test for [no_nested_borrows::test_is_cons] -/
-#assert (test_is_cons == Result.ret ())
+#assert (test_is_cons == Result.ok ())
/- [no_nested_borrows::split_list]:
Source: 'src/no_nested_borrows.rs', lines 259:0-259: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.Cons hd tl => Result.ok (hd, tl)
| List.Nil => Result.fail .panic
/- [no_nested_borrows::test_split_list]:
@@ -319,10 +319,10 @@ def test_split_list : Result Unit :=
let (hd, _) := p
if ¬ (hd = 0#i32)
then Result.fail .panic
- else Result.ret ()
+ else Result.ok ()
/- Unit test for [no_nested_borrows::test_split_list] -/
-#assert (test_split_list == Result.ret ())
+#assert (test_split_list == Result.ok ())
/- [no_nested_borrows::choose]:
Source: 'src/no_nested_borrows.rs', lines 274:0-274:70 -/
@@ -331,10 +331,10 @@ def choose
Result (T × (T → Result (T × T)))
:=
if b
- 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)
+ then let back := fun ret => Result.ok (ret, y)
+ Result.ok (x, back)
+ else let back := fun ret => Result.ok (x, ret)
+ Result.ok (y, back)
/- [no_nested_borrows::choose_test]:
Source: 'src/no_nested_borrows.rs', lines 282:0-282:20 -/
@@ -351,15 +351,15 @@ def choose_test : Result Unit :=
then Result.fail .panic
else if ¬ (y = 0#i32)
then Result.fail .panic
- else Result.ret ()
+ else Result.ok ()
/- Unit test for [no_nested_borrows::choose_test] -/
-#assert (choose_test == Result.ret ())
+#assert (choose_test == Result.ok ())
/- [no_nested_borrows::test_char]:
Source: 'src/no_nested_borrows.rs', lines 294:0-294:26 -/
def test_char : Result Char :=
- Result.ret 'a'
+ Result.ok 'a'
mutual
@@ -384,7 +384,7 @@ divergent def list_length (T : Type) (l : List T) : Result U32 :=
| List.Cons _ l1 => do
let i ← list_length T l1
1#u32 + i
- | List.Nil => Result.ret 0#u32
+ | List.Nil => Result.ok 0#u32
/- [no_nested_borrows::list_nth_shared]:
Source: 'src/no_nested_borrows.rs', lines 347:0-347:62 -/
@@ -392,7 +392,7 @@ divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T :=
match l with
| List.Cons x tl =>
if i = 0#u32
- then Result.ret x
+ then Result.ok x
else do
let i1 ← i - 1#u32
list_nth_shared T tl i1
@@ -406,8 +406,8 @@ divergent def list_nth_mut
| List.Cons x tl =>
if i = 0#u32
then
- let back := fun ret => Result.ret (List.Cons ret tl)
- Result.ret (x, back)
+ let back := fun ret => Result.ok (List.Cons ret tl)
+ Result.ok (x, back)
else
do
let i1 ← i - 1#u32
@@ -416,8 +416,8 @@ divergent def list_nth_mut
fun ret =>
do
let tl1 ← list_nth_mut_back ret
- Result.ret (List.Cons x tl1)
- Result.ret (t, back)
+ Result.ok (List.Cons x tl1)
+ Result.ok (t, back)
| List.Nil => Result.fail .panic
/- [no_nested_borrows::list_rev_aux]:
@@ -426,7 +426,7 @@ divergent def list_rev_aux
(T : Type) (li : List T) (lo : List T) : Result (List T) :=
match li with
| List.Cons hd tl => list_rev_aux T tl (List.Cons hd lo)
- | List.Nil => Result.ret lo
+ | List.Nil => Result.ok lo
/- [no_nested_borrows::list_rev]:
Source: 'src/no_nested_borrows.rs', lines 393:0-393:42 -/
@@ -476,10 +476,10 @@ def test_list_functions : Result Unit :=
let i6 ← list_nth_shared I32 ls 2#u32
if ¬ (i6 = 2#i32)
then Result.fail .panic
- else Result.ret ()
+ else Result.ok ()
/- Unit test for [no_nested_borrows::test_list_functions] -/
-#assert (test_list_functions == Result.ret ())
+#assert (test_list_functions == Result.ok ())
/- [no_nested_borrows::id_mut_pair1]:
Source: 'src/no_nested_borrows.rs', lines 414:0-414:89 -/
@@ -487,7 +487,7 @@ def id_mut_pair1
(T1 T2 : Type) (x : T1) (y : T2) :
Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2)))
:=
- Result.ret ((x, y), Result.ret)
+ Result.ok ((x, y), Result.ok)
/- [no_nested_borrows::id_mut_pair2]:
Source: 'src/no_nested_borrows.rs', lines 418:0-418:88 -/
@@ -496,7 +496,7 @@ def id_mut_pair2
Result ((T1 × T2) × ((T1 × T2) → Result (T1 × T2)))
:=
let (t, t1) := p
- Result.ret ((t, t1), Result.ret)
+ Result.ok ((t, t1), Result.ok)
/- [no_nested_borrows::id_mut_pair3]:
Source: 'src/no_nested_borrows.rs', lines 422:0-422:93 -/
@@ -504,7 +504,7 @@ def id_mut_pair3
(T1 T2 : Type) (x : T1) (y : T2) :
Result ((T1 × T2) × (T1 → Result T1) × (T2 → Result T2))
:=
- Result.ret ((x, y), Result.ret, Result.ret)
+ Result.ok ((x, y), Result.ok, Result.ok)
/- [no_nested_borrows::id_mut_pair4]:
Source: 'src/no_nested_borrows.rs', lines 426:0-426:92 -/
@@ -513,7 +513,7 @@ def id_mut_pair4
Result ((T1 × T2) × (T1 → Result T1) × (T2 → Result T2))
:=
let (t, t1) := p
- Result.ret ((t, t1), Result.ret, Result.ret)
+ Result.ok ((t, t1), Result.ok, Result.ok)
/- [no_nested_borrows::StructWithTuple]
Source: 'src/no_nested_borrows.rs', lines 433:0-433:34 -/
@@ -523,17 +523,17 @@ structure StructWithTuple (T1 T2 : Type) where
/- [no_nested_borrows::new_tuple1]:
Source: 'src/no_nested_borrows.rs', lines 437:0-437:48 -/
def new_tuple1 : Result (StructWithTuple U32 U32) :=
- Result.ret { p := (1#u32, 2#u32) }
+ Result.ok { p := (1#u32, 2#u32) }
/- [no_nested_borrows::new_tuple2]:
Source: 'src/no_nested_borrows.rs', lines 441:0-441:48 -/
def new_tuple2 : Result (StructWithTuple I16 I16) :=
- Result.ret { p := (1#i16, 2#i16) }
+ Result.ok { p := (1#i16, 2#i16) }
/- [no_nested_borrows::new_tuple3]:
Source: 'src/no_nested_borrows.rs', lines 445:0-445:48 -/
def new_tuple3 : Result (StructWithTuple U64 I64) :=
- Result.ret { p := (1#u64, 2#i64) }
+ Result.ok { p := (1#u64, 2#i64) }
/- [no_nested_borrows::StructWithPair]
Source: 'src/no_nested_borrows.rs', lines 450:0-450:33 -/
@@ -543,7 +543,7 @@ structure StructWithPair (T1 T2 : Type) where
/- [no_nested_borrows::new_pair1]:
Source: 'src/no_nested_borrows.rs', lines 454:0-454:46 -/
def new_pair1 : Result (StructWithPair U32 U32) :=
- Result.ret { p := { x := 1#u32, y := 2#u32 } }
+ Result.ok { p := { x := 1#u32, y := 2#u32 } }
/- [no_nested_borrows::test_constants]:
Source: 'src/no_nested_borrows.rs', lines 462:0-462:23 -/
@@ -570,18 +570,18 @@ def test_constants : Result Unit :=
let swp ← new_pair1
if ¬ (swp.p.x = 1#u32)
then Result.fail .panic
- else Result.ret ()
+ else Result.ok ()
/- Unit test for [no_nested_borrows::test_constants] -/
-#assert (test_constants == Result.ret ())
+#assert (test_constants == Result.ok ())
/- [no_nested_borrows::test_weird_borrows1]:
Source: 'src/no_nested_borrows.rs', lines 471:0-471:28 -/
def test_weird_borrows1 : Result Unit :=
- Result.ret ()
+ Result.ok ()
/- Unit test for [no_nested_borrows::test_weird_borrows1] -/
-#assert (test_weird_borrows1 == Result.ret ())
+#assert (test_weird_borrows1 == Result.ok ())
/- [no_nested_borrows::test_mem_replace]:
Source: 'src/no_nested_borrows.rs', lines 481:0-481:37 -/
@@ -589,31 +589,31 @@ def test_mem_replace (px : U32) : Result U32 :=
let (y, _) := core.mem.replace U32 px 1#u32
if ¬ (y = 0#u32)
then Result.fail .panic
- else Result.ret 2#u32
+ else Result.ok 2#u32
/- [no_nested_borrows::test_shared_borrow_bool1]:
Source: 'src/no_nested_borrows.rs', lines 488:0-488:47 -/
def test_shared_borrow_bool1 (b : Bool) : Result U32 :=
if b
- then Result.ret 0#u32
- else Result.ret 1#u32
+ then Result.ok 0#u32
+ else Result.ok 1#u32
/- [no_nested_borrows::test_shared_borrow_bool2]:
Source: 'src/no_nested_borrows.rs', lines 501:0-501:40 -/
def test_shared_borrow_bool2 : Result U32 :=
- Result.ret 0#u32
+ Result.ok 0#u32
/- [no_nested_borrows::test_shared_borrow_enum1]:
Source: 'src/no_nested_borrows.rs', lines 516:0-516:52 -/
def test_shared_borrow_enum1 (l : List U32) : Result U32 :=
match l with
- | List.Cons _ _ => Result.ret 1#u32
- | List.Nil => Result.ret 0#u32
+ | List.Cons _ _ => Result.ok 1#u32
+ | List.Nil => Result.ok 0#u32
/- [no_nested_borrows::test_shared_borrow_enum2]:
Source: 'src/no_nested_borrows.rs', lines 528:0-528:40 -/
def test_shared_borrow_enum2 : Result U32 :=
- Result.ret 0#u32
+ Result.ok 0#u32
/- [no_nested_borrows::incr]:
Source: 'src/no_nested_borrows.rs', lines 539:0-539:24 -/
@@ -630,7 +630,7 @@ def call_incr (x : U32) : Result U32 :=
def read_then_incr (x : U32) : Result (U32 × U32) :=
do
let x1 ← x + 1#u32
- Result.ret (x, x1)
+ Result.ok (x, x1)
/- [no_nested_borrows::Tuple]
Source: 'src/no_nested_borrows.rs', lines 554:0-554:24 -/
@@ -639,12 +639,12 @@ def Tuple (T1 T2 : Type) := T1 × T2
/- [no_nested_borrows::use_tuple_struct]:
Source: 'src/no_nested_borrows.rs', lines 556:0-556:48 -/
def use_tuple_struct (x : Tuple U32 U32) : Result (Tuple U32 U32) :=
- Result.ret (1#u32, x.#1)
+ Result.ok (1#u32, x.#1)
/- [no_nested_borrows::create_tuple_struct]:
Source: 'src/no_nested_borrows.rs', lines 560:0-560:61 -/
def create_tuple_struct (x : U32) (y : U64) : Result (Tuple U32 U64) :=
- Result.ret (x, y)
+ Result.ok (x, y)
/- [no_nested_borrows::IdType]
Source: 'src/no_nested_borrows.rs', lines 565:0-565:20 -/
@@ -653,11 +653,11 @@ def create_tuple_struct (x : U32) (y : U64) : Result (Tuple U32 U64) :=
/- [no_nested_borrows::use_id_type]:
Source: 'src/no_nested_borrows.rs', lines 567:0-567:40 -/
def use_id_type (T : Type) (x : IdType T) : Result T :=
- Result.ret x
+ Result.ok x
/- [no_nested_borrows::create_id_type]:
Source: 'src/no_nested_borrows.rs', lines 571:0-571:43 -/
def create_id_type (T : Type) (x : T) : Result (IdType T) :=
- Result.ret x
+ Result.ok x
end no_nested_borrows
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index 5b00aa83..32203eca 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -17,10 +17,10 @@ def test_incr : Result Unit :=
let x ← ref_incr 0#i32
if ¬ (x = 1#i32)
then Result.fail .panic
- else Result.ret ()
+ else Result.ok ()
/- Unit test for [paper::test_incr] -/
-#assert (test_incr == Result.ret ())
+#assert (test_incr == Result.ok ())
/- [paper::choose]:
Source: 'src/paper.rs', lines 15:0-15:70 -/
@@ -29,10 +29,10 @@ def choose
Result (T × (T → Result (T × T)))
:=
if b
- 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)
+ then let back := fun ret => Result.ok (ret, y)
+ Result.ok (x, back)
+ else let back := fun ret => Result.ok (x, ret)
+ Result.ok (y, back)
/- [paper::test_choose]:
Source: 'src/paper.rs', lines 23:0-23:20 -/
@@ -49,10 +49,10 @@ def test_choose : Result Unit :=
then Result.fail .panic
else if ¬ (y = 0#i32)
then Result.fail .panic
- else Result.ret ()
+ else Result.ok ()
/- Unit test for [paper::test_choose] -/
-#assert (test_choose == Result.ret ())
+#assert (test_choose == Result.ok ())
/- [paper::List]
Source: 'src/paper.rs', lines 35:0-35:16 -/
@@ -68,8 +68,8 @@ divergent def list_nth_mut
| List.Cons x tl =>
if i = 0#u32
then
- let back := fun ret => Result.ret (List.Cons ret tl)
- Result.ret (x, back)
+ let back := fun ret => Result.ok (List.Cons ret tl)
+ Result.ok (x, back)
else
do
let i1 ← i - 1#u32
@@ -78,8 +78,8 @@ divergent def list_nth_mut
fun ret =>
do
let tl1 ← list_nth_mut_back ret
- Result.ret (List.Cons x tl1)
- Result.ret (t, back)
+ Result.ok (List.Cons x tl1)
+ Result.ok (t, back)
| List.Nil => Result.fail .panic
/- [paper::sum]:
@@ -89,7 +89,7 @@ divergent def sum (l : List I32) : Result I32 :=
| List.Cons x tl => do
let i ← sum tl
x + i
- | List.Nil => Result.ret 0#i32
+ | List.Nil => Result.ok 0#i32
/- [paper::test_nth]:
Source: 'src/paper.rs', lines 68:0-68:17 -/
@@ -103,10 +103,10 @@ def test_nth : Result Unit :=
let i ← sum l2
if ¬ (i = 7#i32)
then Result.fail .panic
- else Result.ret ()
+ else Result.ok ()
/- Unit test for [paper::test_nth] -/
-#assert (test_nth == Result.ret ())
+#assert (test_nth == Result.ok ())
/- [paper::call_choose]:
Source: 'src/paper.rs', lines 76:0-76:44 -/
@@ -116,6 +116,6 @@ def call_choose (p : (U32 × U32)) : Result U32 :=
let (pz, choose_back) ← choose U32 true px py
let pz1 ← pz + 1#u32
let (px1, _) ← choose_back pz1
- Result.ret px1
+ Result.ok px1
end paper
diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index c657237f..09f41056 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -20,7 +20,7 @@ divergent def get_list_at_x
match ls with
| List.Cons hd tl =>
if hd = x
- then Result.ret (List.Cons hd tl, Result.ret)
+ then Result.ok (List.Cons hd tl, Result.ok)
else
do
let (l, get_list_at_x_back) ← get_list_at_x tl x
@@ -28,8 +28,8 @@ divergent def get_list_at_x
fun ret =>
do
let tl1 ← get_list_at_x_back ret
- Result.ret (List.Cons hd tl1)
- Result.ret (l, back)
- | List.Nil => Result.ret (List.Nil, Result.ret)
+ Result.ok (List.Cons hd tl1)
+ Result.ok (l, back)
+ | List.Nil => Result.ok (List.Nil, Result.ok)
end polonius_list
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index 766b109d..0076e6f6 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -13,7 +13,7 @@ structure BoolTrait (Self : Type) where
/- [traits::{(traits::BoolTrait for bool)}::get_bool]:
Source: 'src/traits.rs', lines 12:4-12:30 -/
def BoolTraitBool.get_bool (self : Bool) : Result Bool :=
- Result.ret self
+ Result.ok self
/- Trait implementation: [traits::{(traits::BoolTrait for bool)}]
Source: 'src/traits.rs', lines 11:0-11:23 -/
@@ -25,7 +25,7 @@ def BoolTraitBool : BoolTrait Bool := {
Source: 'src/traits.rs', lines 6:4-6:30 -/
def BoolTrait.ret_true
{Self : Type} (self_clause : BoolTrait Self) (self : Self) : Result Bool :=
- Result.ret true
+ Result.ok true
/- [traits::test_bool_trait_bool]:
Source: 'src/traits.rs', lines 17:0-17:44 -/
@@ -34,14 +34,14 @@ def test_bool_trait_bool (x : Bool) : Result Bool :=
let b ← BoolTraitBool.get_bool x
if b
then BoolTrait.ret_true BoolTraitBool x
- else Result.ret false
+ else Result.ok false
/- [traits::{(traits::BoolTrait for core::option::Option<T>)#1}::get_bool]:
Source: 'src/traits.rs', lines 23:4-23:30 -/
def BoolTraitOption.get_bool (T : Type) (self : Option T) : Result Bool :=
match self with
- | none => Result.ret false
- | some _ => Result.ret true
+ | none => Result.ok false
+ | some _ => Result.ok true
/- Trait implementation: [traits::{(traits::BoolTrait for core::option::Option<T>)#1}]
Source: 'src/traits.rs', lines 22:0-22:31 -/
@@ -56,7 +56,7 @@ def test_bool_trait_option (T : Type) (x : Option T) : Result Bool :=
let b ← BoolTraitOption.get_bool T x
if b
then BoolTrait.ret_true (BoolTraitOption T) x
- else Result.ret false
+ else Result.ok false
/- [traits::test_bool_trait]:
Source: 'src/traits.rs', lines 35:0-35:50 -/
@@ -72,7 +72,7 @@ structure ToU64 (Self : Type) where
/- [traits::{(traits::ToU64 for u64)#2}::to_u64]:
Source: 'src/traits.rs', lines 44:4-44:26 -/
def ToU64U64.to_u64 (self : U64) : Result U64 :=
- Result.ret self
+ Result.ok self
/- Trait implementation: [traits::{(traits::ToU64 for u64)#2}]
Source: 'src/traits.rs', lines 43:0-43:18 -/
@@ -148,7 +148,7 @@ structure ToType (Self T : Type) where
/- [traits::{(traits::ToType<bool> for u64)#5}::to_type]:
Source: 'src/traits.rs', lines 93:4-93:28 -/
def ToTypeU64Bool.to_type (self : U64) : Result Bool :=
- Result.ret (self > 0#u64)
+ Result.ok (self > 0#u64)
/- Trait implementation: [traits::{(traits::ToType<bool> for u64)#5}]
Source: 'src/traits.rs', lines 92:0-92:25 -/
@@ -202,7 +202,7 @@ structure TestType.test.TestTrait (Self : Type) where
Source: 'src/traits.rs', lines 139:12-139:34 -/
def TestType.test.TestTraittraitsTestTypetestTestType1.test
(self : TestType.test.TestType1) : Result Bool :=
- Result.ret (self > 1#u64)
+ Result.ok (self > 1#u64)
/- Trait implementation: [traits::{traits::TestType<T>#6}::test::{(traits::{traits::TestType<T>#6}::test::TestTrait for traits::{traits::TestType<T>#6}::test::TestType1)}]
Source: 'src/traits.rs', lines 138:8-138:36 -/
@@ -219,7 +219,7 @@ def TestType.test
let x1 ← ToU64Inst.to_u64 x
if x1 > 0#u64
then TestType.test.TestTraittraitsTestTypetestTestType1.test 0#u64
- else Result.ret false
+ else Result.ok false
/- [traits::BoolWrapper]
Source: 'src/traits.rs', lines 150:0-150:22 -/
@@ -243,7 +243,7 @@ def ToTypetraitsBoolWrapperT (T : Type) (ToTypeBoolTInst : ToType Bool T) :
/- [traits::WithConstTy::LEN2]
Source: 'src/traits.rs', lines 164:4-164:21 -/
def WithConstTy.LEN2_default_body (Self : Type) (LEN : Usize) : Result Usize :=
- Result.ret 32#usize
+ Result.ok 32#usize
def WithConstTy.LEN2_default (Self : Type) (LEN : Usize) : Usize :=
eval_global (WithConstTy.LEN2_default_body Self LEN)
@@ -259,13 +259,13 @@ structure WithConstTy (Self : Type) (LEN : Usize) where
/- [traits::{(traits::WithConstTy<32: usize> for bool)#8}::LEN1]
Source: 'src/traits.rs', lines 175:4-175:21 -/
-def WithConstTyBool32.LEN1_body : Result Usize := Result.ret 12#usize
+def WithConstTyBool32.LEN1_body : Result Usize := Result.ok 12#usize
def WithConstTyBool32.LEN1 : Usize := eval_global WithConstTyBool32.LEN1_body
/- [traits::{(traits::WithConstTy<32: usize> for bool)#8}::f]:
Source: 'src/traits.rs', lines 180:4-180:39 -/
def WithConstTyBool32.f (i : U64) (a : Array U8 32#usize) : Result U64 :=
- Result.ret i
+ Result.ok i
/- Trait implementation: [traits::{(traits::WithConstTy<32: usize> for bool)#8}]
Source: 'src/traits.rs', lines 174:0-174:29 -/
@@ -284,7 +284,7 @@ def use_with_const_ty1
(H : Type) (LEN : Usize) (WithConstTyInst : WithConstTy H LEN) :
Result Usize
:=
- Result.ret WithConstTyInst.LEN1
+ Result.ok WithConstTyInst.LEN1
/- [traits::use_with_const_ty2]:
Source: 'src/traits.rs', lines 187:0-187:73 -/
@@ -293,7 +293,7 @@ def use_with_const_ty2
(w : WithConstTyInst.W) :
Result Unit
:=
- Result.ret ()
+ Result.ok ()
/- [traits::use_with_const_ty3]:
Source: 'src/traits.rs', lines 189:0-189:80 -/
@@ -307,7 +307,7 @@ def use_with_const_ty3
/- [traits::test_where1]:
Source: 'src/traits.rs', lines 193:0-193:40 -/
def test_where1 (T : Type) (_x : T) : Result Unit :=
- Result.ret ()
+ Result.ok ()
/- [traits::test_where2]:
Source: 'src/traits.rs', lines 194:0-194:57 -/
@@ -315,7 +315,7 @@ def test_where2
(T : Type) (WithConstTyT32Inst : WithConstTy T 32#usize) (_x : U32) :
Result Unit
:=
- Result.ret ()
+ Result.ok ()
/- Trait declaration: [traits::ParentTrait0]
Source: 'src/traits.rs', lines 200:0-200:22 -/
@@ -355,7 +355,7 @@ def order1
ParentTrait0 U) :
Result Unit
:=
- Result.ret ()
+ Result.ok ()
/- Trait declaration: [traits::ChildTrait1]
Source: 'src/traits.rs', lines 222:0-222:35 -/
@@ -429,7 +429,7 @@ def ParentTrait2U32 : ParentTrait2 U32 := {
/- [traits::{(traits::ChildTrait2 for u32)#13}::convert]:
Source: 'src/traits.rs', lines 273:4-273:29 -/
def ChildTrait2U32.convert (x : U32) : Result U32 :=
- Result.ret x
+ Result.ok x
/- Trait implementation: [traits::{(traits::ChildTrait2 for u32)#13}]
Source: 'src/traits.rs', lines 272:0-272:24 -/
@@ -475,7 +475,7 @@ structure Trait (Self : Type) where
/- [traits::{(traits::Trait for @Array<T, N>)#14}::LEN]
Source: 'src/traits.rs', lines 315:4-315:20 -/
-def TraitArray.LEN_body (T : Type) (N : Usize) : Result Usize := Result.ret N
+def TraitArray.LEN_body (T : Type) (N : Usize) : Result Usize := Result.ok N
def TraitArray.LEN (T : Type) (N : Usize) : Usize :=
eval_global (TraitArray.LEN_body T N)
@@ -489,7 +489,7 @@ def TraitArray (T : Type) (N : Usize) : Trait (Array T N) := {
Source: 'src/traits.rs', lines 319:4-319:20 -/
def TraittraitsWrapper.LEN_body (T : Type) (TraitInst : Trait T)
: Result Usize :=
- Result.ret 0#usize
+ Result.ok 0#usize
def TraittraitsWrapper.LEN (T : Type) (TraitInst : Trait T) : Usize :=
eval_global (TraittraitsWrapper.LEN_body T TraitInst)
@@ -503,7 +503,7 @@ def TraittraitsWrapper (T : Type) (TraitInst : Trait T) : Trait (Wrapper T)
/- [traits::use_wrapper_len]:
Source: 'src/traits.rs', lines 322:0-322:43 -/
def use_wrapper_len (T : Type) (TraitInst : Trait T) : Result Usize :=
- Result.ret (TraittraitsWrapper T TraitInst).LEN
+ Result.ok (TraittraitsWrapper T TraitInst).LEN
/- [traits::Foo]
Source: 'src/traits.rs', lines 326:0-326:20 -/
@@ -522,7 +522,7 @@ inductive core.result.Result (T E : Type) :=
Source: 'src/traits.rs', lines 332:4-332:33 -/
def Foo.FOO_body (T U : Type) (TraitInst : Trait T)
: Result (core.result.Result T I32) :=
- Result.ret (core.result.Result.Err 0#i32)
+ Result.ok (core.result.Result.Err 0#i32)
def Foo.FOO (T U : Type) (TraitInst : Trait T) : core.result.Result T I32 :=
eval_global (Foo.FOO_body T U TraitInst)
@@ -530,12 +530,12 @@ def Foo.FOO (T U : Type) (TraitInst : Trait T) : core.result.Result T I32 :=
Source: 'src/traits.rs', lines 335:0-335:48 -/
def use_foo1
(T U : Type) (TraitInst : Trait T) : Result (core.result.Result T I32) :=
- Result.ret (Foo.FOO T U TraitInst)
+ Result.ok (Foo.FOO T U TraitInst)
/- [traits::use_foo2]:
Source: 'src/traits.rs', lines 339:0-339:48 -/
def use_foo2
(T U : Type) (TraitInst : Trait U) : Result (core.result.Result U I32) :=
- Result.ret (Foo.FOO U T TraitInst)
+ Result.ok (Foo.FOO U T TraitInst)
end traits
generated by cgit v1.2.3 (git 2.25.1) at 2024-10-19 16:43:45 +0000