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

namespace paper

/- [paper::ref_incr]:
   Source: 'tests/src/paper.rs', lines 6:0-6:28 -/
def ref_incr (x : I32) : Result I32 :=
  x + 1#i32

/- [paper::test_incr]:
   Source: 'tests/src/paper.rs', lines 10:0-10:18 -/
def test_incr : Result Unit :=
  do
  let x ← ref_incr 0#i32
  if ¬ (x = 1#i32)
  then Result.fail .panic
  else Result.ok ()

/- Unit test for [paper::test_incr] -/
#assert (test_incr == Result.ok ())

/- [paper::choose]:
   Source: 'tests/src/paper.rs', lines 17:0-17:70 -/
def choose
  (T : Type) (b : Bool) (x : T) (y : T) :
  Result (T × (T → Result (T × T)))
  :=
  if b
  then let back := fun ret => Result.ok (ret, y)
       Result.ok (x, back)
  else let back := fun ret => Result.ok (x, ret)
       Result.ok (y, back)

/- [paper::test_choose]:
   Source: 'tests/src/paper.rs', lines 25:0-25: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)
  then Result.fail .panic
  else
    do
    let (x, y) ← choose_back z1
    if ¬ (x = 1#i32)
    then Result.fail .panic
    else if ¬ (y = 0#i32)
         then Result.fail .panic
         else Result.ok ()

/- Unit test for [paper::test_choose] -/
#assert (test_choose == Result.ok ())

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

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

/- [paper::sum]:
   Source: 'tests/src/paper.rs', lines 59:0-59:32 -/
divergent def sum (l : List I32) : Result I32 :=
  match l with
  | List.Cons x tl => do
                      let i ← sum tl
                      x + i
  | List.Nil => Result.ok 0#i32

/- [paper::test_nth]:
   Source: 'tests/src/paper.rs', lines 70:0-70: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 l2 ← list_nth_mut_back x1
  let i ← sum l2
  if ¬ (i = 7#i32)
  then Result.fail .panic
  else Result.ok ()

/- Unit test for [paper::test_nth] -/
#assert (test_nth == Result.ok ())

/- [paper::call_choose]:
   Source: 'tests/src/paper.rs', lines 78:0-78:44 -/
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 (px1, _) ← choose_back pz1
  Result.ok px1

end paper