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
|
//@ [coq,fstar] aeneas-args=-use-fuel
#![allow(clippy::needless_lifetimes)]
/* Simple functions */
pub fn choose<'a, T>(b: bool, x: &'a mut T, y: &'a mut T) -> &'a mut T {
if b {
x
} else {
y
}
}
pub fn mul2_add1(x: u32) -> u32 {
(x + x) + 1
}
pub fn use_mul2_add1(x: u32, y: u32) -> u32 {
mul2_add1(x) + y
}
pub fn incr<'a>(x: &'a mut u32) {
*x += 1;
}
pub fn use_incr() {
let mut x = 0;
incr(&mut x);
incr(&mut x);
incr(&mut x);
}
/* Recursion, loops */
pub enum CList<T> {
CCons(T, Box<CList<T>>),
CNil,
}
pub fn list_nth<'a, T>(l: &'a CList<T>, i: u32) -> &'a T {
match l {
CList::CCons(x, tl) => {
if i == 0 {
x
} else {
list_nth(tl, i - 1)
}
}
CList::CNil => {
panic!()
}
}
}
pub fn list_nth_mut<'a, T>(l: &'a mut CList<T>, i: u32) -> &'a mut T {
match l {
CList::CCons(x, tl) => {
if i == 0 {
x
} else {
list_nth_mut(tl, i - 1)
}
}
CList::CNil => {
panic!()
}
}
}
pub fn list_nth_mut1<'a, T>(mut l: &'a mut CList<T>, mut i: u32) -> &'a mut T {
while let CList::CCons(x, tl) = l {
if i == 0 {
return x;
}
i -= 1;
l = tl;
}
panic!()
}
pub fn i32_id(i: i32) -> i32 {
if i == 0 {
0
} else {
i32_id(i - 1) + 1
}
}
pub fn list_tail<'a, T>(l: &'a mut CList<T>) -> &'a mut CList<T> {
match l {
CList::CCons(_, tl) => list_tail(tl),
CList::CNil => l,
}
}
/* Traits */
pub trait Counter {
fn incr(&mut self) -> usize;
}
impl Counter for usize {
fn incr(&mut self) -> usize {
let x = *self;
*self += 1;
x
}
}
pub fn use_counter<'a, T: Counter>(cnt: &'a mut T) -> usize {
cnt.incr()
}
|
