aprender_contracts_cli/commands/
infer.rs

1use std::path::Path;
2
3use provable_contracts::infer::{
4    format_binding_entry, format_contract_stub, infer, ContractSuggestion, InferResult,
5    InferredBinding,
6};
7use provable_contracts::schema::{parse_contract, Contract};
8
9#[allow(clippy::unnecessary_wraps)]
10pub fn run(
11    crate_dir: &Path,
12    binding_path: &Path,
13    contract_dir: &Path,
14    top_n: usize,
15) -> Result<(), Box<dyn std::error::Error>> {
16    let contracts = load_contracts(contract_dir);
17    let refs: Vec<(String, &Contract)> = contracts.iter().map(|(s, c)| (s.clone(), c)).collect();
18
19    let result = infer(crate_dir, binding_path, &refs);
20
21    print_header(crate_dir, &contracts, &result);
22    print_matched(&result.matched, top_n);
23    print_suggestions(&result.suggestions, top_n);
24
25    if result.matched.is_empty() && result.suggestions.is_empty() {
26        println!("No inferences found. All non-trivial functions are bound.");
27    }
28
29    Ok(())
30}
31
32/// Load all `*.yaml` contracts under `contract_dir` (excluding binding files).
33fn load_contracts(contract_dir: &Path) -> Vec<(String, Contract)> {
34    let mut contracts = Vec::new();
35    let Ok(entries) = std::fs::read_dir(contract_dir) else {
36        return contracts;
37    };
38    for entry in entries.flatten() {
39        if let Some(loaded) = load_one_contract(&entry.path()) {
40            contracts.push(loaded);
41        }
42    }
43    contracts
44}
45
46fn load_one_contract(path: &Path) -> Option<(String, Contract)> {
47    if path.extension().and_then(|e| e.to_str()) != Some("yaml") {
48        return None;
49    }
50    if path.to_string_lossy().contains("binding") {
51        return None;
52    }
53    let stem = path
54        .file_stem()
55        .and_then(|s| s.to_str())
56        .unwrap_or("unknown")
57        .to_string();
58    parse_contract(path).ok().map(|c| (stem, c))
59}
60
61fn print_header(crate_dir: &Path, contracts: &[(String, Contract)], result: &InferResult) {
62    println!("pv infer — Contract Inference Engine");
63    println!("====================================\n");
64    println!(
65        "Crate: {} | Equations: {} | Unbound: {}",
66        crate_dir.display(),
67        contracts
68            .iter()
69            .map(|(_, c)| c.equations.len())
70            .sum::<usize>(),
71        result.coverage.unbound.len(),
72    );
73    println!(
74        "Reverse coverage: {:.1}% ({}/{})\n",
75        result.coverage.coverage_pct, result.coverage.bound_fns, result.coverage.total_pub_fns,
76    );
77}
78
79fn print_matched(matched: &[InferredBinding], top_n: usize) {
80    if matched.is_empty() {
81        return;
82    }
83    println!("=== Inferred Bindings ({}) ===\n", matched.len());
84    for (i, m) in matched.iter().take(top_n).enumerate() {
85        println!(
86            "[{}] {} → {}/{} ({:.0}%, {})",
87            i + 1,
88            m.function.path,
89            m.contract_stem,
90            m.equation,
91            m.confidence * 100.0,
92            m.strategy,
93        );
94        println!("    {}:{}", m.function.file, m.function.line);
95    }
96    if matched.len() > top_n {
97        println!("    ... and {} more", matched.len() - top_n);
98    }
99
100    println!("\n--- Suggested binding.yaml entries ---\n");
101    for m in matched.iter().take(top_n) {
102        println!("{}\n", format_binding_entry(m));
103    }
104}
105
106fn print_suggestions(suggestions: &[ContractSuggestion], top_n: usize) {
107    if suggestions.is_empty() {
108        return;
109    }
110    println!("=== New Contract Suggestions ({}) ===\n", suggestions.len());
111    for (i, s) in suggestions.iter().take(top_n).enumerate() {
112        println!(
113            "[{}] {} → {}.yaml (Tier {})",
114            i + 1,
115            s.function.path,
116            s.suggested_name,
117            s.suggested_tier,
118        );
119        println!("    {}:{}", s.function.file, s.function.line);
120        println!("    {}", s.reason);
121    }
122    if suggestions.len() > top_n {
123        println!("    ... and {} more", suggestions.len() - top_n);
124    }
125
126    println!("\n--- Sample contract stub ---\n");
127    println!("{}", format_contract_stub(&suggestions[0]));
128}
aprender_contracts_cli/commands/infer.rs

aprender_contracts_cli/commands/
infer.rs
