From cd5542fc82edee11181a43e3a342a2567c929e7e Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 12 Jun 2024 14:53:12 +0200 Subject: Regenerate the tests --- tests/lean/Arrays.lean | 225 ++++++++++++++++++++-------------------- tests/lean/Betree/Funs.lean | 22 ++-- tests/lean/Bitwise.lean | 8 +- tests/lean/Constants.lean | 28 ++--- tests/lean/Demo/Demo.lean | 28 ++--- tests/lean/External/Funs.lean | 2 +- tests/lean/Hashmap/Funs.lean | 62 +++++------ tests/lean/Loops.lean | 94 ++++++++--------- tests/lean/Matches.lean | 6 +- tests/lean/NoNestedBorrows.lean | 138 ++++++++++++------------ tests/lean/Paper.lean | 34 +++--- tests/lean/Traits.lean | 24 ++--- 12 files changed, 333 insertions(+), 338 deletions(-) (limited to 'tests') diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean index 9748919e..70b4a26b 100644 --- a/tests/lean/Arrays.lean +++ b/tests/lean/Arrays.lean @@ -14,34 +14,34 @@ inductive AB := /- [arrays::incr]: Source: 'tests/src/arrays.rs', lines 11:0-11:24 -/ def incr (x : U32) : Result U32 := - x + 1#u32 + x + 1u32 /- [arrays::array_to_shared_slice_]: Source: 'tests/src/arrays.rs', lines 19:0-19:53 -/ def array_to_shared_slice_ - (T : Type) (s : Array T 32#usize) : Result (Slice T) := - Array.to_slice T 32#usize s + (T : Type) (s : Array T 32usize) : Result (Slice T) := + Array.to_slice T 32usize s /- [arrays::array_to_mut_slice_]: Source: 'tests/src/arrays.rs', lines 24:0-24:58 -/ def array_to_mut_slice_ - (T : Type) (s : Array T 32#usize) : - Result ((Slice T) × (Slice T → Result (Array T 32#usize))) + (T : Type) (s : Array T 32usize) : + Result ((Slice T) × (Slice T → Result (Array T 32usize))) := - Array.to_slice_mut T 32#usize s + Array.to_slice_mut T 32usize s /- [arrays::array_len]: Source: 'tests/src/arrays.rs', lines 28:0-28:40 -/ -def array_len (T : Type) (s : Array T 32#usize) : Result Usize := +def array_len (T : Type) (s : Array T 32usize) : Result Usize := do - let s1 ← Array.to_slice T 32#usize s + let s1 ← Array.to_slice T 32usize s Result.ok (Slice.len T s1) /- [arrays::shared_array_len]: Source: 'tests/src/arrays.rs', lines 32:0-32:48 -/ -def shared_array_len (T : Type) (s : Array T 32#usize) : Result Usize := +def shared_array_len (T : Type) (s : Array T 32usize) : Result Usize := do - let s1 ← Array.to_slice T 32#usize s + let s1 ← Array.to_slice T 32usize s Result.ok (Slice.len T s1) /- [arrays::shared_slice_len]: @@ -52,26 +52,26 @@ def shared_slice_len (T : Type) (s : Slice T) : Result Usize := /- [arrays::index_array_shared]: Source: 'tests/src/arrays.rs', lines 40:0-40:57 -/ def index_array_shared - (T : Type) (s : Array T 32#usize) (i : Usize) : Result T := - Array.index_usize T 32#usize s i + (T : Type) (s : Array T 32usize) (i : Usize) : Result T := + Array.index_usize T 32usize s i /- [arrays::index_array_u32]: Source: 'tests/src/arrays.rs', lines 47:0-47:53 -/ -def index_array_u32 (s : Array U32 32#usize) (i : Usize) : Result U32 := - Array.index_usize U32 32#usize s i +def index_array_u32 (s : Array U32 32usize) (i : Usize) : Result U32 := + Array.index_usize U32 32usize s i /- [arrays::index_array_copy]: Source: 'tests/src/arrays.rs', lines 51:0-51:45 -/ -def index_array_copy (x : Array U32 32#usize) : Result U32 := - Array.index_usize U32 32#usize x 0#usize +def index_array_copy (x : Array U32 32usize) : Result U32 := + Array.index_usize U32 32usize x 0usize /- [arrays::index_mut_array]: Source: 'tests/src/arrays.rs', lines 55:0-55:62 -/ def index_mut_array - (T : Type) (s : Array T 32#usize) (i : Usize) : - Result (T × (T → Result (Array T 32#usize))) + (T : Type) (s : Array T 32usize) (i : Usize) : + Result (T × (T → Result (Array T 32usize))) := - Array.index_mut_usize T 32#usize s i + Array.index_mut_usize T 32usize s i /- [arrays::index_slice]: Source: 'tests/src/arrays.rs', lines 59:0-59:46 -/ @@ -109,22 +109,22 @@ def slice_subslice_mut_ /- [arrays::array_to_slice_shared_]: Source: 'tests/src/arrays.rs', lines 75:0-75:54 -/ -def array_to_slice_shared_ (x : Array U32 32#usize) : Result (Slice U32) := - Array.to_slice U32 32#usize x +def array_to_slice_shared_ (x : Array U32 32usize) : Result (Slice U32) := + Array.to_slice U32 32usize x /- [arrays::array_to_slice_mut_]: Source: 'tests/src/arrays.rs', lines 79:0-79:59 -/ def array_to_slice_mut_ - (x : Array U32 32#usize) : - Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize))) + (x : Array U32 32usize) : + Result ((Slice U32) × (Slice U32 → Result (Array U32 32usize))) := - Array.to_slice_mut U32 32#usize x + Array.to_slice_mut U32 32usize x /- [arrays::array_subslice_shared_]: Source: 'tests/src/arrays.rs', lines 83:0-83:74 -/ def array_subslice_shared_ - (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) := - core.array.Array.index U32 (core.ops.range.Range Usize) 32#usize + (x : Array U32 32usize) (y : Usize) (z : Usize) : Result (Slice U32) := + core.array.Array.index U32 (core.ops.range.Range Usize) 32usize (core.ops.index.IndexSliceTIInst U32 (core.ops.range.Range Usize) (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x { start := y, end_ := z } @@ -132,12 +132,12 @@ def array_subslice_shared_ /- [arrays::array_subslice_mut_]: Source: 'tests/src/arrays.rs', lines 87:0-87:79 -/ def array_subslice_mut_ - (x : Array U32 32#usize) (y : Usize) (z : Usize) : - Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize))) + (x : Array U32 32usize) (y : Usize) (z : Usize) : + Result ((Slice U32) × (Slice U32 → Result (Array U32 32usize))) := do let (s, index_mut_back) ← - core.array.Array.index_mut U32 (core.ops.range.Range Usize) 32#usize + core.array.Array.index_mut U32 (core.ops.range.Range Usize) 32usize (core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize) (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x { start := y, end_ := z } @@ -146,50 +146,50 @@ def array_subslice_mut_ /- [arrays::index_slice_0]: Source: 'tests/src/arrays.rs', lines 91:0-91:38 -/ def index_slice_0 (T : Type) (s : Slice T) : Result T := - Slice.index_usize T s 0#usize + Slice.index_usize T s 0usize /- [arrays::index_array_0]: Source: 'tests/src/arrays.rs', lines 95:0-95:42 -/ -def index_array_0 (T : Type) (s : Array T 32#usize) : Result T := - Array.index_usize T 32#usize s 0#usize +def index_array_0 (T : Type) (s : Array T 32usize) : Result T := + Array.index_usize T 32usize s 0usize /- [arrays::index_index_array]: Source: 'tests/src/arrays.rs', lines 106:0-106:71 -/ def index_index_array - (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) : + (s : Array (Array U32 32usize) 32usize) (i : Usize) (j : Usize) : Result U32 := do - let a ← Array.index_usize (Array U32 32#usize) 32#usize s i - Array.index_usize U32 32#usize a j + let a ← Array.index_usize (Array U32 32usize) 32usize s i + Array.index_usize U32 32usize a j /- [arrays::update_update_array]: Source: 'tests/src/arrays.rs', lines 117:0-117:70 -/ def update_update_array - (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) : + (s : Array (Array U32 32usize) 32usize) (i : Usize) (j : Usize) : Result Unit := do let (a, index_mut_back) ← - Array.index_mut_usize (Array U32 32#usize) 32#usize s i - let (_, index_mut_back1) ← Array.index_mut_usize U32 32#usize a j - let a1 ← index_mut_back1 0#u32 + Array.index_mut_usize (Array U32 32usize) 32usize s i + let (_, index_mut_back1) ← Array.index_mut_usize U32 32usize a j + let a1 ← index_mut_back1 0u32 let _ ← index_mut_back a1 Result.ok () /- [arrays::array_local_deep_copy]: Source: 'tests/src/arrays.rs', lines 121:0-121:43 -/ -def array_local_deep_copy (x : Array U32 32#usize) : Result Unit := +def array_local_deep_copy (x : Array U32 32usize) : Result Unit := Result.ok () /- [arrays::take_array]: Source: 'tests/src/arrays.rs', lines 125:0-125:30 -/ -def take_array (a : Array U32 2#usize) : Result Unit := +def take_array (a : Array U32 2usize) : Result Unit := Result.ok () /- [arrays::take_array_borrow]: Source: 'tests/src/arrays.rs', lines 126:0-126:38 -/ -def take_array_borrow (a : Array U32 2#usize) : Result Unit := +def take_array_borrow (a : Array U32 2usize) : Result Unit := Result.ok () /- [arrays::take_slice]: @@ -204,70 +204,67 @@ def take_mut_slice (s : Slice U32) : Result (Slice U32) := /- [arrays::const_array]: Source: 'tests/src/arrays.rs', lines 130:0-130:32 -/ -def const_array : Result (Array U32 2#usize) := - Result.ok (Array.make U32 2#usize [ 0#u32, 0#u32 ]) +def const_array : Result (Array U32 2usize) := + Result.ok (Array.make U32 2usize [ 0u32, 0u32 ]) /- [arrays::const_slice]: Source: 'tests/src/arrays.rs', lines 134:0-134:20 -/ def const_slice : Result Unit := do - let _ ← - Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let _ ← Array.to_slice U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) Result.ok () /- [arrays::take_all]: Source: 'tests/src/arrays.rs', lines 144:0-144:17 -/ def take_all : Result Unit := do - let _ ← take_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let _ ← take_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let _ ← take_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let s ← - Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let _ ← take_array (Array.make U32 2usize [ 0u32, 0u32 ]) + let _ ← take_array (Array.make U32 2usize [ 0u32, 0u32 ]) + let _ ← take_array_borrow (Array.make U32 2usize [ 0u32, 0u32 ]) + let s ← Array.to_slice U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) let _ ← take_slice s let (s1, to_slice_mut_back) ← - Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) let s2 ← take_mut_slice s1 let _ ← to_slice_mut_back s2 Result.ok () /- [arrays::index_array]: Source: 'tests/src/arrays.rs', lines 158:0-158:38 -/ -def index_array (x : Array U32 2#usize) : Result U32 := - Array.index_usize U32 2#usize x 0#usize +def index_array (x : Array U32 2usize) : Result U32 := + Array.index_usize U32 2usize x 0usize /- [arrays::index_array_borrow]: Source: 'tests/src/arrays.rs', lines 161:0-161:46 -/ -def index_array_borrow (x : Array U32 2#usize) : Result U32 := - Array.index_usize U32 2#usize x 0#usize +def index_array_borrow (x : Array U32 2usize) : Result U32 := + Array.index_usize U32 2usize x 0usize /- [arrays::index_slice_u32_0]: Source: 'tests/src/arrays.rs', lines 165:0-165:42 -/ def index_slice_u32_0 (x : Slice U32) : Result U32 := - Slice.index_usize U32 x 0#usize + Slice.index_usize U32 x 0usize /- [arrays::index_mut_slice_u32_0]: Source: 'tests/src/arrays.rs', lines 169:0-169:50 -/ def index_mut_slice_u32_0 (x : Slice U32) : Result (U32 × (Slice U32)) := do - let i ← Slice.index_usize U32 x 0#usize + let i ← Slice.index_usize U32 x 0usize Result.ok (i, x) /- [arrays::index_all]: Source: 'tests/src/arrays.rs', lines 173:0-173:25 -/ def index_all : Result U32 := do - let i ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let i1 ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let i ← index_array (Array.make U32 2usize [ 0u32, 0u32 ]) + let i1 ← index_array (Array.make U32 2usize [ 0u32, 0u32 ]) let i2 ← i + i1 - let i3 ← index_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let i3 ← index_array_borrow (Array.make U32 2usize [ 0u32, 0u32 ]) let i4 ← i2 + i3 - let s ← - Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let s ← Array.to_slice U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) let i5 ← index_slice_u32_0 s let i6 ← i4 + i5 let (s1, to_slice_mut_back) ← - Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) let (i7, s2) ← index_mut_slice_u32_0 s1 let i8 ← i6 + i7 let _ ← to_slice_mut_back s2 @@ -275,35 +272,35 @@ def index_all : Result U32 := /- [arrays::update_array]: Source: 'tests/src/arrays.rs', lines 187:0-187:36 -/ -def update_array (x : Array U32 2#usize) : Result Unit := +def update_array (x : Array U32 2usize) : Result Unit := do - let (_, index_mut_back) ← Array.index_mut_usize U32 2#usize x 0#usize - let _ ← index_mut_back 1#u32 + let (_, index_mut_back) ← Array.index_mut_usize U32 2usize x 0usize + let _ ← index_mut_back 1u32 Result.ok () /- [arrays::update_array_mut_borrow]: Source: 'tests/src/arrays.rs', lines 190:0-190:48 -/ def update_array_mut_borrow - (x : Array U32 2#usize) : Result (Array U32 2#usize) := + (x : Array U32 2usize) : Result (Array U32 2usize) := do - let (_, index_mut_back) ← Array.index_mut_usize U32 2#usize x 0#usize - index_mut_back 1#u32 + let (_, index_mut_back) ← Array.index_mut_usize U32 2usize x 0usize + index_mut_back 1u32 /- [arrays::update_mut_slice]: Source: 'tests/src/arrays.rs', lines 193:0-193:38 -/ def update_mut_slice (x : Slice U32) : Result (Slice U32) := do - let (_, index_mut_back) ← Slice.index_mut_usize U32 x 0#usize - index_mut_back 1#u32 + let (_, index_mut_back) ← Slice.index_mut_usize U32 x 0usize + index_mut_back 1u32 /- [arrays::update_all]: Source: 'tests/src/arrays.rs', lines 197:0-197:19 -/ def update_all : Result Unit := do - let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let x ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) - let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2#usize x + let _ ← update_array (Array.make U32 2usize [ 0u32, 0u32 ]) + let _ ← update_array (Array.make U32 2usize [ 0u32, 0u32 ]) + let x ← update_array_mut_borrow (Array.make U32 2usize [ 0u32, 0u32 ]) + let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2usize x let s1 ← update_mut_slice s let _ ← to_slice_mut_back s1 Result.ok () @@ -313,37 +310,37 @@ def update_all : Result Unit := def range_all : Result Unit := do let (s, index_mut_back) ← - core.array.Array.index_mut U32 (core.ops.range.Range Usize) 4#usize + core.array.Array.index_mut U32 (core.ops.range.Range Usize) 4usize (core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize) (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) - (Array.make U32 4#usize [ 0#u32, 0#u32, 0#u32, 0#u32 ]) - { start := 1#usize, end_ := 3#usize } + (Array.make U32 4usize [ 0u32, 0u32, 0u32, 0u32 ]) + { start := 1usize, end_ := 3usize } let s1 ← update_mut_slice s let _ ← index_mut_back s1 Result.ok () /- [arrays::deref_array_borrow]: Source: 'tests/src/arrays.rs', lines 217:0-217:46 -/ -def deref_array_borrow (x : Array U32 2#usize) : Result U32 := - Array.index_usize U32 2#usize x 0#usize +def deref_array_borrow (x : Array U32 2usize) : Result U32 := + Array.index_usize U32 2usize x 0usize /- [arrays::deref_array_mut_borrow]: Source: 'tests/src/arrays.rs', lines 222:0-222:54 -/ def deref_array_mut_borrow - (x : Array U32 2#usize) : Result (U32 × (Array U32 2#usize)) := + (x : Array U32 2usize) : Result (U32 × (Array U32 2usize)) := do - let i ← Array.index_usize U32 2#usize x 0#usize + let i ← Array.index_usize U32 2usize x 0usize Result.ok (i, x) /- [arrays::take_array_t]: Source: 'tests/src/arrays.rs', lines 230:0-230:31 -/ -def take_array_t (a : Array AB 2#usize) : Result Unit := +def take_array_t (a : Array AB 2usize) : Result Unit := Result.ok () /- [arrays::non_copyable_array]: Source: 'tests/src/arrays.rs', lines 232:0-232:27 -/ def non_copyable_array : Result Unit := - take_array_t (Array.make AB 2#usize [ AB.A, AB.B ]) + take_array_t (Array.make AB 2usize [ AB.A, AB.B ]) /- [arrays::sum]: loop 0: Source: 'tests/src/arrays.rs', lines 245:0-253:1 -/ @@ -354,14 +351,14 @@ divergent def sum_loop (s : Slice U32) (sum1 : U32) (i : Usize) : Result U32 := do let i2 ← Slice.index_usize U32 s i let sum3 ← sum1 + i2 - let i3 ← i + 1#usize + let i3 ← i + 1usize sum_loop s sum3 i3 else Result.ok sum1 /- [arrays::sum]: Source: 'tests/src/arrays.rs', lines 245:0-245:28 -/ def sum (s : Slice U32) : Result U32 := - sum_loop s 0#u32 0#usize + sum_loop s 0u32 0usize /- [arrays::sum2]: loop 0: Source: 'tests/src/arrays.rs', lines 255:0-264:1 -/ @@ -375,7 +372,7 @@ divergent def sum2_loop let i3 ← Slice.index_usize U32 s2 i let i4 ← i2 + i3 let sum3 ← sum1 + i4 - let i5 ← i + 1#usize + let i5 ← i + 1usize sum2_loop s s2 sum3 i5 else Result.ok sum1 @@ -385,7 +382,7 @@ def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 := let i := Slice.len U32 s let i1 := Slice.len U32 s2 if i = i1 - then sum2_loop s s2 0#u32 0#usize + then sum2_loop s s2 0u32 0usize else Result.fail .panic /- [arrays::f0]: @@ -393,9 +390,9 @@ def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 := def f0 : Result Unit := do let (s, to_slice_mut_back) ← - Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) - let (_, index_mut_back) ← Slice.index_mut_usize U32 s 0#usize - let s1 ← index_mut_back 1#u32 + Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ]) + let (_, index_mut_back) ← Slice.index_mut_usize U32 s 0usize + let s1 ← index_mut_back 1u32 let _ ← to_slice_mut_back s1 Result.ok () @@ -404,9 +401,9 @@ def f0 : Result Unit := def f1 : Result Unit := do let (_, index_mut_back) ← - Array.index_mut_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) - 0#usize - let _ ← index_mut_back 1#u32 + Array.index_mut_usize U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ]) + 0usize + let _ ← index_mut_back 1u32 Result.ok () /- [arrays::f2]: @@ -416,8 +413,8 @@ def f2 (i : U32) : Result Unit := /- [arrays::f4]: Source: 'tests/src/arrays.rs', lines 285:0-285:54 -/ -def f4 (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) := - core.array.Array.index U32 (core.ops.range.Range Usize) 32#usize +def f4 (x : Array U32 32usize) (y : Usize) (z : Usize) : Result (Slice U32) := + core.array.Array.index U32 (core.ops.range.Range Usize) 32usize (core.ops.index.IndexSliceTIInst U32 (core.ops.range.Range Usize) (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x { start := y, end_ := z } @@ -427,34 +424,32 @@ def f4 (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) := def f3 : Result U32 := do let i ← - Array.index_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) - 0#usize + Array.index_usize U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ]) 0usize let _ ← f2 i - let b := Array.repeat U32 32#usize 0#u32 - let s ← - Array.to_slice U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) - let s1 ← f4 b 16#usize 18#usize + let b := Array.repeat U32 32usize 0u32 + let s ← Array.to_slice U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ]) + let s1 ← f4 b 16usize 18usize sum2 s s1 /- [arrays::SZ] Source: 'tests/src/arrays.rs', lines 289:0-289:19 -/ -def SZ_body : Result Usize := Result.ok 32#usize +def SZ_body : Result Usize := Result.ok 32usize def SZ : Usize := eval_global SZ_body /- [arrays::f5]: Source: 'tests/src/arrays.rs', lines 292:0-292:31 -/ -def f5 (x : Array U32 32#usize) : Result U32 := - Array.index_usize U32 32#usize x 0#usize +def f5 (x : Array U32 32usize) : Result U32 := + Array.index_usize U32 32usize x 0usize /- [arrays::ite]: Source: 'tests/src/arrays.rs', lines 297:0-297:12 -/ def ite : Result Unit := do let (s, to_slice_mut_back) ← - Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) let (_, s1) ← index_mut_slice_u32_0 s let (s2, to_slice_mut_back1) ← - Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) let (_, s3) ← index_mut_slice_u32_0 s2 let _ ← to_slice_mut_back1 s3 let _ ← to_slice_mut_back s1 @@ -468,8 +463,8 @@ divergent def zero_slice_loop then do let (_, index_mut_back) ← Slice.index_mut_usize U8 a i - let i1 ← i + 1#usize - let a1 ← index_mut_back 0#u8 + let i1 ← i + 1usize + let a1 ← index_mut_back 0u8 zero_slice_loop a1 i1 len else Result.ok a @@ -477,14 +472,14 @@ divergent def zero_slice_loop Source: 'tests/src/arrays.rs', lines 306:0-306:31 -/ def zero_slice (a : Slice U8) : Result (Slice U8) := let len := Slice.len U8 a - zero_slice_loop a 0#usize len + zero_slice_loop a 0usize len /- [arrays::iter_mut_slice]: loop 0: Source: 'tests/src/arrays.rs', lines 315:0-321:1 -/ divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit := if i < len then do - let i1 ← i + 1#usize + let i1 ← i + 1usize iter_mut_slice_loop len i1 else Result.ok () @@ -493,7 +488,7 @@ divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit := 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 + let _ ← iter_mut_slice_loop len 0usize Result.ok a /- [arrays::sum_mut_slice]: loop 0: @@ -506,7 +501,7 @@ divergent def sum_mut_slice_loop do let i2 ← Slice.index_usize U32 a i let s1 ← s + i2 - let i3 ← i + 1#usize + let i3 ← i + 1usize sum_mut_slice_loop a i3 s1 else Result.ok s @@ -514,7 +509,7 @@ divergent def sum_mut_slice_loop Source: 'tests/src/arrays.rs', lines 323:0-323:42 -/ def sum_mut_slice (a : Slice U32) : Result (U32 × (Slice U32)) := do - let i ← sum_mut_slice_loop a 0#usize 0#u32 + let i ← sum_mut_slice_loop a 0usize 0u32 Result.ok (i, a) end arrays diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean index 7d8b4714..74344e01 100644 --- a/tests/lean/Betree/Funs.lean +++ b/tests/lean/Betree/Funs.lean @@ -41,20 +41,20 @@ def betree.store_leaf_node Source: 'src/betree.rs', lines 55:0-55:48 -/ def betree.fresh_node_id (counter : U64) : Result (U64 × U64) := do - let counter1 ← counter + 1#u64 + let counter1 ← counter + 1u64 Result.ok (counter, counter1) /- [betree::betree::{betree::betree::NodeIdCounter}::new]: Source: 'src/betree.rs', lines 206:4-206:20 -/ def betree.NodeIdCounter.new : Result betree.NodeIdCounter := - Result.ok { next_node_id := 0#u64 } + Result.ok { next_node_id := 0u64 } /- [betree::betree::{betree::betree::NodeIdCounter}::fresh_id]: Source: 'src/betree.rs', lines 210:4-210:36 -/ def betree.NodeIdCounter.fresh_id (self : betree.NodeIdCounter) : Result (U64 × betree.NodeIdCounter) := do - let i ← self.next_node_id + 1#u64 + let i ← self.next_node_id + 1u64 Result.ok (self.next_node_id, { next_node_id := i }) /- [betree::betree::upsert_update]: @@ -65,7 +65,7 @@ def betree.upsert_update | none => match st with | betree.UpsertFunState.Add v => Result.ok v - | betree.UpsertFunState.Sub _ => Result.ok 0#u64 + | betree.UpsertFunState.Sub _ => Result.ok 0u64 | some prev1 => match st with | betree.UpsertFunState.Add v => @@ -77,7 +77,7 @@ def betree.upsert_update | betree.UpsertFunState.Sub v => if prev1 >= v then prev1 - v - else Result.ok 0#u64 + else Result.ok 0u64 /- [betree::betree::{betree::betree::List#1}::len]: loop 0: Source: 'src/betree.rs', lines 276:4-284:5 -/ @@ -86,14 +86,14 @@ divergent def betree.List.len_loop match self with | betree.List.Cons _ tl => do - let len1 ← len + 1#u64 + let len1 ← len + 1u64 betree.List.len_loop T tl len1 | betree.List.Nil => Result.ok len /- [betree::betree::{betree::betree::List#1}::len]: Source: 'src/betree.rs', lines 276:4-276:24 -/ def betree.List.len (T : Type) (self : betree.List T) : Result U64 := - betree.List.len_loop T self 0#u64 + betree.List.len_loop T self 0u64 /- [betree::betree::{betree::betree::List#1}::reverse]: loop 0: Source: 'src/betree.rs', lines 304:4-312:5 -/ @@ -118,12 +118,12 @@ divergent def betree.List.split_at_loop (T : Type) (n : U64) (beg : betree.List T) (self : betree.List T) : Result ((betree.List T) × (betree.List T)) := - if n > 0#u64 + if n > 0u64 then match self with | betree.List.Cons hd tl => do - let n1 ← n - 1#u64 + let n1 ← n - 1u64 betree.List.split_at_loop T n1 (betree.List.Cons hd beg) tl | betree.List.Nil => Result.fail .panic else do @@ -706,7 +706,7 @@ divergent def betree.Node.apply_messages let (st1, content) ← betree.load_leaf_node node.id st let content1 ← betree.Node.apply_messages_to_leaf content msgs let len ← betree.List.len (U64 × U64) content1 - let i ← 2#u64 * params.split_size + let i ← 2u64 * params.split_size if len >= i then do @@ -751,7 +751,7 @@ def betree.BeTree.new { params := { min_flush_size := min_flush_size, split_size := split_size }, node_id_cnt := node_id_cnt1, - root := (betree.Node.Leaf { id := id, size := 0#u64 }) + root := (betree.Node.Leaf { id := id, size := 0u64 }) }) /- [betree::betree::{betree::betree::BeTree#6}::apply]: diff --git a/tests/lean/Bitwise.lean b/tests/lean/Bitwise.lean index 23ec66b4..8884d309 100644 --- a/tests/lean/Bitwise.lean +++ b/tests/lean/Bitwise.lean @@ -9,15 +9,15 @@ namespace bitwise Source: 'tests/src/bitwise.rs', lines 5:0-5:31 -/ def shift_u32 (a : U32) : Result U32 := do - let t ← a >>> 16#usize - t <<< 16#usize + let t ← a >>> 16usize + t <<< 16usize /- [bitwise::shift_i32]: Source: 'tests/src/bitwise.rs', lines 12:0-12:31 -/ def shift_i32 (a : I32) : Result I32 := do - let t ← a >>> 16#isize - t <<< 16#isize + let t ← a >>> 16isize + t <<< 16isize /- [bitwise::xor_u32]: Source: 'tests/src/bitwise.rs', lines 19:0-19:37 -/ diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean index ecb91c16..a72ac98d 100644 --- a/tests/lean/Constants.lean +++ b/tests/lean/Constants.lean @@ -7,7 +7,7 @@ namespace constants /- [constants::X0] Source: 'tests/src/constants.rs', lines 8:0-8:17 -/ -def X0_body : Result U32 := Result.ok 0#u32 +def X0_body : Result U32 := Result.ok 0u32 def X0 : U32 := eval_global X0_body /- [constants::X1] @@ -17,17 +17,17 @@ def X1 : U32 := eval_global X1_body /- [constants::X2] Source: 'tests/src/constants.rs', lines 13:0-13:17 -/ -def X2_body : Result U32 := Result.ok 3#u32 +def X2_body : Result U32 := Result.ok 3u32 def X2 : U32 := eval_global X2_body /- [constants::incr]: Source: 'tests/src/constants.rs', lines 20:0-20:32 -/ def incr (n : U32) : Result U32 := - n + 1#u32 + n + 1u32 /- [constants::X3] Source: 'tests/src/constants.rs', lines 18:0-18:17 -/ -def X3_body : Result U32 := incr 32#u32 +def X3_body : Result U32 := incr 32u32 def X3 : U32 := eval_global X3_body /- [constants::mk_pair0]: @@ -48,22 +48,22 @@ def mk_pair1 (x : U32) (y : U32) : Result (Pair U32 U32) := /- [constants::P0] Source: 'tests/src/constants.rs', lines 34:0-34:24 -/ -def P0_body : Result (U32 × U32) := mk_pair0 0#u32 1#u32 +def P0_body : Result (U32 × U32) := mk_pair0 0u32 1u32 def P0 : (U32 × U32) := eval_global P0_body /- [constants::P1] Source: 'tests/src/constants.rs', lines 35:0-35:28 -/ -def P1_body : Result (Pair U32 U32) := mk_pair1 0#u32 1#u32 +def P1_body : Result (Pair U32 U32) := mk_pair1 0u32 1u32 def P1 : Pair U32 U32 := eval_global P1_body /- [constants::P2] Source: 'tests/src/constants.rs', lines 36:0-36:24 -/ -def P2_body : Result (U32 × U32) := Result.ok (0#u32, 1#u32) +def P2_body : Result (U32 × U32) := Result.ok (0u32, 1u32) def P2 : (U32 × U32) := eval_global P2_body /- [constants::P3] Source: 'tests/src/constants.rs', lines 37:0-37:28 -/ -def P3_body : Result (Pair U32 U32) := Result.ok { x := 0#u32, y := 1#u32 } +def P3_body : Result (Pair U32 U32) := Result.ok { x := 0u32, y := 1u32 } def P3 : Pair U32 U32 := eval_global P3_body /- [constants::Wrap] @@ -78,7 +78,7 @@ def Wrap.new (T : Type) (value : T) : Result (Wrap T) := /- [constants::Y] Source: 'tests/src/constants.rs', lines 44:0-44:22 -/ -def Y_body : Result (Wrap I32) := Wrap.new I32 2#i32 +def Y_body : Result (Wrap I32) := Wrap.new I32 2i32 def Y : Wrap I32 := eval_global Y_body /- [constants::unwrap_y]: @@ -93,7 +93,7 @@ def YVAL : I32 := eval_global YVAL_body /- [constants::get_z1::Z1] Source: 'tests/src/constants.rs', lines 65:4-65:17 -/ -def get_z1.Z1_body : Result I32 := Result.ok 3#i32 +def get_z1.Z1_body : Result I32 := Result.ok 3i32 def get_z1.Z1 : I32 := eval_global get_z1.Z1_body /- [constants::get_z1]: @@ -108,7 +108,7 @@ def add (a : I32) (b : I32) : Result I32 := /- [constants::Q1] Source: 'tests/src/constants.rs', lines 77:0-77:17 -/ -def Q1_body : Result I32 := Result.ok 5#i32 +def Q1_body : Result I32 := Result.ok 5i32 def Q1 : I32 := eval_global Q1_body /- [constants::Q2] @@ -118,7 +118,7 @@ def Q2 : I32 := eval_global Q2_body /- [constants::Q3] Source: 'tests/src/constants.rs', lines 79:0-79:17 -/ -def Q3_body : Result I32 := add Q2 3#i32 +def Q3_body : Result I32 := add Q2 3i32 def Q3 : I32 := eval_global Q3_body /- [constants::get_z2]: @@ -131,7 +131,7 @@ def get_z2 : Result I32 := /- [constants::S1] Source: 'tests/src/constants.rs', lines 83:0-83:18 -/ -def S1_body : Result U32 := Result.ok 6#u32 +def S1_body : Result U32 := Result.ok 6u32 def S1 : U32 := eval_global S1_body /- [constants::S2] @@ -146,7 +146,7 @@ def S3 : Pair U32 U32 := eval_global S3_body /- [constants::S4] Source: 'tests/src/constants.rs', lines 86:0-86:29 -/ -def S4_body : Result (Pair U32 U32) := mk_pair1 7#u32 8#u32 +def S4_body : Result (Pair U32 U32) := mk_pair1 7u32 8u32 def S4 : Pair U32 U32 := eval_global S4_body /- [constants::V] diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean index 48ac2062..9d8b085c 100644 --- a/tests/lean/Demo/Demo.lean +++ b/tests/lean/Demo/Demo.lean @@ -22,7 +22,7 @@ def choose def mul2_add1 (x : U32) : Result U32 := do let i ← x + x - i + 1#u32 + i + 1u32 /- [demo::use_mul2_add1]: Source: 'tests/src/demo.rs', lines 19:0-19:43 -/ @@ -34,13 +34,13 @@ def use_mul2_add1 (x : U32) (y : U32) : Result U32 := /- [demo::incr]: Source: 'tests/src/demo.rs', lines 23:0-23:31 -/ def incr (x : U32) : Result U32 := - x + 1#u32 + x + 1u32 /- [demo::use_incr]: Source: 'tests/src/demo.rs', lines 27:0-27:17 -/ def use_incr : Result Unit := do - let x ← incr 0#u32 + let x ← incr 0u32 let x1 ← incr x let _ ← incr x1 Result.ok () @@ -56,10 +56,10 @@ inductive CList (T : Type) := divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T := match l with | CList.CCons x tl => - if i = 0#u32 + if i = 0u32 then Result.ok x else do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 list_nth T tl i1 | CList.CNil => Result.fail .panic @@ -71,13 +71,13 @@ divergent def list_nth_mut := match l with | CList.CCons x tl => - if i = 0#u32 + if i = 0u32 then let back := fun ret => Result.ok (CList.CCons ret tl) Result.ok (x, back) else do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 let (t, list_nth_mut_back) ← list_nth_mut T tl i1 let back := fun ret => @@ -95,13 +95,13 @@ divergent def list_nth_mut1_loop := match l with | CList.CCons x tl => - if i = 0#u32 + if i = 0u32 then let back := fun ret => Result.ok (CList.CCons ret tl) Result.ok (x, back) else do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 let (t, back) ← list_nth_mut1_loop T tl i1 let back1 := fun ret => do @@ -121,12 +121,12 @@ def list_nth_mut1 /- [demo::i32_id]: Source: 'tests/src/demo.rs', lines 82:0-82:28 -/ divergent def i32_id (i : I32) : Result I32 := - if i = 0#i32 - then Result.ok 0#i32 + if i = 0i32 + then Result.ok 0i32 else do - let i1 ← i - 1#i32 + let i1 ← i - 1i32 let i2 ← i32_id i1 - i2 + 1#i32 + i2 + 1i32 /- [demo::list_tail]: Source: 'tests/src/demo.rs', lines 90:0-90:64 -/ @@ -155,7 +155,7 @@ structure Counter (Self : Type) where Source: 'tests/src/demo.rs', lines 104:4-104:31 -/ def CounterUsize.incr (self : Usize) : Result (Usize × Usize) := do - let self1 ← self + 1#usize + let self1 ← self + 1usize Result.ok (self, self1) /- Trait implementation: [demo::{(demo::Counter for usize)}] diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean index 1b1d5cdf..c828720a 100644 --- a/tests/lean/External/Funs.lean +++ b/tests/lean/External/Funs.lean @@ -27,7 +27,7 @@ def incr := do let (st1, (i, get_mut_back)) ← core.cell.Cell.get_mut U32 rc st - let i1 ← i + 1#u32 + let i1 ← i + 1u32 let (_, rc1) ← get_mut_back i1 st1 Result.ok (st1, rc1) diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index 612e1848..3c244ee0 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -18,11 +18,11 @@ divergent def HashMap.allocate_slots_loop (T : Type) (slots : alloc.vec.Vec (List T)) (n : Usize) : Result (alloc.vec.Vec (List T)) := - if n > 0#usize + if n > 0usize then do let slots1 ← alloc.vec.Vec.push (List T) slots List.Nil - let n1 ← n - 1#usize + let n1 ← n - 1usize HashMap.allocate_slots_loop T slots1 n1 else Result.ok slots @@ -47,7 +47,7 @@ def HashMap.new_with_capacity let i1 ← i / max_load_divisor Result.ok { - num_entries := 0#usize, + num_entries := 0usize, max_load_factor := (max_load_dividend, max_load_divisor), max_load := i1, slots := slots @@ -56,7 +56,7 @@ def HashMap.new_with_capacity /- [hashmap::{hashmap::HashMap}::new]: Source: 'tests/src/hashmap.rs', lines 85:4-85:24 -/ def HashMap.new (T : Type) : Result (HashMap T) := - HashMap.new_with_capacity T 32#usize 4#usize 5#usize + HashMap.new_with_capacity T 32usize 4usize 5usize /- [hashmap::{hashmap::HashMap}::clear]: loop 0: Source: 'tests/src/hashmap.rs', lines 90:4-98:5 -/ @@ -71,7 +71,7 @@ divergent def HashMap.clear_loop let (_, index_mut_back) ← alloc.vec.Vec.index_mut (List T) Usize (core.slice.index.SliceIndexUsizeSliceTInst (List T)) slots i - let i2 ← i + 1#usize + let i2 ← i + 1usize let slots1 ← index_mut_back List.Nil HashMap.clear_loop T slots1 i2 else Result.ok slots @@ -80,8 +80,8 @@ divergent def HashMap.clear_loop Source: 'tests/src/hashmap.rs', lines 90:4-90:27 -/ def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) := do - let hm ← HashMap.clear_loop T self.slots 0#usize - Result.ok { self with num_entries := 0#usize, slots := hm } + let hm ← HashMap.clear_loop T self.slots 0usize + Result.ok { self with num_entries := 0usize, slots := hm } /- [hashmap::{hashmap::HashMap}::len]: Source: 'tests/src/hashmap.rs', lines 100:4-100:30 -/ @@ -129,7 +129,7 @@ def HashMap.insert_no_resize if inserted then do - let i1 ← self.num_entries + 1#usize + let i1 ← self.num_entries + 1usize let v ← index_mut_back l1 Result.ok { self with num_entries := i1, slots := v } else do @@ -169,7 +169,7 @@ divergent def HashMap.move_elements_loop (core.slice.index.SliceIndexUsizeSliceTInst (List T)) slots i let (ls, l1) := core.mem.replace (List T) l List.Nil let ntable1 ← HashMap.move_elements_from_list T ntable ls - let i2 ← i + 1#usize + let i2 ← i + 1usize let slots1 ← index_mut_back l1 HashMap.move_elements_loop T ntable1 slots1 i2 else Result.ok (ntable, slots) @@ -189,15 +189,15 @@ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) := do let max_usize ← Scalar.cast .Usize core_u32_max let capacity := alloc.vec.Vec.len (List T) self.slots - let n1 ← max_usize / 2#usize + let n1 ← max_usize / 2usize let (i, i1) := self.max_load_factor let i2 ← n1 / i if capacity <= i2 then do - let i3 ← capacity * 2#usize + let i3 ← capacity * 2usize let ntable ← HashMap.new_with_capacity T i3 i i1 - let p ← HashMap.move_elements T ntable self.slots 0#usize + let p ← HashMap.move_elements T ntable self.slots 0usize let (ntable1, _) := p Result.ok { @@ -377,7 +377,7 @@ def HashMap.remove Result.ok (none, { self with slots := v }) | some x1 => do - let i1 ← self.num_entries - 1#usize + let i1 ← self.num_entries - 1usize let v ← index_mut_back l1 Result.ok (some x1, { self with num_entries := i1, slots := v }) @@ -395,37 +395,37 @@ def insert_on_disk def test1 : Result Unit := do let hm ← HashMap.new U64 - let hm1 ← HashMap.insert U64 hm 0#usize 42#u64 - let hm2 ← HashMap.insert U64 hm1 128#usize 18#u64 - let hm3 ← HashMap.insert U64 hm2 1024#usize 138#u64 - let hm4 ← HashMap.insert U64 hm3 1056#usize 256#u64 - let i ← HashMap.get U64 hm4 128#usize - if i = 18#u64 + let hm1 ← HashMap.insert U64 hm 0usize 42u64 + let hm2 ← HashMap.insert U64 hm1 128usize 18u64 + let hm3 ← HashMap.insert U64 hm2 1024usize 138u64 + let hm4 ← HashMap.insert U64 hm3 1056usize 256u64 + let i ← HashMap.get U64 hm4 128usize + if i = 18u64 then do - let (_, get_mut_back) ← HashMap.get_mut U64 hm4 1024#usize - let hm5 ← get_mut_back 56#u64 - let i1 ← HashMap.get U64 hm5 1024#usize - if i1 = 56#u64 + let (_, get_mut_back) ← HashMap.get_mut U64 hm4 1024usize + let hm5 ← get_mut_back 56u64 + let i1 ← HashMap.get U64 hm5 1024usize + if i1 = 56u64 then do - let (x, hm6) ← HashMap.remove U64 hm5 1024#usize + let (x, hm6) ← HashMap.remove U64 hm5 1024usize match x with | none => Result.fail .panic | some x1 => - if x1 = 56#u64 + if x1 = 56u64 then do - let i2 ← HashMap.get U64 hm6 0#usize - if i2 = 42#u64 + let i2 ← HashMap.get U64 hm6 0usize + if i2 = 42u64 then do - let i3 ← HashMap.get U64 hm6 128#usize - if i3 = 18#u64 + let i3 ← HashMap.get U64 hm6 128usize + if i3 = 18u64 then do - let i4 ← HashMap.get U64 hm6 1056#usize - if i4 = 256#u64 + let i4 ← HashMap.get U64 hm6 1056usize + if i4 = 256u64 then Result.ok () else Result.fail .panic else Result.fail .panic diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean index 199605d5..567d2b44 100644 --- a/tests/lean/Loops.lean +++ b/tests/lean/Loops.lean @@ -11,14 +11,14 @@ divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 := if i < max then do let s1 ← s + i - let i1 ← i + 1#u32 + let i1 ← i + 1u32 sum_loop max i1 s1 - else s * 2#u32 + else s * 2u32 /- [loops::sum]: Source: 'tests/src/loops.rs', lines 8:0-8:27 -/ def sum (max : U32) : Result U32 := - sum_loop max 0#u32 0#u32 + sum_loop max 0u32 0u32 /- [loops::sum_with_mut_borrows]: loop 0: Source: 'tests/src/loops.rs', lines 23:0-35:1 -/ @@ -28,14 +28,14 @@ divergent def sum_with_mut_borrows_loop then do let ms ← s + i - let mi ← i + 1#u32 + let mi ← i + 1u32 sum_with_mut_borrows_loop max mi ms - else s * 2#u32 + else s * 2u32 /- [loops::sum_with_mut_borrows]: Source: 'tests/src/loops.rs', lines 23:0-23:44 -/ def sum_with_mut_borrows (max : U32) : Result U32 := - sum_with_mut_borrows_loop max 0#u32 0#u32 + sum_with_mut_borrows_loop max 0u32 0u32 /- [loops::sum_with_shared_borrows]: loop 0: Source: 'tests/src/loops.rs', lines 38:0-52:1 -/ @@ -44,15 +44,15 @@ divergent def sum_with_shared_borrows_loop if i < max then do - let i1 ← i + 1#u32 + let i1 ← i + 1u32 let s1 ← s + i1 sum_with_shared_borrows_loop max i1 s1 - else s * 2#u32 + else s * 2u32 /- [loops::sum_with_shared_borrows]: Source: 'tests/src/loops.rs', lines 38:0-38:47 -/ def sum_with_shared_borrows (max : U32) : Result U32 := - sum_with_shared_borrows_loop max 0#u32 0#u32 + sum_with_shared_borrows_loop max 0u32 0u32 /- [loops::sum_array]: loop 0: Source: 'tests/src/loops.rs', lines 54:0-62:1 -/ @@ -63,14 +63,14 @@ divergent def sum_array_loop do let i1 ← Array.index_usize U32 N a i let s1 ← s + i1 - let i2 ← i + 1#usize + let i2 ← i + 1usize sum_array_loop N a i2 s1 else Result.ok s /- [loops::sum_array]: Source: 'tests/src/loops.rs', lines 54:0-54:52 -/ def sum_array (N : Usize) (a : Array U32 N) : Result U32 := - sum_array_loop N a 0#usize 0#u32 + sum_array_loop N a 0usize 0u32 /- [loops::clear]: loop 0: Source: 'tests/src/loops.rs', lines 66:0-72:1 -/ @@ -83,15 +83,15 @@ divergent def clear_loop let (_, index_mut_back) ← alloc.vec.Vec.index_mut U32 Usize (core.slice.index.SliceIndexUsizeSliceTInst U32) v i - let i2 ← i + 1#usize - let v1 ← index_mut_back 0#u32 + let i2 ← i + 1usize + let v1 ← index_mut_back 0u32 clear_loop v1 i2 else Result.ok v /- [loops::clear]: Source: 'tests/src/loops.rs', lines 66:0-66:30 -/ def clear (v : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) := - clear_loop v 0#usize + clear_loop v 0usize /- [loops::List] Source: 'tests/src/loops.rs', lines 74:0-74:16 -/ @@ -119,13 +119,13 @@ divergent def list_nth_mut_loop_loop (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) := match ls with | List.Cons x tl => - if i = 0#u32 + if i = 0u32 then let back := fun ret => Result.ok (List.Cons ret tl) Result.ok (x, back) else do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 let (t, back) ← list_nth_mut_loop_loop T tl i1 let back1 := fun ret => do @@ -146,10 +146,10 @@ divergent def list_nth_shared_loop_loop (T : Type) (ls : List T) (i : U32) : Result T := match ls with | List.Cons x tl => - if i = 0#u32 + if i = 0u32 then Result.ok x else do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 list_nth_shared_loop_loop T tl i1 | List.Nil => Result.fail .panic @@ -189,7 +189,7 @@ def get_elem_mut do let (ls, index_mut_back) ← alloc.vec.Vec.index_mut (List Usize) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize + (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0usize let (i, back) ← get_elem_mut_loop x ls let back1 := fun ret => do let l ← back ret @@ -213,7 +213,7 @@ def get_elem_shared do let ls ← alloc.vec.Vec.index (List Usize) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize + (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0usize get_elem_shared_loop x ls /- [loops::id_mut]: @@ -235,13 +235,13 @@ divergent def list_nth_mut_loop_with_id_loop (T : Type) (i : U32) (ls : List T) : Result (T × (T → Result (List T))) := match ls with | List.Cons x tl => - if i = 0#u32 + if i = 0u32 then let back := fun ret => Result.ok (List.Cons ret tl) Result.ok (x, back) else do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 let (t, back) ← list_nth_mut_loop_with_id_loop T i1 tl let back1 := fun ret => do @@ -268,10 +268,10 @@ divergent def list_nth_shared_loop_with_id_loop (T : Type) (i : U32) (ls : List T) : Result T := match ls with | List.Cons x tl => - if i = 0#u32 + if i = 0u32 then Result.ok x else do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 list_nth_shared_loop_with_id_loop T i1 tl | List.Nil => Result.fail .panic @@ -293,14 +293,14 @@ divergent def list_nth_mut_loop_pair_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = 0#u32 + if i = 0u32 then 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 + let i1 ← i - 1u32 let (p, back'a, back'b) ← list_nth_mut_loop_pair_loop T tl0 tl1 i1 let back'a1 := fun ret => do @@ -330,10 +330,10 @@ divergent def list_nth_shared_loop_pair_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = 0#u32 + if i = 0u32 then Result.ok (x0, x1) else do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 list_nth_shared_loop_pair_loop T tl0 tl1 i1 | List.Nil => Result.fail .panic | List.Nil => Result.fail .panic @@ -354,7 +354,7 @@ divergent def list_nth_mut_loop_pair_merge_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = 0#u32 + if i = 0u32 then let back := fun ret => @@ -363,7 +363,7 @@ divergent def list_nth_mut_loop_pair_merge_loop Result.ok ((x0, x1), back) else do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 let (p, back) ← list_nth_mut_loop_pair_merge_loop T tl0 tl1 i1 let back1 := fun ret => @@ -390,11 +390,11 @@ divergent def list_nth_shared_loop_pair_merge_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = 0#u32 + if i = 0u32 then Result.ok (x0, x1) else do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 list_nth_shared_loop_pair_merge_loop T tl0 tl1 i1 | List.Nil => Result.fail .panic | List.Nil => Result.fail .panic @@ -415,13 +415,13 @@ divergent def list_nth_mut_shared_loop_pair_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = 0#u32 + if i = 0u32 then let back := fun ret => Result.ok (List.Cons ret tl0) Result.ok ((x0, x1), back) else do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 let (p, back) ← list_nth_mut_shared_loop_pair_loop T tl0 tl1 i1 let back1 := fun ret => do @@ -449,13 +449,13 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = 0#u32 + if i = 0u32 then let back := fun ret => Result.ok (List.Cons ret tl0) Result.ok ((x0, x1), back) else do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 let (p, back) ← list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i1 let back1 := fun ret => do @@ -483,13 +483,13 @@ divergent def list_nth_shared_mut_loop_pair_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = 0#u32 + if i = 0u32 then let back := fun ret => Result.ok (List.Cons ret tl1) Result.ok ((x0, x1), back) else do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 let (p, back) ← list_nth_shared_mut_loop_pair_loop T tl0 tl1 i1 let back1 := fun ret => do @@ -517,13 +517,13 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = 0#u32 + if i = 0u32 then let back := fun ret => Result.ok (List.Cons ret tl1) Result.ok ((x0, x1), back) else do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 let (p, back) ← list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i1 let back1 := fun ret => do @@ -544,9 +544,9 @@ def list_nth_shared_mut_loop_pair_merge /- [loops::ignore_input_mut_borrow]: loop 0: Source: 'tests/src/loops.rs', lines 349:0-353:1 -/ divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit := - if i > 0#u32 + if i > 0u32 then do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 ignore_input_mut_borrow_loop i1 else Result.ok () @@ -560,9 +560,9 @@ def ignore_input_mut_borrow (_a : U32) (i : U32) : Result U32 := /- [loops::incr_ignore_input_mut_borrow]: loop 0: Source: 'tests/src/loops.rs', lines 357:0-362:1 -/ divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit := - if i > 0#u32 + if i > 0u32 then do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 incr_ignore_input_mut_borrow_loop i1 else Result.ok () @@ -570,16 +570,16 @@ divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit := Source: 'tests/src/loops.rs', lines 357:0-357:60 -/ def incr_ignore_input_mut_borrow (a : U32) (i : U32) : Result U32 := do - let a1 ← a + 1#u32 + let a1 ← a + 1u32 let _ ← incr_ignore_input_mut_borrow_loop i Result.ok a1 /- [loops::ignore_input_shared_borrow]: loop 0: Source: 'tests/src/loops.rs', lines 366:0-370:1 -/ divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit := - if i > 0#u32 + if i > 0u32 then do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 ignore_input_shared_borrow_loop i1 else Result.ok () diff --git a/tests/lean/Matches.lean b/tests/lean/Matches.lean index 3e3a558b..34f899b1 100644 --- a/tests/lean/Matches.lean +++ b/tests/lean/Matches.lean @@ -9,8 +9,8 @@ namespace matches Source: 'tests/src/matches.rs', lines 4:0-4:27 -/ def match_u32 (x : U32) : Result U32 := match x with - | 0#u32 => Result.ok 0#u32 - | 1#u32 => Result.ok 1#u32 - | _ => Result.ok 2#u32 + | 0u32 => Result.ok 0u32 + | 1u32 => Result.ok 1u32 + | _ => Result.ok 2u32 end matches diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean index f0438050..01f6736c 100644 --- a/tests/lean/NoNestedBorrows.lean +++ b/tests/lean/NoNestedBorrows.lean @@ -62,7 +62,7 @@ def cast_bool_to_bool (x : Bool) : Result Bool := Source: 'tests/src/no_nested_borrows.rs', lines 63:0-63:14 -/ def test2 : Result Unit := do - let _ ← 23#u32 + 44#u32 + let _ ← 23u32 + 44u32 Result.ok () /- Unit test for [no_nested_borrows::test2] -/ @@ -79,10 +79,10 @@ def get_max (x : U32) (y : U32) : Result U32 := Source: 'tests/src/no_nested_borrows.rs', lines 83:0-83:14 -/ def test3 : Result Unit := do - let x ← get_max 4#u32 3#u32 - let y ← get_max 10#u32 11#u32 + let x ← get_max 4u32 3u32 + let y ← get_max 10u32 11u32 let z ← x + y - if z = 15#u32 + if z = 15u32 then Result.ok () else Result.fail .panic @@ -93,8 +93,8 @@ def test3 : Result Unit := Source: 'tests/src/no_nested_borrows.rs', lines 90:0-90:18 -/ def test_neg1 : Result Unit := do - let y ← -. 3#i32 - if y = (-3)#i32 + let y ← -. 3i32 + if y = (-3)i32 then Result.ok () else Result.fail .panic @@ -104,7 +104,7 @@ def test_neg1 : Result Unit := /- [no_nested_borrows::refs_test1]: Source: 'tests/src/no_nested_borrows.rs', lines 97:0-97:19 -/ def refs_test1 : Result Unit := - if 1#i32 = 1#i32 + if 1i32 = 1i32 then Result.ok () else Result.fail .panic @@ -114,12 +114,12 @@ def refs_test1 : Result Unit := /- [no_nested_borrows::refs_test2]: Source: 'tests/src/no_nested_borrows.rs', lines 108:0-108:19 -/ def refs_test2 : Result Unit := - if 2#i32 = 2#i32 + if 2i32 = 2i32 then - if 0#i32 = 0#i32 + if 0i32 = 0i32 then - if 2#i32 = 2#i32 - then if 2#i32 = 2#i32 + if 2i32 = 2i32 + then if 2i32 = 2i32 then Result.ok () else Result.fail .panic else Result.fail .panic @@ -141,10 +141,10 @@ def test_list1 : Result Unit := Source: 'tests/src/no_nested_borrows.rs', lines 129:0-129:18 -/ def test_box1 : Result Unit := do - let (_, deref_mut_back) ← alloc.boxed.Box.deref_mut I32 0#i32 - let b ← deref_mut_back 1#i32 + let (_, deref_mut_back) ← alloc.boxed.Box.deref_mut I32 0i32 + let b ← deref_mut_back 1i32 let x ← alloc.boxed.Box.deref I32 b - if x = 1#i32 + if x = 1i32 then Result.ok () else Result.fail .panic @@ -174,8 +174,8 @@ def test_panic (b : Bool) : Result Unit := Source: 'tests/src/no_nested_borrows.rs', lines 160:0-160:22 -/ def test_copy_int : Result Unit := do - let y ← copy_int 0#i32 - if 0#i32 = y + let y ← copy_int 0i32 + if 0i32 = y then Result.ok () else Result.fail .panic @@ -193,7 +193,7 @@ def is_cons (T : Type) (l : List T) : Result Bool := Source: 'tests/src/no_nested_borrows.rs', lines 174:0-174:21 -/ def test_is_cons : Result Unit := do - let b ← is_cons I32 (List.Cons 0#i32 List.Nil) + let b ← is_cons I32 (List.Cons 0i32 List.Nil) if b then Result.ok () else Result.fail .panic @@ -212,9 +212,9 @@ def split_list (T : Type) (l : List T) : Result (T × (List T)) := Source: 'tests/src/no_nested_borrows.rs', lines 188:0-188:24 -/ def test_split_list : Result Unit := do - let p ← split_list I32 (List.Cons 0#i32 List.Nil) + let p ← split_list I32 (List.Cons 0i32 List.Nil) let (hd, _) := p - if hd = 0#i32 + if hd = 0i32 then Result.ok () else Result.fail .panic @@ -237,14 +237,14 @@ def choose Source: 'tests/src/no_nested_borrows.rs', lines 203:0-203:20 -/ def choose_test : Result Unit := do - let (z, choose_back) ← choose I32 true 0#i32 0#i32 - let z1 ← z + 1#i32 - if z1 = 1#i32 + let (z, choose_back) ← choose I32 true 0i32 0i32 + let z1 ← z + 1i32 + if z1 = 1i32 then do let (x, y) ← choose_back z1 - if x = 1#i32 - then if y = 0#i32 + if x = 1i32 + then if y = 0i32 then Result.ok () else Result.fail .panic else Result.fail .panic @@ -285,18 +285,18 @@ divergent def list_length (T : Type) (l : List T) : Result U32 := match l with | List.Cons _ l1 => do let i ← list_length T l1 - 1#u32 + i - | List.Nil => Result.ok 0#u32 + 1u32 + i + | List.Nil => Result.ok 0u32 /- [no_nested_borrows::list_nth_shared]: Source: 'tests/src/no_nested_borrows.rs', lines 273:0-273:62 -/ 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 + if i = 0u32 then Result.ok x else do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 list_nth_shared T tl i1 | List.Nil => Result.fail .panic @@ -306,13 +306,13 @@ divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result (T × (T → Result (List T))) := match l with | List.Cons x tl => - if i = 0#u32 + if i = 0u32 then let back := fun ret => Result.ok (List.Cons ret tl) Result.ok (x, back) else do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 let (t, list_nth_mut_back) ← list_nth_mut T tl i1 let back := fun ret => @@ -340,37 +340,37 @@ def list_rev (T : Type) (l : List T) : Result (List T) := Source: 'tests/src/no_nested_borrows.rs', lines 324:0-324:28 -/ def test_list_functions : Result Unit := do - let l := List.Cons 2#i32 List.Nil - let l1 := List.Cons 1#i32 l - let i ← list_length I32 (List.Cons 0#i32 l1) - if i = 3#u32 + let l := List.Cons 2i32 List.Nil + let l1 := List.Cons 1i32 l + let i ← list_length I32 (List.Cons 0i32 l1) + if i = 3u32 then do - let i1 ← list_nth_shared I32 (List.Cons 0#i32 l1) 0#u32 - if i1 = 0#i32 + let i1 ← list_nth_shared I32 (List.Cons 0i32 l1) 0u32 + if i1 = 0i32 then do - let i2 ← list_nth_shared I32 (List.Cons 0#i32 l1) 1#u32 - if i2 = 1#i32 + let i2 ← list_nth_shared I32 (List.Cons 0i32 l1) 1u32 + if i2 = 1i32 then do - let i3 ← list_nth_shared I32 (List.Cons 0#i32 l1) 2#u32 - if i3 = 2#i32 + let i3 ← list_nth_shared I32 (List.Cons 0i32 l1) 2u32 + if i3 = 2i32 then do let (_, list_nth_mut_back) ← - list_nth_mut I32 (List.Cons 0#i32 l1) 1#u32 - let ls ← list_nth_mut_back 3#i32 - let i4 ← list_nth_shared I32 ls 0#u32 - if i4 = 0#i32 + list_nth_mut I32 (List.Cons 0i32 l1) 1u32 + let ls ← list_nth_mut_back 3i32 + let i4 ← list_nth_shared I32 ls 0u32 + if i4 = 0i32 then do - let i5 ← list_nth_shared I32 ls 1#u32 - if i5 = 3#i32 + let i5 ← list_nth_shared I32 ls 1u32 + if i5 = 3i32 then do - let i6 ← list_nth_shared I32 ls 2#u32 - if i6 = 2#i32 + let i6 ← list_nth_shared I32 ls 2u32 + if i6 = 2i32 then Result.ok () else Result.fail .panic else Result.fail .panic @@ -425,17 +425,17 @@ structure StructWithTuple (T1 T2 : Type) where /- [no_nested_borrows::new_tuple1]: Source: 'tests/src/no_nested_borrows.rs', lines 363:0-363:48 -/ def new_tuple1 : Result (StructWithTuple U32 U32) := - Result.ok { p := (1#u32, 2#u32) } + Result.ok { p := (1u32, 2u32) } /- [no_nested_borrows::new_tuple2]: Source: 'tests/src/no_nested_borrows.rs', lines 367:0-367:48 -/ def new_tuple2 : Result (StructWithTuple I16 I16) := - Result.ok { p := (1#i16, 2#i16) } + Result.ok { p := (1i16, 2i16) } /- [no_nested_borrows::new_tuple3]: Source: 'tests/src/no_nested_borrows.rs', lines 371:0-371:48 -/ def new_tuple3 : Result (StructWithTuple U64 I64) := - Result.ok { p := (1#u64, 2#i64) } + Result.ok { p := (1u64, 2i64) } /- [no_nested_borrows::StructWithPair] Source: 'tests/src/no_nested_borrows.rs', lines 376:0-376:33 -/ @@ -445,7 +445,7 @@ structure StructWithPair (T1 T2 : Type) where /- [no_nested_borrows::new_pair1]: Source: 'tests/src/no_nested_borrows.rs', lines 380:0-380:46 -/ def new_pair1 : Result (StructWithPair U32 U32) := - Result.ok { p := { x := 1#u32, y := 2#u32 } } + Result.ok { p := { x := 1u32, y := 2u32 } } /- [no_nested_borrows::test_constants]: Source: 'tests/src/no_nested_borrows.rs', lines 388:0-388:23 -/ @@ -453,21 +453,21 @@ def test_constants : Result Unit := do let swt ← new_tuple1 let (i, _) := swt.p - if i = 1#u32 + if i = 1u32 then do let swt1 ← new_tuple2 let (i1, _) := swt1.p - if i1 = 1#i16 + if i1 = 1i16 then do let swt2 ← new_tuple3 let (i2, _) := swt2.p - if i2 = 1#u64 + if i2 = 1u64 then do let swp ← new_pair1 - if swp.p.x = 1#u32 + if swp.p.x = 1u32 then Result.ok () else Result.fail .panic else Result.fail .panic @@ -488,39 +488,39 @@ def test_weird_borrows1 : Result Unit := /- [no_nested_borrows::test_mem_replace]: Source: 'tests/src/no_nested_borrows.rs', lines 407:0-407:37 -/ def test_mem_replace (px : U32) : Result U32 := - let (y, _) := core.mem.replace U32 px 1#u32 - if y = 0#u32 - then Result.ok 2#u32 + let (y, _) := core.mem.replace U32 px 1u32 + if y = 0u32 + then Result.ok 2u32 else Result.fail .panic /- [no_nested_borrows::test_shared_borrow_bool1]: Source: 'tests/src/no_nested_borrows.rs', lines 414:0-414:47 -/ def test_shared_borrow_bool1 (b : Bool) : Result U32 := if b - then Result.ok 0#u32 - else Result.ok 1#u32 + then Result.ok 0u32 + else Result.ok 1u32 /- [no_nested_borrows::test_shared_borrow_bool2]: Source: 'tests/src/no_nested_borrows.rs', lines 427:0-427:40 -/ def test_shared_borrow_bool2 : Result U32 := - Result.ok 0#u32 + Result.ok 0u32 /- [no_nested_borrows::test_shared_borrow_enum1]: Source: 'tests/src/no_nested_borrows.rs', lines 442:0-442:52 -/ def test_shared_borrow_enum1 (l : List U32) : Result U32 := match l with - | List.Cons _ _ => Result.ok 1#u32 - | List.Nil => Result.ok 0#u32 + | List.Cons _ _ => Result.ok 1u32 + | List.Nil => Result.ok 0u32 /- [no_nested_borrows::test_shared_borrow_enum2]: Source: 'tests/src/no_nested_borrows.rs', lines 454:0-454:40 -/ def test_shared_borrow_enum2 : Result U32 := - Result.ok 0#u32 + Result.ok 0u32 /- [no_nested_borrows::incr]: Source: 'tests/src/no_nested_borrows.rs', lines 465:0-465:24 -/ def incr (x : U32) : Result U32 := - x + 1#u32 + x + 1u32 /- [no_nested_borrows::call_incr]: Source: 'tests/src/no_nested_borrows.rs', lines 469:0-469:35 -/ @@ -531,7 +531,7 @@ def call_incr (x : U32) : Result U32 := Source: 'tests/src/no_nested_borrows.rs', lines 474:0-474:41 -/ def read_then_incr (x : U32) : Result (U32 × U32) := do - let x1 ← x + 1#u32 + let x1 ← x + 1u32 Result.ok (x, x1) /- [no_nested_borrows::Tuple] @@ -548,7 +548,7 @@ def read_tuple (x : (U32 × U32)) : Result U32 := Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:39 -/ def update_tuple (x : (U32 × U32)) : Result (U32 × U32) := let (_, i) := x - Result.ok (1#u32, i) + Result.ok (1u32, i) /- [no_nested_borrows::read_tuple_struct]: Source: 'tests/src/no_nested_borrows.rs', lines 490:0-490:52 -/ @@ -560,7 +560,7 @@ def read_tuple_struct (x : Tuple U32 U32) : Result U32 := Source: 'tests/src/no_nested_borrows.rs', lines 494:0-494:51 -/ def update_tuple_struct (x : Tuple U32 U32) : Result (Tuple U32 U32) := let (_, i) := x - Result.ok (1#u32, i) + Result.ok (1u32, i) /- [no_nested_borrows::create_tuple_struct]: Source: 'tests/src/no_nested_borrows.rs', lines 498:0-498:61 -/ diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean index 03b96903..400406f1 100644 --- a/tests/lean/Paper.lean +++ b/tests/lean/Paper.lean @@ -8,14 +8,14 @@ namespace paper /- [paper::ref_incr]: Source: 'tests/src/paper.rs', lines 7:0-7:28 -/ def ref_incr (x : I32) : Result I32 := - x + 1#i32 + x + 1i32 /- [paper::test_incr]: Source: 'tests/src/paper.rs', lines 11:0-11:18 -/ def test_incr : Result Unit := do - let x ← ref_incr 0#i32 - if x = 1#i32 + let x ← ref_incr 0i32 + if x = 1i32 then Result.ok () else Result.fail .panic @@ -38,14 +38,14 @@ def choose Source: 'tests/src/paper.rs', lines 26:0-26:20 -/ def test_choose : Result Unit := do - let (z, choose_back) ← choose I32 true 0#i32 0#i32 - let z1 ← z + 1#i32 - if z1 = 1#i32 + let (z, choose_back) ← choose I32 true 0i32 0i32 + let z1 ← z + 1i32 + if z1 = 1i32 then do let (x, y) ← choose_back z1 - if x = 1#i32 - then if y = 0#i32 + if x = 1i32 + then if y = 0i32 then Result.ok () else Result.fail .panic else Result.fail .panic @@ -66,13 +66,13 @@ divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result (T × (T → Result (List T))) := match l with | List.Cons x tl => - if i = 0#u32 + if i = 0u32 then let back := fun ret => Result.ok (List.Cons ret tl) Result.ok (x, back) else do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 let (t, list_nth_mut_back) ← list_nth_mut T tl i1 let back := fun ret => @@ -89,19 +89,19 @@ divergent def sum (l : List I32) : Result I32 := | List.Cons x tl => do let i ← sum tl x + i - | List.Nil => Result.ok 0#i32 + | List.Nil => Result.ok 0i32 /- [paper::test_nth]: Source: 'tests/src/paper.rs', lines 71:0-71:17 -/ def test_nth : Result Unit := do - let l := List.Cons 3#i32 List.Nil - let l1 := List.Cons 2#i32 l - let (x, list_nth_mut_back) ← list_nth_mut I32 (List.Cons 1#i32 l1) 2#u32 - let x1 ← x + 1#i32 + let l := List.Cons 3i32 List.Nil + let l1 := List.Cons 2i32 l + let (x, list_nth_mut_back) ← list_nth_mut I32 (List.Cons 1i32 l1) 2u32 + let x1 ← x + 1i32 let l2 ← list_nth_mut_back x1 let i ← sum l2 - if i = 7#i32 + if i = 7i32 then Result.ok () else Result.fail .panic @@ -114,7 +114,7 @@ def call_choose (p : (U32 × U32)) : Result U32 := do let (px, py) := p let (pz, choose_back) ← choose U32 true px py - let pz1 ← pz + 1#u32 + let pz1 ← pz + 1u32 let (px1, _) ← choose_back pz1 Result.ok px1 diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index 0dd692fe..1cd8644b 100644 --- a/tests/lean/Traits.lean +++ b/tests/lean/Traits.lean @@ -148,7 +148,7 @@ structure ToType (Self T : Type) where /- [traits::{(traits::ToType for u64)#5}::to_type]: Source: 'tests/src/traits.rs', lines 94:4-94:28 -/ def ToTypeU64Bool.to_type (self : U64) : Result Bool := - Result.ok (self > 0#u64) + Result.ok (self > 0u64) /- Trait implementation: [traits::{(traits::ToType for u64)#5}] Source: 'tests/src/traits.rs', lines 93:0-93:25 -/ @@ -202,7 +202,7 @@ structure TestType.test.TestTrait (Self : Type) where Source: 'tests/src/traits.rs', lines 140:12-140:34 -/ def TestType.test.TestTraittraitsTestTypetestTestType1.test (self : TestType.test.TestType1) : Result Bool := - Result.ok (self > 1#u64) + Result.ok (self > 1u64) /- Trait implementation: [traits::{traits::TestType#6}::test::{(traits::{traits::TestType#6}::test::TestTrait for traits::{traits::TestType#6}::test::TestType1)}] Source: 'tests/src/traits.rs', lines 139:8-139:36 -/ @@ -217,8 +217,8 @@ def TestType.test (T : Type) (ToU64Inst : ToU64 T) (self : TestType T) (x : T) : Result Bool := do let x1 ← ToU64Inst.to_u64 x - if x1 > 0#u64 - then TestType.test.TestTraittraitsTestTypetestTestType1.test 0#u64 + if x1 > 0u64 + then TestType.test.TestTraittraitsTestTypetestTestType1.test 0u64 else Result.ok false /- [traits::BoolWrapper] @@ -243,7 +243,7 @@ def ToTypetraitsBoolWrapperT (T : Type) (ToTypeBoolTInst : ToType Bool T) : /- [traits::WithConstTy::LEN2] Source: 'tests/src/traits.rs', lines 165:4-165:21 -/ def WithConstTy.LEN2_default_body (Self : Type) (LEN : Usize) : Result Usize := - Result.ok 32#usize + Result.ok 32usize def WithConstTy.LEN2_default (Self : Type) (LEN : Usize) : Usize := eval_global (WithConstTy.LEN2_default_body Self LEN) @@ -259,19 +259,19 @@ structure WithConstTy (Self : Type) (LEN : Usize) where /- [traits::{(traits::WithConstTy<32: usize> for bool)#8}::LEN1] Source: 'tests/src/traits.rs', lines 176:4-176:21 -/ -def WithConstTyBool32.LEN1_body : Result Usize := Result.ok 12#usize +def WithConstTyBool32.LEN1_body : Result Usize := Result.ok 12usize def WithConstTyBool32.LEN1 : Usize := eval_global WithConstTyBool32.LEN1_body /- [traits::{(traits::WithConstTy<32: usize> for bool)#8}::f]: Source: 'tests/src/traits.rs', lines 181:4-181:39 -/ -def WithConstTyBool32.f (i : U64) (a : Array U8 32#usize) : Result U64 := +def WithConstTyBool32.f (i : U64) (a : Array U8 32usize) : Result U64 := Result.ok i /- Trait implementation: [traits::{(traits::WithConstTy<32: usize> for bool)#8}] Source: 'tests/src/traits.rs', lines 175:0-175:29 -/ -def WithConstTyBool32 : WithConstTy Bool 32#usize := { +def WithConstTyBool32 : WithConstTy Bool 32usize := { LEN1 := WithConstTyBool32.LEN1 - LEN2 := WithConstTy.LEN2_default Bool 32#usize + LEN2 := WithConstTy.LEN2_default Bool 32usize V := U8 W := U64 W_clause_0 := ToU64U64 @@ -312,7 +312,7 @@ def test_where1 (T : Type) (_x : T) : Result Unit := /- [traits::test_where2]: Source: 'tests/src/traits.rs', lines 195:0-195:57 -/ def test_where2 - (T : Type) (WithConstTyT32Inst : WithConstTy T 32#usize) (_x : U32) : + (T : Type) (WithConstTyT32Inst : WithConstTy T 32usize) (_x : U32) : Result Unit := Result.ok () @@ -489,7 +489,7 @@ def TraitArray (T : Type) (N : Usize) : Trait (Array T N) := { Source: 'tests/src/traits.rs', lines 320:4-320:20 -/ def TraittraitsWrapper.LEN_body (T : Type) (TraitInst : Trait T) : Result Usize := - Result.ok 0#usize + Result.ok 0usize def TraittraitsWrapper.LEN (T : Type) (TraitInst : Trait T) : Usize := eval_global (TraittraitsWrapper.LEN_body T TraitInst) @@ -522,7 +522,7 @@ inductive core.result.Result (T E : Type) := Source: 'tests/src/traits.rs', lines 333:4-333:33 -/ def Foo.FOO_body (T U : Type) (TraitInst : Trait T) : Result (core.result.Result T I32) := - Result.ok (core.result.Result.Err 0#i32) + Result.ok (core.result.Result.Err 0i32) def Foo.FOO (T U : Type) (TraitInst : Trait T) : core.result.Result T I32 := eval_global (Foo.FOO_body T U TraitInst) -- cgit v1.2.3 From f05a0faf14fdd558039da52624d57028eb64f9fd Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 12 Jun 2024 16:54:24 +0200 Subject: Fix some mistakes --- tests/lean/Arrays.lean | 4 ++-- tests/lean/Demo/Properties.lean | 4 ++-- tests/lean/Tutorial.lean | 22 +++++++++++----------- 3 files changed, 15 insertions(+), 15 deletions(-) (limited to 'tests') diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean index 70b4a26b..5f50e580 100644 --- a/tests/lean/Arrays.lean +++ b/tests/lean/Arrays.lean @@ -266,9 +266,9 @@ def index_all : Result U32 := let (s1, to_slice_mut_back) ← Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) let (i7, s2) ← index_mut_slice_u32_0 s1 - let i8 ← i6 + i7 + let i9 ← i6 + i7 let _ ← to_slice_mut_back s2 - Result.ok i8 + Result.ok i9 /- [arrays::update_array]: Source: 'tests/src/arrays.rs', lines 187:0-187:36 -/ diff --git a/tests/lean/Demo/Properties.lean b/tests/lean/Demo/Properties.lean index abdc2985..67023727 100644 --- a/tests/lean/Demo/Properties.lean +++ b/tests/lean/Demo/Properties.lean @@ -43,7 +43,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32) simp_all; scalar_tac | CCons hd tl => simp_all - if hi: i = 0#u32 then + if hi: i = 0u32 then simp_all else simp_all @@ -54,7 +54,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32) theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) : ∃ y, i32_id x = ok y ∧ x.val = y.val := by rw [i32_id] - if hx : x = 0#i32 then + if hx : x = 0i32 then simp_all else simp_all diff --git a/tests/lean/Tutorial.lean b/tests/lean/Tutorial.lean index 94b70991..7d347277 100644 --- a/tests/lean/Tutorial.lean +++ b/tests/lean/Tutorial.lean @@ -17,7 +17,7 @@ namespace Tutorial def mul2_add1 (x : U32) : Result U32 := do let x1 ← x + x - let x2 ← x1 + 1#u32 + let x2 ← x1 + 1u32 ok x2 /- There are several things to note. @@ -27,7 +27,7 @@ def mul2_add1 (x : U32) : Result U32 := do Because Rust programs manipulate machine integers which occupy a fixed size in memory, we model integers by using types like [U32], which is the type of integers which take their values between 0 and 2^32 - 1 (inclusive). - [1#u32] is simply the constant 1 (seen as a [U32]). + [1u32] is simply the constant 1 (seen as a [U32]). You can see a definition or its type by using the [#print] and [#check] commands. It is also possible to jump to definitions (right-click + "Go to Definition" @@ -229,10 +229,10 @@ open CList divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T := match l with | CCons x tl => - if i = 0#u32 + if i = 0u32 then ok x else do - let i1 ← i - 1#u32 + let i1 ← i - 1u32 list_nth T tl i1 | CNil => fail Error.panic @@ -285,9 +285,9 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32) simp only [] -- Perform a case disjunction on [i]. -- The notation [hi : ...] allows us to introduce an assumption in the - -- context, to remember the fact that in the branches we have [i = 0#u32] - -- and [¬ i = 0#u32]. - if hi: i = 0#u32 then + -- context, to remember the fact that in the branches we have [i = 0u32] + -- and [¬ i = 0u32]. + if hi: i = 0u32 then -- We can finish the proof simply by using the simplifier. -- We decompose the proof into several calls on purpose, so that it is -- easier to understand what is going on. @@ -348,17 +348,17 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32) annotates it with the [divergent] keyword. -/ divergent def i32_id (x : I32) : Result I32 := - if x = 0#i32 then ok 0#i32 + if x = 0i32 then ok 0i32 else do - let x1 ← x - 1#i32 + let x1 ← x - 1i32 let x2 ← i32_id x1 - x2 + 1#i32 + x2 + 1i32 /- We can easily prove that [i32_id] behaves like the identity on positive inputs -/ theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) : ∃ y, i32_id x = ok y ∧ x.val = y.val := by rw [i32_id] - if hx : x = 0#i32 then + if hx : x = 0i32 then simp_all else simp [hx] -- cgit v1.2.3 From 8ca43c32b30c03cc3fde51736ea5884dfd1c2c50 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 12 Jun 2024 18:20:14 +0200 Subject: Revert "Fix some mistakes" This reverts commit f05a0faf14fdd558039da52624d57028eb64f9fd. --- tests/lean/Arrays.lean | 4 ++-- tests/lean/Demo/Properties.lean | 4 ++-- tests/lean/Tutorial.lean | 22 +++++++++++----------- 3 files changed, 15 insertions(+), 15 deletions(-) (limited to 'tests') diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean index 5f50e580..70b4a26b 100644 --- a/tests/lean/Arrays.lean +++ b/tests/lean/Arrays.lean @@ -266,9 +266,9 @@ def index_all : Result U32 := let (s1, to_slice_mut_back) ← Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) let (i7, s2) ← index_mut_slice_u32_0 s1 - let i9 ← i6 + i7 + let i8 ← i6 + i7 let _ ← to_slice_mut_back s2 - Result.ok i9 + Result.ok i8 /- [arrays::update_array]: Source: 'tests/src/arrays.rs', lines 187:0-187:36 -/ diff --git a/tests/lean/Demo/Properties.lean b/tests/lean/Demo/Properties.lean index 67023727..abdc2985 100644 --- a/tests/lean/Demo/Properties.lean +++ b/tests/lean/Demo/Properties.lean @@ -43,7 +43,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32) simp_all; scalar_tac | CCons hd tl => simp_all - if hi: i = 0u32 then + if hi: i = 0#u32 then simp_all else simp_all @@ -54,7 +54,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32) theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) : ∃ y, i32_id x = ok y ∧ x.val = y.val := by rw [i32_id] - if hx : x = 0i32 then + if hx : x = 0#i32 then simp_all else simp_all diff --git a/tests/lean/Tutorial.lean b/tests/lean/Tutorial.lean index 7d347277..94b70991 100644 --- a/tests/lean/Tutorial.lean +++ b/tests/lean/Tutorial.lean @@ -17,7 +17,7 @@ namespace Tutorial def mul2_add1 (x : U32) : Result U32 := do let x1 ← x + x - let x2 ← x1 + 1u32 + let x2 ← x1 + 1#u32 ok x2 /- There are several things to note. @@ -27,7 +27,7 @@ def mul2_add1 (x : U32) : Result U32 := do Because Rust programs manipulate machine integers which occupy a fixed size in memory, we model integers by using types like [U32], which is the type of integers which take their values between 0 and 2^32 - 1 (inclusive). - [1u32] is simply the constant 1 (seen as a [U32]). + [1#u32] is simply the constant 1 (seen as a [U32]). You can see a definition or its type by using the [#print] and [#check] commands. It is also possible to jump to definitions (right-click + "Go to Definition" @@ -229,10 +229,10 @@ open CList divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T := match l with | CCons x tl => - if i = 0u32 + if i = 0#u32 then ok x else do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 list_nth T tl i1 | CNil => fail Error.panic @@ -285,9 +285,9 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32) simp only [] -- Perform a case disjunction on [i]. -- The notation [hi : ...] allows us to introduce an assumption in the - -- context, to remember the fact that in the branches we have [i = 0u32] - -- and [¬ i = 0u32]. - if hi: i = 0u32 then + -- context, to remember the fact that in the branches we have [i = 0#u32] + -- and [¬ i = 0#u32]. + if hi: i = 0#u32 then -- We can finish the proof simply by using the simplifier. -- We decompose the proof into several calls on purpose, so that it is -- easier to understand what is going on. @@ -348,17 +348,17 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32) annotates it with the [divergent] keyword. -/ divergent def i32_id (x : I32) : Result I32 := - if x = 0i32 then ok 0i32 + if x = 0#i32 then ok 0#i32 else do - let x1 ← x - 1i32 + let x1 ← x - 1#i32 let x2 ← i32_id x1 - x2 + 1i32 + x2 + 1#i32 /- We can easily prove that [i32_id] behaves like the identity on positive inputs -/ theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) : ∃ y, i32_id x = ok y ∧ x.val = y.val := by rw [i32_id] - if hx : x = 0i32 then + if hx : x = 0#i32 then simp_all else simp [hx] -- cgit v1.2.3 From d85d160ae9736f50d9c043b411c5a831f1fbb964 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 12 Jun 2024 18:20:35 +0200 Subject: Revert "Regenerate the tests" This reverts commit cd5542fc82edee11181a43e3a342a2567c929e7e. --- tests/lean/Arrays.lean | 225 ++++++++++++++++++++-------------------- tests/lean/Betree/Funs.lean | 22 ++-- tests/lean/Bitwise.lean | 8 +- tests/lean/Constants.lean | 28 ++--- tests/lean/Demo/Demo.lean | 28 ++--- tests/lean/External/Funs.lean | 2 +- tests/lean/Hashmap/Funs.lean | 62 +++++------ tests/lean/Loops.lean | 94 ++++++++--------- tests/lean/Matches.lean | 6 +- tests/lean/NoNestedBorrows.lean | 138 ++++++++++++------------ tests/lean/Paper.lean | 34 +++--- tests/lean/Traits.lean | 24 ++--- 12 files changed, 338 insertions(+), 333 deletions(-) (limited to 'tests') diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean index 70b4a26b..9748919e 100644 --- a/tests/lean/Arrays.lean +++ b/tests/lean/Arrays.lean @@ -14,34 +14,34 @@ inductive AB := /- [arrays::incr]: Source: 'tests/src/arrays.rs', lines 11:0-11:24 -/ def incr (x : U32) : Result U32 := - x + 1u32 + x + 1#u32 /- [arrays::array_to_shared_slice_]: Source: 'tests/src/arrays.rs', lines 19:0-19:53 -/ def array_to_shared_slice_ - (T : Type) (s : Array T 32usize) : Result (Slice T) := - Array.to_slice T 32usize s + (T : Type) (s : Array T 32#usize) : Result (Slice T) := + Array.to_slice T 32#usize s /- [arrays::array_to_mut_slice_]: Source: 'tests/src/arrays.rs', lines 24:0-24:58 -/ def array_to_mut_slice_ - (T : Type) (s : Array T 32usize) : - Result ((Slice T) × (Slice T → Result (Array T 32usize))) + (T : Type) (s : Array T 32#usize) : + Result ((Slice T) × (Slice T → Result (Array T 32#usize))) := - Array.to_slice_mut T 32usize s + Array.to_slice_mut T 32#usize s /- [arrays::array_len]: Source: 'tests/src/arrays.rs', lines 28:0-28:40 -/ -def array_len (T : Type) (s : Array T 32usize) : Result Usize := +def array_len (T : Type) (s : Array T 32#usize) : Result Usize := do - let s1 ← Array.to_slice T 32usize s + let s1 ← Array.to_slice T 32#usize s Result.ok (Slice.len T s1) /- [arrays::shared_array_len]: Source: 'tests/src/arrays.rs', lines 32:0-32:48 -/ -def shared_array_len (T : Type) (s : Array T 32usize) : Result Usize := +def shared_array_len (T : Type) (s : Array T 32#usize) : Result Usize := do - let s1 ← Array.to_slice T 32usize s + let s1 ← Array.to_slice T 32#usize s Result.ok (Slice.len T s1) /- [arrays::shared_slice_len]: @@ -52,26 +52,26 @@ def shared_slice_len (T : Type) (s : Slice T) : Result Usize := /- [arrays::index_array_shared]: Source: 'tests/src/arrays.rs', lines 40:0-40:57 -/ def index_array_shared - (T : Type) (s : Array T 32usize) (i : Usize) : Result T := - Array.index_usize T 32usize s i + (T : Type) (s : Array T 32#usize) (i : Usize) : Result T := + Array.index_usize T 32#usize s i /- [arrays::index_array_u32]: Source: 'tests/src/arrays.rs', lines 47:0-47:53 -/ -def index_array_u32 (s : Array U32 32usize) (i : Usize) : Result U32 := - Array.index_usize U32 32usize s i +def index_array_u32 (s : Array U32 32#usize) (i : Usize) : Result U32 := + Array.index_usize U32 32#usize s i /- [arrays::index_array_copy]: Source: 'tests/src/arrays.rs', lines 51:0-51:45 -/ -def index_array_copy (x : Array U32 32usize) : Result U32 := - Array.index_usize U32 32usize x 0usize +def index_array_copy (x : Array U32 32#usize) : Result U32 := + Array.index_usize U32 32#usize x 0#usize /- [arrays::index_mut_array]: Source: 'tests/src/arrays.rs', lines 55:0-55:62 -/ def index_mut_array - (T : Type) (s : Array T 32usize) (i : Usize) : - Result (T × (T → Result (Array T 32usize))) + (T : Type) (s : Array T 32#usize) (i : Usize) : + Result (T × (T → Result (Array T 32#usize))) := - Array.index_mut_usize T 32usize s i + Array.index_mut_usize T 32#usize s i /- [arrays::index_slice]: Source: 'tests/src/arrays.rs', lines 59:0-59:46 -/ @@ -109,22 +109,22 @@ def slice_subslice_mut_ /- [arrays::array_to_slice_shared_]: Source: 'tests/src/arrays.rs', lines 75:0-75:54 -/ -def array_to_slice_shared_ (x : Array U32 32usize) : Result (Slice U32) := - Array.to_slice U32 32usize x +def array_to_slice_shared_ (x : Array U32 32#usize) : Result (Slice U32) := + Array.to_slice U32 32#usize x /- [arrays::array_to_slice_mut_]: Source: 'tests/src/arrays.rs', lines 79:0-79:59 -/ def array_to_slice_mut_ - (x : Array U32 32usize) : - Result ((Slice U32) × (Slice U32 → Result (Array U32 32usize))) + (x : Array U32 32#usize) : + Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize))) := - Array.to_slice_mut U32 32usize x + Array.to_slice_mut U32 32#usize x /- [arrays::array_subslice_shared_]: Source: 'tests/src/arrays.rs', lines 83:0-83:74 -/ def array_subslice_shared_ - (x : Array U32 32usize) (y : Usize) (z : Usize) : Result (Slice U32) := - core.array.Array.index U32 (core.ops.range.Range Usize) 32usize + (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) := + core.array.Array.index U32 (core.ops.range.Range Usize) 32#usize (core.ops.index.IndexSliceTIInst U32 (core.ops.range.Range Usize) (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x { start := y, end_ := z } @@ -132,12 +132,12 @@ def array_subslice_shared_ /- [arrays::array_subslice_mut_]: Source: 'tests/src/arrays.rs', lines 87:0-87:79 -/ def array_subslice_mut_ - (x : Array U32 32usize) (y : Usize) (z : Usize) : - Result ((Slice U32) × (Slice U32 → Result (Array U32 32usize))) + (x : Array U32 32#usize) (y : Usize) (z : Usize) : + Result ((Slice U32) × (Slice U32 → Result (Array U32 32#usize))) := do let (s, index_mut_back) ← - core.array.Array.index_mut U32 (core.ops.range.Range Usize) 32usize + core.array.Array.index_mut 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 } @@ -146,50 +146,50 @@ def array_subslice_mut_ /- [arrays::index_slice_0]: Source: 'tests/src/arrays.rs', lines 91:0-91:38 -/ def index_slice_0 (T : Type) (s : Slice T) : Result T := - Slice.index_usize T s 0usize + Slice.index_usize T s 0#usize /- [arrays::index_array_0]: Source: 'tests/src/arrays.rs', lines 95:0-95:42 -/ -def index_array_0 (T : Type) (s : Array T 32usize) : Result T := - Array.index_usize T 32usize s 0usize +def index_array_0 (T : Type) (s : Array T 32#usize) : Result T := + Array.index_usize T 32#usize s 0#usize /- [arrays::index_index_array]: Source: 'tests/src/arrays.rs', lines 106:0-106:71 -/ def index_index_array - (s : Array (Array U32 32usize) 32usize) (i : Usize) (j : Usize) : + (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) : Result U32 := do - let a ← Array.index_usize (Array U32 32usize) 32usize s i - Array.index_usize U32 32usize a j + let a ← Array.index_usize (Array U32 32#usize) 32#usize s i + Array.index_usize U32 32#usize a j /- [arrays::update_update_array]: Source: 'tests/src/arrays.rs', lines 117:0-117:70 -/ def update_update_array - (s : Array (Array U32 32usize) 32usize) (i : Usize) (j : Usize) : + (s : Array (Array U32 32#usize) 32#usize) (i : Usize) (j : Usize) : Result Unit := do let (a, index_mut_back) ← - Array.index_mut_usize (Array U32 32usize) 32usize s i - let (_, index_mut_back1) ← Array.index_mut_usize U32 32usize a j - let a1 ← index_mut_back1 0u32 + Array.index_mut_usize (Array U32 32#usize) 32#usize s i + 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.ok () /- [arrays::array_local_deep_copy]: Source: 'tests/src/arrays.rs', lines 121:0-121:43 -/ -def array_local_deep_copy (x : Array U32 32usize) : Result Unit := +def array_local_deep_copy (x : Array U32 32#usize) : Result Unit := Result.ok () /- [arrays::take_array]: Source: 'tests/src/arrays.rs', lines 125:0-125:30 -/ -def take_array (a : Array U32 2usize) : Result Unit := +def take_array (a : Array U32 2#usize) : Result Unit := Result.ok () /- [arrays::take_array_borrow]: Source: 'tests/src/arrays.rs', lines 126:0-126:38 -/ -def take_array_borrow (a : Array U32 2usize) : Result Unit := +def take_array_borrow (a : Array U32 2#usize) : Result Unit := Result.ok () /- [arrays::take_slice]: @@ -204,67 +204,70 @@ def take_mut_slice (s : Slice U32) : Result (Slice U32) := /- [arrays::const_array]: Source: 'tests/src/arrays.rs', lines 130:0-130:32 -/ -def const_array : Result (Array U32 2usize) := - Result.ok (Array.make U32 2usize [ 0u32, 0u32 ]) +def const_array : Result (Array U32 2#usize) := + Result.ok (Array.make U32 2#usize [ 0#u32, 0#u32 ]) /- [arrays::const_slice]: Source: 'tests/src/arrays.rs', lines 134:0-134:20 -/ def const_slice : Result Unit := do - let _ ← Array.to_slice U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) + let _ ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) Result.ok () /- [arrays::take_all]: Source: 'tests/src/arrays.rs', lines 144:0-144:17 -/ def take_all : Result Unit := do - let _ ← take_array (Array.make U32 2usize [ 0u32, 0u32 ]) - let _ ← take_array (Array.make U32 2usize [ 0u32, 0u32 ]) - let _ ← take_array_borrow (Array.make U32 2usize [ 0u32, 0u32 ]) - let s ← Array.to_slice U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) + let _ ← take_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let _ ← take_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let _ ← take_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let s ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) let _ ← take_slice s let (s1, to_slice_mut_back) ← - Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) + 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.ok () /- [arrays::index_array]: Source: 'tests/src/arrays.rs', lines 158:0-158:38 -/ -def index_array (x : Array U32 2usize) : Result U32 := - Array.index_usize U32 2usize x 0usize +def index_array (x : Array U32 2#usize) : Result U32 := + Array.index_usize U32 2#usize x 0#usize /- [arrays::index_array_borrow]: Source: 'tests/src/arrays.rs', lines 161:0-161:46 -/ -def index_array_borrow (x : Array U32 2usize) : Result U32 := - Array.index_usize U32 2usize x 0usize +def index_array_borrow (x : Array U32 2#usize) : Result U32 := + Array.index_usize U32 2#usize x 0#usize /- [arrays::index_slice_u32_0]: Source: 'tests/src/arrays.rs', lines 165:0-165:42 -/ def index_slice_u32_0 (x : Slice U32) : Result U32 := - Slice.index_usize U32 x 0usize + Slice.index_usize U32 x 0#usize /- [arrays::index_mut_slice_u32_0]: Source: 'tests/src/arrays.rs', lines 169:0-169:50 -/ def index_mut_slice_u32_0 (x : Slice U32) : Result (U32 × (Slice U32)) := do - let i ← Slice.index_usize U32 x 0usize + let i ← Slice.index_usize U32 x 0#usize Result.ok (i, x) /- [arrays::index_all]: Source: 'tests/src/arrays.rs', lines 173:0-173:25 -/ def index_all : Result U32 := do - let i ← index_array (Array.make U32 2usize [ 0u32, 0u32 ]) - let i1 ← index_array (Array.make U32 2usize [ 0u32, 0u32 ]) + let i ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let i1 ← index_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) let i2 ← i + i1 - let i3 ← index_array_borrow (Array.make U32 2usize [ 0u32, 0u32 ]) + let i3 ← index_array_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) let i4 ← i2 + i3 - let s ← Array.to_slice U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) + let s ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) let i5 ← index_slice_u32_0 s let i6 ← i4 + i5 let (s1, to_slice_mut_back) ← - Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) + Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) let (i7, s2) ← index_mut_slice_u32_0 s1 let i8 ← i6 + i7 let _ ← to_slice_mut_back s2 @@ -272,35 +275,35 @@ def index_all : Result U32 := /- [arrays::update_array]: Source: 'tests/src/arrays.rs', lines 187:0-187:36 -/ -def update_array (x : Array U32 2usize) : Result Unit := +def update_array (x : Array U32 2#usize) : Result Unit := do - let (_, index_mut_back) ← Array.index_mut_usize U32 2usize x 0usize - let _ ← index_mut_back 1u32 + let (_, index_mut_back) ← Array.index_mut_usize U32 2#usize x 0#usize + let _ ← index_mut_back 1#u32 Result.ok () /- [arrays::update_array_mut_borrow]: Source: 'tests/src/arrays.rs', lines 190:0-190:48 -/ def update_array_mut_borrow - (x : Array U32 2usize) : Result (Array U32 2usize) := + (x : Array U32 2#usize) : Result (Array U32 2#usize) := do - let (_, index_mut_back) ← Array.index_mut_usize U32 2usize x 0usize - index_mut_back 1u32 + let (_, index_mut_back) ← Array.index_mut_usize U32 2#usize x 0#usize + index_mut_back 1#u32 /- [arrays::update_mut_slice]: Source: 'tests/src/arrays.rs', lines 193:0-193:38 -/ def update_mut_slice (x : Slice U32) : Result (Slice U32) := do - let (_, index_mut_back) ← Slice.index_mut_usize U32 x 0usize - index_mut_back 1u32 + let (_, index_mut_back) ← Slice.index_mut_usize U32 x 0#usize + index_mut_back 1#u32 /- [arrays::update_all]: Source: 'tests/src/arrays.rs', lines 197:0-197:19 -/ def update_all : Result Unit := do - let _ ← update_array (Array.make U32 2usize [ 0u32, 0u32 ]) - let _ ← update_array (Array.make U32 2usize [ 0u32, 0u32 ]) - let x ← update_array_mut_borrow (Array.make U32 2usize [ 0u32, 0u32 ]) - let (s, to_slice_mut_back) ← Array.to_slice_mut U32 2usize x + let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let _ ← update_array (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + let x ← update_array_mut_borrow (Array.make U32 2#usize [ 0#u32, 0#u32 ]) + 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.ok () @@ -310,37 +313,37 @@ def update_all : Result Unit := def range_all : Result Unit := do let (s, index_mut_back) ← - core.array.Array.index_mut U32 (core.ops.range.Range Usize) 4usize + core.array.Array.index_mut U32 (core.ops.range.Range Usize) 4#usize (core.ops.index.IndexMutSliceTIInst U32 (core.ops.range.Range Usize) (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) - (Array.make U32 4usize [ 0u32, 0u32, 0u32, 0u32 ]) - { start := 1usize, end_ := 3usize } + (Array.make U32 4#usize [ 0#u32, 0#u32, 0#u32, 0#u32 ]) + { start := 1#usize, end_ := 3#usize } let s1 ← update_mut_slice s let _ ← index_mut_back s1 Result.ok () /- [arrays::deref_array_borrow]: Source: 'tests/src/arrays.rs', lines 217:0-217:46 -/ -def deref_array_borrow (x : Array U32 2usize) : Result U32 := - Array.index_usize U32 2usize x 0usize +def deref_array_borrow (x : Array U32 2#usize) : Result U32 := + Array.index_usize U32 2#usize x 0#usize /- [arrays::deref_array_mut_borrow]: Source: 'tests/src/arrays.rs', lines 222:0-222:54 -/ def deref_array_mut_borrow - (x : Array U32 2usize) : Result (U32 × (Array U32 2usize)) := + (x : Array U32 2#usize) : Result (U32 × (Array U32 2#usize)) := do - let i ← Array.index_usize U32 2usize x 0usize + let i ← Array.index_usize U32 2#usize x 0#usize Result.ok (i, x) /- [arrays::take_array_t]: Source: 'tests/src/arrays.rs', lines 230:0-230:31 -/ -def take_array_t (a : Array AB 2usize) : Result Unit := +def take_array_t (a : Array AB 2#usize) : Result Unit := Result.ok () /- [arrays::non_copyable_array]: Source: 'tests/src/arrays.rs', lines 232:0-232:27 -/ def non_copyable_array : Result Unit := - take_array_t (Array.make AB 2usize [ AB.A, AB.B ]) + take_array_t (Array.make AB 2#usize [ AB.A, AB.B ]) /- [arrays::sum]: loop 0: Source: 'tests/src/arrays.rs', lines 245:0-253:1 -/ @@ -351,14 +354,14 @@ divergent def sum_loop (s : Slice U32) (sum1 : U32) (i : Usize) : Result U32 := do let i2 ← Slice.index_usize U32 s i let sum3 ← sum1 + i2 - let i3 ← i + 1usize + let i3 ← i + 1#usize sum_loop s sum3 i3 else Result.ok sum1 /- [arrays::sum]: Source: 'tests/src/arrays.rs', lines 245:0-245:28 -/ def sum (s : Slice U32) : Result U32 := - sum_loop s 0u32 0usize + sum_loop s 0#u32 0#usize /- [arrays::sum2]: loop 0: Source: 'tests/src/arrays.rs', lines 255:0-264:1 -/ @@ -372,7 +375,7 @@ divergent def sum2_loop let i3 ← Slice.index_usize U32 s2 i let i4 ← i2 + i3 let sum3 ← sum1 + i4 - let i5 ← i + 1usize + let i5 ← i + 1#usize sum2_loop s s2 sum3 i5 else Result.ok sum1 @@ -382,7 +385,7 @@ def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 := let i := Slice.len U32 s let i1 := Slice.len U32 s2 if i = i1 - then sum2_loop s s2 0u32 0usize + then sum2_loop s s2 0#u32 0#usize else Result.fail .panic /- [arrays::f0]: @@ -390,9 +393,9 @@ def sum2 (s : Slice U32) (s2 : Slice U32) : Result U32 := def f0 : Result Unit := do let (s, to_slice_mut_back) ← - Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ]) - let (_, index_mut_back) ← Slice.index_mut_usize U32 s 0usize - let s1 ← index_mut_back 1u32 + Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) + 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.ok () @@ -401,9 +404,9 @@ def f0 : Result Unit := def f1 : Result Unit := do let (_, index_mut_back) ← - Array.index_mut_usize U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ]) - 0usize - let _ ← index_mut_back 1u32 + 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.ok () /- [arrays::f2]: @@ -413,8 +416,8 @@ def f2 (i : U32) : Result Unit := /- [arrays::f4]: Source: 'tests/src/arrays.rs', lines 285:0-285:54 -/ -def f4 (x : Array U32 32usize) (y : Usize) (z : Usize) : Result (Slice U32) := - core.array.Array.index U32 (core.ops.range.Range Usize) 32usize +def f4 (x : Array U32 32#usize) (y : Usize) (z : Usize) : Result (Slice U32) := + core.array.Array.index U32 (core.ops.range.Range Usize) 32#usize (core.ops.index.IndexSliceTIInst U32 (core.ops.range.Range Usize) (core.slice.index.SliceIndexRangeUsizeSliceTInst U32)) x { start := y, end_ := z } @@ -424,32 +427,34 @@ def f4 (x : Array U32 32usize) (y : Usize) (z : Usize) : Result (Slice U32) := def f3 : Result U32 := do let i ← - Array.index_usize U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ]) 0usize + Array.index_usize U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) + 0#usize let _ ← f2 i - let b := Array.repeat U32 32usize 0u32 - let s ← Array.to_slice U32 2usize (Array.make U32 2usize [ 1u32, 2u32 ]) - let s1 ← f4 b 16usize 18usize + let b := Array.repeat U32 32#usize 0#u32 + let s ← + Array.to_slice U32 2#usize (Array.make U32 2#usize [ 1#u32, 2#u32 ]) + let s1 ← f4 b 16#usize 18#usize sum2 s s1 /- [arrays::SZ] Source: 'tests/src/arrays.rs', lines 289:0-289:19 -/ -def SZ_body : Result Usize := Result.ok 32usize +def SZ_body : Result Usize := Result.ok 32#usize def SZ : Usize := eval_global SZ_body /- [arrays::f5]: Source: 'tests/src/arrays.rs', lines 292:0-292:31 -/ -def f5 (x : Array U32 32usize) : Result U32 := - Array.index_usize U32 32usize x 0usize +def f5 (x : Array U32 32#usize) : Result U32 := + Array.index_usize U32 32#usize x 0#usize /- [arrays::ite]: Source: 'tests/src/arrays.rs', lines 297:0-297:12 -/ def ite : Result Unit := do let (s, to_slice_mut_back) ← - Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) + Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) let (_, s1) ← index_mut_slice_u32_0 s let (s2, to_slice_mut_back1) ← - Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ]) + Array.to_slice_mut U32 2#usize (Array.make U32 2#usize [ 0#u32, 0#u32 ]) let (_, s3) ← index_mut_slice_u32_0 s2 let _ ← to_slice_mut_back1 s3 let _ ← to_slice_mut_back s1 @@ -463,8 +468,8 @@ divergent def zero_slice_loop then do let (_, index_mut_back) ← Slice.index_mut_usize U8 a i - let i1 ← i + 1usize - let a1 ← index_mut_back 0u8 + let i1 ← i + 1#usize + let a1 ← index_mut_back 0#u8 zero_slice_loop a1 i1 len else Result.ok a @@ -472,14 +477,14 @@ divergent def zero_slice_loop Source: 'tests/src/arrays.rs', lines 306:0-306:31 -/ def zero_slice (a : Slice U8) : Result (Slice U8) := let len := Slice.len U8 a - zero_slice_loop a 0usize len + zero_slice_loop a 0#usize len /- [arrays::iter_mut_slice]: loop 0: Source: 'tests/src/arrays.rs', lines 315:0-321:1 -/ divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit := if i < len then do - let i1 ← i + 1usize + let i1 ← i + 1#usize iter_mut_slice_loop len i1 else Result.ok () @@ -488,7 +493,7 @@ divergent def iter_mut_slice_loop (len : Usize) (i : Usize) : Result Unit := def iter_mut_slice (a : Slice U8) : Result (Slice U8) := do let len := Slice.len U8 a - let _ ← iter_mut_slice_loop len 0usize + let _ ← iter_mut_slice_loop len 0#usize Result.ok a /- [arrays::sum_mut_slice]: loop 0: @@ -501,7 +506,7 @@ divergent def sum_mut_slice_loop do let i2 ← Slice.index_usize U32 a i let s1 ← s + i2 - let i3 ← i + 1usize + let i3 ← i + 1#usize sum_mut_slice_loop a i3 s1 else Result.ok s @@ -509,7 +514,7 @@ divergent def sum_mut_slice_loop Source: 'tests/src/arrays.rs', lines 323:0-323:42 -/ def sum_mut_slice (a : Slice U32) : Result (U32 × (Slice U32)) := do - let i ← sum_mut_slice_loop a 0usize 0u32 + let i ← sum_mut_slice_loop a 0#usize 0#u32 Result.ok (i, a) end arrays diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean index 74344e01..7d8b4714 100644 --- a/tests/lean/Betree/Funs.lean +++ b/tests/lean/Betree/Funs.lean @@ -41,20 +41,20 @@ def betree.store_leaf_node Source: 'src/betree.rs', lines 55:0-55:48 -/ def betree.fresh_node_id (counter : U64) : Result (U64 × U64) := do - let counter1 ← counter + 1u64 + let counter1 ← counter + 1#u64 Result.ok (counter, counter1) /- [betree::betree::{betree::betree::NodeIdCounter}::new]: Source: 'src/betree.rs', lines 206:4-206:20 -/ def betree.NodeIdCounter.new : Result betree.NodeIdCounter := - Result.ok { next_node_id := 0u64 } + Result.ok { next_node_id := 0#u64 } /- [betree::betree::{betree::betree::NodeIdCounter}::fresh_id]: Source: 'src/betree.rs', lines 210:4-210:36 -/ def betree.NodeIdCounter.fresh_id (self : betree.NodeIdCounter) : Result (U64 × betree.NodeIdCounter) := do - let i ← self.next_node_id + 1u64 + let i ← self.next_node_id + 1#u64 Result.ok (self.next_node_id, { next_node_id := i }) /- [betree::betree::upsert_update]: @@ -65,7 +65,7 @@ def betree.upsert_update | none => match st with | betree.UpsertFunState.Add v => Result.ok v - | betree.UpsertFunState.Sub _ => Result.ok 0u64 + | betree.UpsertFunState.Sub _ => Result.ok 0#u64 | some prev1 => match st with | betree.UpsertFunState.Add v => @@ -77,7 +77,7 @@ def betree.upsert_update | betree.UpsertFunState.Sub v => if prev1 >= v then prev1 - v - else Result.ok 0u64 + else Result.ok 0#u64 /- [betree::betree::{betree::betree::List#1}::len]: loop 0: Source: 'src/betree.rs', lines 276:4-284:5 -/ @@ -86,14 +86,14 @@ divergent def betree.List.len_loop match self with | betree.List.Cons _ tl => do - let len1 ← len + 1u64 + let len1 ← len + 1#u64 betree.List.len_loop T tl len1 | betree.List.Nil => Result.ok len /- [betree::betree::{betree::betree::List#1}::len]: Source: 'src/betree.rs', lines 276:4-276:24 -/ def betree.List.len (T : Type) (self : betree.List T) : Result U64 := - betree.List.len_loop T self 0u64 + betree.List.len_loop T self 0#u64 /- [betree::betree::{betree::betree::List#1}::reverse]: loop 0: Source: 'src/betree.rs', lines 304:4-312:5 -/ @@ -118,12 +118,12 @@ divergent def betree.List.split_at_loop (T : Type) (n : U64) (beg : betree.List T) (self : betree.List T) : Result ((betree.List T) × (betree.List T)) := - if n > 0u64 + if n > 0#u64 then match self with | betree.List.Cons hd tl => do - let n1 ← n - 1u64 + let n1 ← n - 1#u64 betree.List.split_at_loop T n1 (betree.List.Cons hd beg) tl | betree.List.Nil => Result.fail .panic else do @@ -706,7 +706,7 @@ divergent def betree.Node.apply_messages let (st1, content) ← betree.load_leaf_node node.id st let content1 ← betree.Node.apply_messages_to_leaf content msgs let len ← betree.List.len (U64 × U64) content1 - let i ← 2u64 * params.split_size + let i ← 2#u64 * params.split_size if len >= i then do @@ -751,7 +751,7 @@ def betree.BeTree.new { params := { min_flush_size := min_flush_size, split_size := split_size }, node_id_cnt := node_id_cnt1, - root := (betree.Node.Leaf { id := id, size := 0u64 }) + root := (betree.Node.Leaf { id := id, size := 0#u64 }) }) /- [betree::betree::{betree::betree::BeTree#6}::apply]: diff --git a/tests/lean/Bitwise.lean b/tests/lean/Bitwise.lean index 8884d309..23ec66b4 100644 --- a/tests/lean/Bitwise.lean +++ b/tests/lean/Bitwise.lean @@ -9,15 +9,15 @@ namespace bitwise Source: 'tests/src/bitwise.rs', lines 5:0-5:31 -/ def shift_u32 (a : U32) : Result U32 := do - let t ← a >>> 16usize - t <<< 16usize + let t ← a >>> 16#usize + t <<< 16#usize /- [bitwise::shift_i32]: Source: 'tests/src/bitwise.rs', lines 12:0-12:31 -/ def shift_i32 (a : I32) : Result I32 := do - let t ← a >>> 16isize - t <<< 16isize + let t ← a >>> 16#isize + t <<< 16#isize /- [bitwise::xor_u32]: Source: 'tests/src/bitwise.rs', lines 19:0-19:37 -/ diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean index a72ac98d..ecb91c16 100644 --- a/tests/lean/Constants.lean +++ b/tests/lean/Constants.lean @@ -7,7 +7,7 @@ namespace constants /- [constants::X0] Source: 'tests/src/constants.rs', lines 8:0-8:17 -/ -def X0_body : Result U32 := Result.ok 0u32 +def X0_body : Result U32 := Result.ok 0#u32 def X0 : U32 := eval_global X0_body /- [constants::X1] @@ -17,17 +17,17 @@ def X1 : U32 := eval_global X1_body /- [constants::X2] Source: 'tests/src/constants.rs', lines 13:0-13:17 -/ -def X2_body : Result U32 := Result.ok 3u32 +def X2_body : Result U32 := Result.ok 3#u32 def X2 : U32 := eval_global X2_body /- [constants::incr]: Source: 'tests/src/constants.rs', lines 20:0-20:32 -/ def incr (n : U32) : Result U32 := - n + 1u32 + n + 1#u32 /- [constants::X3] Source: 'tests/src/constants.rs', lines 18:0-18:17 -/ -def X3_body : Result U32 := incr 32u32 +def X3_body : Result U32 := incr 32#u32 def X3 : U32 := eval_global X3_body /- [constants::mk_pair0]: @@ -48,22 +48,22 @@ def mk_pair1 (x : U32) (y : U32) : Result (Pair U32 U32) := /- [constants::P0] Source: 'tests/src/constants.rs', lines 34:0-34:24 -/ -def P0_body : Result (U32 × U32) := mk_pair0 0u32 1u32 +def P0_body : Result (U32 × U32) := mk_pair0 0#u32 1#u32 def P0 : (U32 × U32) := eval_global P0_body /- [constants::P1] Source: 'tests/src/constants.rs', lines 35:0-35:28 -/ -def P1_body : Result (Pair U32 U32) := mk_pair1 0u32 1u32 +def P1_body : Result (Pair U32 U32) := mk_pair1 0#u32 1#u32 def P1 : Pair U32 U32 := eval_global P1_body /- [constants::P2] Source: 'tests/src/constants.rs', lines 36:0-36:24 -/ -def P2_body : Result (U32 × U32) := Result.ok (0u32, 1u32) +def P2_body : Result (U32 × U32) := Result.ok (0#u32, 1#u32) def P2 : (U32 × U32) := eval_global P2_body /- [constants::P3] Source: 'tests/src/constants.rs', lines 37:0-37:28 -/ -def P3_body : Result (Pair U32 U32) := Result.ok { x := 0u32, y := 1u32 } +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] @@ -78,7 +78,7 @@ def Wrap.new (T : Type) (value : T) : Result (Wrap T) := /- [constants::Y] Source: 'tests/src/constants.rs', lines 44:0-44:22 -/ -def Y_body : Result (Wrap I32) := Wrap.new I32 2i32 +def Y_body : Result (Wrap I32) := Wrap.new I32 2#i32 def Y : Wrap I32 := eval_global Y_body /- [constants::unwrap_y]: @@ -93,7 +93,7 @@ def YVAL : I32 := eval_global YVAL_body /- [constants::get_z1::Z1] Source: 'tests/src/constants.rs', lines 65:4-65:17 -/ -def get_z1.Z1_body : Result I32 := Result.ok 3i32 +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]: @@ -108,7 +108,7 @@ def add (a : I32) (b : I32) : Result I32 := /- [constants::Q1] Source: 'tests/src/constants.rs', lines 77:0-77:17 -/ -def Q1_body : Result I32 := Result.ok 5i32 +def Q1_body : Result I32 := Result.ok 5#i32 def Q1 : I32 := eval_global Q1_body /- [constants::Q2] @@ -118,7 +118,7 @@ def Q2 : I32 := eval_global Q2_body /- [constants::Q3] Source: 'tests/src/constants.rs', lines 79:0-79:17 -/ -def Q3_body : Result I32 := add Q2 3i32 +def Q3_body : Result I32 := add Q2 3#i32 def Q3 : I32 := eval_global Q3_body /- [constants::get_z2]: @@ -131,7 +131,7 @@ def get_z2 : Result I32 := /- [constants::S1] Source: 'tests/src/constants.rs', lines 83:0-83:18 -/ -def S1_body : Result U32 := Result.ok 6u32 +def S1_body : Result U32 := Result.ok 6#u32 def S1 : U32 := eval_global S1_body /- [constants::S2] @@ -146,7 +146,7 @@ def S3 : Pair U32 U32 := eval_global S3_body /- [constants::S4] Source: 'tests/src/constants.rs', lines 86:0-86:29 -/ -def S4_body : Result (Pair U32 U32) := mk_pair1 7u32 8u32 +def S4_body : Result (Pair U32 U32) := mk_pair1 7#u32 8#u32 def S4 : Pair U32 U32 := eval_global S4_body /- [constants::V] diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean index 9d8b085c..48ac2062 100644 --- a/tests/lean/Demo/Demo.lean +++ b/tests/lean/Demo/Demo.lean @@ -22,7 +22,7 @@ def choose def mul2_add1 (x : U32) : Result U32 := do let i ← x + x - i + 1u32 + i + 1#u32 /- [demo::use_mul2_add1]: Source: 'tests/src/demo.rs', lines 19:0-19:43 -/ @@ -34,13 +34,13 @@ def use_mul2_add1 (x : U32) (y : U32) : Result U32 := /- [demo::incr]: Source: 'tests/src/demo.rs', lines 23:0-23:31 -/ def incr (x : U32) : Result U32 := - x + 1u32 + x + 1#u32 /- [demo::use_incr]: Source: 'tests/src/demo.rs', lines 27:0-27:17 -/ def use_incr : Result Unit := do - let x ← incr 0u32 + let x ← incr 0#u32 let x1 ← incr x let _ ← incr x1 Result.ok () @@ -56,10 +56,10 @@ inductive CList (T : Type) := divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T := match l with | CList.CCons x tl => - if i = 0u32 + if i = 0#u32 then Result.ok x else do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 list_nth T tl i1 | CList.CNil => Result.fail .panic @@ -71,13 +71,13 @@ divergent def list_nth_mut := match l with | CList.CCons x tl => - if i = 0u32 + if i = 0#u32 then let back := fun ret => Result.ok (CList.CCons ret tl) Result.ok (x, back) else do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 let (t, list_nth_mut_back) ← list_nth_mut T tl i1 let back := fun ret => @@ -95,13 +95,13 @@ divergent def list_nth_mut1_loop := match l with | CList.CCons x tl => - if i = 0u32 + if i = 0#u32 then let back := fun ret => Result.ok (CList.CCons ret tl) Result.ok (x, back) else do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 let (t, back) ← list_nth_mut1_loop T tl i1 let back1 := fun ret => do @@ -121,12 +121,12 @@ def list_nth_mut1 /- [demo::i32_id]: Source: 'tests/src/demo.rs', lines 82:0-82:28 -/ divergent def i32_id (i : I32) : Result I32 := - if i = 0i32 - then Result.ok 0i32 + if i = 0#i32 + then Result.ok 0#i32 else do - let i1 ← i - 1i32 + let i1 ← i - 1#i32 let i2 ← i32_id i1 - i2 + 1i32 + i2 + 1#i32 /- [demo::list_tail]: Source: 'tests/src/demo.rs', lines 90:0-90:64 -/ @@ -155,7 +155,7 @@ structure Counter (Self : Type) where Source: 'tests/src/demo.rs', lines 104:4-104:31 -/ def CounterUsize.incr (self : Usize) : Result (Usize × Usize) := do - let self1 ← self + 1usize + let self1 ← self + 1#usize Result.ok (self, self1) /- Trait implementation: [demo::{(demo::Counter for usize)}] diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean index c828720a..1b1d5cdf 100644 --- a/tests/lean/External/Funs.lean +++ b/tests/lean/External/Funs.lean @@ -27,7 +27,7 @@ def incr := do let (st1, (i, get_mut_back)) ← core.cell.Cell.get_mut U32 rc st - let i1 ← i + 1u32 + let i1 ← i + 1#u32 let (_, rc1) ← get_mut_back i1 st1 Result.ok (st1, rc1) diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean index 3c244ee0..612e1848 100644 --- a/tests/lean/Hashmap/Funs.lean +++ b/tests/lean/Hashmap/Funs.lean @@ -18,11 +18,11 @@ divergent def HashMap.allocate_slots_loop (T : Type) (slots : alloc.vec.Vec (List T)) (n : Usize) : Result (alloc.vec.Vec (List T)) := - if n > 0usize + if n > 0#usize then do let slots1 ← alloc.vec.Vec.push (List T) slots List.Nil - let n1 ← n - 1usize + let n1 ← n - 1#usize HashMap.allocate_slots_loop T slots1 n1 else Result.ok slots @@ -47,7 +47,7 @@ def HashMap.new_with_capacity let i1 ← i / max_load_divisor Result.ok { - num_entries := 0usize, + num_entries := 0#usize, max_load_factor := (max_load_dividend, max_load_divisor), max_load := i1, slots := slots @@ -56,7 +56,7 @@ def HashMap.new_with_capacity /- [hashmap::{hashmap::HashMap}::new]: Source: 'tests/src/hashmap.rs', lines 85:4-85:24 -/ def HashMap.new (T : Type) : Result (HashMap T) := - HashMap.new_with_capacity T 32usize 4usize 5usize + HashMap.new_with_capacity T 32#usize 4#usize 5#usize /- [hashmap::{hashmap::HashMap}::clear]: loop 0: Source: 'tests/src/hashmap.rs', lines 90:4-98:5 -/ @@ -71,7 +71,7 @@ divergent def HashMap.clear_loop let (_, index_mut_back) ← alloc.vec.Vec.index_mut (List T) Usize (core.slice.index.SliceIndexUsizeSliceTInst (List T)) slots i - let i2 ← i + 1usize + let i2 ← i + 1#usize let slots1 ← index_mut_back List.Nil HashMap.clear_loop T slots1 i2 else Result.ok slots @@ -80,8 +80,8 @@ divergent def HashMap.clear_loop Source: 'tests/src/hashmap.rs', lines 90:4-90:27 -/ def HashMap.clear (T : Type) (self : HashMap T) : Result (HashMap T) := do - let hm ← HashMap.clear_loop T self.slots 0usize - Result.ok { self with num_entries := 0usize, slots := hm } + let hm ← HashMap.clear_loop T self.slots 0#usize + Result.ok { self with num_entries := 0#usize, slots := hm } /- [hashmap::{hashmap::HashMap}::len]: Source: 'tests/src/hashmap.rs', lines 100:4-100:30 -/ @@ -129,7 +129,7 @@ def HashMap.insert_no_resize if inserted then do - let i1 ← self.num_entries + 1usize + let i1 ← self.num_entries + 1#usize let v ← index_mut_back l1 Result.ok { self with num_entries := i1, slots := v } else do @@ -169,7 +169,7 @@ divergent def HashMap.move_elements_loop (core.slice.index.SliceIndexUsizeSliceTInst (List T)) slots i let (ls, l1) := core.mem.replace (List T) l List.Nil let ntable1 ← HashMap.move_elements_from_list T ntable ls - let i2 ← i + 1usize + let i2 ← i + 1#usize let slots1 ← index_mut_back l1 HashMap.move_elements_loop T ntable1 slots1 i2 else Result.ok (ntable, slots) @@ -189,15 +189,15 @@ def HashMap.try_resize (T : Type) (self : HashMap T) : Result (HashMap T) := do let max_usize ← Scalar.cast .Usize core_u32_max let capacity := alloc.vec.Vec.len (List T) self.slots - let n1 ← max_usize / 2usize + let n1 ← max_usize / 2#usize let (i, i1) := self.max_load_factor let i2 ← n1 / i if capacity <= i2 then do - let i3 ← capacity * 2usize + let i3 ← capacity * 2#usize let ntable ← HashMap.new_with_capacity T i3 i i1 - let p ← HashMap.move_elements T ntable self.slots 0usize + let p ← HashMap.move_elements T ntable self.slots 0#usize let (ntable1, _) := p Result.ok { @@ -377,7 +377,7 @@ def HashMap.remove Result.ok (none, { self with slots := v }) | some x1 => do - let i1 ← self.num_entries - 1usize + let i1 ← self.num_entries - 1#usize let v ← index_mut_back l1 Result.ok (some x1, { self with num_entries := i1, slots := v }) @@ -395,37 +395,37 @@ def insert_on_disk def test1 : Result Unit := do let hm ← HashMap.new U64 - let hm1 ← HashMap.insert U64 hm 0usize 42u64 - let hm2 ← HashMap.insert U64 hm1 128usize 18u64 - let hm3 ← HashMap.insert U64 hm2 1024usize 138u64 - let hm4 ← HashMap.insert U64 hm3 1056usize 256u64 - let i ← HashMap.get U64 hm4 128usize - if i = 18u64 + let hm1 ← HashMap.insert U64 hm 0#usize 42#u64 + let hm2 ← HashMap.insert U64 hm1 128#usize 18#u64 + let hm3 ← HashMap.insert U64 hm2 1024#usize 138#u64 + let hm4 ← HashMap.insert U64 hm3 1056#usize 256#u64 + let i ← HashMap.get U64 hm4 128#usize + if i = 18#u64 then do - let (_, get_mut_back) ← HashMap.get_mut U64 hm4 1024usize - let hm5 ← get_mut_back 56u64 - let i1 ← HashMap.get U64 hm5 1024usize - if i1 = 56u64 + let (_, get_mut_back) ← HashMap.get_mut U64 hm4 1024#usize + let hm5 ← get_mut_back 56#u64 + let i1 ← HashMap.get U64 hm5 1024#usize + if i1 = 56#u64 then do - let (x, hm6) ← HashMap.remove U64 hm5 1024usize + let (x, hm6) ← HashMap.remove U64 hm5 1024#usize match x with | none => Result.fail .panic | some x1 => - if x1 = 56u64 + if x1 = 56#u64 then do - let i2 ← HashMap.get U64 hm6 0usize - if i2 = 42u64 + let i2 ← HashMap.get U64 hm6 0#usize + if i2 = 42#u64 then do - let i3 ← HashMap.get U64 hm6 128usize - if i3 = 18u64 + let i3 ← HashMap.get U64 hm6 128#usize + if i3 = 18#u64 then do - let i4 ← HashMap.get U64 hm6 1056usize - if i4 = 256u64 + let i4 ← HashMap.get U64 hm6 1056#usize + if i4 = 256#u64 then Result.ok () else Result.fail .panic else Result.fail .panic diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean index 567d2b44..199605d5 100644 --- a/tests/lean/Loops.lean +++ b/tests/lean/Loops.lean @@ -11,14 +11,14 @@ divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 := if i < max then do let s1 ← s + i - let i1 ← i + 1u32 + let i1 ← i + 1#u32 sum_loop max i1 s1 - else s * 2u32 + else s * 2#u32 /- [loops::sum]: Source: 'tests/src/loops.rs', lines 8:0-8:27 -/ def sum (max : U32) : Result U32 := - sum_loop max 0u32 0u32 + sum_loop max 0#u32 0#u32 /- [loops::sum_with_mut_borrows]: loop 0: Source: 'tests/src/loops.rs', lines 23:0-35:1 -/ @@ -28,14 +28,14 @@ divergent def sum_with_mut_borrows_loop then do let ms ← s + i - let mi ← i + 1u32 + let mi ← i + 1#u32 sum_with_mut_borrows_loop max mi ms - else s * 2u32 + else s * 2#u32 /- [loops::sum_with_mut_borrows]: Source: 'tests/src/loops.rs', lines 23:0-23:44 -/ def sum_with_mut_borrows (max : U32) : Result U32 := - sum_with_mut_borrows_loop max 0u32 0u32 + sum_with_mut_borrows_loop max 0#u32 0#u32 /- [loops::sum_with_shared_borrows]: loop 0: Source: 'tests/src/loops.rs', lines 38:0-52:1 -/ @@ -44,15 +44,15 @@ divergent def sum_with_shared_borrows_loop if i < max then do - let i1 ← i + 1u32 + let i1 ← i + 1#u32 let s1 ← s + i1 sum_with_shared_borrows_loop max i1 s1 - else s * 2u32 + else s * 2#u32 /- [loops::sum_with_shared_borrows]: Source: 'tests/src/loops.rs', lines 38:0-38:47 -/ def sum_with_shared_borrows (max : U32) : Result U32 := - sum_with_shared_borrows_loop max 0u32 0u32 + sum_with_shared_borrows_loop max 0#u32 0#u32 /- [loops::sum_array]: loop 0: Source: 'tests/src/loops.rs', lines 54:0-62:1 -/ @@ -63,14 +63,14 @@ divergent def sum_array_loop do let i1 ← Array.index_usize U32 N a i let s1 ← s + i1 - let i2 ← i + 1usize + let i2 ← i + 1#usize sum_array_loop N a i2 s1 else Result.ok s /- [loops::sum_array]: Source: 'tests/src/loops.rs', lines 54:0-54:52 -/ def sum_array (N : Usize) (a : Array U32 N) : Result U32 := - sum_array_loop N a 0usize 0u32 + sum_array_loop N a 0#usize 0#u32 /- [loops::clear]: loop 0: Source: 'tests/src/loops.rs', lines 66:0-72:1 -/ @@ -83,15 +83,15 @@ divergent def clear_loop let (_, index_mut_back) ← alloc.vec.Vec.index_mut U32 Usize (core.slice.index.SliceIndexUsizeSliceTInst U32) v i - let i2 ← i + 1usize - let v1 ← index_mut_back 0u32 + let i2 ← i + 1#usize + let v1 ← index_mut_back 0#u32 clear_loop v1 i2 else Result.ok v /- [loops::clear]: Source: 'tests/src/loops.rs', lines 66:0-66:30 -/ def clear (v : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) := - clear_loop v 0usize + clear_loop v 0#usize /- [loops::List] Source: 'tests/src/loops.rs', lines 74:0-74:16 -/ @@ -119,13 +119,13 @@ divergent def list_nth_mut_loop_loop (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) := match ls with | List.Cons x tl => - if i = 0u32 + if i = 0#u32 then let back := fun ret => Result.ok (List.Cons ret tl) Result.ok (x, back) else do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 let (t, back) ← list_nth_mut_loop_loop T tl i1 let back1 := fun ret => do @@ -146,10 +146,10 @@ divergent def list_nth_shared_loop_loop (T : Type) (ls : List T) (i : U32) : Result T := match ls with | List.Cons x tl => - if i = 0u32 + if i = 0#u32 then Result.ok x else do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 list_nth_shared_loop_loop T tl i1 | List.Nil => Result.fail .panic @@ -189,7 +189,7 @@ def get_elem_mut do let (ls, index_mut_back) ← alloc.vec.Vec.index_mut (List Usize) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0usize + (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize let (i, back) ← get_elem_mut_loop x ls let back1 := fun ret => do let l ← back ret @@ -213,7 +213,7 @@ def get_elem_shared do let ls ← alloc.vec.Vec.index (List Usize) Usize - (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0usize + (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize get_elem_shared_loop x ls /- [loops::id_mut]: @@ -235,13 +235,13 @@ divergent def list_nth_mut_loop_with_id_loop (T : Type) (i : U32) (ls : List T) : Result (T × (T → Result (List T))) := match ls with | List.Cons x tl => - if i = 0u32 + if i = 0#u32 then let back := fun ret => Result.ok (List.Cons ret tl) Result.ok (x, back) else do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 let (t, back) ← list_nth_mut_loop_with_id_loop T i1 tl let back1 := fun ret => do @@ -268,10 +268,10 @@ divergent def list_nth_shared_loop_with_id_loop (T : Type) (i : U32) (ls : List T) : Result T := match ls with | List.Cons x tl => - if i = 0u32 + if i = 0#u32 then Result.ok x else do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 list_nth_shared_loop_with_id_loop T i1 tl | List.Nil => Result.fail .panic @@ -293,14 +293,14 @@ divergent def list_nth_mut_loop_pair_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = 0u32 + if i = 0#u32 then 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 - 1u32 + let i1 ← i - 1#u32 let (p, back'a, back'b) ← list_nth_mut_loop_pair_loop T tl0 tl1 i1 let back'a1 := fun ret => do @@ -330,10 +330,10 @@ divergent def list_nth_shared_loop_pair_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = 0u32 + if i = 0#u32 then Result.ok (x0, x1) else do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 list_nth_shared_loop_pair_loop T tl0 tl1 i1 | List.Nil => Result.fail .panic | List.Nil => Result.fail .panic @@ -354,7 +354,7 @@ divergent def list_nth_mut_loop_pair_merge_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = 0u32 + if i = 0#u32 then let back := fun ret => @@ -363,7 +363,7 @@ divergent def list_nth_mut_loop_pair_merge_loop Result.ok ((x0, x1), back) else do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 let (p, back) ← list_nth_mut_loop_pair_merge_loop T tl0 tl1 i1 let back1 := fun ret => @@ -390,11 +390,11 @@ divergent def list_nth_shared_loop_pair_merge_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = 0u32 + if i = 0#u32 then Result.ok (x0, x1) else do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 list_nth_shared_loop_pair_merge_loop T tl0 tl1 i1 | List.Nil => Result.fail .panic | List.Nil => Result.fail .panic @@ -415,13 +415,13 @@ divergent def list_nth_mut_shared_loop_pair_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = 0u32 + if i = 0#u32 then let back := fun ret => Result.ok (List.Cons ret tl0) Result.ok ((x0, x1), back) else do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 let (p, back) ← list_nth_mut_shared_loop_pair_loop T tl0 tl1 i1 let back1 := fun ret => do @@ -449,13 +449,13 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = 0u32 + if i = 0#u32 then let back := fun ret => Result.ok (List.Cons ret tl0) Result.ok ((x0, x1), back) else do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 let (p, back) ← list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i1 let back1 := fun ret => do @@ -483,13 +483,13 @@ divergent def list_nth_shared_mut_loop_pair_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = 0u32 + if i = 0#u32 then let back := fun ret => Result.ok (List.Cons ret tl1) Result.ok ((x0, x1), back) else do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 let (p, back) ← list_nth_shared_mut_loop_pair_loop T tl0 tl1 i1 let back1 := fun ret => do @@ -517,13 +517,13 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop | List.Cons x0 tl0 => match ls1 with | List.Cons x1 tl1 => - if i = 0u32 + if i = 0#u32 then let back := fun ret => Result.ok (List.Cons ret tl1) Result.ok ((x0, x1), back) else do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 let (p, back) ← list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i1 let back1 := fun ret => do @@ -544,9 +544,9 @@ def list_nth_shared_mut_loop_pair_merge /- [loops::ignore_input_mut_borrow]: loop 0: Source: 'tests/src/loops.rs', lines 349:0-353:1 -/ divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit := - if i > 0u32 + if i > 0#u32 then do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 ignore_input_mut_borrow_loop i1 else Result.ok () @@ -560,9 +560,9 @@ def ignore_input_mut_borrow (_a : U32) (i : U32) : Result U32 := /- [loops::incr_ignore_input_mut_borrow]: loop 0: Source: 'tests/src/loops.rs', lines 357:0-362:1 -/ divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit := - if i > 0u32 + if i > 0#u32 then do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 incr_ignore_input_mut_borrow_loop i1 else Result.ok () @@ -570,16 +570,16 @@ divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit := Source: 'tests/src/loops.rs', lines 357:0-357:60 -/ def incr_ignore_input_mut_borrow (a : U32) (i : U32) : Result U32 := do - let a1 ← a + 1u32 + let a1 ← a + 1#u32 let _ ← incr_ignore_input_mut_borrow_loop i Result.ok a1 /- [loops::ignore_input_shared_borrow]: loop 0: Source: 'tests/src/loops.rs', lines 366:0-370:1 -/ divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit := - if i > 0u32 + if i > 0#u32 then do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 ignore_input_shared_borrow_loop i1 else Result.ok () diff --git a/tests/lean/Matches.lean b/tests/lean/Matches.lean index 34f899b1..3e3a558b 100644 --- a/tests/lean/Matches.lean +++ b/tests/lean/Matches.lean @@ -9,8 +9,8 @@ namespace matches Source: 'tests/src/matches.rs', lines 4:0-4:27 -/ def match_u32 (x : U32) : Result U32 := match x with - | 0u32 => Result.ok 0u32 - | 1u32 => Result.ok 1u32 - | _ => Result.ok 2u32 + | 0#u32 => Result.ok 0#u32 + | 1#u32 => Result.ok 1#u32 + | _ => Result.ok 2#u32 end matches diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean index 01f6736c..f0438050 100644 --- a/tests/lean/NoNestedBorrows.lean +++ b/tests/lean/NoNestedBorrows.lean @@ -62,7 +62,7 @@ def cast_bool_to_bool (x : Bool) : Result Bool := Source: 'tests/src/no_nested_borrows.rs', lines 63:0-63:14 -/ def test2 : Result Unit := do - let _ ← 23u32 + 44u32 + let _ ← 23#u32 + 44#u32 Result.ok () /- Unit test for [no_nested_borrows::test2] -/ @@ -79,10 +79,10 @@ def get_max (x : U32) (y : U32) : Result U32 := Source: 'tests/src/no_nested_borrows.rs', lines 83:0-83:14 -/ def test3 : Result Unit := do - let x ← get_max 4u32 3u32 - let y ← get_max 10u32 11u32 + let x ← get_max 4#u32 3#u32 + let y ← get_max 10#u32 11#u32 let z ← x + y - if z = 15u32 + if z = 15#u32 then Result.ok () else Result.fail .panic @@ -93,8 +93,8 @@ def test3 : Result Unit := Source: 'tests/src/no_nested_borrows.rs', lines 90:0-90:18 -/ def test_neg1 : Result Unit := do - let y ← -. 3i32 - if y = (-3)i32 + let y ← -. 3#i32 + if y = (-3)#i32 then Result.ok () else Result.fail .panic @@ -104,7 +104,7 @@ def test_neg1 : Result Unit := /- [no_nested_borrows::refs_test1]: Source: 'tests/src/no_nested_borrows.rs', lines 97:0-97:19 -/ def refs_test1 : Result Unit := - if 1i32 = 1i32 + if 1#i32 = 1#i32 then Result.ok () else Result.fail .panic @@ -114,12 +114,12 @@ def refs_test1 : Result Unit := /- [no_nested_borrows::refs_test2]: Source: 'tests/src/no_nested_borrows.rs', lines 108:0-108:19 -/ def refs_test2 : Result Unit := - if 2i32 = 2i32 + if 2#i32 = 2#i32 then - if 0i32 = 0i32 + if 0#i32 = 0#i32 then - if 2i32 = 2i32 - then if 2i32 = 2i32 + if 2#i32 = 2#i32 + then if 2#i32 = 2#i32 then Result.ok () else Result.fail .panic else Result.fail .panic @@ -141,10 +141,10 @@ def test_list1 : Result Unit := Source: 'tests/src/no_nested_borrows.rs', lines 129:0-129:18 -/ def test_box1 : Result Unit := do - let (_, deref_mut_back) ← alloc.boxed.Box.deref_mut I32 0i32 - let b ← deref_mut_back 1i32 + let (_, deref_mut_back) ← alloc.boxed.Box.deref_mut I32 0#i32 + let b ← deref_mut_back 1#i32 let x ← alloc.boxed.Box.deref I32 b - if x = 1i32 + if x = 1#i32 then Result.ok () else Result.fail .panic @@ -174,8 +174,8 @@ def test_panic (b : Bool) : Result Unit := Source: 'tests/src/no_nested_borrows.rs', lines 160:0-160:22 -/ def test_copy_int : Result Unit := do - let y ← copy_int 0i32 - if 0i32 = y + let y ← copy_int 0#i32 + if 0#i32 = y then Result.ok () else Result.fail .panic @@ -193,7 +193,7 @@ def is_cons (T : Type) (l : List T) : Result Bool := Source: 'tests/src/no_nested_borrows.rs', lines 174:0-174:21 -/ def test_is_cons : Result Unit := do - let b ← is_cons I32 (List.Cons 0i32 List.Nil) + let b ← is_cons I32 (List.Cons 0#i32 List.Nil) if b then Result.ok () else Result.fail .panic @@ -212,9 +212,9 @@ def split_list (T : Type) (l : List T) : Result (T × (List T)) := Source: 'tests/src/no_nested_borrows.rs', lines 188:0-188:24 -/ def test_split_list : Result Unit := do - let p ← split_list I32 (List.Cons 0i32 List.Nil) + let p ← split_list I32 (List.Cons 0#i32 List.Nil) let (hd, _) := p - if hd = 0i32 + if hd = 0#i32 then Result.ok () else Result.fail .panic @@ -237,14 +237,14 @@ def choose Source: 'tests/src/no_nested_borrows.rs', lines 203:0-203:20 -/ def choose_test : Result Unit := do - let (z, choose_back) ← choose I32 true 0i32 0i32 - let z1 ← z + 1i32 - if z1 = 1i32 + let (z, choose_back) ← choose I32 true 0#i32 0#i32 + let z1 ← z + 1#i32 + if z1 = 1#i32 then do let (x, y) ← choose_back z1 - if x = 1i32 - then if y = 0i32 + if x = 1#i32 + then if y = 0#i32 then Result.ok () else Result.fail .panic else Result.fail .panic @@ -285,18 +285,18 @@ divergent def list_length (T : Type) (l : List T) : Result U32 := match l with | List.Cons _ l1 => do let i ← list_length T l1 - 1u32 + i - | List.Nil => Result.ok 0u32 + 1#u32 + i + | List.Nil => Result.ok 0#u32 /- [no_nested_borrows::list_nth_shared]: Source: 'tests/src/no_nested_borrows.rs', lines 273:0-273:62 -/ divergent def list_nth_shared (T : Type) (l : List T) (i : U32) : Result T := match l with | List.Cons x tl => - if i = 0u32 + if i = 0#u32 then Result.ok x else do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 list_nth_shared T tl i1 | List.Nil => Result.fail .panic @@ -306,13 +306,13 @@ divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result (T × (T → Result (List T))) := match l with | List.Cons x tl => - if i = 0u32 + if i = 0#u32 then let back := fun ret => Result.ok (List.Cons ret tl) Result.ok (x, back) else do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 let (t, list_nth_mut_back) ← list_nth_mut T tl i1 let back := fun ret => @@ -340,37 +340,37 @@ def list_rev (T : Type) (l : List T) : Result (List T) := Source: 'tests/src/no_nested_borrows.rs', lines 324:0-324:28 -/ def test_list_functions : Result Unit := do - let l := List.Cons 2i32 List.Nil - let l1 := List.Cons 1i32 l - let i ← list_length I32 (List.Cons 0i32 l1) - if i = 3u32 + let l := List.Cons 2#i32 List.Nil + let l1 := List.Cons 1#i32 l + let i ← list_length I32 (List.Cons 0#i32 l1) + if i = 3#u32 then do - let i1 ← list_nth_shared I32 (List.Cons 0i32 l1) 0u32 - if i1 = 0i32 + let i1 ← list_nth_shared I32 (List.Cons 0#i32 l1) 0#u32 + if i1 = 0#i32 then do - let i2 ← list_nth_shared I32 (List.Cons 0i32 l1) 1u32 - if i2 = 1i32 + let i2 ← list_nth_shared I32 (List.Cons 0#i32 l1) 1#u32 + if i2 = 1#i32 then do - let i3 ← list_nth_shared I32 (List.Cons 0i32 l1) 2u32 - if i3 = 2i32 + let i3 ← list_nth_shared I32 (List.Cons 0#i32 l1) 2#u32 + if i3 = 2#i32 then do let (_, list_nth_mut_back) ← - list_nth_mut I32 (List.Cons 0i32 l1) 1u32 - let ls ← list_nth_mut_back 3i32 - let i4 ← list_nth_shared I32 ls 0u32 - if i4 = 0i32 + list_nth_mut I32 (List.Cons 0#i32 l1) 1#u32 + let ls ← list_nth_mut_back 3#i32 + let i4 ← list_nth_shared I32 ls 0#u32 + if i4 = 0#i32 then do - let i5 ← list_nth_shared I32 ls 1u32 - if i5 = 3i32 + let i5 ← list_nth_shared I32 ls 1#u32 + if i5 = 3#i32 then do - let i6 ← list_nth_shared I32 ls 2u32 - if i6 = 2i32 + let i6 ← list_nth_shared I32 ls 2#u32 + if i6 = 2#i32 then Result.ok () else Result.fail .panic else Result.fail .panic @@ -425,17 +425,17 @@ structure StructWithTuple (T1 T2 : Type) where /- [no_nested_borrows::new_tuple1]: Source: 'tests/src/no_nested_borrows.rs', lines 363:0-363:48 -/ def new_tuple1 : Result (StructWithTuple U32 U32) := - Result.ok { p := (1u32, 2u32) } + Result.ok { p := (1#u32, 2#u32) } /- [no_nested_borrows::new_tuple2]: Source: 'tests/src/no_nested_borrows.rs', lines 367:0-367:48 -/ def new_tuple2 : Result (StructWithTuple I16 I16) := - Result.ok { p := (1i16, 2i16) } + Result.ok { p := (1#i16, 2#i16) } /- [no_nested_borrows::new_tuple3]: Source: 'tests/src/no_nested_borrows.rs', lines 371:0-371:48 -/ def new_tuple3 : Result (StructWithTuple U64 I64) := - Result.ok { p := (1u64, 2i64) } + Result.ok { p := (1#u64, 2#i64) } /- [no_nested_borrows::StructWithPair] Source: 'tests/src/no_nested_borrows.rs', lines 376:0-376:33 -/ @@ -445,7 +445,7 @@ structure StructWithPair (T1 T2 : Type) where /- [no_nested_borrows::new_pair1]: Source: 'tests/src/no_nested_borrows.rs', lines 380:0-380:46 -/ def new_pair1 : Result (StructWithPair U32 U32) := - Result.ok { p := { x := 1u32, y := 2u32 } } + Result.ok { p := { x := 1#u32, y := 2#u32 } } /- [no_nested_borrows::test_constants]: Source: 'tests/src/no_nested_borrows.rs', lines 388:0-388:23 -/ @@ -453,21 +453,21 @@ def test_constants : Result Unit := do let swt ← new_tuple1 let (i, _) := swt.p - if i = 1u32 + if i = 1#u32 then do let swt1 ← new_tuple2 let (i1, _) := swt1.p - if i1 = 1i16 + if i1 = 1#i16 then do let swt2 ← new_tuple3 let (i2, _) := swt2.p - if i2 = 1u64 + if i2 = 1#u64 then do let swp ← new_pair1 - if swp.p.x = 1u32 + if swp.p.x = 1#u32 then Result.ok () else Result.fail .panic else Result.fail .panic @@ -488,39 +488,39 @@ def test_weird_borrows1 : Result Unit := /- [no_nested_borrows::test_mem_replace]: Source: 'tests/src/no_nested_borrows.rs', lines 407:0-407:37 -/ def test_mem_replace (px : U32) : Result U32 := - let (y, _) := core.mem.replace U32 px 1u32 - if y = 0u32 - then Result.ok 2u32 + let (y, _) := core.mem.replace U32 px 1#u32 + if y = 0#u32 + then Result.ok 2#u32 else Result.fail .panic /- [no_nested_borrows::test_shared_borrow_bool1]: Source: 'tests/src/no_nested_borrows.rs', lines 414:0-414:47 -/ def test_shared_borrow_bool1 (b : Bool) : Result U32 := if b - then Result.ok 0u32 - else Result.ok 1u32 + then Result.ok 0#u32 + else Result.ok 1#u32 /- [no_nested_borrows::test_shared_borrow_bool2]: Source: 'tests/src/no_nested_borrows.rs', lines 427:0-427:40 -/ def test_shared_borrow_bool2 : Result U32 := - Result.ok 0u32 + Result.ok 0#u32 /- [no_nested_borrows::test_shared_borrow_enum1]: Source: 'tests/src/no_nested_borrows.rs', lines 442:0-442:52 -/ def test_shared_borrow_enum1 (l : List U32) : Result U32 := match l with - | List.Cons _ _ => Result.ok 1u32 - | List.Nil => Result.ok 0u32 + | List.Cons _ _ => Result.ok 1#u32 + | List.Nil => Result.ok 0#u32 /- [no_nested_borrows::test_shared_borrow_enum2]: Source: 'tests/src/no_nested_borrows.rs', lines 454:0-454:40 -/ def test_shared_borrow_enum2 : Result U32 := - Result.ok 0u32 + Result.ok 0#u32 /- [no_nested_borrows::incr]: Source: 'tests/src/no_nested_borrows.rs', lines 465:0-465:24 -/ def incr (x : U32) : Result U32 := - x + 1u32 + x + 1#u32 /- [no_nested_borrows::call_incr]: Source: 'tests/src/no_nested_borrows.rs', lines 469:0-469:35 -/ @@ -531,7 +531,7 @@ def call_incr (x : U32) : Result U32 := Source: 'tests/src/no_nested_borrows.rs', lines 474:0-474:41 -/ def read_then_incr (x : U32) : Result (U32 × U32) := do - let x1 ← x + 1u32 + let x1 ← x + 1#u32 Result.ok (x, x1) /- [no_nested_borrows::Tuple] @@ -548,7 +548,7 @@ def read_tuple (x : (U32 × U32)) : Result U32 := Source: 'tests/src/no_nested_borrows.rs', lines 486:0-486:39 -/ def update_tuple (x : (U32 × U32)) : Result (U32 × U32) := let (_, i) := x - Result.ok (1u32, i) + Result.ok (1#u32, i) /- [no_nested_borrows::read_tuple_struct]: Source: 'tests/src/no_nested_borrows.rs', lines 490:0-490:52 -/ @@ -560,7 +560,7 @@ def read_tuple_struct (x : Tuple U32 U32) : Result U32 := Source: 'tests/src/no_nested_borrows.rs', lines 494:0-494:51 -/ def update_tuple_struct (x : Tuple U32 U32) : Result (Tuple U32 U32) := let (_, i) := x - Result.ok (1u32, i) + Result.ok (1#u32, i) /- [no_nested_borrows::create_tuple_struct]: Source: 'tests/src/no_nested_borrows.rs', lines 498:0-498:61 -/ diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean index 400406f1..03b96903 100644 --- a/tests/lean/Paper.lean +++ b/tests/lean/Paper.lean @@ -8,14 +8,14 @@ namespace paper /- [paper::ref_incr]: Source: 'tests/src/paper.rs', lines 7:0-7:28 -/ def ref_incr (x : I32) : Result I32 := - x + 1i32 + x + 1#i32 /- [paper::test_incr]: Source: 'tests/src/paper.rs', lines 11:0-11:18 -/ def test_incr : Result Unit := do - let x ← ref_incr 0i32 - if x = 1i32 + let x ← ref_incr 0#i32 + if x = 1#i32 then Result.ok () else Result.fail .panic @@ -38,14 +38,14 @@ def choose Source: 'tests/src/paper.rs', lines 26:0-26:20 -/ def test_choose : Result Unit := do - let (z, choose_back) ← choose I32 true 0i32 0i32 - let z1 ← z + 1i32 - if z1 = 1i32 + let (z, choose_back) ← choose I32 true 0#i32 0#i32 + let z1 ← z + 1#i32 + if z1 = 1#i32 then do let (x, y) ← choose_back z1 - if x = 1i32 - then if y = 0i32 + if x = 1#i32 + then if y = 0#i32 then Result.ok () else Result.fail .panic else Result.fail .panic @@ -66,13 +66,13 @@ divergent def list_nth_mut (T : Type) (l : List T) (i : U32) : Result (T × (T → Result (List T))) := match l with | List.Cons x tl => - if i = 0u32 + if i = 0#u32 then let back := fun ret => Result.ok (List.Cons ret tl) Result.ok (x, back) else do - let i1 ← i - 1u32 + let i1 ← i - 1#u32 let (t, list_nth_mut_back) ← list_nth_mut T tl i1 let back := fun ret => @@ -89,19 +89,19 @@ divergent def sum (l : List I32) : Result I32 := | List.Cons x tl => do let i ← sum tl x + i - | List.Nil => Result.ok 0i32 + | List.Nil => Result.ok 0#i32 /- [paper::test_nth]: Source: 'tests/src/paper.rs', lines 71:0-71:17 -/ def test_nth : Result Unit := do - let l := List.Cons 3i32 List.Nil - let l1 := List.Cons 2i32 l - let (x, list_nth_mut_back) ← list_nth_mut I32 (List.Cons 1i32 l1) 2u32 - let x1 ← x + 1i32 + let l := List.Cons 3#i32 List.Nil + let l1 := List.Cons 2#i32 l + let (x, list_nth_mut_back) ← list_nth_mut I32 (List.Cons 1#i32 l1) 2#u32 + let x1 ← x + 1#i32 let l2 ← list_nth_mut_back x1 let i ← sum l2 - if i = 7i32 + if i = 7#i32 then Result.ok () else Result.fail .panic @@ -114,7 +114,7 @@ def call_choose (p : (U32 × U32)) : Result U32 := do let (px, py) := p let (pz, choose_back) ← choose U32 true px py - let pz1 ← pz + 1u32 + let pz1 ← pz + 1#u32 let (px1, _) ← choose_back pz1 Result.ok px1 diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index 1cd8644b..0dd692fe 100644 --- a/tests/lean/Traits.lean +++ b/tests/lean/Traits.lean @@ -148,7 +148,7 @@ structure ToType (Self T : Type) where /- [traits::{(traits::ToType for u64)#5}::to_type]: Source: 'tests/src/traits.rs', lines 94:4-94:28 -/ def ToTypeU64Bool.to_type (self : U64) : Result Bool := - Result.ok (self > 0u64) + Result.ok (self > 0#u64) /- Trait implementation: [traits::{(traits::ToType for u64)#5}] Source: 'tests/src/traits.rs', lines 93:0-93:25 -/ @@ -202,7 +202,7 @@ structure TestType.test.TestTrait (Self : Type) where Source: 'tests/src/traits.rs', lines 140:12-140:34 -/ def TestType.test.TestTraittraitsTestTypetestTestType1.test (self : TestType.test.TestType1) : Result Bool := - Result.ok (self > 1u64) + Result.ok (self > 1#u64) /- Trait implementation: [traits::{traits::TestType#6}::test::{(traits::{traits::TestType#6}::test::TestTrait for traits::{traits::TestType#6}::test::TestType1)}] Source: 'tests/src/traits.rs', lines 139:8-139:36 -/ @@ -217,8 +217,8 @@ def TestType.test (T : Type) (ToU64Inst : ToU64 T) (self : TestType T) (x : T) : Result Bool := do let x1 ← ToU64Inst.to_u64 x - if x1 > 0u64 - then TestType.test.TestTraittraitsTestTypetestTestType1.test 0u64 + if x1 > 0#u64 + then TestType.test.TestTraittraitsTestTypetestTestType1.test 0#u64 else Result.ok false /- [traits::BoolWrapper] @@ -243,7 +243,7 @@ def ToTypetraitsBoolWrapperT (T : Type) (ToTypeBoolTInst : ToType Bool T) : /- [traits::WithConstTy::LEN2] Source: 'tests/src/traits.rs', lines 165:4-165:21 -/ def WithConstTy.LEN2_default_body (Self : Type) (LEN : Usize) : Result Usize := - Result.ok 32usize + Result.ok 32#usize def WithConstTy.LEN2_default (Self : Type) (LEN : Usize) : Usize := eval_global (WithConstTy.LEN2_default_body Self LEN) @@ -259,19 +259,19 @@ structure WithConstTy (Self : Type) (LEN : Usize) where /- [traits::{(traits::WithConstTy<32: usize> for bool)#8}::LEN1] Source: 'tests/src/traits.rs', lines 176:4-176:21 -/ -def WithConstTyBool32.LEN1_body : Result Usize := Result.ok 12usize +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: 'tests/src/traits.rs', lines 181:4-181:39 -/ -def WithConstTyBool32.f (i : U64) (a : Array U8 32usize) : Result U64 := +def WithConstTyBool32.f (i : U64) (a : Array U8 32#usize) : Result U64 := Result.ok i /- Trait implementation: [traits::{(traits::WithConstTy<32: usize> for bool)#8}] Source: 'tests/src/traits.rs', lines 175:0-175:29 -/ -def WithConstTyBool32 : WithConstTy Bool 32usize := { +def WithConstTyBool32 : WithConstTy Bool 32#usize := { LEN1 := WithConstTyBool32.LEN1 - LEN2 := WithConstTy.LEN2_default Bool 32usize + LEN2 := WithConstTy.LEN2_default Bool 32#usize V := U8 W := U64 W_clause_0 := ToU64U64 @@ -312,7 +312,7 @@ def test_where1 (T : Type) (_x : T) : Result Unit := /- [traits::test_where2]: Source: 'tests/src/traits.rs', lines 195:0-195:57 -/ def test_where2 - (T : Type) (WithConstTyT32Inst : WithConstTy T 32usize) (_x : U32) : + (T : Type) (WithConstTyT32Inst : WithConstTy T 32#usize) (_x : U32) : Result Unit := Result.ok () @@ -489,7 +489,7 @@ def TraitArray (T : Type) (N : Usize) : Trait (Array T N) := { Source: 'tests/src/traits.rs', lines 320:4-320:20 -/ def TraittraitsWrapper.LEN_body (T : Type) (TraitInst : Trait T) : Result Usize := - Result.ok 0usize + Result.ok 0#usize def TraittraitsWrapper.LEN (T : Type) (TraitInst : Trait T) : Usize := eval_global (TraittraitsWrapper.LEN_body T TraitInst) @@ -522,7 +522,7 @@ inductive core.result.Result (T E : Type) := Source: 'tests/src/traits.rs', lines 333:4-333:33 -/ def Foo.FOO_body (T U : Type) (TraitInst : Trait T) : Result (core.result.Result T I32) := - Result.ok (core.result.Result.Err 0i32) + 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) -- cgit v1.2.3 From 19abb19134efe0b16409f955b13af36262f231a8 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 12 Jun 2024 18:40:27 +0200 Subject: Update the code extraction and regenerate the tests --- tests/lean/Matches.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tests') diff --git a/tests/lean/Matches.lean b/tests/lean/Matches.lean index 3e3a558b..9233841b 100644 --- a/tests/lean/Matches.lean +++ b/tests/lean/Matches.lean @@ -9,8 +9,8 @@ namespace matches Source: 'tests/src/matches.rs', lines 4:0-4:27 -/ def match_u32 (x : U32) : Result U32 := match x with - | 0#u32 => Result.ok 0#u32 - | 1#u32 => Result.ok 1#u32 + | 0#scalar => Result.ok 0#u32 + | 1#scalar => Result.ok 1#u32 | _ => Result.ok 2#u32 end matches -- cgit v1.2.3 From d5cf75a0f8209298ad85f46249f14d5c3a24faf6 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 13 Jun 2024 22:37:18 +0200 Subject: Update the tests --- tests/lean/Hashmap/Properties.lean | 30 +++++++++++++++--------------- tests/lean/lake-manifest.json | 26 +++++++++++++------------- tests/lean/lean-toolchain | 2 +- 3 files changed, 29 insertions(+), 29 deletions(-) (limited to 'tests') diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index fcaf5806..5be778e7 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -137,15 +137,16 @@ theorem insert_in_list_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) ( distinct_keys l1.v ∧ -- We need this auxiliary property to prove that the keys distinct properties is preserved (∀ k, k ≠ key → l0.v.allP (λ (k1, _) => k ≠ k1) → l1.v.allP (λ (k1, _) => k ≠ k1)) - := - match l0 with - | .Nil => by + := by + cases l0 with + | Nil => exists true -- TODO: why do we need to do this? + simp [insert_in_list] + rw [insert_in_list_loop] simp (config := {contextual := true}) - [insert_in_list, insert_in_list_loop, - List.v, slot_s_inv_hash, distinct_keys, List.pairwise_rel] - | .Cons k v tl0 => - if h: k = key then by + [List.v, slot_s_inv_hash, distinct_keys, List.pairwise_rel] + | Cons k v tl0 => + if h: k = key then rw [insert_in_list] rw [insert_in_list_loop] simp [h] @@ -157,21 +158,21 @@ theorem insert_in_list_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) ( . simp [*, distinct_keys] at * apply hdk . tauto - else by + else rw [insert_in_list] rw [insert_in_list_loop] simp [h] - have : slot_s_inv_hash l (hash_mod_key key l) (List.v tl0) := by checkpoint + have : slot_s_inv_hash l (hash_mod_key key l) (List.v tl0) := by simp_all [List.v, slot_s_inv_hash] - have : distinct_keys (List.v tl0) := by checkpoint + have : distinct_keys (List.v tl0) := by simp [distinct_keys] at hdk simp [hdk, distinct_keys] progress keep heq as ⟨ b, tl1 .. ⟩ simp only [insert_in_list] at heq - have : slot_s_inv_hash l (hash_mod_key key l) (List.v (List.Cons k v tl1)) := by checkpoint + have : slot_s_inv_hash l (hash_mod_key key l) (List.v (List.Cons k v tl1)) := by simp [List.v, slot_s_inv_hash] at * simp [*] - have : distinct_keys ((k, v) :: List.v tl1) := by checkpoint + have : distinct_keys ((k, v) :: List.v tl1) := by simp [distinct_keys] at * simp [*] -- TODO: canonize addition by default? @@ -231,7 +232,6 @@ def mk_opaque {α : Sort u} (x : α) : { y : α // y = x} := --set_option trace.profiler true -- For pretty printing (useful when copy-pasting goals) -attribute [pp_dot] List.length -- use the dot notation when printing set_option pp.coercions false -- do not print coercions with ↑ (this doesn't parse) -- The proof below is a bit expensive, so we need to increase the maximum number @@ -305,7 +305,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value -- zeta reduction? For now I have to do this peculiar manipulation have ⟨ nhm, nhm_eq ⟩ := @mk_opaque (HashMap α) { num_entries := i0, max_load_factor := hm.max_load_factor, max_load := hm.max_load, slots := v } exists nhm - have hupdt : lookup nhm key = some value := by checkpoint + have hupdt : lookup nhm key = some value := by simp [lookup, List.lookup] at * simp_all have hlkp : ∀ k, ¬ k = key → nhm.lookup k = hm.lookup k := by @@ -340,7 +340,7 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value have _ : match hm.lookup key with | none => nhm.len_s = hm.len_s + 1 - | some _ => nhm.len_s = hm.len_s := by checkpoint + | some _ => nhm.len_s = hm.len_s := by simp only [lookup, List.lookup, len_s, al_v, HashMap.v, slots_t_lookup] at * -- We have to do a case disjunction simp_all diff --git a/tests/lean/lake-manifest.json b/tests/lean/lake-manifest.json index 404d3dab..b1c3c9dc 100644 --- a/tests/lean/lake-manifest.json +++ b/tests/lean/lake-manifest.json @@ -1,11 +1,11 @@ -{"version": 7, +{"version": "1.0.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/std4", + [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "32983874c1b897d78f20d620fe92fc8fd3f06c3a", - "name": "std", + "rev": "f96a34401de084c73c787ecb45b85d4fb47bb981", + "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, @@ -13,7 +13,7 @@ {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, - "rev": "64365c656d5e1bffa127d2a1795f471529ee0178", + "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -22,25 +22,25 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79", + "rev": "7e3bd939c6badfcb1e607c0fddb509548baafd05", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, - "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8", + "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.30", + "inputRev": "v0.0.36", "inherited": true, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/lean4-cli", "type": "git", "subDir": null, - "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5", + "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29", "name": "Cli", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -49,16 +49,16 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662", + "rev": "7983e959f8f4a79313215720de3ef1eca2d6d474", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", "inherited": true, - "configFile": "lakefile.lean"}, + "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "d9c412b8103b5098bf8b66cbb981b81a57375925", + "rev": "c9f95f42b82684937a26ba395ebf7f25a81734ca", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/tests/lean/lean-toolchain b/tests/lean/lean-toolchain index 9ad30404..0ba3faf8 100644 --- a/tests/lean/lean-toolchain +++ b/tests/lean/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.7.0 +leanprover/lean4:v4.9.0-rc1 -- cgit v1.2.3 From adf5c77214cf1cfe14a386f3feefdfa1ebfd1d45 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Fri, 14 Jun 2024 14:09:51 +0200 Subject: Update the tests --- tests/lean/lake-manifest.json | 6 +++--- tests/lean/lean-toolchain | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'tests') diff --git a/tests/lean/lake-manifest.json b/tests/lean/lake-manifest.json index b1c3c9dc..904f10ad 100644 --- a/tests/lean/lake-manifest.json +++ b/tests/lean/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "f96a34401de084c73c787ecb45b85d4fb47bb981", + "rev": "15d42e1a92a80d0db5ca1c12123866ba392b9d76", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "7e3bd939c6badfcb1e607c0fddb509548baafd05", + "rev": "3e1025b53ab7a8c8e6b82a72eccf2b109f09349e", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -58,7 +58,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "c9f95f42b82684937a26ba395ebf7f25a81734ca", + "rev": "c14e9d00a51390cda9a094386b41bfb70d78570e", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, diff --git a/tests/lean/lean-toolchain b/tests/lean/lean-toolchain index 0ba3faf8..29c0cea4 100644 --- a/tests/lean/lean-toolchain +++ b/tests/lean/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.9.0-rc1 +leanprover/lean4:v4.9.0-rc2 -- cgit v1.2.3 From 85098d7caf5e3196c2e8f92411efd2814bfed1ea Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 17 Jun 2024 06:14:06 +0200 Subject: Update the Lean dependencies --- tests/lean/lake-manifest.json | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'tests') diff --git a/tests/lean/lake-manifest.json b/tests/lean/lake-manifest.json index 904f10ad..94b2f080 100644 --- a/tests/lean/lake-manifest.json +++ b/tests/lean/lake-manifest.json @@ -4,7 +4,7 @@ [{"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "15d42e1a92a80d0db5ca1c12123866ba392b9d76", + "rev": "47e4cc5c5800c07d9bf232173c9941fa5bf68589", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -22,7 +22,7 @@ {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, - "rev": "3e1025b53ab7a8c8e6b82a72eccf2b109f09349e", + "rev": "882561b77bd2aaa98bd8665a56821062bdb3034c", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -49,7 +49,7 @@ {"url": "https://github.com/leanprover-community/import-graph.git", "type": "git", "subDir": null, - "rev": "7983e959f8f4a79313215720de3ef1eca2d6d474", + "rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -58,7 +58,7 @@ {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, - "rev": "c14e9d00a51390cda9a094386b41bfb70d78570e", + "rev": "77e1ea0a339a4663eced9cacc3a46eb45f967b51", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, -- cgit v1.2.3