//! V-Enriched Categories.
//!
//! Provenance: Lean 4 → Safe Rust
//! Source: HeytingLean.EpistemicCalculus.Enrichment.VEnrichedCategory
//!         HeytingLean.EpistemicCalculus.Enrichment.ChangeOfEnrichment
//! Paper: Aambø, arXiv:2603.04188, Section 4.1
//!
//! A V-enriched category in the posetal setting:
//! - Objects: indexed by usize
//! - Hom: hom(x, y) is a V-value
//! - Identity: unit ≤ hom(x, x)
//! - Composition: hom(y, z) ⊗ hom(x, y) ≤ hom(x, z)

use crate::epistemic_calculus::EpistemicCalculus;

/// A V-enriched category with a fixed number of objects.
// Theorem preserved: VEnrichedCat
pub struct VEnrichedCat<V: EpistemicCalculus> {
    pub n_obj: usize,
    hom_values: Vec<Vec<V>>,
}

impl<V: EpistemicCalculus> VEnrichedCat<V> {
    /// Create a new V-enriched category from a hom matrix.
    pub fn new(hom_values: Vec<Vec<V>>) -> Self {
        let n = hom_values.len();
        assert!(hom_values.iter().all(|row| row.len() == n));
        VEnrichedCat { n_obj: n, hom_values }
    }

    /// Get hom(x, y).
    pub fn hom(&self, x: usize, y: usize) -> &V {
        &self.hom_values[x][y]
    }

    /// Check identity law: unit ≤ hom(x, x) for all x.
    // Theorem preserved: identity
    pub fn check_identity(&self) -> bool {
        let u = V::unit();
        (0..self.n_obj).all(|x| u <= *self.hom(x, x))
    }

    /// Check composition law: hom(y,z) ⊗ hom(x,y) ≤ hom(x,z) for all x,y,z.
    // Theorem preserved: composition
    pub fn check_composition(&self) -> bool {
        for x in 0..self.n_obj {
            for y in 0..self.n_obj {
                for z in 0..self.n_obj {
                    let fused = V::fusion(self.hom(y, z), self.hom(x, y));
                    if !(fused <= *self.hom(x, z)) {
                        return false;
                    }
                }
            }
        }
        true
    }
}

/// Change of enrichment: a conservative change F: V → W transports
/// a V-enriched category to a W-enriched category.
// Theorem preserved: changeEnrichment
pub fn change_enrichment<V, W>(
    cat: &VEnrichedCat<V>,
    map: &dyn Fn(&V) -> W,
) -> VEnrichedCat<W>
where
    V: EpistemicCalculus,
    W: EpistemicCalculus,
{
    let hom_values: Vec<Vec<W>> = (0..cat.n_obj)
        .map(|x| (0..cat.n_obj).map(|y| map(cat.hom(x, y))).collect())
        .collect();
    VEnrichedCat::new(hom_values)
}

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

    #[test]
    fn two_object_cf_enriched() {
        // The odds category: hom(x,y) = weight(y)/weight(x), weights = {1, 2}
        let cat = VEnrichedCat::new(vec![
            vec![CF::new(1.0), CF::new(2.0)],  // hom(0,0)=1, hom(0,1)=2
            vec![CF::new(0.5), CF::new(1.0)],   // hom(1,0)=0.5, hom(1,1)=1
        ]);

        assert!(cat.check_identity());
        assert!(cat.check_composition());
    }

    #[test]
    fn change_enrichment_identity() {
        let cat = VEnrichedCat::new(vec![
            vec![CF::new(1.0), CF::new(2.0)],
            vec![CF::new(0.5), CF::new(1.0)],
        ]);

        let transported = change_enrichment(&cat, &|v: &CF| v.clone());
        assert_eq!(transported.hom(0, 1).val(), 2.0);
        assert_eq!(transported.hom(1, 0).val(), 0.5);
    }
}