path: root/tests/lean/Loops.lean

-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [loops]
import Base
open Primitives

namespace loops

/- [loops::sum]: loop 0:
   Source: 'tests/src/loops.rs', lines 7:0-17:1 -/
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
       sum_loop max i1 s1
  else s * 2#u32

/- [loops::sum]:
   Source: 'tests/src/loops.rs', lines 7:0-7: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 22:0-34:1 -/
divergent def sum_with_mut_borrows_loop
  (max : U32) (i : U32) (s : U32) : Result U32 :=
  if i < max
  then
    do
    let ms ← s + i
    let mi ← i + 1#u32
    sum_with_mut_borrows_loop max mi ms
  else s * 2#u32

/- [loops::sum_with_mut_borrows]:
   Source: 'tests/src/loops.rs', lines 22:0-22: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 37:0-51:1 -/
divergent def sum_with_shared_borrows_loop
  (max : U32) (i : U32) (s : U32) : Result U32 :=
  if i < max
  then
    do
    let i1 ← i + 1#u32
    let s1 ← s + i1
    sum_with_shared_borrows_loop max i1 s1
  else s * 2#u32

/- [loops::sum_with_shared_borrows]:
   Source: 'tests/src/loops.rs', lines 37:0-37: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 53:0-61:1 -/
divergent def sum_array_loop
  (N : Usize) (a : Array U32 N) (i : Usize) (s : U32) : Result U32 :=
  if i < N
  then
    do
    let i1 ← Array.index_usize U32 N a i
    let s1 ← s + i1
    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 53:0-53: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 65:0-71: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
  if i < i1
  then
    do
    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
    clear_loop v1 i2
  else Result.ok v

/- [loops::clear]:
   Source: 'tests/src/loops.rs', lines 65:0-65: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 73:0-73: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 79:0-88:1 -/
divergent def list_mem_loop (x : U32) (ls : List U32) : Result Bool :=
  match ls with
  | List.Cons y tl => if y = x
                      then Result.ok true
                      else list_mem_loop x tl
  | List.Nil => Result.ok false

/- [loops::list_mem]:
   Source: 'tests/src/loops.rs', lines 79:0-79: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 91:0-101:1 -/
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
    then
      let back := fun ret => Result.ok (List.Cons ret tl)
      Result.ok (x, back)
    else
      do
      let i1 ← i - 1#u32
      let (t, back) ← list_nth_mut_loop_loop T tl i1
      let back1 :=
        fun ret => do
                   let tl1 ← back ret
                   Result.ok (List.Cons x tl1)
      Result.ok (t, back1)
  | List.Nil => Result.fail .panic

/- [loops::list_nth_mut_loop]:
   Source: 'tests/src/loops.rs', lines 91:0-91: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 104:0-114:1 -/
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
    then Result.ok x
    else do
         let i1 ← i - 1#u32
         list_nth_shared_loop_loop T tl i1
  | List.Nil => Result.fail .panic

/- [loops::list_nth_shared_loop]:
   Source: 'tests/src/loops.rs', lines 104:0-104: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 116:0-130:1 -/
divergent def get_elem_mut_loop
  (x : Usize) (ls : List Usize) :
  Result (Usize × (Usize → Result (List Usize)))
  :=
  match ls with
  | List.Cons y tl =>
    if y = x
    then
      let back := fun ret => Result.ok (List.Cons ret tl)
      Result.ok (y, back)
    else
      do
      let (i, back) ← get_elem_mut_loop x tl
      let back1 :=
        fun ret => do
                   let tl1 ← back ret
                   Result.ok (List.Cons y tl1)
      Result.ok (i, back1)
  | List.Nil => Result.fail .panic

/- [loops::get_elem_mut]:
   Source: 'tests/src/loops.rs', lines 116:0-116:73 -/
def get_elem_mut
  (slots : alloc.vec.Vec (List Usize)) (x : Usize) :
  Result (Usize × (Usize → Result (alloc.vec.Vec (List Usize))))
  :=
  do
  let (ls, index_mut_back) ←
    alloc.vec.Vec.index_mut (List Usize) Usize
      (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
                          index_mut_back l
  Result.ok (i, back1)

/- [loops::get_elem_shared]: loop 0:
   Source: 'tests/src/loops.rs', lines 132:0-146:1 -/
divergent def get_elem_shared_loop
  (x : Usize) (ls : List Usize) : Result Usize :=
  match ls with
  | List.Cons y tl => if y = x
                      then Result.ok y
                      else get_elem_shared_loop x tl
  | List.Nil => Result.fail .panic

/- [loops::get_elem_shared]:
   Source: 'tests/src/loops.rs', lines 132:0-132:68 -/
def get_elem_shared
  (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize :=
  do
  let ls ←
    alloc.vec.Vec.index (List Usize) Usize
      (core.slice.index.SliceIndexUsizeSliceTInst (List Usize)) slots 0#usize
  get_elem_shared_loop x ls

/- [loops::id_mut]:
   Source: 'tests/src/loops.rs', lines 148:0-148:50 -/
def id_mut
  (T : Type) (ls : List T) :
  Result ((List T) × (List T → Result (List T)))
  :=
  Result.ok (ls, Result.ok)

/- [loops::id_shared]:
   Source: 'tests/src/loops.rs', lines 152:0-152: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 157:0-168: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
  | List.Cons x tl =>
    if i = 0#u32
    then
      let back := fun ret => Result.ok (List.Cons ret tl)
      Result.ok (x, back)
    else
      do
      let i1 ← i - 1#u32
      let (t, back) ← list_nth_mut_loop_with_id_loop T i1 tl
      let back1 :=
        fun ret => do
                   let tl1 ← back ret
                   Result.ok (List.Cons x tl1)
      Result.ok (t, back1)
  | List.Nil => Result.fail .panic

/- [loops::list_nth_mut_loop_with_id]:
   Source: 'tests/src/loops.rs', lines 157:0-157:75 -/
def list_nth_mut_loop_with_id
  (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
  do
  let (ls1, id_mut_back) ← id_mut T ls
  let (t, back) ← list_nth_mut_loop_with_id_loop T i ls1
  let back1 := fun ret => do
                          let l ← back ret
                          id_mut_back l
  Result.ok (t, back1)

/- [loops::list_nth_shared_loop_with_id]: loop 0:
   Source: 'tests/src/loops.rs', lines 171:0-182:1 -/
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
    then Result.ok x
    else do
         let i1 ← i - 1#u32
         list_nth_shared_loop_with_id_loop T i1 tl
  | List.Nil => Result.fail .panic

/- [loops::list_nth_shared_loop_with_id]:
   Source: 'tests/src/loops.rs', lines 171:0-171:70 -/
def list_nth_shared_loop_with_id
  (T : Type) (ls : List T) (i : U32) : Result T :=
  do
  let ls1 ← id_shared T ls
  list_nth_shared_loop_with_id_loop T i ls1

/- [loops::list_nth_mut_loop_pair]: loop 0:
   Source: 'tests/src/loops.rs', lines 187:0-208: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)))
  :=
  match ls0 with
  | List.Cons x0 tl0 =>
    match ls1 with
    | List.Cons x1 tl1 =>
      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 - 1#u32
        let (p, back'a, back'b) ← list_nth_mut_loop_pair_loop T tl0 tl1 i1
        let back'a1 :=
          fun ret => do
                     let tl01 ← back'a ret
                     Result.ok (List.Cons x0 tl01)
        let back'b1 :=
          fun ret => do
                     let tl11 ← back'b ret
                     Result.ok (List.Cons x1 tl11)
        Result.ok (p, back'a1, back'b1)
    | List.Nil => Result.fail .panic
  | List.Nil => Result.fail .panic

/- [loops::list_nth_mut_loop_pair]:
   Source: 'tests/src/loops.rs', lines 187:0-191: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)))
  :=
  list_nth_mut_loop_pair_loop T ls0 ls1 i

/- [loops::list_nth_shared_loop_pair]: loop 0:
   Source: 'tests/src/loops.rs', lines 211:0-232: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
  | List.Cons x0 tl0 =>
    match ls1 with
    | List.Cons x1 tl1 =>
      if i = 0#u32
      then Result.ok (x0, x1)
      else do
           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

/- [loops::list_nth_shared_loop_pair]:
   Source: 'tests/src/loops.rs', lines 211:0-215: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 236:0-251: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))))
  :=
  match ls0 with
  | List.Cons x0 tl0 =>
    match ls1 with
    | List.Cons x1 tl1 =>
      if i = 0#u32
      then
        let back :=
          fun ret =>
            let (t, t1) := ret
            Result.ok (List.Cons t tl0, List.Cons t1 tl1)
        Result.ok ((x0, x1), back)
      else
        do
        let i1 ← i - 1#u32
        let (p, back) ← list_nth_mut_loop_pair_merge_loop T tl0 tl1 i1
        let back1 :=
          fun ret =>
            do
            let (tl01, tl11) ← back ret
            Result.ok (List.Cons x0 tl01, List.Cons x1 tl11)
        Result.ok (p, back1)
    | List.Nil => Result.fail .panic
  | List.Nil => Result.fail .panic

/- [loops::list_nth_mut_loop_pair_merge]:
   Source: 'tests/src/loops.rs', lines 236:0-240: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))))
  :=
  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 254:0-269: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
  | List.Cons x0 tl0 =>
    match ls1 with
    | List.Cons x1 tl1 =>
      if i = 0#u32
      then Result.ok (x0, x1)
      else
        do
        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

/- [loops::list_nth_shared_loop_pair_merge]:
   Source: 'tests/src/loops.rs', lines 254:0-258: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 272:0-287: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)))
  :=
  match ls0 with
  | List.Cons x0 tl0 =>
    match ls1 with
    | List.Cons x1 tl1 =>
      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 - 1#u32
        let (p, back) ← list_nth_mut_shared_loop_pair_loop T tl0 tl1 i1
        let back1 :=
          fun ret => do
                     let tl01 ← back ret
                     Result.ok (List.Cons x0 tl01)
        Result.ok (p, back1)
    | List.Nil => Result.fail .panic
  | List.Nil => Result.fail .panic

/- [loops::list_nth_mut_shared_loop_pair]:
   Source: 'tests/src/loops.rs', lines 272:0-276: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)))
  :=
  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 291:0-306: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)))
  :=
  match ls0 with
  | List.Cons x0 tl0 =>
    match ls1 with
    | List.Cons x1 tl1 =>
      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 - 1#u32
        let (p, back) ← list_nth_mut_shared_loop_pair_merge_loop T tl0 tl1 i1
        let back1 :=
          fun ret => do
                     let tl01 ← back ret
                     Result.ok (List.Cons x0 tl01)
        Result.ok (p, back1)
    | List.Nil => Result.fail .panic
  | List.Nil => Result.fail .panic

/- [loops::list_nth_mut_shared_loop_pair_merge]:
   Source: 'tests/src/loops.rs', lines 291:0-295: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)))
  :=
  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 310:0-325: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)))
  :=
  match ls0 with
  | List.Cons x0 tl0 =>
    match ls1 with
    | List.Cons x1 tl1 =>
      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 - 1#u32
        let (p, back) ← list_nth_shared_mut_loop_pair_loop T tl0 tl1 i1
        let back1 :=
          fun ret => do
                     let tl11 ← back ret
                     Result.ok (List.Cons x1 tl11)
        Result.ok (p, back1)
    | List.Nil => Result.fail .panic
  | List.Nil => Result.fail .panic

/- [loops::list_nth_shared_mut_loop_pair]:
   Source: 'tests/src/loops.rs', lines 310:0-314: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)))
  :=
  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 329:0-344: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)))
  :=
  match ls0 with
  | List.Cons x0 tl0 =>
    match ls1 with
    | List.Cons x1 tl1 =>
      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 - 1#u32
        let (p, back) ← list_nth_shared_mut_loop_pair_merge_loop T tl0 tl1 i1
        let back1 :=
          fun ret => do
                     let tl11 ← back ret
                     Result.ok (List.Cons x1 tl11)
        Result.ok (p, back1)
    | List.Nil => Result.fail .panic
  | List.Nil => Result.fail .panic

/- [loops::list_nth_shared_mut_loop_pair_merge]:
   Source: 'tests/src/loops.rs', lines 329:0-333: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)))
  :=
  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 348:0-352:1 -/
divergent def ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
  if i > 0#u32
  then do
       let i1 ← i - 1#u32
       ignore_input_mut_borrow_loop i1
  else Result.ok ()

/- [loops::ignore_input_mut_borrow]:
   Source: 'tests/src/loops.rs', lines 348:0-348: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 356:0-361:1 -/
divergent def incr_ignore_input_mut_borrow_loop (i : U32) : Result Unit :=
  if i > 0#u32
  then do
       let i1 ← i - 1#u32
       incr_ignore_input_mut_borrow_loop i1
  else Result.ok ()

/- [loops::incr_ignore_input_mut_borrow]:
   Source: 'tests/src/loops.rs', lines 356:0-356:60 -/
def incr_ignore_input_mut_borrow (a : U32) (i : U32) : Result U32 :=
  do
  let a1 ← a + 1#u32
  let _ ← incr_ignore_input_mut_borrow_loop i
  Result.ok a1

/- [loops::ignore_input_shared_borrow]: loop 0:
   Source: 'tests/src/loops.rs', lines 365:0-369:1 -/
divergent def ignore_input_shared_borrow_loop (i : U32) : Result Unit :=
  if i > 0#u32
  then do
       let i1 ← i - 1#u32
       ignore_input_shared_borrow_loop i1
  else Result.ok ()

/- [loops::ignore_input_shared_borrow]:
   Source: 'tests/src/loops.rs', lines 365:0-365:59 -/
def ignore_input_shared_borrow (_a : U32) (i : U32) : Result U32 :=
  do
  let _ ← ignore_input_shared_borrow_loop i
  Result.ok _a

end loops