pr4xis 0.5.0

use super::property::Quality;
use crate::category::{Category, Entity, Relationship};
use crate::logic::Axiom;
use crate::ontology::Ontology;
use proptest::prelude::*;

// =============================================================================
// Example: Traffic Light Ontology
//
// Individuals: Red, Yellow, Green
// Relations: transitions between lights (including composites for closure)
// Qualities: duration (how long each light stays on)
// Axioms: no dead states, green is the longest phase
// =============================================================================

#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
enum Light {
    Red,
    Yellow,
    Green,
}

impl Entity for Light {
    fn variants() -> Vec<Self> {
        vec![Light::Red, Light::Yellow, Light::Green]
    }
}

#[derive(Debug, Clone, PartialEq, Eq)]
enum LightTransition {
    Identity(Light),
    RedToGreen,
    GreenToYellow,
    YellowToRed,
    RedToYellow,
    GreenToRed,
    YellowToGreen,
}

impl Relationship for LightTransition {
    type Object = Light;

    fn source(&self) -> Light {
        match self {
            LightTransition::Identity(l) => *l,
            LightTransition::RedToGreen | LightTransition::RedToYellow => Light::Red,
            LightTransition::GreenToYellow | LightTransition::GreenToRed => Light::Green,
            LightTransition::YellowToRed | LightTransition::YellowToGreen => Light::Yellow,
        }
    }

    fn target(&self) -> Light {
        match self {
            LightTransition::Identity(l) => *l,
            LightTransition::RedToGreen | LightTransition::YellowToGreen => Light::Green,
            LightTransition::GreenToYellow | LightTransition::RedToYellow => Light::Yellow,
            LightTransition::YellowToRed | LightTransition::GreenToRed => Light::Red,
        }
    }
}

struct TrafficLightCat;

impl Category for TrafficLightCat {
    type Object = Light;
    type Morphism = LightTransition;

    fn identity(obj: &Light) -> LightTransition {
        LightTransition::Identity(*obj)
    }

    fn compose(f: &LightTransition, g: &LightTransition) -> Option<LightTransition> {
        if f.target() != g.source() {
            return None;
        }
        if let LightTransition::Identity(_) = f {
            return Some(g.clone());
        }
        if let LightTransition::Identity(_) = g {
            return Some(f.clone());
        }
        Some(match (f.source(), g.target()) {
            (s, t) if s == t => LightTransition::Identity(s),
            (Light::Red, Light::Yellow) => LightTransition::RedToYellow,
            (Light::Red, Light::Green) => LightTransition::RedToGreen,
            (Light::Green, Light::Red) => LightTransition::GreenToRed,
            (Light::Green, Light::Yellow) => LightTransition::GreenToYellow,
            (Light::Yellow, Light::Green) => LightTransition::YellowToGreen,
            (Light::Yellow, Light::Red) => LightTransition::YellowToRed,
            _ => return None,
        })
    }

    fn morphisms() -> Vec<LightTransition> {
        vec![
            LightTransition::Identity(Light::Red),
            LightTransition::Identity(Light::Yellow),
            LightTransition::Identity(Light::Green),
            LightTransition::RedToGreen,
            LightTransition::GreenToYellow,
            LightTransition::YellowToRed,
            LightTransition::RedToYellow,
            LightTransition::GreenToRed,
            LightTransition::YellowToGreen,
        ]
    }
}

// --- Quality: duration of each light phase ---

#[derive(Debug, Clone)]
struct Duration;

impl Quality for Duration {
    type Individual = Light;
    type Value = u32; // seconds

    fn get(&self, individual: &Light) -> Option<u32> {
        match individual {
            Light::Red => Some(30),
            Light::Yellow => Some(5),
            Light::Green => Some(45),
        }
    }
}

// --- Axiom: green must be the longest phase ---

struct GreenIsLongest;

impl Axiom for GreenIsLongest {
    fn description(&self) -> &str {
        "green phase must be the longest"
    }

    fn holds(&self) -> bool {
        let dur = Duration;
        let green_dur = dur.get(&Light::Green).unwrap_or(0);
        Light::variants()
            .iter()
            .all(|l| dur.get(l).unwrap_or(0) <= green_dur)
    }
}

// --- Axiom: no dead states ---

struct NoDeadStates;

impl Axiom for NoDeadStates {
    fn description(&self) -> &str {
        "every light has at least one outgoing transition"
    }

    fn holds(&self) -> bool {
        Light::variants()
            .iter()
            .all(|obj| !TrafficLightCat::morphisms_from(obj).is_empty())
    }
}

// --- Ontology: tie it all together ---

struct TrafficLightOntology;

impl Ontology for TrafficLightOntology {
    type Cat = TrafficLightCat;
    type Qual = Duration;

    fn axioms() -> Vec<Box<dyn Axiom>> {
        vec![Box::new(GreenIsLongest), Box::new(NoDeadStates)]
    }
}

// =============================================================================
// Proptest strategies
// =============================================================================

fn arb_light() -> impl Strategy<Value = Light> {
    prop_oneof![Just(Light::Red), Just(Light::Yellow), Just(Light::Green),]
}

fn arb_transition() -> impl Strategy<Value = LightTransition> {
    prop_oneof![
        arb_light().prop_map(LightTransition::Identity),
        Just(LightTransition::RedToGreen),
        Just(LightTransition::GreenToYellow),
        Just(LightTransition::YellowToRed),
        Just(LightTransition::RedToYellow),
        Just(LightTransition::GreenToRed),
        Just(LightTransition::YellowToGreen),
    ]
}

// =============================================================================
// Property-based tests — Ontology invariants
// =============================================================================

proptest! {
    /// Ontology validation succeeds structurally
    #[test]
    fn prop_ontology_validates(_obj in arb_light()) {
        prop_assert!(TrafficLightOntology::validate().is_ok());
    }

    /// Every individual has a quality value (total quality)
    #[test]
    fn prop_duration_is_total(individual in arb_light()) {
        let dur = Duration;
        prop_assert!(dur.get(&individual).is_some());
    }

    /// Duration is always positive
    #[test]
    fn prop_duration_is_positive(individual in arb_light()) {
        let dur = Duration;
        let val = dur.get(&individual).unwrap();
        prop_assert!(val > 0);
    }

    /// Green is always >= any other light's duration
    #[test]
    fn prop_green_is_longest(individual in arb_light()) {
        let dur = Duration;
        let green = dur.get(&Light::Green).unwrap();
        let other = dur.get(&individual).unwrap();
        prop_assert!(green >= other);
    }

    /// Every individual has outgoing morphisms
    #[test]
    fn prop_no_dead_states(individual in arb_light()) {
        let outgoing = TrafficLightCat::morphisms_from(&individual);
        prop_assert!(!outgoing.is_empty());
    }

    /// Every individual has incoming morphisms
    #[test]
    fn prop_no_orphan_states(individual in arb_light()) {
        let incoming = TrafficLightCat::morphisms_to(&individual);
        prop_assert!(!incoming.is_empty());
    }

    /// Qualities are deterministic
    #[test]
    fn prop_quality_deterministic(individual in arb_light()) {
        let dur = Duration;
        prop_assert_eq!(dur.get(&individual), dur.get(&individual));
    }

    /// individuals_with returns all when quality is total
    #[test]
    fn prop_individuals_with_complete(_individual in arb_light()) {
        let dur = Duration;
        prop_assert_eq!(dur.individuals_with().len(), Light::variants().len());
    }

    /// All axioms hold for any context
    #[test]
    fn prop_all_axioms_hold(_individual in arb_light()) {
        for axiom in TrafficLightOntology::axioms() {
            prop_assert!(axiom.holds(), "Axiom failed: {}", axiom.description());
        }
    }
}

// =============================================================================
// Property-based tests — Category laws via Ontology
// =============================================================================

proptest! {
    /// Left identity
    #[test]
    fn prop_left_identity(m in arb_transition()) {
        let id = TrafficLightCat::identity(&m.source());
        prop_assert_eq!(TrafficLightCat::compose(&id, &m), Some(m));
    }

    /// Right identity
    #[test]
    fn prop_right_identity(m in arb_transition()) {
        let id = TrafficLightCat::identity(&m.target());
        prop_assert_eq!(TrafficLightCat::compose(&m, &id), Some(m));
    }

    /// Associativity
    #[test]
    fn prop_associativity(f in arb_transition(), g in arb_transition(), h in arb_transition()) {
        let fg = TrafficLightCat::compose(&f, &g);
        let gh = TrafficLightCat::compose(&g, &h);
        let left = fg.as_ref().and_then(|fg| TrafficLightCat::compose(fg, &h));
        let right = gh.as_ref().and_then(|gh| TrafficLightCat::compose(&f, gh));
        prop_assert_eq!(left, right);
    }

    /// Closure: composable pairs always produce Some
    #[test]
    fn prop_closure(f in arb_transition(), g in arb_transition()) {
        if f.target() == g.source() {
            prop_assert!(TrafficLightCat::compose(&f, &g).is_some());
        }
    }

    /// Morphism endpoints are valid
    #[test]
    fn prop_morphism_endpoints_valid(m in arb_transition()) {
        let variants = Light::variants();
        prop_assert!(variants.contains(&m.source()));
        prop_assert!(variants.contains(&m.target()));
    }

    /// Incompatible composition returns None
    #[test]
    fn prop_type_safety(f in arb_transition(), g in arb_transition()) {
        if f.target() != g.source() {
            prop_assert_eq!(TrafficLightCat::compose(&f, &g), None);
        }
    }
}

// =============================================================================
// Exhaustive tests
// =============================================================================

#[test]
fn test_ontology_validates() {
    TrafficLightOntology::validate().unwrap();
}

#[test]
fn test_ontology_check() {
    super::validate::check_ontology::<TrafficLightOntology>().unwrap();
}

#[test]
fn test_quality_get() {
    let dur = Duration;
    assert_eq!(dur.get(&Light::Red), Some(30));
    assert_eq!(dur.get(&Light::Yellow), Some(5));
    assert_eq!(dur.get(&Light::Green), Some(45));
}

#[test]
fn test_quality_individuals_with() {
    let dur = Duration;
    assert_eq!(dur.individuals_with().len(), 3);
}

#[test]
fn test_axiom_green_is_longest() {
    assert!(GreenIsLongest.holds());
}

#[test]
fn test_axiom_no_dead_states() {
    assert!(NoDeadStates.holds());
}