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
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
impl ExpData
pub fn ptr_eq(e1: &Exp, e2: &Exp) -> bool
pub fn node_id(&self) -> NodeId
pub fn call_args(&self) -> &[Exp]
pub fn node_ids(&self) -> Vec<NodeId> ⓘ
sourcepub fn free_vars(&self, env: &GlobalEnv) -> Vec<(Symbol, Type)> ⓘ
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.
sourcepub fn used_memory(
&self,
env: &GlobalEnv
) -> BTreeSet<(QualifiedInstId<StructId>, Option<MemoryLabel>)>
pub fn used_memory( &self, env: &GlobalEnv ) -> BTreeSet<(QualifiedInstId<StructId>, Option<MemoryLabel>)>
Returns the used memory of this expression.
sourcepub fn temporaries(&self, env: &GlobalEnv) -> Vec<(TempIndex, Type)> ⓘ
pub fn temporaries(&self, env: &GlobalEnv) -> Vec<(TempIndex, Type)> ⓘ
Returns the temporaries used in this expression. Result is ordered by occurrence.
sourcepub fn visit<F>(&self, visitor: &mut F)where
F: FnMut(&ExpData),
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) -> boolwhere P: FnMut(&ExpData) -> bool,
sourcepub fn visit_pre_post<F>(&self, visitor: &mut F)where
F: FnMut(bool, &ExpData),
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.
sourcepub fn rewrite<F>(exp: Exp, exp_rewriter: &mut F) -> Expwhere
F: FnMut(Exp) -> Result<Exp, Exp>,
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)
.
sourcepub fn rewrite_node_id<F>(exp: Exp, node_rewriter: &mut F) -> Expwhere
F: FnMut(NodeId) -> Option<NodeId>,
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.
sourcepub 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>,
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
sourcepub fn instantiate_node(
env: &GlobalEnv,
id: NodeId,
targs: &[Type]
) -> Option<NodeId>
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.
sourcepub fn module_usage(&self, usage: &mut BTreeSet<ModuleId>)
pub fn module_usage(&self, usage: &mut BTreeSet<ModuleId>)
Returns the set of module ids used by this expression.
Trait Implementations§
source§impl PartialEq<ExpData> for ExpData
impl PartialEq<ExpData> for ExpData
impl Eq for ExpData
impl StructuralEq for ExpData
impl StructuralPartialEq for ExpData
Auto Trait Implementations§
impl RefUnwindSafe for ExpData
impl !Send for ExpData
impl !Sync for ExpData
impl Unpin for ExpData
impl UnwindSafe for ExpData
Blanket Implementations§
source§impl<Q, K> Equivalent<K> for Qwhere
Q: Eq + ?Sized,
K: Borrow<Q> + ?Sized,
impl<Q, K> Equivalent<K> for Qwhere Q: Eq + ?Sized, K: Borrow<Q> + ?Sized,
source§fn equivalent(&self, key: &K) -> bool
fn equivalent(&self, key: &K) -> bool
key
and return true
if they are equal.