Iter 18d.1: Term::ReuseAs schema + linearity check
Schema floor for explicit reuse hints. Adds Term::ReuseAs
{ source: Box<Term>, body: Box<Term> } with serde tag "reuse-as",
form-A (reuse-as <source> <body>). Schema choice (wrapper, not
modifier-on-Ctor) and rationale recorded in DESIGN.md.
Codegen is identity under all --alloc strategies — lower body,
drop source on the floor. Iter 18d.2 will lower this as the
in-place rewrite under --alloc=rc.
User-facing diagnostics:
- typecheck reuse-as-non-allocating-body: body must be a
Term::Ctor or Term::Lam, the two AST shapes that allocate.
Other shapes (literal, var, app, ...) emit this with a
suggested_rewrite that drops the wrapper.
- linearity reuse-as-source-not-bare-var: source must be a
Term::Var referring to an in-scope binder. Anything else
(literal, nested expression) is rejected here. Suggested
rewrite drops the wrapper.
- linearity use-after-consume at a reuse-as site: source must
not have been consumed earlier in the body. Suggested rewrite
drops the wrapper.
- Visiting reuse-as marks source consumed for the rest of the
body, so a subsequent use of the same binder flags
use-after-consume against it.
Uniqueness inference treats source as Consume — the consume
shows up in the side table for the codegen consumer.
Tests:
- 4 surface parse-tests (round-trip, no-args, one-arg, full
parse_term/term_to_form_a round-trip).
- 1 typecheck unit test (non-allocating body).
- 2 linearity unit tests (non-var source, after-consume).
- 1 integration test (happy-path map_inc in all-explicit mode
is linearity-clean).
- 1 E2E test running the canonical map_inc-via-reuse-as fixture
under --alloc=gc, asserting stdout 9.
- New fixture examples/reuse_as_demo.{ailx,ail.json}.
Test deltas: E2E 55 -> 56, ailang-check unit 43 -> 46,
ailang-check workspace 8 -> 9, surface 14 -> 18. cargo test
--workspace green. No existing fixture's canonical JSON changed.
This commit is contained in:
@@ -406,6 +406,126 @@ fn consume_while_borrowed_in_sibling_arg_is_reported() {
|
||||
assert_suggested_rewrites_well_formed(d);
|
||||
}
|
||||
|
||||
/// Iter 18d.1: happy-path `(reuse-as xs (term-ctor List Cons ...))`
|
||||
/// inside an all-explicit-mode `map_inc`-style fn must produce NO
|
||||
/// diagnostics — neither `reuse-as-non-allocating-body` (body is a
|
||||
/// Ctor) nor `reuse-as-source-not-bare-var` (source is `xs`) nor
|
||||
/// `use-after-consume` (xs is matched then consumed once via
|
||||
/// reuse-as in the Cons arm; the merge across arms is consistent).
|
||||
///
|
||||
/// Body:
|
||||
/// `(match xs
|
||||
/// (case Nil (term-ctor List Nil))
|
||||
/// (case (Cons h t)
|
||||
/// (reuse-as xs (term-ctor List Cons (+ h 1) (app map_inc t)))))`
|
||||
#[test]
|
||||
fn reuse_as_happy_path_in_map_inc_is_linearity_clean() {
|
||||
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![] },
|
||||
Ctor {
|
||||
name: "Cons".into(),
|
||||
fields: vec![
|
||||
Type::Con { name: "Int".into(), args: vec![] },
|
||||
Type::Con { name: "List".into(), args: vec![] },
|
||||
],
|
||||
},
|
||||
],
|
||||
doc: None,
|
||||
});
|
||||
|
||||
let map_inc_ty = Type::Fn {
|
||||
params: vec![Type::Con { name: "List".into(), args: vec![] }],
|
||||
param_modes: vec![ParamMode::Own],
|
||||
ret: Box::new(Type::Con { name: "List".into(), args: vec![] }),
|
||||
ret_mode: ParamMode::Own,
|
||||
effects: vec![],
|
||||
};
|
||||
|
||||
// Cons arm body:
|
||||
// (reuse-as xs
|
||||
// (term-ctor List Cons (app + h 1) (app map_inc t)))
|
||||
let cons_arm_body = Term::ReuseAs {
|
||||
source: Box::new(Term::Var { name: "xs".into() }),
|
||||
body: Box::new(Term::Ctor {
|
||||
type_name: "List".into(),
|
||||
ctor: "Cons".into(),
|
||||
args: vec![
|
||||
Term::App {
|
||||
callee: Box::new(Term::Var { name: "+".into() }),
|
||||
args: vec![
|
||||
Term::Var { name: "h".into() },
|
||||
Term::Lit { lit: Literal::Int { value: 1 } },
|
||||
],
|
||||
tail: false,
|
||||
},
|
||||
Term::App {
|
||||
callee: Box::new(Term::Var { name: "map_inc".into() }),
|
||||
args: vec![Term::Var { name: "t".into() }],
|
||||
tail: false,
|
||||
},
|
||||
],
|
||||
}),
|
||||
};
|
||||
|
||||
let map_inc_body = Term::Match {
|
||||
scrutinee: Box::new(Term::Var { name: "xs".into() }),
|
||||
arms: vec![
|
||||
Arm {
|
||||
pat: Pattern::Ctor { ctor: "Nil".into(), fields: vec![] },
|
||||
body: Term::Ctor {
|
||||
type_name: "List".into(),
|
||||
ctor: "Nil".into(),
|
||||
args: vec![],
|
||||
},
|
||||
},
|
||||
Arm {
|
||||
pat: Pattern::Ctor {
|
||||
ctor: "Cons".into(),
|
||||
fields: vec![
|
||||
Pattern::Var { name: "h".into() },
|
||||
Pattern::Var { name: "t".into() },
|
||||
],
|
||||
},
|
||||
body: cons_arm_body,
|
||||
},
|
||||
],
|
||||
};
|
||||
|
||||
let map_inc = Def::Fn(FnDef {
|
||||
name: "map_inc".into(),
|
||||
ty: map_inc_ty,
|
||||
params: vec!["xs".into()],
|
||||
body: map_inc_body,
|
||||
doc: None,
|
||||
});
|
||||
|
||||
let m = Module {
|
||||
schema: ailang_core::SCHEMA.into(),
|
||||
name: "reuse_as_happy".into(),
|
||||
imports: vec![],
|
||||
defs: vec![list_adt, map_inc],
|
||||
};
|
||||
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);
|
||||
assert!(
|
||||
diags.is_empty(),
|
||||
"happy-path reuse-as must check clean; got: {:#?}",
|
||||
diags
|
||||
);
|
||||
}
|
||||
|
||||
/// 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:
|
||||
|
||||
Reference in New Issue
Block a user