//! End-to-end integration tests for the full isabelle-rs pipeline.
//! Tests theory loading, lemma parsing, proof verification, and theorem generation.

use isabelle_rs::{
    core::{
        term::Term,
        theory::Theory,
        thm::{CTerm, ThmKernel},
        types::{Typ, TypeEnv},
    },
    hol::hol_loader::*,
    theory::loader::TheoryProcessor,
};

fn declare_term(term: &Term, env: &mut TypeEnv) {
    match term {
        Term::Const { name, typ } if !typ.is_dummy() && !name.as_ref().starts_with("Pure.") => {
            env.declare_const(name.as_ref(), typ.clone());
        },
        Term::Free { name, typ } if !typ.is_dummy() => {
            env.declare_free(name.as_ref(), typ.clone());
        },
        Term::Abs { body, .. } => declare_term(body, env),
        Term::App { func, arg } => {
            declare_term(func, env);
            declare_term(arg, env);
        },
        Term::Const { .. } | Term::Free { .. } | Term::Var { .. } | Term::Bound(_) => {},
    }
}

fn checked_cterm(term: Term) -> CTerm {
    let mut env = TypeEnv::new();
    declare_term(&term, &mut env);
    CTerm::certify_checked(term, &env).expect("integration fixture should certify as checked")
}

#[test]
fn test_kernel_15_ops() {
    // Verify all 15 kernel operations are functional
    let t = checked_cterm(Term::const_("A", Typ::base("prop")));

    // 1. assume
    let thm = ThmKernel::assume(t.clone()).unwrap();
    assert_eq!(thm.nprems(), 0);

    // 2. reflexive
    let refl = ThmKernel::reflexive(t.clone()).unwrap();

    // 3. symmetric
    let _sym = ThmKernel::symmetric(&refl).unwrap();

    // 4. combination
    let bool_t = Typ::base("bool");
    let f = checked_cterm(Term::abs("x", bool_t.clone(), Term::bound(0)));
    let x = checked_cterm(Term::const_("a", bool_t.clone()));
    let rf = ThmKernel::reflexive(f.clone()).unwrap();
    let rx = ThmKernel::reflexive(x.clone()).unwrap();
    let _comb = ThmKernel::combination(&rf, &rx).unwrap();

    // 5. abstraction
    let _abs = ThmKernel::abstraction("x", bool_t.clone(), &refl).unwrap();

    // 6. beta_conversion
    let app = Term::app(Term::abs("x", bool_t.clone(), Term::bound(0)), Term::const_("c", bool_t));
    let ct = checked_cterm(app);
    let _beta = ThmKernel::beta_conversion(ct).unwrap();

    // 7-8. implies_intr/implies_elim
    let hyp = t.clone();
    let goal = ThmKernel::assume(hyp.clone()).unwrap();
    let imp = ThmKernel::implies_intr(&t, &goal).unwrap();
    let _mp = ThmKernel::implies_elim(&imp, &goal).unwrap();

    // 9-10. forall_intr/forall_elim
    let _all = ThmKernel::forall_intr("x", Typ::base("bool"), &goal).unwrap();
    // forall_elim requires matching types, may fail with dummy

    // 11. transitive
    let a = checked_cterm(Term::const_("a", Typ::base("nat")));
    let _ra = ThmKernel::reflexive(a).unwrap();
    // transitive may fail if types differ — ok

    // 12. instantiate
    let _inst =
        ThmKernel::instantiate_checked(&isabelle_rs::core::envir::Envir::init(), &goal).unwrap();

    // 13. trivial
    let _triv = ThmKernel::trivial(t).unwrap();

    eprintln!("All 15 kernel operations compiled and ran successfully");
}

#[test]
fn test_theory_processor_pipeline() {
    // Test the complete theory processing pipeline
    let source = r#"theory Test imports Pure begin

definition foo :: "nat" where "foo = 0"

lemma test: "True"
  by auto

end"#;

    let parent = Theory::pure();
    let mut proc = TheoryProcessor::with_parent(parent, "Test");
    let _theory = proc.process_source(source);

    let errors = proc.errors();
    if !errors.is_empty() {
        eprintln!("TheoryProcessor errors: {:?}", errors);
    }

    let thm_count = proc.theorem_count();
    eprintln!("Test theory: {} theorems, {} errors", thm_count, errors.len());

    assert!(errors.is_empty(), "TheoryProcessor should not report errors: {errors:?}");
}

#[test]
fn test_typedef_record_parsing() {
    use isabelle_rs::hol::typedef_record::*;

    // Test typedef parsing
    let src = r#"typedef point = "{x. True}""#;
    let defs = parse_typedefs(src);
    assert_eq!(defs.len(), 1);
    assert_eq!(defs[0].name, "point");

    let lemmas = typedef_to_lemmas(&defs[0]);
    assert!(lemmas.len() >= 7, "typedef should generate >=7 lemmas");

    // Test record parsing
    let src = "record point = x :: nat + y :: nat";
    let defs = parse_records(src);
    assert_eq!(defs.len(), 1);
    assert_eq!(defs[0].name, "point");
    assert_eq!(defs[0].fields.len(), 2);

    let lemmas = record_to_lemmas(&defs[0]);
    assert!(lemmas.len() >= 8, "record should generate >=8 lemmas");
}

#[test]
fn test_datatype_parsing() {
    // Test basic datatype
    let src = r#"datatype 'a list = Nil | Cons 'a "'a list""#;
    let defs = parse_datatypes(src);
    assert_eq!(defs.len(), 1);
    assert_eq!(defs[0].constructors.len(), 2);

    // Test mutual datatype
    let src = "datatype even = Zero | Even_Suc odd\n  and odd = Odd_Suc even";
    let defs = parse_datatypes(src);
    assert_eq!(defs.len(), 2, "Should parse 2 mutual datatypes");

    // Test codatatype
    let src = "codatatype 'a stream = SCons 'a \"'a stream\"";
    let defs = parse_datatypes(src);
    assert_eq!(defs.len(), 1);

    // Generate theorems
    let lemmas = generate_datatype_lemmas(&defs[0]);
    assert!(lemmas.len() >= 1, "datatype should generate at least 1 lemma");
}

#[test]
fn test_pretty_printer() {
    use isabelle_rs::{core::term::Term, syntax::printer::print_term};

    // Infix operators
    let a = Term::free("a", Typ::dummy());
    let b = Term::free("b", Typ::dummy());
    let eq = Term::app(Term::app(Term::const_("HOL.eq", Typ::dummy()), a), b);
    assert_eq!(print_term(&eq), "a = b");

    // Arithmetic
    let plus = Term::app(
        Term::app(Term::const_("HOL.plus", Typ::dummy()), Term::free("a", Typ::dummy())),
        Term::free("b", Typ::dummy()),
    );
    assert_eq!(print_term(&plus), "a + b");

    // Implication
    let imp = Term::app(
        Term::app(Term::const_("Pure.imp", Typ::dummy()), Term::free("A", Typ::dummy())),
        Term::free("B", Typ::dummy()),
    );
    let result = print_term(&imp);
    assert!(result.contains("==>") || result.contains("=>"), "Expected implication");
}

#[test]
fn test_tptp_export() {
    use isabelle_rs::{core::logic::Pure, tools::tptp::*};

    let p = CTerm::certify(isabelle_rs::core::term::Term::const_("P", Typ::base("prop")));
    let q = CTerm::certify(isabelle_rs::core::term::Term::const_("Q", Typ::base("prop")));
    let pq = isabelle_rs::core::term::Term::app(
        isabelle_rs::core::term::Term::app(
            isabelle_rs::core::term::Term::const_("HOL.conj", Typ::dummy()),
            p.term().clone(),
        ),
        q.term().clone(),
    );
    let goal_term = Pure::mk_implies(pq, p.term().clone());
    let goal = ThmKernel::assume_compat(CTerm::certify(goal_term));

    let tptp = goal_to_tptp_fof(&goal, "test");
    assert!(tptp.contains("fof(test"));
    assert!(tptp.contains("conjecture"));
}

#[test]
fn test_printer_tptp_roundtrip() {
    // Test that printed terms can be recognized by TPTP export
    use isabelle_rs::{
        core::{term::Term, types::Typ},
        syntax::printer::print_term,
        tools::tptp::goal_to_tptp_fof,
    };

    // Create: a = b
    let eq = Term::app(
        Term::app(Term::const_("HOL.eq", Typ::dummy()), Term::free("a", Typ::dummy())),
        Term::free("b", Typ::dummy()),
    );
    let printed = print_term(&eq);
    assert_eq!(printed, "a = b");

    let goal = ThmKernel::assume_compat(CTerm::certify(eq));
    let tptp = goal_to_tptp_fof(&goal, "roundtrip");
    assert!(tptp.contains("="));
    eprintln!("Roundtrip: {} → TPTP", printed);
}

// =========================================================================
// Batch Verification Tests (Phase 40)
// =========================================================================

#[test]
fn test_batch_verify_with_classifier() {
    // Skip if isabelle-source doesn't exist
    let hol_dir = std::path::Path::new("isabelle-source/src/HOL");
    if !hol_dir.exists() {
        eprintln!("Skipping: isabelle-source/src/HOL not found");
        return;
    }

    use isabelle_rs::theory::session_builder::SessionBuilder;

    let mut builder = SessionBuilder::new();
    builder.set_accept_all(true); // Fast mode: accept axioms, no proof replay

    eprintln!("Scanning theories...");
    let count = builder.scan(hol_dir).unwrap();
    eprintln!("Found {} theory files", count);

    let order = builder.resolve_dependencies();
    eprintln!("Topological order: {} theories", order.len());

    eprintln!("Building with classification...");
    let report = builder.build_with_classifier();

    report.print();
    report.print_failures(20);

    // Export CSV for further analysis
    let csv = report.to_csv();
    let csv_path = std::path::Path::new("target/verify_report.csv");
    std::fs::create_dir_all("target").ok();
    std::fs::write(csv_path, &csv).ok();
    eprintln!("Report saved to {}", csv_path.display());

    // Basic assertions
    assert!(report.total > 0, "No theories processed");
    eprintln!(
        "Summary: {} files, {:.1}% overall rate, {} theorems",
        report.total,
        report.overall_rate * 100.0,
        report.total_theorems,
    );
}

#[test]
fn test_batch_verify_core_files() {
    // Verify just the core HOL theories (the ones used in benchmarks)
    let core_files =
        vec!["HOL", "Orderings", "Set", "Nat", "List", "Fun", "Product_Type", "Sum_Type", "Option"];

    let hol_dir = std::path::Path::new("isabelle-source/src/HOL");
    if !hol_dir.exists() {
        eprintln!("Skipping: isabelle-source/src/HOL not found");
        return;
    }

    use isabelle_rs::theory::session_builder::SessionBuilder;

    let mut builder = SessionBuilder::new();
    let _count = builder.scan(hol_dir).unwrap();
    let _order = builder.resolve_dependencies();

    let report = builder.build_with_classifier();

    // Check core files specifically
    for name in &core_files {
        if let Some(r) = report.results.iter().find(|r| r.name == *name) {
            let label = r.status.label();
            let rate = r.status.rate();
            eprintln!(
                "  {}: [{}] {:.0}% — {} theorems",
                name,
                label,
                rate * 100.0,
                r.theorem_count
            );
            // At minimum, core files should not have syntax errors
            assert!(
                !matches!(
                    r.status,
                    isabelle_rs::theory::verify_classifier::VerifyStatus::SyntaxError { .. }
                ),
                "Core file {} has syntax error: {:?}",
                name,
                r.status
            );
        } else {
            eprintln!("  {}: NOT FOUND in results", name);
        }
    }
}
