// SPDX-License-Identifier: MPL-2.0
// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
//
// Code generation orchestrator for dafniser.
// Coordinates parsing manifest specs into ABI types, generating .dfy files,
// and producing build/verify commands.

pub mod compiler;
pub mod dafny_gen;
pub mod parser;

use anyhow::{Context, Result};
use std::fs;
use std::path::Path;

use crate::manifest::Manifest;

/// Generate all Dafny artifacts from a manifest.
///
/// 1. Parse function specs into ABI-level `DafnyFunction` values.
/// 2. Generate .dfy source files with requires/ensures/decreases clauses.
/// 3. Write verification and build command scripts.
pub fn generate_all(manifest: &Manifest, output_dir: &str) -> Result<()> {
    let out = Path::new(output_dir);
    fs::create_dir_all(out).context("Failed to create output directory")?;

    // Step 1: parse manifest specs into ABI-level DafnyModule.
    let module = parser::parse_manifest(manifest)?;

    // Step 2: generate the .dfy file.
    let dfy_content = dafny_gen::generate_dfy(&module);
    let dfy_path = out.join(format!("{}.dfy", module.name));
    fs::write(&dfy_path, &dfy_content)
        .with_context(|| format!("Failed to write {}", dfy_path.display()))?;

    // Step 3: generate verification and build command scripts.
    let target = parser::parse_target(&manifest.dafny.target)?;
    let verify_cmd = compiler::verification_command(&dfy_path, manifest.dafny.verify_timeout);
    let build_cmd = compiler::build_command(&dfy_path, target);

    let commands_path = out.join("commands.sh");
    let commands_content = format!(
        "#!/usr/bin/env bash\n\
         # SPDX-License-Identifier: MPL-2.0\n\
         # Generated by dafniser — do not edit.\n\n\
         # Verify all assertions, pre/postconditions, invariants:\n\
         {}\n\n\
         # Compile to target language ({}):\n\
         {}\n",
        verify_cmd, target, build_cmd,
    );
    fs::write(&commands_path, &commands_content)
        .with_context(|| format!("Failed to write {}", commands_path.display()))?;

    println!("  Generated: {}", dfy_path.display());
    println!("  Generated: {}", commands_path.display());
    Ok(())
}

/// Build the generated Dafny artifacts using the Dafny compiler.
pub fn build(manifest: &Manifest, _release: bool) -> Result<()> {
    let target = parser::parse_target(&manifest.dafny.target)?;
    println!(
        "Build plan for '{}' -> target {}:",
        manifest.project.name, target
    );
    println!(
        "  1. dafny verify <file>.dfy --verification-time-limit {}",
        manifest.dafny.verify_timeout
    );
    println!(
        "  2. dafny build <file>.dfy --target {}",
        target.dafny_target_flag()
    );
    println!("  (Run `dafniser generate` first, then execute commands.sh)");
    Ok(())
}

/// Run the compiled workload.
pub fn run(manifest: &Manifest, _args: &[String]) -> Result<()> {
    let target = parser::parse_target(&manifest.dafny.target)?;
    println!(
        "Run plan for '{}' (target {}):",
        manifest.project.name, target
    );
    println!("  Execute the compiled output from `dafny build`.");
    println!(
        "  (Ensure Dafny runtime is available for target {}.)",
        target
    );
    Ok(())
}
