hax_rust_engine/
printer.rs

1//! Printer infrastructure: allocators, traits, and the printing pipeline.
2//!
3//! This module contains the common plumbing that backends and printers rely on
4//! to turn AST values into formatted text:
5//! - [`Allocator`]: a thin wrapper around the `pretty` crate's allocator,
6//!   parameterized by the backend, used to produce [`pretty::Doc`] nodes.
7//! - [`PrettyAst`]: the trait that printers implement to provide per-type
8//!   formatting of Hax AST nodes (re-exported from [`pretty_ast`]).
9//! - The resugaring pipeline: a sequence of local AST rewrites that make
10//!   emitted code idiomatic for the target language before pretty-printing.
11
12use std::ops::Deref;
13
14use crate::{
15    ast::{self, span::Span},
16    attributes::LinkedItemGraph,
17    printer::pretty_ast::ToDocument,
18};
19use ast::visitors::dyn_compatible;
20
21pub mod pretty_ast;
22pub use pretty_ast::PrettyAst;
23
24pub mod render_view;
25
26/// A resugaring is an erased mapper visitor with a name.
27/// A resugaring is a *local* transformation on the AST that produces exclusively `ast::resugared` nodes.
28/// Any involved or non-local transformation should be a phase, not a resugaring.
29///
30/// Backends may provide **multiple resugaring phases** to incrementally refine
31/// the tree into something idiomatic for the target language (e.g., desugaring
32/// pattern sugar into a more uniform core, then resugaring back into target
33/// idioms). Each phase mutates the AST in place and should be small, focused,
34/// and easy to test.
35///
36/// If you add a new phase, make sure it appears in the backend’s
37/// `resugaring_phases()` list in the correct order.
38pub trait Resugaring: for<'a> dyn_compatible::AstVisitorMut<'a> {
39    /// Get the name of the resugar.
40    fn name(&self) -> String;
41}
42
43/// A printer defines a list of resugaring phases.
44pub trait Printer: Sized + PrettyAst<Span> + Default + HasLinkedItemGraph {
45    /// The name of the printer
46    const NAME: &'static str = <Self as PrettyAst<Span>>::NAME;
47}
48
49/// Getter and setter for `LinkedItemGraph`, useful for printers.
50pub trait HasLinkedItemGraph {
51    /// Get a reference of the `LinkedItemGraph`.
52    fn linked_item_graph(&self) -> &LinkedItemGraph;
53    /// Set a `LinkedItemGraph`.
54    fn with_linked_item_graph(self, graph: std::rc::Rc<LinkedItemGraph>) -> Self;
55}
56
57#[derive(Clone, Debug, serde::Serialize, serde::Deserialize)]
58/// Placeholder type for sourcemaps.
59pub struct SourceMap;
60
61/// Helper trait to print AST fragments.
62pub trait Print<T>
63where
64    for<'a> dyn Resugaring: dyn_compatible::AstVisitableMut<'a, T>,
65{
66    /// Print a single AST fragment using this backend.
67    fn print_returning_fragment(&mut self, fragment: T) -> (String, SourceMap, T)
68    where
69        T: ToDocument<Self, Span>;
70
71    /// Print a single AST fragment using this backend.
72    fn print(&mut self, fragment: T) -> (String, SourceMap)
73    where
74        T: ToDocument<Self, Span>;
75}
76
77impl<P: Printer, T> Print<T> for P
78where
79    for<'a> dyn Resugaring: dyn_compatible::AstVisitableMut<'a, T>,
80{
81    fn print_returning_fragment(&mut self, fragment: T) -> (String, SourceMap, T)
82    where
83        T: ToDocument<Self, Span>,
84    {
85        let doc_builder = fragment.to_document(self).into_doc();
86        (
87            doc_builder.deref().pretty(80).to_string(),
88            SourceMap,
89            fragment,
90        )
91    }
92
93    fn print(&mut self, fragment: T) -> (String, SourceMap)
94    where
95        T: ToDocument<Self, Span>,
96    {
97        let (rendered, sourcemap, _) = <Self as Print<_>>::print_returning_fragment(self, fragment);
98        (rendered, sourcemap)
99    }
100}
hax_rust_engine/printer.rs

hax_rust_engine/
printer.rs
