tessellate 0.3.0

mod explain;
mod lsp;
mod project;
mod repl;
mod snapshot;
mod verify_output;

use clap::{ArgGroup, Args, Parser, Subcommand, ValueEnum};
use serde_json::{Value as JsonValue, json};
use std::fs::{self, OpenOptions};
use std::io::{self, Read, Write};
use std::path::{Path, PathBuf};
use std::process::ExitCode;
use tess::analysis::analyze_with_solver;
use tess::ast::{Cardinality, Declaration, ExprKind, NumericLiteral};
use tess::engine::{Input, Query, evaluate_query};
use tess::lexer::{TokenKind, lex};
use tess::{
    AnalysisOptions, AnalysisReport, CompiledProgram, DecisionStatus, Diagnostic, PolicyGraph,
    Severity, SolverMode, SourceFile, analyze_traces, build_policy_graph,
    compile_project_with_dependency_graph, compile_source, diff_policy_graphs,
    evaluate_query_with_provenance, format_source, run_tests,
};

const SUCCESS: u8 = 0;
const LANGUAGE_FAILURE: u8 = 1;
const USAGE_OR_IO_FAILURE: u8 = 2;

#[derive(Debug, Parser)]
#[command(
    name = "tess",
    version,
    about = "Define, test, and verify deterministic rule systems"
)]
struct Cli {
    #[command(subcommand)]
    command: Command,
}

#[derive(Debug, Subcommand)]
enum Command {
    /// Create a scalable multi-file Tess project.
    Init(InitArgs),
    /// Generate or update the deterministic local package lockfile.
    Lock(LockArgs),
    /// Validate Tess syntax, types, names, and project structure.
    Validate(ValidateArgs),
    /// Report compiler and fast static-analysis diagnostics.
    Lint(LintArgs),
    /// Execute declared tests.
    Test(TestArgs),
    /// Record or compare deterministic declared-test decision snapshots.
    Snapshot(snapshot::SnapshotArgs),
    /// Evaluate decisions from declared tests, or one explicitly selected decision.
    Run(EvaluationArgs),
    /// Evaluate one decision and print its provenance.
    Explain(EvaluationArgs),
    /// Interactively evaluate decisions and edit input facts.
    Repl(ReplArgs),
    /// Render a policy graph or compare it with a recorded JSON baseline.
    Graph(GraphArgs),
    /// Verify quantified assertions and bounded state traces.
    Verify(VerifyArgs),
    /// Rewrite a source file using the canonical format.
    Fmt(FormatArgs),
    /// Run the Language Server Protocol server over stdio.
    Lsp,
}

#[derive(Debug, Args)]
struct InitArgs {
    /// Directory to create (or an existing empty directory).
    directory: PathBuf,
    /// Tess module identifier; defaults to a sanitized directory name.
    #[arg(long, value_name = "IDENTIFIER")]
    module: Option<String>,
}

#[derive(Debug, Args)]
struct LockArgs {
    /// `tess.toml`, its project directory, or an owned `.tes` file.
    #[arg(value_name = "TARGET")]
    file: PathBuf,
}

#[derive(Debug, Args)]
struct ValidateArgs {
    /// Entry `.tes` file, `tess.toml`, or project directory.
    #[arg(value_name = "TARGET")]
    file: PathBuf,
    /// Emit the validation result as one JSON document.
    #[arg(long)]
    json: bool,
}

#[derive(Debug, Args)]
struct LintArgs {
    /// Entry `.tes` file, `tess.toml`, project directory, or `-` for stdin.
    #[arg(value_name = "TARGET")]
    file: PathBuf,
    #[arg(long)]
    json: bool,
    /// Fail when warnings are present without changing their severity.
    #[arg(long)]
    warnings_as_errors: bool,
}

#[derive(Debug, Args)]
struct TestArgs {
    /// Entry `.tes` file, `tess.toml`, or project directory.
    #[arg(value_name = "TARGET")]
    file: PathBuf,
    /// Run only this declared test.
    #[arg(long = "test", value_name = "NAME")]
    case: Option<String>,
    /// Shorthand for `--format json`.
    #[arg(long, conflicts_with = "format")]
    json: bool,
    /// Test report serialization format.
    #[arg(long, value_enum, value_name = "FORMAT", conflicts_with = "json")]
    format: Option<TestOutputFormat>,
}

#[derive(Clone, Copy, Debug, Default, ValueEnum)]
enum TestOutputFormat {
    #[default]
    Text,
    Json,
    Junit,
}

#[derive(Debug, Args)]
#[command(
    after_help = "Inside the REPL, type `help` for commands. Press Tab once to complete a suggestion and repeatedly to cycle through alternatives."
)]
struct ReplArgs {
    /// Entry `.tes` file, `tess.toml`, or project directory.
    #[arg(value_name = "TARGET")]
    file: PathBuf,
}

#[derive(Debug, Args)]
struct GraphArgs {
    /// Entry `.tes` file, `tess.toml`, or project directory.
    #[arg(value_name = "TARGET")]
    file: PathBuf,
    /// Keep this decision's rules, called functions, basis fragments, and reference closure.
    #[arg(long, value_name = "NAME")]
    decision: Option<String>,
    /// Compare the current graph with a previously recorded JSON graph.
    #[arg(long, value_name = "FILE")]
    baseline: Option<PathBuf>,
    /// Output format. Defaults to DOT normally and concise text with --baseline.
    #[arg(long, value_enum)]
    format: Option<GraphFormat>,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq, ValueEnum)]
enum GraphFormat {
    Json,
    Dot,
    Text,
}

#[derive(Debug, Args)]
#[command(group(
    ArgGroup::new("input_source")
        .required(false)
        .multiple(false)
        .args(["case", "input"])
))]
struct EvaluationArgs {
    /// Entry `.tes` file, `tess.toml`, or project directory.
    #[arg(value_name = "TARGET")]
    file: PathBuf,
    /// Use the named declared test as input for one decision evaluation.
    #[arg(long = "test", value_name = "NAME")]
    case: Option<String>,
    /// Read input facts from a JSON file instead of a declared test.
    #[arg(long, value_name = "JSON_FILE")]
    input: Option<PathBuf>,
    /// Decision call to evaluate; inferred from a selected test's first expectation.
    #[arg(long)]
    query: Option<String>,
    #[arg(long)]
    json: bool,
    #[command(flatten)]
    human_output: HumanEvaluationOutputArgs,
    /// Emit the versioned runtime provenance DAG with the raw evaluation.
    #[arg(long, requires = "json", conflicts_with_all = ["compact", "verbose"])]
    provenance: bool,
}

#[derive(Debug, Args)]
struct HumanEvaluationOutputArgs {
    /// Print only the decision result without its explanation.
    #[arg(long, conflicts_with_all = ["json", "verbose"])]
    compact: bool,
    /// Print the complete rule trace with conditions, source excerpts, and locations.
    #[arg(long, conflicts_with_all = ["json", "compact"])]
    verbose: bool,
}

#[derive(Debug, Args)]
struct VerifyArgs {
    /// Entry `.tes` file, `tess.toml`, or project directory.
    #[arg(value_name = "TARGET")]
    file: PathBuf,
    /// Verify only this declared assertion; defaults to all assertions.
    #[arg(long = "assert", value_name = "NAME")]
    invariant: Option<String>,
    /// Verify only this declared bounded trace instead of assertions.
    #[arg(long, value_name = "NAME", conflicts_with = "invariant")]
    trace: Option<String>,
    /// Maximum concrete evaluator runs per assertion; symbolic solver queries do not consume it.
    #[arg(
        long,
        default_value = "100_000",
        value_name = "N",
        value_parser = positive_usize
    )]
    max_evaluations: usize,
    /// Embedded exact solver policy for supported relational numeric assertions.
    #[arg(long, value_enum, default_value = "auto")]
    solver: SolverArgument,
    /// Emit the verification report as one JSON document.
    #[arg(long)]
    json: bool,
}

#[derive(Clone, Copy, Debug, ValueEnum)]
enum SolverArgument {
    Auto,
    Off,
    Z3,
}

impl From<SolverArgument> for SolverMode {
    fn from(value: SolverArgument) -> Self {
        match value {
            SolverArgument::Auto => Self::Auto,
            SolverArgument::Off => Self::Off,
            SolverArgument::Z3 => Self::Z3,
        }
    }
}

#[derive(Debug, Args)]
struct FormatArgs {
    /// Entry `.tes` file, `tess.toml`, or project directory.
    #[arg(value_name = "TARGET")]
    file: PathBuf,
    #[arg(long, conflicts_with = "stdout")]
    check: bool,
    #[arg(long, conflicts_with = "check")]
    stdout: bool,
}

struct CompiledFile {
    source: SourceFile,
    program: CompiledProgram,
    diagnostics: Vec<Diagnostic>,
}

enum LoadFailure {
    Io(String),
    Language {
        source: SourceFile,
        diagnostics: Vec<Diagnostic>,
    },
}

fn main() -> ExitCode {
    let cli = match Cli::try_parse() {
        Ok(cli) => cli,
        Err(error) => {
            let code = error.exit_code();
            let _ = error.print();
            return ExitCode::from(u8::try_from(code).unwrap_or(USAGE_OR_IO_FAILURE));
        }
    };
    ExitCode::from(run(cli))
}

fn run(cli: Cli) -> u8 {
    match &cli.command {
        Command::Init(arguments) => init(arguments),
        Command::Lock(arguments) => lock(arguments),
        Command::Validate(arguments) => validate(arguments),
        Command::Lint(arguments) => lint(arguments),
        Command::Test(arguments) => test(arguments),
        Command::Snapshot(arguments) => snapshot::run(arguments),
        Command::Run(arguments) => evaluate(arguments, false),
        Command::Explain(arguments) => evaluate(arguments, true),
        Command::Repl(arguments) => repl(arguments),
        Command::Graph(arguments) => graph(arguments),
        Command::Verify(arguments) => verify(arguments),
        Command::Fmt(arguments) => format(arguments),
        Command::Lsp => language_server(),
    }
}

fn graph(arguments: &GraphArgs) -> u8 {
    let loaded = match load_compiled(&arguments.file) {
        Ok(loaded) => loaded,
        Err(failure) => return report_load_failure(failure, "graph", false),
    };
    let graph = match build_policy_graph(&loaded.program, arguments.decision.as_deref()) {
        Ok(graph) => graph,
        Err(error) => {
            render_diagnostics(
                &[Diagnostic::error(
                    "C4001",
                    error.to_string(),
                    tess::Span::default(),
                )],
                &loaded.source,
            );
            return LANGUAGE_FAILURE;
        }
    };
    render_diagnostics(&loaded.diagnostics, &loaded.source);
    if let Some(path) = &arguments.baseline {
        let format = arguments.format.unwrap_or(GraphFormat::Text);
        if format == GraphFormat::Dot {
            eprintln!("error: --baseline supports `--format text` or `--format json`, not DOT");
            return USAGE_OR_IO_FAILURE;
        }
        let text = match fs::read_to_string(path) {
            Ok(text) => text,
            Err(error) => {
                eprintln!(
                    "error: could not read policy graph baseline `{}`: {error}",
                    path.display()
                );
                return USAGE_OR_IO_FAILURE;
            }
        };
        let baseline: PolicyGraph = match serde_json::from_str(&text) {
            Ok(graph) => graph,
            Err(error) => {
                eprintln!(
                    "error: invalid policy graph baseline `{}`: {error}",
                    path.display()
                );
                return USAGE_OR_IO_FAILURE;
            }
        };
        let diff = match diff_policy_graphs(&baseline, &graph) {
            Ok(diff) => diff,
            Err(error) => {
                eprintln!("error: could not compare policy graphs: {error}");
                return USAGE_OR_IO_FAILURE;
            }
        };
        let matches = diff.matches();
        let rendered = match format {
            GraphFormat::Text => diff.render_text(),
            GraphFormat::Json => match serde_json::to_string_pretty(&diff) {
                Ok(json) => format!("{json}\n"),
                Err(error) => {
                    eprintln!("error: could not encode policy graph diff as JSON: {error}");
                    return USAGE_OR_IO_FAILURE;
                }
            },
            GraphFormat::Dot => unreachable!("DOT was rejected above"),
        };
        return match write_stdout(&rendered) {
            Ok(()) if matches => SUCCESS,
            Ok(()) => LANGUAGE_FAILURE,
            Err(error) => report_io("write stdout", &error),
        };
    }

    let format = arguments.format.unwrap_or(GraphFormat::Dot);
    if format == GraphFormat::Text {
        eprintln!("error: --format text requires --baseline");
        return USAGE_OR_IO_FAILURE;
    }
    let rendered = match format {
        GraphFormat::Dot => graph.render_dot(),
        GraphFormat::Json => match serde_json::to_string_pretty(&graph) {
            Ok(json) => format!("{json}\n"),
            Err(error) => {
                eprintln!("error: could not encode policy graph as JSON: {error}");
                return USAGE_OR_IO_FAILURE;
            }
        },
        GraphFormat::Text => unreachable!("text was rejected above"),
    };
    match write_stdout(&rendered) {
        Ok(()) => SUCCESS,
        Err(error) => report_io("write stdout", &error),
    }
}

fn repl(arguments: &ReplArgs) -> u8 {
    match repl::run(&arguments.file) {
        repl::ExitStatus::Success => SUCCESS,
        repl::ExitStatus::LanguageFailure => LANGUAGE_FAILURE,
        repl::ExitStatus::IoFailure => USAGE_OR_IO_FAILURE,
    }
}

fn init(arguments: &InitArgs) -> u8 {
    match project::scaffold(&arguments.directory, arguments.module.as_deref()) {
        Ok(module) => match write_stdout(&format!(
            "created Tess project `{}` (module `{module}`)\nnext: cd {} && tess validate .\n",
            arguments.directory.display(),
            arguments.directory.display()
        )) {
            Ok(()) => SUCCESS,
            Err(error) => report_io("write stdout", &error),
        },
        Err(message) => {
            eprintln!("error: {message}");
            USAGE_OR_IO_FAILURE
        }
    }
}

fn lock(arguments: &LockArgs) -> u8 {
    match project::update_lockfile(&arguments.file) {
        Ok(path) => match write_stdout(&format!("updated {}\n", path.display())) {
            Ok(()) => SUCCESS,
            Err(error) => report_io("write stdout", &error),
        },
        Err(message) => {
            eprintln!("error: {message}");
            USAGE_OR_IO_FAILURE
        }
    }
}

fn validate(arguments: &ValidateArgs) -> u8 {
    let loaded = match load_compiled(&arguments.file) {
        Ok(loaded) => loaded,
        Err(failure) => return report_load_failure(failure, "validate", arguments.json),
    };
    if arguments.json {
        let result = json!({ "module": loaded.program.ast().module.value });
        return write_envelope("validate", true, &loaded.diagnostics, &result);
    }
    render_diagnostics(&loaded.diagnostics, &loaded.source);
    match write_stdout(&format!("validated {}\n", arguments.file.display())) {
        Ok(()) => SUCCESS,
        Err(error) => report_io("write stdout", &error),
    }
}

fn lint(arguments: &LintArgs) -> u8 {
    let (source, output) = if arguments.file == Path::new("-") {
        let source = match read_lint_source(&arguments.file) {
            Ok(source) => source,
            Err(message) => {
                eprintln!("error: {message}");
                return USAGE_OR_IO_FAILURE;
            }
        };
        let output = compile_source(source.clone());
        (source, output)
    } else {
        let project = match compile_target(&arguments.file) {
            Ok(project) => project,
            Err(message) => {
                eprintln!("error: {message}");
                return USAGE_OR_IO_FAILURE;
            }
        };
        (project.source, project.compile)
    };
    let errors = output
        .diagnostics
        .iter()
        .filter(|diagnostic| diagnostic.severity == Severity::Error)
        .count();
    let warnings = output.diagnostics.len().saturating_sub(errors);
    let ok = errors == 0 && (!arguments.warnings_as_errors || warnings == 0);
    if arguments.json {
        return write_envelope(
            "lint",
            ok,
            &output.diagnostics,
            &json!({
                "errors": errors,
                "warnings": warnings,
                "warnings_as_errors": arguments.warnings_as_errors,
            }),
        );
    }
    render_diagnostics(&output.diagnostics, &source);
    let label = if arguments.file == Path::new("-") {
        "<stdin>".to_owned()
    } else {
        arguments.file.display().to_string()
    };
    match write_stdout(&format!(
        "linted {label}: {errors} error(s), {warnings} warning(s)\n"
    )) {
        Ok(()) if ok => SUCCESS,
        Ok(()) => LANGUAGE_FAILURE,
        Err(error) => report_io("write stdout", &error),
    }
}

fn language_server() -> u8 {
    match lsp::run_stdio() {
        Ok(()) => SUCCESS,
        Err(error) => {
            eprintln!("error: Tess language server failed: {error}");
            USAGE_OR_IO_FAILURE
        }
    }
}

fn test(arguments: &TestArgs) -> u8 {
    let format = if arguments.json {
        TestOutputFormat::Json
    } else {
        arguments.format.unwrap_or_default()
    };
    let loaded = match load_compiled(&arguments.file) {
        Ok(loaded) => loaded,
        Err(failure) => {
            return report_load_failure(failure, "test", matches!(format, TestOutputFormat::Json));
        }
    };
    let case = arguments.case.as_deref().map(normalize_identifier);
    let report = run_tests(&loaded.program, case.as_deref());
    let has_selected_case = !report.outcomes.is_empty();
    let ok = has_selected_case && report.success();
    let missing_case_diagnostic = (!has_selected_case).then(|| {
        let message = case.as_ref().map_or_else(
            || "no tests are declared in this file".to_owned(),
            |name| format!("test `{name}` was not found"),
        );
        Diagnostic::error("C1001", message, tess::Span::default())
    });
    if matches!(format, TestOutputFormat::Json) {
        let mut diagnostics = loaded.diagnostics.clone();
        diagnostics.extend(missing_case_diagnostic);
        return write_envelope("test", ok, &diagnostics, &json!(report));
    }
    render_diagnostics(&loaded.diagnostics, &loaded.source);
    if let Some(diagnostic) = missing_case_diagnostic {
        render_diagnostics(&[diagnostic], &loaded.source);
    }
    let rendered = match format {
        TestOutputFormat::Text => report.render_text(),
        TestOutputFormat::Junit => report.render_junit_xml(),
        TestOutputFormat::Json => unreachable!("JSON output returned above"),
    };
    match write_stdout(&rendered) {
        Ok(()) if ok => SUCCESS,
        Ok(()) => LANGUAGE_FAILURE,
        Err(error) => report_io("write stdout", &error),
    }
}

fn evaluate(arguments: &EvaluationArgs, explain: bool) -> u8 {
    let command = if explain { "explain" } else { "run" };
    let loaded = match load_compiled(&arguments.file) {
        Ok(loaded) => loaded,
        Err(failure) => return report_load_failure(failure, command, arguments.json),
    };

    if !explain
        && arguments.case.is_none()
        && arguments.input.is_none()
        && arguments.query.is_none()
        && !arguments.provenance
    {
        return evaluate_declared_cases(
            &loaded,
            arguments.json,
            arguments.human_output.compact,
            arguments.human_output.verbose,
        );
    }

    let prepared = prepare_evaluation(&loaded, arguments);
    let (input, query, case_name) = match prepared {
        Ok(value) => value,
        Err(PrepareFailure::Usage(message) | PrepareFailure::Io(message)) => {
            eprintln!("error: {message}");
            return USAGE_OR_IO_FAILURE;
        }
        Err(PrepareFailure::Language(diagnostics)) => {
            return report_language(command, arguments.json, &loaded.source, &diagnostics);
        }
    };

    if arguments.provenance {
        let evaluation = match evaluate_query_with_provenance(&loaded.program, &input, &query) {
            Ok(evaluation) => evaluation,
            Err(diagnostic) => {
                return report_language(command, true, &loaded.source, &[diagnostic]);
            }
        };
        let ok = decision_succeeded(
            &evaluation.evaluation.result.status,
            evaluation.evaluation.result.cardinality,
        );
        return write_envelope(command, ok, &loaded.diagnostics, &json!(evaluation));
    }

    let evaluation = match evaluate_query(&loaded.program, &input, &query) {
        Ok(evaluation) => evaluation,
        Err(diagnostic) => {
            return report_language(command, arguments.json, &loaded.source, &[diagnostic]);
        }
    };
    let ok = decision_succeeded(&evaluation.result.status, evaluation.result.cardinality);
    if arguments.json {
        let mut result = evaluation_json(&evaluation);
        if explain {
            let JsonValue::Object(ref mut object) = result else {
                unreachable!("evaluation JSON is always an object");
            };
            object.insert("rules".into(), json!(evaluation.rules));
            object.insert("candidates".into(), json!(evaluation.result.candidates));
            object.insert("suppressed".into(), json!(evaluation.result.suppressed));
        }
        return write_envelope(command, ok, &loaded.diagnostics, &result);
    }
    render_diagnostics(&loaded.diagnostics, &loaded.source);
    let rendered = if arguments.human_output.compact {
        evaluation.render_text()
    } else if arguments.human_output.verbose {
        crate::explain::render_evaluation(
            &loaded.program,
            &input,
            &evaluation,
            case_name.as_deref(),
            stdout_supports_color(),
        )
    } else {
        crate::explain::render_concise_evaluation(
            &evaluation,
            case_name.as_deref(),
            stdout_supports_color(),
        )
    };
    match write_stdout(&rendered) {
        Ok(()) if ok => SUCCESS,
        Ok(()) => LANGUAGE_FAILURE,
        Err(error) => report_io("write stdout", &error),
    }
}

fn evaluate_declared_cases(
    loaded: &CompiledFile,
    json_output: bool,
    compact: bool,
    verbose: bool,
) -> u8 {
    if loaded.program.cases().is_empty() {
        eprintln!(
            "error: no tests are declared; add a test, or pass --input JSON_FILE with --query 'decision(binding)'"
        );
        return USAGE_OR_IO_FAILURE;
    }

    let mut cases = Vec::with_capacity(loaded.program.cases().len());
    for case in loaded.program.cases().values() {
        if case.expectations.is_empty() {
            return report_language(
                "run",
                json_output,
                &loaded.source,
                &[Diagnostic::error(
                    "C3003",
                    format!(
                        "test `{}` has no expectation from which to infer a query",
                        case.name.value
                    ),
                    case.name.span,
                )],
            );
        }
        let input = match Input::from_case(&loaded.program, case) {
            Ok(input) => input,
            Err(diagnostics) => {
                return report_language("run", json_output, &loaded.source, &diagnostics);
            }
        };
        let mut evaluations = Vec::with_capacity(case.expectations.len());
        for expectation in &case.expectations {
            let query = match query_from_expectation(expectation) {
                Ok(query) => query,
                Err(message) => {
                    return report_language(
                        "run",
                        json_output,
                        &loaded.source,
                        &[Diagnostic::error("C3003", message, expectation.span)],
                    );
                }
            };
            match evaluate_query(&loaded.program, &input, &query) {
                Ok(evaluation) => evaluations.push(evaluation),
                Err(diagnostic) => {
                    return report_language("run", json_output, &loaded.source, &[diagnostic]);
                }
            }
        }
        cases.push((case.name.value.clone(), input, evaluations));
    }

    let ok = cases.iter().all(|(_, _, evaluations)| {
        evaluations.iter().all(|evaluation| {
            decision_succeeded(&evaluation.result.status, evaluation.result.cardinality)
        })
    });
    if json_output {
        let result = json!({
            "cases": cases
                .iter()
                .map(|(case, _, evaluations)| json!({
                    "case": case,
                    "evaluations": evaluations.iter().map(evaluation_json).collect::<Vec<_>>(),
                }))
                .collect::<Vec<_>>(),
        });
        return write_envelope("run", ok, &loaded.diagnostics, &result);
    }

    render_diagnostics(&loaded.diagnostics, &loaded.source);
    match write_stdout(&render_declared_case_evaluations(
        &loaded.program,
        &cases,
        compact,
        verbose,
        stdout_supports_color(),
    )) {
        Ok(()) if ok => SUCCESS,
        Ok(()) => LANGUAGE_FAILURE,
        Err(error) => report_io("write stdout", &error),
    }
}

fn render_declared_case_evaluations(
    program: &CompiledProgram,
    cases: &[(String, Input, Vec<tess::Evaluation>)],
    compact: bool,
    verbose: bool,
    color: bool,
) -> String {
    if verbose {
        let mut output = String::new();
        for (case, input, evaluations) in cases {
            if !output.is_empty() {
                output.push('\n');
            }
            let rendered =
                crate::explain::render_evaluations(program, input, evaluations, Some(case), color);
            output.push_str(rendered.trim_end_matches('\n'));
            output.push('\n');
        }
        return output;
    }

    if !compact {
        let mut output = String::new();
        for (index, (case, _, evaluations)) in cases.iter().enumerate() {
            if index > 0 {
                output.push('\n');
            }
            output.push_str(&crate::explain::render_concise_evaluations(
                evaluations,
                Some(case),
                color,
            ));
        }
        return output;
    }

    if let [(_, _, evaluations)] = cases {
        return evaluations
            .iter()
            .map(tess::Evaluation::render_text)
            .collect();
    }

    let mut output = String::new();
    for (index, (case, _, evaluations)) in cases.iter().enumerate() {
        if index > 0 {
            output.push('\n');
        }
        output.push_str(case);
        output.push_str(":\n");
        for evaluation in evaluations {
            for line in evaluation.render_text().lines() {
                output.push_str("  ");
                output.push_str(line);
                output.push('\n');
            }
        }
    }
    output
}

fn verify(arguments: &VerifyArgs) -> u8 {
    let loaded = match load_compiled(&arguments.file) {
        Ok(loaded) => loaded,
        Err(failure) => return report_load_failure(failure, "verify", arguments.json),
    };
    let selected_invariant = arguments.invariant.as_deref().map(normalize_identifier);
    let selected_trace = arguments.trace.as_deref().map(normalize_identifier);
    let options = AnalysisOptions {
        max_evaluations: arguments.max_evaluations,
        ..AnalysisOptions::default()
    };
    let report = if let Some(trace) = selected_trace.as_deref() {
        AnalysisReport {
            invariants: Vec::new(),
            traces: analyze_traces(&loaded.program, Some(trace), &options),
            findings: Vec::new(),
        }
    } else {
        analyze_with_solver(
            &loaded.program,
            selected_invariant.as_deref(),
            &options,
            arguments.solver.into(),
        )
    };
    let found = if selected_trace.is_some() {
        !report.traces.is_empty()
    } else if selected_invariant.is_some() {
        !report.invariants.is_empty()
    } else {
        !report.invariants.is_empty() || !report.traces.is_empty()
    };
    let ok = found && report.success();
    let missing_property_diagnostic = (!found).then(|| {
        let (code, message) = if let Some(name) = selected_trace.as_ref() {
            ("C2002", format!("trace `{name}` was not found"))
        } else if let Some(name) = selected_invariant.as_ref() {
            ("C2001", format!("assertion `{name}` was not found"))
        } else {
            (
                "C2001",
                "no assertions or bounded traces are declared in this target".to_owned(),
            )
        };
        Diagnostic::error(code, message, tess::Span::default())
    });
    if arguments.json {
        let mut diagnostics = loaded.diagnostics.clone();
        diagnostics.extend(missing_property_diagnostic);
        return write_envelope("verify", ok, &diagnostics, &json!(report));
    }
    render_diagnostics(&loaded.diagnostics, &loaded.source);
    if let Some(diagnostic) = missing_property_diagnostic {
        render_diagnostics(&[diagnostic], &loaded.source);
    }
    match write_stdout(&crate::verify_output::render_report(
        &report,
        stdout_supports_color(),
    )) {
        Ok(()) if ok => SUCCESS,
        Ok(()) => LANGUAGE_FAILURE,
        Err(error) => report_io("write stdout", &error),
    }
}

fn format(arguments: &FormatArgs) -> u8 {
    let target = match project::resolve_target(&arguments.file) {
        Ok(target) => target,
        Err(message) => {
            eprintln!("error: {message}");
            return USAGE_OR_IO_FAILURE;
        }
    };
    let project = match compile_target(&arguments.file) {
        Ok(project) => project,
        Err(message) => {
            eprintln!("error: {message}");
            return USAGE_OR_IO_FAILURE;
        }
    };
    let import_diagnostics: Vec<_> = project
        .compile
        .diagnostics
        .iter()
        .filter(|diagnostic| diagnostic.code.starts_with('M'))
        .cloned()
        .collect();
    if !import_diagnostics.is_empty() {
        render_diagnostics(&import_diagnostics, &project.source);
        return LANGUAGE_FAILURE;
    }
    let root = target.root.canonicalize().unwrap_or(target.root);
    let project_files = project
        .files
        .iter()
        .filter(|path| path.starts_with(&root))
        .collect::<Vec<_>>();
    if arguments.stdout && project_files.len() != 1 {
        eprintln!(
            "error: --stdout requires a target with exactly one reachable source file (found {})",
            project_files.len()
        );
        return USAGE_OR_IO_FAILURE;
    }

    let mut candidates = Vec::with_capacity(project_files.len());
    for path in project_files {
        let source = match read_source(path) {
            Ok(source) => source,
            Err(message) => {
                eprintln!("error: {message}");
                return USAGE_OR_IO_FAILURE;
            }
        };
        let formatted = match format_source(source.clone()) {
            Ok(formatted) => formatted,
            Err(diagnostics) => {
                render_diagnostics(&diagnostics, &source);
                return LANGUAGE_FAILURE;
            }
        };
        candidates.push((path, source, formatted));
    }
    if arguments.stdout {
        return match write_stdout(&candidates[0].2) {
            Ok(()) => SUCCESS,
            Err(error) => report_io("write stdout", &error),
        };
    }
    if arguments.check {
        let mut changed = false;
        for (path, source, formatted) in &candidates {
            if formatted.as_str() != source.text.as_ref() {
                eprintln!("{} is not canonically formatted", path.display());
                changed = true;
            }
        }
        return if changed { LANGUAGE_FAILURE } else { SUCCESS };
    }
    for (path, source, formatted) in &candidates {
        if formatted.as_str() == source.text.as_ref() {
            continue;
        }
        if let Err(error) = atomic_replace(path, formatted.as_bytes()) {
            return report_io(&format!("write `{}`", path.display()), &error);
        }
    }
    SUCCESS
}

enum PrepareFailure {
    Usage(String),
    Io(String),
    Language(Vec<Diagnostic>),
}

fn prepare_evaluation(
    loaded: &CompiledFile,
    arguments: &EvaluationArgs,
) -> Result<(Input, Query, Option<String>), PrepareFailure> {
    let selected_case = if let Some(case_name) = &arguments.case {
        let normalized = normalize_identifier(case_name);
        Some(
            loaded
                .program
                .ast()
                .declarations
                .iter()
                .find_map(|declaration| match declaration {
                    Declaration::Case(case) if case.name.value == normalized => Some(case),
                    _ => None,
                })
                .ok_or_else(|| {
                    PrepareFailure::Language(vec![Diagnostic::error(
                        "C3001",
                        format!("test `{normalized}` was not found"),
                        tess::Span::default(),
                    )])
                })?,
        )
    } else if arguments.input.is_none() {
        Some(select_sole_case(loaded)?)
    } else {
        None
    };

    if let Some(case) = selected_case {
        let query = if let Some(query) = &arguments.query {
            parse_cli_query(query).map_err(|message| {
                PrepareFailure::Language(vec![Diagnostic::error(
                    "C3002",
                    message,
                    tess::Span::default(),
                )])
            })?
        } else {
            query_from_first_expectation(case).map_err(|message| {
                PrepareFailure::Language(vec![Diagnostic::error("C3003", message, case.name.span)])
            })?
        };
        let input = Input::from_case(&loaded.program, case).map_err(PrepareFailure::Language)?;
        return Ok((input, query, Some(case.name.value.clone())));
    }

    let input_path = arguments.input.as_ref().ok_or_else(|| {
        PrepareFailure::Usage(
            "choose a test with --test NAME or provide --input JSON_FILE".to_owned(),
        )
    })?;
    let query_text = arguments.query.as_deref().ok_or_else(|| {
        PrepareFailure::Usage("--query is required when --input is used".to_owned())
    })?;
    let query = parse_cli_query(query_text).map_err(|message| {
        PrepareFailure::Language(vec![Diagnostic::error(
            "C3002",
            message,
            tess::Span::default(),
        )])
    })?;
    let text = fs::read_to_string(input_path).map_err(|error| {
        PrepareFailure::Io(format!(
            "could not read `{}`: {error}",
            input_path.display()
        ))
    })?;
    let json = serde_json::from_str(&text).map_err(|error| {
        PrepareFailure::Io(format!(
            "invalid JSON in `{}`: {error}",
            input_path.display()
        ))
    })?;
    let input =
        Input::from_json(&loaded.program, &query, &json).map_err(PrepareFailure::Language)?;
    Ok((input, query, None))
}

fn select_sole_case(loaded: &CompiledFile) -> Result<&tess::ast::CaseDecl, PrepareFailure> {
    let cases: Vec<_> = loaded
        .program
        .ast()
        .declarations
        .iter()
        .filter_map(|declaration| match declaration {
            Declaration::Case(case) => Some(case),
            _ => None,
        })
        .collect();
    match cases.as_slice() {
        [case] => Ok(case),
        [] => Err(PrepareFailure::Usage(
            "no tests are declared; add a test and use --test NAME, or pass --input JSON_FILE with --query 'decision(binding)'"
                .to_owned(),
        )),
        _ => {
            let names = cases
                .iter()
                .map(|case| format!("`{}`", case.name.value))
                .collect::<Vec<_>>()
                .join(", ");
            Err(PrepareFailure::Usage(format!(
                "multiple tests are declared ({names}); choose one with --test NAME, or pass --input JSON_FILE with --query 'decision(binding)'"
            )))
        }
    }
}

fn query_from_first_expectation(case: &tess::ast::CaseDecl) -> Result<Query, String> {
    let expectation = case.expectations.first().ok_or_else(|| {
        format!(
            "test `{}` has no expectation from which to infer a query",
            case.name.value
        )
    })?;
    query_from_expectation(expectation)
}

fn query_from_expectation(expectation: &tess::ast::Expectation) -> Result<Query, String> {
    let arguments = expectation
        .arguments
        .iter()
        .map(|argument| match &argument.kind {
            ExprKind::Name(name) => Ok(name.clone()),
            _ => Err("an expectation contains a non-name query argument".to_owned()),
        })
        .collect::<Result<Vec<_>, _>>()?;
    Ok(Query {
        decision: expectation.decision.value.clone(),
        arguments,
    })
}

fn parse_cli_query(text: &str) -> Result<Query, String> {
    let source = SourceFile::new("<query>", text);
    let output = lex(&source);
    if let Some(diagnostic) = output.diagnostics.first() {
        return Err(format!("invalid query: {}", diagnostic.message));
    }
    let tokens = &output.tokens;
    let Some(TokenKind::Identifier(decision)) = tokens.first().map(|token| &token.kind) else {
        return Err("a query must start with a decision identifier".to_owned());
    };
    if !matches!(
        tokens.get(1).map(|token| &token.kind),
        Some(TokenKind::LeftParen)
    ) {
        return Err("a query must have the form decision(binding)".to_owned());
    }
    let mut cursor = 2;
    let mut arguments = Vec::new();
    if !matches!(
        tokens.get(cursor).map(|token| &token.kind),
        Some(TokenKind::RightParen)
    ) {
        loop {
            let Some(TokenKind::Identifier(argument)) = tokens.get(cursor).map(|token| &token.kind)
            else {
                return Err("query arguments must be identifiers".to_owned());
            };
            arguments.push(argument.clone());
            cursor += 1;
            match tokens.get(cursor).map(|token| &token.kind) {
                Some(TokenKind::Comma) => cursor += 1,
                Some(TokenKind::RightParen) => break,
                _ => return Err("query arguments must be separated by commas".to_owned()),
            }
        }
    }
    if !matches!(
        tokens.get(cursor).map(|token| &token.kind),
        Some(TokenKind::RightParen)
    ) {
        return Err("a query is missing `)`".to_owned());
    }
    cursor += 1;
    if !matches!(
        tokens.get(cursor).map(|token| &token.kind),
        Some(TokenKind::Eof)
    ) {
        return Err("unexpected text after query `)`".to_owned());
    }
    Ok(Query {
        decision: decision.clone(),
        arguments,
    })
}

fn normalize_identifier(value: &str) -> String {
    let source = SourceFile::new("<identifier>", value);
    let output = lex(&source);
    match output.tokens.as_slice() {
        [token, eof]
            if matches!(eof.kind, TokenKind::Eof)
                && matches!(token.kind, TokenKind::Identifier(_)) =>
        {
            let TokenKind::Identifier(value) = &token.kind else {
                unreachable!();
            };
            value.clone()
        }
        _ => value.to_owned(),
    }
}

fn decision_succeeded(status: &DecisionStatus, cardinality: Cardinality) -> bool {
    match status {
        DecisionStatus::Resolved { .. } => true,
        DecisionStatus::Undefined => {
            matches!(cardinality, Cardinality::ZeroOrOne | Cardinality::Many)
        }
        DecisionStatus::Unknown { .. } | DecisionStatus::Conflict { .. } => false,
    }
}

fn evaluation_json(evaluation: &tess::Evaluation) -> JsonValue {
    let (status, values, missing, reasons) = match &evaluation.result.status {
        DecisionStatus::Resolved { values } => (
            "resolved",
            values
                .iter()
                .map(tess::value::Value::to_plain_json)
                .collect(),
            Vec::<String>::new(),
            Vec::<String>::new(),
        ),
        DecisionStatus::Undefined => (
            "undefined",
            Vec::new(),
            Vec::<String>::new(),
            Vec::<String>::new(),
        ),
        DecisionStatus::Unknown { missing } => {
            ("unknown", Vec::new(), missing.clone(), Vec::<String>::new())
        }
        DecisionStatus::Conflict { values, reasons } => (
            "conflict",
            values
                .iter()
                .map(tess::value::Value::to_plain_json)
                .collect(),
            Vec::<String>::new(),
            reasons.clone(),
        ),
    };
    json!({
        "query": evaluation.query,
        "decision": evaluation.result.decision,
        "cardinality": evaluation.result.cardinality,
        "status": status,
        "values": values,
        "missing": missing,
        "reasons": reasons,
    })
}

fn load_compiled(path: &Path) -> Result<CompiledFile, LoadFailure> {
    let project = compile_target(path).map_err(LoadFailure::Io)?;
    match project.compile.program {
        Some(program) => Ok(CompiledFile {
            source: project.source,
            program,
            diagnostics: project.compile.diagnostics,
        }),
        None => Err(LoadFailure::Language {
            source: project.source,
            diagnostics: project.compile.diagnostics,
        }),
    }
}

fn compile_target(path: &Path) -> Result<tess::ProjectCompileOutput, String> {
    let target = project::resolve_target(path)?;
    compile_project_with_dependency_graph(&target.entry, &target.root, &target.dependencies)
        .map_err(|error| error.to_string())
}

fn read_source(path: &Path) -> Result<SourceFile, String> {
    fs::read_to_string(path)
        .map(|text| SourceFile::new(path.display().to_string(), text))
        .map_err(|error| format!("could not read `{}`: {error}", path.display()))
}

fn read_lint_source(path: &Path) -> Result<SourceFile, String> {
    if path != Path::new("-") {
        return read_source(path);
    }
    let mut text = String::new();
    io::stdin()
        .read_to_string(&mut text)
        .map_err(|error| format!("could not read UTF-8 source from stdin: {error}"))?;
    Ok(SourceFile::new("<stdin>", text))
}

fn report_load_failure(failure: LoadFailure, command: &str, machine: bool) -> u8 {
    match failure {
        LoadFailure::Io(message) => {
            eprintln!("error: {message}");
            USAGE_OR_IO_FAILURE
        }
        LoadFailure::Language {
            source,
            diagnostics,
        } => report_language(command, machine, &source, &diagnostics),
    }
}

fn report_language(
    command: &str,
    machine: bool,
    source: &SourceFile,
    diagnostics: &[Diagnostic],
) -> u8 {
    if machine {
        write_envelope(command, false, diagnostics, &JsonValue::Null)
    } else {
        render_diagnostics(diagnostics, source);
        LANGUAGE_FAILURE
    }
}

fn render_diagnostics(diagnostics: &[Diagnostic], source: &SourceFile) {
    for diagnostic in diagnostics {
        eprint!("{}", diagnostic.render(source));
    }
}

fn write_envelope(command: &str, ok: bool, diagnostics: &[Diagnostic], result: &JsonValue) -> u8 {
    let envelope = json!({
        "ok": ok,
        "command": command,
        "diagnostics": diagnostics,
        "result": result,
    });
    let text = match serde_json::to_string_pretty(&envelope) {
        Ok(text) => text,
        Err(error) => {
            eprintln!("error: could not encode JSON output: {error}");
            return USAGE_OR_IO_FAILURE;
        }
    };
    match write_stdout(&format!("{text}\n")) {
        Ok(()) if ok => SUCCESS,
        Ok(()) => LANGUAGE_FAILURE,
        Err(error) => report_io("write stdout", &error),
    }
}

pub(crate) fn stdout_supports_color() -> bool {
    matches!(
        anstream::AutoStream::choice(&io::stdout()),
        anstream::ColorChoice::Always | anstream::ColorChoice::AlwaysAnsi
    )
}

pub(crate) fn write_stdout(text: &str) -> io::Result<()> {
    let mut lock = anstream::AutoStream::auto(io::stdout()).lock();
    lock.write_all(text.as_bytes())?;
    lock.flush()
}

fn report_io(context: &str, error: &io::Error) -> u8 {
    eprintln!("error: could not {context}: {error}");
    USAGE_OR_IO_FAILURE
}

fn atomic_replace(path: &Path, contents: &[u8]) -> io::Result<()> {
    let parent = path.parent().unwrap_or_else(|| Path::new("."));
    let name = path
        .file_name()
        .and_then(|name| name.to_str())
        .unwrap_or("tess-source");
    let permissions = fs::metadata(path)
        .ok()
        .map(|metadata| metadata.permissions());
    for attempt in 0..100_u32 {
        let temporary = parent.join(format!(".{name}.tess-tmp-{}-{attempt}", std::process::id()));
        let mut file = match OpenOptions::new()
            .write(true)
            .create_new(true)
            .open(&temporary)
        {
            Ok(file) => file,
            Err(error) if error.kind() == io::ErrorKind::AlreadyExists => continue,
            Err(error) => return Err(error),
        };
        let result = (|| {
            file.write_all(contents)?;
            if let Some(permissions) = &permissions {
                file.set_permissions(permissions.clone())?;
            }
            file.sync_all()?;
            drop(file);
            fs::rename(&temporary, path)
        })();
        if result.is_err() {
            let _ = fs::remove_file(&temporary);
        }
        return result;
    }
    Err(io::Error::new(
        io::ErrorKind::AlreadyExists,
        "could not allocate a temporary file",
    ))
}

fn positive_usize(value: &str) -> Result<usize, String> {
    let value = match tess::parse_numeric_literal(value) {
        Some(NumericLiteral::Int(value)) => {
            usize::try_from(value).map_err(|_| "must be a positive integer".to_owned())?
        }
        Some(NumericLiteral::Decimal(_)) | None => {
            return Err("must be a positive integer".to_owned());
        }
    };
    if value == 0 {
        Err("must be greater than zero".to_owned())
    } else {
        Ok(value)
    }
}