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

hax_rust_engine/printer/
pretty_ast.rs
