Trait move_model::exp_rewriter::ExpRewriterFunctions
source · pub trait ExpRewriterFunctions {
Show 21 methods
// Provided methods
fn rewrite_exp(&mut self, exp: Exp) -> Exp { ... }
fn rewrite_vec(&mut self, exps: &[Exp]) -> Vec<Exp> ⓘ { ... }
fn rewrite_enter_scope<'a>(
&mut self,
decls: impl Iterator<Item = &'a LocalVarDecl>
) { ... }
fn rewrite_exit_scope(&mut self) { ... }
fn rewrite_node_id(&mut self, id: NodeId) -> Option<NodeId> { ... }
fn rewrite_local_var(&mut self, id: NodeId, sym: Symbol) -> Option<Exp> { ... }
fn rewrite_temporary(&mut self, id: NodeId, idx: TempIndex) -> Option<Exp> { ... }
fn rewrite_value(&mut self, id: NodeId, value: &Value) -> Option<Exp> { ... }
fn rewrite_spec_var(
&mut self,
id: NodeId,
mid: ModuleId,
vid: SpecVarId,
label: &Option<MemoryLabel>
) -> Option<Exp> { ... }
fn rewrite_call(
&mut self,
id: NodeId,
oper: &Operation,
args: &[Exp]
) -> Option<Exp> { ... }
fn rewrite_invoke(
&mut self,
id: NodeId,
target: &Exp,
args: &[Exp]
) -> Option<Exp> { ... }
fn rewrite_lambda(
&mut self,
id: NodeId,
vars: &[LocalVarDecl],
body: &Exp
) -> Option<Exp> { ... }
fn rewrite_block(
&mut self,
id: NodeId,
vars: &[LocalVarDecl],
body: &Exp
) -> Option<Exp> { ... }
fn rewrite_quant(
&mut self,
id: NodeId,
vars: &[(LocalVarDecl, Exp)],
triggers: &[Vec<Exp>],
cond: &Option<Exp>,
body: &Exp
) -> Option<Exp> { ... }
fn rewrite_if_else(
&mut self,
id: NodeId,
cond: &Exp,
then: &Exp,
else_: &Exp
) -> Option<Exp> { ... }
fn rewrite_exp_descent(&mut self, exp: Exp) -> Exp { ... }
fn internal_rewrite_id(&mut self, id: &NodeId) -> (bool, NodeId) { ... }
fn internal_rewrite_exp(&mut self, exp: &Exp) -> (bool, Exp) { ... }
fn internal_rewrite_vec(&mut self, exps: &[Exp]) -> Option<Vec<Exp>> { ... }
fn internal_rewrite_decls(
&mut self,
decls: &[LocalVarDecl]
) -> (bool, Vec<LocalVarDecl>) { ... }
fn internal_rewrite_quant_decls(
&mut self,
decls: &[(LocalVarDecl, Exp)]
) -> (bool, Vec<(LocalVarDecl, Exp)>) { ... }
}Expand description
A general trait for expression rewriting.
This allows customization by re-implementing any of the rewrite_local_var,
rewrite_temporary, etc. functions. Each expression node has an equivalent of such
a function.
This rewriter takes care of preserving sharing between expressions: only expression trees which are actually modified are reconstructed.
For most rewriting problems, there are already specializations of this trait, like ExpRewriter
in this module, and Exp::rewrite in the AST module.
When custom implementing this trait, consider the semantics of the generic logic used.
When any of the rewrite_<exp-variant> functions is called, any arguments have been already
recursively rewritten, inclusive of the passed node id. To implement a pre-descent
transformation, you need to implement the rewrite_exp function and after pre-processing,
continue (or not) descent with rewrite_exp_descent for sub-expressions.
Provided Methods§
sourcefn rewrite_exp(&mut self, exp: Exp) -> Exp
fn rewrite_exp(&mut self, exp: Exp) -> Exp
Top-level entry for rewriting an expression. Can be re-implemented to do some
pre/post processing embedding a call to do_rewrite.