hax_rust_engine/
backends.rs

1//! Code generation backends.
2//!
3//! A backend is consititued of:
4//!  - a list of AST transformations to apply, those are called phases.
5//!  - and a printer.
6//!
7//! This top-level module is mostly an index of available backends and a
8//! small prelude to make backend modules concise.
9//!
10//! # Adding a new backend
11//! 1. Create a submodule under `src/backends/`, e.g. `foo.rs`.
12//! 2. Put your printer and backend there.
13//! 3. Re-export it here with `pub mod foo;`.
14//!
15//! See [`rust`] for an example implementation.
16
17pub mod lean;
18pub mod rust;
19
20use std::collections::HashMap;
21
22use crate::{
23    ast::{Item, Metadata, Module, span::Span},
24    printer::{Print, Printer},
25};
26use camino::Utf8PathBuf;
27use hax_types::engine_api::File;
28
29/// A hax backend.
30///
31/// A backend is responsible for turning the hax AST into sources of a target language.
32/// It combines:
33/// - a sequence of AST transformation phases, and
34/// - a printer that generates textual output.
35///
36/// For example, we have F\*, Coq, and Lean backends.
37/// Some are still in the old OCaml engine.
38pub trait Backend {
39    /// The printer type used by this backend.
40    type Printer: Printer;
41
42    /// Construct a new printer instance.
43    ///
44    /// By default this calls `Default::default` on the printer type.
45    fn printer(&self) -> Self::Printer {
46        Self::Printer::default()
47    }
48
49    /// A short name identifying the backend.
50    ///
51    /// By default, this is delegated to the associated printer's [`Printer::NAME`].
52    const NAME: &'static str = Self::Printer::NAME;
53
54    /// The AST phases to apply before printing.
55    ///
56    /// Backends can override this to add transformations.
57    /// The default is an empty list (no transformations).
58    fn phases(&self) -> Vec<Box<dyn crate::phase::Phase>> {
59        vec![]
60    }
61
62    /// Group a flat list of items into modules.
63    fn items_to_module(&self, items: Vec<Item>) -> Vec<Module> {
64        let mut modules: HashMap<_, Vec<_>> = HashMap::new();
65        for item in items {
66            let module_ident = item.ident.mod_only_closest_parent();
67            modules.entry(module_ident).or_default().push(item);
68        }
69        modules
70            .into_iter()
71            .map(|(ident, items)| Module {
72                ident,
73                items,
74                meta: Metadata {
75                    span: Span::dummy(),
76                    attributes: vec![],
77                },
78            })
79            .collect()
80    }
81
82    /// Compute the relative filesystem path where a given module should be written.
83    fn module_path(&self, module: &Module) -> Utf8PathBuf;
84}
85
86/// Apply a backend to a collection of AST items, producing output files.
87///
88/// This runs all of the backend's [`Backend::phases`], groups the items into
89/// modules via [`Backend::items_to_module`], and then uses the backend's printer
90/// to generate source files with paths determined by [`Backend::module_path`].
91pub fn apply_backend<B: Backend + 'static>(backend: B, mut items: Vec<Item>) -> Vec<File> {
92    for phase in backend.phases() {
93        phase.apply(&mut items);
94    }
95
96    let modules = backend.items_to_module(items);
97    modules
98        .into_iter()
99        .map(|module: Module| {
100            let path = backend.module_path(&module).into_string();
101            let (contents, _) = backend.printer().print(module);
102            File {
103                path,
104                contents,
105                sourcemap: None,
106            }
107        })
108        .collect()
109}
110
111#[allow(unused)]
112mod prelude {
113    //! Small "bring-into-scope" set used by backend modules.
114    //!
115    //! Importing this prelude saves repetitive `use` lists in per-backend
116    //! modules without forcing these names on downstream users.
117    pub use super::Backend;
118    pub use crate::ast::identifiers::global_id::view::AnyKind;
119    pub use crate::ast::identifiers::*;
120    pub use crate::ast::literals::*;
121    pub use crate::ast::resugared::*;
122    pub use crate::ast::*;
123    pub use crate::printer::render_view::*;
124    pub use crate::printer::*;
125    pub use crate::symbol::Symbol;
126    pub use hax_rust_engine_macros::prepend_associated_functions_with;
127    pub use pretty::DocAllocator;
128    pub use pretty::DocBuilder;
129    pub use pretty::Pretty;
130    pub use pretty_ast::install_pretty_helpers;
131}
hax_rust_engine/backends.rs

hax_rust_engine/
backends.rs
