summaryrefslogtreecommitdiff
path: root/tests/lean/Paper.lean
blob: 400406f111377b0b5e5d681922868c25c2693c1e (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [paper]
import Base
open Primitives

namespace paper

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

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

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

/- [paper::choose]:
   Source: 'tests/src/paper.rs', lines 18:0-18: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 26:0-26:20 -/
def test_choose : Result Unit :=
  do
  let (z, choose_back)  choose I32 true 0i32 0i32
  let z1  z + 1i32
  if z1 = 1i32
  then
    do
    let (x, y)  choose_back z1
    if x = 1i32
    then if y = 0i32
         then Result.ok ()
         else Result.fail .panic
    else Result.fail .panic
  else Result.fail .panic

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

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

/- [paper::list_nth_mut]:
   Source: 'tests/src/paper.rs', lines 45:0-45: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 = 0u32
    then
      let back := fun ret => Result.ok (List.Cons ret tl)
      Result.ok (x, back)
    else
      do
      let i1  i - 1u32
      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 60:0-60: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 0i32

/- [paper::test_nth]:
   Source: 'tests/src/paper.rs', lines 71:0-71:17 -/
def test_nth : Result Unit :=
  do
  let l := List.Cons 3i32 List.Nil
  let l1 := List.Cons 2i32 l
  let (x, list_nth_mut_back)  list_nth_mut I32 (List.Cons 1i32 l1) 2u32
  let x1  x + 1i32
  let l2  list_nth_mut_back x1
  let i  sum l2
  if i = 7i32
  then Result.ok ()
  else Result.fail .panic

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

/- [paper::call_choose]:
   Source: 'tests/src/paper.rs', lines 79:0-79: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 + 1u32
  let (px1, _)  choose_back pz1
  Result.ok px1

end paper