//! "Native" structured format for ASPIC+ theories.
//!
//! Unlike the [simple format](super::simple) where formulae are plain
//! strings, the native format uses fully-structured [`Formula`] values
//! that mirror the library's internal representation.  This makes it
//! lossless for round-tripping and suitable for programmatic generation.
//!
//! The central types are:
//!
//! - [`SerializableSystem`] — the system itself (premises, rules,
//!   contrariness, classical negation flag).
//! - [`NativeTheory`] — a [`SerializableSystem`] together with optional
//!   [`RulePreference`] entries, forming
//!   the complete input schema that the CLI accepts under `--format native`.

use std::collections::HashSet;

use serde::{Deserialize, Serialize};

use crate::error::{AspicError, SerialError};
use crate::io::simple::RulePreference;
use crate::language::formula::Formula;
use crate::system::contrariness::{ContrarinessFunction, ContrarinessRelation};
use crate::system::knowledge::{KnowledgeBase, Premise, PremiseKind};
use crate::system::rules::{DefeasibleRule, RuleId, StrictRule};
use crate::system::AspicSystem;

// ---------------------------------------------------------------------------
// Serialisable component types
// ---------------------------------------------------------------------------

/// A serialisable representation of a contrariness entry.
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct SerializableContrarinessEntry {
    pub target: Formula,
    pub attacker: Formula,
    pub relation: String,
}

/// A serialisable representation of a premise.
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct SerializablePremise {
    pub formula: Formula,
    pub kind: String,
}

/// A serialisable representation of a strict rule.
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct SerializableStrictRule {
    pub id: String,
    pub antecedents: Vec<Formula>,
    pub consequent: Formula,
}

/// A serialisable representation of a defeasible rule.
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct SerializableDefeasibleRule {
    pub id: String,
    pub antecedents: Vec<Formula>,
    pub consequent: Formula,
    pub name: Option<Formula>,
}

// ---------------------------------------------------------------------------
// SerializableSystem
// ---------------------------------------------------------------------------

/// A fully serialisable ASPIC+ system.
///
/// Use [`from_system`](Self::from_system) to snapshot an [`AspicSystem`]
/// and [`to_system`](Self::to_system) to reconstruct one.
///
/// # Example
///
/// (Requires the `json` feature.)
///
#[cfg_attr(feature = "json", doc = "```")]
#[cfg_attr(not(feature = "json"), doc = "```ignore")]
/// use pickaxe_rs::prelude::*;
///
/// let (system, _) = AspicSystemBuilder::new()
///     .ordinary_premise(formula!(p))
///     .defeasible_rule("d1", vec![formula!(p)], formula!(q))
///     .with_classical_negation()
///     .build();
///
/// // Round-trip via JSON.
/// let serialisable = SerializableSystem::from_system(&system);
/// let json = serialisable.to_json().unwrap();
/// let restored = SerializableSystem::from_json(&json).unwrap();
/// let system2 = restored.to_system().unwrap();
///
/// assert_eq!(system.strict_rules.len(), system2.strict_rules.len());
/// ```
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct SerializableSystem {
    pub premises: Vec<SerializablePremise>,
    pub strict_rules: Vec<SerializableStrictRule>,
    pub defeasible_rules: Vec<SerializableDefeasibleRule>,
    pub contrariness: Vec<SerializableContrarinessEntry>,
    pub classical_negation: bool,
}

impl SerializableSystem {
    /// Convert from an [`AspicSystem`].
    pub fn from_system(system: &AspicSystem) -> Self {
        let premises = system
            .knowledge_base
            .premises
            .iter()
            .map(|p| SerializablePremise {
                formula: p.formula.clone(),
                kind: match p.kind {
                    PremiseKind::Axiom => "axiom".to_string(),
                    PremiseKind::Ordinary => "ordinary".to_string(),
                },
            })
            .collect();

        let strict_rules = system
            .strict_rules
            .iter()
            .map(|r| SerializableStrictRule {
                id: r.id.0.clone(),
                antecedents: r.antecedents.clone(),
                consequent: r.consequent.clone(),
            })
            .collect();

        let defeasible_rules = system
            .defeasible_rules
            .iter()
            .map(|r| SerializableDefeasibleRule {
                id: r.id.0.clone(),
                antecedents: r.antecedents.clone(),
                consequent: r.consequent.clone(),
                name: r.name.clone(),
            })
            .collect();

        let mut contrariness = Vec::new();
        let mut seen_contradictory: HashSet<(Formula, Formula)> = HashSet::new();
        for (target, attackers) in system.contrariness.entries() {
            for (attacker, relation) in attackers {
                match relation {
                    ContrarinessRelation::Contrary => {
                        contrariness.push(SerializableContrarinessEntry {
                            target: target.clone(),
                            attacker: attacker.clone(),
                            relation: "contrary".to_string(),
                        });
                    }
                    ContrarinessRelation::Contradictory => {
                        let canonical = if target <= attacker {
                            (target.clone(), attacker.clone())
                        } else {
                            (attacker.clone(), target.clone())
                        };
                        if seen_contradictory.insert(canonical) {
                            contrariness.push(SerializableContrarinessEntry {
                                target: target.clone(),
                                attacker: attacker.clone(),
                                relation: "contradictory".to_string(),
                            });
                        }
                    }
                }
            }
        }

        SerializableSystem {
            premises,
            strict_rules,
            defeasible_rules,
            contrariness,
            classical_negation: system.contrariness.has_classical_negation(),
        }
    }

    /// Convert back to an [`AspicSystem`].
    ///
    /// # Errors
    ///
    /// Returns [`AspicError`] if a premise `kind` or contrariness `relation`
    /// string is not one of the supported values.
    pub fn to_system(&self) -> Result<AspicSystem, AspicError> {
        let mut premises = Vec::new();
        for p in &self.premises {
            let kind = match p.kind.as_str() {
                "axiom" => PremiseKind::Axiom,
                "ordinary" => PremiseKind::Ordinary,
                other => return Err(SerialError::UnknownPremiseKind(other.to_string()).into()),
            };
            premises.push(Premise {
                formula: p.formula.clone(),
                kind,
            });
        }

        let strict_rules: Vec<StrictRule> = self
            .strict_rules
            .iter()
            .map(|r| StrictRule {
                id: RuleId(r.id.clone()),
                antecedents: r.antecedents.clone(),
                consequent: r.consequent.clone(),
            })
            .collect();

        let defeasible_rules: Vec<DefeasibleRule> = self
            .defeasible_rules
            .iter()
            .map(|r| DefeasibleRule {
                id: RuleId(r.id.clone()),
                antecedents: r.antecedents.clone(),
                consequent: r.consequent.clone(),
                name: r.name.clone(),
            })
            .collect();

        let mut contrariness = ContrarinessFunction::new();
        for entry in &self.contrariness {
            match entry.relation.as_str() {
                "contrary" => {
                    contrariness.add_contrary(entry.target.clone(), entry.attacker.clone());
                }
                "contradictory" => {
                    contrariness.add_contradictory(entry.target.clone(), entry.attacker.clone());
                }
                other => {
                    return Err(SerialError::UnknownContrarinessRelation(other.to_string()).into())
                }
            }
        }
        if self.classical_negation {
            contrariness = contrariness.with_classical_negation();
        }

        Ok(AspicSystem {
            knowledge_base: KnowledgeBase { premises },
            strict_rules,
            defeasible_rules,
            contrariness,
        })
    }

    /// Serialize to JSON string.  Requires the `json` feature.
    ///
    /// # Errors
    ///
    /// Returns [`serde_json::Error`] if serialization fails.
    #[cfg(feature = "json")]
    pub fn to_json(&self) -> Result<String, serde_json::Error> {
        serde_json::to_string_pretty(self)
    }

    /// Deserialize from JSON string.  Requires the `json` feature.
    ///
    /// # Errors
    ///
    /// Returns [`serde_json::Error`] if `json` is not valid
    /// JSON or does not match this type's schema.
    #[cfg(feature = "json")]
    pub fn from_json(json: &str) -> Result<Self, serde_json::Error> {
        serde_json::from_str(json)
    }

    /// Serialize to TOML string.  Requires the `toml-ser` feature.
    ///
    /// # Errors
    ///
    /// Returns [`toml::ser::Error`] if serialization fails.
    #[cfg(feature = "toml-ser")]
    pub fn to_toml(&self) -> Result<String, toml::ser::Error> {
        toml::to_string_pretty(self)
    }

    /// Deserialize from TOML string.  Requires the `toml-ser` feature.
    ///
    /// # Errors
    ///
    /// Returns [`toml::de::Error`] if `toml_str` is not valid
    /// TOML or does not match this type's schema.
    #[cfg(feature = "toml-ser")]
    pub fn from_toml(toml_str: &str) -> Result<Self, toml::de::Error> {
        toml::from_str(toml_str)
    }
}

// ---------------------------------------------------------------------------
// NativeTheory — the full input schema for the native format
// ---------------------------------------------------------------------------

/// A complete native-format theory: a [`SerializableSystem`] plus optional
/// [`RulePreference`] entries.
///
/// This is the top-level schema that the CLI deserialises when invoked
/// with `--format native`.
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct NativeTheory {
    #[serde(flatten)]
    pub system: SerializableSystem,
    #[serde(default)]
    pub rule_preferences: Vec<RulePreference>,
}
