summaryrefslogtreecommitdiff
path: root/tests/lean/Loops.lean
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/Loops.lean')
-rw-r--r--tests/lean/Loops.lean98
1 files changed, 49 insertions, 49 deletions
diff --git a/tests/lean/Loops.lean b/tests/lean/Loops.lean
index d5bda6ab..199605d5 100644
--- a/tests/lean/Loops.lean
+++ b/tests/lean/Loops.lean
@@ -6,7 +6,7 @@ open Primitives
namespace loops
/- [loops::sum]: loop 0:
- Source: 'tests/src/loops.rs', lines 4:0-14:1 -/
+ Source: 'tests/src/loops.rs', lines 8:0-18:1 -/
divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 :=
if i < max
then do
@@ -16,12 +16,12 @@ divergent def sum_loop (max : U32) (i : U32) (s : U32) : Result U32 :=
else s * 2#u32
/- [loops::sum]:
- Source: 'tests/src/loops.rs', lines 4:0-4:27 -/
+ Source: 'tests/src/loops.rs', lines 8:0-8:27 -/
def sum (max : U32) : Result U32 :=
sum_loop max 0#u32 0#u32
/- [loops::sum_with_mut_borrows]: loop 0:
- Source: 'tests/src/loops.rs', lines 19:0-31:1 -/
+ Source: 'tests/src/loops.rs', lines 23:0-35:1 -/
divergent def sum_with_mut_borrows_loop
(max : U32) (i : U32) (s : U32) : Result U32 :=
if i < max
@@ -33,12 +33,12 @@ divergent def sum_with_mut_borrows_loop
else s * 2#u32
/- [loops::sum_with_mut_borrows]:
- Source: 'tests/src/loops.rs', lines 19:0-19:44 -/
+ 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
/- [loops::sum_with_shared_borrows]: loop 0:
- Source: 'tests/src/loops.rs', lines 34:0-48:1 -/
+ Source: 'tests/src/loops.rs', lines 38:0-52:1 -/
divergent def sum_with_shared_borrows_loop
(max : U32) (i : U32) (s : U32) : Result U32 :=
if i < max
@@ -50,12 +50,12 @@ divergent def sum_with_shared_borrows_loop
else s * 2#u32
/- [loops::sum_with_shared_borrows]:
- Source: 'tests/src/loops.rs', lines 34:0-34:47 -/
+ 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
/- [loops::sum_array]: loop 0:
- Source: 'tests/src/loops.rs', lines 50:0-58:1 -/
+ Source: 'tests/src/loops.rs', lines 54:0-62:1 -/
divergent def sum_array_loop
(N : Usize) (a : Array U32 N) (i : Usize) (s : U32) : Result U32 :=
if i < N
@@ -68,12 +68,12 @@ divergent def sum_array_loop
else Result.ok s
/- [loops::sum_array]:
- Source: 'tests/src/loops.rs', lines 50:0-50:52 -/
+ 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
/- [loops::clear]: loop 0:
- Source: 'tests/src/loops.rs', lines 62:0-68:1 -/
+ Source: 'tests/src/loops.rs', lines 66:0-72:1 -/
divergent def clear_loop
(v : alloc.vec.Vec U32) (i : Usize) : Result (alloc.vec.Vec U32) :=
let i1 := alloc.vec.Vec.len U32 v
@@ -89,18 +89,18 @@ divergent def clear_loop
else Result.ok v
/- [loops::clear]:
- Source: 'tests/src/loops.rs', lines 62:0-62:30 -/
+ 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
/- [loops::List]
- Source: 'tests/src/loops.rs', lines 70:0-70:16 -/
+ Source: 'tests/src/loops.rs', lines 74:0-74:16 -/
inductive List (T : Type) :=
| Cons : T → List T → List T
| Nil : List T
/- [loops::list_mem]: loop 0:
- Source: 'tests/src/loops.rs', lines 76:0-85:1 -/
+ Source: 'tests/src/loops.rs', lines 80:0-89:1 -/
divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool :=
match ls with
| List.Cons y tl => if y = x
@@ -109,12 +109,12 @@ divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool :=
| List.Nil => Result.ok false
/- [loops::list_mem]:
- Source: 'tests/src/loops.rs', lines 76:0-76:52 -/
+ Source: 'tests/src/loops.rs', lines 80:0-80:52 -/
def list_mem (x : U32) (ls : List U32) : Result Bool :=
list_mem_loop x ls
/- [loops::list_nth_mut_loop]: loop 0:
- Source: 'tests/src/loops.rs', lines 88:0-98:1 -/
+ Source: 'tests/src/loops.rs', lines 92:0-102:1 -/
divergent def list_nth_mut_loop_loop
(T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
match ls with
@@ -135,13 +135,13 @@ divergent def list_nth_mut_loop_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_mut_loop]:
- Source: 'tests/src/loops.rs', lines 88:0-88:71 -/
+ Source: 'tests/src/loops.rs', lines 92:0-92:71 -/
def list_nth_mut_loop
(T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
list_nth_mut_loop_loop T ls i
/- [loops::list_nth_shared_loop]: loop 0:
- Source: 'tests/src/loops.rs', lines 101:0-111:1 -/
+ Source: 'tests/src/loops.rs', lines 105:0-115:1 -/
divergent def list_nth_shared_loop_loop
(T : Type) (ls : List T) (i : U32) : Result T :=
match ls with
@@ -154,12 +154,12 @@ divergent def list_nth_shared_loop_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_shared_loop]:
- Source: 'tests/src/loops.rs', lines 101:0-101:66 -/
+ Source: 'tests/src/loops.rs', lines 105:0-105:66 -/
def list_nth_shared_loop (T : Type) (ls : List T) (i : U32) : Result T :=
list_nth_shared_loop_loop T ls i
/- [loops::get_elem_mut]: loop 0:
- Source: 'tests/src/loops.rs', lines 113:0-127:1 -/
+ Source: 'tests/src/loops.rs', lines 117:0-131:1 -/
divergent def get_elem_mut_loop
(x : Usize) (ls : List Usize) :
Result (Usize × (Usize → Result (List Usize)))
@@ -181,7 +181,7 @@ divergent def get_elem_mut_loop
| List.Nil => Result.fail .panic
/- [loops::get_elem_mut]:
- Source: 'tests/src/loops.rs', lines 113:0-113:73 -/
+ Source: 'tests/src/loops.rs', lines 117:0-117:73 -/
def get_elem_mut
(slots : alloc.vec.Vec (List Usize)) (x : Usize) :
Result (Usize × (Usize → Result (alloc.vec.Vec (List Usize))))
@@ -197,7 +197,7 @@ def get_elem_mut
Result.ok (i, back1)
/- [loops::get_elem_shared]: loop 0:
- Source: 'tests/src/loops.rs', lines 129:0-143:1 -/
+ Source: 'tests/src/loops.rs', lines 133:0-147:1 -/
divergent def get_elem_shared_loop
(x : Usize) (ls : List Usize) : Result Usize :=
match ls with
@@ -207,7 +207,7 @@ divergent def get_elem_shared_loop
| List.Nil => Result.fail .panic
/- [loops::get_elem_shared]:
- Source: 'tests/src/loops.rs', lines 129:0-129:68 -/
+ Source: 'tests/src/loops.rs', lines 133:0-133:68 -/
def get_elem_shared
(slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize :=
do
@@ -217,7 +217,7 @@ def get_elem_shared
get_elem_shared_loop x ls
/- [loops::id_mut]:
- Source: 'tests/src/loops.rs', lines 145:0-145:50 -/
+ Source: 'tests/src/loops.rs', lines 149:0-149:50 -/
def id_mut
(T : Type) (ls : List T) :
Result ((List T) × (List T → Result (List T)))
@@ -225,12 +225,12 @@ def id_mut
Result.ok (ls, Result.ok)
/- [loops::id_shared]:
- Source: 'tests/src/loops.rs', lines 149:0-149:45 -/
+ Source: 'tests/src/loops.rs', lines 153:0-153:45 -/
def id_shared (T : Type) (ls : List T) : Result (List T) :=
Result.ok ls
/- [loops::list_nth_mut_loop_with_id]: loop 0:
- Source: 'tests/src/loops.rs', lines 154:0-165:1 -/
+ Source: 'tests/src/loops.rs', lines 158:0-169:1 -/
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
@@ -251,7 +251,7 @@ divergent def list_nth_mut_loop_with_id_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_mut_loop_with_id]:
- Source: 'tests/src/loops.rs', lines 154:0-154:75 -/
+ Source: 'tests/src/loops.rs', lines 158:0-158:75 -/
def list_nth_mut_loop_with_id
(T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
do
@@ -263,7 +263,7 @@ def list_nth_mut_loop_with_id
Result.ok (t, back1)
/- [loops::list_nth_shared_loop_with_id]: loop 0:
- Source: 'tests/src/loops.rs', lines 168:0-179:1 -/
+ Source: 'tests/src/loops.rs', lines 172:0-183:1 -/
divergent def list_nth_shared_loop_with_id_loop
(T : Type) (i : U32) (ls : List T) : Result T :=
match ls with
@@ -276,7 +276,7 @@ divergent def list_nth_shared_loop_with_id_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_shared_loop_with_id]:
- Source: 'tests/src/loops.rs', lines 168:0-168:70 -/
+ Source: 'tests/src/loops.rs', lines 172:0-172:70 -/
def list_nth_shared_loop_with_id
(T : Type) (ls : List T) (i : U32) : Result T :=
do
@@ -284,7 +284,7 @@ def list_nth_shared_loop_with_id
list_nth_shared_loop_with_id_loop T i ls1
/- [loops::list_nth_mut_loop_pair]: loop 0:
- Source: 'tests/src/loops.rs', lines 184:0-205:1 -/
+ Source: 'tests/src/loops.rs', lines 188:0-209:1 -/
divergent def list_nth_mut_loop_pair_loop
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)) × (T → Result (List T)))
@@ -315,7 +315,7 @@ divergent def list_nth_mut_loop_pair_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_mut_loop_pair]:
- Source: 'tests/src/loops.rs', lines 184:0-188:27 -/
+ Source: 'tests/src/loops.rs', lines 188:0-192:27 -/
def list_nth_mut_loop_pair
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)) × (T → Result (List T)))
@@ -323,7 +323,7 @@ def list_nth_mut_loop_pair
list_nth_mut_loop_pair_loop T ls0 ls1 i
/- [loops::list_nth_shared_loop_pair]: loop 0:
- Source: 'tests/src/loops.rs', lines 208:0-229:1 -/
+ Source: 'tests/src/loops.rs', lines 212:0-233:1 -/
divergent def list_nth_shared_loop_pair_loop
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
match ls0 with
@@ -339,13 +339,13 @@ divergent def list_nth_shared_loop_pair_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_shared_loop_pair]:
- Source: 'tests/src/loops.rs', lines 208:0-212:19 -/
+ Source: 'tests/src/loops.rs', lines 212:0-216:19 -/
def list_nth_shared_loop_pair
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
list_nth_shared_loop_pair_loop T ls0 ls1 i
/- [loops::list_nth_mut_loop_pair_merge]: loop 0:
- Source: 'tests/src/loops.rs', lines 233:0-248:1 -/
+ Source: 'tests/src/loops.rs', lines 237:0-252:1 -/
divergent def list_nth_mut_loop_pair_merge_loop
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × ((T × T) → Result ((List T) × (List T))))
@@ -375,7 +375,7 @@ divergent def list_nth_mut_loop_pair_merge_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_mut_loop_pair_merge]:
- Source: 'tests/src/loops.rs', lines 233:0-237:27 -/
+ Source: 'tests/src/loops.rs', lines 237:0-241:27 -/
def list_nth_mut_loop_pair_merge
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × ((T × T) → Result ((List T) × (List T))))
@@ -383,7 +383,7 @@ def list_nth_mut_loop_pair_merge
list_nth_mut_loop_pair_merge_loop T ls0 ls1 i
/- [loops::list_nth_shared_loop_pair_merge]: loop 0:
- Source: 'tests/src/loops.rs', lines 251:0-266:1 -/
+ Source: 'tests/src/loops.rs', lines 255:0-270:1 -/
divergent def list_nth_shared_loop_pair_merge_loop
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
match ls0 with
@@ -400,13 +400,13 @@ divergent def list_nth_shared_loop_pair_merge_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_shared_loop_pair_merge]:
- Source: 'tests/src/loops.rs', lines 251:0-255:19 -/
+ Source: 'tests/src/loops.rs', lines 255:0-259:19 -/
def list_nth_shared_loop_pair_merge
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
list_nth_shared_loop_pair_merge_loop T ls0 ls1 i
/- [loops::list_nth_mut_shared_loop_pair]: loop 0:
- Source: 'tests/src/loops.rs', lines 269:0-284:1 -/
+ Source: 'tests/src/loops.rs', lines 273:0-288:1 -/
divergent def list_nth_mut_shared_loop_pair_loop
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)))
@@ -432,7 +432,7 @@ divergent def list_nth_mut_shared_loop_pair_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_mut_shared_loop_pair]:
- Source: 'tests/src/loops.rs', lines 269:0-273:23 -/
+ Source: 'tests/src/loops.rs', lines 273:0-277:23 -/
def list_nth_mut_shared_loop_pair
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)))
@@ -440,7 +440,7 @@ def list_nth_mut_shared_loop_pair
list_nth_mut_shared_loop_pair_loop T ls0 ls1 i
/- [loops::list_nth_mut_shared_loop_pair_merge]: loop 0:
- Source: 'tests/src/loops.rs', lines 288:0-303:1 -/
+ Source: 'tests/src/loops.rs', lines 292:0-307:1 -/
divergent def list_nth_mut_shared_loop_pair_merge_loop
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)))
@@ -466,7 +466,7 @@ divergent def list_nth_mut_shared_loop_pair_merge_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_mut_shared_loop_pair_merge]:
- Source: 'tests/src/loops.rs', lines 288:0-292:23 -/
+ Source: 'tests/src/loops.rs', lines 292:0-296:23 -/
def list_nth_mut_shared_loop_pair_merge
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)))
@@ -474,7 +474,7 @@ def list_nth_mut_shared_loop_pair_merge
list_nth_mut_shared_loop_pair_merge_loop T ls0 ls1 i
/- [loops::list_nth_shared_mut_loop_pair]: loop 0:
- Source: 'tests/src/loops.rs', lines 307:0-322:1 -/
+ Source: 'tests/src/loops.rs', lines 311:0-326:1 -/
divergent def list_nth_shared_mut_loop_pair_loop
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)))
@@ -500,7 +500,7 @@ divergent def list_nth_shared_mut_loop_pair_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_shared_mut_loop_pair]:
- Source: 'tests/src/loops.rs', lines 307:0-311:23 -/
+ Source: 'tests/src/loops.rs', lines 311:0-315:23 -/
def list_nth_shared_mut_loop_pair
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)))
@@ -508,7 +508,7 @@ def list_nth_shared_mut_loop_pair
list_nth_shared_mut_loop_pair_loop T ls0 ls1 i
/- [loops::list_nth_shared_mut_loop_pair_merge]: loop 0:
- Source: 'tests/src/loops.rs', lines 326:0-341:1 -/
+ Source: 'tests/src/loops.rs', lines 330:0-345:1 -/
divergent def list_nth_shared_mut_loop_pair_merge_loop
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)))
@@ -534,7 +534,7 @@ divergent def list_nth_shared_mut_loop_pair_merge_loop
| List.Nil => Result.fail .panic
/- [loops::list_nth_shared_mut_loop_pair_merge]:
- Source: 'tests/src/loops.rs', lines 326:0-330:23 -/
+ Source: 'tests/src/loops.rs', lines 330:0-334:23 -/
def list_nth_shared_mut_loop_pair_merge
(T : Type) (ls0 : List T) (ls1 : List T) (i : U32) :
Result ((T × T) × (T → Result (List T)))
@@ -542,7 +542,7 @@ def list_nth_shared_mut_loop_pair_merge
list_nth_shared_mut_loop_pair_merge_loop T ls0 ls1 i
/- [loops::ignore_input_mut_borrow]: loop 0:
- Source: 'tests/src/loops.rs', lines 345:0-349:1 -/
+ 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
then do
@@ -551,14 +551,14 @@ divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
else Result.ok ()
/- [loops::ignore_input_mut_borrow]:
- Source: 'tests/src/loops.rs', lines 345:0-345:56 -/
+ Source: 'tests/src/loops.rs', lines 349:0-349:56 -/
def ignore_input_mut_borrow (_a : U32) (i : U32) : Result U32 :=
do
let _ ← ignore_input_mut_borrow_loop i
Result.ok _a
/- [loops::incr_ignore_input_mut_borrow]: loop 0:
- Source: 'tests/src/loops.rs', lines 353:0-358:1 -/
+ 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
then do
@@ -567,7 +567,7 @@ divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
else Result.ok ()
/- [loops::incr_ignore_input_mut_borrow]:
- Source: 'tests/src/loops.rs', lines 353:0-353:60 -/
+ 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
@@ -575,7 +575,7 @@ def incr_ignore_input_mut_borrow (a : U32) (i : U32) : Result U32 :=
Result.ok a1
/- [loops::ignore_input_shared_borrow]: loop 0:
- Source: 'tests/src/loops.rs', lines 362:0-366:1 -/
+ 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
then do
@@ -584,7 +584,7 @@ divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit :=
else Result.ok ()
/- [loops::ignore_input_shared_borrow]:
- Source: 'tests/src/loops.rs', lines 362:0-362:59 -/
+ Source: 'tests/src/loops.rs', lines 366:0-366:59 -/
def ignore_input_shared_borrow (_a : U32) (i : U32) : Result U32 :=
do
let _ ← ignore_input_shared_borrow_loop i
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 04:44:48 +0000