Struct LeanDemo 

pub struct LeanDemo { /* private fields */ }

Demo struct showing hash-consing performance in WASM

Implementations

impl LeanDemo

pub fn new() -> Self

Create a new Lean demo instance

pub fn create_variable(&mut self, index: u32) -> bool

Demonstrate hash-consing: creating same term twice reuses memory Returns true if successful

pub fn demonstrate_hash_consing(&mut self) -> bool

Create two identical variables and verify they share the same ID Returns true if hash-consing worked (same IDs)

pub fn get_stats(&self) -> String

Get statistics about the arena (number of unique terms)

pub fn create_type(&mut self) -> bool

Create a simple type (Type universe)

pub fn create_identity_function(&mut self) -> bool

Create a lambda abstraction (x : Type) => x

pub fn benchmark_equality(&mut self) -> String

Verify that hash-consing provides O(1) equality

Trait Implementations

impl From<LeanDemo> for JsValue

fn from(value: LeanDemo) -> Self

Converts to this type from the input type.

impl FromWasmAbi for LeanDemo

type Abi = u32

The Wasm ABI type that this converts from when coming back out from the ABI boundary.

unsafe fn from_abi(js: u32) -> Self

Recover a Self from Self::Abi.

impl IntoWasmAbi for LeanDemo

type Abi = u32

The Wasm ABI type that this converts into when crossing the ABI boundary.

fn into_abi(self) -> u32

Convert self into Self::Abi so that it can be sent across the wasm ABI boundary.

impl LongRefFromWasmAbi for LeanDemo

type Abi = u32

Same as RefFromWasmAbi::Abi

type Anchor = RcRef<LeanDemo>

Same as RefFromWasmAbi::Anchor

unsafe fn long_ref_from_abi(js: Self::Abi) -> Self::Anchor

Same as RefFromWasmAbi::ref_from_abi

impl OptionFromWasmAbi for LeanDemo

fn is_none(abi: &Self::Abi) -> bool

Tests whether the argument is a “none” instance. If so it will be deserialized as None, and otherwise it will be passed to FromWasmAbi.

impl OptionIntoWasmAbi for LeanDemo

fn none() -> Self::Abi

Returns an ABI instance indicating “none”, which JS will interpret as the None branch of this option.

impl RefFromWasmAbi for LeanDemo

type Abi = u32

The Wasm ABI type references to Self are recovered from.

type Anchor = RcRef<LeanDemo>

The type that holds the reference to Self for the duration of the invocation of the function that has an &Self parameter. This is required to ensure that the lifetimes don’t persist beyond one function call, and so that they remain anonymous.

unsafe fn ref_from_abi(js: Self::Abi) -> Self::Anchor

Recover a Self::Anchor from Self::Abi.

impl RefMutFromWasmAbi for LeanDemo

type Abi = u32

Same as RefFromWasmAbi::Abi

type Anchor = RcRefMut<LeanDemo>

Same as RefFromWasmAbi::Anchor

unsafe fn ref_mut_from_abi(js: Self::Abi) -> Self::Anchor

Same as RefFromWasmAbi::ref_from_abi

impl TryFromJsValue for LeanDemo

type Error = JsValue

The type returned in the event of a conversion error.

fn try_from_js_value(value: JsValue) -> Result<Self, Self::Error>

Performs the conversion.

impl VectorFromWasmAbi for LeanDemo

type Abi = <Box<[JsValue]> as FromWasmAbi>::Abi

unsafe fn vector_from_abi(js: Self::Abi) -> Box<[LeanDemo]>

impl VectorIntoWasmAbi for LeanDemo

type Abi = <Box<[JsValue]> as IntoWasmAbi>::Abi

fn vector_into_abi(vector: Box<[LeanDemo]>) -> Self::Abi

impl WasmDescribe for LeanDemo

fn describe()

impl WasmDescribeVector for LeanDemo

fn describe_vector()

impl SupportsConstructor for LeanDemo

impl SupportsInstanceProperty for LeanDemo

impl SupportsStaticProperty for LeanDemo