Trait move_model::simplifier::SpecRewriter

source · [−]
pub trait SpecRewriter {
    fn rewrite_module_spec(
        &mut self, 
        _env: &GlobalEnv, 
        _module_id: ModuleId, 
        _spec: &Spec
    ) -> Result<Option<Spec>> { ... }
    fn rewrite_function_spec(
        &mut self, 
        _env: &GlobalEnv, 
        _fun_id: QualifiedId<FunId>, 
        _spec: &Spec
    ) -> Result<Option<Spec>> { ... }
    fn rewrite_inline_spec(
        &mut self, 
        _env: &GlobalEnv, 
        _fun_id: QualifiedId<FunId>, 
        _code_offset: CodeOffset, 
        _spec: &Spec
    ) -> Result<Option<Spec>> { ... }
    fn override_with_rewrite(&mut self, env: &mut GlobalEnv) -> Result<()> { ... }
}
Expand description

A generic trait for rewriting the specifications in the GlobalEnv. A rewriter is expected to implement at least one rewrite_* function, depending on which type(s) of specs the rewriter targets. All the rewrite_* function should follow the convention on return value:

  • Ok(None) –> nothing to rewrite on this spec
  • Ok(Some(new_spec)) –> the spec is re-written and the new_spec is the output
  • Err(..) –> something wrong (invariant violation) happened in the rewriting

Provided methods

Rewrite a module-level specification

Rewrite a function-level specification

Rewrite a code-level specification

Iterate over the specs in the GlobalEnv, rewrite each spec, and apply changes back to the GlobalEnv.

Implementors