assura 0.4.0

Contract-first AI-native language. Write what it should do. AI proves it does.
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123

use std::io::{self, Read};
use std::path::Path;

use assura_config::{CompilerConfig, ProjectConfig};

/// Load `assura.toml` from the project root, if it exists.
pub(crate) fn load_project_config(
    start_path: &Path,
) -> Option<(ProjectConfig, std::path::PathBuf)> {
    assura_config::load_project_config(start_path, assura_resolve::find_project_root)
}

/// Read source from a path, or from stdin when `path` is `"-"`.
///
/// Display name for diagnostics is `"<stdin>"` when reading from stdin.
pub(crate) fn read_source_arg(path: &str) -> io::Result<(String, String)> {
    if path == "-" {
        let mut buf = String::new();
        io::stdin().read_to_string(&mut buf)?;
        Ok((buf, "<stdin>".to_string()))
    } else {
        let source = std::fs::read_to_string(path)?;
        Ok((source, path.to_string()))
    }
}

/// True when the path argument means standard input (`-`).
pub(crate) fn is_stdin_arg(path: &str) -> bool {
    path == "-"
}

/// Validate `--format` for subcommands that only support human/json.
///
/// When `as_json` is true (global `--json` or explicit `--format json`),
/// invalid values emit a JSON error object on stdout so agents stay pure.
pub(crate) fn validate_human_json_format(format: &str, cmd: &str, as_json: bool) {
    match format {
        "human" | "json" => {}
        other => {
            if as_json {
                let report = serde_json::json!({
                    "ok": false,
                    "command": cmd,
                    "error": "invalid_format",
                    "format": other,
                    "message": format!(
                        "invalid --format '{other}' for {cmd} (expected human or json)"
                    ),
                });
                println!("{}", serde_json::to_string_pretty(&report).unwrap());
            } else {
                eprintln!("Error: invalid --format '{other}' for {cmd} (expected human or json)");
            }
            std::process::exit(2);
        }
    }
}

/// Type alias: CLI code uses this name to destructure `CompilationOutput`.
pub(crate) type CompilationResult = assura_pipeline::CompilationOutput;

/// Format a counterexample as a clean single-line summary for diagnostics.
///
/// If a structured `CounterexampleModel` is available, produces a summary
/// like `"counterexample: a = -2, b = 1"`. Otherwise, parses the raw Z3
/// model string and formats it the same way.
pub(crate) fn format_counterexample_summary(
    counter_model: &Option<assura_smt::CounterexampleModel>,
    raw_model: &str,
) -> String {
    // Use the display module's formatting to get clean lines
    let lines = assura_smt::display::format_counterexample_lines(counter_model, raw_model);
    // Each line starts with "| "; strip that and join into a single line
    let pairs: Vec<&str> = lines
        .iter()
        .map(|l| l.strip_prefix("| ").unwrap_or(l.as_str()))
        .collect();
    if pairs.is_empty() {
        return "counterexample found".to_string();
    }
    format!("counterexample: {}", pairs.join("; "))
}

/// Discover the project root, load config, and build the dependency map.
///
/// Returns `(project_root, dep_map, dep_warnings)`. If no `assura.toml`
/// exists, `dep_map` is empty.
pub(crate) fn load_project_deps(
    project_dir: &Path,
) -> (
    std::path::PathBuf,
    assura_resolve::DependencyMap,
    Vec<String>,
) {
    let project_root = if project_dir.join("assura.toml").exists() {
        project_dir.to_path_buf()
    } else {
        assura_resolve::find_project_root(project_dir).unwrap_or_else(|| project_dir.to_path_buf())
    };

    let config = load_project_config(&project_root);
    let (dep_map, dep_warnings) = if let Some((ref cfg, ref root)) = config {
        assura_resolve::resolve_dependency_map(root, cfg)
    } else {
        (assura_resolve::DependencyMap::new(), vec![])
    };

    (project_root, dep_map, dep_warnings)
}

/// Run lex -> parse -> resolve -> typecheck on source text, collecting all diagnostics.
pub(crate) fn compile(source: &str, filename: &str) -> CompilationResult {
    assura_pipeline::compile(source, filename, &CompilerConfig::default())
}

/// Run the full pipeline with explicit configuration.
pub(crate) fn compile_with_config(
    source: &str,
    filename: &str,
    config: &CompilerConfig,
) -> CompilationResult {
    assura_pipeline::compile(source, filename, config)
}