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, rc::Rc};
21
22use crate::{
23    ast::{Item, Metadata, Module, span::Span},
24    attributes::LinkedItemGraph,
25    printer::{HasLinkedItemGraph, Print, Printer},
26};
27use camino::Utf8PathBuf;
28use hax_types::engine_api::File;
29
30/// A hax backend.
31///
32/// A backend is responsible for turning the hax AST into sources of a target language.
33/// It combines:
34/// - a sequence of AST transformation phases, and
35/// - a printer that generates textual output.
36///
37/// For example, we have F\*, Coq, and Lean backends.
38/// Some are still in the old OCaml engine.
39pub trait Backend {
40    /// The printer type used by this backend.
41    type Printer: Printer;
42
43    /// Construct a new printer instance.
44    ///
45    /// By default this calls `Default::default` on the printer type.
46    fn printer(&self, linked_item_graph: Rc<LinkedItemGraph>) -> Self::Printer {
47        Self::Printer::default().with_linked_item_graph(linked_item_graph)
48    }
49
50    /// A short name identifying the backend.
51    ///
52    /// By default, this is delegated to the associated printer's [`Printer::NAME`].
53    const NAME: &'static str = Self::Printer::NAME;
54
55    /// The AST phases to apply before printing.
56    ///
57    /// Backends can override this to add transformations.
58    /// The default is an empty list (no transformations).
59    fn phases(&self) -> Vec<Box<dyn crate::phase::Phase>> {
60        vec![]
61    }
62
63    /// Group a flat list of items into modules.
64    fn items_to_module(&self, items: Vec<Item>) -> Vec<Module> {
65        let mut modules: HashMap<_, Vec<_>> = HashMap::new();
66        for item in items {
67            let module_ident = item.ident.mod_only_closest_parent();
68            modules.entry(module_ident).or_default().push(item);
69        }
70        modules
71            .into_iter()
72            .map(|(ident, items)| Module {
73                ident,
74                items,
75                meta: Metadata {
76                    span: Span::dummy(),
77                    attributes: vec![],
78                },
79            })
80            .collect()
81    }
82
83    /// Compute the relative filesystem path where a given module should be written.
84    fn module_path(&self, module: &Module) -> Utf8PathBuf;
85}
86
87/// Apply a backend to a collection of AST items, producing output files.
88///
89/// This runs all of the backend's [`Backend::phases`], groups the items into
90/// modules via [`Backend::items_to_module`], and then uses the backend's printer
91/// to generate source files with paths determined by [`Backend::module_path`].
92pub fn apply_backend<B: Backend + 'static>(backend: B, mut items: Vec<Item>) -> Vec<File> {
93    for phase in backend.phases() {
94        phase.apply(&mut items);
95    }
96
97    let linked_items_graph = Rc::new(LinkedItemGraph::new(
98        &items,
99        prelude::diagnostics::Context::Printer(B::NAME.into()),
100    ));
101
102    /// Drop any item marked with a hax attribute whose payload deserializes to
103    /// `AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true })`.
104    ///
105    /// Items with such a "late-skip" attribute are typically generated by hax
106    /// attributes.
107    fn drop_skip_late_items(items: &mut Vec<Item>) {
108        items.retain_mut(|item| {
109            use hax_lib_macros_types::{AttrPayload, ItemStatus};
110            !item.meta.hax_attributes().any(|attr| {
111                matches!(
112                    attr,
113                    AttrPayload::ItemStatus(ItemStatus::Included { late_skip: true })
114                )
115            })
116        });
117    }
118
119    drop_skip_late_items(&mut items);
120
121    let modules = backend.items_to_module(items);
122    modules
123        .into_iter()
124        .map(|module: Module| {
125            let path = backend.module_path(&module).into_string();
126            let (contents, _) = backend.printer(linked_items_graph.clone()).print(module);
127            File {
128                path,
129                contents,
130                sourcemap: None,
131            }
132        })
133        .collect()
134}
135
136mod prelude {
137    //! Small "bring-into-scope" set used by backend modules.
138    //!
139    //! Importing this prelude saves repetitive `use` lists in per-backend
140    //! modules without forcing these names on downstream users.
141    pub use super::Backend;
142    pub use crate::ast::{
143        identifiers::{global_id::view::AnyKind, *},
144        literals::*,
145        resugared::*,
146        *,
147    };
148    pub use crate::printer::{
149        pretty_ast::{DocBuilder, PrettyAst, ToDocument, install_pretty_helpers},
150        render_view::*,
151        *,
152    };
153    pub use crate::resugarings::*;
154    pub use crate::symbol::Symbol;
155    pub use hax_rust_engine_macros::{prepend_associated_functions_with, setup_printer_struct};
156}
hax_rust_engine/backends.rs

hax_rust_engine/
backends.rs
