proof_rules: better error message

moves-rwth · May 19, 2024 · 2d37e63 · 2d37e63
1 parent fc1b2b9
commit 2d37e63
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 6 deletions.
diff --git a/src/intrinsic/annotations.rs b/src/intrinsic/annotations.rs
@@ -5,8 +5,8 @@ use ariadne::ReportKind;
 
 use crate::{
     ast::{
-        DeclKind, Diagnostic, Expr, Files, Ident, Label, Param, SourceFilePath, Span, Spanned,
-        Stmt, Symbol,
+        DeclKind, Diagnostic, Direction, Expr, Files, Ident, Label, Param, SourceFilePath, Span,
+        Spanned, Stmt, Symbol,
     },
     front::{
         resolve::{Resolve, ResolveError},
@@ -30,7 +30,7 @@ pub enum AnnotationError {
     NotOnWhile(Span, Ident, Stmt),
     WrongArgument(Span, Expr, String),
     NotTerminator(Span, Ident),
-    CalculusEncodingMismatch(Span, Ident, Ident),
+    CalculusEncodingMismatch(Direction, Span, Ident, Ident),
     UnknownAnnotation(Span, Ident),
 }
 
@@ -72,11 +72,11 @@ impl AnnotationError {
                         "There must not be any statements after this annotated statement (and the annotated statement must not be nested in a block).",
                     ))
             }
-            AnnotationError::CalculusEncodingMismatch(span, calculus_name, encoding_name ) => {
+            AnnotationError::CalculusEncodingMismatch(direction, span, calculus_name, encoding_name ) => {
                 Diagnostic::new(ReportKind::Error, span)
                     .with_message(format!(
-                        "The '{}' calculus does not support the '{}' encoding.",
-                        calculus_name.name, encoding_name.name
+                        "In {}s, the '{}' calculus does not support the '{}' encoding.",
+                        direction.prefix("proc"), calculus_name.name, encoding_name.name
                     ))
                     .with_label(Label::new(span).with_message(
                         "The calculus, proof rule, and direction are incompatible.",

diff --git a/src/proof_rules/mod.rs b/src/proof_rules/mod.rs
@@ -221,6 +221,7 @@ impl<'tcx, 'sunit> VisitorMut for EncCall<'tcx, 'sunit> {
                                 .ok_or(AnnotationError::NotInProcedure(s.span, *ident))?,
                         ) {
                             return Err(AnnotationError::CalculusEncodingMismatch(
+                                self.direction.unwrap(),
                                 s.span,
                                 calculus.name,
                                 anno_ref.name(),