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**. It also exposes a handful of ergonomic helper macros that wire the
5//! [`pretty`](https://docs.rs/pretty/) crate's allocator into concise printing code, while
6//! taking care of annotations/spans for you.
7//!
8//! # Quickstart
9//! In most printers you:
10//! 1. Implement [`Printer`] for your allocator/type,
11//! 2. Implement [`PrettyAst`] for that allocator,
12//! 3. Call `x.pretty(&allocator)` on AST values.
13//!
14//! See [`super::backends`] for backend and printer examples.
15//!
16//! # Lifetimes and Parameters
17//! - `'a`: lifetime tied to the **document allocator** (from `pretty::DocAllocator`).
18//! - `'b`: lifetime of the **borrowed AST** node(s) being printed.
19//! - `A`: the **annotation** type carried in documents (e.g., spans for source maps).
20//!   `PrettyAst` is generic over `A`.
21
22use std::fmt::Display;
23
24use super::*;
25use crate::ast::*;
26use pretty::{DocAllocator, DocBuilder};
27
28use crate::symbol::Symbol;
29use identifiers::*;
30use literals::*;
31use resugared::*;
32
33/// This type is primarily useful inside printer implementations when you want a
34/// low-friction way to inspect an AST fragment.
35///
36/// # What it does
37/// - Appends a JSON representation of the wrapped value to
38///   `"/tmp/hax-ast-debug.json"` (one JSON document per line).
39/// - Implements [`std::fmt::Display`] to print a `just` invocation you can paste in a shell
40///   to re-open that same JSON by line number:
41///   `just debug-json <line-id>`
42///
43/// # Example
44/// ```rust
45/// # use hax_rust_engine::printer::pretty_ast::DebugJSON;
46/// # #[derive(serde::Serialize)]
47/// # struct Small { x: u32 }
48/// let s = Small { x: 42 };
49/// // Prints something like: `just debug-json 17`.
50/// println!("{}", DebugJSON(&s));
51/// // Running `just debug-json 17` will print `{"x":42}`
52/// ```
53///
54/// # Notes
55/// - This is a **debugging convenience** and intentionally has a side-effect (file write).
56///   Avoid keeping it in user-facing output paths.
57/// - The file grows over time; occasionally delete it if you no longer need historical entries.
58pub struct DebugJSON<T: serde::Serialize>(pub T);
59
60impl<T: serde::Serialize> Display for DebugJSON<T> {
61    #[cfg(not(unix))]
62    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
63        write!(f, "<unknown, DebugJSON supported on unix plateforms only>")
64    }
65    #[cfg(unix)]
66    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
67        const PATH: &str = "/tmp/hax-ast-debug.json";
68        /// Write a new JSON as a line at the end of `PATH`
69        fn append_line_json(value: &serde_json::Value) -> std::io::Result<usize> {
70            use std::io::{BufRead, BufReader, Write};
71            cleanup();
72            let file = std::fs::OpenOptions::new()
73                .read(true)
74                .append(true)
75                .create(true)
76                .open(PATH)?;
77            let count = BufReader::new(&file).lines().count();
78            writeln!(&file, "{value}")?;
79            Ok(count)
80        }
81
82        /// Drop the file at `PATH` when we first write
83        fn cleanup() {
84            static DID_RUN: AtomicBool = AtomicBool::new(false);
85            use std::sync::atomic::{AtomicBool, Ordering};
86            if DID_RUN
87                .compare_exchange(false, true, Ordering::AcqRel, Ordering::Acquire)
88                .is_ok()
89            {
90                let _ignored = std::fs::remove_file(PATH);
91            }
92        }
93
94        if let Ok(id) = append_line_json(&serde_json::to_value(&self.0).unwrap()) {
95            write!(f, "`just debug-json {id}`")
96        } else {
97            write!(f, "<DebugJSON failed>")
98        }
99    }
100}
101
102impl<'a, 'b, A: 'a + Clone, P: PrettyAst<'a, 'b, A>, T: 'b + serde::Serialize> Pretty<'a, P, A>
103    for DebugJSON<T>
104{
105    fn pretty(self, allocator: &'a P) -> DocBuilder<'a, P, A> {
106        allocator.as_string(format!("{self}"))
107    }
108}
109
110#[macro_export]
111/// Similar to [`std::todo`], but returns a document instead of panicking with a message.
112/// In addition, `todo_document!` accepts a prefix to point to a specific issue number.
113///
114/// ## Examples:
115/// - `todo_document!(allocator)`
116/// - `todo_document!(allocator, "This is a todo")`
117/// - `todo_document!(allocator, issue #42)`
118/// - `todo_document!(allocator, issue #42, "This is a todo")`
119macro_rules! todo_document {
120    ($allocator:ident, issue $issue:literal) => {
121        {return $allocator.todo_document(&format!("TODO_LINE_{}", std::line!()), Some($issue));}
122    };
123    ($allocator:ident, issue $issue:literal, $($tt:tt)*) => {
124        {
125            let message = format!($($tt)*);
126            return $allocator.todo_document(&message, Some($issue));
127        }
128    };
129    ($allocator:ident,) => {
130        {return $allocator.todo_document(&format!("TODO_LINE_{}", std::line!()), None);}
131    };
132    ($allocator:ident, $($tt:tt)*) => {
133        {
134            let message = format!($($tt)*);
135            return $allocator.todo_document(&message, None);
136        }
137    };
138}
139pub use todo_document;
140
141#[macro_export]
142/// Install pretty-printing helpers partially applied with a given local
143/// allocator.
144///
145/// This macro declares a set of small, local macros that proxy to the
146/// underlying [`pretty::DocAllocator`] methods and macro while capturing your
147/// allocator value. It keeps printing code concise and avoids passing the
148/// allocator around explicitly.
149///
150/// # Syntax
151/// ```rust,ignore
152/// install_pretty_helpers!(alloc_ident: AllocatorType)
153/// ```
154///
155/// - `alloc_ident`: the in-scope variable that implements both
156///   [`pretty::DocAllocator`] and [`Printer`].
157/// - `AllocatorType`: the concrete type of that variable.
158///
159/// # What gets installed
160/// - macro shorthands for common allocator methods:
161///   [`pretty::DocAllocator::nil`], [`pretty::DocAllocator::fail`],
162///   [`pretty::DocAllocator::hardline`], [`pretty::DocAllocator::space`],
163///   [`pretty::DocAllocator::line`], [`pretty::DocAllocator::line_`],
164///   [`pretty::DocAllocator::softline`], [`pretty::DocAllocator::softline_`],
165///   [`pretty::DocAllocator::as_string`], [`pretty::DocAllocator::text`],
166///   [`pretty::DocAllocator::concat`], [`pretty::DocAllocator::intersperse`],
167///   [`pretty::DocAllocator::column`], [`pretty::DocAllocator::nesting`],
168///   [`pretty::DocAllocator::reflow`].
169/// - a partially applied version of [`pretty::docs!`].
170/// - [`todo_document!`]: produce a placeholder document (that does not panic).
171macro_rules! install_pretty_helpers {
172    ($allocator:ident : $allocator_type:ty) => {
173        $crate::printer::pretty_ast::install_pretty_helpers!(
174            @$allocator,
175            #[doc = ::std::concat!("Proxy macro for [`", stringify!($crate), "::printer::pretty_ast::todo_document`] that automatically uses `", stringify!($allocator),"` as allocator.")]
176            #[doc = ::std::concat!(r#"Example: `disambiguated_todo!("Error message")` or `disambiguated_todo!(issue #123, "Error message with issue attached")`."#)]
177            disambiguated_todo{$crate::printer::pretty_ast::todo_document!},
178            #[doc = ::std::concat!("Proxy macro for [`pretty::docs`] that automatically uses `", stringify!($allocator),"` as allocator.")]
179            docs{pretty::docs!},
180            #[doc = ::std::concat!("Proxy macro for [`pretty::DocAllocator::nil`] that automatically uses `", stringify!($allocator),"` as allocator.")]
181            nil{<$allocator_type as ::pretty::DocAllocator<'_, _>>::nil},
182            #[doc = ::std::concat!("Proxy macro for [`pretty::DocAllocator::fail`] that automatically uses `", stringify!($allocator),"` as allocator.")]
183            fail{<$allocator_type as ::pretty::DocAllocator<'_, _>>::fail},
184            #[doc = ::std::concat!("Proxy macro for [`pretty::DocAllocator::hardline`] that automatically uses `", stringify!($allocator),"` as allocator.")]
185            hardline{<$allocator_type as ::pretty::DocAllocator<'_, _>>::hardline},
186            #[doc = ::std::concat!("Proxy macro for [`pretty::DocAllocator::space`] that automatically uses `", stringify!($allocator),"` as allocator.")]
187            space{<$allocator_type as ::pretty::DocAllocator<'_, _>>::space},
188            #[doc = ::std::concat!("Proxy macro for [`pretty::DocAllocator::line`] that automatically uses `", stringify!($allocator),"` as allocator.")]
189            disambiguated_line{<$allocator_type as ::pretty::DocAllocator<'_, _>>::line},
190            #[doc = ::std::concat!("Proxy macro for [`pretty::DocAllocator::line_`] that automatically uses `", stringify!($allocator),"` as allocator.")]
191            line_{<$allocator_type as ::pretty::DocAllocator<'_, _>>::line_},
192            #[doc = ::std::concat!("Proxy macro for [`pretty::DocAllocator::softline`] that automatically uses `", stringify!($allocator),"` as allocator.")]
193            softline{<$allocator_type as ::pretty::DocAllocator<'_, _>>::softline},
194            #[doc = ::std::concat!("Proxy macro for [`pretty::DocAllocator::softline_`] that automatically uses `", stringify!($allocator),"` as allocator.")]
195            softline_{<$allocator_type as ::pretty::DocAllocator<'_, _>>::softline_},
196            #[doc = ::std::concat!("Proxy macro for [`pretty::DocAllocator::as_string`] that automatically uses `", stringify!($allocator),"` as allocator.")]
197            as_string{<$allocator_type as ::pretty::DocAllocator<'_, _>>::as_string},
198            #[doc = ::std::concat!("Proxy macro for [`pretty::DocAllocator::text`] that automatically uses `", stringify!($allocator),"` as allocator.")]
199            text{<$allocator_type as ::pretty::DocAllocator<'_, _>>::text},
200            #[doc = ::std::concat!("Proxy macro for [`pretty::DocAllocator::concat`] that automatically uses `", stringify!($allocator),"` as allocator.")]
201            disambiguated_concat{<$allocator_type as ::pretty::DocAllocator<'_, _>>::concat},
202            #[doc = ::std::concat!("Proxy macro for [`pretty::DocAllocator::intersperse`] that automatically uses `", stringify!($allocator),"` as allocator.")]
203            intersperse{<$allocator_type as ::pretty::DocAllocator<'_, _>>::intersperse},
204            #[doc = ::std::concat!("Proxy macro for [`pretty::DocAllocator::column`] that automatically uses `", stringify!($allocator),"` as allocator.")]
205            column{<$allocator_type as ::pretty::DocAllocator<'_, _>>::column},
206            #[doc = ::std::concat!("Proxy macro for [`pretty::DocAllocator::nesting`] that automatically uses `", stringify!($allocator),"` as allocator.")]
207            nesting{<$allocator_type as ::pretty::DocAllocator<'_, _>>::nesting},
208            #[doc = ::std::concat!("Proxy macro for [`pretty::DocAllocator::reflow`] that automatically uses `", stringify!($allocator),"` as allocator.")]
209            reflow{<$allocator_type as ::pretty::DocAllocator<'_, _>>::reflow}
210        );
211    };
212    (@$allocator:ident, $($(#[$($attrs:tt)*])*$name:ident{$($callable:tt)*}),*) => {
213        $(
214            #[hax_rust_engine_macros::partial_apply($($callable)*, $allocator,)]
215            #[allow(unused)]
216            $(#[$($attrs)*])*
217            macro_rules! $name {}
218        )*
219    };
220}
221pub use install_pretty_helpers;
222
223// This module tracks a span information via a global mutex, because our
224// printers cannot really carry information in a nice way. See issue
225// https://github.com/cryspen/hax/issues/1667. Once addressed this can go away.
226mod default_global_span_context {
227    use super::Span;
228
229    use std::sync::{LazyLock, Mutex};
230    static STATE: LazyLock<Mutex<Option<Span>>> = LazyLock::new(|| Mutex::new(None));
231
232    pub(super) fn with_span<T>(span: Span, action: impl Fn() -> T) -> T {
233        let previous_span = STATE.lock().unwrap().clone();
234        *STATE.lock().unwrap() = Some(span);
235        let result = action();
236        *STATE.lock().unwrap() = previous_span;
237        result
238    }
239
240    pub(super) fn get_ambiant_span() -> Option<Span> {
241        STATE.lock().unwrap().clone()
242    }
243}
244
245macro_rules! mk {
246    ($($ty:ident),*) => {
247        pastey::paste! {
248            /// A trait that defines a print method per type in the AST.
249            ///
250            /// This is the main trait a printer should implement. It ties
251            /// together:
252            /// - the [`pretty::DocAllocator`] implementation that builds
253            ///   documents,
254            /// - the [`Printer`] behavior (syntax highlighting, punctuation
255            ///   helpers, …),
256            /// - and annotation plumbing (`A`) used for source maps.
257            ///
258            /// ## Lifetimes and Type Parameters
259            /// - `'a`: the allocator/document lifetime.
260            /// - `'b`: the lifetime of borrowed AST values being printed.
261            /// - `A`: the annotation type carried by documents (must be
262            ///   `Clone`).
263            ///
264            /// ## Implementing `PrettyAst`
265            /// ```rust,ignore
266            /// impl<'a, 'b, A: 'a + Clone> PrettyAst<'a, 'b, A> for MyPrinter { }
267            /// ```
268            ///
269            /// You then implement the actual formatting logic in the generated
270            /// per-type methods. These methods are intentionally marked
271            /// `#[deprecated]` to discourage calling them directly; instead,
272            /// call `node.pretty(self)` from the [`pretty::Pretty`] trait to
273            /// ensure annotations and spans are applied correctly.
274            ///
275            /// Note that using `install_pretty_helpers!` will produce macro
276            /// that implicitely use `self` as allocator. Take a look at a
277            /// printer in the [`backends`] module for an example.
278            pub trait PrettyAst<'a, 'b, A: 'a + Clone>: DocAllocator<'a, A> + Sized {
279                /// A name for this instance of `PrettyAst`.
280                /// Useful for diagnostics and debugging.
281                const NAME: &'static str;
282
283                /// Emit a diagnostic with proper context and span.
284                fn emit_diagnostic(&'a self, kind: hax_types::diagnostics::Kind) {
285                    let span = default_global_span_context::get_ambiant_span().unwrap_or_else(|| Span::dummy());
286                    use crate::printer::pretty_ast::diagnostics::{DiagnosticInfo, Context};
287                    (DiagnosticInfo {
288                        context: Context::Printer(Self::NAME.to_string()),
289                        span,
290                        kind
291                    }).emit()
292                }
293
294                /// Produce a non-panicking placeholder document. In general, prefer the use of the helper macro [`todo_document!`].
295                fn todo_document(&'a self, message: &str, issue_id: Option<u32>) -> DocBuilder<'a, Self, A> {
296                    self.emit_diagnostic(hax_types::diagnostics::Kind::Unimplemented {
297                        issue_id,
298                        details: Some(message.into()),
299                    });
300                    self.as_string(message)
301                }
302                /// Execute an action with a span hint. Useful for errors.
303                fn with_span<T>(&self, span: Span, action: impl Fn(&Self) -> T) -> T {
304                    default_global_span_context::with_span(span, || action(self))
305                }
306                /// Produce a structured error document for an unimplemented
307                /// method.
308                ///
309                /// Printers may override this for nicer diagnostics (e.g.,
310                /// colored "unimplemented" banners or links back to source
311                /// locations). The default produces a small, debuggable piece
312                /// of text that includes the method name and a JSON handle for
313                /// the AST fragment (via [`DebugJSON`]).
314                fn unimplemented_method(&'a self, method: &str, ast: ast::fragment::FragmentRef<'_>) -> DocBuilder<'a, Self, A> {
315                    let debug_json = DebugJSON(ast).to_string();
316                    self.emit_diagnostic(hax_types::diagnostics::Kind::Unimplemented {
317                        issue_id: None,
318                        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)),
319                    });
320                    self.text(format!("`{method}` unimpl, {debug_json}", )).parens()
321                }
322                $(
323                    #[doc = "Define how the printer formats a value of this AST type."]
324                    #[doc = "Do not call this method directly. Use [`pretty::Pretty::pretty`] instead, so annotations/spans are preserved correctly."]
325                    #[deprecated = "Do not call this method directly. Use [`pretty::Pretty::pretty`] instead, so annotations/spans are preserved correctly."]
326                    fn [<$ty:snake>](&'a self, [<$ty:snake>]: &'b $ty) -> DocBuilder<'a, Self, A> {
327                        mk!(@method_body $ty [<$ty:snake>] self [<$ty:snake>])
328                    }
329                )*
330            }
331
332            $(
333                impl<'a, 'b, A: 'a + Clone, P: PrettyAst<'a, 'b, A>> Pretty<'a, P, A> for &'b $ty {
334                    fn pretty(self, allocator: &'a P) -> DocBuilder<'a, P, A> {
335                        // Note about deprecation:
336                        //   Here is the only place where calling the deprecated methods from the trait `PrettyAst` is fine.
337                        //   Here is the place we (will) take care of spans, etc.
338                        #[allow(deprecated)]
339                        let print = <P as PrettyAst<'_, '_, _>>::[<$ty:snake>];
340                        print(allocator, self)
341                    }
342                }
343            )*
344        }
345    };
346    // Special default implementation for specific types
347    (@method_body Symbol $meth:ident $self:ident $value:ident) => {
348        $self.text($value.to_string())
349    };
350    (@method_body LocalId $meth:ident $self:ident $value:ident) => {
351        ::pretty::docs![$self, &$value.0]
352    };
353    (@method_body $ty:ident $meth:ident $self:ident $value:ident) => {
354        $self.unimplemented_method(stringify!($meth), ast::fragment::FragmentRef::from($meth))
355    };
356}
357
358#[hax_rust_engine_macros::replace(AstNodes => include(VisitableAstNodes))]
359mk!(GlobalId, AstNodes);
hax_rust_engine/printer/pretty_ast.rs

hax_rust_engine/printer/
pretty_ast.rs
