summaryrefslogtreecommitdiff
path: root/tests/lean/Demo/Demo.lean
blob: 854b4853f3d3adf2a3ccdd3736241c8b696759e5 (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
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
-- [demo]
import Base
open Primitives

namespace demo

/- [demo::choose]:
   Source: 'src/demo.rs', lines 5:0-5:70 -/
def choose
  (T : Type) (b : Bool) (x : T) (y : T) :
  Result (T × (T  Result (T × T)))
  :=
  if b
  then let back_'a := fun ret => Result.ret (ret, y)
       Result.ret (x, back_'a)
  else let back_'a := fun ret => Result.ret (x, ret)
       Result.ret (y, back_'a)

/- [demo::mul2_add1]:
   Source: 'src/demo.rs', lines 13:0-13:31 -/
def mul2_add1 (x : U32) : Result U32 :=
  do
  let i  x + x
  i + 1#u32

/- [demo::use_mul2_add1]:
   Source: 'src/demo.rs', lines 17:0-17:43 -/
def use_mul2_add1 (x : U32) (y : U32) : Result U32 :=
  do
  let i  mul2_add1 x
  i + y

/- [demo::incr]:
   Source: 'src/demo.rs', lines 21:0-21:31 -/
def incr (x : U32) : Result U32 :=
  x + 1#u32

/- [demo::CList]
   Source: 'src/demo.rs', lines 27:0-27:17 -/
inductive CList (T : Type) :=
| CCons : T  CList T  CList T
| CNil : CList T

/- [demo::list_nth]:
   Source: 'src/demo.rs', lines 32:0-32:56 -/
divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
  match l with
  | CList.CCons x tl =>
    if i = 0#u32
    then Result.ret x
    else do
         let i1  i - 1#u32
         list_nth T tl i1
  | CList.CNil => Result.fail .panic

/- [demo::list_nth_mut]:
   Source: 'src/demo.rs', lines 47:0-47:68 -/
divergent def list_nth_mut
  (T : Type) (l : CList T) (i : U32) :
  Result (T × (T  Result (CList T)))
  :=
  match l with
  | CList.CCons x tl =>
    if i = 0#u32
    then
      let back_'a := fun ret => Result.ret (CList.CCons ret tl)
      Result.ret (x, back_'a)
    else
      do
      let i1  i - 1#u32
      let (t, list_nth_mut_back)  list_nth_mut T tl i1
      let back_'a :=
        fun ret =>
          do
          let tl1  list_nth_mut_back ret
          Result.ret (CList.CCons x tl1)
      Result.ret (t, back_'a)
  | CList.CNil => Result.fail .panic

/- [demo::list_nth_mut1]: loop 0:
   Source: 'src/demo.rs', lines 62:0-71:1 -/
divergent def list_nth_mut1_loop
  (T : Type) (l : CList T) (i : U32) :
  Result (T × (T  Result (CList T)))
  :=
  match l with
  | CList.CCons x tl =>
    if i = 0#u32
    then
      let back_'a := fun ret => Result.ret (CList.CCons ret tl)
      Result.ret (x, back_'a)
    else
      do
      let i1  i - 1#u32
      let (t, back_'a)  list_nth_mut1_loop T tl i1
      let back_'a1 :=
        fun ret => do
                   let tl1  back_'a ret
                   Result.ret (CList.CCons x tl1)
      Result.ret (t, back_'a1)
  | CList.CNil => Result.fail .panic

/- [demo::list_nth_mut1]:
   Source: 'src/demo.rs', lines 62:0-62:77 -/
def list_nth_mut1
  (T : Type) (l : CList T) (i : U32) :
  Result (T × (T  Result (CList T)))
  :=
  do
  let (t, back_'a)  list_nth_mut1_loop T l i
  Result.ret (t, back_'a)

/- [demo::i32_id]:
   Source: 'src/demo.rs', lines 73:0-73:28 -/
divergent def i32_id (i : I32) : Result I32 :=
  if i = 0#i32
  then Result.ret 0#i32
  else do
       let i1  i - 1#i32
       let i2  i32_id i1
       i2 + 1#i32

/- Trait declaration: [demo::Counter]
   Source: 'src/demo.rs', lines 83:0-83:17 -/
structure Counter (Self : Type) where
  incr : Self  Result (Usize × Self)

/- [demo::{(demo::Counter for usize)}::incr]:
   Source: 'src/demo.rs', lines 88:4-88:31 -/
def CounterUsize.incr (self : Usize) : Result (Usize × Usize) :=
  do
  let self1  self + 1#usize
  Result.ret (self, self1)

/- Trait implementation: [demo::{(demo::Counter for usize)}]
   Source: 'src/demo.rs', lines 87:0-87:22 -/
def CounterUsize : Counter Usize := {
  incr := CounterUsize.incr
}

/- [demo::use_counter]:
   Source: 'src/demo.rs', lines 95:0-95:59 -/
def use_counter
  (T : Type) (CounterInst : Counter T) (cnt : T) : Result (Usize × T) :=
  CounterInst.incr cnt

end demo