-
Notifications
You must be signed in to change notification settings - Fork 0
/
iterator.zz
113 lines (98 loc) · 2.03 KB
/
iterator.zz
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
using list::{ List }
using node::{ Node }
using zxutils as utils
/**
* The list iterator iteration direction.
*/
export enum Direction {
Head = 0,
Tail = 1
}
/**
* The `Direction::Head` enum value exported as a
* constant for better ergonomics.
*/
export const int HEAD = Direction::Head;
/**
* The `Direction::Tail` enum value exported as a
* constant for better ergonomics.
*/
export const int TAIL = Direction::Tail;
/**
* An iterator context for a list.
*/
export struct Iterator {
Direction direction;
bool ended;
Node unsafe *node;
}
/**
* `Iterator` stack constructor with direction from a list.
*/
export fn make(Iterator new mut *self, List *list, Direction direction)
model safe(self)
where safe(list)
{
self->ended = false;
self->direction = direction;
switch direction {
Direction::Head => { self->node = list->head; }
Direction::Tail => { self->node = list->tail; }
}
if 0 == self->node {
self->ended = true;
}
}
/**
* Returns a pointer to the next node in the list.
* @example
* new list = zxlist::make();
* let it = list.iterator();
* while !it.ended {
* let node = it.next();
* }
*/
export fn next(Iterator mut *self) -> Node *
model safe(self)
model safe(return)
model safe(return->value)
where false == self->ended
{
let node = self->node;
if 0 != node {
static_attest(safe(node));
switch self->direction {
Direction::Head => { self->node = node->next; }
Direction::Tail => { self->node = node->prev; }
}
}
if 0 == self->node {
self->ended = true;
}
static_attest(safe(node));
static_attest(safe(node->value));
return node;
}
/**
* Marks the iterator as "ended".
* @example
* new list = zxlist::make();
* let mut it = list.iterator();
*
* while !it.ended {
* if list.contains(key) {
* it.end();
* } else {
* it.next();
* }
* }
*
* it.destroy();
*/
export fn end(Iterator mut *self)
model safe(self)
where false == self->ended
{
self->ended = true;
self->node = 0;
}