Struct move_model::ast::Exp

pub struct Exp { /* private fields */ }

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>

pub fn node_id(&self) -> NodeId

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

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

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.

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

Returns the used memory of this expression.

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

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

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

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

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

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.

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

Returns the set of module ids used by this expression.

pub fn extract_ghost_mem_access(
    &self,
    env: &GlobalEnv
) -> Option<(QualifiedInstId<StructId>, FieldId, Exp)>

Extract access to ghost memory from expression. Returns a tuple of the instantiated struct, the field of the selected value, and the expression with the address of the access.

pub fn struct_usage(&self, usage: &mut BTreeSet<QualifiedId<StructId>>)

Collect struct-related operations

pub fn field_usage(
    &self,
    usage: &mut BTreeSet<(QualifiedId<StructId>, FieldId)>
)

Collect field-related operations

pub fn vector_usage(&self, usage: &mut HashSet<Operation>)

Collect vector-related operations

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

Determines whether this expression depends on global memory

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

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

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

impl AsRef<ExpData> for Exp

fn as_ref(&self) -> &ExpData

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

impl Borrow<ExpData> for Exp

fn borrow(&self) -> &ExpData

Immutably borrows from an owned value.

impl Clone for Exp

fn clone(&self) -> Exp

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for Exp

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

Formats the value using the given formatter.

impl Deref for Exp

type Target = ExpData

The resulting type after dereferencing.

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

Dereferences the value.

impl From<Exp> for ExpData

fn from(exp: Exp) -> ExpData

Takes an expression and returns expression data.

impl From<ExpData> for Exp

fn from(data: ExpData) -> Self

Converts to this type from the input type.

impl Hash for Exp

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

Feeds this value into the given Hasher.

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

Feeds a slice of this type into the given Hasher.

impl PartialEq<Exp> for Exp

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

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

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

This method tests for !=.

impl Eq for Exp

impl StructuralEq for Exp

impl StructuralPartialEq for Exp