csw-cli 0.1.0

//! # csw-cli
//!
//! Command-line interface for the Categorical Semantics Workbench.
//!
//! ## Usage
//!
//! ```bash
//! # Show help
//! csw --help
//!
//! # Show a derived type system
//! csw show --example stlc
//!
//! # Generate code
//! csw derive --example stlc --output generated/stlc/
//! ```

use anyhow::Result;
use clap::{Parser, Subcommand};
use csw_core::CategoryBuilder;
use csw_derive::Deriver;
use csw_generate::{Generator, RustGenerator};
use std::path::PathBuf;

#[derive(Parser)]
#[command(name = "csw")]
#[command(author, version, about = "Categorical Semantics Workbench - derive type systems from categorical structures", long_about = None)]
struct Cli {
    #[command(subcommand)]
    command: Commands,
}

#[derive(Subcommand)]
enum Commands {
    /// Derive a type system and generate code
    Derive {
        /// Use a built-in example (stlc, linear, affine)
        #[arg(long)]
        example: Option<String>,

        /// Output directory for generated code
        #[arg(short, long)]
        output: PathBuf,

        /// Target language (rust, typescript)
        #[arg(long, default_value = "rust")]
        target: String,
    },

    /// Show a derived type system without generating code
    Show {
        /// Use a built-in example (stlc, linear, affine)
        #[arg(long)]
        example: Option<String>,
    },

    /// Validate a specification
    Validate {
        /// Use a built-in example
        #[arg(long)]
        example: Option<String>,
    },
}

fn main() -> Result<()> {
    let cli = Cli::parse();

    match cli.command {
        Commands::Derive {
            example,
            output,
            target,
        } => {
            let spec = get_example_spec(&example.unwrap_or_else(|| "stlc".to_string()))?;
            let ts = Deriver::derive(&spec);

            println!("Deriving type system: {}", ts.name);
            println!("Generating {} code to: {}", target, output.display());

            match target.as_str() {
                "rust" => RustGenerator::generate(&ts, &output)?,
                _ => anyhow::bail!("unsupported target: {}", target),
            }

            println!("Done!");
            Ok(())
        }

        Commands::Show { example } => {
            let spec = get_example_spec(&example.unwrap_or_else(|| "stlc".to_string()))?;
            let ts = Deriver::derive(&spec);
            println!("{}", ts);
            Ok(())
        }

        Commands::Validate { example } => {
            let name = example.unwrap_or_else(|| "stlc".to_string());
            match get_example_spec(&name) {
                Ok(spec) => {
                    println!("✓ {} is valid", spec.name);
                    println!("  Terminal: {}", spec.structure.terminal);
                    println!("  Products: {}", spec.structure.products);
                    println!("  Exponentials: {}", spec.structure.exponentials);
                    println!("  Cartesian: {}", spec.is_cartesian());
                    println!("  Linear: {}", spec.is_linear());
                    println!("  Affine: {}", spec.is_affine());
                    Ok(())
                }
                Err(e) => {
                    println!("✗ Validation failed: {}", e);
                    std::process::exit(1);
                }
            }
        }
    }
}

fn get_example_spec(name: &str) -> Result<csw_core::CategorySpec> {
    match name {
        "stlc" => CategoryBuilder::new("STLC")
            .with_base("Int")
            .with_base("Bool")
            .with_terminal()
            .with_products()
            .with_exponentials()
            .cartesian()
            .build()
            .map_err(|e| anyhow::anyhow!("{}", e)),

        "linear" => CategoryBuilder::new("Linear")
            .with_base("Int")
            .with_base("Bool")
            .with_tensor()
            .with_linear_hom()
            .with_symmetry()
            .linear()
            .build()
            .map_err(|e| anyhow::anyhow!("{}", e)),

        "affine" => CategoryBuilder::new("Affine")
            .with_base("Int")
            .with_base("Bool")
            .with_tensor()
            .with_linear_hom()
            .with_symmetry()
            .affine()
            .build()
            .map_err(|e| anyhow::anyhow!("{}", e)),

        "bccc" => CategoryBuilder::new("BCCC")
            .with_base("Int")
            .with_base("Bool")
            .with_terminal()
            .with_initial()
            .with_products()
            .with_coproducts()
            .with_exponentials()
            .cartesian()
            .build()
            .map_err(|e| anyhow::anyhow!("{}", e)),

        _ => anyhow::bail!("unknown example: {}. Available: stlc, linear, affine, bccc", name),
    }
}