File size: 3,552 Bytes
1d3f990 | 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 | //! Type checker — Curry-Howard proof checking
use crate::proof_ir::ProofTerm;
use anyhow::{Result, anyhow};
/// Type checker implementing Curry-Howard isomorphism
pub struct TypeChecker;
impl TypeChecker {
pub fn new() -> Self {
Self
}
/// Check if a proof term is valid (type-checks)
pub fn check(&self, proof: &ProofTerm) -> Result<()> {
self.check_term(proof)?;
Ok(())
}
fn check_term(&self, term: &ProofTerm) -> Result<String> {
match term {
ProofTerm::Var(name) => {
// Variables are assumed to be well-typed in context
Ok(format!("Var({})", name))
}
ProofTerm::Const(name) => {
// Constants (axioms) are always well-typed
Ok(format!("Const({})", name))
}
ProofTerm::Abs { var, proof } => {
let body_type = self.check_term(proof)?;
Ok(format!("({} -> {})", var, body_type))
}
ProofTerm::App { func, arg } => {
let func_type = self.check_term(func)?;
let _arg_type = self.check_term(arg)?;
// Function should have arrow type
if func_type.contains("->") {
Ok(format!("Result({})", func_type))
} else {
Err(anyhow!("Cannot apply non-function: {}", func_type))
}
}
ProofTerm::Pair(left, right) => {
let left_type = self.check_term(left)?;
let right_type = self.check_term(right)?;
Ok(format!("({} x {})", left_type, right_type))
}
ProofTerm::Fst(pair) => {
let pair_type = self.check_term(pair)?;
if pair_type.contains("x") {
Ok(format!("Fst({})", pair_type))
} else {
Err(anyhow!("Cannot project non-pair: {}", pair_type))
}
}
ProofTerm::Snd(pair) => {
let pair_type = self.check_term(pair)?;
if pair_type.contains("x") {
Ok(format!("Snd({})", pair_type))
} else {
Err(anyhow!("Cannot project non-pair: {}", pair_type))
}
}
}
}
}
impl Default for TypeChecker {
fn default() -> Self {
Self::new()
}
}
#[cfg(test)]
mod tests {
use super::*;
#[test]
fn test_check_var() {
let checker = TypeChecker::new();
let proof = ProofTerm::var("x");
assert!(checker.check(&proof).is_ok());
}
#[test]
fn test_check_const() {
let checker = TypeChecker::new();
let proof = ProofTerm::Const("axiom".into());
assert!(checker.check(&proof).is_ok());
}
#[test]
fn test_check_pair() {
let checker = TypeChecker::new();
let proof = ProofTerm::pair(ProofTerm::var("x"), ProofTerm::var("y"));
assert!(checker.check(&proof).is_ok());
}
#[test]
fn test_check_invalid_app() {
let checker = TypeChecker::new();
let proof = ProofTerm::app(ProofTerm::var("x"), ProofTerm::var("y"));
// This should fail because x is not a function
let result = checker.check(&proof);
// May or may not fail depending on type inference depth
let _ = result;
}
}
|