Struct move_model::ast::Exp

source ·
pub struct Exp { /* private fields */ }
Expand description

An internalized expression. We do use a wrapper around the underlying internement implementation variant to ensure a unique API (LocalIntern and ArcIntern e.g. differ in the presence of the Copy trait, and by wrapping we effectively remove the Copy from LocalIntern).

Methods from Deref<Target = ExpData>§

source

pub fn node_id(&self) -> NodeId

source

pub fn call_args(&self) -> &[Exp]

source

pub fn node_ids(&self) -> Vec<NodeId>

source

pub fn free_vars(&self, env: &GlobalEnv) -> Vec<(Symbol, Type)>

Returns the free local variables, inclusive their types, used in this expression. Result is ordered by occurrence.

source

pub fn used_memory( &self, env: &GlobalEnv ) -> BTreeSet<(QualifiedInstId<StructId>, Option<MemoryLabel>)>

Returns the used memory of this expression.

source

pub fn temporaries(&self, env: &GlobalEnv) -> Vec<(TempIndex, Type)>

Returns the temporaries used in this expression. Result is ordered by occurrence.

source

pub fn visit<F>(&self, visitor: &mut F)where F: FnMut(&ExpData),

Visits expression, calling visitor on each sub-expression, depth first.

source

pub fn any<P>(&self, predicate: &mut P) -> boolwhere P: FnMut(&ExpData) -> bool,

source

pub fn visit_pre_post<F>(&self, visitor: &mut F)where F: FnMut(bool, &ExpData),

Visits expression, calling visitor on each sub-expression. visitor(false, ..) will be called before descending into expression, and visitor(true, ..) after. Notice we use one function instead of two so a lambda can be passed which encapsulates mutable references.

source

pub fn module_usage(&self, usage: &mut BTreeSet<ModuleId>)

Returns the set of module ids used by this expression.

source

pub fn uses_memory<F>(&self, check_pure: &F) -> boolwhere F: Fn(ModuleId, SpecFunId) -> bool,

Determines whether this expression depends on global memory

source

pub fn is_pure(&self, env: &GlobalEnv) -> bool

Checks whether the expression is pure, i.e. does not depend on memory or mutable variables.

source

pub fn display<'a>(&'a self, env: &'a GlobalEnv) -> ExpDisplay<'a>

Creates a display of an expression which can be used in formatting.

Trait Implementations§

source§

impl AsRef<ExpData> for Exp

source§

fn as_ref(&self) -> &ExpData

Converts this type into a shared reference of the (usually inferred) input type.
source§

impl Borrow<ExpData> for Exp

source§

fn borrow(&self) -> &ExpData

Immutably borrows from an owned value. Read more
source§

impl Clone for Exp

source§

fn clone(&self) -> Exp

Returns a copy of the value. Read more
1.0.0 · source§

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source. Read more
source§

impl Debug for Exp

source§

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter. Read more
source§

impl Deref for Exp

§

type Target = ExpData

The resulting type after dereferencing.
source§

fn deref(&self) -> &Self::Target

Dereferences the value.
source§

impl From<Exp> for ExpData

source§

fn from(exp: Exp) -> ExpData

Takes an expression and returns expression data.

source§

impl From<ExpData> for Exp

source§

fn from(data: ExpData) -> Self

Converts to this type from the input type.
source§

impl Hash for Exp

source§

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher. Read more
1.3.0 · source§

fn hash_slice<H>(data: &[Self], state: &mut H)where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher. Read more
source§

impl PartialEq<Exp> for Exp

source§

fn eq(&self, other: &Exp) -> bool

This method tests for self and other values to be equal, and is used by ==.
1.0.0 · source§

fn ne(&self, other: &Rhs) -> bool

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.
source§

impl Eq for Exp

source§

impl StructuralEq for Exp

source§

impl StructuralPartialEq for Exp

Auto Trait Implementations§

§

impl RefUnwindSafe for Exp

§

impl !Send for Exp

§

impl !Sync for Exp

§

impl Unpin for Exp

§

impl UnwindSafe for Exp

Blanket Implementations§

source§

impl<T> Any for Twhere T: 'static + ?Sized,

source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
source§

impl<T> Borrow<T> for Twhere T: ?Sized,

const: unstable · source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
source§

impl<T> BorrowMut<T> for Twhere T: ?Sized,

const: unstable · source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
§

impl<T> CallHasher for Twhere T: Hash + ?Sized,

§

fn get_hash<H, B>(value: &H, build_hasher: &B) -> u64where H: Hash + ?Sized, B: BuildHasher,

source§

impl<Q, K> Equivalent<K> for Qwhere Q: Eq + ?Sized, K: Borrow<Q> + ?Sized,

source§

fn equivalent(&self, key: &K) -> bool

Compare self to key and return true if they are equal.
source§

impl<T> From<T> for T

const: unstable · source§

fn from(t: T) -> T

Returns the argument unchanged.

source§

impl<T, U> Into<U> for Twhere U: From<T>,

const: unstable · source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

source§

impl<T> ToOwned for Twhere T: Clone,

§

type Owned = T

The resulting type after obtaining ownership.
source§

fn to_owned(&self) -> T

Creates owned data from borrowed data, usually by cloning. Read more
source§

fn clone_into(&self, target: &mut T)

Uses borrowed data to replace owned data, usually by cloning. Read more
source§

impl<T, U> TryFrom<U> for Twhere U: Into<T>,

§

type Error = Infallible

The type returned in the event of a conversion error.
const: unstable · source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
source§

impl<T, U> TryInto<U> for Twhere U: TryFrom<T>,

§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
const: unstable · source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
§

impl<V, T> VZip<V> for Twhere V: MultiLane<T>,

§

fn vzip(self) -> V