logicaffeine_kernel/
error.rs

1//! Error types for the kernel type checker.
2
3use std::fmt;
4
5/// Errors that can occur during type checking.
6#[derive(Debug)]
7pub enum KernelError {
8    /// Reference to an undefined variable.
9    UnboundVariable(String),
10
11    /// Attempted to apply a non-function term.
12    NotAFunction(String),
13
14    /// Expected a type (something with type Sort), got something else.
15    NotAType(String),
16
17    /// Type mismatch: expected one type, found another.
18    TypeMismatch { expected: String, found: String },
19
20    /// Attempted to match on a non-inductive type.
21    NotAnInductive(String),
22
23    /// Invalid motive in match expression.
24    InvalidMotive(String),
25
26    /// Wrong number of cases in match expression.
27    WrongNumberOfCases { expected: usize, found: usize },
28
29    /// Error during proof certification.
30    CertificationError(String),
31
32    /// Recursive call does not decrease structurally.
33    ///
34    /// This error prevents infinite loops in proofs.
35    /// A fixpoint must recurse on a structurally smaller argument.
36    TerminationViolation { fix_name: String, reason: String },
37
38    /// Inductive type appears in negative position in constructor.
39    ///
40    /// This error prevents logical paradoxes (Russell's paradox, etc).
41    /// An inductive must appear strictly positively in its constructors.
42    PositivityViolation {
43        inductive: String,
44        constructor: String,
45        reason: String,
46    },
47
48    /// Cannot infer the type of a hole without context.
49    ///
50    /// Holes (implicit arguments) need to be checked against an expected type,
51    /// not inferred standalone.
52    CannotInferHole,
53}
54
55impl fmt::Display for KernelError {
56    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
57        match self {
58            KernelError::UnboundVariable(v) => {
59                write!(f, "Unbound variable: {}", v)
60            }
61            KernelError::NotAFunction(t) => {
62                write!(f, "Not a function: {}", t)
63            }
64            KernelError::NotAType(t) => {
65                write!(f, "Not a type: {}", t)
66            }
67            KernelError::TypeMismatch { expected, found } => {
68                write!(f, "Type mismatch: expected {}, found {}", expected, found)
69            }
70            KernelError::NotAnInductive(t) => {
71                write!(f, "Not an inductive type: {}", t)
72            }
73            KernelError::InvalidMotive(t) => {
74                write!(f, "Invalid motive: {}", t)
75            }
76            KernelError::WrongNumberOfCases { expected, found } => {
77                write!(
78                    f,
79                    "Wrong number of cases: expected {}, found {}",
80                    expected, found
81                )
82            }
83            KernelError::CertificationError(msg) => {
84                write!(f, "Certification error: {}", msg)
85            }
86            KernelError::TerminationViolation { fix_name, reason } => {
87                write!(
88                    f,
89                    "Termination violation in '{}': {}",
90                    fix_name, reason
91                )
92            }
93            KernelError::PositivityViolation {
94                inductive,
95                constructor,
96                reason,
97            } => {
98                write!(
99                    f,
100                    "Positivity violation: constructor '{}' of '{}': {}",
101                    constructor, inductive, reason
102                )
103            }
104            KernelError::CannotInferHole => {
105                write!(f, "Cannot infer type of implicit argument (_) without context")
106            }
107        }
108    }
109}
110
111impl std::error::Error for KernelError {}
112
113/// Result type for kernel operations.
114pub type KernelResult<T> = Result<T, KernelError>;
logicaffeine_kernel/error.rs

logicaffeine_kernel/
error.rs
