Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Module 0x1::option

This module defines the Option type and its methods to represent and handle an optional value.

use 0x1::mem;
use 0x1::vector;

Enum Option

Abstraction of a value that may or may not be present.

enum Option<Element> has copy, drop, store
Variants
None
Fields
Some
Fields
e: Element

Constants

The Option is in an invalid state for the operation attempted. The Option is Some while it should be None.

const EOPTION_IS_SET: u64 = 262144;

The Option is in an invalid state for the operation attempted. The Option is None while it should be Some.

const EOPTION_NOT_SET: u64 = 262145;

Cannot construct an option from a vector with 2 or more elements.

const EOPTION_VEC_TOO_LONG: u64 = 262146;

Function none

Return an empty Option

public fun none<Element>(): option::Option<Element>
Implementation
public fun none<Element>(): Option<Element> {
    Option::None
}

Function some

Return an Option containing e

public fun some<Element>(e: Element): option::Option<Element>
Implementation
public fun some<Element>(e: Element): Option<Element> {
    Option::Some { e }
}

Function from_vec

public fun from_vec<Element>(vec: vector<Element>): option::Option<Element>
Implementation
public fun from_vec<Element>(vec: vector<Element>): Option<Element> {
    assert!(vec.length() <= 1, EOPTION_VEC_TOO_LONG);
    if (vec.is_empty()) {
        vec.destroy_empty();
        Option::None
    } else {
        let e = vec.pop_back();
        vec.destroy_empty();
        Option::Some { e }
    }
}

Function is_none

Return true if self does not hold a value

public fun is_none<Element>(self: &option::Option<Element>): bool
Implementation
public fun is_none<Element>(self: &Option<Element>): bool {
    self is Option::None<Element>
}

Function is_some

Return true if self holds a value

public fun is_some<Element>(self: &option::Option<Element>): bool
Implementation
public fun is_some<Element>(self: &Option<Element>): bool {
    self is Option::Some<Element>
}

Function contains

Return true if the value in self is equal to e_ref Always returns false if self does not hold a value

public fun contains<Element>(self: &option::Option<Element>, e_ref: &Element): bool
Implementation
public fun contains<Element>(self: &Option<Element>, e_ref: &Element): bool {
    if (self is Option::None<Element>) {
        false
    } else {
        &self.e == e_ref
    }
}

Function borrow

Return an immutable reference to the value inside self Aborts if self does not hold a value

public fun borrow<Element>(self: &option::Option<Element>): &Element
Implementation
public fun borrow<Element>(self: &Option<Element>): &Element {
    if (self is Option::None<Element>) {
        abort EOPTION_NOT_SET
    } else {
        &self.e
    }
}

Function borrow_with_default

Return a reference to the value inside self if it holds one Return default_ref if self does not hold a value

public fun borrow_with_default<Element>(self: &option::Option<Element>, default_ref: &Element): &Element
Implementation
public fun borrow_with_default<Element>(self: &Option<Element>, default_ref: &Element): &Element {
    match (self) {
        Option::None => default_ref,
        Option::Some { e } => e,
    }
}

Function get_with_default

Return the value inside self if it holds one Return default if self does not hold a value

public fun get_with_default<Element: copy, drop>(self: &option::Option<Element>, default: Element): Element
Implementation
public fun get_with_default<Element: copy + drop>(
    self: &Option<Element>,
    default: Element,
): Element {
    match (self) {
        Option::None => default,
        Option::Some { e } => *e,
    }
}

Function fill

Convert the none option self to a some option by adding e. Aborts if self already holds a value

public fun fill<Element>(self: &mut option::Option<Element>, e: Element)
Implementation
public fun fill<Element>(self: &mut Option<Element>, e: Element) {
    let old = mem::replace(self, Option::Some { e });
    match (old) {
        Option::None => {},
        Option::Some { e: _ } => {
           abort EOPTION_IS_SET
        },
    }
}

Function extract

Convert a some option to a none by removing and returning the value stored inside self Aborts if self does not hold a value

public fun extract<Element>(self: &mut option::Option<Element>): Element
Implementation
public fun extract<Element>(self: &mut Option<Element>): Element {
    let inner = mem::replace(self, Option::None);
    match (inner) {
        Option::Some { e } => e,
        Option::None => {
           abort EOPTION_NOT_SET
        },
    }
}

Function borrow_mut

Return a mutable reference to the value inside self Aborts if self does not hold a value

public fun borrow_mut<Element>(self: &mut option::Option<Element>): &mut Element
Implementation
public fun borrow_mut<Element>(self: &mut Option<Element>): &mut Element {
    match (self) {
        Option::None => {
            abort EOPTION_NOT_SET
        },
        Option::Some { e } => e,
    }
}

Function swap

Swap the old value inside self with e and return the old value Aborts if self does not hold a value

public fun swap<Element>(self: &mut option::Option<Element>, el: Element): Element
Implementation
public fun swap<Element>(self: &mut Option<Element>, el: Element): Element {
    match (self) {
        Option::None => {
            abort EOPTION_NOT_SET
        },
        Option::Some { e } => {
            mem::replace(e, el)
        },
    }
}

Function swap_or_fill

Swap the old value inside self with e and return the old value; or if there is no old value, fill it with e. Different from swap(), swap_or_fill() allows for self not holding a value.

public fun swap_or_fill<Element>(self: &mut option::Option<Element>, e: Element): option::Option<Element>
Implementation
public fun swap_or_fill<Element>(self: &mut Option<Element>, e: Element): Option<Element> {
    mem::replace(self, Option::Some { e })
}

Function destroy_with_default

Destroys self. If self holds a value, return it. Returns default otherwise

public fun destroy_with_default<Element: drop>(self: option::Option<Element>, default: Element): Element
Implementation
public fun destroy_with_default<Element: drop>(self: Option<Element>, default: Element): Element {
    match (self) {
        Option::None => default,
        Option::Some { e } => e,
    }
}

Function destroy_some

Unpack self and return its contents Aborts if self does not hold a value

public fun destroy_some<Element>(self: option::Option<Element>): Element
Implementation
public fun destroy_some<Element>(self: Option<Element>): Element {
    match (self) {
        Option::None => {
            abort EOPTION_NOT_SET
        },
        Option::Some { e } => e,
    }
}

Function destroy_none

Unpack self Aborts if self holds a value

public fun destroy_none<Element>(self: option::Option<Element>)
Implementation
public fun destroy_none<Element>(self: Option<Element>) {
    match (self) {
        Option::None => {},
        Option::Some { e: _ } => {
            abort EOPTION_IS_SET
        },
    }
}

Function to_vec

Convert self into a vector of length 1 if it is Some, and an empty vector otherwise

public fun to_vec<Element>(self: option::Option<Element>): vector<Element>
Implementation
public fun to_vec<Element>(self: Option<Element>): vector<Element> {
    match (self) {
        Option::None => vector::empty(),
        Option::Some { e } => vector::singleton(e),
    }
}

Function for_each

Apply the function to the optional element, consuming it. Does nothing if no value present.

public fun for_each<Element>(self: option::Option<Element>, f: |Element|)
Implementation
public inline fun for_each<Element>(self: Option<Element>, f: |Element|) {
    if (self.is_some()) {
        f(self.destroy_some())
    } else {
        self.destroy_none()
    }
}

Function for_each_ref

Apply the function to the optional element reference. Does nothing if no value present.

public fun for_each_ref<Element>(self: &option::Option<Element>, f: |&Element|)
Implementation
public inline fun for_each_ref<Element>(self: &Option<Element>, f: |&Element|) {
    if (self.is_some()) {
        f(self.borrow())
    }
}

Function for_each_mut

Apply the function to the optional element reference. Does nothing if no value present.

public fun for_each_mut<Element>(self: &mut option::Option<Element>, f: |&mut Element|)
Implementation
public inline fun for_each_mut<Element>(self: &mut Option<Element>, f: |&mut Element|) {
    if (self.is_some()) {
        f(self.borrow_mut())
    }
}

Function fold

Folds the function over the optional element.

public fun fold<Accumulator, Element>(self: option::Option<Element>, init: Accumulator, f: |Accumulator, Element|Accumulator): Accumulator
Implementation
public inline fun fold<Accumulator, Element>(
    self: Option<Element>,
    init: Accumulator,
    f: |Accumulator,Element|Accumulator
): Accumulator {
    if (self.is_some()) {
        f(init, self.destroy_some())
    } else {
        self.destroy_none();
        init
    }
}

Function map

Maps the content of an option.

public fun map<Element, OtherElement>(self: option::Option<Element>, f: |Element|OtherElement): option::Option<OtherElement>
Implementation
public inline fun map<Element, OtherElement>(self: Option<Element>, f: |Element|OtherElement): Option<OtherElement> {
    if (self.is_some()) {
        some(f(self.destroy_some()))
    } else {
        self.destroy_none();
        none()
    }
}

Function map_ref

Maps the content of an option without destroying the original option.

public fun map_ref<Element, OtherElement>(self: &option::Option<Element>, f: |&Element|OtherElement): option::Option<OtherElement>
Implementation
public inline fun map_ref<Element, OtherElement>(
    self: &Option<Element>, f: |&Element|OtherElement): Option<OtherElement> {
    if (self.is_some()) {
        some(f(self.borrow()))
    } else {
        none()
    }
}

Function filter

Filters the content of an option

public fun filter<Element: drop>(self: option::Option<Element>, f: |&Element|bool): option::Option<Element>
Implementation
public inline fun filter<Element:drop>(self: Option<Element>, f: |&Element|bool): Option<Element> {
    if (self.is_some() && f(self.borrow())) {
        self
    } else {
        none()
    }
}

Function any

Returns true if the option contains an element which satisfies predicate.

public fun any<Element>(self: &option::Option<Element>, p: |&Element|bool): bool
Implementation
public inline fun any<Element>(self: &Option<Element>, p: |&Element|bool): bool {
    self.is_some() && p(self.borrow())
}

Function destroy

Utility function to destroy an option that is not droppable.

public fun destroy<Element>(self: option::Option<Element>, d: |Element|)
Implementation
public inline fun destroy<Element>(self: Option<Element>, d: |Element|) {
    let vec = self.to_vec();
    vec.destroy(|e| d(e));
}

Specification

pragma aborts_if_is_strict;

Helper Schema

schema AbortsIfNone<Element> {
    self: Option<Element>;
    aborts_if self.is_none() with EOPTION_NOT_SET;
}

Function none

public fun none<Element>(): option::Option<Element>
pragma opaque;
aborts_if false;
ensures result == spec_none<Element>();

fun spec_none<Element>(): Option<Element> {
   Option::None
}

Function some

public fun some<Element>(e: Element): option::Option<Element>
pragma opaque;
aborts_if false;
ensures result == spec_some(e);

fun spec_some<Element>(e: Element): Option<Element> {
   Option::Some { e }
}

Function from_vec

public fun from_vec<Element>(vec: vector<Element>): option::Option<Element>
aborts_if vec.length() > 1;

Function is_none

public fun is_none<Element>(self: &option::Option<Element>): bool
pragma opaque;
aborts_if false;
ensures result == spec_is_none(self);

fun spec_is_none<Element>(self: Option<Element>): bool {
   self is Option::None<Element>
}

Function is_some

public fun is_some<Element>(self: &option::Option<Element>): bool
pragma opaque;
aborts_if false;
ensures result == spec_is_some(self);

fun spec_is_some<Element>(self: Option<Element>): bool {
   self is Option::Some<Element>
}

Function contains

public fun contains<Element>(self: &option::Option<Element>, e_ref: &Element): bool
pragma opaque;
aborts_if false;
ensures result == spec_contains(self, e_ref);

fun spec_contains<Element>(self: Option<Element>, e: Element): bool {
   (self is Option::Some<Element>) && self.borrow() == e
}

Function borrow

public fun borrow<Element>(self: &option::Option<Element>): &Element
pragma opaque;
include AbortsIfNone<Element>;
ensures result == spec_borrow(self);

fun spec_borrow<Element>(self: Option<Element>): Element
{
   if (self is Option::Some<Element>) {
       self.e
   } else {
       abort EOPTION_NOT_SET
   }
}

Function borrow_with_default

public fun borrow_with_default<Element>(self: &option::Option<Element>, default_ref: &Element): &Element
pragma opaque;
aborts_if false;
ensures result == (if (self.is_some()) self.borrow() else default_ref);

Function get_with_default

public fun get_with_default<Element: copy, drop>(self: &option::Option<Element>, default: Element): Element
pragma opaque;
aborts_if false;
ensures result == (if (self.is_some()) self.borrow() else default);

Function fill

public fun fill<Element>(self: &mut option::Option<Element>, e: Element)
pragma opaque;
aborts_if self.is_some() with EOPTION_IS_SET;
ensures self.is_some();
ensures self.borrow() == e;

Function extract

public fun extract<Element>(self: &mut option::Option<Element>): Element
pragma opaque;
include AbortsIfNone<Element>;
ensures result == old(self).borrow();
ensures self.is_none();

Function borrow_mut

public fun borrow_mut<Element>(self: &mut option::Option<Element>): &mut Element
include AbortsIfNone<Element>;
ensures result == self.borrow();
ensures self == old(self);

Function swap

public fun swap<Element>(self: &mut option::Option<Element>, el: Element): Element
pragma opaque;
include AbortsIfNone<Element>;
ensures result == old(self).borrow();
ensures self.is_some();
ensures self.borrow() == el;

Function swap_or_fill

public fun swap_or_fill<Element>(self: &mut option::Option<Element>, e: Element): option::Option<Element>
pragma opaque;
aborts_if false;
ensures result == old(self);
ensures self.borrow() == e;

Function destroy_with_default

public fun destroy_with_default<Element: drop>(self: option::Option<Element>, default: Element): Element
pragma opaque;
aborts_if false;
ensures result == (if (self.is_some()) self.borrow() else default);

Function destroy_some

public fun destroy_some<Element>(self: option::Option<Element>): Element
pragma opaque;
include AbortsIfNone<Element>;
ensures result == self.borrow();

Function destroy_none

public fun destroy_none<Element>(self: option::Option<Element>)
pragma opaque;
aborts_if self.is_some() with EOPTION_IS_SET;

Function to_vec

public fun to_vec<Element>(self: option::Option<Element>): vector<Element>
pragma opaque;
aborts_if false;
ensures result == (if (self.is_some()) vector[self.borrow()] else vector::empty());