flux_core/iter/traits/
iterator.rs

1use flux_attrs::*;
2
3defs! {
4    fn default_iterator_size<T>(self: T) -> int;
5    fn default_iterator_done<T>(self: T) -> bool;
6    fn max(a: int, b: int) -> int { if a > b { a } else { b } }
7}
8
9#[extern_spec(core::iter)]
10#[assoc(
11    fn valid_item(self: Self, item: Self::Item) -> bool { true }
12    fn size(self: Self) -> int { default_iterator_size(self) }
13    fn done(self: Self) -> bool { default_iterator_done(self) }
14    fn step(self: Self, other: Self) -> bool { true }
15)]
16trait Iterator {
17    #[spec(
18        fn(self: &mut Self[@curr_s]) -> Option<Self::Item>[!<Self as Iterator>::done(curr_s)]
19        ensures self: Self{next_s: <Self as Iterator>::step(curr_s, next_s)}
20    )]
21    fn next(&mut self) -> Option<Self::Item>;
22
23    #[spec(fn(Self[@s]) -> Enumerate<Self>[0, s])]
24    fn enumerate(self) -> Enumerate<Self>
25    where
26        Self: Sized;
27
28    #[spec(
29        fn(Self[@s], f: F) -> Map<Self, F>[s]
30        where
31            F: FnMut(Self::Item{item: <Self as Iterator>::valid_item(s, item)}) -> B
32    )]
33    fn map<B, F>(self, f: F) -> Map<Self, F>
34    where
35        Self: Sized,
36        F: FnMut(Self::Item) -> B;
37
38    #[spec(fn(Self[@s], n: usize) -> Skip<Self>[max(0, <Self as Iterator>::size(s) - n)])]
39    fn skip(self, n: usize) -> Skip<Self>
40    where
41        Self: Sized;
42
43    #[spec(fn(Self[@s], f: F) where F: FnMut(Self::Item{item: <Self as Iterator>::valid_item(s, item)}) -> () )]
44    fn for_each<F>(self, f: F)
45    where
46        Self: Sized,
47        F: FnMut(Self::Item);
48
49    #[spec(fn (Self[@s]) -> B{v: <B as FromIterator<Self::Item>>::with_size(v, <Self as Iterator>::size(s))})]
50    fn collect<B: FromIterator<Self::Item>>(self) -> B
51    where
52        Self: Sized;
53}
flux_core/iter/traits/iterator.rs

flux_core/iter/traits/
iterator.rs
