//! Change of Calculi morphisms.
//!
//! Provenance: Lean 4 → Safe Rust
//! Source: HeytingLean.EpistemicCalculus.ChangeOfCalculi.*
//! Paper: Aambø, arXiv:2603.04188, Section 4 (Definition 4.1, Lemma 4.1)
//!
//! Three classes of morphisms between epistemic calculi:
//!   Conservative (lax monoidal):  F(x) ⊗ F(y) ≤ F(x ⊗ y)
//!   Liberal (oplax monoidal):     F(x ⊗ y) ≤ F(x) ⊗ F(y)
//!   Balanced (strict monoidal):   F(x ⊗ y) = F(x) ⊗ F(y)

use crate::epistemic_calculus::EpistemicCalculus;

/// Conservative change of calculi (lax monoidal functor).
// Theorem preserved: ConservativeChange
pub struct ConservativeChange<V: EpistemicCalculus, W: EpistemicCalculus> {
    pub map: Box<dyn Fn(&V) -> W>,
}

/// Liberal change of calculi (oplax monoidal functor).
// Theorem preserved: LiberalChange
pub struct LiberalChange<V: EpistemicCalculus, W: EpistemicCalculus> {
    pub map: Box<dyn Fn(&V) -> W>,
}

/// Balanced change of calculi (strict monoidal functor).
// Theorem preserved: BalancedChange
pub struct BalancedChange<V: EpistemicCalculus, W: EpistemicCalculus> {
    pub map: Box<dyn Fn(&V) -> W>,
}

// Theorem preserved: BalancedChange.toConservative
impl<V: EpistemicCalculus, W: EpistemicCalculus> BalancedChange<V, W> {
    pub fn to_conservative(self) -> ConservativeChange<V, W> {
        ConservativeChange { map: self.map }
    }
}

// Theorem preserved: BalancedChange.toLiberal
impl<V: EpistemicCalculus, W: EpistemicCalculus> BalancedChange<V, W> {
    pub fn to_liberal(self) -> LiberalChange<V, W> {
        LiberalChange { map: self.map }
    }
}

/// PTbi ≅ IP: the identity map is balanced.
// Theorem preserved: ptbiIsoIp
pub fn ptbi_to_ip_balanced() -> BalancedChange<
    crate::bipolar_possibility::PTbi,
    crate::bipolar_possibility::IP,
> {
    BalancedChange {
        map: Box::new(|x| x.clone()),
    }
}

/// PT → CF: the constant-at-unit map is liberal.
// Theorem preserved: ptToCfLiberal
pub fn pt_to_cf_liberal() -> LiberalChange<
    crate::possibility_theory::PT,
    crate::certainty_factors::CF,
> {
    LiberalChange {
        map: Box::new(|_| crate::certainty_factors::CF::new(1.0)),
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::bipolar_possibility::PTbi;
    use crate::certainty_factors::CF;
    use crate::possibility_theory::PT;

    #[test]
    fn ptbi_to_ip_is_identity() {
        let bc = ptbi_to_ip_balanced();
        let x = PTbi::new(0.2, 0.8);
        assert_eq!((bc.map)(&x), x);
    }

    #[test]
    fn pt_to_cf_is_constant() {
        let lc = pt_to_cf_liberal();
        assert_eq!((lc.map)(&PT::new(0.3)).val(), 1.0);
        assert_eq!((lc.map)(&PT::new(0.9)).val(), 1.0);
    }

    #[test]
    fn balanced_to_conservative() {
        let bc = ptbi_to_ip_balanced();
        let cc = bc.to_conservative();
        let x = PTbi::new(0.5, 0.5);
        assert_eq!((cc.map)(&x), x);
    }

    #[test]
    fn pt_to_cf_oplax() {
        let lc = pt_to_cf_liberal();
        let x = PT::new(0.3);
        let y = PT::new(0.7);
        // oplax: map(x ⊗ y) ≤ map(x) ⊗ map(y)
        // map(min(0.3,0.7)) = 1 ≤ 1*1 = 1
        let lhs = (lc.map)(&PT::fusion(&x, &y)).val();
        let rhs = CF::fusion(&(lc.map)(&x), &(lc.map)(&y)).val();
        assert!(lhs <= rhs);
    }
}