//! CLI runner for the pickaxe-rs library.
//!
//! Reads a theory JSON file, configures the ASPIC+ pipeline, evaluates under
//! the chosen semantics, and outputs structured JSON with extensions and
//! per-stage timing instrumentation.

use std::path::PathBuf;
use std::process::ExitCode;
use std::time::Instant;

use clap::{Parser, ValueEnum};
use pickaxe_rs::io::simple;
use pickaxe_rs::prelude::*;

// ---------------------------------------------------------------------------
// CLI argument definitions
// ---------------------------------------------------------------------------

/// Run the ASPIC+ pipeline on a theory JSON file.
#[derive(Parser)]
#[command(version, about = "Run the ASPIC+ structured argumentation pipeline")]
struct Cli {
    /// Path to the theory JSON file.
    #[arg(short, long)]
    input: PathBuf,

    /// Semantics to evaluate.
    #[arg(short, long)]
    semantics: SemanticsArg,

    /// Preference mode for classical evaluation.
    #[arg(short, long, default_value = "none")]
    preferences: PrefMode,

    /// Grounder implementation.
    #[arg(long, default_value = "naive")]
    grounder: GrounderArg,

    /// Attack computer implementation.
    #[arg(long, default_value = "pairwise")]
    attack_computer: AttackArg,

    /// Semantics solver implementation.
    #[arg(long, default_value = "naive-enumeration")]
    solver: SolverArg,

    /// Path to the ASPARTIX encodings directory (required with --solver aspartix).
    #[arg(long)]
    encodings_dir: Option<PathBuf>,

    /// Path to external solver binary (required with --solver mutoksia).
    #[arg(long)]
    solver_path: Option<PathBuf>,

    /// Named pipeline preset. Mutually exclusive with --grounder, --attack-computer, --solver.
    #[arg(long)]
    preset: Option<PresetArg>,

    /// Task mode: enumerate all extensions, find a single extension, or count.
    #[arg(long, default_value = "enumerate-all")]
    task: TaskArg,

    /// Input JSON format.
    #[arg(long, default_value = "simple")]
    format: FormatArg,

    /// Lifting strategy for accrual mode.
    #[arg(long, default_value = "elitist")]
    accrual_lifting: LiftingArg,
}

#[derive(Clone, Debug, ValueEnum)]
enum SemanticsArg {
    Grounded,
    Preferred,
    Stable,
    Complete,
    #[value(name = "semi-stable")]
    SemiStable,
    Ideal,
    Eager,
    Admissible,
}

impl SemanticsArg {
    fn to_semantics(&self) -> Semantics {
        match self {
            Self::Grounded => Semantics::Grounded,
            Self::Preferred => Semantics::Preferred,
            Self::Stable => Semantics::Stable,
            Self::Complete => Semantics::Complete,
            Self::SemiStable => Semantics::SemiStable,
            Self::Ideal => Semantics::Ideal,
            Self::Eager => Semantics::Eager,
            Self::Admissible => Semantics::Admissible,
        }
    }
}

#[derive(Clone, Debug, ValueEnum)]
enum TaskArg {
    #[value(name = "enumerate-all")]
    EnumerateAll,
    #[value(name = "find-one")]
    FindOne,
    Count,
}

#[derive(Clone, Debug, ValueEnum)]
enum GrounderArg {
    Naive,
    #[value(name = "semi-naive")]
    SemiNaive,
}

#[derive(Clone, Debug, ValueEnum)]
enum AttackArg {
    Pairwise,
    Indexed,
}

#[derive(Clone, Debug, ValueEnum)]
enum SolverArg {
    #[value(name = "naive-enumeration")]
    NaiveEnumeration,
    #[cfg(feature = "sat")]
    Sat,
    #[cfg(feature = "sat")]
    #[value(name = "scc-sat")]
    SccSat,
    #[cfg(feature = "cadical")]
    #[value(name = "sat-cadical")]
    SatCadical,
    #[cfg(feature = "cadical")]
    #[value(name = "scc-sat-cadical")]
    SccSatCadical,
    #[cfg(feature = "aspartix")]
    Aspartix,
    #[cfg(feature = "iccma")]
    Mutoksia,
}

#[derive(Clone, Debug, ValueEnum)]
enum PresetArg {
    Classical,
    #[cfg(feature = "sat")]
    Optimised,
    Accrual,
}

#[derive(Clone, Debug, ValueEnum)]
enum PrefMode {
    None,
    Flat,
    #[value(name = "last-link-elitist")]
    LastLinkElitist,
    #[value(name = "last-link-democratic")]
    LastLinkDemocratic,
    #[value(name = "weakest-link-elitist")]
    WeakestLinkElitist,
    #[value(name = "weakest-link-democratic")]
    WeakestLinkDemocratic,
}

impl PrefMode {
    fn to_preference_mode(&self) -> PreferenceMode {
        match self {
            PrefMode::None => PreferenceMode::None,
            PrefMode::Flat => PreferenceMode::Flat,
            PrefMode::LastLinkElitist => PreferenceMode::LastLinkElitist,
            PrefMode::LastLinkDemocratic => PreferenceMode::LastLinkDemocratic,
            PrefMode::WeakestLinkElitist => PreferenceMode::WeakestLinkElitist,
            PrefMode::WeakestLinkDemocratic => PreferenceMode::WeakestLinkDemocratic,
        }
    }
}

#[derive(Clone, Debug, ValueEnum)]
enum FormatArg {
    Simple,
    Native,
}

#[derive(Clone, Debug, ValueEnum)]
enum LiftingArg {
    Elitist,
    Democratic,
}

// ---------------------------------------------------------------------------
// Pipeline configuration
// ---------------------------------------------------------------------------

fn build_pipeline_config(cli: &Cli) -> Result<PipelineConfig, Box<dyn std::error::Error>> {
    if let Some(preset) = &cli.preset {
        return Ok(match preset {
            PresetArg::Classical => PipelineConfig::classical(),
            #[cfg(feature = "sat")]
            PresetArg::Optimised => PipelineConfig::optimised(),
            PresetArg::Accrual => PipelineConfig::accrual(),
        });
    }

    let grounder = match cli.grounder {
        GrounderArg::Naive => GrounderConfig::Naive,
        GrounderArg::SemiNaive => GrounderConfig::SemiNaive,
    };

    let attack_computer = match cli.attack_computer {
        AttackArg::Pairwise => AttackComputerConfig::Pairwise,
        AttackArg::Indexed => AttackComputerConfig::Indexed,
    };

    let solver = match cli.solver {
        SolverArg::NaiveEnumeration => SolverConfig::NaiveEnumeration,
        #[cfg(feature = "sat")]
        SolverArg::Sat => SolverConfig::Sat,
        #[cfg(feature = "sat")]
        SolverArg::SccSat => SolverConfig::SccSat,
        #[cfg(feature = "cadical")]
        SolverArg::SatCadical => SolverConfig::SatCadical,
        #[cfg(feature = "cadical")]
        SolverArg::SccSatCadical => SolverConfig::SccSatCadical,
        #[cfg(feature = "aspartix")]
        SolverArg::Aspartix => {
            let encodings_dir = cli
                .encodings_dir
                .as_ref()
                .map(|p| p.to_string_lossy().into_owned())
                .ok_or("--encodings-dir is required when using --solver aspartix")?;
            SolverConfig::Aspartix {
                clingo_path: "clingo".into(),
                encodings_dir,
            }
        }
        #[cfg(feature = "iccma")]
        SolverArg::Mutoksia => {
            let solver_path = cli
                .solver_path
                .as_ref()
                .map(|p| p.to_string_lossy().into_owned())
                .ok_or("--solver-path is required when using --solver=mutoksia")?;
            SolverConfig::Mutoksia { solver_path }
        }
    };

    Ok(PipelineConfig {
        name: String::new(),
        grounder,
        arg_constructor: ArgConstructorConfig::ForwardChaining,
        attack_computer,
        evaluator: EvaluatorConfig::Classical { solver },
    })
}

fn build_preference(cli: &Cli, prefs: &[RulePreference]) -> PreferenceConfig {
    if let Some(PresetArg::Accrual) = &cli.preset {
        let lifting = match cli.accrual_lifting {
            LiftingArg::Elitist => LiftingStrategy::Elitist,
            LiftingArg::Democratic => LiftingStrategy::Democratic,
        };
        let ordering = build_ordering(&PreferenceMode::None, prefs);
        return PreferenceConfig::SetPreference(Box::new(LiftedSetPreference {
            base: ordering,
            lifting,
        }));
    }

    PreferenceConfig::ArgumentOrdering(build_ordering(&cli.preferences.to_preference_mode(), prefs))
}

// ---------------------------------------------------------------------------
// Preset / component-flag mutual exclusivity check
// ---------------------------------------------------------------------------

fn check_preset_conflicts(cli: &Cli) -> Result<(), Box<dyn std::error::Error>> {
    if cli.preset.is_none() {
        return Ok(());
    }

    let has_grounder = std::env::args().any(|a| a == "--grounder");
    let has_attack = std::env::args().any(|a| a == "--attack-computer");
    let has_solver = std::env::args().any(|a| a == "--solver");

    if has_grounder || has_attack || has_solver {
        return Err(
            "--preset is mutually exclusive with --grounder, --attack-computer, and --solver"
                .into(),
        );
    }
    Ok(())
}

// ---------------------------------------------------------------------------
// Main
// ---------------------------------------------------------------------------

fn run() -> Result<(), Box<dyn std::error::Error>> {
    let cli = Cli::parse();

    check_preset_conflicts(&cli)?;

    let json_str = std::fs::read_to_string(&cli.input)
        .map_err(|e| format!("failed to read input file '{}': {e}", cli.input.display()))?;

    let (system, rule_prefs) = match cli.format {
        FormatArg::Simple => {
            let theory: SimpleTheory = serde_json::from_str(&json_str).map_err(|e| {
                format!(
                    "failed to parse theory JSON from '{}': {e}",
                    cli.input.display()
                )
            })?;
            let prefs = theory.rule_preferences.clone();
            let (sys, warnings) = simple::build_system(&theory)
                .map_err(|e| format!("failed to build system: {e}"))?;
            for w in &warnings {
                eprintln!("warning: {w:?}");
            }
            (sys, prefs)
        }
        FormatArg::Native => {
            let native: NativeTheory = serde_json::from_str(&json_str).map_err(|e| {
                format!(
                    "failed to parse native theory JSON from '{}': {e}",
                    cli.input.display()
                )
            })?;
            let sys = native
                .system
                .to_system()
                .map_err(|e| format!("failed to convert native theory to AspicSystem: {e}"))?;
            (sys, native.rule_preferences)
        }
    };

    let semantics = cli.semantics.to_semantics();

    let config = build_pipeline_config(&cli)?;
    let preference = build_preference(&cli, &rule_prefs);
    let pipeline = config.build(system, preference);

    let t0 = Instant::now();
    let grounded_system = pipeline
        .ground()
        .map_err(|e| format!("grounding failed: {e}"))?;
    let grounding_ms = t0.elapsed().as_secs_f64() * 1000.0;

    let t1 = Instant::now();
    let store = pipeline.construct(&grounded_system);
    let construction_ms = t1.elapsed().as_secs_f64() * 1000.0;

    let t2 = Instant::now();
    let attacks = pipeline.compute_attacks(&store, &grounded_system.contrariness);
    let attacks_ms = t2.elapsed().as_secs_f64() * 1000.0;

    let num_attacks = attacks.len();

    let output = match cli.task {
        TaskArg::EnumerateAll => {
            let t3 = Instant::now();
            let eval = pipeline
                .evaluator
                .evaluate(&store, &attacks, semantics, &pipeline.preference)
                .map_err(|e| format!("evaluation failed: {e}"))?;
            let evaluation_ms = t3.elapsed().as_secs_f64() * 1000.0;
            let total_ms = t0.elapsed().as_secs_f64() * 1000.0;
            let timings = Timings {
                grounding_ms,
                construction_ms,
                attacks_ms,
                evaluation_ms,
                total_ms,
                num_attacks,
            };
            PipelineOutput::from_evaluation(&store, &eval, timings)
        }
        TaskArg::FindOne => {
            let t3 = Instant::now();
            let eval = pipeline
                .evaluator
                .find_one(&store, &attacks, semantics, &pipeline.preference)
                .map_err(|e| format!("evaluation failed: {e}"))?;
            let evaluation_ms = t3.elapsed().as_secs_f64() * 1000.0;
            let total_ms = t0.elapsed().as_secs_f64() * 1000.0;
            let timings = Timings {
                grounding_ms,
                construction_ms,
                attacks_ms,
                evaluation_ms,
                total_ms,
                num_attacks,
            };
            PipelineOutput::from_evaluation(&store, &eval, timings)
        }
        TaskArg::Count => {
            let t3 = Instant::now();
            let count = pipeline
                .evaluator
                .count(&store, &attacks, semantics, &pipeline.preference)
                .map_err(|e| format!("evaluation failed: {e}"))?;
            let evaluation_ms = t3.elapsed().as_secs_f64() * 1000.0;
            let total_ms = t0.elapsed().as_secs_f64() * 1000.0;
            let timings = Timings {
                grounding_ms,
                construction_ms,
                attacks_ms,
                evaluation_ms,
                total_ms,
                num_attacks,
            };
            PipelineOutput::from_count(&store, count, timings)
        }
    };

    println!(
        "{}",
        serde_json::to_string_pretty(&output).expect("failed to serialise output JSON")
    );

    Ok(())
}

fn main() -> ExitCode {
    match run() {
        Ok(()) => ExitCode::SUCCESS,
        Err(e) => {
            eprintln!("error: {e}");
            ExitCode::FAILURE
        }
    }
}
