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
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
|
-- 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::use_incr]:
Source: 'src/demo.rs', lines 25:0-25:17 -/
def use_incr : Result Unit :=
do
let x ← incr 0#u32
let x1 ← incr x
let _ ← incr x1
Result.ret ()
/- [demo::CList]
Source: 'src/demo.rs', lines 34:0-34:17 -/
inductive CList (T : Type) :=
| CCons : T → CList T → CList T
| CNil : CList T
/- [demo::list_nth]:
Source: 'src/demo.rs', lines 39:0-39: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 54:0-54: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 69:0-78: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 69:0-69:77 -/
def list_nth_mut1
(T : Type) (l : CList T) (i : U32) :
Result (T × (T → Result (CList T)))
:=
list_nth_mut1_loop T l i
/- [demo::i32_id]:
Source: 'src/demo.rs', lines 80:0-80: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
/- [demo::list_tail]:
Source: 'src/demo.rs', lines 88:0-88:64 -/
divergent def list_tail
(T : Type) (l : CList T) :
Result ((CList T) × (CList T → Result (CList T)))
:=
match l with
| CList.CCons t tl =>
do
let (c, list_tail_back) ← list_tail T tl
let back_'a :=
fun ret =>
do
let tl1 ← list_tail_back ret
Result.ret (CList.CCons t tl1)
Result.ret (c, back_'a)
| CList.CNil => Result.ret (CList.CNil, Result.ret)
/- Trait declaration: [demo::Counter]
Source: 'src/demo.rs', lines 97:0-97:17 -/
structure Counter (Self : Type) where
incr : Self → Result (Usize × Self)
/- [demo::{(demo::Counter for usize)}::incr]:
Source: 'src/demo.rs', lines 102:4-102: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 101:0-101:22 -/
def CounterUsize : Counter Usize := {
incr := CounterUsize.incr
}
/- [demo::use_counter]:
Source: 'src/demo.rs', lines 109:0-109:59 -/
def use_counter
(T : Type) (CounterInst : Counter T) (cnt : T) : Result (Usize × T) :=
CounterInst.incr cnt
end demo
|
