//! Loading an ASPIC+ theory from JSON using the "simple" format.
//!
//! The simple format represents formulae as plain strings (e.g. `"p"`,
//! `"-q"`) and is designed for hand-authored theory files and external
//! tool interop.
//!
//! Run with: `cargo run --example json_input --features json`

use pickaxe_rs::io::simple::{build_system, SimpleTheory};
use pickaxe_rs::prelude::*;

fn main() {
    // ── 1. Define a theory in JSON ──────────────────────────────────────

    let json = r#"{
        "premises": [
            { "formula": "bird", "kind": "ordinary" },
            { "formula": "penguin", "kind": "ordinary" }
        ],
        "strict_rules": [
            { "id": "s1", "antecedents": ["penguin"], "consequent": "bird" },
            { "id": "s2", "antecedents": ["penguin"], "consequent": "-flies" }
        ],
        "defeasible_rules": [
            { "id": "d1", "antecedents": ["bird"], "consequent": "flies" }
        ],
        "contrariness": [
            { "target": "flies", "attacker": "-flies", "relation": "contradictory" }
        ],
        "rule_preferences": [
            { "superior": "s2", "inferior": "d1" }
        ],
        "classical_negation": false
    }"#;

    // ── 2. Parse and build the system ───────────────────────────────────

    let theory: SimpleTheory = serde_json::from_str(json).expect("invalid JSON");
    let (system, warnings) = build_system(&theory).expect("build failed");

    println!(
        "Loaded system: {} premise(s), {} strict rule(s), {} defeasible rule(s)",
        system.knowledge_base.premises.len(),
        system.strict_rules.len(),
        system.defeasible_rules.len(),
    );
    for w in &warnings {
        println!("  warning: {w:?}");
    }

    // ── 3. Build an ordering from the rule_preferences ──────────────────

    let tiers: Vec<Vec<RuleId>> = theory
        .rule_preferences
        .iter()
        .map(|p| vec![RuleId(p.superior.clone()), RuleId(p.inferior.clone())])
        .collect();

    let ordering: Box<dyn ArgumentOrdering> = Box::new(LastLinkOrdering {
        rule_ordering: Box::new(TieredOrdering::new(tiers)),
        premise_ordering: Box::new(NoPreference),
        lifting: LiftingStrategy::Elitist,
    });

    // ── 4. Evaluate ─────────────────────────────────────────────────────

    let pipeline = AspicPipeline::classical(system, ordering);
    let result = pipeline
        .evaluate(Semantics::Grounded)
        .expect("evaluation failed");

    println!(
        "\nGrounded extension ({} argument(s)):",
        result.extensions[0].len(),
    );
    for &arg_id in &result.extensions[0] {
        let arg = result.store.get(arg_id).unwrap();
        println!("  A{}: {}", arg_id.0, arg.conclusion());
    }

    // ── 5. Round-trip via the native format ─────────────────────────────

    let native = SerializableSystem::from_system(
        &AspicSystemBuilder::new()
            .ordinary_premise(formula!(bird))
            .with_classical_negation()
            .build()
            .0,
    );
    let json_out = native.to_json().expect("serialisation failed");
    println!("\nNative JSON round-trip:\n{json_out}");
}
