-
Notifications
You must be signed in to change notification settings - Fork 17
/
range.rs
57 lines (50 loc) · 1.23 KB
/
range.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
#[flux::refined_by(lo: int, hi: int)]
pub struct RngIter {
#[flux::field(i32[@lo])]
_lo: i32,
#[flux::field(i32[@hi])]
hi: i32,
#[flux::field(i32{v:lo <= v && v <= hi})]
cur: i32,
}
impl RngIter {
#[flux::sig(fn(lo:i32, hi:i32{lo <= hi}) -> RngIter[lo, hi])]
pub fn new(lo: i32, hi: i32) -> RngIter {
Self { _lo: lo, hi, cur: lo }
}
}
#[flux::refined_by(lo: int, hi: int)]
pub struct Rng {
#[flux::field(i32[@lo])]
lo: i32,
#[flux::field({i32[@hi] : lo <= hi})]
hi: i32,
}
impl Rng {
#[flux::sig(fn(lo:i32, hi:i32{lo <= hi}) -> Rng[lo, hi])]
pub fn new(lo: i32, hi: i32) -> Rng {
Self { lo, hi }
}
}
impl Iterator for RngIter {
type Item = i32;
#[flux::sig(fn(self: &mut RngIter[@lo, @hi]) -> Option<i32{v:lo <= v && v < hi}>)]
fn next(&mut self) -> Option<i32> {
let cur = self.cur;
let hi = self.hi;
if cur < hi {
self.cur = cur + 1;
Some(cur)
} else {
None
}
}
}
impl IntoIterator for Rng {
type Item = i32;
type IntoIter = RngIter;
#[flux::sig(fn(Rng[@lo, @hi]) -> RngIter[lo, hi])]
fn into_iter(self) -> RngIter {
RngIter::new(self.lo, self.hi)
}
}