-
Notifications
You must be signed in to change notification settings - Fork 99
/
list.rs
86 lines (73 loc) · 1.58 KB
/
list.rs
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
//! Example of linked list
#![feature(nll)]
#![feature(box_patterns)]
#![feature(box_syntax)]
use prusti_contracts::*;
enum List {
Nil,
Const {
val: i32,
next: Box<List>
},
}
fn head(list: List) -> Option<i32> {
match list {
List::Nil => None,
List::Const { val, box next } => Some(val),
}
}
fn tail(list: List) -> Option<List> {
match list {
List::Nil => None,
List::Const { val, box next } => Some(next),
}
}
fn length(list: List) -> u32 {
match list {
List::Nil => 0,
List::Const { val, box next } => 1 + length(next),
}
}
fn last_value(list: List) -> Option<i32> {
match list {
List::Nil => None,
List::Const { val, box next } => match last_value(next) {
None => Some(val),
Some(last) => Some(last),
}
}
}
fn empty_list(val: i32) -> List {
List::Nil
}
fn singleton_list(val: i32) -> List {
List::Const {
val,
next: box List::Nil
}
}
fn prepend(val: i32, list: List) -> List {
List::Const {
val,
next: box list
}
}
fn append(new_val: i32, list: List) -> List {
match list {
List::Nil => List::Const {
val: new_val,
next: box List::Nil
},
List::Const { val, box next } => List::Const {
val: val,
next: box append(new_val, next)
},
}
}
fn revert(list: List) -> List {
match list {
List::Nil => List::Nil,
List::Const { val, box next } => append(val, revert(next))
}
}
fn main() {}