use std::env;
use std::fmt::write;
use std::path::PathBuf;
// CLI output.
pub(crate) mod output;

use crate::artifact::{
    Artifact, ArtifactCreator, ArtifactSaver, JsonTrace, TlaConfigFile, TlaFile, TlaFileSuite,
    TlaTrace,
};
use crate::Error;
use clap::{AppSettings, Clap, Subcommand};
use serde_json::{json, Value as JsonValue};
use std::path::Path;

/// A struct that generates a CLI for `modelator` using [`clap`].
#[derive(Clap, Debug)]
#[clap(name = "modelator")]
#[clap(setting = AppSettings::DisableHelpSubcommand)]
pub struct CliOptions {
    #[clap(subcommand)]
    subcommand: Modules,
}

#[derive(Debug, Subcommand)]
enum Modules {
    /// Generate TLA+ test cases and parse TLA+ traces.
    #[clap(subcommand)]
    Tla(TlaMethods),
    /// Generate TLA+ traces using Apalache.
    #[clap(subcommand)]
    Apalache(ApalacheMethods),
    /// Generate TLA+ traces using TLC.
    #[clap(subcommand)]
    Tlc(TlcMethods),
}

#[derive(Debug, Subcommand)]
#[clap(setting = AppSettings::DisableHelpSubcommand)]
enum TlaMethods {
    /// Generate TLA+ tests.
    GenerateTests {
        /// TLA+ file with test cases.
        tla_file: String,
        /// TLA+ config file with CONSTANTS, INIT and NEXT.
        tla_config_file: String,
    },
    /// Convert a TLA+ trace to a JSON trace.
    TlaTraceToJsonTrace {
        /// File with a TLA+ trace produced by the Apalache or TLC modules.
        tla_trace_file: String,
    },
}

#[derive(Debug, Subcommand)]
#[clap(setting = AppSettings::DisableHelpSubcommand)]
enum ApalacheMethods {
    /// Generate TLA+ trace from a TLA+ test.
    Test {
        /// TLA+ file generated by the generate-test method in the TLA module.
        tla_file: String,
        /// TLA+ config file generated by the generate-test method in the TLA module.
        tla_config_file: String,
    },
    /// Parse a TLA+ file.
    Parse {
        /// TLA+ file to be parsed.
        tla_file: String,
    },
}

#[derive(Debug, Subcommand)]
#[clap(setting = AppSettings::DisableHelpSubcommand)]
enum TlcMethods {
    /// Generate TLA+ trace from a TLA+ test.
    Test {
        /// TLA+ file generated by the generate-test method in the TLA module.
        tla_file: String,
        /// TLA+ config file generated by the generate-test method in the TLA module.
        tla_config_file: String,
    },
}

impl CliOptions {
    /// Function that runs `modelator` given the parameters in the [CliOptions].
    pub fn run(self) -> output::CliOutput {
        let result = self.subcommand.run();
        output::CliOutput::with_result(result)
    }
}

impl Modules {
    fn run(self) -> Result<JsonValue, Error> {
        // setup modelator
        let runtime = crate::ModelatorRuntime::default();
        runtime.setup()?;

        // run the subcommand
        match self {
            Self::Tla(options) => options.run(),
            Self::Apalache(options) => options.run(),
            Self::Tlc(options) => options.run(),
        }
    }
}

impl TlaMethods {
    fn run(self) -> Result<JsonValue, Error> {
        match self {
            Self::GenerateTests {
                tla_file,
                tla_config_file,
            } => Self::generate_tests(tla_file, tla_config_file),
            Self::TlaTraceToJsonTrace { tla_trace_file } => {
                Self::tla_trace_to_json_trace(tla_trace_file)
            }
        }
    }

    fn generate_tests(
        tla_file_path: String,
        tla_config_file_path: String,
    ) -> Result<JsonValue, Error> {
        let file_suite =
            TlaFileSuite::from_tla_and_config_paths(tla_file_path, tla_config_file_path)?;
        let tests = crate::model::language::Tla::generate_tests(&file_suite)?;
        tracing::debug!("Tla::generate_tests output {:#?}", tests);

        let dir = env::current_dir()?;

        // Write the results, collect path names
        let written_files = {
            let mut ret = Vec::<(PathBuf, PathBuf)>::new();
            for tla_test_suite in tests {
                let tla_file_full_path = tla_test_suite.tla_file.try_write_to_dir(&dir)?;
                let cfg_file_full_path = tla_test_suite.tla_config_file.try_write_to_dir(&dir)?;
                ret.push((tla_file_full_path, cfg_file_full_path));
            }
            ret
        };

        json_list_generated_tests(written_files)
    }

    fn tla_trace_to_json_trace(tla_trace_file: String) -> Result<JsonValue, Error> {
        let tla_trace = TlaTrace::try_read_from_file(tla_trace_file)?;
        let json_trace = crate::model::language::Tla::tla_trace_to_json_trace(tla_trace)?;
        tracing::debug!("Tla::tla_trace_to_json_trace output {}", json_trace);
        write_json_trace_to_file(json_trace)
    }
}

impl ApalacheMethods {
    fn run(self) -> Result<JsonValue, Error> {
        match self {
            Self::Test {
                tla_file,
                tla_config_file,
            } => Self::test(tla_file, tla_config_file),
            Self::Parse { tla_file } => Self::parse(tla_file),
        }
    }

    fn test(tla_file_path: String, tla_config_file_path: String) -> Result<JsonValue, Error> {
        let runtime = crate::ModelatorRuntime::default();
        let input_artifacts =
            TlaFileSuite::from_tla_and_config_paths(tla_file_path, tla_config_file_path)?;
        let res = {
            let mut ret = crate::model::checker::Apalache::test(&input_artifacts, &runtime)?;
            ret.0.extends_module_name = Some(input_artifacts.tla_file.module_name().to_string());
            ret
        };
        tracing::debug!("Apalache::test output {}", res.0);
        write_tla_trace_to_file(res.0)
    }

    fn parse(tla_file: String) -> Result<JsonValue, Error> {
        let runtime = crate::ModelatorRuntime::default();
        let tla_file = TlaFileSuite::from_tla_path(tla_file)?;
        let res = crate::model::checker::Apalache::parse(&tla_file, &runtime)?;
        tracing::debug!("Apalache::parse output {}", res.0);
        write_parsed_tla_file_to_file(res.0)
    }
}

impl TlcMethods {
    fn run(self) -> Result<JsonValue, Error> {
        match self {
            Self::Test {
                tla_file,
                tla_config_file,
            } => Self::test(tla_file, tla_config_file),
        }
    }

    fn test(tla_file_path: String, tla_config_file_path: String) -> Result<JsonValue, Error> {
        let runtime = crate::ModelatorRuntime::default();
        let input_artifacts =
            TlaFileSuite::from_tla_and_config_paths(tla_file_path, tla_config_file_path)?;
        let tla_trace = {
            let mut ret = crate::model::checker::Tlc::test(&input_artifacts, &runtime)?;
            ret.0.extends_module_name = Some(input_artifacts.tla_file.module_name().to_string());
            //TODO: do something with log
            ret.0
        };
        tracing::debug!("Tlc::test output {}", tla_trace);
        write_tla_trace_to_file(tla_trace)
    }
}

#[allow(clippy::unnecessary_wraps)]
fn json_list_generated_tests(test_files: Vec<(PathBuf, PathBuf)>) -> Result<JsonValue, Error> {
    let json_array = test_files
        .into_iter()
        .map(|(tla, cfg)| {
            json!({
                "tla_file": tla.into_os_string().into_string().unwrap(),
                "tla_config_file": cfg.into_os_string().into_string().unwrap()
            })
        })
        .collect();
    Ok(JsonValue::Array(json_array))
}

#[allow(clippy::unnecessary_wraps)]
fn write_parsed_tla_file_to_file(tla_file: TlaFile) -> Result<JsonValue, Error> {
    // The parsed file is a TLA+ module with the same module name as the passed input module.
    // Therefore we provide another name for the output.
    let name = format!("{}Parsed.tla", tla_file.module_name());
    let path = Path::new(&name);
    tla_file.try_write_to_file(path)?;
    Ok(json!({
        "tla_file": crate::util::absolute_path(path),
    }))
}

fn write_tla_trace_to_file(tla_trace: TlaTrace) -> Result<JsonValue, Error> {
    // TODO: hardcoded!
    let path = Path::new("trace.tla");
    tla_trace.try_write_to_file(path)?;
    Ok(json!({
        "tla_trace_file": crate::util::absolute_path(&path),
    }))
}

fn write_json_trace_to_file(json_trace: JsonTrace) -> Result<JsonValue, Error> {
    // TODO: hardcoded!
    let path = Path::new("trace.json");
    json_trace.try_write_to_file(path)?;
    Ok(json!({
        "json_trace_file": crate::util::absolute_path(&path),
    }))
}