//! Quick verification — processes only 10 core HOL theories.
//! Gives fast, actionable data for Phase 47.

#[cfg(test)]
mod quick_verify {
    use std::{path::Path, time::Instant};

    use isabelle_rs::{core::theory::Theory, theory::loader::TheoryProcessor};

    const CORE_FILES: &[(&str, &str)] = &[
        ("HOL", "isabelle-source/src/HOL/HOL.thy"),
        ("Orderings", "isabelle-source/src/HOL/Orderings.thy"),
        ("Set", "isabelle-source/src/HOL/Set.thy"),
        ("Fun", "isabelle-source/src/HOL/Fun.thy"),
        ("Product_Type", "isabelle-source/src/HOL/Product_Type.thy"),
    ];

    const EXTRA_FILES: &[(&str, &str)] = &[
        ("Nat", "isabelle-source/src/HOL/Nat.thy"),
        ("List", "isabelle-source/src/HOL/List.thy"),
        ("Option", "isabelle-source/src/HOL/Option.thy"),
        ("Lattices", "isabelle-source/src/HOL/Lattices.thy"),
        ("Groups", "isabelle-source/src/HOL/Groups.thy"),
    ];

    #[test]
    fn test_batch1_core() {
        verify_files(CORE_FILES, "Batch 1 — Core");
    }

    #[test]
    fn test_batch2_extra() {
        verify_files(EXTRA_FILES, "Batch 2 — Extra");
    }

    fn verify_files(files: &[(&str, &str)], label: &str) {
        let mut total_theorems = 0usize;
        let mut total_errors = 0usize;
        let mut total_time = 0f64;
        let mut ok_count = 0usize;

        eprintln!("\n╔══════════════════════════════════════════════╗");
        eprintln!("║   {} — {} HOL Theories        ║", label, files.len());
        eprintln!("╚══════════════════════════════════════════════╝\n");

        for (name, path_str) in files {
            let path = Path::new(path_str);
            if !path.exists() {
                eprintln!("  ❓ {:>15} — file not found", name);
                continue;
            }

            let start = Instant::now();
            let source = match std::fs::read_to_string(path) {
                Ok(s) => s,
                Err(e) => {
                    eprintln!("  ❌ {:>15} — read error: {}", name, e);
                    total_errors += 1;
                    continue;
                },
            };

            let mut proc = TheoryProcessor::with_parent(Theory::pure(), name);
            proc.accept_all = true; // accept_all: avoids deep recursion in BNF generation
            let _thy = proc.process_source(&source);
            let elapsed = start.elapsed();

            let thms = proc.theorem_count();
            let errs = proc.errors().len();
            let icon = if errs == 0 { "✅" } else { "⚠️" };

            eprintln!(
                "  {} {:>15} — {:>4} thms, {:>3} errs, {:>6.1}ms",
                icon,
                name,
                thms,
                errs,
                elapsed.as_secs_f64() * 1000.0
            );

            total_theorems += thms;
            total_errors += errs;
            total_time += elapsed.as_secs_f64();

            if errs == 0 {
                ok_count += 1;
            } else {
                // Show first few errors
                for (i, e) in proc.errors().iter().take(3).enumerate() {
                    let short: String = e.chars().take(100).collect();
                    eprintln!("       {} {}", i + 1, short);
                }
            }
        }

        eprintln!("\n───────────────────────────────────────────────");
        eprintln!(
            "  Total: {} theorems, {} errors, {:.1}s",
            total_theorems, total_errors, total_time
        );
        eprintln!("  Passed: {}/{} files", ok_count, CORE_FILES.len());
        eprintln!("───────────────────────────────────────────────\n");

        // At minimum, some core files should verify
        assert!(total_theorems > 0, "No theorems generated from core files!");
    }
}
