Rust Engine: add a Backend trait

cli/subcommands/src/cargo_hax.rs

@@ -264,13 +264,13 @@ fn run_engine(
         input: haxmeta.items,
         impl_infos: haxmeta.impl_infos,
     };
-    let mut hax_engine_command = if let Backend::Lean { .. }
-    | Backend::GenerateRustEngineNames { .. } =
-        &engine_options.backend.backend
-    {
-        find_rust_hax_engine(message_format)
-    } else {
-        find_hax_engine(message_format)
+    let mut hax_engine_command = match &engine_options.backend.backend {
+        Backend::Fstar(_)
+        | Backend::Coq
+        | Backend::Ssprove
+        | Backend::Easycrypt
+        | Backend::ProVerif(_) => find_hax_engine(message_format),
+        _ => find_rust_hax_engine(message_format),
     };
     let mut engine_subprocess = hax_engine_command
         .stdin(std::process::Stdio::piped())

engine/bin/lib.ml

@@ -141,16 +141,18 @@ let run (options : Types.engine_options) : Types.output =
         | Coq -> run (module Coq_backend) ()
         | Ssprove -> run (module Ssprove_backend) ()
         | Easycrypt -> run (module Easycrypt_backend) ()
-        | Lean ->
-            failwith
-              "The OCaml hax engine should never be called for lean. The Lean \
-               backend uses the newer rust engine. Please report this issue on \
-               our GitHub repository: https://github.com/cryspen/hax."
         | GenerateRustEngineNames ->
             failwith
               "The OCaml hax engine should never be called with \
                `GenerateRustEngineNames`, it is an rust engine only internal \
-               command.")
+               command."
+        | backend ->
+            failwith
+              ("The OCaml hax engine should never be called with backend `"
+              ^ [%show: Types.backend_for__null] backend
+              ^ "`. This backend uses the newer rust engine. Please report \
+                 this issue on our GitHub repository: \
+                 https://github.com/cryspen/hax."))
   in
   {
     diagnostics = List.map ~f:Diagnostics.to_thir_diagnostic diagnostics;

hax-types/src/cli_options/mod.rs

@@ -185,6 +185,9 @@ pub enum Backend<E: Extension> {
     /// Use the Lean backend (warning: work in progress!)
     #[clap(hide = true)]
     Lean,
+    /// Use the Rust backend (warning: work in progress!)
+    #[clap(hide = true)]
+    Rust,
     /// Extract `DefId`s of the crate as a Rust module tree.
     /// This is a command that regenerates code for the rust engine.
     #[clap(hide = true)]
@@ -200,6 +203,7 @@ impl fmt::Display for Backend<()> {
             Backend::Easycrypt { .. } => write!(f, "easycrypt"),
             Backend::ProVerif { .. } => write!(f, "proverif"),
             Backend::Lean { .. } => write!(f, "lean"),
+            Backend::Rust { .. } => write!(f, "rust"),
             Backend::GenerateRustEngineNames { .. } => write!(f, "generate_rust_engine_names"),
         }
     }

rust-engine/Cargo.toml

@@ -21,3 +21,4 @@ pretty = "0.12"
 itertools.workspace = true
 derive_generic_visitor = { git = "https://github.com/W95Psp/derive-generic-visitor.git", branch = "visitable-group-add-attrs" }
 pastey = "0.1.0"
+camino = "1.1.11"

rust-engine/src/backends.rs

@@ -14,14 +14,103 @@
 //!
 //! See [`rust`] for an example implementation.
 
+pub mod lean;
 pub mod rust;
 
+use crate::{
+    ast::{Item, Metadata, Module, span::Span},
+    printer::{Print, Printer},
+};
+use camino::Utf8PathBuf;
+use hax_types::engine_api::File;
+
+/// 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.
+pub trait Backend {
+    /// The printer type used by this backend.
+    type Printer: Printer;
+
+    /// Construct a new printer instance.
+    ///
+    /// By default this calls `Default::default` on the printer type.
+    fn printer(&self) -> Self::Printer {
+        Self::Printer::default()
+    }
+
+    /// A short name identifying the backend.
+    ///
+    /// By default, this is delegated to the associated printer's [`Printer::NAME`].
+    const NAME: &'static str = Self::Printer::NAME;
+
+    /// The AST phases to apply before printing.
+    ///
+    /// Backends can override this to add transformations.  
+    /// The default is an empty list (no transformations).
+    fn phases(&self) -> Vec<Box<dyn crate::phase::Phase>> {
+        vec![]
+    }
+
+    /// Group a flat list of items into modules.
+    ///
+    /// By default, everything is packed into a single module, since we
+    /// don't yet support proper name rendering (see issue #1599).
+    fn items_to_module(&self, items: Vec<Item>) -> Vec<Module> {
+        let Some(first) = items.first() else {
+            return vec![];
+        };
+        vec![Module {
+            ident: first.ident.clone(),
+            items,
+            meta: Metadata {
+                span: Span::dummy(),
+                attributes: vec![],
+            },
+        }]
+    }
+
+    /// Compute the relative filesystem path where a given module should be written.
+    fn module_path(&self, module: &Module) -> Utf8PathBuf;
+}
+
+/// Apply a backend to a collection of AST items, producing output files.
+///
+/// This runs all of the backend's [`Backend::phases`], groups the items into
+/// modules via [`Backend::items_to_module`], and then uses the backend's printer
+/// to generate source files with paths determined by [`Backend::module_path`].
+pub fn apply_backend<B: Backend + 'static>(backend: B, mut items: Vec<Item>) -> Vec<File> {
+    for phase in backend.phases() {
+        phase.apply(&mut items);
+    }
+
+    let modules = backend.items_to_module(items);
+    modules
+        .into_iter()
+        .map(|module: Module| {
+            let path = backend.module_path(&module).into_string();
+            let (contents, _) = backend.printer().print(module);
+            File {
+                path,
+                contents,
+                sourcemap: None,
+            }
+        })
+        .collect()
+}
+
 #[allow(unused)]
 mod prelude {
     //! Small "bring-into-scope" set used by backend modules.
     //!
     //! Importing this prelude saves repetitive `use` lists in per-backend
     //! modules without forcing these names on downstream users.
+    pub use super::Backend;
     pub use crate::ast::*;
     pub use crate::printer::*;
     pub use hax_rust_engine_macros::prepend_associated_functions_with;

rust-engine/src/lean.rs → rust-engine/src/backends/lean.rs

@@ -5,14 +5,110 @@
 //! source maps).
 
 use crate::ast::span::Span;
-use crate::printer::Allocator;
 
 use pretty::{DocAllocator, DocBuilder, Pretty, docs};
 
 use crate::ast::identifiers::*;
 use crate::ast::literals::*;
 use crate::ast::*;
 
+// Note: this module was moved here temporarly.
+// This module used to provide a wrapper type `Allocator`.
+// This wrapper type is no longer useful.
+// It was thus removed from the `printer`, and moved here, where it is still used.
+// This is temporary: see https://github.com/cryspen/hax/issues/1604.
+mod deprecated_allocator_module {
+    //! This module provides a custom [`pretty`] allocator, indexed by a printer,
+    //! enabling multiple printers to cohexist and to implement the type `Pretty`.
+
+    use crate::ast::span::Span;
+    use pretty::*;
+
+    /// A printer-specific [`pretty`] allocator.
+    pub struct Allocator<Printer> {
+        /// The pretty allocator
+        allocator: BoxAllocator,
+        /// Extra printer-specific context
+        pub printer: Printer,
+    }
+
+    impl<Printer> Allocator<Printer> {
+        /// Creates a new allocator from a printer.
+        pub fn new(printer: Printer) -> Self {
+            Self {
+                allocator: BoxAllocator,
+                printer,
+            }
+        }
+    }
+
+    impl<'a, P, A: 'a> DocAllocator<'a, A> for Allocator<P> {
+        type Doc = <BoxAllocator as DocAllocator<'a, A>>::Doc;
+
+        fn alloc(&'a self, doc: Doc<'a, Self::Doc, A>) -> Self::Doc {
+            self.allocator.alloc(doc)
+        }
+
+        fn alloc_column_fn(
+            &'a self,
+            f: impl Fn(usize) -> Self::Doc + 'a,
+        ) -> <Self::Doc as DocPtr<'a, A>>::ColumnFn {
+            self.allocator.alloc_column_fn(f)
+        }
+
+        fn alloc_width_fn(
+            &'a self,
+            f: impl Fn(isize) -> Self::Doc + 'a,
+        ) -> <Self::Doc as DocPtr<'a, A>>::WidthFn {
+            self.allocator.alloc_width_fn(f)
+        }
+    }
+
+    /// A helper type used to manually implement `Pretty` for types that carry spans.
+    ///
+    /// By default, we implement the `Pretty` trait for all span-carrying
+    /// types. These implementations annotate spans in the generated document, allowing
+    /// source spans to be produced during pretty-printing. However, this default behavior
+    /// does not provide access to the underlying data, which is sometimes necessary
+    /// for custom printing logic.
+    ///
+    /// For example, when printing an item, it's often useful to access its attributes.
+    /// To support this, the default `Pretty` implementations delegate to `Manual<Item>`,
+    /// which allows printers to access the inner value directly.
+    ///
+    /// In practice, calling `expr.pretty(..)` will internally use
+    /// `Manual(expr).pretty(..)`, enabling more flexible control over printing behavior.
+    struct Manual<T>(T);
+
+    use crate::ast::*;
+    macro_rules! impl_pretty_kind_meta {
+        ($($type:ty),*) => {
+            $(impl<'a, 'b, P> Pretty<'a, Allocator<P>, Span> for &'b $type
+            where
+                Manual<&'b $type>: Pretty<'a, Allocator<P>, Span>,
+            {
+                fn pretty(self, allocator: &'a Allocator<P>) -> DocBuilder<'a, Allocator<P>, Span> {
+                    let doc = Manual(self).pretty(allocator);
+                    doc.annotate(self.span())
+                }
+            })*
+        };
+    }
+    impl_pretty_kind_meta!(
+        Item,
+        Expr,
+        Pat,
+        Guard,
+        Arm,
+        ImplItem,
+        TraitItem,
+        GenericParam,
+        Attribute
+    );
+}
+
+pub use deprecated_allocator_module::Allocator;
+
 macro_rules! print_todo {
     ($allocator:ident) => {
         $allocator

rust-engine/src/backends/rust.rs

@@ -3,19 +3,33 @@
 
 use super::prelude::*;
 
-/// The Rust backend and printer.
-pub struct Rust;
+/// The Rust printer.
+#[derive(Default)]
+pub struct RustPrinter;
+impl_doc_allocator_for!(RustPrinter);
 
-impl Printer for Rust {
+impl Printer for RustPrinter {
     fn resugaring_phases() -> Vec<Box<dyn Resugaring>> {
         vec![]
     }
 
-    const NAME: &str = "Rust";
+    const NAME: &'static str = "Rust";
 }
 
 const INDENT: isize = 4;
 
+/// The Rust backend.
+pub struct RustBackend;
+
+impl Backend for RustBackend {
+    type Printer = RustPrinter;
+
+    fn module_path(&self, _module: &Module) -> camino::Utf8PathBuf {
+        // TODO: dummy path for now, until we have GlobalId rendering (see #1599).
+        camino::Utf8PathBuf::from("dummy.rs")
+    }
+}
+
 #[prepend_associated_functions_with(install_pretty_helpers!(self: Self))]
 // Note: the `const` wrapping makes my IDE and LSP happy. Otherwise, I don't get
 // autocompletion of methods in the impl block below.
@@ -28,7 +42,7 @@ const _: () = {
     #[allow(unused)]
     macro_rules! concat {($($tt:tt)*) => {disambiguated_concat!($($tt)*)};}
 
-    impl<'a, 'b, A: 'a + Clone> PrettyAst<'a, 'b, A> for Allocator<Rust> {
+    impl<'a, 'b, A: 'a + Clone> PrettyAst<'a, 'b, A> for RustPrinter {
         fn module(&'a self, module: &'b Module) -> pretty::DocBuilder<'a, Self, A> {
             intersperse!(&module.items, docs![hardline!(), hardline!()])
         }

rust-engine/src/lib.rs

@@ -11,8 +11,8 @@
 pub mod ast;
 pub mod backends;
 pub mod hax_io;
-pub mod lean;
 pub mod names;
 pub mod ocaml_engine;
+pub mod phase;
 pub mod printer;
 pub mod symbol;