//! Possibility Theory epistemic calculus.
//!
//! Provenance: Lean 4 → Safe Rust
//! Source: HeytingLean.EpistemicCalculus.Examples.PossibilityTheory
//! Paper: Aambø, arXiv:2603.04188, Section 2.1
//!
//! PT = [0, 1], fusion = min, unit = 1.
//! Satisfies: E1 (Optimistic), E6 (Idempotent), E7 (Fallible).

use crate::epistemic_calculus::{EpistemicCalculus, Fallible, IdempotentFusion, Optimistic};

/// Possibility theory carrier: a value in [0, 1].
#[derive(Debug, Clone, PartialEq)]
pub struct PT(f64);

impl PT {
    /// Create a PT value. Panics if not in [0, 1].
    pub fn new(val: f64) -> Self {
        assert!((0.0..=1.0).contains(&val), "PT values must be in [0, 1]");
        PT(val)
    }

    pub fn val(&self) -> f64 {
        self.0
    }
}

// Theorem preserved: ptZero, ptOne
pub const PT_ZERO: f64 = 0.0;
pub const PT_ONE: f64 = 1.0;

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

// Theorem preserved: instEpistemicCalculusPT
impl EpistemicCalculus for PT {
    fn fusion(x: &Self, y: &Self) -> Self {
        PT(x.0.min(y.0))
    }

    fn unit() -> Self {
        PT(PT_ONE)
    }
}

// Theorem preserved: Optimistic PT — top = 1
impl Optimistic for PT {
    fn top() -> Self {
        PT(PT_ONE)
    }
}

// Theorem preserved: IdempotentFusion PT — min(x, x) = x
impl IdempotentFusion for PT {}

// Theorem preserved: Fallible PT — witness z = y, min(x, y) <= y
impl Fallible for PT {
    fn revisable_witness(_x: &Self, y: &Self) -> Self {
        y.clone()
    }
}

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

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

    #[test]
    fn fusion_assoc() {
        let a = PT::new(0.2);
        let b = PT::new(0.5);
        let c = PT::new(0.8);
        assert_eq!(
            PT::fusion(&PT::fusion(&a, &b), &c).val(),
            PT::fusion(&a, &PT::fusion(&b, &c)).val()
        );
    }

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

    #[test]
    fn idempotent() {
        let x = PT::new(0.4);
        assert_eq!(PT::fusion(&x, &x).val(), x.val());
    }

    #[test]
    fn nontrivial() {
        assert_ne!(PT::new(PT_ZERO), PT::new(PT_ONE));
    }

    #[test]
    fn optimistic() {
        let x = PT::new(0.5);
        assert!(x <= PT::top());
    }

    #[test]
    fn revisable() {
        let x = PT::new(0.3);
        let y = PT::new(0.7);
        let w = PT::revisable_witness(&x, &y);
        assert!(PT::fusion(&x, &w) <= y);
    }
}