Trait IteratorSpecImpl 

pub trait IteratorSpecImpl: Iterator {
    // Required methods
    exec fn obeys_prophetic_iter_laws(&self) -> bool;
    exec fn remaining(&self) -> Seq<Self::Item>;
    exec fn will_return_none(&self) -> bool;
    exec fn decrease(&self) -> Option<nat>;
    exec fn peek(&self, index: int) -> Option<Self::Item>;
}

Required Methods

exec fn obeys_prophetic_iter_laws(&self) -> bool

This iterator obeys the specifications below on next, expressed in terms of prophetic spec functions. Only iterators that terminate (i.e., eventually return None and then continue to return None) should use this interface.

exec fn remaining(&self) -> Seq<Self::Item>

Sequence of items that will (eventually) be returned

exec fn will_return_none(&self) -> bool

Does this iterator complete with a None after the above sequence? (As opposed to hanging indefinitely on a next() call) Trivially true for most iterators but important for iterators that apply an exec closure that may not terminate.

exec fn decrease(&self) -> Option<nat>

Value used by default for the decreases clause when no explicit decreases clause is provided (the user can override this with an explicit decreases clause). If there’s no appropriate metric to decrease, this can return None, and the user will have to provide an explicit decreases clause.

exec fn peek(&self, index: int) -> Option<Self::Item>

Implementations on Foreign Types

impl<'a> IteratorSpecImpl for Chars<'a>

Available on verus_keep_ghost and crate feature alloc only.

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

uninterp spec fn will_return_none(&self) -> bool

uninterp spec fn decrease(&self) -> Option<nat>

open spec fn peek(&self, index: int) -> Option<Self::Item>

{
    if 0 <= index < into_iter_elts(*self).len() {
        Some(into_iter_elts(*self)[index])
    } else {
        None
    }
}

impl<'a, K> IteratorSpecImpl for Iter<'a, K>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

uninterp spec fn will_return_none(&self) -> bool

uninterp spec fn decrease(&self) -> Option<nat>

open spec fn peek(&self, index: int) -> Option<Self::Item>

{
    if 0 <= index < into_iter_hash_keys(*self).len() {
        Some(&into_iter_hash_keys(*self)[index])
    } else {
        None
    }
}

impl<'a, K, V> IteratorSpecImpl for Iter<'a, K, V>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

uninterp spec fn will_return_none(&self) -> bool

uninterp spec fn decrease(&self) -> Option<nat>

open spec fn peek(&self, index: int) -> Option<Self::Item>

{
    if 0 <= index < into_iter(*self).len() {
        let (k, v) = into_iter(*self)[index];
        Some((&k, &v))
    } else {
        None
    }
}

impl<'a, K, V> IteratorSpecImpl for Keys<'a, K, V>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

uninterp spec fn will_return_none(&self) -> bool

uninterp spec fn decrease(&self) -> Option<nat>

open spec fn peek(&self, index: int) -> Option<Self::Item>

{
    if 0 <= index < into_iter_keys(*self).len() {
        Some(&into_iter_keys(*self)[index])
    } else {
        None
    }
}

impl<'a, K, V> IteratorSpecImpl for Values<'a, K, V>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

uninterp spec fn will_return_none(&self) -> bool

uninterp spec fn decrease(&self) -> Option<nat>

open spec fn peek(&self, index: int) -> Option<Self::Item>

{
    if 0 <= index < into_iter_values(*self).len() {
        Some(&into_iter_values(*self)[index])
    } else {
        None
    }
}

impl<'a, K, V> IteratorSpecImpl for Iter<'a, K, V>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

uninterp spec fn will_return_none(&self) -> bool

uninterp spec fn decrease(&self) -> Option<nat>

open spec fn peek(&self, index: int) -> Option<Self::Item>

{
    if 0 <= index < into_iter(*self).len() {
        let (k, v) = into_iter(*self)[index];
        Some((&k, &v))
    } else {
        None
    }
}

impl<'a, K, V> IteratorSpecImpl for Keys<'a, K, V>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

uninterp spec fn will_return_none(&self) -> bool

uninterp spec fn decrease(&self) -> Option<nat>

open spec fn peek(&self, index: int) -> Option<Self::Item>

{
    if 0 <= index < into_iter_keys(*self).len() {
        Some(&into_iter_keys(*self)[index])
    } else {
        None
    }
}

impl<'a, K, V> IteratorSpecImpl for Values<'a, K, V>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

uninterp spec fn will_return_none(&self) -> bool

uninterp spec fn decrease(&self) -> Option<nat>

open spec fn peek(&self, index: int) -> Option<Self::Item>

{
    if 0 <= index < into_iter_values(*self).len() {
        Some(&into_iter_values(*self)[index])
    } else {
        None
    }
}

impl<'a, T> IteratorSpecImpl for Iter<'a, T>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

uninterp spec fn will_return_none(&self) -> bool

uninterp spec fn decrease(&self) -> Option<nat>

open spec fn peek(&self, index: int) -> Option<Self::Item>

{
    if 0 <= index < into_iter_btree_keys(*self).len() {
        Some(&into_iter_btree_keys(*self)[index])
    } else {
        None
    }
}

impl<'a, T: 'a> IteratorSpecImpl for Iter<'a, T>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

uninterp spec fn will_return_none(&self) -> bool

uninterp spec fn decrease(&self) -> Option<nat>

open spec fn peek(&self, index: int) -> Option<Self::Item>

{
    if 0 <= index < into_iter_elts(*self).len() {
        Some(&into_iter_elts(*self)[index])
    } else {
        None
    }
}

impl<'a, T: 'a> IteratorSpecImpl for Iter<'a, T>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

uninterp spec fn will_return_none(&self) -> bool

uninterp spec fn decrease(&self) -> Option<nat>

open spec fn peek(&self, index: int) -> Option<Self::Item>

{
    if 0 <= index < into_iter_elts(*self).len() {
        Some(&into_iter_elts(*self)[index])
    } else {
        None
    }
}

impl<A: Step> IteratorSpecImpl for Range<A>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

open spec fn remaining(&self) -> Seq<Self::Item>

{
    let steps = self.start.spec_steps_between_int(self.end);
    let len = if steps > 0 { steps } else { 0 };
    Seq::new(len as nat, |i: int| self.start.spec_forward_checked_int(i).unwrap())
}

uninterp spec fn will_return_none(&self) -> bool

open spec fn decrease(&self) -> Option<nat>

{ Some(self.start.spec_steps_between_int(self.end) as nat) }

open spec fn peek(&self, index: int) -> Option<Self::Item>

{
    if 0 <= index <= self.start.spec_steps_between_int(self.end) {
        Some(self.start.spec_forward_checked_int(index).unwrap())
    } else {
        None
    }
}

impl<A: Step> IteratorSpecImpl for RangeInclusive<A>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

open spec fn remaining(&self) -> Seq<Self::Item>

{
    Seq::new(
        (self@.start.spec_steps_between_int(self@.end) + 1) as nat,
        |i: int| self@.start.spec_forward_checked_int(i).unwrap(),
    )
}

uninterp spec fn will_return_none(&self) -> bool

open spec fn decrease(&self) -> Option<nat>

{ Some((self@.start.spec_steps_between_int(self@.end) + 1) as nat) }

open spec fn peek(&self, index: int) -> Option<Self::Item>

{
    if 0 <= index <= self@.start.spec_steps_between_int(self@.end) + 1 {
        Some(self@.start.spec_forward_checked_int(index).unwrap())
    } else {
        None
    }
}

impl<I> IteratorSpecImpl for &mut I

where I: Iterator,

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ <I as IteratorSpec>::obeys_prophetic_iter_laws(*self) }

open spec fn remaining(&self) -> Seq<Self::Item>

{ <I as IteratorSpec>::remaining(*self) }

open spec fn will_return_none(&self) -> bool

{ <I as IteratorSpec>::will_return_none(*self) }

open spec fn decrease(&self) -> Option<nat>

{ <I as IteratorSpec>::decrease(*self) }

open spec fn peek(&self, index: int) -> Option<Self::Item>

{ <I as IteratorSpec>::peek(*self, index) }

impl<I> IteratorSpecImpl for Rev<I>

where I: DoubleEndedIterator + DoubleEndedIteratorSpec,

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ rev_iter(*self).obeys_prophetic_iter_laws() }

closed spec fn remaining(&self) -> Seq<Self::Item>

closed spec fn will_return_none(&self) -> bool

closed spec fn decrease(&self) -> Option<nat>

open spec fn peek(&self, index: int) -> Option<Self::Item>

{ rev_iter(*self).peek_back(index) }

impl<T, A: Allocator> IteratorSpecImpl for IntoIter<T, A>

open spec fn obeys_prophetic_iter_laws(&self) -> bool

{ true }

uninterp spec fn remaining(&self) -> Seq<Self::Item>

uninterp spec fn will_return_none(&self) -> bool

uninterp spec fn decrease(&self) -> Option<nat>

open spec fn peek(&self, index: int) -> Option<Self::Item>

{
    if 0 <= index < into_iter_elts(*self).len() {
        Some(into_iter_elts(*self)[index])
    } else {
        None
    }
}

Implementors