//! TPTP format output — convert Isabelle goals to TPTP for external ATPs.
//!
//! Supports:
//! - FOF (First-Order Form) — for E, Vampire, iProver
//! - TFF0 (Typed First-Order Form) — for typed provers
//!
//! This is the first step towards Sledgehammer integration.

use crate::{
    core::{logic::Pure, term::Term, thm::Thm},
    hol::hologic,
};

/// Export a goal to TPTP FOF format.
pub fn goal_to_tptp_fof(thm: &Thm, name: &str) -> String {
    let mut buf = String::new();

    // Header
    buf.push_str(&format!("% TPTP FOF for goal: {name}\n"));
    buf.push_str("% Generated by isabelle-rs\n\n");

    // Declare the conjecture
    buf.push_str("fof(");
    buf.push_str(name);
    buf.push_str(", conjecture,\n    ");

    let (_prems, concl) = Pure::strip_imp_prems(thm.prop().term());
    term_to_tptp(concl, &mut buf);

    buf.push_str(").\n");
    buf
}

/// Export a goal with premises to TPTP FOF format.
pub fn goal_with_prems_to_tptp(thm: &Thm, name: &str) -> String {
    let mut buf = String::new();

    buf.push_str(&format!("% TPTP FOF for goal: {name}\n"));
    buf.push_str("% Generated by isabelle-rs\n\n");

    let (prems, concl) = Pure::strip_imp_prems(thm.prop().term());

    // Declare premises as axioms
    for (i, prem) in prems.iter().enumerate() {
        buf.push_str("fof(");
        buf.push_str(&format!("premise_{i}"));
        buf.push_str(", axiom,\n    ");
        term_to_tptp(prem, &mut buf);
        buf.push_str(").\n\n");
    }

    // Declare the conjecture
    buf.push_str("fof(");
    buf.push_str(name);
    buf.push_str(", conjecture,\n    ");
    term_to_tptp(concl, &mut buf);
    buf.push_str(").\n");

    buf
}

/// Convert a term to TPTP FOF expression.
pub fn term_to_tptp(term: &Term, buf: &mut String) {
    match term {
        Term::Const { name, .. } => {
            let n = name.as_ref();
            // Map common Isabelle constants to TPTP symbols
            match n {
                "HOL.eq" | "Pure.eq" => buf.push('='),
                "HOL.True" => buf.push_str("$true"),
                "HOL.False" => buf.push_str("$false"),
                "HOL.Not" => buf.push('~'),
                "HOL.conj" | "HOL.and" => buf.push('&'),
                "HOL.disj" | "HOL.or" => buf.push('|'),
                "HOL.imp" | "Pure.imp" => buf.push_str("=>"),
                "HOL.All" | "Pure.all" => buf.push('!'),
                "HOL.Ex" => buf.push('?'),
                _ => {
                    // Sanitize name for TPTP
                    let clean = n.replace('.', "_").replace('\'', "");
                    buf.push_str(&clean);
                },
            }
        },
        Term::Free { name, .. } | Term::Var { name, .. } => {
            // TPTP variables start with uppercase
            let s = name.as_ref();
            let first = s.chars().next().map(|c| c.to_uppercase().to_string()).unwrap_or_default();
            let rest: String = s.chars().skip(1).collect();
            buf.push_str(&first);
            buf.push_str(&rest);
        },
        Term::Bound(i) => {
            buf.push_str(&format!("BOUND_{i}"));
        },
        Term::App { func, arg } => {
            match func.as_ref() {
                Term::Const { name, .. } => {
                    let n = name.as_ref();
                    match n {
                        // Infix operators
                        "HOL.eq" | "Pure.eq" => {
                            buf.push('(');
                            term_to_tptp(arg, buf);
                            buf.push_str(" = ");
                            // Need to get the second arg — but App only has one arg
                            buf.push_str("/* rhs */");
                            buf.push(')');
                        },
                        "HOL.Not" => {
                            buf.push('~');
                            buf.push('(');
                            term_to_tptp(arg, buf);
                            buf.push(')');
                        },
                        // Quantifiers: ! [X] : body
                        "HOL.All" | "Pure.all" => {
                            if let Term::Abs { name, body, .. } = arg.as_ref() {
                                buf.push('!');
                                buf.push_str(" [");
                                buf.push_str(name);
                                buf.push_str("] : ");
                                term_to_tptp(body, buf);
                            } else {
                                buf.push('!');
                                buf.push_str(" [X] : ");
                                term_to_tptp(arg, buf);
                            }
                        },
                        "HOL.Ex" => {
                            if let Term::Abs { name, body, .. } = arg.as_ref() {
                                buf.push('?');
                                buf.push_str(" [");
                                buf.push_str(name);
                                buf.push_str("] : ");
                                term_to_tptp(body, buf);
                            } else {
                                buf.push('?');
                                buf.push_str(" [X] : ");
                                term_to_tptp(arg, buf);
                            }
                        },
                        _ => {
                            // Binary application: check if it's an infix
                            if let Term::App { func: inner, arg: left } = func.as_ref()
                                && let Term::Const { name: op_name, .. } = inner.as_ref()
                            {
                                let op = match op_name.as_ref() {
                                    "HOL.conj" | "HOL.and" => " & ",
                                    "HOL.disj" | "HOL.or" => " | ",
                                    "HOL.imp" | "Pure.imp" => " => ",
                                    _ => "",
                                };
                                if !op.is_empty() {
                                    buf.push('(');
                                    term_to_tptp(left, buf);
                                    buf.push_str(op);
                                    term_to_tptp(arg, buf);
                                    buf.push(')');
                                    return;
                                }
                            }
                            // Plain function application
                            term_to_tptp(func, buf);
                            buf.push('(');
                            term_to_tptp(arg, buf);
                            buf.push(')');
                        },
                    }
                },
                _ => {
                    // Plain application
                    term_to_tptp(func, buf);
                    buf.push('(');
                    term_to_tptp(arg, buf);
                    buf.push(')');
                },
            }
        },
        Term::Abs { name, body, .. } => {
            buf.push('!');
            buf.push_str(" [");
            buf.push_str(name);
            buf.push_str("] : ");
            term_to_tptp(body, buf);
        },
    }
}

// =========================================================================
// Tests
// =========================================================================

#[cfg(test)]
mod tests {
    use super::*;
    use crate::core::{
        thm::{CTerm, ThmKernel},
        types::Typ,
    };

    #[test]
    fn test_goal_to_tptp_simple() {
        // P & Q => P
        let p = CTerm::certify(Term::const_("P", Typ::base("prop")));
        let q = CTerm::certify(Term::const_("Q", Typ::base("prop")));
        let pq = Term::app(Term::app(hologic::conj_const(), 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("conjecture"));
        assert!(tptp.contains("fof(test"));
    }

    #[test]
    fn test_tptp_quantifier() {
        // ! [X] : p(X)
        let px = Term::app(Term::const_("p", Typ::dummy()), Term::bound(0));
        let all = Term::abs("X", Typ::dummy(), px);
        let all_prop = Term::app(hologic::all_const(Typ::dummy()), all);
        let goal = ThmKernel::assume_compat(CTerm::certify(all_prop));

        let tptp = goal_to_tptp_fof(&goal, "quant");
        assert!(tptp.contains("! [X]"));
    }

    #[test]
    fn test_tptp_equality() {
        // a = b
        let eq = Term::app(
            Term::app(hologic::eq_const(Typ::dummy()), Term::const_("a", Typ::dummy())),
            Term::const_("b", Typ::dummy()),
        );
        let goal = ThmKernel::assume_compat(CTerm::certify(eq));
        let tptp = goal_to_tptp_fof(&goal, "eq_test");
        assert!(tptp.contains("="));
    }
}
