//! Binario de `sheafsync`. Hito M1 (§8): dos corridas de signo opuesto que
//! prueban el núcleo entero de punta a punta.
//!
//! - Corrida A (G-Counter, monótono): compartición acíclica → `H¹ = 0` → corre libre.
//! - Corrida B (ResettableRegister, no monótono): el reset introduce un enlace
//!   irreconciliable sobre el dato ya compartido por las réplicas 1 y 2 → ciclo
//!   localizado → `H¹ ≠ 0` → coordina ahí.

use sheafsync::cell::{Cell, GCounter, ResettableRegister};
use sheafsync::cohomology::{self, Cohomology};
use sheafsync::invariant::AccountConfig;
use sheafsync::oracle::{Config, Share};
use sheafsync::sheaf::Sheaf;
use sheafsync::verdict::Verdict;

fn main() {
    println!("sheafsync — hito M1\n");
    corrida_a();
    println!();
    corrida_b();
    println!();
    contraste_tarski();
    println!();
    contraste_invariante();
}

/// Imprime el veredicto de un haz ya construido.
fn veredicto(nombre: &str, sheaf: &Sheaf) -> Cohomology {
    let coho = cohomology::compute(sheaf).expect("haz bien formado");
    let verdict = Verdict::diagnose(sheaf, &coho);
    println!(
        "  cohomología: dim H⁰ = {}, dim H¹ = {}  (rank δ = {}, dim C⁰ = {}, dim C¹ = {})",
        coho.dim_h0, coho.dim_h1, coho.rank_delta, coho.dim_c0, coho.dim_c1
    );
    println!("  veredicto [{nombre}]: {verdict}");
    coho
}

/// Corrida A — G-Counter monótono sobre 3 réplicas que comparten en camino.
///
/// Cada réplica incrementa solo su casilla y difunde el vector a sus vecinas.
/// Al fundir por máximo siempre convergen; la compartición es acíclica, así que
/// no hay obstrucción posible: `H¹ = 0`.
fn corrida_a() {
    println!("Corrida A — G-Counter (monótono: {})", GCounter::is_monotone());

    // Demostración del CRDT: tres réplicas incrementan lo suyo y se funden.
    let mut r0 = GCounter::zeros(3);
    let mut r1 = GCounter::zeros(3);
    let mut r2 = GCounter::zeros(3);
    r0.increment(0, 5);
    r1.increment(1, 3);
    r2.increment(2, 7);
    let fundido = r0.join(&r1).join(&r2);
    println!(
        "  merge de las 3 réplicas: {:?}  (valor total = {})",
        fundido.slots,
        fundido.value()
    );

    // Haz: stalk = el vector contador (ℤ³), restricciones = identidad (comparten
    // el vector completo), topología = camino 0—1—2 (acíclica).
    let sheaf = Sheaf::constant(3, &[(0, 1), (1, 2)], 3);
    veredicto("A", &sheaf);
}

/// Corrida B — ResettableRegister no monótono sobre 3 réplicas en ciclo.
///
/// Las réplicas 1 y 2 comparten un registro. El reset (no monótono) impone un
/// segundo enlace sobre ese mismo dato que no puede reconciliarse globalmente:
/// forma un ciclo entre 1 y 2. El haz lo detecta y lo localiza ahí.
fn corrida_b() {
    println!(
        "Corrida B — ResettableRegister (monótono: {})",
        ResettableRegister::is_monotone()
    );

    // Demostración del CRDT: un reset con valor menor gana por generación.
    let alto = ResettableRegister::new(10);
    let mut reseteado = alto.clone();
    reseteado.reset(0);
    let fundido = alto.join(&reseteado);
    println!(
        "  merge tras reset: value = {} (gen {}) — el reset retracta el 10 previo",
        fundido.value, fundido.generation
    );

    // Haz: stalk = valor del registro (escalar), restricciones = identidad.
    // Aristas: 0—1 (single) y un DOBLE enlace 1—2 (el original + el que fuerza el
    // reset), irreconciliables → ciclo localizado entre réplicas 1 y 2.
    let sheaf = Sheaf::constant(3, &[(0, 1), (1, 2), (1, 2)], 1);
    veredicto("B", &sheaf);
}

/// Contraste de la pista de retículos (Addendum §F): el triángulo monótono.
///
/// El motor LINEAL ve la topología del ciclo e inventa una obstrucción; la
/// difusión de TARSKI reconcilia el dato monótono sin colapsar → corre libre,
/// igualando a CALM. Es la brecha de modelado (§2.3) cerrada, en vivo.
fn contraste_tarski() {
    println!("Contraste — triángulo monótono (0—1—2—0, dato que se funde solo)");

    let triangulo = Config::new(
        "triangulo-monotono",
        3,
        vec![
            Share::monotona(0, 1),
            Share::monotona(1, 2),
            Share::monotona(2, 0),
        ],
    );

    println!("  oráculo (CALM):     {:?}", triangulo.oracle_verdict());
    println!(
        "  haz lineal (H¹):    {:?}   ← falsa obstrucción topológica",
        triangulo.sheaf_verdict()
    );
    println!(
        "  difusión de Tarski: {:?}      ← reconcilia al join, discrepancia RESUELTA",
        triangulo.tarski_verdict()
    );
}

/// La discrepancia buena (T8c, §D): donde de verdad se supera al CALM sintáctico.
///
/// Dos réplicas retiran 10 de una cuenta de 100 (invariante: saldo ≥ 0). Los
/// valores caben → el haz (I-confluence sobre el grafo) corre libre; el CALM
/// sintáctico condena el retiro por-programa. Análisis sensible a la instancia.
fn contraste_invariante() {
    println!("Discrepancia buena — retiros que caben (saldo ≥ 0, cuenta de 100)");

    let caben = AccountConfig::new("retiros-que-caben", 100, vec![10, 10], vec![(0, 1)]);
    let sobregiran = AccountConfig::new("sobregiran", 100, vec![60, 60], vec![(0, 1)]);

    println!("  A) retiros [10,10] → Σ=20 ≤ 100:");
    println!("     CALM sintáctico: {:?}  (condena el retiro)", caben.calm_syntactic());
    println!(
        "     haz (I-confluence): {:?}   ← corre libre: los valores pegan",
        caben.haz_coordination()
    );
    println!("  B) retiros [60,60] → Σ=120 > 100:");
    println!(
        "     haz (I-confluence): {:?}   ← coordina: el merge rompe el invariante",
        sobregiran.haz_coordination()
    );
}