//! Bipolar Possibility Theory and Interval Probabilities.
//!
//! Provenance: Lean 4 → Safe Rust
//! Source: HeytingLean.EpistemicCalculus.Examples.BipolarPossibility
//!         HeytingLean.EpistemicCalculus.Examples.IntervalProbability
//! Paper: Aambø, arXiv:2603.04188, Section 2.1
//!
//! PTbi = { (lo, hi) | lo, hi ∈ [0,1] }
//! Fusion: (lo₁, hi₁) ⊗ (lo₂, hi₂) = (max(lo₁,lo₂), min(hi₁,hi₂))
//! Unit: (0, 1)
//! Order: (lo₁, hi₁) ≤ (lo₂, hi₂) iff lo₂ ≤ lo₁ and hi₁ ≤ hi₂
//!
//! IP is definitionally the same carrier (type alias).

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

/// Bipolar possibility theory carrier: (lo, hi) confidence bounds.
/// Inconsistent pairs (lo > hi) are allowed.
#[derive(Debug, Clone, PartialEq)]
pub struct PTbi {
    pub lo: f64,
    pub hi: f64,
}

impl PTbi {
    pub fn new(lo: f64, hi: f64) -> Self {
        assert!((0.0..=1.0).contains(&lo), "lo must be in [0,1]");
        assert!((0.0..=1.0).contains(&hi), "hi must be in [0,1]");
        PTbi { lo, hi }
    }
}

// Theorem preserved: ptbiUnit
pub fn ptbi_unit() -> PTbi {
    PTbi { lo: 0.0, hi: 1.0 }
}

// Theorem preserved: ptbiInconsistent
pub fn ptbi_inconsistent() -> PTbi {
    PTbi { lo: 1.0, hi: 0.0 }
}

// Theorem preserved: LE PTbi — b.lo ≤ a.lo and a.hi ≤ b.hi
impl PartialOrd for PTbi {
    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
        let lo_ok = other.lo <= self.lo;
        let hi_ok = self.hi <= other.hi;
        if lo_ok && hi_ok {
            if self.lo == other.lo && self.hi == other.hi {
                Some(std::cmp::Ordering::Equal)
            } else {
                Some(std::cmp::Ordering::Less)
            }
        } else if self.lo <= other.lo && other.hi <= self.hi {
            if self.lo == other.lo && self.hi == other.hi {
                Some(std::cmp::Ordering::Equal)
            } else {
                Some(std::cmp::Ordering::Greater)
            }
        } else {
            None
        }
    }
}

// Theorem preserved: instEpistemicCalculusPTbi
impl EpistemicCalculus for PTbi {
    fn fusion(x: &Self, y: &Self) -> Self {
        PTbi {
            lo: x.lo.max(y.lo),
            hi: x.hi.min(y.hi),
        }
    }

    fn unit() -> Self {
        ptbi_unit()
    }
}

// Theorem preserved: Optimistic PTbi — top = (0, 1)
impl Optimistic for PTbi {
    fn top() -> Self {
        ptbi_unit()
    }
}

// Theorem preserved: IdempotentFusion PTbi
impl IdempotentFusion for PTbi {}

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

/// IP (Interval Probabilities) is definitionally PTbi.
// Theorem preserved: ptbiIsoIp — the isomorphism is the identity
pub type IP = PTbi;

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

    #[test]
    fn fusion_comm() {
        let a = PTbi::new(0.2, 0.8);
        let b = PTbi::new(0.3, 0.9);
        assert_eq!(PTbi::fusion(&a, &b), PTbi::fusion(&b, &a));
    }

    #[test]
    fn fusion_assoc() {
        let a = PTbi::new(0.2, 0.8);
        let b = PTbi::new(0.3, 0.9);
        let c = PTbi::new(0.1, 0.7);
        assert_eq!(
            PTbi::fusion(&PTbi::fusion(&a, &b), &c),
            PTbi::fusion(&a, &PTbi::fusion(&b, &c))
        );
    }

    #[test]
    fn fusion_unit_left() {
        let a = PTbi::new(0.2, 0.8);
        assert_eq!(PTbi::fusion(&PTbi::unit(), &a), a);
    }

    #[test]
    fn idempotent() {
        let a = PTbi::new(0.2, 0.8);
        assert_eq!(PTbi::fusion(&a, &a), a);
    }

    #[test]
    fn nontrivial() {
        assert_ne!(ptbi_unit(), ptbi_inconsistent());
    }

    #[test]
    fn optimistic() {
        let a = PTbi::new(0.2, 0.8);
        assert!(a <= PTbi::top());
    }

    #[test]
    fn fusion_values() {
        let a = PTbi::new(0.2, 0.8);
        let b = PTbi::new(0.3, 0.9);
        let ab = PTbi::fusion(&a, &b);
        assert_eq!(ab.lo, 0.3); // max(0.2, 0.3)
        assert_eq!(ab.hi, 0.8); // min(0.8, 0.9)
    }

    #[test]
    fn ip_is_ptbi() {
        let ip: IP = PTbi::new(0.1, 0.9);
        let ptbi = PTbi::new(0.1, 0.9);
        assert_eq!(ip, ptbi);
    }
}