Enum move_model::ast::ExpData

source ·
pub enum ExpData {
    Invalid(NodeId),
    Value(NodeId, Value),
    LocalVar(NodeId, Symbol),
    Temporary(NodeId, TempIndex),
    SpecVar(NodeId, ModuleId, SpecVarId, Option<MemoryLabel>),
    Call(NodeId, Operation, Vec<Exp>),
    Invoke(NodeId, Exp, Vec<Exp>),
    Lambda(NodeId, Vec<LocalVarDecl>, Exp),
    Quant(NodeId, QuantKind, Vec<(LocalVarDecl, Exp)>, Vec<Vec<Exp>>, Option<Exp>, Exp),
    Block(NodeId, Vec<LocalVarDecl>, Exp),
    IfElse(NodeId, Exp, Exp, Exp),
}
Expand description

The type of expression data.

Expression layout follows the following design principles:

  • We try to keep the number of expression variants minimal, for easier treatment in generic traversals. Builtin and user functions are abstracted into a general Call(.., operation, args) construct.
  • Each expression has a unique node id assigned. This id allows to build attribute tables for additional information, like expression type and source location. The id is globally unique.

Variants§

§

Invalid(NodeId)

Represents an invalid expression. This is used as a stub for algorithms which generate expressions but can fail with multiple errors, like a translator from some other source into expressions. Consumers of expressions should assume this variant is not present and can panic when seeing it.

§

Value(NodeId, Value)

Represents a value.

§

LocalVar(NodeId, Symbol)

Represents a reference to a local variable introduced by a specification construct, e.g. a quantifier.

§

Temporary(NodeId, TempIndex)

Represents a reference to a temporary used in bytecode.

§

SpecVar(NodeId, ModuleId, SpecVarId, Option<MemoryLabel>)

Represents a reference to a global specification (ghost) variable.

§

Call(NodeId, Operation, Vec<Exp>)

Represents a call to an operation. The Operation enum covers all builtin functions (including operators, constants, …) as well as user functions.

§

Invoke(NodeId, Exp, Vec<Exp>)

Represents an invocation of a function value, as a lambda.

§

Lambda(NodeId, Vec<LocalVarDecl>, Exp)

Represents a lambda.

§

Quant(NodeId, QuantKind, Vec<(LocalVarDecl, Exp)>, Vec<Vec<Exp>>, Option<Exp>, Exp)

Tuple Fields

§2: Vec<(LocalVarDecl, Exp)>

Ranges

§3: Vec<Vec<Exp>>

Triggers

§4: Option<Exp>

Optional where clause

Represents a quantified formula over multiple variables and ranges.

§

Block(NodeId, Vec<LocalVarDecl>, Exp)

Represents a block which contains a set of variable bindings and an expression for which those are defined.

§

IfElse(NodeId, Exp, Exp, Exp)

Represents a conditional.

Implementations§

source§

impl ExpData

source

pub fn into_exp(self) -> Exp

Version of into which does not require type annotations.

source

pub fn ptr_eq(e1: &Exp, e2: &Exp) -> bool

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 rewrite<F>(exp: Exp, exp_rewriter: &mut F) -> Expwhere F: FnMut(Exp) -> Result<Exp, Exp>,

Rewrites this expression and sub-expression based on the rewriter function. The function returns Ok(e) if the expression is rewritten, and passes back ownership using Err(e) if the expression stays unchanged. This function stops traversing on Ok(e) and descents into sub-expressions on Err(e).

source

pub fn rewrite_node_id<F>(exp: Exp, node_rewriter: &mut F) -> Expwhere F: FnMut(NodeId) -> Option<NodeId>,

Rewrites the node ids in the expression. This is used to rewrite types of expressions.

source

pub fn rewrite_exp_and_node_id<F, G>( exp: Exp, exp_rewriter: &mut F, node_rewriter: &mut G ) -> Expwhere F: FnMut(Exp) -> Result<Exp, Exp>, G: FnMut(NodeId) -> Option<NodeId>,

Rewrites the expression and for unchanged sub-expressions, the node ids in the expression

source

pub fn instantiate_node( env: &GlobalEnv, id: NodeId, targs: &[Type] ) -> Option<NodeId>

A function which can be used for Exp::rewrite_node_id to instantiate types in an expression based on a type parameter instantiation.

source

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

Returns the set of module ids used by this expression.

source§

impl ExpData

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§

impl ExpData

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§

impl ExpData

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 ExpData

source§

fn clone(&self) -> ExpData

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 ExpData

source§

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

Formats the value using the given formatter. Read more
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 ExpData

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<ExpData> for ExpData

source§

fn eq(&self, other: &ExpData) -> 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 ExpData

source§

impl StructuralEq for ExpData

source§

impl StructuralPartialEq for ExpData

Auto Trait Implementations§

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