use voltaic_ast::Program;
use voltaic_ast::Span;
use voltaic_lattice::Inferred;
use voltaic_lattice::Obligation;
use voltaic_diag::Code;
use voltaic_diag::Diagnostic;
use voltaic_diag::DiagnosticCode;
use voltaic_diag::Severity;
use std::path::Path;
pub fn judge(path: &Path, source: &str, program: &Program) -> Vec<Diagnostic> {
let shown = path.display().to_string();
let found = voltaic_lattice::walk(program);
let outcome = voltaic_lattice::solve_with(&found.store, &found.known);
let mut diagnostics = Vec::new();
for failure in outcome.contradictions(&found.store) {
if let Some(held) = found.store.at(failure.at) {
let owner = enclosing(found.definitions.as_slice(), held.provenance.span);
diagnostics.push(Diagnostic {
code: DiagnosticCode::from(Code::LatticeConflict),
severity: Severity::Warning,
message: stated(owner, &held.obligation, &outcome),
span: boundary(owner, held.provenance.span),
related: sides(
&found.store,
failure.at,
&held.obligation,
&outcome,
held.provenance.span,
),
help: Some(advice(owner, &held.provenance)),
path: shown.clone(),
source: source.to_string(),
});
}
}
diagnostics
}
fn enclosing(definitions: &[Inferred], at: Span) -> Option<&Inferred> {
let mut best: Option<&Inferred> = None;
for definition in definitions.iter() {
if definition.span.0 <= at.0 && at.1 <= definition.span.1 {
if let Some(held) = best {
if definition.span.1 - definition.span.0 < held.span.1 - held.span.0 {
best = Some(definition);
}
} else {
best = Some(definition);
}
}
}
best
}
fn boundary(owner: Option<&Inferred>, at: Span) -> Span {
if let Some(definition) = owner {
return definition.span;
}
at
}
fn stated(
owner: Option<&Inferred>,
obligation: &Obligation,
outcome: &voltaic_lattice::Outcome,
) -> String {
let named = if let Some(definition) = owner {
format!("`{}` ", definition.name)
} else {
String::new()
};
match obligation {
Obligation::Unify { left, right, .. } => format!(
"{}cannot be both {} and {}",
named,
outcome.resolved(left),
outcome.resolved(right)
),
_ => format!("{}{}", named, voltaic_lattice::summarise(obligation)),
}
}
fn sides(
store: &voltaic_lattice::Store,
at_index: usize,
obligation: &Obligation,
outcome: &voltaic_lattice::Outcome,
at: Span,
) -> Vec<(Span, String)> {
let mut found = Vec::new();
if let Obligation::Unify { left, right, .. } = obligation {
found.push((at, format!("required {} here", outcome.resolved(right))));
if let Some(other) = opposing(store, at_index) {
found.push((
other.0,
format!("inferred {} here, {}", outcome.resolved(left), other.1),
));
}
}
found
}
fn opposing(store: &voltaic_lattice::Store, at_index: usize) -> Option<(Span, String)> {
let failing = store.at(at_index)?;
let wanted = failing.holes();
for pair in store.all().iter().enumerate() {
if pair.0 == at_index {
continue;
}
if pair.1.provenance.span != failing.provenance.span && shares(&wanted, pair.1) {
return Some((
pair.1.provenance.span,
pair.1.provenance.reason.phrasing().to_string(),
));
}
}
None
}
fn shares(wanted: &[voltaic_lattice::Variable], candidate: &voltaic_lattice::Constraint) -> bool {
for hole in candidate.holes() {
if wanted.contains(&hole) {
return true;
}
}
false
}
fn advice(owner: Option<&Inferred>, provenance: &voltaic_lattice::Provenance) -> String {
let reason = provenance.reason.phrasing();
if let Some(definition) = owner {
format!(
"{}. Run `voltaic sig --why {}` for the constraint chain.",
reason, definition.name
)
} else {
format!(
"{}. Run `voltaic sig --why` for the constraint chain.",
reason
)
}
}
pub fn judgements(program: &Program) -> Vec<(String, String)> {
let found = voltaic_lattice::walk(program);
let outcome = voltaic_lattice::solve_with(&found.store, &found.known);
let mut shown = Vec::new();
for definition in found.definitions.iter() {
let resolved = definition.judged(&outcome);
let row = if definition.row.is_empty() {
String::new()
} else {
format!(" ! {}", definition.row)
};
shown.push((definition.name.clone(), format!("{}{}", resolved, row)));
}
shown
}
#[cfg(test)]
mod __vlt_tests {
use super::*;
#[test]
fn a_program_with_no_contradiction_gets_no_judgement_diagnostic() {
let source = "twice : u64 -> u64\ntwice n = n + n\n";
let program = voltaic_parser::parse_source(source).expect("should parse");
assert!(judge(Path::new("probe.vlt"), source, &program).is_empty());
}
#[test]
fn a_body_contradicting_its_signature_is_reported_as_a_warning_not_an_error() {
let source = "wrong : u64\nwrong = true\n";
let program = voltaic_parser::parse_source(source).expect("should parse");
let found = judge(Path::new("probe.vlt"), source, &program);
assert_eq!(found.len(), 1);
assert_eq!(
found[0].severity,
Severity::Warning,
"rustc is the authority; Lattice advises"
);
}
#[test]
fn a_judgement_names_the_enclosing_definition_in_its_message() {
let source = "wrong : u64\nwrong = true\n";
let program = voltaic_parser::parse_source(source).expect("should parse");
let found = judge(Path::new("probe.vlt"), source, &program);
assert!(found[0].message.contains("`wrong`"), "{}", found[0].message);
}
#[test]
fn a_judgement_is_reported_against_the_definition_s_span_not_the_constraint_s() {
let source = "wrong : u64\nwrong = true\n";
let program = voltaic_parser::parse_source(source).expect("should parse");
let tree = voltaic_lattice::walk(&program);
let definition = tree.find("wrong").expect("wrong");
let found = judge(Path::new("probe.vlt"), source, &program);
assert_eq!(found[0].span, definition.span);
}
#[test]
fn a_judgement_carries_two_spans_because_a_unification_failure_has_two_sides() {
let source = "wrong : u64\nwrong = true\n";
let program = voltaic_parser::parse_source(source).expect("should parse");
let found = judge(Path::new("probe.vlt"), source, &program);
assert_eq!(
found[0].related.len(),
2,
"one span makes inference feel arbitrary"
);
}
#[test]
fn the_two_spans_are_different_places_in_the_program() {
let source = "wrong : u64\nwrong = true\n";
let program = voltaic_parser::parse_source(source).expect("should parse");
let found = judge(Path::new("probe.vlt"), source, &program);
assert!(
found[0].related[0].0 != found[0].related[1].0,
"{:?}",
found[0].related
);
}
#[test]
fn neither_secondary_span_repeats_the_primary() {
let source = "wrong : u64\nwrong = true\n";
let program = voltaic_parser::parse_source(source).expect("should parse");
let found = judge(Path::new("probe.vlt"), source, &program);
for other in found[0].related.iter() {
assert!(
other.0 != found[0].span,
"a repeated snippet reads as two findings"
);
}
}
#[test]
fn the_help_names_the_definition_and_the_command_that_explains_it() {
let source = "wrong : u64\nwrong = true\n";
let program = voltaic_parser::parse_source(source).expect("should parse");
let found = judge(Path::new("probe.vlt"), source, &program);
let help = found[0].help.clone().expect("a help line");
assert!(help.contains("sig --why wrong"), "{}", help);
}
#[test]
fn judgements_are_reported_per_definition() {
let source = "twice : u64 -> u64\ntwice n = n + n\nthrice : u64 -> u64\nthrice n = n + n + n\n";
let program = voltaic_parser::parse_source(source).expect("should parse");
let named = judgements(&program);
assert_eq!(named.len(), 2);
assert_eq!(named[0].0, "twice");
assert_eq!(named[0].1, "u64 -> u64");
}
#[test]
fn the_innermost_enclosing_definition_wins_when_two_spans_nest() {
let source = "data Box = Box { side : f64 }\nouter : &Box -> f64\nouter b = b.side\ninner : &Box -> f64\ninner b = b.side\n";
let program = voltaic_parser::parse_source(source).expect("should parse");
let tree = voltaic_lattice::walk(&program);
let held = tree.find("inner").expect("inner");
assert_eq!(
enclosing(tree.definitions.as_slice(), held.span).map(|d| d.name.clone()),
Some("inner".to_string())
);
}
#[test]
fn a_span_inside_no_definition_has_no_enclosing_one() {
let program = voltaic_parser::parse_source("a : u64\na = 1\n").expect("should parse");
let tree = voltaic_lattice::walk(&program);
assert!(enclosing(tree.definitions.as_slice(), (9000, 9001)).is_none());
}
}