# Module `0x1::option` This module defines the Option type and its methods to represent and handle an optional value. - [Struct `Option`](#0x1_option_Option) - [Constants](#@Constants_0) - [Function `none`](#0x1_option_none) - [Function `some`](#0x1_option_some) - [Function `is_none`](#0x1_option_is_none) - [Function `is_some`](#0x1_option_is_some) - [Function `contains`](#0x1_option_contains) - [Function `borrow`](#0x1_option_borrow) - [Function `borrow_with_default`](#0x1_option_borrow_with_default) - [Function `get_with_default`](#0x1_option_get_with_default) - [Function `fill`](#0x1_option_fill) - [Function `extract`](#0x1_option_extract) - [Function `borrow_mut`](#0x1_option_borrow_mut) - [Function `swap`](#0x1_option_swap) - [Function `swap_or_fill`](#0x1_option_swap_or_fill) - [Function `destroy_with_default`](#0x1_option_destroy_with_default) - [Function `destroy_some`](#0x1_option_destroy_some) - [Function `destroy_none`](#0x1_option_destroy_none) - [Function `to_vec`](#0x1_option_to_vec) - [Module Specification](#@Module_Specification_1) - [Helper Schema](#@Helper_Schema_2)

use 0x1::vector;

## Struct `Option` Abstraction of a value that may or may not be present. Implemented with a vector of size zero or one because Move bytecode does not have ADTs.

struct Option<Element> has copy, drop, store

Fields

vec: vector<Element>

Specification

The size of vector is always less than equal to 1 because it's 0 for "none" or 1 for "some".

invariant len(vec) <= 1;

## 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;

## Function `none` Return an empty Option

public fun none<Element>(): option::Option<Element>

Implementation

public fun none<Element>(): Option<Element> {
    Option { vec: vector::empty() }
}

Specification

pragma opaque;
aborts_if false;
ensures result == spec_none<Element>();

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

## 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 { vec: vector::singleton(e) }
}

Specification

pragma opaque;
aborts_if false;
ensures result == spec_some(e);

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

## Function `is_none` Return true if t does not hold a value

public fun is_none<Element>(t: &option::Option<Element>): bool

Implementation

public fun is_none<Element>(t: &Option<Element>): bool {
    vector::is_empty(&t.vec)
}

Specification

pragma opaque;
aborts_if false;
ensures result == is_none(t);

## Function `is_some` Return true if t holds a value

public fun is_some<Element>(t: &option::Option<Element>): bool

Implementation

public fun is_some<Element>(t: &Option<Element>): bool {
    !vector::is_empty(&t.vec)
}

Specification

pragma opaque;
aborts_if false;
ensures result == is_some(t);

## Function `contains` Return true if the value in t is equal to e_ref Always returns false if t does not hold a value

public fun contains<Element>(t: &option::Option<Element>, e_ref: &Element): bool

Implementation

public fun contains<Element>(t: &Option<Element>, e_ref: &Element): bool {
    vector::contains(&t.vec, e_ref)
}

Specification

pragma opaque;
aborts_if false;
ensures result == spec_contains(t, e_ref);

fun spec_contains<Element>(t: Option<Element>, e: Element): bool {
   is_some(t) && borrow(t) == e
}

## Function `borrow` Return an immutable reference to the value inside t Aborts if t does not hold a value

public fun borrow<Element>(t: &option::Option<Element>): &Element

Implementation

public fun borrow<Element>(t: &Option<Element>): &Element {
    assert!(is_some(t), EOPTION_NOT_SET);
    vector::borrow(&t.vec, 0)
}

Specification

pragma opaque;
include AbortsIfNone<Element>;
ensures result == borrow(t);

## Function `borrow_with_default` Return a reference to the value inside t if it holds one Return default_ref if t does not hold a value

public fun borrow_with_default<Element>(t: &option::Option<Element>, default_ref: &Element): &Element

Implementation

public fun borrow_with_default<Element>(t: &Option<Element>, default_ref: &Element): &Element {
    let vec_ref = &t.vec;
    if (vector::is_empty(vec_ref)) default_ref
    else vector::borrow(vec_ref, 0)
}

Specification

pragma opaque;
aborts_if false;
ensures result == (if (is_some(t)) borrow(t) else default_ref);

## Function `get_with_default` Return the value inside t if it holds one Return default if t does not hold a value

public fun get_with_default<Element: copy, drop>(t: &option::Option<Element>, default: Element): Element

Implementation

public fun get_with_default<Element: copy + drop>(
    t: &Option<Element>,
    default: Element,
): Element {
    let vec_ref = &t.vec;
    if (vector::is_empty(vec_ref)) default
    else *vector::borrow(vec_ref, 0)
}

Specification

pragma opaque;
aborts_if false;
ensures result == (if (is_some(t)) borrow(t) else default);

## Function `fill` Convert the none option t to a some option by adding e. Aborts if t already holds a value

public fun fill<Element>(t: &mut option::Option<Element>, e: Element)

Implementation

public fun fill<Element>(t: &mut Option<Element>, e: Element) {
    let vec_ref = &mut t.vec;
    if (vector::is_empty(vec_ref)) vector::push_back(vec_ref, e)
    else abort EOPTION_IS_SET
}

Specification

pragma opaque;
aborts_if is_some(t) with EOPTION_IS_SET;
ensures is_some(t);
ensures borrow(t) == e;

## Function `extract` Convert a some option to a none by removing and returning the value stored inside t Aborts if t does not hold a value

public fun extract<Element>(t: &mut option::Option<Element>): Element

Implementation

public fun extract<Element>(t: &mut Option<Element>): Element {
    assert!(is_some(t), EOPTION_NOT_SET);
    vector::pop_back(&mut t.vec)
}

Specification

pragma opaque;
include AbortsIfNone<Element>;
ensures result == borrow(old(t));
ensures is_none(t);

## Function `borrow_mut` Return a mutable reference to the value inside t Aborts if t does not hold a value

public fun borrow_mut<Element>(t: &mut option::Option<Element>): &mut Element

Implementation

public fun borrow_mut<Element>(t: &mut Option<Element>): &mut Element {
    assert!(is_some(t), EOPTION_NOT_SET);
    vector::borrow_mut(&mut t.vec, 0)
}

Specification

pragma opaque;
include AbortsIfNone<Element>;
ensures result == borrow(t);

## Function `swap` Swap the old value inside t with e and return the old value Aborts if t does not hold a value

public fun swap<Element>(t: &mut option::Option<Element>, e: Element): Element

Implementation

public fun swap<Element>(t: &mut Option<Element>, e: Element): Element {
    assert!(is_some(t), EOPTION_NOT_SET);
    let vec_ref = &mut t.vec;
    let old_value = vector::pop_back(vec_ref);
    vector::push_back(vec_ref, e);
    old_value
}

Specification

pragma opaque;
include AbortsIfNone<Element>;
ensures result == borrow(old(t));
ensures is_some(t);
ensures borrow(t) == e;

## Function `swap_or_fill` Swap the old value inside t 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 t not holding a value.

public fun swap_or_fill<Element>(t: &mut option::Option<Element>, e: Element): option::Option<Element>

Implementation

public fun swap_or_fill<Element>(t: &mut Option<Element>, e: Element): Option<Element> {
    let vec_ref = &mut t.vec;
    let old_value = if (vector::is_empty(vec_ref)) none()
        else some(vector::pop_back(vec_ref));
    vector::push_back(vec_ref, e);
    old_value
}

Specification

pragma opaque;
ensures result == old(t);
ensures borrow(t) == e;

## Function `destroy_with_default` Destroys t. If t holds a value, return it. Returns default otherwise

public fun destroy_with_default<Element: drop>(t: option::Option<Element>, default: Element): Element

Implementation

public fun destroy_with_default<Element: drop>(t: Option<Element>, default: Element): Element {
    let Option { vec } = t;
    if (vector::is_empty(&mut vec)) default
    else vector::pop_back(&mut vec)
}

Specification

pragma opaque;
aborts_if false;
ensures result == (if (is_some(t)) borrow(t) else default);

## Function `destroy_some` Unpack t and return its contents Aborts if t does not hold a value

public fun destroy_some<Element>(t: option::Option<Element>): Element

Implementation

public fun destroy_some<Element>(t: Option<Element>): Element {
    assert!(is_some(&t), EOPTION_NOT_SET);
    let Option { vec } = t;
    let elem = vector::pop_back(&mut vec);
    vector::destroy_empty(vec);
    elem
}

Specification

pragma opaque;
include AbortsIfNone<Element>;
ensures result == borrow(t);

## Function `destroy_none` Unpack t Aborts if t holds a value

public fun destroy_none<Element>(t: option::Option<Element>)

Implementation

public fun destroy_none<Element>(t: Option<Element>) {
    assert!(is_none(&t), EOPTION_IS_SET);
    let Option { vec } = t;
    vector::destroy_empty(vec)
}

Specification

pragma opaque;
aborts_if is_some(t) with EOPTION_IS_SET;

## Function `to_vec` Convert t into a vector of length 1 if it is Some, and an empty vector otherwise

public fun to_vec<Element>(t: option::Option<Element>): vector<Element>

Implementation

public fun to_vec<Element>(t: Option<Element>): vector<Element> {
    let Option { vec } = t;
    vec
}

Specification

pragma opaque;
aborts_if false;
ensures result == t.vec;

## Module Specification

pragma aborts_if_is_strict;

### Helper Schema

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

[//]: # ("File containing references which can be used from documentation")