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

namespace loops

/- [loops::sum]: loop 0:
   Source: 'tests/src/loops.rs', lines 4:0-14: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 4:0-4: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 -/
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 19:0-19: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 -/
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 34:0-34: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 -/
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 50:0-50:52 -/
def sum_array (N : Usize) (a : Array U32 N) : Result U32 :=
  sum_array_loop N a 0#usize 0#u32

/- [loops::clear]:
   Source: 'tests/src/loops.rs', lines 62:0-62:30 -/
def clear (v : alloc.vec.Vec U32) : Result (alloc.vec.Vec U32) :=
  sorry

/- [loops::List]
   Source: 'tests/src/loops.rs', lines 70:0-70:16 -/
inductive List (T : Type) :=
| Cons : T → List T → List T
| Nil : List T

/- [loops::list_mem]:
   Source: 'tests/src/loops.rs', lines 76:0-76:52 -/
def list_mem (x : U32) (ls : List U32) : Result Bool :=
  sorry

/- [loops::list_nth_mut_loop]:
   Source: 'tests/src/loops.rs', lines 88:0-88:71 -/
def list_nth_mut_loop
  (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
  sorry

/- [loops::list_nth_shared_loop]:
   Source: 'tests/src/loops.rs', lines 101:0-101:66 -/
def list_nth_shared_loop (T : Type) (ls : List T) (i : U32) : Result T :=
  sorry

/- [loops::get_elem_mut]:
   Source: 'tests/src/loops.rs', lines 113:0-113:73 -/
def get_elem_mut
  (slots : alloc.vec.Vec (List Usize)) (x : Usize) :
  Result (Usize × (Usize → Result (alloc.vec.Vec (List Usize))))
  :=
  sorry

/- [loops::get_elem_shared]:
   Source: 'tests/src/loops.rs', lines 129:0-129:68 -/
def get_elem_shared
  (slots : alloc.vec.Vec (List Usize)) (x : Usize) : Result Usize :=
  sorry

/- [loops::id_mut]:
   Source: 'tests/src/loops.rs', lines 145:0-145: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 149:0-149:45 -/
def id_shared (T : Type) (ls : List T) : Result (List T) :=
  Result.ok ls

/- [loops::list_nth_mut_loop_with_id]:
   Source: 'tests/src/loops.rs', lines 154:0-154:75 -/
def list_nth_mut_loop_with_id
  (T : Type) (ls : List T) (i : U32) : Result (T × (T → Result (List T))) :=
  sorry

/- [loops::list_nth_shared_loop_with_id]:
   Source: 'tests/src/loops.rs', lines 168:0-168:70 -/
def list_nth_shared_loop_with_id
  (T : Type) (ls : List T) (i : U32) : Result T :=
  sorry

/- [loops::list_nth_mut_loop_pair]:
   Source: 'tests/src/loops.rs', lines 184:0-188: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)))
  :=
  sorry

/- [loops::list_nth_shared_loop_pair]:
   Source: 'tests/src/loops.rs', lines 208:0-212:19 -/
def list_nth_shared_loop_pair
  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
  sorry

/- [loops::list_nth_mut_loop_pair_merge]:
   Source: 'tests/src/loops.rs', lines 233:0-237: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))))
  :=
  sorry

/- [loops::list_nth_shared_loop_pair_merge]:
   Source: 'tests/src/loops.rs', lines 251:0-255:19 -/
def list_nth_shared_loop_pair_merge
  (T : Type) (ls0 : List T) (ls1 : List T) (i : U32) : Result (T × T) :=
  sorry

/- [loops::list_nth_mut_shared_loop_pair]:
   Source: 'tests/src/loops.rs', lines 269:0-273: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)))
  :=
  sorry

/- [loops::list_nth_mut_shared_loop_pair_merge]:
   Source: 'tests/src/loops.rs', lines 288:0-292: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)))
  :=
  sorry

/- [loops::list_nth_shared_mut_loop_pair]:
   Source: 'tests/src/loops.rs', lines 307:0-311: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)))
  :=
  sorry

/- [loops::list_nth_shared_mut_loop_pair_merge]:
   Source: 'tests/src/loops.rs', lines 326:0-330: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)))
  :=
  sorry

/- [loops::ignore_input_mut_borrow]: loop 0:
   Source: 'tests/src/loops.rs', lines 345:0-349: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 345:0-345: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 -/
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 353:0-353: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 362:0-366: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 362:0-362: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