//! `oracle` — evaluador CRDT/CALM de referencia, independiente del haz (§8 M3).
//!
//! Para cada configuración el oráculo dice, por CALM puro (monotonicidad de las
//! operaciones compartidas), si es coordination-free — sin mirar el haz. El test
//! maestro compara ese veredicto con el del haz para validar la Hipótesis H
//! (§2.2). Donde discrepan (§11 R1) se documenta en `DISCREPANCIES.md`.

use crate::cohomology::compute_with;
use crate::gf2::Gf2Backend;
use crate::lattice::{IdentityGalois, ResetVal};
use crate::sheaf::Sheaf;
use crate::tarski::LatticeSheaf;
use crate::verdict::Verdict;

/// Predicción independiente del oráculo para una configuración.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum OracleVerdict {
    /// El oráculo cree que la configuración es libre de coordinación.
    CoordinationFree,
    /// El oráculo cree que hace falta coordinar.
    NeedsCoordination,
}

/// Un dato compartido entre dos réplicas, con la marca CALM de si la operación
/// que lo toca es monótona.
#[derive(Debug, Clone, Copy)]
pub struct Share {
    /// Primera réplica que comparte.
    pub a: usize,
    /// Segunda réplica que comparte.
    pub b: usize,
    /// ¿La operación sobre este dato es monótona? (viene de `Cell::is_monotone`).
    pub monotone: bool,
}

impl Share {
    /// Dato compartido monótono (se funde solo).
    pub fn monotona(a: usize, b: usize) -> Self {
        Self { a, b, monotone: true }
    }

    /// Dato compartido no monótono (reset/overwrite → posible conflicto).
    pub fn no_monotona(a: usize, b: usize) -> Self {
        Self { a, b, monotone: false }
    }
}

/// Una configuración de réplicas con sus datos compartidos.
#[derive(Debug, Clone)]
pub struct Config {
    /// Nombre del caso (para reportes).
    pub name: String,
    /// Número de réplicas.
    pub replicas: usize,
    /// Datos compartidos.
    pub shares: Vec<Share>,
}

impl Config {
    /// Construye una configuración.
    pub fn new(name: impl Into<String>, replicas: usize, shares: Vec<Share>) -> Self {
        Self {
            name: name.into(),
            replicas,
            shares,
        }
    }

    /// **Oráculo CALM (independiente del haz).** Coordination-free ⟺ toda
    /// operación compartida es monótona. En cuanto aparece una no monótona
    /// compartida, CALM exige coordinación.
    pub fn oracle_verdict(&self) -> OracleVerdict {
        if self.shares.iter().all(|s| s.monotone) {
            OracleVerdict::CoordinationFree
        } else {
            OracleVerdict::NeedsCoordination
        }
    }

    /// Codificación lineal de la configuración como haz (la codificación honesta
    /// de la §2.3, sin colapsar ciclos monótonos):
    /// - cada dato compartido → una arista de acuerdo (restricción identidad);
    /// - una operación no monótona añade un segundo enlace en conflicto sobre el
    ///   mismo par → un 2-ciclo localizado (como la Corrida B de M1).
    pub fn to_sheaf(&self) -> Sheaf {
        let mut edges = Vec::new();
        for s in &self.shares {
            edges.push((s.a, s.b));
            if !s.monotone {
                edges.push((s.a, s.b)); // el reset impone un segundo constraint irreconciliable
            }
        }
        Sheaf::constant(self.replicas, &edges, 1)
    }

    /// **Veredicto del haz lineal.** Coordination-free ⟺ `H¹ = 0`. Usa la
    /// aritmética exacta `GF(2)`. Es el detector topológico barato del MVP.
    pub fn sheaf_verdict(&self) -> OracleVerdict {
        let sheaf = self.to_sheaf();
        let coho = compute_with(&sheaf, &Gf2Backend).expect("haz bien formado");
        if coho.dim_h1 == 0 {
            OracleVerdict::CoordinationFree
        } else {
            OracleVerdict::NeedsCoordination
        }
    }

    /// Generación de retículo por réplica = componente del **subgrafo monótono**.
    /// Réplicas ligadas por datos monótonos comparten generación (comparables);
    /// las separadas por una operación no monótona caen en generaciones distintas
    /// (incomparables → su reconciliación colapsa a ⊤).
    fn monotone_generations(&self) -> Vec<u64> {
        let mut parent: Vec<usize> = (0..self.replicas).collect();
        fn find(parent: &mut [usize], x: usize) -> usize {
            let mut r = x;
            while parent[r] != r {
                r = parent[r];
            }
            r
        }
        for s in &self.shares {
            if s.monotone {
                let ra = find(&mut parent, s.a);
                let rb = find(&mut parent, s.b);
                if ra != rb {
                    parent[ra] = rb;
                }
            }
        }
        (0..self.replicas).map(|r| find(&mut parent, r) as u64).collect()
    }

    /// **Veredicto por difusión de Tarski** (Addendum §C, T7): encoda la config
    /// como haz de retículos (`ResetVal` uniforme, restricción identidad),
    /// siembra cada réplica en la generación de su componente monótona, y
    /// harmoniza. Coordination-free ⟺ el punto fijo no colapsa a ⊤.
    pub fn tarski_verdict(&self) -> OracleVerdict {
        let gens = self.monotone_generations();
        let seed: Vec<ResetVal> = (0..self.replicas)
            .map(|r| ResetVal::Gen {
                generation: gens[r],
                value: r as i64,
            })
            .collect();
        let sheaf = LatticeSheaf::new(
            self.replicas,
            self.shares.iter().map(|s| (s.a, s.b)).collect(),
            IdentityGalois,
        );
        match Verdict::via_tarski(&sheaf, &seed) {
            Verdict::RunsFree => OracleVerdict::CoordinationFree,
            Verdict::NeedsCoordination { .. } => OracleVerdict::NeedsCoordination,
        }
    }
}

/// Batería de casos donde el haz y el oráculo **coinciden** (§8 M3, ≥20 casos).
///
/// Régimen de acuerdo: sharing monótono acíclico (→ ambos "corre libre") y
/// cualquier configuración con al menos una operación no monótona (→ ambos
/// "coordina"). El test maestro verifica la coincidencia en todos.
pub fn casos_de_acuerdo() -> Vec<Config> {
    let mut casos = Vec::new();

    // --- Monótonos acíclicos → CoordinationFree ---
    // Caminos de longitud creciente.
    for k in 2..=10 {
        let shares = (0..k - 1).map(|i| Share::monotona(i, i + 1)).collect();
        casos.push(Config::new(format!("camino-monotono-{k}"), k, shares));
    }
    // Estrella (centro 0, hojas 1..=4).
    casos.push(Config::new(
        "estrella-monotona",
        5,
        (1..=4).map(|h| Share::monotona(0, h)).collect(),
    ));
    // Árbol binario.
    casos.push(Config::new(
        "arbol-binario-monotono",
        5,
        vec![
            Share::monotona(0, 1),
            Share::monotona(0, 2),
            Share::monotona(1, 3),
            Share::monotona(1, 4),
        ],
    ));
    // Bosque desconexo (dos árboles).
    casos.push(Config::new(
        "bosque-monotono",
        5,
        vec![
            Share::monotona(0, 1),
            Share::monotona(1, 2),
            Share::monotona(3, 4),
        ],
    ));
    // Réplicas sin compartir nada (trivialmente libre).
    casos.push(Config::new("aislado", 3, vec![]));

    // --- Con operación no monótona → NeedsCoordination ---
    // Par único con reset.
    casos.push(Config::new(
        "par-no-monotono",
        2,
        vec![Share::no_monotona(0, 1)],
    ));
    // Camino monótono con un reset en un tramo (localiza el nudo ahí).
    for reset_edge in 0..3 {
        let mut shares: Vec<Share> = (0..3).map(|i| Share::monotona(i, i + 1)).collect();
        shares[reset_edge] = Share::no_monotona(reset_edge, reset_edge + 1);
        casos.push(Config::new(
            format!("camino-con-reset-en-{reset_edge}"),
            4,
            shares,
        ));
    }
    // Dos resets independientes en partes distintas.
    casos.push(Config::new(
        "dos-resets-separados",
        4,
        vec![Share::no_monotona(0, 1), Share::no_monotona(2, 3)],
    ));
    // Estrella monótona con una hoja reseteada.
    casos.push(Config::new(
        "estrella-con-reset",
        5,
        vec![
            Share::monotona(0, 1),
            Share::monotona(0, 2),
            Share::monotona(0, 3),
            Share::no_monotona(0, 4),
        ],
    ));
    // Árbol grande con reset en una rama.
    casos.push(Config::new(
        "arbol-con-reset",
        6,
        vec![
            Share::monotona(0, 1),
            Share::monotona(1, 2),
            Share::monotona(2, 3),
            Share::monotona(1, 4),
            Share::no_monotona(4, 5),
        ],
    ));
    // Todo no monótono.
    casos.push(Config::new(
        "todo-reset",
        3,
        vec![Share::no_monotona(0, 1), Share::no_monotona(1, 2)],
    ));

    casos
}

/// Casos donde el haz y el oráculo **discrepan** (§11 R1): dato monótono sobre
/// un grafo de compartición **cíclico**. CALM dice coordination-free (el join
/// existe siempre), pero la codificación lineal ve la obstrucción topológica del
/// ciclo (`H¹ = b₁ ≠ 0`). Documentados en `DISCREPANCIES.md`.
pub fn casos_de_discrepancia() -> Vec<Config> {
    vec![
        Config::new(
            "triangulo-monotono",
            3,
            vec![
                Share::monotona(0, 1),
                Share::monotona(1, 2),
                Share::monotona(2, 0),
            ],
        ),
        Config::new(
            "cuadrado-monotono",
            4,
            vec![
                Share::monotona(0, 1),
                Share::monotona(1, 2),
                Share::monotona(2, 3),
                Share::monotona(3, 0),
            ],
        ),
    ]
}

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

    /// Test maestro (§8 M3): el veredicto del haz coincide con el del oráculo en
    /// toda la batería de acuerdo, que tiene ≥20 casos.
    #[test]
    fn haz_coincide_con_oraculo() {
        let casos = casos_de_acuerdo();
        assert!(casos.len() >= 20, "la batería debe tener ≥20 casos, tiene {}", casos.len());
        for c in &casos {
            assert_eq!(
                c.sheaf_verdict(),
                c.oracle_verdict(),
                "discrepancia inesperada en el caso '{}'",
                c.name
            );
        }
    }

    /// Las discrepancias del MVP **lineal** (R1) son reales y esperadas: el haz
    /// topológico dice coordinar donde CALM dice libre. Es el control histórico.
    #[test]
    fn discrepancias_del_lineal_persisten() {
        for c in casos_de_discrepancia() {
            assert_eq!(c.oracle_verdict(), OracleVerdict::CoordinationFree);
            assert_eq!(
                c.sheaf_verdict(),
                OracleVerdict::NeedsCoordination,
                "el ciclo monótono '{}' produce una falsa obstrucción topológica",
                c.name
            );
        }
    }

    /// Test maestro de la pista de retículos (Addendum §F): el veredicto de
    /// **Tarski** coincide con el oráculo en TODA la batería de acuerdo.
    #[test]
    fn tarski_coincide_con_oraculo() {
        for c in &casos_de_acuerdo() {
            assert_eq!(
                c.tarski_verdict(),
                c.oracle_verdict(),
                "Tarski discrepa del oráculo en '{}'",
                c.name
            );
        }
    }

    /// El cierre (Addendum §F): donde el MVP lineal inventaba obstrucción
    /// (ciclo monótono), Tarski la **disuelve** y coincide con el oráculo. Las
    /// discrepancias de `DISCREPANCIES.md` quedan RESUELTAS.
    #[test]
    fn tarski_resuelve_las_discrepancias_del_lineal() {
        for c in casos_de_discrepancia() {
            // El lineal dice coordinar (falso positivo)...
            assert_eq!(c.sheaf_verdict(), OracleVerdict::NeedsCoordination);
            // ...pero Tarski corre libre, igualando al oráculo.
            assert_eq!(c.oracle_verdict(), OracleVerdict::CoordinationFree);
            assert_eq!(
                c.tarski_verdict(),
                OracleVerdict::CoordinationFree,
                "Tarski debe disolver la falsa obstrucción de '{}'",
                c.name
            );
        }
    }
}