Trait move_model::exp_rewriter::ExpRewriterFunctions

source · [−]
pub trait ExpRewriterFunctions {

Show 21 methods    fn rewrite_exp(&mut self, exp: Exp) -> Exp { ... }
    fn rewrite_vec(&mut self, exps: &[Exp]) -> Vec<Exp>ⓘNotable traits for Vec<u8, A>impl<A> Write for Vec<u8, A> where
    A: Allocator,  { ... }
    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

Top-level entry for rewriting an expression. Can be re-implemented to do some pre/post processing embedding a call to do_rewrite.

Implementors