logicaffeine_proof/
error.rs

1//! Error types for proof search and unification.
2//!
3//! This module defines [`ProofError`], which captures all failure modes
4//! during proof construction. Errors are designed to be informative for
5//! debugging and educational feedback.
6//!
7//! # Error Categories
8//!
9//! | Category | Variants | Meaning |
10//! |----------|----------|---------|
11//! | Search | `NoProofFound`, `DepthExceeded` | Proof search terminated |
12//! | Unification | `OccursCheck`, `UnificationFailed`, `ExprUnificationFailed` | Terms cannot be unified |
13//! | Matching | `SymbolMismatch`, `ArityMismatch` | Structural incompatibility |
14//! | Higher-Order | `PatternNotDistinct`, `NotAPattern`, `ScopeViolation` | Miller pattern failures |
15//!
16//! # Example
17//!
18//! ```
19//! use logicaffeine_proof::ProofError;
20//!
21//! fn check_result(result: Result<(), ProofError>) {
22//!     match result {
23//!         Ok(()) => println!("Proof found"),
24//!         Err(ProofError::NoProofFound) => println!("No proof exists"),
25//!         Err(ProofError::DepthExceeded) => println!("Search too deep"),
26//!         Err(e) => println!("Error: {}", e),
27//!     }
28//! }
29//! ```
30
31use crate::{ProofExpr, ProofTerm};
32use std::fmt;
33
34/// Errors that can occur during proof search.
35#[derive(Debug, Clone)]
36pub enum ProofError {
37    /// No proof was found for the given goal.
38    NoProofFound,
39
40    /// The proof search exceeded the maximum depth limit.
41    DepthExceeded,
42
43    /// Unification failed due to occurs check.
44    /// This prevents infinite types like x = f(x).
45    OccursCheck {
46        variable: String,
47        term: ProofTerm,
48    },
49
50    /// Unification failed because terms could not be unified.
51    UnificationFailed {
52        left: ProofTerm,
53        right: ProofTerm,
54    },
55
56    /// Expression-level unification failed.
57    ExprUnificationFailed {
58        left: ProofExpr,
59        right: ProofExpr,
60    },
61
62    /// Symbol mismatch during unification.
63    SymbolMismatch {
64        left: String,
65        right: String,
66    },
67
68    /// Arity mismatch during unification.
69    ArityMismatch {
70        expected: usize,
71        found: usize,
72    },
73
74    // --- Higher-Order Pattern Unification ---
75
76    /// The pattern has non-distinct arguments (e.g., ?F(x, x))
77    /// Miller patterns require distinct bound variables.
78    PatternNotDistinct(String),
79
80    /// Expression is not a valid Miller pattern.
81    /// Pattern arguments must be Term(BoundVarRef(...)).
82    NotAPattern(ProofExpr),
83
84    /// RHS uses variables not in pattern scope.
85    /// In ?P(x) = Body, Body must only use variables that appear in the pattern.
86    ScopeViolation {
87        var: String,
88        allowed: Vec<String>,
89    },
90}
91
92impl fmt::Display for ProofError {
93    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
94        match self {
95            ProofError::NoProofFound => {
96                write!(f, "No proof found: the goal could not be derived from the knowledge base")
97            }
98            ProofError::DepthExceeded => {
99                write!(f, "Proof search exceeded maximum depth limit")
100            }
101            ProofError::OccursCheck { variable, term } => {
102                write!(
103                    f,
104                    "Occurs check failed: variable '{}' appears in term '{}' (would create infinite type)",
105                    variable, term
106                )
107            }
108            ProofError::UnificationFailed { left, right } => {
109                write!(f, "Unification failed: cannot unify '{}' with '{}'", left, right)
110            }
111            ProofError::ExprUnificationFailed { left, right } => {
112                write!(f, "Expression unification failed: cannot unify '{}' with '{}'", left, right)
113            }
114            ProofError::SymbolMismatch { left, right } => {
115                write!(f, "Symbol mismatch: '{}' vs '{}'", left, right)
116            }
117            ProofError::ArityMismatch { expected, found } => {
118                write!(f, "Arity mismatch: expected {} arguments, found {}", expected, found)
119            }
120            ProofError::PatternNotDistinct(var) => {
121                write!(f, "Pattern has duplicate variable '{}': Miller patterns require distinct bound variables", var)
122            }
123            ProofError::NotAPattern(expr) => {
124                write!(f, "Not a valid Miller pattern: '{}' (arguments must be bound variable references)", expr)
125            }
126            ProofError::ScopeViolation { var, allowed } => {
127                write!(f, "Scope violation: variable '{}' not in pattern scope {:?}", var, allowed)
128            }
129        }
130    }
131}
132
133impl std::error::Error for ProofError {}
134
135/// Result type for proof operations.
136pub type ProofResult<T> = Result<T, ProofError>;
logicaffeine_proof/error.rs

logicaffeine_proof/
error.rs
