//! Certainty Factors epistemic calculus.
//!
//! Provenance: Lean 4 → Safe Rust
//! Source: HeytingLean.EpistemicCalculus.Examples.CertaintyFactors
//! Paper: Aambø, arXiv:2603.04188, Section 2.1
//!
//! CF = { x ∈ ℝ | x > 0 }, fusion = multiplication, unit = 1.
//! Satisfies: E4 (Closed), E7 (Fallible), E8 (Cancellative).

use crate::epistemic_calculus::{Closed, EpistemicCalculus, Fallible};

/// Certainty factor carrier: a positive real number.
#[derive(Debug, Clone, PartialEq)]
pub struct CF(f64);

impl CF {
    /// Create a CF value. Panics if value is not positive.
    pub fn new(val: f64) -> Self {
        assert!(val > 0.0, "CF values must be positive");
        CF(val)
    }

    /// Get the underlying value.
    pub fn val(&self) -> f64 {
        self.0
    }
}

// Theorem preserved: cfOne
pub const CF_ONE: f64 = 1.0;

// Theorem preserved: cfTwo
pub const CF_TWO: f64 = 2.0;

impl PartialOrd for CF {
    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
        self.0.partial_cmp(&other.0)
    }
}

// Theorem preserved: instEpistemicCalculusCF
impl EpistemicCalculus for CF {
    fn fusion(x: &Self, y: &Self) -> Self {
        CF(x.0 * y.0)
    }

    fn unit() -> Self {
        CF(CF_ONE)
    }
}

// Theorem preserved: Closed CF
// ihom(y, z) = z / y
impl Closed for CF {
    fn ihom(y: &Self, z: &Self) -> Self {
        CF(z.0 / y.0)
    }
}

// Theorem preserved: Fallible CF
// revisable witness: z = y/x, then x * (y/x) = y
impl Fallible for CF {
    fn revisable_witness(x: &Self, y: &Self) -> Self {
        CF(y.0 / x.0)
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn fusion_comm() {
        let a = CF::new(2.0);
        let b = CF::new(3.0);
        assert_eq!(CF::fusion(&a, &b).val(), CF::fusion(&b, &a).val());
    }

    #[test]
    fn fusion_assoc() {
        let a = CF::new(2.0);
        let b = CF::new(3.0);
        let c = CF::new(4.0);
        let lhs = CF::fusion(&CF::fusion(&a, &b), &c).val();
        let rhs = CF::fusion(&a, &CF::fusion(&b, &c)).val();
        assert!((lhs - rhs).abs() < 1e-12);
    }

    #[test]
    fn fusion_unit_left() {
        let x = CF::new(5.0);
        let u = CF::unit();
        assert_eq!(CF::fusion(&u, &x).val(), x.val());
    }

    #[test]
    fn nontrivial() {
        assert_ne!(CF::new(CF_ONE), CF::new(CF_TWO));
    }

    #[test]
    fn ihom_adjunction() {
        let x = CF::new(2.0);
        let y = CF::new(3.0);
        let z = CF::new(7.0);
        // x * y <= z  iff  x <= z/y
        let fused = CF::fusion(&x, &y).val();
        let ihom = CF::ihom(&y, &z).val();
        assert_eq!(fused <= z.val(), x.val() <= ihom);
    }

    #[test]
    fn revisable() {
        let x = CF::new(3.0);
        let y = CF::new(7.0);
        let w = CF::revisable_witness(&x, &y);
        let fused = CF::fusion(&x, &w).val();
        assert!((fused - y.val()).abs() < 1e-12);
    }
}