(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
(** [loops] *)
Require Import Primitives.
Import Primitives.
Require Import Coq.ZArith.ZArith.
Require Import List.
Import ListNotations.
Local Open Scope Primitives_scope.
Module Loops.

(** [loops::sum]: loop 0:
    Source: 'tests/src/loops.rs', lines 4:0-14:1 *)
Fixpoint sum_loop (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
  match n with
  | O => Fail_ OutOfFuel
  | S n1 =>
    if i s< max
    then (s1 <- u32_add s i; i1 <- u32_add i 1%u32; sum_loop n1 max i1 s1)
    else u32_mul s 2%u32
  end
.

(** [loops::sum]:
    Source: 'tests/src/loops.rs', lines 4:0-4:27 *)
Definition sum (n : nat) (max : u32) : result u32 :=
  sum_loop n max 0%u32 0%u32
.

(** [loops::sum_with_mut_borrows]: loop 0:
    Source: 'tests/src/loops.rs', lines 19:0-31:1 *)
Fixpoint sum_with_mut_borrows_loop
  (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
  match n with
  | O => Fail_ OutOfFuel
  | S n1 =>
    if i s< max
    then (
      ms <- u32_add s i;
      mi <- u32_add i 1%u32;
      sum_with_mut_borrows_loop n1 max mi ms)
    else u32_mul s 2%u32
  end
.

(** [loops::sum_with_mut_borrows]:
    Source: 'tests/src/loops.rs', lines 19:0-19:44 *)
Definition sum_with_mut_borrows (n : nat) (max : u32) : result u32 :=
  sum_with_mut_borrows_loop n max 0%u32 0%u32
.

(** [loops::sum_with_shared_borrows]: loop 0:
    Source: 'tests/src/loops.rs', lines 34:0-48:1 *)
Fixpoint sum_with_shared_borrows_loop
  (n : nat) (max : u32) (i : u32) (s : u32) : result u32 :=
  match n with
  | O => Fail_ OutOfFuel
  | S n1 =>
    if i s< max
    then (
      i1 <- u32_add i 1%u32;
      s1 <- u32_add s i1;
      sum_with_shared_borrows_loop n1 max i1 s1)
    else u32_mul s 2%u32
  end
.

(** [loops::sum_with_shared_borrows]:
    Source: 'tests/src/loops.rs', lines 34:0-34:47 *)
Definition sum_with_shared_borrows (n : nat) (max : u32) : result u32 :=
  sum_with_shared_borrows_loop n max 0%u32 0%u32
.

(** [loops::sum_array]: loop 0:
    Source: 'tests/src/loops.rs', lines 50:0-58:1 *)
Fixpoint sum_array_loop
  (N : usize) (n : nat) (a : array u32 N) (i : usize) (s : u32) : result u32 :=
  match n with
  | O => Fail_ OutOfFuel
  | S n1 =>
    if i s< N
    then (
      i1 <- array_index_usize u32 N a i;
      s1 <- u32_add s i1;
      i2 <- usize_add i 1%usize;
      sum_array_loop N n1 a i2 s1)
    else Ok s
  end
.

(** [loops::sum_array]:
    Source: 'tests/src/loops.rs', lines 50:0-50:52 *)
Definition sum_array (N : usize) (n : nat) (a : array u32 N) : result u32 :=
  sum_array_loop N n a 0%usize 0%u32
.

(** [loops::clear]:
    Source: 'tests/src/loops.rs', lines 62:0-62:30 *)
Definition clear
  (n : nat) (v : alloc_vec_Vec u32) : result (alloc_vec_Vec u32) :=
  admit
.

(** [loops::List]
    Source: 'tests/src/loops.rs', lines 70:0-70:16 *)
Inductive List_t (T : Type) :=
| List_Cons : T -> List_t T -> List_t T
| List_Nil : List_t T
.

Arguments List_Cons { _ }.
Arguments List_Nil { _ }.

(** [loops::list_mem]:
    Source: 'tests/src/loops.rs', lines 76:0-76:52 *)
Definition list_mem (n : nat) (x : u32) (ls : List_t u32) : result bool :=
  admit
.

(** [loops::list_nth_mut_loop]:
    Source: 'tests/src/loops.rs', lines 88:0-88:71 *)
Definition list_nth_mut_loop
  (T : Type) (n : nat) (ls : List_t T) (i : u32) :
  result (T * (T -> result (List_t T)))
  :=
  admit
.

(** [loops::list_nth_shared_loop]:
    Source: 'tests/src/loops.rs', lines 101:0-101:66 *)
Definition list_nth_shared_loop
  (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
  admit
.

(** [loops::get_elem_mut]:
    Source: 'tests/src/loops.rs', lines 113:0-113:73 *)
Definition get_elem_mut
  (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) :
  result (usize * (usize -> result (alloc_vec_Vec (List_t usize))))
  :=
  admit
.

(** [loops::get_elem_shared]:
    Source: 'tests/src/loops.rs', lines 129:0-129:68 *)
Definition get_elem_shared
  (n : nat) (slots : alloc_vec_Vec (List_t usize)) (x : usize) :
  result usize
  :=
  admit
.

(** [loops::id_mut]:
    Source: 'tests/src/loops.rs', lines 145:0-145:50 *)
Definition id_mut
  (T : Type) (ls : List_t T) :
  result ((List_t T) * (List_t T -> result (List_t T)))
  :=
  Ok (ls, Ok)
.

(** [loops::id_shared]:
    Source: 'tests/src/loops.rs', lines 149:0-149:45 *)
Definition id_shared (T : Type) (ls : List_t T) : result (List_t T) :=
  Ok ls.

(** [loops::list_nth_mut_loop_with_id]:
    Source: 'tests/src/loops.rs', lines 154:0-154:75 *)
Definition list_nth_mut_loop_with_id
  (T : Type) (n : nat) (ls : List_t T) (i : u32) :
  result (T * (T -> result (List_t T)))
  :=
  admit
.

(** [loops::list_nth_shared_loop_with_id]:
    Source: 'tests/src/loops.rs', lines 168:0-168:70 *)
Definition list_nth_shared_loop_with_id
  (T : Type) (n : nat) (ls : List_t T) (i : u32) : result T :=
  admit
.

(** [loops::list_nth_mut_loop_pair]:
    Source: 'tests/src/loops.rs', lines 184:0-188:27 *)
Definition list_nth_mut_loop_pair
  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
  result ((T * T) * (T -> result (List_t T)) * (T -> result (List_t T)))
  :=
  admit
.

(** [loops::list_nth_shared_loop_pair]:
    Source: 'tests/src/loops.rs', lines 208:0-212:19 *)
Definition list_nth_shared_loop_pair
  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
  result (T * T)
  :=
  admit
.

(** [loops::list_nth_mut_loop_pair_merge]:
    Source: 'tests/src/loops.rs', lines 233:0-237:27 *)
Definition list_nth_mut_loop_pair_merge
  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
  result ((T * T) * ((T * T) -> result ((List_t T) * (List_t T))))
  :=
  admit
.

(** [loops::list_nth_shared_loop_pair_merge]:
    Source: 'tests/src/loops.rs', lines 251:0-255:19 *)
Definition list_nth_shared_loop_pair_merge
  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
  result (T * T)
  :=
  admit
.

(** [loops::list_nth_mut_shared_loop_pair]:
    Source: 'tests/src/loops.rs', lines 269:0-273:23 *)
Definition list_nth_mut_shared_loop_pair
  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
  result ((T * T) * (T -> result (List_t T)))
  :=
  admit
.

(** [loops::list_nth_mut_shared_loop_pair_merge]:
    Source: 'tests/src/loops.rs', lines 288:0-292:23 *)
Definition list_nth_mut_shared_loop_pair_merge
  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
  result ((T * T) * (T -> result (List_t T)))
  :=
  admit
.

(** [loops::list_nth_shared_mut_loop_pair]:
    Source: 'tests/src/loops.rs', lines 307:0-311:23 *)
Definition list_nth_shared_mut_loop_pair
  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
  result ((T * T) * (T -> result (List_t T)))
  :=
  admit
.

(** [loops::list_nth_shared_mut_loop_pair_merge]:
    Source: 'tests/src/loops.rs', lines 326:0-330:23 *)
Definition list_nth_shared_mut_loop_pair_merge
  (T : Type) (n : nat) (ls0 : List_t T) (ls1 : List_t T) (i : u32) :
  result ((T * T) * (T -> result (List_t T)))
  :=
  admit
.

(** [loops::ignore_input_mut_borrow]: loop 0:
    Source: 'tests/src/loops.rs', lines 345:0-349:1 *)
Fixpoint ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
  match n with
  | O => Fail_ OutOfFuel
  | S n1 =>
    if i s> 0%u32
    then (i1 <- u32_sub i 1%u32; ignore_input_mut_borrow_loop n1 i1)
    else Ok tt
  end
.

(** [loops::ignore_input_mut_borrow]:
    Source: 'tests/src/loops.rs', lines 345:0-345:56 *)
Definition ignore_input_mut_borrow
  (n : nat) (_a : u32) (i : u32) : result u32 :=
  _ <- ignore_input_mut_borrow_loop n i; Ok _a
.

(** [loops::incr_ignore_input_mut_borrow]: loop 0:
    Source: 'tests/src/loops.rs', lines 353:0-358:1 *)
Fixpoint incr_ignore_input_mut_borrow_loop (n : nat) (i : u32) : result unit :=
  match n with
  | O => Fail_ OutOfFuel
  | S n1 =>
    if i s> 0%u32
    then (i1 <- u32_sub i 1%u32; incr_ignore_input_mut_borrow_loop n1 i1)
    else Ok tt
  end
.

(** [loops::incr_ignore_input_mut_borrow]:
    Source: 'tests/src/loops.rs', lines 353:0-353:60 *)
Definition incr_ignore_input_mut_borrow
  (n : nat) (a : u32) (i : u32) : result u32 :=
  a1 <- u32_add a 1%u32; _ <- incr_ignore_input_mut_borrow_loop n i; Ok a1
.

(** [loops::ignore_input_shared_borrow]: loop 0:
    Source: 'tests/src/loops.rs', lines 362:0-366:1 *)
Fixpoint ignore_input_shared_borrow_loop (n : nat) (i : u32) : result unit :=
  match n with
  | O => Fail_ OutOfFuel
  | S n1 =>
    if i s> 0%u32
    then (i1 <- u32_sub i 1%u32; ignore_input_shared_borrow_loop n1 i1)
    else Ok tt
  end
.

(** [loops::ignore_input_shared_borrow]:
    Source: 'tests/src/loops.rs', lines 362:0-362:59 *)
Definition ignore_input_shared_borrow
  (n : nat) (_a : u32) (i : u32) : result u32 :=
  _ <- ignore_input_shared_borrow_loop n i; Ok _a
.

End Loops.