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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
//! Error types for proof search and unification.
//!
//! This module defines [`ProofError`], which captures all failure modes
//! during proof construction. Errors are designed to be informative for
//! debugging and educational feedback.
//!
//! # Error Categories
//!
//! | Category | Variants | Meaning |
//! |----------|----------|---------|
//! | Search | `NoProofFound`, `DepthExceeded` | Proof search terminated |
//! | Unification | `OccursCheck`, `UnificationFailed`, `ExprUnificationFailed` | Terms cannot be unified |
//! | Matching | `SymbolMismatch`, `ArityMismatch` | Structural incompatibility |
//! | Higher-Order | `PatternNotDistinct`, `NotAPattern`, `ScopeViolation` | Miller pattern failures |
//!
//! # Example
//!
//! ```
//! use logicaffeine_proof::ProofError;
//!
//! fn check_result(result: Result<(), ProofError>) {
//! match result {
//! Ok(()) => println!("Proof found"),
//! Err(ProofError::NoProofFound) => println!("No proof exists"),
//! Err(ProofError::DepthExceeded) => println!("Search too deep"),
//! Err(e) => println!("Error: {}", e),
//! }
//! }
//! ```
use crate::{ProofExpr, ProofTerm};
use std::fmt;
/// Errors that can occur during proof search.
#[derive(Debug, Clone)]
pub enum ProofError {
/// No proof was found for the given goal.
NoProofFound,
/// The proof search exceeded the maximum depth limit.
DepthExceeded,
/// Unification failed due to occurs check.
/// This prevents infinite types like x = f(x).
OccursCheck {
variable: String,
term: ProofTerm,
},
/// Unification failed because terms could not be unified.
UnificationFailed {
left: ProofTerm,
right: ProofTerm,
},
/// Expression-level unification failed.
ExprUnificationFailed {
left: ProofExpr,
right: ProofExpr,
},
/// Symbol mismatch during unification.
SymbolMismatch {
left: String,
right: String,
},
/// Arity mismatch during unification.
ArityMismatch {
expected: usize,
found: usize,
},
// --- Higher-Order Pattern Unification ---
/// The pattern has non-distinct arguments (e.g., ?F(x, x))
/// Miller patterns require distinct bound variables.
PatternNotDistinct(String),
/// Expression is not a valid Miller pattern.
/// Pattern arguments must be Term(BoundVarRef(...)).
NotAPattern(ProofExpr),
/// RHS uses variables not in pattern scope.
/// In ?P(x) = Body, Body must only use variables that appear in the pattern.
ScopeViolation {
var: String,
allowed: Vec<String>,
},
}
impl fmt::Display for ProofError {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
match self {
ProofError::NoProofFound => {
write!(f, "No proof found: the goal could not be derived from the knowledge base")
}
ProofError::DepthExceeded => {
write!(f, "Proof search exceeded maximum depth limit")
}
ProofError::OccursCheck { variable, term } => {
write!(
f,
"Occurs check failed: variable '{}' appears in term '{}' (would create infinite type)",
variable, term
)
}
ProofError::UnificationFailed { left, right } => {
write!(f, "Unification failed: cannot unify '{}' with '{}'", left, right)
}
ProofError::ExprUnificationFailed { left, right } => {
write!(f, "Expression unification failed: cannot unify '{}' with '{}'", left, right)
}
ProofError::SymbolMismatch { left, right } => {
write!(f, "Symbol mismatch: '{}' vs '{}'", left, right)
}
ProofError::ArityMismatch { expected, found } => {
write!(f, "Arity mismatch: expected {} arguments, found {}", expected, found)
}
ProofError::PatternNotDistinct(var) => {
write!(f, "Pattern has duplicate variable '{}': Miller patterns require distinct bound variables", var)
}
ProofError::NotAPattern(expr) => {
write!(f, "Not a valid Miller pattern: '{}' (arguments must be bound variable references)", expr)
}
ProofError::ScopeViolation { var, allowed } => {
write!(f, "Scope violation: variable '{}' not in pattern scope {:?}", var, allowed)
}
}
}
}
impl std::error::Error for ProofError {}
/// Result type for proof operations.
pub type ProofResult<T> = Result<T, ProofError>;