brrr-lint 0.1.0

//! brrr-lint: A fast linter and language server for F* (FStar).
//!
//! A standalone LSP server and linter for F*, the proof-oriented programming language.
//!
//! # Usage
//!
//! ```bash
//! # Run LSP server (default)
//! brrr-lint serve
//!
//! # Check F* files for issues (like ruff check)
//! brrr-lint check src/
//!
//! # Preview fixes (dry-run mode - DEFAULT, no files modified)
//! brrr-lint fix src/
//!
//! # Actually apply fixes and write changes
//! brrr-lint fix src/ --apply
//!
//! # Run with debug logging
//! brrr-lint --debug serve
//! ```

mod config;
mod connection;
mod document;
mod error;
mod lint;
mod protocol;
mod server;

use clap::{Parser, Subcommand};
use config::LspSettings;
use lint::{DryRunFormat, LintConfig, LintEngine, OutputFormat};
use server::FstarServer;
use std::path::PathBuf;
use tower_lsp::{LspService, Server};
use tracing::{info, Level};
use tracing_subscriber::FmtSubscriber;

/// brrr-lint: Fast F* Linter and Language Server.
#[derive(Parser, Debug)]
#[command(name = "brrr-lint")]
#[command(author)]
#[command(version)]
#[command(about = "A fast linter and language server for F* (FStar)", long_about = None)]
struct Cli {
    /// Enable debug logging.
    #[arg(short, long, global = true)]
    debug: bool,

    /// Path to F* executable.
    #[arg(long, global = true)]
    fstar_exe: Option<String>,

    #[command(subcommand)]
    command: Option<Commands>,
}

#[derive(Subcommand, Debug)]
enum Commands {
    /// Run the LSP server (default if no subcommand).
    Serve {
        /// Run full verification on file open.
        #[arg(long)]
        verify_on_open: bool,

        /// Run full verification on file save (default: true).
        #[arg(long, default_value = "true")]
        verify_on_save: bool,

        /// Enable flycheck (continuous lax checking).
        #[arg(long, default_value = "true")]
        fly_check: bool,

        /// Query timeout in milliseconds.
        #[arg(long, default_value = "30000")]
        timeout_ms: u64,

        /// Maximum concurrent F* processes.
        #[arg(long, default_value = "4")]
        max_processes: usize,

        /// Log to file instead of stderr.
        #[arg(long)]
        log_file: Option<String>,
    },

    /// Check F* files for issues (like `ruff check`).
    Check {
        /// Files or directories to check.
        #[arg(required = true)]
        paths: Vec<PathBuf>,

        /// Comma-separated list of rule codes to enable (e.g., FST001,FST002).
        #[arg(long)]
        select: Option<String>,

        /// Comma-separated list of rule codes to ignore.
        #[arg(long)]
        ignore: Option<String>,

        /// Output format.
        #[arg(long, value_enum, default_value = "text")]
        format: OutputFormat,

        /// Show fixes that would be applied without applying them.
        #[arg(long)]
        show_fixes: bool,

        /// Exit with code 0 even if issues are found.
        #[arg(long)]
        exit_zero: bool,
    },

    /// Fix F* files automatically (like `ruff check --fix`).
    ///
    /// SAFETY: By default, this command runs in DRY-RUN mode and shows what
    /// would be changed WITHOUT modifying any files. Use --apply to actually
    /// write the changes.
    ///
    /// Safety levels control which fixes can be applied:
    /// - Safe: Can be auto-applied with --apply
    /// - Caution: Shows warning, applies with --apply
    /// - Unsafe: Requires --force in addition to --apply
    Fix {
        /// Files or directories to fix.
        #[arg(required = true)]
        paths: Vec<PathBuf>,

        /// Comma-separated list of rule codes to fix (e.g., FST001,FST002).
        #[arg(long)]
        select: Option<String>,

        /// Comma-separated list of rule codes to ignore.
        #[arg(long)]
        ignore: Option<String>,

        /// Actually apply the fixes and write changes to files.
        /// Without this flag, the command runs in dry-run mode and only
        /// shows what WOULD be changed.
        #[arg(long)]
        apply: bool,

        /// Force applying unsafe fixes (requires --apply).
        /// Unsafe fixes have higher risk and may require manual review.
        /// Use with caution.
        #[arg(long)]
        force: bool,

        /// Output format for diagnostics.
        #[arg(long, value_enum, default_value = "text")]
        format: OutputFormat,

        /// Dry-run output format (when --apply is not used).
        /// - concise: One line per fix with counts
        /// - full: Detailed diff-style output with boxes (default)
        /// - json: Machine-readable JSON output
        #[arg(long, value_enum, default_value = "full")]
        dry_run_format: DryRunFormat,
    },

    /// List all available lint rules.
    Rules,
}

#[tokio::main]
async fn main() {
    let cli = Cli::parse();

    // Initialize logging
    let log_level = if cli.debug { Level::DEBUG } else { Level::INFO };

    let subscriber = FmtSubscriber::builder()
        .with_max_level(log_level)
        .with_writer(std::io::stderr)
        .with_ansi(true)
        .finish();

    tracing::subscriber::set_global_default(subscriber).expect("Failed to set tracing subscriber");

    match cli.command {
        None | Some(Commands::Serve { .. }) => {
            run_server(cli).await;
        }
        Some(Commands::Check {
            paths,
            select,
            ignore,
            format,
            show_fixes,
            exit_zero,
        }) => {
            let config = LintConfig::new(select, ignore, cli.fstar_exe);
            let engine = LintEngine::new(config);
            let exit_code = engine.check(&paths, format, show_fixes).await;
            if !exit_zero {
                std::process::exit(exit_code);
            }
        }
        Some(Commands::Fix {
            paths,
            select,
            ignore,
            apply,
            force,
            format,
            dry_run_format,
        }) => {
            let config = LintConfig::new(select, ignore, cli.fstar_exe);
            let engine = LintEngine::new(config);
            // dry_run is the default (safe mode); --apply enables writing
            let dry_run = !apply;
            // --force only has effect when --apply is also used
            let force_apply = force && apply;
            let exit_code = engine.fix(&paths, format, dry_run, dry_run_format, force_apply).await;
            std::process::exit(exit_code);
        }
        Some(Commands::Rules) => {
            lint::print_rules();
        }
    }
}

async fn run_server(cli: Cli) {
    // Extract serve options or use defaults
    let (verify_on_open, verify_on_save, fly_check, timeout_ms, max_processes) = match cli.command {
        Some(Commands::Serve {
            verify_on_open,
            verify_on_save,
            fly_check,
            timeout_ms,
            max_processes,
            ..
        }) => (
            verify_on_open,
            verify_on_save,
            fly_check,
            timeout_ms,
            max_processes,
        ),
        _ => (false, true, true, 30000, 4),
    };

    info!("brrr-lint LSP server starting");
    info!("Version: {}", env!("CARGO_PKG_VERSION"));
    info!("Debug: {}", cli.debug);

    // Build CLI-derived settings
    let cli_settings = LspSettings {
        verify_on_open,
        verify_on_save,
        fly_check,
        debug: cli.debug,
        timeout_ms,
        max_processes,
        fstar_exe: cli.fstar_exe,
    };

    // Create LSP service with custom F* notification and request handlers
    let (service, socket) = LspService::build(|client| FstarServer::new(client, cli_settings))
        .custom_method(
            "$/fstar/verifyToPosition",
            FstarServer::handle_verify_to_position,
        )
        .custom_method("$/fstar/restart", FstarServer::handle_restart)
        .custom_method(
            "$/fstar/killAndRestartSolver",
            FstarServer::handle_kill_and_restart_solver,
        )
        .custom_method("$/fstar/killAll", FstarServer::handle_kill_all)
        .custom_method(
            "$/fstar/getTranslatedFst",
            FstarServer::handle_get_translated_fst,
        )
        // Custom requests for querying verification state
        .custom_method(
            "$/fstar/getDiagnostics",
            FstarServer::handle_get_diagnostics,
        )
        .custom_method("$/fstar/getFragments", FstarServer::handle_get_fragments)
        .finish();

    // Run server with stdio transport
    let stdin = tokio::io::stdin();
    let stdout = tokio::io::stdout();

    Server::new(stdin, stdout, socket).serve(service).await;

    info!("brrr-lint LSP server shutting down");
}