Skip to main content

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, linked_item_graph: Rc<LinkedItemGraph>) -> Self::Printer { ... }
    fn phases(&self) -> Vec<PhaseKind> { ... }
    fn resugaring_phases() -> Vec<Box<dyn Resugaring>> { ... }
    fn items_to_module(&self, items: Vec<Item>) -> Vec<Module> { ... }
    fn modules_to_files(
        &self,
        modules: Vec<Module>,
        printer: Self::Printer,
    ) -> Vec<File> { ... }
}
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, linked_item_graph: Rc<LinkedItemGraph>) -> Self::Printer

Construct a new printer instance.

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

Source

fn phases(&self) -> Vec<PhaseKind>

The AST phases to apply before printing.

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

Source

fn resugaring_phases() -> Vec<Box<dyn Resugaring>>

A list of resugaring phases.

Source

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

Group a flat list of items into modules.

Source

fn modules_to_files( &self, modules: Vec<Module>, printer: Self::Printer, ) -> Vec<File>

Print a list of modules into files

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors§