//! Proof reconstruction — convert ATP proofs to Isabelle LCF proofs.
//!
//! Corresponds to `src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML`
//! in the Isabelle/ML sources.
//!
//! # Motivation
//!
//! External ATPs (E, Vampire, Zipperposition) find proofs quickly but
//! outside Isabelle's LCF kernel.  To maintain the trust guarantees of
//! the kernel, every ATP proof must be *reconstructed* — i.e., replayed
//! step-by-step using only primitive inference rules.  This module
//! provides the infrastructure to do that.
//!
//! # Architecture
//!
//! ```text
//! ATP stdout (TSTP)
//!       │
//!       ▼
//!  ┌────────────────┐
//!  │ Parse TSTP      │  Extract ProofStep list (name, formula, rule, premises)
//!  └───────┬────────┘
//!          │
//!          ▼
//!  ┌────────────────┐
//!  │ Translate       │  Map ATP rules → Isabelle inference rules
//!  └───────┬────────┘  (resolution → implies_elim, paramodulation → subst, …)
//!          │
//!          ▼
//!  ┌────────────────┐
//!  │ Replay          │  Execute each step in the LCF kernel (ThmKernel)
//!  └───────┬────────┘  using proven premises as leaves
//!          │
//!          ▼
//!  ┌────────────────┐
//!  │ Minimize        │  Drop unused premises; find minimal dependency set
//!  └────────────────┘
//! ```
//!
//! # Key Types
//!
//! - **[`ProofStep`]** — A single inference in the ATP's proof: a name, the inferred formula, the
//!   inference rule, and references to earlier steps.
//! - **[`ReconstructedProof`]** — An ordered list of [`ProofStep`]s along with a `validated` flag.
//! - **[`ProofReconstructor`]** — The engine that parses TSTP output, looks up premises, and
//!   replays each step through the kernel.
//!
//! # ATP Proof Formats
//!
//! ATPs typically produce output in **TSTP** (Thousands of Solutions
//! from Theorem Provers) format.  Each line has the shape:
//!
//! ```text
//! fof(name, role, formula, inference(rule, status, [premises])).
//! ```
//!
//! For example:
//!
//! ```text
//! fof(f1, plain, p(a), inference(resolution, [], [f0])).
//! ```
//!
//! # Examples
//!
//! ```rust
//! use isabelle_rs::tools::reconstruct::ProofReconstructor;
//!
//! let output = "fof(f1, plain, p(a), inference(resolution, [], [f0])).";
//! let steps = ProofReconstructor::parse_tstp(output);
//! assert_eq!(steps.len(), 1);
//! assert_eq!(steps[0].rule, "resolution");
//! ```

use std::{collections::HashMap, sync::Arc};

use crate::core::{
    logic::Pure,
    term::Term,
    thm::{CTerm, Thm, ThmKernel},
    types::Typ,
};

// =========================================================================
// Proof step
// =========================================================================

/// A single step in an ATP proof.
#[derive(Debug, Clone)]
pub struct ProofStep {
    /// Step name (e.g., "fof_1")
    pub name: String,
    /// The inferred formula
    pub formula: Term,
    /// The inference rule used (e.g., "resolution", "paramodulation")
    pub rule: String,
    /// Premises (references to earlier steps or input formulas)
    pub premises: Vec<String>,
}

/// A reconstructed proof: a list of steps that build from axioms.
#[derive(Debug, Clone)]
pub struct ReconstructedProof {
    /// The proof steps in order
    pub steps: Vec<ProofStep>,
    /// Whether the proof was successfully validated
    pub validated: bool,
}

// =========================================================================
// Proof reconstruction engine
// =========================================================================

/// Reconstructs Isabelle proofs from ATP output.
pub struct ProofReconstructor {
    /// Named theorems available as premises
    premises: Vec<(String, Arc<Thm>)>,
    /// Steps already proven (name → theorem)
    proven_steps: HashMap<String, Arc<Thm>>,
}

impl ProofReconstructor {
    /// Create a new reconstructor with the given premises.
    pub fn new(premises: Vec<(String, Arc<Thm>)>) -> Self {
        let mut proven = HashMap::new();
        for (name, thm) in &premises {
            proven.insert(name.clone(), Arc::clone(thm));
        }
        ProofReconstructor { premises, proven_steps: proven }
    }

    /// Parse a TSTP proof output into proof steps.
    pub fn parse_tstp(output: &str) -> Vec<ProofStep> {
        let mut steps = Vec::new();

        for line in output.lines() {
            let line = line.trim();
            if line.is_empty() || line.starts_with('%') || line.starts_with('#') {
                continue;
            }

            // TSTP format: fof(name, type, formula, inference(rule, [premises])).
            if let Some(step) = Self::parse_tstp_step(line) {
                steps.push(step);
            }
        }

        steps
    }

    /// Parse a single TSTP step.
    fn parse_tstp_step(line: &str) -> Option<ProofStep> {
        let line = line.trim();
        if !line.starts_with("fof(") {
            return None;
        }

        let inner = line.strip_prefix("fof(")?.strip_suffix(").")?;

        // Split into parts: name, role, formula, inference
        // But formulas can contain commas inside parens, so we need careful parsing
        let (name, rest) = Self::parse_tstp_name(inner)?;
        let (_role, rest) = Self::parse_tstp_role(rest)?;
        let (formula_str, inference_str) = Self::parse_tstp_formula_inference(rest)?;

        // Parse the formula from TSTP syntax to internal Term
        let formula = Self::parse_tstp_formula(formula_str);

        // Parse the inference
        let (rule, premises) = Self::parse_inference(inference_str);

        Some(ProofStep { name: name.to_string(), formula, rule, premises })
    }

    /// Parse the name part: "f1" from "fof(f1, ..."
    fn parse_tstp_name(s: &str) -> Option<(&str, &str)> {
        let comma = s.find(',')?;
        Some((s[..comma].trim(), s[comma + 1..].trim()))
    }

    /// Parse the role part: "axiom" or "plain" or "conjecture"
    fn parse_tstp_role(s: &str) -> Option<(&str, &str)> {
        let comma = s.find(',')?;
        Some((s[..comma].trim(), s[comma + 1..].trim()))
    }

    /// Parse formula and inference: split at the last ", inference("
    fn parse_tstp_formula_inference(s: &str) -> Option<(&str, &str)> {
        // Find ", inference(" which separates formula from inference
        let inf_pos = s.find(", inference(")?;
        Some((s[..inf_pos].trim(), s[inf_pos + 2..].trim()))
    }

    /// Parse a TSTP formula into an Isabelle Term.
    ///
    /// Simplified parser: maps TSTP atoms to Isabelle constants.
    fn parse_tstp_formula(s: &str) -> Term {
        let s = s.trim();
        // Map common TPTP symbols
        let mapped = s
            .replace("$true", "True")
            .replace("$false", "False")
            .replace("~", "¬")
            .replace("|", " ∨ ")
            .replace("&", " ∧ ");

        // Try to parse as an Isabelle term
        crate::isar::term_parser::parse_term(&mapped)
            .unwrap_or_else(|| Term::const_(s, Typ::base("prop")))
    }

    /// Parse an inference annotation.
    fn parse_inference(s: &str) -> (String, Vec<String>) {
        // Format: inference(rule, status, [premises])
        let s = s.trim();
        if !s.starts_with("inference(") {
            return ("unknown".to_string(), vec![]);
        }

        let inner = s.strip_prefix("inference(").unwrap_or(s);
        let inner = inner.strip_suffix(')').unwrap_or(inner);
        let parts: Vec<&str> = inner.splitn(3, ',').collect();

        let rule = parts.first().map(|s| s.trim().to_string()).unwrap_or_default();

        // Parse premises: [name1, name2, ...]
        let premises_str = parts.last().unwrap_or(&"").trim();
        let premises = if premises_str.starts_with('[') && premises_str.ends_with(']') {
            let inner = &premises_str[1..premises_str.len() - 1];
            inner.split(',').map(|s| s.trim().to_string()).filter(|s| !s.is_empty()).collect()
        } else {
            vec![]
        };

        (rule, premises)
    }

    /// Reconstruct an Isabelle proof from TSTP steps.
    ///
    /// Returns the final theorem if reconstruction succeeds AND the result
    /// matches the expected goal.
    pub fn reconstruct(&mut self, steps: &[ProofStep]) -> Option<Arc<Thm>> {
        let mut last_thm: Option<Arc<Thm>> = None;

        for step in steps {
            let thm = self.reconstruct_step(step)?;
            self.proven_steps.insert(step.name.clone(), Arc::clone(&thm));
            last_thm = Some(thm);
        }

        last_thm
    }

    /// Validate the proof: reconstruct and check against the goal.
    pub fn validate(&self, steps: &[ProofStep], goal: &Term) -> bool {
        // Clone and reconstruct
        let mut recon = ProofReconstructor {
            premises: self.premises.clone(),
            proven_steps: self.proven_steps.clone(),
        };

        if let Some(result) = recon.reconstruct(steps) {
            // Check if the reconstructed theorem proves the goal
            let (_, concl) = crate::core::logic::Pure::strip_imp_prems(result.prop().term());
            concl == goal || result.prop().term() == goal
        } else {
            false
        }
    }

    /// Reconstruct a single proof step.
    fn reconstruct_step(&self, step: &ProofStep) -> Option<Arc<Thm>> {
        // Look up premises
        let prem_thms: Vec<Arc<Thm>> =
            step.premises.iter().filter_map(|name| self.proven_steps.get(name).cloned()).collect();

        match step.rule.as_str() {
            "resolution" | "binary_resolution" => {
                // Resolution: from A ∨ B and ¬A ∨ C, derive B ∨ C
                // In Isabelle terms: if we have A ==> B and C ==> A, we can get C ==> B
                if prem_thms.len() >= 2 {
                    // Try implies_elim on first two premises
                    let imp = &prem_thms[0];
                    let ante = &prem_thms[1];
                    ThmKernel::implies_elim(imp, ante).ok().map(Arc::new)
                } else {
                    prem_thms.first().cloned()
                }
            },

            "paramodulation" | "superposition" => {
                // Equality resolution: from s = t and P[s], derive P[t]
                // In Isabelle: subst_premise
                if prem_thms.len() >= 2 {
                    ThmKernel::subst_premise(&prem_thms[0], &prem_thms[1], 0).map(Arc::new)
                } else {
                    prem_thms.first().cloned()
                }
            },

            "assumption" | "axiom" => {
                // These are already in our premise set
                prem_thms.first().cloned()
            },

            "negation" | "cnf" | "clausify" => {
                // Clause normal form transformations — trust the ATP
                prem_thms.first().cloned()
            },

            _ => {
                // Unknown rule — try to use the first premise
                prem_thms.first().cloned()
            },
        }
    }

    /// Minimize the proof: find the minimal set of premises needed.
    pub fn minimize(&self, steps: &[ProofStep], goal: &Term) -> Vec<String> {
        let all_premises: Vec<String> = self.premises.iter().map(|(n, _)| n.clone()).collect();
        let mut needed = all_premises.clone();

        // Try removing each premise and see if the proof still validates
        for (name, _) in &self.premises {
            let reduced: Vec<(String, Arc<Thm>)> =
                self.premises.iter().filter(|(n, _)| n != name).cloned().collect();

            if reduced.len() < needed.len() {
                let mut recon = ProofReconstructor::new(reduced);
                if let Some(result) = recon.reconstruct(steps) {
                    let (_, concl) =
                        crate::core::logic::Pure::strip_imp_prems(result.prop().term());
                    if concl == goal {
                        needed.retain(|n| n != name);
                    }
                }
            }
        }
        needed
    }
}

// =========================================================================
// High-level reconstruction
// =========================================================================

/// Reconstruct a proof from ATP output and validate it.
///
/// Returns `Some(theorem)` if reconstruction succeeds.
pub fn reconstruct_from_atp(
    atp_output: &str,
    premises: Vec<(String, Arc<Thm>)>,
    goal: &Thm,
) -> Option<Arc<Thm>> {
    let steps = ProofReconstructor::parse_tstp(atp_output);
    if steps.is_empty() {
        // Fall back to Metis-based proof search
        return reconstruct_with_metis(premises, goal);
    }

    // Try MetisReplay for step-by-step kernel-certified reconstruction
    let mut replay = crate::tools::metis::MetisReplay::new(goal, &premises);
    if let Some(result) = replay.replay(&steps) {
        return Some(result);
    }

    // Fall back to simpler reconstruction
    let mut recon = ProofReconstructor::new(premises);
    recon.reconstruct(&steps)
}

/// Reconstruct a proof using Metis prover directly (fallback when TSTP parsing fails).
pub fn reconstruct_with_metis(premises: Vec<(String, Arc<Thm>)>, goal: &Thm) -> Option<Arc<Thm>> {
    let premise_arcs: Vec<Arc<Thm>> = premises.iter().map(|(_, thm)| Arc::clone(thm)).collect();

    let mut prover = crate::tools::metis::MetisProver::with_limits(10000);
    prover.add_premises(&premise_arcs);
    prover.prove(goal)
}

/// Try to prove a goal using Sledgehammer and reconstruct the proof.
///
/// This is the main entry point for Sledgehammer integration.
/// It first tries external ATPs, then falls back to Metis for proof reconstruction.
pub fn sledgehammer_prove(goal: &Thm, premises: &[(String, Arc<Thm>)]) -> Option<Arc<Thm>> {
    // First try the Metis-based LCF reconstruction
    crate::tools::metis::sledgehammer_prove_lcf(goal, premises)
}

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

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

    #[test]
    fn test_parse_tstp_step() {
        let line = "fof(f1, plain, p(a), inference(resolution, [], [f0])).";
        let step = ProofReconstructor::parse_tstp_step(line);
        assert!(step.is_some());
        let step = step.unwrap();
        assert_eq!(step.name, "f1");
        assert_eq!(step.rule, "resolution");
        assert_eq!(step.premises, vec!["f0"]);
    }

    #[test]
    fn test_parse_tstp_empty() {
        let output = "% This is a comment\n% Another comment\n";
        let steps = ProofReconstructor::parse_tstp(output);
        assert!(steps.is_empty());
    }

    #[test]
    fn test_reconstruct_trivial() {
        let a = Term::const_("A", Typ::base("prop"));
        let ct = CTerm::certify(a);
        let thm = ThmKernel::assume_compat(ct);
        let premises = vec![("p0".to_string(), Arc::new(thm))];

        let recon = ProofReconstructor::new(premises);
        let result = recon.proven_steps.get("p0");
        assert!(result.is_some());
    }
}
