ostd::specs::mm::frame::linked_list::linked_list_owners

Struct CursorModel

pub struct CursorModel {
    pub fore: Seq<LinkModel>,
    pub rear: Seq<LinkModel>,
    pub list_model: LinkedListModel,
}

Fields§

§fore: Seq<LinkModel>§rear: Seq<LinkModel>§list_model: LinkedListModel

Implementations§

Source §

impl CursorModel

Source

pub open spec fn current(self) -> Option<LinkModel>

{ if self.rear.len() > 0 { Some(self.rear[0]) } else { None } }

Source §

impl CursorModel

Source

pub open spec fn move_next_spec(self) -> Self

{
    if self.list_model.list.len() > 0 {
        if self.rear.len() > 0 {
            let cur = self.rear[0];
            Self {
                fore: self.fore.insert(self.fore.len() as int, cur),
                rear: self.rear.remove(0),
                list_model: self.list_model,
            }
        } else {
            Self {
                fore: Seq::<LinkModel>::empty(),
                rear: self.fore,
                list_model: self.list_model,
            }
        }
    } else {
        self
    }
}

Source

pub open spec fn move_prev_spec(self) -> Self

{
    if self.list_model.list.len() > 0 {
        if self.fore.len() > 0 {
            let cur = self.fore[self.fore.len() - 1];
            Self {
                fore: self.fore.remove(self.fore.len() - 1),
                rear: self.rear.insert(0, cur),
                list_model: self.list_model,
            }
        } else {
            Self {
                fore: self.rear,
                rear: Seq::<LinkModel>::empty(),
                list_model: self.list_model,
            }
        }
    } else {
        self
    }
}

Source

pub open spec fn remove(self) -> Self

{
    let rear = self.rear.remove(0);
    Self {
        fore: self.fore,
        rear: rear,
        list_model: LinkedListModel {
            list: self.fore.add(rear),
        },
    }
}

Source

pub open spec fn insert(self, link: LinkModel) -> Self

{
    let fore = self.fore.insert(self.fore.len() - 1, link);
    Self {
        fore: fore,
        rear: self.rear,
        list_model: LinkedListModel {
            list: fore.add(self.rear),
        },
    }
}