//! Core syntactic types for the ASPIC+ logical language.
//!
//! The type hierarchy follows classical first-order logic restricted to the
//! Bernays–Schönfinkel fragment (function-free, ∃*∀* prefix):
//!
//! ```text
//! Term  ::=  Variable | Constant
//! Atom  ::=  predicate(Term, …)
//! Literal  ::=  Atom | ¬Atom          (classical negation)
//! Formula  ::=  Literal | Formula ∧ … | Formula ∨ … | Formula ⇒ Formula | ~Formula
//! ```
//!
//! Once grounded (all variables replaced by constants), every formula is
//! effectively propositional.

use serde::{Deserialize, Serialize};
use std::fmt;

/// A first-order term: either a variable to be grounded, or a concrete
/// constant.
///
/// By convention the [`formula!`](crate::formula) macro treats identifiers
/// starting with an uppercase letter as variables and lowercase as constants.
#[derive(Clone, Debug, Eq, Hash, PartialEq, Ord, PartialOrd, Serialize, Deserialize)]
pub enum Term {
    /// A variable, eliminated during grounding.
    Var(String),
    /// A ground constant.
    Const(String),
}

impl fmt::Display for Term {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Term::Var(v) => write!(f, "{v}"),
            Term::Const(c) => write!(f, "{c}"),
        }
    }
}

impl Term {
    /// Returns `true` if this term is a variable (to be eliminated during grounding).
    pub fn is_var(&self) -> bool {
        matches!(self, Term::Var(_))
    }

    /// Returns `true` if this term is a ground constant.
    pub fn is_const(&self) -> bool {
        matches!(self, Term::Const(_))
    }
}

/// An atomic proposition: a predicate symbol applied to zero or more terms.
///
/// A nullary atom (empty `terms`) acts as a propositional variable.
#[derive(Clone, Debug, Eq, Hash, PartialEq, Ord, PartialOrd, Serialize, Deserialize)]
pub struct Atom {
    /// The predicate name, e.g. `"flies"` in `flies(tweety)`.
    pub predicate: String,
    /// The argument list. Empty for propositional atoms.
    pub terms: Vec<Term>,
}

impl fmt::Display for Atom {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        if self.terms.is_empty() {
            write!(f, "{}", self.predicate)
        } else {
            let terms: Vec<String> = self
                .terms
                .iter()
                .map(std::string::ToString::to_string)
                .collect();
            write!(f, "{}({})", self.predicate, terms.join(", "))
        }
    }
}

/// A literal: an atom or its classical (strong) negation.
///
/// Classical negation is written with a leading `-` in display form (e.g.
/// `-flies(tweety)`). This is distinct from the logical `~` (formula-level
/// negation) represented by [`Formula::Not`].
#[derive(Clone, Debug, Eq, Hash, PartialEq, Ord, PartialOrd, Serialize, Deserialize)]
pub enum Literal {
    /// An unnegated atom.
    Pos(Atom),
    /// A classically negated atom.
    Neg(Atom),
}

impl Literal {
    /// The underlying atom, regardless of polarity.
    pub fn atom(&self) -> &Atom {
        match self {
            Literal::Pos(a) | Literal::Neg(a) => a,
        }
    }

    /// Returns `true` if this literal is positive (unnegated).
    pub fn is_positive(&self) -> bool {
        matches!(self, Literal::Pos(_))
    }

    /// Returns `true` if this literal is classically negated.
    pub fn is_negative(&self) -> bool {
        matches!(self, Literal::Neg(_))
    }

    /// Return the classical negation of this literal (flips `Pos` ↔ `Neg`).
    pub fn negate(&self) -> Literal {
        match self {
            Literal::Pos(a) => Literal::Neg(a.clone()),
            Literal::Neg(a) => Literal::Pos(a.clone()),
        }
    }
}

impl fmt::Display for Literal {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Literal::Pos(a) => write!(f, "{a}"),
            Literal::Neg(a) => write!(f, "-{a}"),
        }
    }
}

/// A formula in the ASPIC+ language.
///
/// Formulae are the currency of ASPIC+ knowledge bases and rules: premises
/// are formulae, rule antecedents and consequents are formulae, and
/// contrariness is defined over formulae.
///
/// # Variants
///
/// | Variant   | Display      | Meaning                        |
/// |-----------|--------------|--------------------------------|
/// | `Lit`     | `p` / `-p`   | A (possibly negated) atom      |
/// | `And`     | `(a & b)`    | Conjunction                    |
/// | `Or`      | `(a \| b)`   | Disjunction                    |
/// | `Implies` | `(a => b)`   | Material implication           |
/// | `Not`     | `~a`         | Formula-level (weak) negation  |
#[derive(Clone, Debug, Eq, Hash, PartialEq, Ord, PartialOrd, Serialize, Deserialize)]
pub enum Formula {
    /// A literal (positive or classically negated atom).
    Lit(Literal),
    /// Conjunction of sub-formulae.
    And(Vec<Formula>),
    /// Disjunction of sub-formulae.
    Or(Vec<Formula>),
    /// Material implication: `antecedent => consequent`.
    Implies(Box<Formula>, Box<Formula>),
    /// Formula-level (weak) negation, distinct from classical negation on
    /// literals.
    Not(Box<Formula>),
}

impl Formula {
    /// Create a positive literal with the given predicate and terms.
    pub fn pos(predicate: impl Into<String>, terms: Vec<Term>) -> Self {
        Formula::Lit(Literal::Pos(Atom {
            predicate: predicate.into(),
            terms,
        }))
    }

    /// Create a classically negated literal with the given predicate and terms.
    pub fn neg(predicate: impl Into<String>, terms: Vec<Term>) -> Self {
        Formula::Lit(Literal::Neg(Atom {
            predicate: predicate.into(),
            terms,
        }))
    }

    /// Create a positive propositional atom (no terms).
    pub fn prop(name: impl Into<String>) -> Self {
        Formula::pos(name, vec![])
    }

    /// Create a classically negated propositional atom (no terms).
    pub fn neg_prop(name: impl Into<String>) -> Self {
        Formula::neg(name, vec![])
    }

    /// Collect all variables occurring in this formula.
    pub fn variables(&self) -> Vec<&String> {
        let mut seen = std::collections::HashSet::new();
        let mut vars = Vec::new();
        self.collect_variables_inner(&mut seen, &mut vars);
        vars
    }

    fn collect_variables_inner<'a>(
        &'a self,
        seen: &mut std::collections::HashSet<&'a String>,
        vars: &mut Vec<&'a String>,
    ) {
        match self {
            Formula::Lit(lit) => {
                for term in &lit.atom().terms {
                    if let Term::Var(v) = term {
                        if seen.insert(v) {
                            vars.push(v);
                        }
                    }
                }
            }
            Formula::And(fs) | Formula::Or(fs) => {
                for f in fs {
                    f.collect_variables_inner(seen, vars);
                }
            }
            Formula::Implies(a, b) => {
                a.collect_variables_inner(seen, vars);
                b.collect_variables_inner(seen, vars);
            }
            Formula::Not(f) => f.collect_variables_inner(seen, vars),
        }
    }

    /// Collect all constants occurring in this formula.
    pub fn constants(&self) -> Vec<&String> {
        let mut seen = std::collections::HashSet::new();
        let mut consts = Vec::new();
        self.collect_constants_inner(&mut seen, &mut consts);
        consts
    }

    fn collect_constants_inner<'a>(
        &'a self,
        seen: &mut std::collections::HashSet<&'a String>,
        consts: &mut Vec<&'a String>,
    ) {
        match self {
            Formula::Lit(lit) => {
                for term in &lit.atom().terms {
                    if let Term::Const(c) = term {
                        if seen.insert(c) {
                            consts.push(c);
                        }
                    }
                }
            }
            Formula::And(fs) | Formula::Or(fs) => {
                for f in fs {
                    f.collect_constants_inner(seen, consts);
                }
            }
            Formula::Implies(a, b) => {
                a.collect_constants_inner(seen, consts);
                b.collect_constants_inner(seen, consts);
            }
            Formula::Not(f) => f.collect_constants_inner(seen, consts),
        }
    }

    /// Whether this formula contains any variables.
    pub fn is_ground(&self) -> bool {
        self.variables().is_empty()
    }

    /// Substitute a variable with a term throughout this formula.
    pub fn substitute(&self, var: &str, replacement: &Term) -> Formula {
        match self {
            Formula::Lit(lit) => {
                let atom = lit.atom();
                let new_terms: Vec<Term> = atom
                    .terms
                    .iter()
                    .map(|t| match t {
                        Term::Var(v) if v == var => replacement.clone(),
                        other => other.clone(),
                    })
                    .collect();
                let new_atom = Atom {
                    predicate: atom.predicate.clone(),
                    terms: new_terms,
                };
                match lit {
                    Literal::Pos(_) => Formula::Lit(Literal::Pos(new_atom)),
                    Literal::Neg(_) => Formula::Lit(Literal::Neg(new_atom)),
                }
            }
            Formula::And(fs) => {
                Formula::And(fs.iter().map(|f| f.substitute(var, replacement)).collect())
            }
            Formula::Or(fs) => {
                Formula::Or(fs.iter().map(|f| f.substitute(var, replacement)).collect())
            }
            Formula::Implies(a, b) => Formula::Implies(
                Box::new(a.substitute(var, replacement)),
                Box::new(b.substitute(var, replacement)),
            ),
            Formula::Not(f) => Formula::Not(Box::new(f.substitute(var, replacement))),
        }
    }

    /// Returns the classical negation of this formula.
    /// For a literal, this flips Pos/Neg. For compound formulae, wraps in Not.
    pub fn classical_negation(&self) -> Formula {
        match self {
            Formula::Lit(lit) => Formula::Lit(lit.negate()),
            other => Formula::Not(Box::new(other.clone())),
        }
    }
}

impl fmt::Display for Formula {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Formula::Lit(lit) => write!(f, "{lit}"),
            Formula::And(fs) => {
                let parts: Vec<String> = fs.iter().map(std::string::ToString::to_string).collect();
                write!(f, "({})", parts.join(" & "))
            }
            Formula::Or(fs) => {
                let parts: Vec<String> = fs.iter().map(std::string::ToString::to_string).collect();
                write!(f, "({})", parts.join(" | "))
            }
            Formula::Implies(a, b) => write!(f, "({a} => {b})"),
            Formula::Not(inner) => write!(f, "~{inner}"),
        }
    }
}
