diff --git a/CHANGELOG.md b/CHANGELOG.md index f979a0848..13a1a5e55 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -14,6 +14,7 @@ Changes to the Rust Engine: - Add support for enums and structs to the Lean backend (type definitions, expressions, pattern-matching) (#1623) - Update name rendering infrastructure in the Lean backend (#1623, #1624) +- Printers now emit proper diagnostics (PR #1669) Changes to the frontend: - Add an explicit `Self: Trait` clause to trait methods and consts (#1559) diff --git a/rust-engine/src/ast/diagnostics.rs b/rust-engine/src/ast/diagnostics.rs index db8b90d71..a110b24e1 100644 --- a/rust-engine/src/ast/diagnostics.rs +++ b/rust-engine/src/ast/diagnostics.rs @@ -68,4 +68,6 @@ pub enum Context { Import, /// Error during the projection from idenitfiers to views NameView, + /// Error in a printer + Printer(String), } diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 577fbd382..5f0cdd96a 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -111,8 +111,6 @@ impl Printer for LeanPrinter { binops::logical_op_or(), ]))] } - - const NAME: &str = "Lean"; } /// The Lean backend @@ -289,6 +287,8 @@ const _: () = { } impl<'a, 'b, A: 'a + Clone> PrettyAst<'a, 'b, A> for LeanPrinter { + const NAME: &'static str = "Lean"; + fn module(&'a self, module: &'b Module) -> DocBuilder<'a, Self, A> { let items = &module.items; docs![ diff --git a/rust-engine/src/backends/rust.rs b/rust-engine/src/backends/rust.rs index ab4bc52f8..62080d92e 100644 --- a/rust-engine/src/backends/rust.rs +++ b/rust-engine/src/backends/rust.rs @@ -12,8 +12,6 @@ impl Printer for RustPrinter { fn resugaring_phases() -> Vec> { vec![] } - - const NAME: &'static str = "Rust"; } const INDENT: isize = 4; @@ -43,6 +41,8 @@ const _: () = { macro_rules! concat {($($tt:tt)*) => {disambiguated_concat!($($tt)*)};} impl<'a, 'b, A: 'a + Clone> PrettyAst<'a, 'b, A> for RustPrinter { + const NAME: &'static str = "Rust"; + fn module(&'a self, module: &'b Module) -> DocBuilder<'a, Self, A> { intersperse!(&module.items, docs![hardline!(), hardline!()]) } diff --git a/rust-engine/src/printer.rs b/rust-engine/src/printer.rs index 881abce01..7f22cb8d4 100644 --- a/rust-engine/src/printer.rs +++ b/rust-engine/src/printer.rs @@ -78,7 +78,7 @@ pub trait Printer: Sized + for<'a, 'b> PrettyAst<'a, 'b, Span> + Default { /// A list of resugaring phases. fn resugaring_phases() -> Vec>; /// The name of the printer - const NAME: &'static str; + const NAME: &'static str = >::NAME; } /// Placeholder type for sourcemaps. diff --git a/rust-engine/src/printer/pretty_ast.rs b/rust-engine/src/printer/pretty_ast.rs index 2498ac95e..784ea9156 100644 --- a/rust-engine/src/printer/pretty_ast.rs +++ b/rust-engine/src/printer/pretty_ast.rs @@ -109,14 +109,30 @@ impl<'a, 'b, A: 'a + Clone, P: PrettyAst<'a, 'b, A>, T: 'b + serde::Serialize> P #[macro_export] /// Similar to [`std::todo`], but returns a document instead of panicking with a message. +/// In addition, `todo_document!` accepts a prefix to point to a specific issue number. +/// +/// ## Examples: +/// - `todo_document!(allocator)` +/// - `todo_document!(allocator, "This is a todo")` +/// - `todo_document!(allocator, issue #42)` +/// - `todo_document!(allocator, issue #42, "This is a todo")` macro_rules! todo_document { + ($allocator:ident, issue $issue:literal) => { + {return $allocator.todo_document(&format!("TODO_LINE_{}", std::line!()), Some($issue));} + }; + ($allocator:ident, issue $issue:literal, $($tt:tt)*) => { + { + let message = format!($($tt)*); + return $allocator.todo_document(&message, Some($issue)); + } + }; ($allocator:ident,) => { - {return $allocator.todo_document(&format!("TODO_LINE_{}", std::line!()));} + {return $allocator.todo_document(&format!("TODO_LINE_{}", std::line!()), None);} }; ($allocator:ident, $($tt:tt)*) => { { let message = format!($($tt)*); - return $allocator.todo_document(&message); + return $allocator.todo_document(&message, None); } }; } @@ -157,6 +173,7 @@ macro_rules! install_pretty_helpers { $crate::printer::pretty_ast::install_pretty_helpers!( @$allocator, #[doc = ::std::concat!("Proxy macro for [`", stringify!($crate), "::printer::pretty_ast::todo_document`] that automatically uses `", stringify!($allocator),"` as allocator.")] + #[doc = ::std::concat!(r#"Example: `disambiguated_todo!("Error message")` or `disambiguated_todo!(issue #123, "Error message with issue attached")`."#)] disambiguated_todo{$crate::printer::pretty_ast::todo_document!}, #[doc = ::std::concat!("Proxy macro for [`pretty::docs`] that automatically uses `", stringify!($allocator),"` as allocator.")] docs{pretty::docs!}, @@ -203,6 +220,28 @@ macro_rules! install_pretty_helpers { } pub use install_pretty_helpers; +// This module tracks a span information via a global mutex, because our +// printers cannot really carry information in a nice way. See issue +// https://github.com/cryspen/hax/issues/1667. Once addressed this can go away. +mod default_global_span_context { + use super::Span; + + use std::sync::{LazyLock, Mutex}; + static STATE: LazyLock>> = LazyLock::new(|| Mutex::new(None)); + + pub(super) fn with_span(span: Span, action: impl Fn() -> T) -> T { + let previous_span = STATE.lock().unwrap().clone(); + *STATE.lock().unwrap() = Some(span); + let result = action(); + *STATE.lock().unwrap() = previous_span; + result + } + + pub(super) fn get_ambiant_span() -> Option { + STATE.lock().unwrap().clone() + } +} + macro_rules! mk { ($($ty:ident),*) => { pastey::paste! { @@ -237,10 +276,33 @@ macro_rules! mk { /// that implicitely use `self` as allocator. Take a look at a /// printer in the [`backends`] module for an example. pub trait PrettyAst<'a, 'b, A: 'a + Clone>: DocAllocator<'a, A> + Sized { + /// A name for this instance of `PrettyAst`. + /// Useful for diagnostics and debugging. + const NAME: &'static str; + + /// Emit a diagnostic with proper context and span. + fn emit_diagnostic(&'a self, kind: hax_types::diagnostics::Kind) { + let span = default_global_span_context::get_ambiant_span().unwrap_or_else(|| Span::dummy()); + use crate::printer::pretty_ast::diagnostics::{DiagnosticInfo, Context}; + (DiagnosticInfo { + context: Context::Printer(Self::NAME.to_string()), + span, + kind + }).emit() + } + /// Produce a non-panicking placeholder document. In general, prefer the use of the helper macro [`todo_document!`]. - fn todo_document(&'a self, message: &str) -> DocBuilder<'a, Self, A> { + fn todo_document(&'a self, message: &str, issue_id: Option) -> DocBuilder<'a, Self, A> { + self.emit_diagnostic(hax_types::diagnostics::Kind::Unimplemented { + issue_id, + details: Some(message.into()), + }); self.as_string(message) } + /// Execute an action with a span hint. Useful for errors. + fn with_span(&self, span: Span, action: impl Fn(&Self) -> T) -> T { + default_global_span_context::with_span(span, || action(self)) + } /// Produce a structured error document for an unimplemented /// method. /// @@ -250,7 +312,12 @@ macro_rules! mk { /// of text that includes the method name and a JSON handle for /// the AST fragment (via [`DebugJSON`]). fn unimplemented_method(&'a self, method: &str, ast: ast::fragment::FragmentRef<'_>) -> DocBuilder<'a, Self, A> { - self.text(format!("`{method}` unimpl, {}", DebugJSON(ast))).parens() + let debug_json = DebugJSON(ast).to_string(); + self.emit_diagnostic(hax_types::diagnostics::Kind::Unimplemented { + issue_id: None, + 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)), + }); + self.text(format!("`{method}` unimpl, {debug_json}", )).parens() } $( #[doc = "Define how the printer formats a value of this AST type."]