//! `lattice` — estados de retículo y restricciones de Galois (Addendum §D, T5).
//!
//! La pista de retículos (Ghrist–Riess 2022): reemplaza los espacios vectoriales
//! del MVP por **retículos** y las matrices por **conexiones de Galois**. No toca
//! el motor lineal (`cohomology`), que sigue como oráculo topológico barato.
//!
//! Aquí viven las piezas de grado 0: los tipos de retículo (`Nat`, `ResetVal`) y
//! la interfaz de restricción adjunta (`GaloisRestriction`). El Laplaciano de
//! Tarski que las difunde a punto fijo llega en T6 (`tarski`).

use std::cmp::Ordering;

/// Un estado local con estructura de retículo acotado (Addendum §D).
///
/// `join` (∨) y `meet` (∧) deben ser asociativos, conmutativos, idempotentes y
/// cumplir absorción; `bottom` (⊥) y `top` (⊤) son sus neutros/absorbentes.
pub trait LatticeCell: Clone + PartialOrd {
    /// Supremo ∨ (least upper bound).
    fn join(&self, other: &Self) -> Self;
    /// Ínfimo ∧ (greatest lower bound).
    fn meet(&self, other: &Self) -> Self;
    /// Elemento mínimo ⊥.
    fn bottom() -> Self;
    /// Elemento máximo ⊤.
    fn top() -> Self;
}

/// Una casilla de `GCounter` como cadena ℕ con ⊤ = ∞ (Addendum §D.1).
///
/// Join = máximo, meet = mínimo. Monótono por construcción: nunca resta. El
/// `GCounter` completo es el **producto** de estas cadenas (se arma en la stalk
/// del haz de retículos en T6).
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord)]
pub struct Nat(pub u64);

impl Nat {
    /// Representación de ∞ (el ⊤ de la cadena).
    pub const INF: Nat = Nat(u64::MAX);
}

impl LatticeCell for Nat {
    fn join(&self, other: &Self) -> Self {
        Nat(self.0.max(other.0))
    }
    fn meet(&self, other: &Self) -> Self {
        Nat(self.0.min(other.0))
    }
    fn bottom() -> Self {
        Nat(0)
    }
    fn top() -> Self {
        Nat::INF
    }
}

/// Un `ResettableRegister` como retículo donde el post-reset es **incomparable**
/// al pre-reset (Addendum §D.1). Dos generaciones distintas no tienen refinamiento
/// común no trivial: su join colapsa a ⊤ y su meet a ⊥. Ese colapso a ⊤ es la
/// señal de obstrucción **real** (semántica, no topológica) de la §C.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum ResetVal {
    /// ⊥.
    Bottom,
    /// Un valor concreto en una generación. Comparable solo dentro de su generación.
    Gen { generation: u64, value: i64 },
    /// ⊤ (colapso: no hay reconciliación no trivial).
    Top,
}

impl PartialOrd for ResetVal {
    fn partial_cmp(&self, other: &Self) -> Option<Ordering> {
        use ResetVal::*;
        match (self, other) {
            (Bottom, Bottom) | (Top, Top) => Some(Ordering::Equal),
            (Bottom, _) | (_, Top) => Some(Ordering::Less),
            (_, Bottom) | (Top, _) => Some(Ordering::Greater),
            (
                Gen { generation: g1, value: v1 },
                Gen { generation: g2, value: v2 },
            ) => {
                if g1 == g2 {
                    Some(v1.cmp(v2))
                } else {
                    None // generaciones distintas: incomparables
                }
            }
        }
    }
}

impl LatticeCell for ResetVal {
    fn join(&self, other: &Self) -> Self {
        use ResetVal::*;
        match (self, other) {
            (Bottom, x) | (x, Bottom) => x.clone(),
            (Top, _) | (_, Top) => Top,
            (
                Gen { generation: g1, value: v1 },
                Gen { generation: g2, value: v2 },
            ) => {
                if g1 == g2 {
                    Gen { generation: *g1, value: *v1.max(v2) }
                } else {
                    Top // incomparables → colapso
                }
            }
        }
    }

    fn meet(&self, other: &Self) -> Self {
        use ResetVal::*;
        match (self, other) {
            (Top, x) | (x, Top) => x.clone(),
            (Bottom, _) | (_, Bottom) => Bottom,
            (
                Gen { generation: g1, value: v1 },
                Gen { generation: g2, value: v2 },
            ) => {
                if g1 == g2 {
                    Gen { generation: *g1, value: *v1.min(v2) }
                } else {
                    Bottom
                }
            }
        }
    }

    fn bottom() -> Self {
        ResetVal::Bottom
    }
    fn top() -> Self {
        ResetVal::Top
    }
}

/// Un mapa de restricción como **conexión de Galois** (Addendum §D): un par
/// adjunto `(lower, upper)` que reemplaza a la matriz lineal del MVP.
///
/// Ley adjunta (monótona): `lower(a) ≤ b  ⟺  a ≤ upper(b)`. De ella se siguen
/// que `lower` preserva joins y `upper` preserva meets, sin necesidad de restar.
pub trait GaloisRestriction<A: LatticeCell, B: LatticeCell> {
    /// `F_{v⊴e}`: sube el estado local a la arista. Preserva joins.
    fn lower(&self, a: &A) -> B;
    /// `F_{v⊴e}^*`: la adjunta; baja de la arista al vértice. Preserva meets.
    fn upper(&self, b: &B) -> A;
}

/// La conexión de Galois identidad: comparten el mismo dato tal cual.
#[derive(Debug, Clone, Copy, Default)]
pub struct IdentityGalois;

impl<L: LatticeCell> GaloisRestriction<L, L> for IdentityGalois {
    fn lower(&self, a: &L) -> L {
        a.clone()
    }
    fn upper(&self, b: &L) -> L {
        b.clone()
    }
}

/// Conexión de Galois no trivial sobre ℕ: `lower(a) = k·a`, `upper(b) = ⌊b/k⌋`.
/// Es la adjunción clásica multiplicación/división: `k·a ≤ b ⟺ a ≤ ⌊b/k⌋`.
#[derive(Debug, Clone, Copy)]
pub struct ScaleGalois {
    /// Factor de escala, `k ≥ 1`.
    pub k: u64,
}

impl ScaleGalois {
    /// Crea una escala con `k ≥ 1` (satura en 1 si se pasa 0).
    pub fn new(k: u64) -> Self {
        Self { k: k.max(1) }
    }
}

impl GaloisRestriction<Nat, Nat> for ScaleGalois {
    fn lower(&self, a: &Nat) -> Nat {
        Nat(a.0.saturating_mul(self.k))
    }
    fn upper(&self, b: &Nat) -> Nat {
        Nat(b.0 / self.k)
    }
}

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

    /// Comprueba las cuatro leyes de retículo sobre una terna concreta.
    fn leyes_de_reticulo<L: LatticeCell + std::fmt::Debug>(a: &L, b: &L, c: &L) {
        // Conmutatividad.
        assert_eq!(a.join(b), b.join(a));
        assert_eq!(a.meet(b), b.meet(a));
        // Asociatividad.
        assert_eq!(a.join(b).join(c), a.join(&b.join(c)));
        assert_eq!(a.meet(b).meet(c), a.meet(&b.meet(c)));
        // Idempotencia.
        assert_eq!(a.join(a), a.clone());
        assert_eq!(a.meet(a), a.clone());
        // Absorción.
        assert_eq!(a.join(&a.meet(b)), a.clone());
        assert_eq!(a.meet(&a.join(b)), a.clone());
        // Neutros.
        assert_eq!(a.join(&L::bottom()), a.clone());
        assert_eq!(a.meet(&L::top()), a.clone());
    }

    fn nat_st() -> impl Strategy<Value = Nat> {
        (0u64..10_000).prop_map(Nat)
    }

    fn reset_st() -> impl Strategy<Value = ResetVal> {
        prop_oneof![
            Just(ResetVal::Bottom),
            Just(ResetVal::Top),
            (0u64..4, -100i64..100)
                .prop_map(|(generation, value)| ResetVal::Gen { generation, value }),
        ]
    }

    proptest! {
        #[test]
        fn nat_es_reticulo(a in nat_st(), b in nat_st(), c in nat_st()) {
            leyes_de_reticulo(&a, &b, &c);
        }

        #[test]
        fn resetval_es_reticulo(a in reset_st(), b in reset_st(), c in reset_st()) {
            leyes_de_reticulo(&a, &b, &c);
        }

        /// Generaciones distintas colapsan: su join es ⊤ y su meet es ⊥.
        #[test]
        fn reset_incomparable_colapsa(v1 in -100i64..100, v2 in -100i64..100) {
            let a = ResetVal::Gen { generation: 0, value: v1 };
            let b = ResetVal::Gen { generation: 1, value: v2 };
            prop_assert!(a.partial_cmp(&b).is_none(), "gen distintas son incomparables");
            prop_assert_eq!(a.join(&b), ResetVal::Top);
            prop_assert_eq!(a.meet(&b), ResetVal::Bottom);
        }

        /// Ley adjunta de Galois para la identidad: trivial pero debe cumplirse.
        #[test]
        fn galois_identidad(a in nat_st(), b in nat_st()) {
            let g = IdentityGalois;
            prop_assert_eq!(g.lower(&a) <= b, a <= g.upper(&b));
        }

        /// Ley adjunta de Galois para la escala k·a ≤ b ⟺ a ≤ ⌊b/k⌋, y
        /// monotonía de `lower`.
        #[test]
        fn galois_escala(a in 0u64..1000, a2 in 0u64..1000, b in 0u64..1000, k in 1u64..8) {
            let g = ScaleGalois::new(k);
            let (na, nb) = (Nat(a), Nat(b));
            prop_assert_eq!(g.lower(&na) <= nb, na <= g.upper(&nb), "ley adjunta");
            // Monotonía de lower: a ≤ a' ⟹ lower(a) ≤ lower(a').
            let (lo, hi) = (Nat(a.min(a2)), Nat(a.max(a2)));
            prop_assert!(g.lower(&lo) <= g.lower(&hi));
        }
    }
}