//! "Simple" JSON format for ASPIC+ theories.
//!
//! Formulae are plain strings (`"p"`, `"-q"`) and the system is built via
//! [`AspicSystemBuilder`].  This is the human-friendly input format,
//! designed for hand-authored theory files and external tool interop.
//!
//! All types derive both [`Serialize`] and
//! [`Deserialize`], so they can be round-tripped
//! through JSON (or any serde-compatible format).
//!
//! See [`native`](super::native) for the fully-structured "native" format
//! that uses [`Formula`] values directly.

use serde::{Deserialize, Serialize};

use crate::error::SerialError;
use crate::language::formula::Formula;
use crate::system::builder::AspicSystemBuilder;
use crate::system::warning::Warning;
use crate::system::AspicSystem;

// ---------------------------------------------------------------------------
// Simple-format schema
// ---------------------------------------------------------------------------

/// A theory in the "simple" JSON format, where formulae are strings.
///
/// # Example (JSON)
///
/// ```json
/// {
///   "premises": [
///     { "formula": "bird", "kind": "ordinary" },
///     { "formula": "penguin", "kind": "axiom" }
///   ],
///   "strict_rules": [
///     { "id": "s1", "antecedents": ["penguin"], "consequent": "bird" }
///   ],
///   "defeasible_rules": [
///     { "id": "d1", "antecedents": ["bird"], "consequent": "flies" }
///   ],
///   "contrariness": [
///     { "target": "flies", "attacker": "-flies", "relation": "contradictory" }
///   ],
///   "rule_preferences": [
///     { "superior": "s1", "inferior": "d1" }
///   ],
///   "classical_negation": false
/// }
/// ```
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct SimpleTheory {
    pub premises: Vec<SimplePremise>,
    pub strict_rules: Vec<SimpleStrictRule>,
    pub defeasible_rules: Vec<SimpleDefeasibleRule>,
    pub contrariness: Vec<SimpleContrariness>,
    #[serde(default)]
    pub rule_preferences: Vec<RulePreference>,
    #[serde(default)]
    pub classical_negation: bool,
}

/// A premise in the simple format.
///
/// `kind` must be `"axiom"` or `"ordinary"`.
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct SimplePremise {
    pub formula: String,
    pub kind: String,
}

/// A strict rule in the simple format.
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct SimpleStrictRule {
    pub id: String,
    pub antecedents: Vec<String>,
    pub consequent: String,
}

/// A defeasible rule in the simple format.
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct SimpleDefeasibleRule {
    pub id: String,
    pub antecedents: Vec<String>,
    pub consequent: String,
    #[serde(default)]
    pub name: Option<String>,
}

/// A contrariness entry in the simple format.
///
/// `relation` must be `"contradictory"` or `"contrary"`.
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct SimpleContrariness {
    pub target: String,
    pub attacker: String,
    pub relation: String,
}

/// A pairwise rule preference: `superior` is strictly preferred over
/// `inferior`.
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct RulePreference {
    pub superior: String,
    pub inferior: String,
}

// ---------------------------------------------------------------------------
// Formula parsing
// ---------------------------------------------------------------------------

/// Parse a simple string formula: `"-p"` becomes a negated atom,
/// `"p"` becomes a positive atom.  No terms/arity.
pub fn parse_formula(s: &str) -> Formula {
    if let Some(stripped) = s.strip_prefix('-') {
        Formula::neg(stripped, vec![])
    } else {
        Formula::pos(s, vec![])
    }
}

// ---------------------------------------------------------------------------
// System construction
// ---------------------------------------------------------------------------

/// Build an [`AspicSystem`] from a [`SimpleTheory`].
///
/// Returns the system and any builder warnings.  Returns an error if an
/// unknown premise kind or contrariness relation is encountered.
///
/// # Errors
///
/// Returns [`SerialError`] if a premise `kind` or contrariness `relation`
/// string is not one of the supported values.
///
/// # Example
///
/// (Requires the `json` feature.)
///
#[cfg_attr(feature = "json", doc = "```")]
#[cfg_attr(not(feature = "json"), doc = "```ignore")]
/// use pickaxe_rs::prelude::*;
/// use pickaxe_rs::io::simple::{SimpleTheory, build_system};
///
/// let json = r#"{
///   "premises": [{ "formula": "bird", "kind": "ordinary" }],
///   "strict_rules": [],
///   "defeasible_rules": [
///     { "id": "d1", "antecedents": ["bird"], "consequent": "flies" }
///   ],
///   "contrariness": [],
///   "classical_negation": true
/// }"#;
///
/// let theory: SimpleTheory = serde_json::from_str(json).unwrap();
/// let (system, warnings) = build_system(&theory).unwrap();
/// assert!(warnings.is_empty());
/// ```
pub fn build_system(theory: &SimpleTheory) -> Result<(AspicSystem, Vec<Warning>), SerialError> {
    let mut builder = AspicSystemBuilder::new();

    if theory.classical_negation {
        builder = builder.with_classical_negation();
    }

    for p in &theory.premises {
        let f = parse_formula(&p.formula);
        match p.kind.as_str() {
            "axiom" => builder = builder.axiom(f),
            "ordinary" => builder = builder.ordinary_premise(f),
            other => return Err(SerialError::UnknownPremiseKind(other.to_string())),
        }
    }

    for r in &theory.strict_rules {
        let ants: Vec<Formula> = r.antecedents.iter().map(|a| parse_formula(a)).collect();
        let cons = parse_formula(&r.consequent);
        builder = builder.strict_rule(&r.id, ants, cons);
    }

    for r in &theory.defeasible_rules {
        let ants: Vec<Formula> = r.antecedents.iter().map(|a| parse_formula(a)).collect();
        let cons = parse_formula(&r.consequent);
        if let Some(name) = &r.name {
            builder = builder.named_defeasible_rule(&r.id, parse_formula(name), ants, cons);
        } else {
            builder = builder.defeasible_rule(&r.id, ants, cons);
        }
    }

    for c in &theory.contrariness {
        let target = parse_formula(&c.target);
        let attacker = parse_formula(&c.attacker);
        match c.relation.as_str() {
            "contradictory" => builder = builder.contradictory(target, attacker),
            "contrary" => builder = builder.contrary(target, attacker),
            other => return Err(SerialError::UnknownContrarinessRelation(other.to_string())),
        }
    }

    let (system, warnings) = builder.build();
    Ok((system, warnings))
}
