hax_rust_engine/printer/
pretty_ast.rs

1//! Pretty-printing support for the hax AST.
2//!
3//! This module defines the trait [`PrettyAst`], which is the **primary trait a printer should
4//! implement**.
5//!
6//! # Quickstart
7//! In most printers you:
8//! 1. Implement [`Printer`] for your printer type,
9//! 2. Implement [`PrettyAst`] for that printer type,
10//! 3. Call `ast_value.to_document(&print)` on AST values.
11//!
12//! See [`crate::backends`] for backend and printer examples.
13
14use std::{borrow::Cow, fmt::Display};
15
16use super::*;
17use crate::ast::*;
18use pretty::BoxAllocator;
19
20use crate::symbol::Symbol;
21use identifiers::*;
22use literals::*;
23use resugared::*;
24
25mod debug_json;
26mod to_document;
27pub use debug_json::*;
28pub use to_document::*;
29
30#[macro_export]
31/// Similar to [`std::todo`], but returns a document instead of panicking with a message.
32/// In addition, `todo_document!` accepts a prefix to point to a specific issue number.
33///
34/// ## Examples:
35/// - `todo_document!(allocator)`
36/// - `todo_document!(allocator, "This is a todo")`
37/// - `todo_document!(allocator, issue 42)`
38/// - `todo_document!(allocator, issue 42, "This is a todo")`
39macro_rules! todo_document {
40    ($allocator:ident, issue $issue:literal) => {
41        {return $allocator.todo_document(&format!("TODO_LINE_{}", std::line!()), Some($issue));}
42    };
43    ($allocator:ident, issue $issue:literal, $($tt:tt)*) => {
44        {
45            let message = format!($($tt)*);
46            return $allocator.todo_document(&message, Some($issue));
47        }
48    };
49    ($allocator:ident,) => {
50        {return $allocator.todo_document(&format!("TODO_LINE_{}", std::line!()), None);}
51    };
52    ($allocator:ident, $($tt:tt)*) => {
53        {
54            let message = format!($($tt)*);
55            return $allocator.todo_document(&message, None);
56        }
57    };
58}
59pub use todo_document;
60
61/// Expand a list of values into documents and concatenate them in order.
62///
63/// This helper mirrors [`pretty::docs!`] but automatically calls
64/// [`ToDocumentOwned::to_document_owned`] on each argument before appending it
65/// to the accumulator that starts as [`PrettyAstExt::nil`].
66#[macro_export]
67macro_rules! pretty_ast_docs {
68    ($printer: expr, $docs:expr) => {{
69        use $crate::printer::pretty_ast::{ToDocumentOwned};
70        $docs.to_document_owned($printer)
71    }};
72    ($printer: expr, $($docs:expr),*$(,)?) => {{
73        use $crate::printer::pretty_ast::{ToDocumentOwned};
74        nil!()
75        $(.append($docs.to_document_owned($printer)))*
76    }};
77}
78pub use pretty_ast_docs;
79
80/// Convert a collection of values into documents separated by another
81/// document.
82///
83/// It forwards to [`PrettyAstExt::intersperse`] after materialising the
84/// separator. The macro exists so call sites can stay concise while still
85/// benefiting from the allocator captured by [`install_pretty_helpers!`].
86#[macro_export]
87macro_rules! pretty_ast_intersperse {
88    ($printer: expr, $docs:expr, $sep: expr$(,)?) => {{
89        let docs = $docs;
90        let sep = $sep;
91        $crate::printer::pretty_ast::PrettyAstExt::intersperse($printer, docs, sep)
92    }};
93}
94pub use pretty_ast_intersperse;
95
96#[macro_export]
97/// Install pretty-printing helpers partially applied with a given local
98/// allocator.
99///
100/// This macro declares a set of small, local macros that proxy to the
101/// underlying [`pretty::DocAllocator`] methods and macro while capturing your
102/// allocator value. It keeps printing code concise and avoids passing the
103/// allocator around explicitly.
104///
105/// # Syntax
106/// ```rust,ignore
107/// install_pretty_helpers!(alloc_ident: AllocatorType)
108/// ```
109///
110/// - `alloc_ident`: the in-scope variable that implements both
111///   [`pretty::DocAllocator`] and [`Printer`].
112/// - `AllocatorType`: the concrete type of that variable.
113///
114/// # What gets installed
115/// - macro shorthands for common allocator methods:
116///   [`PrettyAstExt::nil`], [`PrettyAstExt::fail`],
117///   [`PrettyAstExt::hardline`], [`PrettyAstExt::space`],
118///   [`PrettyAstExt::line`], [`PrettyAstExt::line_`],
119///   [`PrettyAstExt::softline`], [`PrettyAstExt::softline_`],
120///   [`PrettyAstExt::as_string`], [`PrettyAstExt::text`],
121///   [`PrettyAstExt::concat`], [`PrettyAstExt::intersperse`],
122///   [`PrettyAstExt::column`], [`PrettyAstExt::nesting`],
123///   [`PrettyAstExt::reflow`].
124/// - a partially applied version of [`pretty::docs!`].
125/// - [`todo_document!`]: produce a placeholder document (that does not panic).
126macro_rules! install_pretty_helpers {
127    ($allocator:ident : $allocator_type:ty) => {
128        $crate::printer::pretty_ast::install_pretty_helpers!(
129            @$allocator,
130            #[doc = ::std::concat!("Proxy macro for [`", stringify!($crate), "::printer::pretty_ast::todo_document`] that automatically uses `", stringify!($allocator),"` as allocator.")]
131            #[doc = ::std::concat!(r#"Example: `disambiguated_todo!("Error message")` or `disambiguated_todo!(issue #123, "Error message with issue attached")`."#)]
132            disambiguated_todo{$crate::printer::pretty_ast::todo_document!},
133            #[doc = ::std::concat!("Proxy macro for [`pretty::docs`] that automatically uses `", stringify!($allocator),"` as allocator.")]
134            docs{$crate::printer::pretty_ast::pretty_ast_docs!},
135            #[doc = ::std::concat!("Proxy macro for [`PrettyAstExt::nil`] that automatically uses `", stringify!($allocator),"` as allocator.")]
136            nil{<$allocator_type as $crate::printer::pretty_ast::PrettyAstExt<_>>::nil},
137            #[doc = ::std::concat!("Proxy macro for [`PrettyAstExt::fail`] that automatically uses `", stringify!($allocator),"` as allocator.")]
138            fail{<$allocator_type as $crate::printer::pretty_ast::PrettyAstExt<_>>::fail},
139            #[doc = ::std::concat!("Proxy macro for [`PrettyAstExt::hardline`] that automatically uses `", stringify!($allocator),"` as allocator.")]
140            hardline{<$allocator_type as $crate::printer::pretty_ast::PrettyAstExt<_>>::hardline},
141            #[doc = ::std::concat!("Proxy macro for [`PrettyAstExt::space`] that automatically uses `", stringify!($allocator),"` as allocator.")]
142            space{<$allocator_type as $crate::printer::pretty_ast::PrettyAstExt<_>>::space},
143            #[doc = ::std::concat!("Proxy macro for [`PrettyAstExt::line`] that automatically uses `", stringify!($allocator),"` as allocator.")]
144            disambiguated_line{<$allocator_type as $crate::printer::pretty_ast::PrettyAstExt<_>>::line},
145            #[doc = ::std::concat!("Proxy macro for [`PrettyAstExt::line_`] that automatically uses `", stringify!($allocator),"` as allocator.")]
146            line_{<$allocator_type as $crate::printer::pretty_ast::PrettyAstExt<_>>::line_},
147            #[doc = ::std::concat!("Proxy macro for [`PrettyAstExt::softline`] that automatically uses `", stringify!($allocator),"` as allocator.")]
148            softline{<$allocator_type as $crate::printer::pretty_ast::PrettyAstExt<_>>::softline},
149            #[doc = ::std::concat!("Proxy macro for [`PrettyAstExt::softline_`] that automatically uses `", stringify!($allocator),"` as allocator.")]
150            softline_{<$allocator_type as $crate::printer::pretty_ast::PrettyAstExt<_>>::softline_},
151            #[doc = ::std::concat!("Proxy macro for [`PrettyAstExt::as_string`] that automatically uses `", stringify!($allocator),"` as allocator.")]
152            as_string{<$allocator_type as $crate::printer::pretty_ast::PrettyAstExt<_>>::as_string},
153            #[doc = ::std::concat!("Proxy macro for [`PrettyAstExt::text`] that automatically uses `", stringify!($allocator),"` as allocator.")]
154            text{<$allocator_type as $crate::printer::pretty_ast::PrettyAstExt<_>>::text},
155            #[doc = ::std::concat!("Proxy macro for [`PrettyAstExt::concat`] that automatically uses `", stringify!($allocator),"` as allocator.")]
156            disambiguated_concat{<$allocator_type as $crate::printer::pretty_ast::PrettyAstExt<_>>::concat},
157            #[doc = ::std::concat!("Proxy macro for [`PrettyAstExt::intersperse`] that automatically uses `", stringify!($allocator),"` as allocator.")]
158            intersperse{$crate::printer::pretty_ast::pretty_ast_intersperse!},
159            #[doc = ::std::concat!("Proxy macro for [`PrettyAstExt::column`] that automatically uses `", stringify!($allocator),"` as allocator.")]
160            column{<$allocator_type as $crate::printer::pretty_ast::PrettyAstExt<_>>::column},
161            #[doc = ::std::concat!("Proxy macro for [`PrettyAstExt::nesting`] that automatically uses `", stringify!($allocator),"` as allocator.")]
162            nesting{<$allocator_type as $crate::printer::pretty_ast::PrettyAstExt<_>>::nesting},
163            #[doc = ::std::concat!("Proxy macro for [`PrettyAstExt::reflow`] that automatically uses `", stringify!($allocator),"` as allocator.")]
164            reflow{<$allocator_type as $crate::printer::pretty_ast::PrettyAstExt<_>>::reflow}
165        );
166    };
167    (@$allocator:ident, $($(#[$($attrs:tt)*])*$name:ident{$($callable:tt)*}),*) => {
168        $(
169            #[hax_rust_engine_macros::partial_apply($($callable)*, $allocator,)]
170            #[allow(unused)]
171            $(#[$($attrs)*])*
172            macro_rules! $name {}
173        )*
174    };
175}
176pub use install_pretty_helpers;
177
178/// `PrettyAstExt` exposes `DocAllocator`-style constructors for printers.
179///
180/// Every method simply forwards to the global [`pretty::BoxAllocator`] so that printers
181/// implementing [`PrettyAst`] can build documents without juggling allocator plumbing.
182pub trait PrettyAstExt<A: 'static>: Sized {
183    /// Returns an empty document.
184    /// Mirrors [`pretty::DocAllocator::nil`].
185    fn nil(&self) -> DocBuilder<A> {
186        pretty::DocAllocator::nil(&BoxAllocator)
187    }
188
189    /// Produces a document that fails rendering immediately.
190    /// Mirrors [`pretty::DocAllocator::fail`].
191    ///
192    /// This is typically used to abort rendering inside the left side of a [`pretty::Doc::Union`].
193    fn fail(&self) -> DocBuilder<A> {
194        pretty::DocAllocator::fail(&BoxAllocator)
195    }
196
197    /// Inserts a mandatory line break.
198    /// Mirrors [`pretty::DocAllocator::hardline`].
199    fn hardline(&self) -> DocBuilder<A> {
200        pretty::DocAllocator::hardline(&BoxAllocator)
201    }
202
203    /// Inserts a single space that disappears when groups flatten.
204    /// Mirrors [`pretty::DocAllocator::space`].
205    fn space(&self) -> DocBuilder<A> {
206        pretty::DocAllocator::space(&BoxAllocator)
207    }
208
209    /// Acts like a `\n` but behaves like `space` once grouped onto a single line.
210    /// Mirrors [`pretty::DocAllocator::line`].
211    fn line(&self) -> DocBuilder<A> {
212        pretty::DocAllocator::line(&BoxAllocator)
213    }
214
215    /// Acts like `line` but collapses to `nil` if grouped on a single line.
216    /// Mirrors [`pretty::DocAllocator::line_`].
217    fn line_(&self) -> DocBuilder<A> {
218        pretty::DocAllocator::line_(&BoxAllocator)
219    }
220
221    /// Acts like `space` when the document fits the page, otherwise behaves like `line`.
222    /// Mirrors [`pretty::DocAllocator::softline`].
223    fn softline(&self) -> DocBuilder<A> {
224        pretty::DocAllocator::softline(&BoxAllocator)
225    }
226
227    /// Acts like `nil` when the document fits the page, otherwise behaves like `line_`.
228    /// Mirrors [`pretty::DocAllocator::softline_`].
229    fn softline_(&self) -> DocBuilder<A> {
230        pretty::DocAllocator::softline_(&BoxAllocator)
231    }
232
233    /// Renders `data` via its [`Display`] implementation.
234    /// Mirrors [`pretty::DocAllocator::as_string`].
235    ///
236    /// The resulting document must not contain explicit line breaks.
237    fn as_string<U: Display>(&self, data: U) -> DocBuilder<A> {
238        pretty::DocAllocator::as_string(&BoxAllocator, data)
239    }
240
241    /// Renders the provided text verbatim.
242    /// Mirrors [`pretty::DocAllocator::text`].
243    ///
244    /// The supplied string must not contain line breaks.
245    fn text<'a>(&self, data: impl Into<Cow<'a, str>>) -> DocBuilder<A> {
246        self.as_string(data.into())
247    }
248
249    /// Concatenates the given values after turning each into a document.
250    /// Mirrors [`pretty::DocAllocator::concat`].
251    fn concat<I>(&self, docs: I) -> DocBuilder<A>
252    where
253        I::Item: ToDocumentOwned<Self, A>,
254        I: IntoIterator,
255    {
256        pretty::DocAllocator::concat(
257            &BoxAllocator,
258            docs.into_iter().map(|doc| doc.to_document_owned(self)),
259        )
260    }
261
262    /// Concatenates documents while interspersing `separator` between every pair.
263    /// Mirrors [`pretty::DocAllocator::intersperse`].
264    ///
265    /// `separator` may need to be cloned; consider cheap pointer documents like `RefDoc` or `RcDoc`.
266    fn intersperse<I, S>(&self, docs: I, separator: S) -> DocBuilder<A>
267    where
268        I::Item: ToDocumentOwned<Self, A>,
269        I: IntoIterator,
270        S: ToDocumentOwned<Self, A> + Clone,
271        A: Clone,
272    {
273        let separator = separator.to_document_owned(self);
274        pretty::DocAllocator::intersperse(
275            &BoxAllocator,
276            docs.into_iter().map(|doc| doc.to_document_owned(self)),
277            separator,
278        )
279    }
280
281    /// Reflows `text`, inserting `softline` wherever whitespace appears.
282    /// Mirrors [`pretty::DocAllocator::reflow`].
283    fn reflow(&self, text: &'static str) -> DocBuilder<A>
284    where
285        A: Clone,
286    {
287        pretty::DocAllocator::reflow(&BoxAllocator, text)
288    }
289}
290
291impl<A: 'static + Clone, P: PrettyAst<A>> PrettyAstExt<A> for P {}
292
293/// Generate a dispatcher macro that forwards a token to specialised macros.
294macro_rules! make_cases_macro {
295    (
296        $macro_name:ident,
297        $(
298            $($idents:ident)|* => $target:ident,
299        )*
300        _ => $fallback:ident $(,)?
301    ) => {
302        macro_rules! $macro_name {
303            $(
304                $(
305                    ($idents $tt:tt) => { $target!($tt); };
306                )*
307            )*
308            ($anything:ident $tt:tt) => { $fallback!($tt); };
309        }
310    };
311}
312
313/// Helper macro used to ignore a matched arm in `make_cases_macro!`.
314macro_rules! skip {
315    ($tt:tt) => {};
316}
317/// Helper macro used to keep the body for specific matches in
318/// `make_cases_macro!`.
319macro_rules! keep {
320    ({$($tt:tt)*}) => { $($tt)* };
321}
322
323make_cases_macro!(method_deny_list,
324    ExprKind | PatKind | TyKind | GuardKind | ImplExprKind | ImplItemKind | TraitItemKind | AttributeKind | DocCommentKind => skip,
325    Signedness  | IntSize => skip,
326    ItemQuoteOrigin | ItemQuoteOriginKind | ItemQuoteOriginPosition => skip,
327    ControlFlowKind | LoopState | LoopKind => skip,
328    _ => keep
329);
330
331make_cases_macro!(span_handling,
332    Item | Expr | Pat | Guard | Arm | ImplItem | TraitItem | GenericParam | Attribute | Attribute => keep,
333    _ => skip
334);
335
336/// A trait that provides an optional contextual span for printers: during a
337/// pretty printing job, spans will be inserted so that errors are always tagged
338/// with precise location information.
339///
340/// This should not be implemented by hand, instead, use
341/// [`hax_rust_engine_macros::setup_printer_struct`].
342pub trait HasContextualSpan: Clone {
343    /// Clone the printer, adding a span hint. Useful for errors.
344    fn with_span(&self, _span: Span) -> Self;
345
346    /// Returns the span currently associated with the printer, if any.
347    fn span(&self) -> Option<Span>;
348}
349
350/// Declare the `PrettyAst` trait and wiring for deriving `ToDocument` for AST
351/// nodes.
352macro_rules! mk {
353    ($($ty:ident),*) => {
354        pastey::paste! {
355            /// A trait that defines a print method per type in the AST.
356            ///
357            /// This is the main trait a printer should implement.
358            ///
359            /// You then implement the actual formatting logic in the generated
360            /// per-type methods. These methods are intentionally marked
361            /// `#[deprecated]` to discourage calling them directly; instead,
362            /// call `node.to_document(self)` from the [`ToDocument`] trait to
363            /// ensure annotations and spans are applied correctly.
364            ///
365            /// Note that using `install_pretty_helpers!` will produce macro
366            /// that implicitely use `self` as allocator. Take a look at a
367            /// printer in the [`backends`] module for an example.
368            pub trait PrettyAst<A: 'static + Clone>: Sized + HasContextualSpan {
369                /// A name for this instance of `PrettyAst`.
370                /// Useful for diagnostics and debugging.
371                const NAME: &'static str;
372
373                /// Emit a diagnostic with proper context and span.
374                fn emit_diagnostic(&self, kind: hax_types::diagnostics::Kind) {
375                    let span = self.span().unwrap_or_else(|| Span::dummy());
376                    use crate::ast::diagnostics::{DiagnosticInfo, Context};
377                    (DiagnosticInfo {
378                        context: Context::Printer(Self::NAME.to_string()),
379                        span,
380                        kind
381                    }).emit()
382                }
383
384                /// Produce a non-panicking placeholder document. In general, prefer the use of the helper macro [`todo_document!`].
385                fn todo_document(&self, message: &str, issue_id: Option<u32>) -> DocBuilder<A> {
386                    self.emit_diagnostic(hax_types::diagnostics::Kind::Unimplemented {
387                        issue_id,
388                        details: Some(message.into()),
389                    });
390                    self.as_string(message)
391                }
392
393                /// Produce a structured error document for an unimplemented
394                /// method.
395                ///
396                /// Printers may override this for nicer diagnostics (e.g.,
397                /// colored "unimplemented" banners or links back to source
398                /// locations). The default produces a small, debuggable piece
399                /// of text that includes the method name and a JSON handle for
400                /// the AST fragment (via [`DebugJSON`]).
401                fn unimplemented_method(&self, method: &str, ast: ast::fragment::FragmentRef<'_>) -> DocBuilder<A> {
402                    let debug_json = DebugJSON(ast).to_string();
403                    self.emit_diagnostic(hax_types::diagnostics::Kind::Unimplemented {
404                        issue_id: None,
405                        details: Some(format!("The method `{method}` is not implemented in the backend {}. To show the AST fragment that could not be printed, run {debug_json}.", Self::NAME)),
406                    });
407                    self.text(format!("`{method}` unimpl, {debug_json}", )).parens()
408                }
409
410                $(
411                    method_deny_list!($ty{
412                        #[doc = "Define how the printer formats a value of this AST type."]
413                        #[doc = "Do not call this method directly. Use [`ToDocument::to_document`] instead, so annotations/spans are preserved correctly."]
414                        #[deprecated = "Do not call this method directly. Use [`ToDocument::to_document`] instead, so annotations/spans are preserved correctly."]
415                        fn [<$ty:snake>](&self, [<$ty:snake>]: &$ty) -> DocBuilder<A> {
416                            mk!(@method_body $ty [<$ty:snake>] self [<$ty:snake>])
417                        }
418                    });
419                )*
420            }
421
422            $(
423                method_deny_list!($ty{
424                    impl<A: 'static + Clone, P: PrettyAst<A>> ToDocument<P, A> for $ty {
425                        fn to_document(&self, printer: &P) -> DocBuilder<A> {
426                            span_handling!($ty{
427                                let printer = &(printer.with_span(self.span()));
428                            });
429                            // Note about deprecation:
430                            //   Here is the only place where calling the deprecated methods from the trait `PrettyAst` is fine.
431                            //   Here is the place we (will) take care of spans, etc.
432                            #[allow(deprecated)]
433                            let print = <P as PrettyAst<A>>::[<$ty:snake>];
434                            print(printer, self)
435                        }
436                    }
437                });
438            )*
439        }
440    };
441
442    // Special default implementation for specific types
443    (@method_body Symbol $meth:ident $self:ident $value:ident) => {
444        $self.as_string($value.to_string())
445    };
446    (@method_body LocalId $meth:ident $self:ident $value:ident) => {
447        $value.0.to_document($self)
448    };
449    (@method_body SpannedTy $meth:ident $self:ident $value:ident) => {
450        $value.ty.to_document($self)
451    };
452    (@method_body $ty:ident $meth:ident $self:ident $value:ident) => {
453        $self.unimplemented_method(stringify!($meth), ast::fragment::FragmentRef::from($meth))
454    };
455}
456
457#[hax_rust_engine_macros::replace(AstNodes => include(VisitableAstNodes))]
458mk!(GlobalId, AstNodes);
hax_rust_engine/printer/pretty_ast.rs

hax_rust_engine/printer/
pretty_ast.rs
