Backend

hax_rust_engine::backends

Trait Backend 

Source 
pub trait Backend {
    type Printer: Printer;

    const NAME: &'static str = <Self::Printer>::NAME;

    // Required method
    fn module_path(&self, module: &Module) -> Utf8PathBuf;

    // Provided methods
    fn printer(&self) -> Self::Printer { ... }
    fn phases(&self) -> Vec<Box<dyn Phase>> { ... }
    fn items_to_module(&self, items: Vec<Item>) -> Vec<Module> { ... }
}
Expand description

A hax backend.

A backend is responsible for turning the hax AST into sources of a target language. It combines:

  • a sequence of AST transformation phases, and
  • a printer that generates textual output.

For example, we have F*, Coq, and Lean backends. Some are still in the old OCaml engine.

Provided Associated Constants§

Source

const NAME: &'static str = <Self::Printer>::NAME

A short name identifying the backend.

By default, this is delegated to the associated printer’s Printer::NAME.

Required Associated Types§

Source

type Printer: Printer

The printer type used by this backend.

Required Methods§

Source

fn module_path(&self, module: &Module) -> Utf8PathBuf

Compute the relative filesystem path where a given module should be written.

Provided Methods§

Source

fn printer(&self) -> Self::Printer

Construct a new printer instance.

By default this calls Default::default on the printer type.

Source

fn phases(&self) -> Vec<Box<dyn Phase>>

The AST phases to apply before printing.

Backends can override this to add transformations. The default is an empty list (no transformations).

Source

fn items_to_module(&self, items: Vec<Item>) -> Vec<Module>

Group a flat list of items into modules.

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§