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