use std::collections::HashMap;
use serde_json::json;
use tower_lsp_server::ls_types::{CodeLens, Command, Position, Range};
use aver::ast::{DecisionImpact, TopLevel, TypeDef, VerifyKind};
fn impact_matches_fn(impact_symbol: &str, fn_name: &str) -> bool {
impact_symbol == fn_name
|| impact_symbol
.rsplit('.')
.next()
.is_some_and(|suffix| suffix == fn_name)
}
use aver::checker::{index_decisions, merge_verify_blocks};
use aver::types::checker::run_type_check_full;
use aver::verify_law::canonical_spec_ref;
use crate::completion;
const OPEN_LOCATION_COMMAND: &str = "aver.openLocation";
pub fn code_lenses(source: &str, base_dir: Option<&str>, uri: &str) -> Vec<CodeLens> {
let items = completion::parse_items(source);
if items.is_empty() {
return Vec::new();
}
let tc_result = run_type_check_full(&items, base_dir);
let verify_by_fn: HashMap<String, Vec<_>> =
merge_verify_blocks(&items)
.into_iter()
.fold(HashMap::new(), |mut acc, vb| {
acc.entry(vb.fn_name.clone()).or_default().push(vb);
acc
});
let decisions = index_decisions(&items);
let mut lenses = Vec::new();
for item in &items {
match item {
TopLevel::FnDef(fd) => {
if let Some(blocks) = verify_by_fn.get(&fd.name) {
let case_count: usize = blocks
.iter()
.filter(|vb| matches!(vb.kind, VerifyKind::Cases))
.map(|vb| vb.cases.len())
.sum();
let laws: Vec<_> = blocks
.iter()
.filter_map(|vb| match &vb.kind {
VerifyKind::Law(law) => Some(law.as_ref()),
VerifyKind::Cases => None,
})
.collect();
let law_names: Vec<&str> = laws.iter().map(|law| law.name.as_str()).collect();
let spec_names = canonical_specs(&fd.name, &laws, &tc_result.fn_sigs);
let mut details = Vec::new();
if case_count > 0 {
details.push(format!("{} concrete case(s)", case_count));
}
if !law_names.is_empty() {
details.push(format!("laws: {}", law_names.join(", ")));
}
if !spec_names.is_empty() {
details.push(format!("specs: {}", spec_names.join(", ")));
}
let verify_line = blocks.iter().map(|vb| vb.line).min().unwrap_or(fd.line);
lenses.push(make_lens(
uri,
verify_line,
fd.line,
format!("verify: {}", summarize_counts(case_count, law_names.len())),
format!("{}()\n{}", fd.name, details.join("\n")),
));
}
let impacted_by: Vec<&str> = decisions
.iter()
.filter(|decision| {
decision.impacts.iter().any(
|impact| matches!(&impact.node, DecisionImpact::Symbol(symbol) if impact_matches_fn(symbol, &fd.name)),
)
})
.map(|decision| decision.name.as_str())
.collect();
if !impacted_by.is_empty() {
let decision_line = decisions
.iter()
.find(|decision| {
decision.impacts.iter().any(|impact| {
matches!(&impact.node, DecisionImpact::Symbol(symbol) if impact_matches_fn(symbol, &fd.name))
})
})
.map(|decision| decision.line)
.unwrap_or(fd.line);
lenses.push(make_lens(
uri,
decision_line,
fd.line,
format!("decisions: {}", impacted_by.len()),
format!("{}() is impacted by:\n{}", fd.name, impacted_by.join("\n")),
));
}
}
TopLevel::Decision(decision) => {
let impacts: Vec<&str> = decision.impacts.iter().map(|s| s.node.text()).collect();
let target_line = first_impact_line(&items, decision).unwrap_or(decision.line);
lenses.push(make_lens(
uri,
target_line,
decision.line,
format!("impacts: {}", impacts.len()),
format!(
"decision {}\nchosen: {}\nimpacts:\n{}",
decision.name,
decision.chosen.node.text(),
impacts.join("\n")
),
));
}
_ => {}
}
}
lenses
}
fn canonical_specs(
fn_name: &str,
laws: &[&aver::ast::VerifyLaw],
fn_sigs: &aver::verify_law::FnSigMap,
) -> Vec<String> {
let mut specs = Vec::new();
for law in laws {
if let Some(spec_ref) = canonical_spec_ref(fn_name, law, fn_sigs)
&& !specs.contains(&spec_ref.spec_fn_name)
{
specs.push(spec_ref.spec_fn_name);
}
}
specs
}
fn summarize_counts(case_count: usize, law_count: usize) -> String {
match (case_count, law_count) {
(0, 1) => "1 law".to_string(),
(0, n) => format!("{} laws", n),
(1, 0) => "1 case".to_string(),
(n, 0) => format!("{} cases", n),
(1, 1) => "1 case, 1 law".to_string(),
(1, n) => format!("1 case, {} laws", n),
(n, 1) => format!("{} cases, 1 law", n),
(n, m) => format!("{} cases, {} laws", n, m),
}
}
fn first_impact_line(items: &[TopLevel], decision: &aver::ast::DecisionBlock) -> Option<usize> {
for impact in &decision.impacts {
let DecisionImpact::Symbol(symbol) = &impact.node else {
continue;
};
for item in items {
match item {
TopLevel::FnDef(fd) if fd.name == *symbol => return Some(fd.line),
TopLevel::Decision(other) if other.name == *symbol => return Some(other.line),
TopLevel::Module(module) if module.name == *symbol => return Some(module.line),
TopLevel::TypeDef(TypeDef::Sum { name, line, .. }) if name == symbol => {
return Some(*line);
}
TopLevel::TypeDef(TypeDef::Product { name, line, .. }) if name == symbol => {
return Some(*line);
}
_ => {}
}
}
}
None
}
fn make_lens(
uri: &str,
target_line: usize,
line: usize,
title: String,
message: String,
) -> CodeLens {
let line = line.saturating_sub(1) as u32;
CodeLens {
range: Range {
start: Position { line, character: 0 },
end: Position { line, character: 0 },
},
command: Some(Command {
title,
command: OPEN_LOCATION_COMMAND.to_string(),
arguments: Some(vec![
json!(uri),
json!(target_line.saturating_sub(1)),
json!(message),
]),
}),
data: None,
}
}
#[cfg(test)]
mod tests {
use serde_json::json;
use super::code_lenses;
#[test]
fn code_lenses_cover_verify_and_decisions() {
let source = r#"module Demo
exposes [publicFn]
decision KeepCorePure
date = "2026-03-10"
reason =
"Keep orchestration explicit."
chosen = "PureCore"
rejected = ["ImpureCore"]
impacts = [publicFn]
fn publicFn(x: Int) -> Int
x + 1
fn publicFnSpec(x: Int) -> Int
x + 1
verify publicFn
publicFn(1) => 2
verify publicFn law publicFnSpec
given x: Int = 0..1
publicFn(x) => publicFnSpec(x)
"#;
let lenses = code_lenses(source, None, "file:///demo.av");
let titles: Vec<&str> = lenses
.iter()
.filter_map(|lens| lens.command.as_ref().map(|command| command.title.as_str()))
.collect();
assert!(titles.contains(&"verify: 1 case, 1 law"));
assert!(titles.contains(&"decisions: 1"));
assert!(titles.contains(&"impacts: 1"));
let verify = lenses
.iter()
.find(|lens| {
lens.command
.as_ref()
.is_some_and(|cmd| cmd.title == "verify: 1 case, 1 law")
})
.and_then(|lens| lens.command.as_ref())
.unwrap();
let args = verify.arguments.as_ref().unwrap();
assert_eq!(args[0], json!("file:///demo.av"));
assert_eq!(args[1], json!(17u64));
}
}