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::ast::{self, span::Span};
15use ast::visitors::dyn_compatible;
16use pretty::Pretty;
17
18pub mod pretty_ast;
19pub use pretty_ast::PrettyAst;
20
21pub mod render_view;
22
23/// Implements `pretty::DocAllocator<'a, A>` for a local types
24/// that already implement `HasAllocator<'a, A>`.
25///
26/// Usage:
27///   impl_doc_allocator_for!(MyType);
28///
29/// Notes:
30/// - Types must be local to your crate (orphan rule).
31#[macro_export]
32macro_rules! impl_doc_allocator_for {
33    ($ty:ty) => {
34        impl<'a, A: 'a> ::pretty::DocAllocator<'a, A> for $ty {
35            type Doc = pretty::BoxDoc<'a, A>;
36
37            fn alloc(&'a self, doc: ::pretty::Doc<'a, Self::Doc, A>) -> Self::Doc {
38                pretty::BoxAllocator.alloc(doc)
39            }
40
41            fn alloc_column_fn(
42                &'a self,
43                f: impl Fn(usize) -> Self::Doc + 'a,
44            ) -> <Self::Doc as ::pretty::DocPtr<'a, A>>::ColumnFn {
45                pretty::BoxAllocator.alloc_column_fn(f)
46            }
47
48            fn alloc_width_fn(
49                &'a self,
50                f: impl Fn(isize) -> Self::Doc + 'a,
51            ) -> <Self::Doc as ::pretty::DocPtr<'a, A>>::WidthFn {
52                pretty::BoxAllocator.alloc_width_fn(f)
53            }
54        }
55    };
56}
57pub use impl_doc_allocator_for;
58
59/// A resugaring is an erased mapper visitor with a name.
60/// A resugaring is a *local* transformation on the AST that produces exclusively `ast::resugared` nodes.
61/// Any involved or non-local transformation should be a phase, not a resugaring.
62///
63/// Backends may provide **multiple resugaring phases** to incrementally refine
64/// the tree into something idiomatic for the target language (e.g., desugaring
65/// pattern sugar into a more uniform core, then resugaring back into target
66/// idioms). Each phase mutates the AST in place and should be small, focused,
67/// and easy to test.
68///
69/// If you add a new phase, make sure it appears in the backend’s
70/// `resugaring_phases()` list in the correct order.
71pub trait Resugaring: for<'a> dyn_compatible::AstVisitorMut<'a> {
72    /// Get the name of the resugar.
73    fn name(&self) -> String;
74}
75
76/// A printer defines a list of resugaring phases.
77pub trait Printer: Sized + for<'a, 'b> PrettyAst<'a, 'b, Span> + Default {
78    /// A list of resugaring phases.
79    fn resugaring_phases() -> Vec<Box<dyn Resugaring>>;
80    /// The name of the printer
81    const NAME: &'static str = <Self as PrettyAst<'static, 'static, Span>>::NAME;
82}
83
84/// Placeholder type for sourcemaps.
85pub struct SourceMap;
86
87/// Helper trait to print AST fragments.
88pub trait Print<T>: Printer {
89    /// Print a single AST fragment using this backend.
90    fn print(&self, mut fragment: T) -> (String, SourceMap)
91    where
92        for<'a, 'b> &'b T: Pretty<'a, Self, Span>,
93        // The following node is equivalent to "T is an AST node"
94        for<'a> dyn Resugaring: dyn_compatible::AstVisitableMut<'a, T>,
95    {
96        for mut reguaring_phase in Self::resugaring_phases() {
97            reguaring_phase.visit(&mut fragment)
98        }
99        let doc_builder = fragment.pretty(self).into_doc();
100        (doc_builder.deref().pretty(80).to_string(), SourceMap)
101    }
102}
103impl<P: Printer, T> Print<T> for P {}
hax_rust_engine/printer.rs

hax_rust_engine/
printer.rs
