lemma/
error.rs

1use crate::parsing::ast::Span;
2use crate::Source;
3use std::fmt;
4use std::sync::Arc;
5
6/// Detailed error information with source location
7#[derive(Debug, Clone)]
8pub struct ErrorDetails {
9    pub message: String,
10    pub source_location: Source,
11    pub source_text: Arc<str>,
12    pub doc_start_line: usize,
13    pub suggestion: Option<String>,
14}
15
16/// Error types for the Lemma system with source location tracking
17#[derive(Debug, Clone)]
18pub enum LemmaError {
19    /// Parse error with source location
20    Parse(Box<ErrorDetails>),
21
22    /// Semantic validation error with source location
23    Semantic(Box<ErrorDetails>),
24
25    /// Inversion error (valid Lemma, but unsupported by inversion) with source location
26    Inversion(Box<ErrorDetails>),
27
28    /// Runtime error during evaluation with source location
29    Runtime(Box<ErrorDetails>),
30
31    /// Engine error with source location
32    Engine(Box<ErrorDetails>),
33
34    /// Missing fact error during evaluation with source location
35    MissingFact(Box<ErrorDetails>),
36
37    /// Circular dependency error with source location and cycle information
38    CircularDependency {
39        details: Box<ErrorDetails>,
40        cycle: Vec<Source>,
41    },
42
43    /// Resource limit exceeded
44    ResourceLimitExceeded {
45        limit_name: String,
46        limit_value: String,
47        actual_value: String,
48        suggestion: String,
49    },
50
51    /// Multiple errors collected together
52    MultipleErrors(Vec<LemmaError>),
53}
54
55impl LemmaError {
56    /// Create a parse error with source information
57    pub fn parse(
58        message: impl Into<String>,
59        span: Span,
60        attribute: impl Into<String>,
61        source_text: Arc<str>,
62        doc_name: impl Into<String>,
63        doc_start_line: usize,
64        suggestion: Option<impl Into<String>>,
65    ) -> Self {
66        Self::Parse(Box::new(ErrorDetails {
67            message: message.into(),
68            source_location: Source::new(attribute, span, doc_name),
69            source_text,
70            doc_start_line,
71            suggestion: suggestion.map(Into::into),
72        }))
73    }
74
75    /// Create a parse error with suggestion
76    pub fn parse_with_suggestion(
77        message: impl Into<String>,
78        span: Span,
79        attribute: impl Into<String>,
80        source_text: Arc<str>,
81        doc_name: impl Into<String>,
82        doc_start_line: usize,
83        suggestion: impl Into<String>,
84    ) -> Self {
85        Self::parse(
86            message,
87            span,
88            attribute,
89            source_text,
90            doc_name,
91            doc_start_line,
92            Some(suggestion),
93        )
94    }
95
96    /// Create a semantic error with source information
97    pub fn semantic(
98        message: impl Into<String>,
99        span: Span,
100        attribute: impl Into<String>,
101        source_text: Arc<str>,
102        doc_name: impl Into<String>,
103        doc_start_line: usize,
104        suggestion: Option<impl Into<String>>,
105    ) -> Self {
106        Self::Semantic(Box::new(ErrorDetails {
107            message: message.into(),
108            source_location: Source::new(attribute, span, doc_name),
109            source_text,
110            doc_start_line,
111            suggestion: suggestion.map(Into::into),
112        }))
113    }
114
115    /// Create a semantic error with suggestion
116    pub fn semantic_with_suggestion(
117        message: impl Into<String>,
118        span: Span,
119        attribute: impl Into<String>,
120        source_text: Arc<str>,
121        doc_name: impl Into<String>,
122        doc_start_line: usize,
123        suggestion: impl Into<String>,
124    ) -> Self {
125        Self::semantic(
126            message,
127            span,
128            attribute,
129            source_text,
130            doc_name,
131            doc_start_line,
132            Some(suggestion),
133        )
134    }
135
136    /// Create an inversion error with source information
137    pub fn inversion(
138        message: impl Into<String>,
139        span: Span,
140        attribute: impl Into<String>,
141        source_text: Arc<str>,
142        doc_name: impl Into<String>,
143        doc_start_line: usize,
144        suggestion: Option<impl Into<String>>,
145    ) -> Self {
146        Self::Inversion(Box::new(ErrorDetails {
147            message: message.into(),
148            source_location: Source::new(attribute, span, doc_name),
149            source_text,
150            doc_start_line,
151            suggestion: suggestion.map(Into::into),
152        }))
153    }
154
155    /// Create an inversion error with suggestion
156    pub fn inversion_with_suggestion(
157        message: impl Into<String>,
158        span: Span,
159        attribute: impl Into<String>,
160        source_text: Arc<str>,
161        doc_name: impl Into<String>,
162        doc_start_line: usize,
163        suggestion: impl Into<String>,
164    ) -> Self {
165        Self::inversion(
166            message,
167            span,
168            attribute,
169            source_text,
170            doc_name,
171            doc_start_line,
172            Some(suggestion),
173        )
174    }
175
176    /// Create an engine error with source information
177    pub fn engine(
178        message: impl Into<String>,
179        span: Span,
180        attribute: impl Into<String>,
181        source_text: Arc<str>,
182        doc_name: impl Into<String>,
183        doc_start_line: usize,
184        suggestion: Option<impl Into<String>>,
185    ) -> Self {
186        Self::Engine(Box::new(ErrorDetails {
187            message: message.into(),
188            source_location: Source::new(attribute, span, doc_name),
189            source_text,
190            doc_start_line,
191            suggestion: suggestion.map(Into::into),
192        }))
193    }
194
195    /// Create a missing fact error with source information
196    pub fn missing_fact(
197        fact_path: crate::FactPath,
198        span: Span,
199        attribute: impl Into<String>,
200        source_text: Arc<str>,
201        doc_name: impl Into<String>,
202        doc_start_line: usize,
203        suggestion: Option<impl Into<String>>,
204    ) -> Self {
205        Self::MissingFact(Box::new(ErrorDetails {
206            message: format!("Missing fact: {}", fact_path),
207            source_location: Source::new(attribute, span, doc_name),
208            source_text,
209            doc_start_line,
210            suggestion: suggestion.map(Into::into),
211        }))
212    }
213
214    /// Create a missing rule error with source information
215    pub fn missing_rule(
216        rule_path: crate::RulePath,
217        span: Span,
218        attribute: impl Into<String>,
219        source_text: Arc<str>,
220        doc_name: impl Into<String>,
221        doc_start_line: usize,
222        suggestion: Option<impl Into<String>>,
223    ) -> Self {
224        Self::Engine(Box::new(ErrorDetails {
225            message: format!("Missing rule: {}", rule_path),
226            source_location: Source::new(attribute, span, doc_name),
227            source_text,
228            doc_start_line,
229            suggestion: suggestion.map(Into::into),
230        }))
231    }
232
233    /// Create a missing type error with source information
234    pub fn missing_type(
235        type_name: impl Into<String>,
236        span: Span,
237        attribute: impl Into<String>,
238        source_text: Arc<str>,
239        doc_name: impl Into<String>,
240        doc_start_line: usize,
241        suggestion: Option<impl Into<String>>,
242    ) -> Self {
243        Self::Engine(Box::new(ErrorDetails {
244            message: format!("Missing type: {}", type_name.into()),
245            source_location: Source::new(attribute, span, doc_name),
246            source_text,
247            doc_start_line,
248            suggestion: suggestion.map(Into::into),
249        }))
250    }
251
252    /// Create a missing document error with source information
253    pub fn missing_doc(
254        doc_name: impl Into<String>,
255        span: Span,
256        attribute: impl Into<String>,
257        source_text: Arc<str>,
258        current_doc_name: impl Into<String>,
259        doc_start_line: usize,
260        suggestion: Option<impl Into<String>>,
261    ) -> Self {
262        Self::Engine(Box::new(ErrorDetails {
263            message: format!("Missing document: {}", doc_name.into()),
264            source_location: Source::new(attribute, span, current_doc_name),
265            source_text,
266            doc_start_line,
267            suggestion: suggestion.map(Into::into),
268        }))
269    }
270
271    /// Create a circular dependency error with source information
272    #[allow(clippy::too_many_arguments)]
273    pub fn circular_dependency(
274        message: impl Into<String>,
275        span: Span,
276        attribute: impl Into<String>,
277        source_text: Arc<str>,
278        doc_name: impl Into<String>,
279        doc_start_line: usize,
280        cycle: Vec<Source>,
281        suggestion: Option<impl Into<String>>,
282    ) -> Self {
283        Self::CircularDependency {
284            details: Box::new(ErrorDetails {
285                message: message.into(),
286                source_location: Source::new(attribute, span, doc_name),
287                source_text,
288                doc_start_line,
289                suggestion: suggestion.map(Into::into),
290            }),
291            cycle,
292        }
293    }
294}
295
296impl fmt::Display for LemmaError {
297    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
298        match self {
299            LemmaError::Parse(details) => {
300                write!(f, "Parse error: {}", details.message)?;
301                if let Some(suggestion) = &details.suggestion {
302                    write!(f, " (suggestion: {suggestion})")?;
303                }
304                write!(
305                    f,
306                    " at {}:{}:{}",
307                    details.source_location.attribute,
308                    details.source_location.span.line,
309                    details.source_location.span.col
310                )
311            }
312            LemmaError::Semantic(details) => {
313                write!(f, "Semantic error: {}", details.message)?;
314                if let Some(suggestion) = &details.suggestion {
315                    write!(f, " (suggestion: {suggestion})")?;
316                }
317                write!(
318                    f,
319                    " at {}:{}:{}",
320                    details.source_location.attribute,
321                    details.source_location.span.line,
322                    details.source_location.span.col
323                )
324            }
325            LemmaError::Inversion(details) => {
326                write!(f, "Inversion error: {}", details.message)?;
327                if let Some(suggestion) = &details.suggestion {
328                    write!(f, " (suggestion: {suggestion})")?;
329                }
330                write!(
331                    f,
332                    " at {}:{}:{}",
333                    details.source_location.attribute,
334                    details.source_location.span.line,
335                    details.source_location.span.col
336                )
337            }
338            LemmaError::Runtime(details) => {
339                write!(f, "Runtime error: {}", details.message)?;
340                if let Some(suggestion) = &details.suggestion {
341                    write!(f, " (suggestion: {suggestion})")?;
342                }
343                write!(
344                    f,
345                    " at {}:{}:{}",
346                    details.source_location.attribute,
347                    details.source_location.span.line,
348                    details.source_location.span.col
349                )
350            }
351            LemmaError::Engine(details) => {
352                write!(f, "Engine error: {}", details.message)?;
353                if let Some(suggestion) = &details.suggestion {
354                    write!(f, " (suggestion: {suggestion})")?;
355                }
356                write!(
357                    f,
358                    " at {}:{}:{}",
359                    details.source_location.attribute,
360                    details.source_location.span.line,
361                    details.source_location.span.col
362                )
363            }
364            LemmaError::MissingFact(details) => {
365                write!(f, "Missing fact: {}", details.message)?;
366                if let Some(suggestion) = &details.suggestion {
367                    write!(f, " (suggestion: {suggestion})")?;
368                }
369                write!(
370                    f,
371                    " at {}:{}:{}",
372                    details.source_location.attribute,
373                    details.source_location.span.line,
374                    details.source_location.span.col
375                )
376            }
377            LemmaError::CircularDependency { details, .. } => {
378                write!(f, "Circular dependency: {}", details.message)?;
379                if let Some(suggestion) = &details.suggestion {
380                    write!(f, " (suggestion: {suggestion})")?;
381                }
382                write!(
383                    f,
384                    " at {}:{}:{}",
385                    details.source_location.attribute,
386                    details.source_location.span.line,
387                    details.source_location.span.col
388                )
389            }
390            LemmaError::ResourceLimitExceeded {
391                limit_name,
392                limit_value,
393                actual_value,
394                suggestion,
395            } => {
396                write!(
397                    f,
398                    "Resource limit exceeded: {limit_name} (limit: {limit_value}, actual: {actual_value}). {suggestion}"
399                )
400            }
401            LemmaError::MultipleErrors(errors) => {
402                writeln!(f, "Multiple errors:")?;
403                for (i, error) in errors.iter().enumerate() {
404                    write!(f, "  {}. {error}", i + 1)?;
405                    if i < errors.len() - 1 {
406                        writeln!(f)?;
407                    }
408                }
409                Ok(())
410            }
411        }
412    }
413}
414
415impl std::error::Error for LemmaError {}
416
417impl From<std::fmt::Error> for LemmaError {
418    fn from(err: std::fmt::Error) -> Self {
419        use crate::parsing::ast::Span;
420        LemmaError::engine(
421            format!("Format error: {err}"),
422            Span {
423                start: 0,
424                end: 0,
425                line: 1,
426                col: 0,
427            },
428            "<format-error>",
429            Arc::from(""),
430            "<format-error>",
431            1,
432            None::<String>,
433        )
434    }
435}
436
437impl LemmaError {
438    /// Get the error message
439    pub fn message(&self) -> &str {
440        match self {
441            LemmaError::Parse(details)
442            | LemmaError::Semantic(details)
443            | LemmaError::Inversion(details)
444            | LemmaError::Runtime(details)
445            | LemmaError::Engine(details)
446            | LemmaError::MissingFact(details) => &details.message,
447            LemmaError::CircularDependency { details, .. } => &details.message,
448            LemmaError::ResourceLimitExceeded { limit_name, .. } => limit_name,
449            LemmaError::MultipleErrors(_) => "Multiple errors occurred",
450        }
451    }
452
453    /// Get the source location if available
454    pub fn location(&self) -> Option<&Source> {
455        match self {
456            LemmaError::Parse(details)
457            | LemmaError::Semantic(details)
458            | LemmaError::Inversion(details)
459            | LemmaError::Runtime(details)
460            | LemmaError::Engine(details)
461            | LemmaError::MissingFact(details) => Some(&details.source_location),
462            LemmaError::CircularDependency { details, .. } => Some(&details.source_location),
463            LemmaError::ResourceLimitExceeded { .. } | LemmaError::MultipleErrors(_) => None,
464        }
465    }
466
467    /// Get the source text if available
468    pub fn source_text(&self) -> Option<&str> {
469        match self {
470            LemmaError::Parse(details)
471            | LemmaError::Semantic(details)
472            | LemmaError::Inversion(details)
473            | LemmaError::Runtime(details)
474            | LemmaError::Engine(details)
475            | LemmaError::MissingFact(details) => Some(&details.source_text),
476            LemmaError::CircularDependency { details, .. } => Some(&details.source_text),
477            LemmaError::ResourceLimitExceeded { .. } | LemmaError::MultipleErrors(_) => None,
478        }
479    }
480
481    /// Get the suggestion if available
482    pub fn suggestion(&self) -> Option<&str> {
483        match self {
484            LemmaError::Parse(details)
485            | LemmaError::Semantic(details)
486            | LemmaError::Inversion(details)
487            | LemmaError::Runtime(details)
488            | LemmaError::Engine(details)
489            | LemmaError::MissingFact(details) => details.suggestion.as_deref(),
490            LemmaError::CircularDependency { details, .. } => details.suggestion.as_deref(),
491            LemmaError::ResourceLimitExceeded { suggestion, .. } => Some(suggestion),
492            LemmaError::MultipleErrors(_) => None,
493        }
494    }
495}
496
497#[cfg(test)]
498mod tests {
499    use super::*;
500    use crate::parsing::ast::Span;
501    use std::sync::Arc;
502
503    type ErrorVariant =
504        fn(String, Span, String, Arc<str>, String, usize, Option<String>) -> LemmaError;
505
506    #[allow(clippy::type_complexity)]
507    fn create_test_error(variant: ErrorVariant) -> LemmaError {
508        let source_text = "fact amount = 100";
509        let span = Span {
510            start: 14,
511            end: 21,
512            line: 1,
513            col: 15,
514        };
515        variant(
516            "Invalid currency".to_string(),
517            span,
518            "test.lemma".to_string(),
519            Arc::from(source_text),
520            "test_doc".to_string(),
521            1,
522            None,
523        )
524    }
525
526    #[test]
527    fn test_error_creation_and_display() {
528        let parse_error = create_test_error(LemmaError::parse);
529        let parse_error_display = format!("{parse_error}");
530        assert!(parse_error_display.contains("Parse error: Invalid currency"));
531        assert!(parse_error_display.contains("test.lemma:1:15"));
532
533        let semantic_error = create_test_error(LemmaError::semantic);
534        let semantic_error_display = format!("{semantic_error}");
535        assert!(semantic_error_display.contains("Semantic error: Invalid currency"));
536        assert!(semantic_error_display.contains("test.lemma:1:15"));
537
538        let source_text = "fact amont = 100";
539        let span = Span {
540            start: 5,
541            end: 10,
542            line: 1,
543            col: 6,
544        };
545        let parse_error_with_suggestion = LemmaError::parse_with_suggestion(
546            "Typo in fact name",
547            span.clone(),
548            "suggestion.lemma",
549            Arc::from(source_text),
550            "suggestion_doc",
551            1,
552            "Did you mean 'amount'?",
553        );
554        let parse_error_with_suggestion_display = format!("{parse_error_with_suggestion}");
555        assert!(parse_error_with_suggestion_display.contains("Typo in fact name"));
556        assert!(parse_error_with_suggestion_display.contains("Did you mean 'amount'?"));
557
558        let semantic_error_with_suggestion = LemmaError::semantic_with_suggestion(
559            "Incompatible types",
560            span.clone(),
561            "suggestion.lemma",
562            Arc::from(source_text),
563            "suggestion_doc",
564            1,
565            "Try converting one of the types.",
566        );
567        let semantic_error_with_suggestion_display = format!("{semantic_error_with_suggestion}");
568        assert!(semantic_error_with_suggestion_display.contains("Incompatible types"));
569        assert!(semantic_error_with_suggestion_display.contains("Try converting one of the types."));
570
571        let engine_error = LemmaError::engine(
572            "Something went wrong",
573            Span {
574                start: 0,
575                end: 0,
576                line: 1,
577                col: 0,
578            },
579            "<test>",
580            Arc::from(""),
581            "<test>",
582            1,
583            None::<String>,
584        );
585        assert!(format!("{engine_error}").contains("Engine error: Something went wrong"));
586
587        let circular_dependency_error = LemmaError::circular_dependency(
588            "a -> b -> a",
589            Span {
590                start: 0,
591                end: 0,
592                line: 1,
593                col: 0,
594            },
595            "<test>",
596            Arc::from(""),
597            "<test>",
598            1,
599            vec![],
600            None::<String>,
601        );
602        assert!(format!("{circular_dependency_error}").contains("Circular dependency: a -> b -> a"));
603
604        let multiple_errors =
605            LemmaError::MultipleErrors(vec![parse_error, semantic_error, engine_error]);
606        let multiple_errors_display = format!("{multiple_errors}");
607        assert!(multiple_errors_display.contains("Multiple errors:"));
608        assert!(multiple_errors_display.contains("Parse error: Invalid currency"));
609        assert!(multiple_errors_display.contains("Semantic error: Invalid currency"));
610        assert!(multiple_errors_display.contains("Engine error: Something went wrong"));
611    }
612}
lemma/error.rs

lemma/
error.rs
