Iter 18c.2: linearity check + suggested_rewrites
Adds a per-fn linearity check that runs on every fn whose param_modes are all explicit (Borrow or Own, no Implicit), tracks each binder's consume/borrow state through the AST, and emits two diagnostics with form-A `suggested_rewrites`: - `use-after-consume` — a binder is referenced after it has already been consumed. - `consume-while-borrowed` — a binder is consumed while a borrow of it is still live (sibling arg slot, or an enclosing-fn Borrow param). Fns with any Implicit param skip the check entirely; that's the back-compat lane that keeps every existing fixture green. Pure diagnostic addition: no IR change, no codegen change, no runtime change. Each diagnostic carries a non-empty `suggested_rewrites` whose `replacement` is form-A AILang text (typically `(clone <name>)`). Adds two new public entrypoints to ailang-surface — `parse_term` and `term_to_form_a` — so the round-trip `parse_term(term_to_form_a(t)) ≡ t` is the contract every emitted replacement must satisfy. Tests assert the contract. Linearity pass runs only on modules that typechecked clean (any upstream typecheck error suppresses it for that module — running on partly-defined IR would produce noise). Tests: 3 unit tests in `linearity::tests`, 3 integration tests in `ailang-check/tests/workspace.rs`, 1 serialisation test in `diagnostic.rs`. `cargo test --workspace` green.
This commit is contained in:
@@ -8,6 +8,28 @@ use ailang_check::{check_workspace, Severity};
|
||||
use ailang_core::load_workspace;
|
||||
use std::path::Path;
|
||||
|
||||
/// Iter 18c.2: assert that the linearity check's `suggested_rewrites`
|
||||
/// payload is non-empty AND each `replacement` parses as a form-A AILang
|
||||
/// term. This is the contract the check promises to consumers of
|
||||
/// `ail check --json`: a machine can take the replacement string and
|
||||
/// substitute it back into the source without re-tokenising the term.
|
||||
fn assert_suggested_rewrites_well_formed(d: &ailang_check::Diagnostic) {
|
||||
assert!(
|
||||
!d.suggested_rewrites.is_empty(),
|
||||
"diagnostic {} (def={:?}) has no suggested_rewrites",
|
||||
d.code,
|
||||
d.def
|
||||
);
|
||||
for r in &d.suggested_rewrites {
|
||||
ailang_surface::parse_term(&r.replacement).unwrap_or_else(|e| {
|
||||
panic!(
|
||||
"suggested rewrite for `{}` does not parse as form-A AILang: {:?}\nreplacement: {}",
|
||||
d.code, e, r.replacement
|
||||
)
|
||||
});
|
||||
}
|
||||
}
|
||||
|
||||
fn examples_dir() -> std::path::PathBuf {
|
||||
let manifest = env!("CARGO_MANIFEST_DIR");
|
||||
Path::new(manifest).parent().unwrap().parent().unwrap().join("examples")
|
||||
@@ -173,3 +195,243 @@ fn body_errors_accumulate_across_defs() {
|
||||
assert!(defs.contains(&"bad_a"), "missing bad_a; got {defs:?}");
|
||||
assert!(defs.contains(&"bad_b"), "missing bad_b; got {defs:?}");
|
||||
}
|
||||
|
||||
/// Iter 18c.2: a fn with all-explicit modes that consumes its
|
||||
/// `(own (con List))` parameter twice should trigger
|
||||
/// `use-after-consume` on the second occurrence and ship a
|
||||
/// non-empty, well-formed `suggested_rewrites`.
|
||||
///
|
||||
/// Body:
|
||||
/// `(seq (app sum_list xs) (app sum_list xs))`
|
||||
///
|
||||
/// Both `xs` are in Own arg position; the second use is after consume.
|
||||
#[test]
|
||||
fn use_after_consume_on_own_param_is_reported() {
|
||||
use ailang_core::ast::*;
|
||||
use std::collections::BTreeMap;
|
||||
|
||||
// Helper: a fn that consumes a (con List) and returns Int.
|
||||
let sum_list = Def::Fn(FnDef {
|
||||
name: "sum_list".into(),
|
||||
ty: Type::Fn {
|
||||
params: vec![Type::Con { name: "List".into(), args: vec![] }],
|
||||
param_modes: vec![ParamMode::Own],
|
||||
ret: Box::new(Type::int()),
|
||||
ret_mode: ParamMode::Implicit,
|
||||
effects: vec![],
|
||||
},
|
||||
params: vec!["ys".into()],
|
||||
body: Term::Lit { lit: Literal::Int { value: 0 } },
|
||||
doc: None,
|
||||
});
|
||||
|
||||
// The offending fn. Body is `(+ (sum_list xs) (sum_list xs))` — both
|
||||
// arg slots of `+` are Implicit/Consume, so `xs` is consumed twice
|
||||
// without intervening clone. The second occurrence triggers
|
||||
// `use-after-consume`. (Using `+` rather than `Seq` keeps the
|
||||
// function's return-type Int, which matches its declared signature.)
|
||||
let bad = Def::Fn(FnDef {
|
||||
name: "bad".into(),
|
||||
ty: Type::Fn {
|
||||
params: vec![Type::Con { name: "List".into(), args: vec![] }],
|
||||
param_modes: vec![ParamMode::Own],
|
||||
ret: Box::new(Type::int()),
|
||||
ret_mode: ParamMode::Implicit,
|
||||
effects: vec![],
|
||||
},
|
||||
params: vec!["xs".into()],
|
||||
body: Term::App {
|
||||
callee: Box::new(Term::Var { name: "+".into() }),
|
||||
args: vec![
|
||||
Term::App {
|
||||
callee: Box::new(Term::Var { name: "sum_list".into() }),
|
||||
args: vec![Term::Var { name: "xs".into() }],
|
||||
tail: false,
|
||||
},
|
||||
Term::App {
|
||||
callee: Box::new(Term::Var { name: "sum_list".into() }),
|
||||
args: vec![Term::Var { name: "xs".into() }],
|
||||
tail: false,
|
||||
},
|
||||
],
|
||||
tail: false,
|
||||
},
|
||||
doc: None,
|
||||
});
|
||||
|
||||
// List ADT (referenced by both fn types via `Type::Con`); a real
|
||||
// module needs the type to be in-scope for `check_type_well_formed`.
|
||||
let list_adt = Def::Type(TypeDef {
|
||||
name: "List".into(),
|
||||
vars: vec![],
|
||||
ctors: vec![Ctor {
|
||||
name: "Nil".into(),
|
||||
fields: vec![],
|
||||
}],
|
||||
doc: None,
|
||||
});
|
||||
|
||||
let m = Module {
|
||||
schema: ailang_core::SCHEMA.into(),
|
||||
name: "lin_uac".into(),
|
||||
imports: vec![],
|
||||
defs: vec![list_adt, sum_list, bad],
|
||||
};
|
||||
let mut modules = BTreeMap::new();
|
||||
modules.insert(m.name.clone(), m.clone());
|
||||
let ws = ailang_core::Workspace {
|
||||
entry: m.name.clone(),
|
||||
modules,
|
||||
root_dir: std::path::PathBuf::from("."),
|
||||
};
|
||||
let diags = check_workspace(&ws);
|
||||
|
||||
let lin: Vec<&ailang_check::Diagnostic> = diags
|
||||
.iter()
|
||||
.filter(|d| d.code == "use-after-consume")
|
||||
.collect();
|
||||
assert_eq!(
|
||||
lin.len(),
|
||||
1,
|
||||
"want exactly one use-after-consume; got: {:#?}",
|
||||
diags
|
||||
);
|
||||
let d = lin[0];
|
||||
assert!(matches!(d.severity, Severity::Error));
|
||||
assert_eq!(d.def.as_deref(), Some("bad"));
|
||||
assert_eq!(
|
||||
d.ctx.get("binder").and_then(|v| v.as_str()),
|
||||
Some("xs"),
|
||||
"ctx should name the offending binder; got {:?}",
|
||||
d.ctx
|
||||
);
|
||||
assert_suggested_rewrites_well_formed(d);
|
||||
}
|
||||
|
||||
/// Iter 18c.2: a fn whose body passes `xs` to a `Borrow` arg and then,
|
||||
/// in a SIBLING arg slot of the same call, consumes it via an `Own`
|
||||
/// arg, should trigger `consume-while-borrowed`.
|
||||
///
|
||||
/// Body:
|
||||
/// `(app dual_fn xs xs)`
|
||||
/// where `dual_fn` has param_modes = [Borrow, Own].
|
||||
#[test]
|
||||
fn consume_while_borrowed_in_sibling_arg_is_reported() {
|
||||
use ailang_core::ast::*;
|
||||
use std::collections::BTreeMap;
|
||||
|
||||
let list_adt = Def::Type(TypeDef {
|
||||
name: "List".into(),
|
||||
vars: vec![],
|
||||
ctors: vec![Ctor {
|
||||
name: "Nil".into(),
|
||||
fields: vec![],
|
||||
}],
|
||||
doc: None,
|
||||
});
|
||||
|
||||
// dual_fn: (borrow List) → (own List) → Int.
|
||||
let dual_fn = Def::Fn(FnDef {
|
||||
name: "dual_fn".into(),
|
||||
ty: Type::Fn {
|
||||
params: vec![
|
||||
Type::Con { name: "List".into(), args: vec![] },
|
||||
Type::Con { name: "List".into(), args: vec![] },
|
||||
],
|
||||
param_modes: vec![ParamMode::Borrow, ParamMode::Own],
|
||||
ret: Box::new(Type::int()),
|
||||
ret_mode: ParamMode::Implicit,
|
||||
effects: vec![],
|
||||
},
|
||||
params: vec!["a".into(), "b".into()],
|
||||
body: Term::Lit { lit: Literal::Int { value: 0 } },
|
||||
doc: None,
|
||||
});
|
||||
|
||||
let bad = Def::Fn(FnDef {
|
||||
name: "bad".into(),
|
||||
ty: Type::Fn {
|
||||
params: vec![Type::Con { name: "List".into(), args: vec![] }],
|
||||
param_modes: vec![ParamMode::Own],
|
||||
ret: Box::new(Type::int()),
|
||||
ret_mode: ParamMode::Implicit,
|
||||
effects: vec![],
|
||||
},
|
||||
params: vec!["xs".into()],
|
||||
body: Term::App {
|
||||
callee: Box::new(Term::Var { name: "dual_fn".into() }),
|
||||
args: vec![
|
||||
Term::Var { name: "xs".into() },
|
||||
Term::Var { name: "xs".into() },
|
||||
],
|
||||
tail: false,
|
||||
},
|
||||
doc: None,
|
||||
});
|
||||
|
||||
let m = Module {
|
||||
schema: ailang_core::SCHEMA.into(),
|
||||
name: "lin_cwb".into(),
|
||||
imports: vec![],
|
||||
defs: vec![list_adt, dual_fn, bad],
|
||||
};
|
||||
let mut modules = BTreeMap::new();
|
||||
modules.insert(m.name.clone(), m.clone());
|
||||
let ws = ailang_core::Workspace {
|
||||
entry: m.name.clone(),
|
||||
modules,
|
||||
root_dir: std::path::PathBuf::from("."),
|
||||
};
|
||||
let diags = check_workspace(&ws);
|
||||
|
||||
let lin: Vec<&ailang_check::Diagnostic> = diags
|
||||
.iter()
|
||||
.filter(|d| d.code == "consume-while-borrowed")
|
||||
.collect();
|
||||
assert_eq!(
|
||||
lin.len(),
|
||||
1,
|
||||
"want exactly one consume-while-borrowed; got: {:#?}",
|
||||
diags
|
||||
);
|
||||
let d = lin[0];
|
||||
assert!(matches!(d.severity, Severity::Error));
|
||||
assert_eq!(d.def.as_deref(), Some("bad"));
|
||||
assert_eq!(
|
||||
d.ctx.get("binder").and_then(|v| v.as_str()),
|
||||
Some("xs"),
|
||||
"ctx should name the offending binder; got {:?}",
|
||||
d.ctx
|
||||
);
|
||||
assert_suggested_rewrites_well_formed(d);
|
||||
}
|
||||
|
||||
/// Iter 18c.2: positive control. The ON-DISK `borrow_own_demo` fixture
|
||||
/// (the only currently-shipping all-explicit-mode program) must remain
|
||||
/// linearity-clean. If this regresses, the check has become incorrect:
|
||||
/// `borrow_own_demo`'s `list_length` (borrow) and `sum_list` (own)
|
||||
/// are exactly the canonical accept shape.
|
||||
#[test]
|
||||
fn borrow_own_demo_is_linearity_clean() {
|
||||
let entry = examples_dir().join("borrow_own_demo.ail.json");
|
||||
let ws = load_workspace(&entry).expect("load borrow_own_demo");
|
||||
let diags = check_workspace(&ws);
|
||||
let lin: Vec<&ailang_check::Diagnostic> = diags
|
||||
.iter()
|
||||
.filter(|d| {
|
||||
d.code == "use-after-consume" || d.code == "consume-while-borrowed"
|
||||
})
|
||||
.collect();
|
||||
assert!(
|
||||
lin.is_empty(),
|
||||
"borrow_own_demo must stay linearity-clean; got: {:#?}",
|
||||
lin
|
||||
);
|
||||
// Belt-and-braces: the *whole* check should be clean too — modes
|
||||
// are still metadata-only at the typechecker level (Iter 18a).
|
||||
assert!(
|
||||
diags.is_empty(),
|
||||
"borrow_own_demo must check clean; got: {:#?}",
|
||||
diags
|
||||
);
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user