Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

iter prep.3-kernel-tier-modules (DONE 9/9): kernel-tier modules + param-in + stub crate — closes #33

Browse Source 
Terminal iteration of the kernel-extension-mechanics milestone. Ships
the four language-level mechanisms named in the spec's § Goal:
Module.kernel + TypeDef.param-in schema, their Form-A surface,
flag-driven kernel-tier auto-injection, and generic param-in checker
enforcement with a new diagnostic.

Schema (Tasks 1+2). Module gains a `kernel: bool` field
(skip_serializing_if = is_false), TypeDef gains a
`param_in: BTreeMap<String, BTreeSet<String>>` field
(skip-if-empty, kebab-renamed to "param-in"). Both fields are
strictly additive — every pre-existing fixture's canonical-JSON hash
is bit-stable except `prelude.ail`, which intentionally gains
`(kernel)`. The struct-literal sweep covered ~104 Module sites and
~35 TypeDef sites across the workspace; the additive serde-default
covers JSON deserialise paths, only Rust struct literals broke.

Form-A surface (Tasks 3+4). `(kernel)` is a bare module-header
attribute; `(param-in (a Int Float) (b Str))` is one outer
TypeDef-body clause carrying one or more inner var-lists (OQ1
decision — mirrors `(ctors …)`, one parser arm, deterministic
BTreeMap iteration). Both round-trip Form-A → JSON → Form-A
bit-identical.

Workspace-load migration (Task 5). The hardcoded `&["prelude"]`
literal at loader.rs:108 became a `modules.values().filter(|m|
m.kernel)` derivation; `parse_prelude()` injection stays because
the prelude has no on-disk manifest in user workspaces. Prelude
now carries `(kernel)` in its source, so the new filter picks it
up automatically. Code-path migration only — observable behaviour
is identical (prelude_free_fns.rs stays green). prelude hash
re-pinned (af372f28c726f29f) with Honesty-Rule provenance comment.
WorkspaceLoadError::ReservedModuleName diagnostic prose
repurposed: any built-in kernel module name is reserved
(currently prelude + kernel_stub), not specifically prelude. CLI
mapping at main.rs updated in lockstep.

Stub crate (Task 6). New `crates/ailang-kernel-stub/` is a
zero-dependency leaf crate carrying only `pub const STUB_AIL:
&str` with the Form-A source of the kernel_stub module (one
parametric TypeDef with param-in, one ctor). The parse hop —
`parse_kernel_stub()` — lives in ailang-surface next to
parse_prelude, keeping the crate-dependency graph acyclic
(`ailang-surface → ailang-kernel-stub → ailang-core`, no
back-edge). The stub is injected unconditionally in all builds as
the ratifying fixture for the kernel-extension mechanism; future
base extensions may add more or retire the stub. Drift-pinned by
`kernel_stub_module_round_trips`.

Checker (Task 7). New `CheckError::ParamNotInRestrictedSet`
variant + code() + ctx() arms + enforcement in
`check_type_well_formed`'s Type::Con arm — generic, data-driven
from the TypeDef, mentions no specific extension type. Two
in-source tests pin both the rejection (`Str` outside `{Int,
Float}`) and the acceptance (`Int` inside) paths.

Workspace-load integration tests (Task 8). New
`workspace_kernel.rs` integration-test crate with three tests:
auto-import without explicit `(import …)` declaration, two
kernel-tier modules co-load, explicit-import-overrides-auto-
import precedence preserved. Loader is import-tree-only so the
auto-import tests use a bridge module that brings the kernel
module into the workspace via the import graph — docstring
captures the reachability nuance for future readers.

Doc-state transitions (Task 9). INDEX.md kernel-extensions row
annotation transitions from "design accepted 2026-05-28; impl in
progress" to "mechanisms milestone closed 2026-05-28; raw-buf and
series milestones pending". Whitepaper STATUS + auto-import +
param-in sections transitioned forward→present for shipped
mechanisms; forward-tense survives only in sections describing
the still-pending raw-buf/series milestones (per Honesty-Rule).
data-model contract gains anchor blocks for both new schema
fields.

Side-effect: every binary's IR snapshot now contains ~52 lines
for `drop_kernel_stub_StubT` because the stub is auto-injected
into every workspace load. Snapshots refreshed; e2e expects 4
modules per workspace (prelude + kernel_stub + entry + zero or
more user modules) instead of the previous 3.

Plan defects scrubbed in the implementation (folded back into
the planner template via the planner's self-review checklist
next time): Task 4 sample test src used fictional
`(ctors (MkT a))` list form (project grammar is per-`(ctor MkT
a)`); Task 6 original wiring would have created a cycle
ailang-surface → ailang-kernel-stub → ailang-surface (inverted —
stub crate is zero-dep, parse hop lives in surface); Task 7 in-
source tests referenced a fictional `check_type_in_module`
helper (used the existing Workspace + check_workspace
convention); Task 8 first integration test expected loader to
auto-load kernel modules from disk (loader is import-tree-only;
tests use a bridge module).

Concern-5 fix folded in pre-commit: workspace.rs ReservedModuleName
doc-prose initially said "in test/dev builds" for kernel_stub —
but stub is unconditionally injected in all builds. Doc copy
tightened to present-state per Honesty-Rule.

Stats: 0 spec-review-loops, 0 quality-review-loops, 2 sweep-script
retries on Task 2 (brace-depth bug on nested vec![Ctor{…}],
recovered via per-file checkout + rewritten anchor-on-existing-
field sweep), 1 e2e-snapshot refresh on Task 6.
This commit is contained in:
Brummel
2026-05-28 18:43:42 +02:00
parent 3b4fb42771
commit 9339279181
38 changed files with 1185 additions and 47 deletions
Download Patch File Download Diff File Expand all files Collapse all files
Cargo.lock
Generated
+5
View File
@@ -54,6 +54,10 @@ dependencies = [
"thiserror",
]
[[package]]
name = "ailang-kernel-stub"
version = "0.0.1"
[[package]]
name = "ailang-prose"
version = "0.0.1"
@@ -67,6 +71,7 @@ name = "ailang-surface"
version = "0.0.1"
dependencies = [
"ailang-core",
"ailang-kernel-stub",
"serde_json",
"tempfile",
"thiserror",
Cargo.toml
+2
View File
@@ -4,6 +4,7 @@ members = [
"crates/ailang-core",
"crates/ailang-check",
"crates/ailang-codegen",
"crates/ailang-kernel-stub",
"crates/ailang-surface",
"crates/ailang-prose",
"crates/ail",
@@ -33,6 +34,7 @@ tempfile = "3"
ailang-core = { path = "crates/ailang-core" }
ailang-check = { path = "crates/ailang-check" }
ailang-codegen = { path = "crates/ailang-codegen" }
ailang-kernel-stub = { path = "crates/ailang-kernel-stub" }
ailang-surface = { path = "crates/ailang-surface" }
ailang-prose = { path = "crates/ailang-prose" }
crates/ail/src/main.rs
+9 -3
View File
@@ -546,6 +546,7 @@ fn main() -> Result<()> {
let one = ailang_core::Module {
schema: m.schema.clone(),
name: m.name.clone(),
kernel: false,
imports: vec![],
defs: vec![def.clone()],
};
@@ -569,6 +570,7 @@ fn main() -> Result<()> {
let one = ailang_core::Module {
schema: m.schema.clone(),
name: m.name.clone(),
kernel: false,
imports: vec![],
defs: vec![def.clone()],
};
@@ -1229,13 +1231,17 @@ fn workspace_error_to_diagnostic(
"type": type_repr,
})),
),
// the user named a module `prelude`, which the
// loader reserves for the auto-injected prelude module.
// the user named a module whose name collides with a
// built-in kernel-tier module that the loader auto-injects
// (e.g. `prelude`). Since prep.3 of the kernel-extension-
// mechanics milestone, the reserved set is derived from the
// kernel-tier filter; the diagnostic message generalises
// accordingly.
W::ReservedModuleName { name } => Some(
ailang_check::Diagnostic::error(
"reserved-module-name",
format!(
"module name {name:?} is reserved (auto-injected by the loader)"
"module `{name}` collides with a built-in kernel-tier module name (reserved)"
),
)
.with_ctx(serde_json::json!({
crates/ail/tests/e2e.rs
+6 -3
View File
@@ -850,9 +850,11 @@ fn workspace_lists_imported_modules() {
);
let modules = v["modules"].as_array().expect("modules must be array");
// the loader auto-injects the `prelude` module, so
// the count is the user's two modules plus prelude.
assert_eq!(modules.len(), 3, "expected 3 modules: {stdout}");
// the loader auto-injects every built-in kernel-tier module
// (`prelude` and, since prep.3 of the kernel-extension-mechanics
// milestone, the ratifying `kernel_stub`), so the count is the
// user's two modules plus the two built-ins.
assert_eq!(modules.len(), 4, "expected 4 modules: {stdout}");
let names: Vec<&str> = modules
.iter()
@@ -861,6 +863,7 @@ fn workspace_lists_imported_modules() {
assert!(names.contains(&"ws_main"), "ws_main missing: {names:?}");
assert!(names.contains(&"ws_lib"), "ws_lib missing: {names:?}");
assert!(names.contains(&"prelude"), "prelude missing: {names:?}");
assert!(names.contains(&"kernel_stub"), "kernel_stub missing: {names:?}");
}
/// Guards Iter 5b: `ail check examples/ws_main.ail.json --json` must
crates/ail/tests/snapshots/hello.ll
+52
View File
@@ -45,6 +45,58 @@ entry:
ret i8 %r
}
define void @drop_kernel_stub_StubT(ptr %p) {
entry:
%is_null = icmp eq ptr %p, null
br i1 %is_null, label %ret, label %live
live:
%tag = load i64, ptr %p, align 8
switch i64 %tag, label %dflt [
i64 0, label %arm_0
]
arm_0:
%a0 = getelementptr inbounds i8, ptr %p, i64 8
%v1 = load ptr, ptr %a0, align 8
call void @ailang_rc_dec(ptr %v1)
br label %join
dflt:
unreachable
join:
call void @ailang_rc_dec(ptr %p)
br label %ret
ret:
ret void
}
define void @partial_drop_kernel_stub_StubT(ptr %p, i64 %mask) {
entry:
%is_null = icmp eq ptr %p, null
br i1 %is_null, label %ret, label %live
live:
%tag = load i64, ptr %p, align 8
switch i64 %tag, label %dflt [
i64 0, label %arm_0
]
arm_0:
%b0 = and i64 %mask, 1
%s1 = icmp ne i64 %b0, 0
br i1 %s1, label %after_0_0, label %do_0_0
do_0_0:
%a2 = getelementptr inbounds i8, ptr %p, i64 8
%v3 = load ptr, ptr %a2, align 8
call void @ailang_rc_dec(ptr %v3)
br label %after_0_0
after_0_0:
br label %join
dflt:
unreachable
join:
call void @ailang_rc_dec(ptr %p)
br label %ret
ret:
ret void
}
define i1 @ail_prelude_float_eq(double %arg_x, double %arg_y) alwaysinline {
entry:
%v1 = fcmp oeq double %arg_x, %arg_y
crates/ail/tests/snapshots/list.ll
+52
View File
@@ -32,6 +32,58 @@ declare i64 @llvm.fptosi.sat.i64.f64(double)
@ail_prelude_float_ge_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_ge_adapter, ptr null }
@ail_prelude_show__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_show__Int_adapter, ptr null }
@ail_prelude_print__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_print__Int_adapter, ptr null }
define void @drop_kernel_stub_StubT(ptr %p) {
entry:
%is_null = icmp eq ptr %p, null
br i1 %is_null, label %ret, label %live
live:
%tag = load i64, ptr %p, align 8
switch i64 %tag, label %dflt [
i64 0, label %arm_0
]
arm_0:
%a0 = getelementptr inbounds i8, ptr %p, i64 8
%v1 = load ptr, ptr %a0, align 8
call void @ailang_rc_dec(ptr %v1)
br label %join
dflt:
unreachable
join:
call void @ailang_rc_dec(ptr %p)
br label %ret
ret:
ret void
}
define void @partial_drop_kernel_stub_StubT(ptr %p, i64 %mask) {
entry:
%is_null = icmp eq ptr %p, null
br i1 %is_null, label %ret, label %live
live:
%tag = load i64, ptr %p, align 8
switch i64 %tag, label %dflt [
i64 0, label %arm_0
]
arm_0:
%b0 = and i64 %mask, 1
%s1 = icmp ne i64 %b0, 0
br i1 %s1, label %after_0_0, label %do_0_0
do_0_0:
%a2 = getelementptr inbounds i8, ptr %p, i64 8
%v3 = load ptr, ptr %a2, align 8
call void @ailang_rc_dec(ptr %v3)
br label %after_0_0
after_0_0:
br label %join
dflt:
unreachable
join:
call void @ailang_rc_dec(ptr %p)
br label %ret
ret:
ret void
}
define i64 @ail_list_sum_list(ptr %arg_xs) {
entry:
%v1 = load i64, ptr %arg_xs, align 8
crates/ail/tests/snapshots/max3.ll
+52
View File
@@ -35,6 +35,58 @@ declare i64 @llvm.fptosi.sat.i64.f64(double)
@ail_prelude_gt__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_gt__Int_adapter, ptr null }
@ail_prelude_show__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_show__Int_adapter, ptr null }
@ail_prelude_print__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_print__Int_adapter, ptr null }
define void @drop_kernel_stub_StubT(ptr %p) {
entry:
%is_null = icmp eq ptr %p, null
br i1 %is_null, label %ret, label %live
live:
%tag = load i64, ptr %p, align 8
switch i64 %tag, label %dflt [
i64 0, label %arm_0
]
arm_0:
%a0 = getelementptr inbounds i8, ptr %p, i64 8
%v1 = load ptr, ptr %a0, align 8
call void @ailang_rc_dec(ptr %v1)
br label %join
dflt:
unreachable
join:
call void @ailang_rc_dec(ptr %p)
br label %ret
ret:
ret void
}
define void @partial_drop_kernel_stub_StubT(ptr %p, i64 %mask) {
entry:
%is_null = icmp eq ptr %p, null
br i1 %is_null, label %ret, label %live
live:
%tag = load i64, ptr %p, align 8
switch i64 %tag, label %dflt [
i64 0, label %arm_0
]
arm_0:
%b0 = and i64 %mask, 1
%s1 = icmp ne i64 %b0, 0
br i1 %s1, label %after_0_0, label %do_0_0
do_0_0:
%a2 = getelementptr inbounds i8, ptr %p, i64 8
%v3 = load ptr, ptr %a2, align 8
call void @ailang_rc_dec(ptr %v3)
br label %after_0_0
after_0_0:
br label %join
dflt:
unreachable
join:
call void @ailang_rc_dec(ptr %p)
br label %ret
ret:
ret void
}
define i64 @ail_max3_max(i64 %arg_a, i64 %arg_b) {
entry:
%v1 = call i1 @ail_prelude_gt__Int(i64 %arg_a, i64 %arg_b)
crates/ail/tests/snapshots/sum.ll
+52
View File
@@ -33,6 +33,58 @@ declare i64 @llvm.fptosi.sat.i64.f64(double)
@ail_prelude_print__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_print__Int_adapter, ptr null }
@ail_sum_sum_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_sum_sum_adapter, ptr null }
@ail_sum_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_sum_main_adapter, ptr null }
define void @drop_kernel_stub_StubT(ptr %p) {
entry:
%is_null = icmp eq ptr %p, null
br i1 %is_null, label %ret, label %live
live:
%tag = load i64, ptr %p, align 8
switch i64 %tag, label %dflt [
i64 0, label %arm_0
]
arm_0:
%a0 = getelementptr inbounds i8, ptr %p, i64 8
%v1 = load ptr, ptr %a0, align 8
call void @ailang_rc_dec(ptr %v1)
br label %join
dflt:
unreachable
join:
call void @ailang_rc_dec(ptr %p)
br label %ret
ret:
ret void
}
define void @partial_drop_kernel_stub_StubT(ptr %p, i64 %mask) {
entry:
%is_null = icmp eq ptr %p, null
br i1 %is_null, label %ret, label %live
live:
%tag = load i64, ptr %p, align 8
switch i64 %tag, label %dflt [
i64 0, label %arm_0
]
arm_0:
%b0 = and i64 %mask, 1
%s1 = icmp ne i64 %b0, 0
br i1 %s1, label %after_0_0, label %do_0_0
do_0_0:
%a2 = getelementptr inbounds i8, ptr %p, i64 8
%v3 = load ptr, ptr %a2, align 8
call void @ailang_rc_dec(ptr %v3)
br label %after_0_0
after_0_0:
br label %join
dflt:
unreachable
join:
call void @ailang_rc_dec(ptr %p)
br label %ret
ret:
ret void
}
define i1 @ail_prelude_float_eq(double %arg_x, double %arg_y) alwaysinline {
entry:
%v1 = fcmp oeq double %arg_x, %arg_y
crates/ail/tests/snapshots/ws_main.ll
+52
View File
@@ -32,6 +32,58 @@ declare i64 @llvm.fptosi.sat.i64.f64(double)
@ail_prelude_print__Int_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_print__Int_adapter, ptr null }
@ail_ws_lib_add_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_ws_lib_add_adapter, ptr null }
@ail_ws_main_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_ws_main_main_adapter, ptr null }
define void @drop_kernel_stub_StubT(ptr %p) {
entry:
%is_null = icmp eq ptr %p, null
br i1 %is_null, label %ret, label %live
live:
%tag = load i64, ptr %p, align 8
switch i64 %tag, label %dflt [
i64 0, label %arm_0
]
arm_0:
%a0 = getelementptr inbounds i8, ptr %p, i64 8
%v1 = load ptr, ptr %a0, align 8
call void @ailang_rc_dec(ptr %v1)
br label %join
dflt:
unreachable
join:
call void @ailang_rc_dec(ptr %p)
br label %ret
ret:
ret void
}
define void @partial_drop_kernel_stub_StubT(ptr %p, i64 %mask) {
entry:
%is_null = icmp eq ptr %p, null
br i1 %is_null, label %ret, label %live
live:
%tag = load i64, ptr %p, align 8
switch i64 %tag, label %dflt [
i64 0, label %arm_0
]
arm_0:
%b0 = and i64 %mask, 1
%s1 = icmp ne i64 %b0, 0
br i1 %s1, label %after_0_0, label %do_0_0
do_0_0:
%a2 = getelementptr inbounds i8, ptr %p, i64 8
%v3 = load ptr, ptr %a2, align 8
call void @ailang_rc_dec(ptr %v3)
br label %after_0_0
after_0_0:
br label %join
dflt:
unreachable
join:
call void @ailang_rc_dec(ptr %p)
br label %ret
ret:
ret void
}
define i1 @ail_prelude_float_eq(double %arg_x, double %arg_y) alwaysinline {
entry:
%v1 = fcmp oeq double %arg_x, %arg_y
crates/ailang-check/src/lib.rs
+188
View File
@@ -737,6 +737,24 @@ pub enum CheckError {
got: &'static str,
},
/// prep.3 (kernel-extension-mechanics): `param-in` violation. A
/// `Type::Con` for a TypeDef that restricts a type variable was
/// instantiated with a type-arg outside the allowed set. The
/// diagnostic carries the TypeDef name (which TypeDef
/// restricts), the variable name (which var was violated), the
/// rejected concrete type name (`found`), and the allowed set
/// (`allowed`, deterministically alphabetical from the BTreeSet
/// source). Code: `param-not-in-restricted-set`.
#[error(
"type-arg `{found}` is not in the restricted set for type-variable `{var}` of `{type_name}`"
)]
ParamNotInRestrictedSet {
type_name: String,
var: String,
found: String,
allowed: Vec<String>,
},
/// an internal invariant in the typechecker / mono pass
/// was violated — surfaced as an error so callers can propagate
/// rather than abort, but in well-formed inputs (typecheck has
@@ -796,6 +814,7 @@ impl CheckError {
CheckError::TypeScopedReceiverNotAType { .. } => "type-scoped-receiver-not-a-type",
CheckError::NewTypeNotConstructible { .. } => "new-type-not-constructible",
CheckError::NewArgKindMismatch { .. } => "new-arg-kind-mismatch",
CheckError::ParamNotInRestrictedSet { .. } => "param-not-in-restricted-set",
CheckError::Internal(_) => "internal",
}
}
@@ -884,6 +903,14 @@ impl CheckError {
"actual": got,
})
}
CheckError::ParamNotInRestrictedSet { type_name, var, found, allowed } => {
serde_json::json!({
"type": type_name,
"var": var,
"found": found,
"allowed": allowed,
})
}
_ => serde_json::Value::Object(serde_json::Map::new()),
}
}
@@ -1966,6 +1993,30 @@ fn check_type_well_formed(t: &Type, env: &Env) -> Result<()> {
args.len()
)));
}
// prep.3 (kernel-extension-mechanics): `param-in`
// enforcement. Every restricted var must have its
// corresponding positional arg's outermost type-name
// in the allowed set. Non-Con arg-types (vars, fn
// types, etc.) are not currently restrictable — the
// spec scopes `param-in` to closed-set named types.
for (var, allowed) in &td.param_in {
let Some(pos) = td.vars.iter().position(|v| v == var) else {
continue;
};
let Some(arg_ty) = args.get(pos) else {
continue;
};
if let Type::Con { name: arg_name, .. } = arg_ty {
if !allowed.contains(arg_name) {
return Err(CheckError::ParamNotInRestrictedSet {
type_name: name.clone(),
var: var.clone(),
found: arg_name.clone(),
allowed: allowed.iter().cloned().collect(),
});
}
}
}
for a in args {
check_type_well_formed(a, env)?;
}
@@ -4942,6 +4993,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"add",
@@ -4971,6 +5023,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"bad",
@@ -4997,6 +5050,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"leaks",
@@ -5029,6 +5083,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"f",
@@ -5058,6 +5113,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Type(TypeDef {
@@ -5072,6 +5128,7 @@ mod tests {
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
}),
fn_def(
"f",
@@ -5109,6 +5166,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Type(TypeDef {
@@ -5123,6 +5181,7 @@ mod tests {
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
}),
fn_def(
"f",
@@ -5165,6 +5224,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"f",
@@ -5199,6 +5259,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"id",
@@ -5279,6 +5340,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![id_def, use_int, use_bool],
};
@@ -5326,6 +5388,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![id_def, bad],
};
@@ -5410,6 +5473,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![apply_def, succ, use_apply],
};
@@ -5429,6 +5493,7 @@ mod tests {
}],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
});
// fn make :: () -> Box<Int> = MkBox(42)
let make = fn_def(
@@ -5453,6 +5518,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![box_def, make],
};
@@ -5472,6 +5538,7 @@ mod tests {
}],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
});
let unbox = Def::Fn(FnDef {
name: "unbox".into(),
@@ -5549,6 +5616,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![box_def, unbox, use_int, use_bool],
};
@@ -5568,6 +5636,7 @@ mod tests {
}],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
});
let bad = fn_def(
"bad",
@@ -5587,6 +5656,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![box_def, bad],
};
@@ -5603,6 +5673,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"f",
@@ -5638,6 +5709,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Type(TypeDef {
@@ -5655,6 +5727,7 @@ mod tests {
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
}),
fn_def(
"loop",
@@ -5695,6 +5768,7 @@ mod tests {
let lib = Module {
schema: SCHEMA.into(),
name: "lib".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Type(TypeDef {
name: "Box".into(),
@@ -5705,6 +5779,7 @@ mod tests {
}],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
})],
};
let mut modules = BTreeMap::new();
@@ -5725,6 +5800,7 @@ mod tests {
let consumer = Module {
schema: SCHEMA.into(),
name: "use_lib".into(),
kernel: false,
imports: vec![Import { module: "lib".into(), alias: None }],
defs: vec![fn_def(
"noop",
@@ -5754,6 +5830,7 @@ mod tests {
let consumer = Module {
schema: SCHEMA.into(),
name: "use_lib".into(),
kernel: false,
imports: vec![Import { module: "lib".into(), alias: None }],
defs: vec![fn_def(
"make",
@@ -5790,6 +5867,7 @@ mod tests {
let consumer = Module {
schema: SCHEMA.into(),
name: "use_lib".into(),
kernel: false,
imports: vec![Import { module: "lib".into(), alias: None }],
defs: vec![fn_def(
"open",
@@ -5837,6 +5915,7 @@ mod tests {
let lib = Module {
schema: SCHEMA.into(),
name: "lst".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Type(TypeDef {
name: "List".into(),
@@ -5856,6 +5935,7 @@ mod tests {
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
})],
};
// Consumer: builds `Cons 1 (Cons 2 (Nil))` via qualified
@@ -5877,6 +5957,7 @@ mod tests {
let consumer = Module {
schema: SCHEMA.into(),
name: "uses_lst".into(),
kernel: false,
imports: vec![Import { module: "lst".into(), alias: None }],
defs: vec![fn_def(
"head_or_zero",
@@ -5942,6 +6023,7 @@ mod tests {
let prelude = Module {
schema: SCHEMA.into(),
name: "p".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Type(TypeDef {
@@ -5954,6 +6036,7 @@ mod tests {
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
}),
Def::Class(ClassDef {
name: "Ord".into(),
@@ -6015,6 +6098,7 @@ mod tests {
let consumer = Module {
schema: SCHEMA.into(),
name: "u".into(),
kernel: false,
imports: vec![Import { module: "p".into(), alias: None }],
defs: vec![fn_def(
"use_compare",
@@ -6101,6 +6185,7 @@ mod tests {
ctors: vec![Ctor { name: "MkFoo".into(), fields: vec![] }],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
});
let input = Type::Forall {
vars: vec!["a".into()],
@@ -6140,6 +6225,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Type(TypeDef {
@@ -6157,6 +6243,7 @@ mod tests {
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
}),
fn_def(
"drain",
@@ -6288,6 +6375,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"outer",
@@ -6323,6 +6411,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"outer",
@@ -6450,6 +6539,7 @@ mod tests {
}],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
};
let letrec = Term::LetRec {
name: "helper".into(),
@@ -6491,6 +6581,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Type(pair_td),
@@ -6583,6 +6674,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"f",
@@ -6644,6 +6736,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"classify",
@@ -6691,6 +6784,7 @@ mod tests {
let lib = Module {
schema: SCHEMA.into(),
name: "lib".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Type(TypeDef {
name: "Box".into(),
@@ -6701,11 +6795,13 @@ mod tests {
}],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
})],
};
let consumer = Module {
schema: SCHEMA.into(),
name: "use_lib".into(),
kernel: false,
imports: vec![Import { module: "lib".into(), alias: None }],
defs: vec![fn_def(
"open",
@@ -6755,6 +6851,7 @@ mod tests {
let consumer = Module {
schema: SCHEMA.into(),
name: "u".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"f",
@@ -6811,6 +6908,7 @@ mod tests {
let consumer = Module {
schema: SCHEMA.into(),
name: "u".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"stale",
@@ -6858,6 +6956,7 @@ mod tests {
let owner = Module {
schema: SCHEMA.into(),
name: "p".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Type(TypeDef {
name: "Ordering".into(),
@@ -6869,11 +6968,13 @@ mod tests {
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
})],
};
let consumer = Module {
schema: SCHEMA.into(),
name: "u".into(),
kernel: false,
imports: vec![Import { module: "p".into(), alias: None }],
defs: vec![fn_def(
"f",
@@ -6920,6 +7021,7 @@ mod tests {
let prelude = Module {
schema: SCHEMA.into(),
name: "p".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Type(TypeDef {
name: "Ordering".into(),
@@ -6931,11 +7033,13 @@ mod tests {
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
})],
};
let consumer = Module {
schema: SCHEMA.into(),
name: "u".into(),
kernel: false,
imports: vec![Import { module: "p".into(), alias: None }],
defs: vec![fn_def(
"lt",
@@ -6982,6 +7086,7 @@ mod tests {
let prelude = Module {
schema: SCHEMA.into(),
name: "prelude".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"dbl",
@@ -6999,6 +7104,7 @@ mod tests {
let consumer = Module {
schema: SCHEMA.into(),
name: "m".into(),
kernel: false,
imports: vec![],
defs: vec![fn_def(
"main",
@@ -7244,6 +7350,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "m".to_string(),
kernel: false,
imports: vec![],
defs: vec![Def::Class(ClassDef {
name: "MyShow".to_string(),
@@ -7310,6 +7417,7 @@ mod tests {
let clsmod = Module {
schema: SCHEMA.into(),
name: "clsmod".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Class(ClassDef {
name: "Show".into(),
@@ -7339,6 +7447,7 @@ mod tests {
let fnmod = Module {
schema: SCHEMA.into(),
name: "fnmod".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "show".into(),
@@ -7426,6 +7535,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "m".to_string(),
kernel: false,
imports: vec![],
defs: vec![Def::Class(ClassDef {
name: "MyCls".to_string(),
@@ -7855,4 +7965,82 @@ mod tests {
"expected diagnostic code `new-arg-kind-mismatch`, got {diags:?}"
);
}
/// prep.3 (kernel-extension-mechanics): `param-in` enforcement
/// rejects a `Type::Con` whose positional arg's outermost
/// type-name is not in the allowed set. Property: a TypeDef
/// carrying `param-in = {"a": {"Int", "Float"}}` referenced as
/// `(con StubT (con Str))` fires `ParamNotInRestrictedSet` with
/// the right type-name, var, found, and allowed-set payload.
#[test]
fn param_in_rejects_disallowed_type() {
let m: Module = serde_json::from_value(serde_json::json!({
"schema": SCHEMA,
"name": "k",
"defs": [
{"kind": "type", "name": "StubT", "vars": ["a"],
"ctors": [{"name": "Stub", "fields": [{"k": "var", "name": "a"}]}],
"param-in": {"a": ["Int", "Float"]}},
// Reference `(con StubT (con Str))` in a fn return
// type — well-formedness check walks the return type.
{"kind": "fn", "name": "bad",
"type": {"k": "fn", "params": [],
"ret": {"k": "con", "name": "StubT",
"args": [{"k": "con", "name": "Str"}]},
"effects": []},
"params": [],
"body": {"t": "lit", "lit": {"kind": "unit"}}}
]
})).unwrap();
let mut modules = BTreeMap::new();
modules.insert("k".to_string(), m);
let ws = Workspace {
entry: "k".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(
diags.iter().any(|d| d.code == "param-not-in-restricted-set"),
"expected diagnostic code `param-not-in-restricted-set`, got {diags:?}"
);
}
/// prep.3 (kernel-extension-mechanics): `param-in` enforcement
/// accepts a type-arg inside the allowed set. Same TypeDef as
/// the RED test, but `(con StubT (con Int))` — Int is in
/// {Int, Float}, so the check passes.
#[test]
fn param_in_accepts_allowed_type() {
let m: Module = serde_json::from_value(serde_json::json!({
"schema": SCHEMA,
"name": "k",
"defs": [
{"kind": "type", "name": "StubT", "vars": ["a"],
"ctors": [{"name": "Stub", "fields": [{"k": "var", "name": "a"}]}],
"param-in": {"a": ["Int", "Float"]}},
{"kind": "fn", "name": "good",
"type": {"k": "fn", "params": [],
"ret": {"k": "con", "name": "StubT",
"args": [{"k": "con", "name": "Int"}]},
"effects": []},
"params": [],
"body": {"t": "lit", "lit": {"kind": "unit"}}}
]
})).unwrap();
let mut modules = BTreeMap::new();
modules.insert("k".to_string(), m);
let ws = Workspace {
entry: "k".into(),
modules,
root_dir: std::path::PathBuf::from("."),
registry: ailang_core::workspace::Registry::default(),
};
let diags = check_workspace(&ws);
assert!(
!diags.iter().any(|d| d.code == "param-not-in-restricted-set"),
"expected NO param-not-in-restricted-set diagnostic, got {diags:?}"
);
}
}
crates/ailang-check/src/linearity.rs
+16
View File
@@ -1266,6 +1266,7 @@ fn make_consume_while_borrowed(def: &str, binder: &str) -> Diagnostic {
mod tests {
use super::*;
use ailang_core::ast::{FnDef, Literal};
use std::collections::BTreeMap;
fn fn_with_modes(name: &str, modes: Vec<ParamMode>, body: Term) -> Def {
Def::Fn(FnDef {
@@ -1295,6 +1296,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_with_modes(
"f",
@@ -1312,6 +1314,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_with_modes(
"f",
@@ -1332,6 +1335,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_with_modes(
"f",
@@ -1360,6 +1364,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_with_modes("f", vec![ParamMode::Own], body)],
};
@@ -1401,6 +1406,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_with_modes("f", vec![ParamMode::Own], body)],
};
@@ -1448,6 +1454,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![read_def, fn_with_modes("f", vec![ParamMode::Own], f_body)],
};
@@ -1497,6 +1504,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_with_modes("f", vec![ParamMode::Own], body)],
};
@@ -1516,6 +1524,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_with_modes(
"f",
@@ -1550,6 +1559,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_with_modes("f", vec![ParamMode::Own], body)],
};
@@ -1584,6 +1594,7 @@ mod tests {
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
})
}
@@ -1632,6 +1643,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![intlist_typedef(), fn_own_intlist("f", body)],
};
@@ -1657,6 +1669,7 @@ mod tests {
}],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
})
}
@@ -1727,6 +1740,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![state_typedef(), fn_own_state("f", body)],
};
@@ -1775,6 +1789,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![intlist_typedef(), fn_own_intlist("f", body)],
};
@@ -1858,6 +1873,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "m".into(),
kernel: false,
imports: vec![],
defs: vec![class_eq, ne],
};
crates/ailang-check/src/reuse_shape.rs
+5
View File
@@ -574,6 +574,7 @@ fn make_shape_mismatch(
mod tests {
use super::*;
use ailang_core::ast::{Ctor, FnDef, Literal};
use std::collections::BTreeMap;
fn list_type_def() -> TypeDef {
TypeDef {
@@ -591,6 +592,7 @@ mod tests {
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
}
}
@@ -656,6 +658,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Type(list_type_def()),
@@ -708,6 +711,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Type(list_type_def()),
@@ -756,6 +760,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Type(list_type_def()),
crates/ailang-check/src/suppress_filter.rs
+1
View File
@@ -112,6 +112,7 @@ mod tests {
Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: name.into(),
crates/ailang-check/src/uniqueness.rs
+5
View File
@@ -471,6 +471,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_simple("f", vec![], body)],
};
@@ -492,6 +493,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_simple("f", vec![], body)],
};
@@ -521,6 +523,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "f".into(),
kernel: false,
imports: vec![],
defs: vec![fn_simple("f", vec![], body)],
};
@@ -544,6 +547,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_simple("f", vec![], body)],
};
@@ -567,6 +571,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![fn_simple("f", vec![], body)],
};
crates/ailang-check/tests/duplicate_ctor_pin.rs
+3
View File
@@ -22,6 +22,7 @@ fn duplicate_ctor_across_two_adts_in_one_module() {
let m = Module {
schema: SCHEMA.into(),
name: "M".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Type(TypeDef {
@@ -33,6 +34,7 @@ fn duplicate_ctor_across_two_adts_in_one_module() {
}],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
}),
Def::Type(TypeDef {
name: "Dog".into(),
@@ -43,6 +45,7 @@ fn duplicate_ctor_across_two_adts_in_one_module() {
}],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
}),
],
};
crates/ailang-check/tests/workspace.rs
+10
View File
@@ -100,6 +100,7 @@ fn invalid_def_name_with_dot_is_reported() {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Const(ConstDef {
name: "weird.name".into(),
@@ -182,6 +183,7 @@ fn body_errors_accumulate_across_defs() {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "two_errors".into(),
kernel: false,
imports: vec![],
defs: vec![bad_a, bad_b],
};
@@ -284,11 +286,13 @@ fn use_after_consume_on_own_param_is_reported() {
}],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
});
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "lin_uac".into(),
kernel: false,
imports: vec![],
defs: vec![list_adt, sum_list, bad],
};
@@ -345,6 +349,7 @@ fn consume_while_borrowed_in_sibling_arg_is_reported() {
}],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
});
// dual_fn: (borrow List) → (own List) → Int.
@@ -393,6 +398,7 @@ fn consume_while_borrowed_in_sibling_arg_is_reported() {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "lin_cwb".into(),
kernel: false,
imports: vec![],
defs: vec![list_adt, dual_fn, bad],
};
@@ -460,6 +466,7 @@ fn reuse_as_happy_path_in_map_inc_is_linearity_clean() {
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
});
let map_inc_ty = Type::Fn {
@@ -533,6 +540,7 @@ fn reuse_as_happy_path_in_map_inc_is_linearity_clean() {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "reuse_as_happy".into(),
kernel: false,
imports: vec![],
defs: vec![list_adt, map_inc],
};
@@ -587,6 +595,7 @@ fn reuse_as_shape_mismatch_is_reported_on_cons_to_nil() {
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
});
let f_ty = Type::Fn {
@@ -646,6 +655,7 @@ fn reuse_as_shape_mismatch_is_reported_on_cons_to_nil() {
let m = Module {
schema: ailang_core::SCHEMA.into(),
name: "reuse_as_mismatch".into(),
kernel: false,
imports: vec![],
defs: vec![list_adt, f],
};
crates/ailang-codegen/src/lib.rs
+22
View File
@@ -3581,6 +3581,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Fn(FnDef {
@@ -3651,6 +3652,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "noentry".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "helper".into(),
@@ -3701,6 +3703,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "rclist".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Type(TypeDef {
@@ -3724,6 +3727,7 @@ mod tests {
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
}),
Def::Fn(FnDef {
name: "main".into(),
@@ -3788,6 +3792,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.to_string(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Const(ConstDef {
@@ -3863,6 +3868,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.to_string(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![
fn_def("ai", plus_int, Type::int()),
@@ -3928,6 +3934,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.to_string(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![
fn_def("ni", neg_int, Type::int()),
@@ -3977,6 +3984,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.to_string(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![
fn_def("k_nan", Term::Var { name: "nan".into() }),
@@ -4002,6 +4010,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "prelude".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Fn(FnDef {
@@ -4064,6 +4073,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "prelude".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Fn(FnDef {
@@ -4128,6 +4138,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "main".into(),
@@ -4226,6 +4237,7 @@ mod tests {
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
});
// Ordering is `ptr` at the LLVM level (boxed ADT).
let compare = Def::Fn(FnDef {
@@ -4261,6 +4273,7 @@ mod tests {
Module {
schema: SCHEMA.into(),
name: "prelude".into(),
kernel: false,
imports: vec![],
defs: vec![ordering, compare, main_def],
}
@@ -4278,6 +4291,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Const(ConstDef {
@@ -4320,6 +4334,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "main".into(),
@@ -4361,6 +4376,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "main".into(),
@@ -4420,6 +4436,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "prelude".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Fn(FnDef {
@@ -4516,6 +4533,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "main".into(),
@@ -4556,6 +4574,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "main".into(),
@@ -4597,6 +4616,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "main".into(),
@@ -4638,6 +4658,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "main".into(),
@@ -4679,6 +4700,7 @@ mod tests {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "main".into(),
crates/ailang-core/src/ast.rs
+31
View File
@@ -17,6 +17,8 @@
//! [`crate::canonical`] for canonical bytes, [`crate::hash`] for content
//! hashes, and the `ailang-check` crate for typechecking.
use std::collections::{BTreeMap, BTreeSet};
use serde::{Deserialize, Serialize};
/// A complete AILang translation unit.
@@ -33,6 +35,14 @@ pub struct Module {
/// (`<name>.ail.json`); the [`crate::workspace`] loader enforces
/// this on import.
pub name: String,
/// Kernel-tier flag. When `true`, the module's top-level type
/// names and free defs are visible to every consumer without an
/// explicit `(import …)` declaration. Strictly additive: omitted
/// from canonical JSON when `false`, so every pre-existing
/// fixture's hash is bit-stable. See prep.3 of the
/// kernel-extension-mechanics milestone.
#[serde(default, skip_serializing_if = "is_false")]
pub kernel: bool,
/// Imports of other modules. Resolved by the workspace loader as
/// `<root_dir>/<module>.ail.json`.
#[serde(default)]
@@ -167,6 +177,27 @@ pub struct TypeDef {
skip_serializing_if = "is_false"
)]
pub drop_iterative: bool,
/// Closed-set restriction on type-parameter instantiation. Maps
/// each var name (drawn from [`Self::vars`]) to a set of allowed
/// concrete type names. When non-empty, the checker enforces
/// that every `Type::Con { name: <self.name>, args }` carries an
/// `args[i]` whose outermost type-name lies in the restricted
/// set for that variable.
///
/// Serialised as `"param-in": { "<var>": ["<T>", ...] }`
/// (kebab-case); the field is **omitted when empty**, preserving
/// the canonical-JSON hash of every fixture that does not
/// restrict.
///
/// See prep.3 of the kernel-extension-mechanics milestone and
/// the new diagnostic `ParamNotInRestrictedSet` in
/// `crates/ailang-check/src/lib.rs`.
#[serde(
default,
rename = "param-in",
skip_serializing_if = "BTreeMap::is_empty"
)]
pub param_in: BTreeMap<String, BTreeSet<String>>,
}
crates/ailang-core/src/desugar.rs
+16
View File
@@ -1785,6 +1785,7 @@ mod tests {
let m = Module {
schema: crate::SCHEMA.to_string(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "f".into(),
@@ -1842,6 +1843,7 @@ mod tests {
let m = Module {
schema: crate::SCHEMA.to_string(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "f".into(),
@@ -1900,6 +1902,7 @@ mod tests {
let m = Module {
schema: crate::SCHEMA.to_string(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "main".into(),
@@ -1963,6 +1966,7 @@ mod tests {
let m = Module {
schema: crate::SCHEMA.to_string(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "outer".into(),
@@ -2111,6 +2115,7 @@ mod tests {
let m = Module {
schema: crate::SCHEMA.to_string(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "main".into(),
@@ -2184,6 +2189,7 @@ mod tests {
}],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
};
let letrec = Term::LetRec {
name: "helper".into(),
@@ -2225,6 +2231,7 @@ mod tests {
let m = Module {
schema: crate::SCHEMA.to_string(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Type(pair_td),
@@ -2309,6 +2316,7 @@ mod tests {
let m = Module {
schema: crate::SCHEMA.to_string(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "main".into(),
@@ -2371,6 +2379,7 @@ mod tests {
let m = Module {
schema: crate::SCHEMA.to_string(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "main".into(),
@@ -2512,6 +2521,7 @@ mod tests {
let m = Module {
schema: crate::SCHEMA.to_string(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "rec_id".into(),
@@ -2616,6 +2626,7 @@ mod tests {
let m = Module {
schema: crate::SCHEMA.to_string(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "outer".into(),
@@ -2702,6 +2713,7 @@ mod tests {
let m = Module {
schema: crate::SCHEMA.to_string(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "main".into(),
@@ -2783,6 +2795,7 @@ mod tests {
let m = Module {
schema: crate::SCHEMA.to_string(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "main".into(),
@@ -2913,6 +2926,7 @@ mod tests {
let m = Module {
schema: crate::SCHEMA.to_string(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "f".into(),
@@ -2987,6 +3001,7 @@ mod tests {
let m = Module {
schema: crate::SCHEMA.to_string(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "f".into(),
@@ -3069,6 +3084,7 @@ mod tests {
let m = Module {
schema: crate::SCHEMA.to_string(),
name: "t".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "f".into(),
crates/ailang-core/src/pretty.rs
+1
View File
@@ -169,6 +169,7 @@ mod tests {
Module {
schema: crate::SCHEMA.into(),
name: "sample".into(),
kernel: false,
imports: vec![],
defs: vec![
Def::Fn(FnDef {
crates/ailang-core/src/workspace.rs
+19 -6
View File
@@ -304,11 +304,16 @@ pub enum WorkspaceLoadError {
type_repr: String,
},
/// a user module attempted to use the reserved
/// module name `prelude`. The prelude is auto-injected by
/// the loader, so a user module of the same name would
/// collide silently. Reject explicitly.
#[error("module name {name:?} is reserved (auto-injected by the loader)")]
/// A user workspace contains a module whose name collides with
/// a built-in kernel-tier module that the loader auto-injects.
/// The current built-in set is `prelude` and `kernel_stub` (the
/// stub is injected unconditionally in all builds as the
/// ratifying fixture for the kernel-extension mechanism;
/// future base extensions may add more or retire the stub).
/// Previously this variant fired specifically for `prelude`;
/// since prep.3 of the kernel-extension-mechanics milestone, it
/// fires for any built-in kernel module name.
#[error("workspace module `{name}` collides with a built-in kernel-tier module name (reserved)")]
ReservedModuleName { name: String },
/// the canonical-form rule for type references: a `Type::Con` whose `name` is
@@ -464,12 +469,20 @@ where
/// pd.1: extract the validation + registry-construction tail of
/// `load_workspace_with` into a public fn that operates on a pre-assembled
/// modules map. The caller (typically `surface::load_workspace`, post-pd.2)
/// modules map. The caller (typically `ailang_surface::loader::load_workspace`)
/// is responsible for injecting any implicit modules (e.g. prelude) into
/// `modules` BEFORE calling this fn, AND for naming those implicit modules
/// in `implicit_imports` so the diagnostic helpers (`check_class_ref`,
/// `check_type_con_name`) include them as fallback candidates.
///
/// `implicit_imports` is the list of module names every consumer
/// should auto-import without an explicit `(import …)` declaration.
/// The caller derives this list from the kernel-tier filter: every
/// loaded module with `kernel: true` enters the list. Since prep.3
/// of the kernel-extension-mechanics milestone, this is the flag-
/// driven generalisation of the prior hardcoded `&["prelude"]`
/// literal.
///
/// Runs the three-stage pipeline:
/// 1. `validate_canonical_type_names` (with `implicit_imports`)
/// 2. `validate_classdefs` (no `implicit_imports` — does not consume it)
crates/ailang-core/tests/design_schema_drift.rs
+134 -1
View File
@@ -14,9 +14,11 @@
//! `## Data model` … `## Pipeline` slicer is no longer needed (the split
//! gave the section its own file).
use std::collections::BTreeMap;
use ailang_core::ast::{
ClassDef, ClassMethod, Constraint, ConstDef, Ctor, Def, FnDef, InstanceDef,
InstanceMethod, Literal, NewArg, Pattern, ParamMode, Suppress, Term, Type, TypeDef,
InstanceMethod, Literal, Module, NewArg, Pattern, ParamMode, Suppress, Term, Type, TypeDef,
};
const DATA_MODEL: &str = include_str!("../../../design/contracts/0002-data-model.md");
@@ -326,6 +328,7 @@ fn design_md_anchors_every_def_kind() {
vars: vec![],
ctors: vec![Ctor { name: "C".into(), fields: vec![] }],
drop_iterative: false,
param_in: BTreeMap::new(),
};
let class_def = ClassDef {
name: "Show".into(),
@@ -629,3 +632,133 @@ fn term_new_type_arg_round_trips() {
}
/// prep.3 (kernel-extension-mechanics): pin the JSON byte-shape of
/// `Module.kernel`. Property protected: when `true`, the key
/// serialises as the bare `"kernel": true` flag adjacent to
/// `"name"`; when `false`, it is omitted entirely from canonical
/// JSON (preserving the bit-identical hash of every pre-existing
/// fixture). A future edit that renames the field, drops the
/// `skip_serializing_if`, or changes its boolean shape breaks the
/// pin in lockstep with the data-model document.
#[test]
fn module_kernel_flag_round_trips() {
let m_on = Module {
schema: ailang_core::SCHEMA.to_string(),
name: "k".into(),
kernel: true,
imports: vec![],
defs: vec![],
};
let json_on = serde_json::to_value(&m_on).expect("serialise kernel: true");
assert_eq!(
json_on["kernel"], true,
"kernel: true must appear as a bare boolean key"
);
let m_off = Module {
schema: ailang_core::SCHEMA.to_string(),
name: "k".into(),
kernel: false,
imports: vec![],
defs: vec![],
};
let json_off = serde_json::to_value(&m_off).expect("serialise kernel: false");
assert!(
json_off.get("kernel").is_none(),
"kernel: false must be omitted from canonical JSON (hash-stability)"
);
let recovered: Module =
serde_json::from_value(json_on).expect("Module with kernel: true round-trips");
assert!(recovered.kernel);
}
/// prep.3 (kernel-extension-mechanics): pin the JSON byte-shape of
/// `TypeDef.param_in`. Property protected: when non-empty, the map
/// serialises under the kebab-case key `"param-in"`; when empty,
/// it is omitted entirely (preserving the bit-identical hash of
/// every fixture that does not restrict). The BTreeMap/BTreeSet
/// choice gives deterministic iteration order (alphabetical) so
/// the canonical-JSON bytes are reproducible. A future edit that
/// renames the field, drops the `skip_serializing_if`, or changes
/// the inner collection type breaks the pin in lockstep with the
/// data-model document.
#[test]
fn typedef_param_in_round_trips() {
use std::collections::BTreeSet;
let mut restrict: BTreeMap<String, BTreeSet<String>> = BTreeMap::new();
restrict.insert(
"a".into(),
["Int".to_string(), "Float".to_string()].into_iter().collect(),
);
let td_on = TypeDef {
name: "T".into(),
vars: vec!["a".into()],
ctors: vec![],
doc: None,
drop_iterative: false,
param_in: restrict.clone(),
};
let json_on = serde_json::to_value(&td_on).expect("serialise param_in non-empty");
let pi = json_on.get("param-in").expect(
"non-empty param_in serialises under kebab key `param-in`",
);
let allowed = pi["a"].as_array().expect("inner value is a Type-name array");
assert_eq!(allowed.len(), 2);
// BTreeSet iteration order is alphabetical:
assert_eq!(allowed[0], "Float");
assert_eq!(allowed[1], "Int");
let td_off = TypeDef {
name: "T".into(),
vars: vec![],
ctors: vec![],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
};
let json_off = serde_json::to_value(&td_off).expect("serialise param_in empty");
assert!(
json_off.get("param-in").is_none(),
"empty param_in must be omitted from canonical JSON (hash-stability)"
);
let recovered: TypeDef =
serde_json::from_value(json_on).expect("TypeDef with param_in round-trips");
assert_eq!(recovered.param_in, restrict);
}
/// prep.3 (kernel-extension-mechanics): pin the JSON byte-shape of
/// the kernel-stub module — exercises all three new schema items
/// in a single fixture (`Module.kernel = true`, one TypeDef with
/// `param-in`, one ctor). A future edit that breaks any of the new
/// additive schema fields will trip this pin in lockstep with the
/// per-field round-trip tests (`module_kernel_flag_round_trips`,
/// `typedef_param_in_round_trips`).
#[test]
fn kernel_stub_module_round_trips() {
let m = ailang_surface::parse_kernel_stub();
assert!(m.kernel, "stub module is kernel-tier");
assert_eq!(m.name, "kernel_stub");
let json = serde_json::to_value(&m).expect("serialise stub module");
assert_eq!(json["kernel"], true);
assert_eq!(json["name"], "kernel_stub");
let recovered: Module =
serde_json::from_value(json).expect("stub module round-trips through serde");
assert!(recovered.kernel);
assert_eq!(recovered.name, "kernel_stub");
// Locate the StubT TypeDef and confirm param_in is intact.
let td = recovered.defs.iter().find_map(|d| match d {
Def::Type(t) if t.name == "StubT" => Some(t),
_ => None,
}).expect("StubT TypeDef present in stub module");
let allowed = td.param_in.get("a").expect("StubT.a restricted");
assert!(allowed.contains("Int"));
assert!(allowed.contains("Float"));
}
crates/ailang-core/tests/spec_drift.rs
+3
View File
@@ -11,6 +11,8 @@
//! without a spec entry fails compilation here long before the test runs.
//! Once the variant is matched, the test asserts the spec mentions it.
use std::collections::BTreeMap;
use ailang_core::ast::{
ConstDef, Ctor, Def, FnDef, Literal, NewArg, Pattern, Suppress, Term, Type, TypeDef,
};
@@ -287,6 +289,7 @@ fn spec_mentions_every_def_kind() {
fields: vec![],
}],
drop_iterative: false,
param_in: BTreeMap::new(),
};
let exemplars: Vec<(&str, Def)> = vec![
("(fn ", Def::Fn(fn_def)),
crates/ailang-core/tests/workspace_kernel.rs
+162
View File
@@ -0,0 +1,162 @@
//! prep.3 (kernel-extension-mechanics): workspace-load tests for
//! kernel-tier auto-import. These tests exercise the flag-driven
//! generalisation of the prior hardcoded `&["prelude"]` literal —
//! every workspace-loaded module with `kernel: true` joins the
//! implicit-imports list and therefore makes its types visible bare
//! to every consumer, even consumers that did not name it under
//! `(import …)`.
//!
//! Reachability: a user `(kernel)` module enters the workspace's
//! modules map only if some module in the import chain reaches it
//! (the standard import-graph DFS). The kernel-tier flag does NOT
//! cause unreachable `.ail` files in the entry's directory to be
//! loaded — see Concern in the iter prep.3 end-report. The
//! built-in `prelude` and `kernel_stub` are always loaded because
//! the loader injects them programmatically; user kernel-tier
//! modules need a path from the entry.
use ailang_surface::load_workspace;
use std::path::{Path, PathBuf};
/// Write a Form-A source file into the temp dir and return its path.
fn write_module(dir: &Path, name: &str, src: &str) -> PathBuf {
let path = dir.join(format!("{name}.ail"));
std::fs::write(&path, src).expect("write fixture");
path
}
/// prep.3: a workspace-loaded `(kernel)` module makes its types
/// visible bare to consumers that did NOT name it under
/// `(import …)`. Property: the kernel-flag filter derives the
/// implicit-imports list from every `kernel: true` module in the
/// modules map — `consumer` references `KT` bare and validates
/// because `bridge` brought `k_mod` into the workspace.
#[test]
fn kernel_tier_module_auto_imports_without_explicit_import() {
let dir = tempfile::tempdir().expect("tempdir");
// k_mod carries (kernel) and declares KT.
write_module(
dir.path(),
"k_mod",
"(module k_mod\n (kernel)\n (data KT (vars a) (ctor KCtor a)))\n",
);
// bridge imports k_mod so it enters the workspace.
write_module(
dir.path(),
"bridge",
concat!(
"(module bridge\n",
" (import k_mod)\n",
" (fn anchor\n",
" (type (forall (vars a) (fn-type (params (con KT a)) (ret (con Unit)))))\n",
" (params k) (body unit)))\n",
),
);
// The entry imports bridge (transitively pulling k_mod), and
// uses `(con KT (var a))` bare — no explicit import of k_mod.
let entry = write_module(
dir.path(),
"consumer",
concat!(
"(module consumer\n",
" (import bridge)\n",
" (fn use_kt\n",
" (type (forall (vars a) (fn-type (params (con KT a)) (ret (con Unit)))))\n",
" (params k) (body unit)))\n",
),
);
let ws = load_workspace(&entry).expect("workspace loads (kernel-tier auto-import)");
assert!(
ws.modules.contains_key("k_mod"),
"k_mod was loaded transitively via bridge"
);
assert!(
ws.modules.get("k_mod").unwrap().kernel,
"k_mod is marked kernel-tier"
);
}
/// prep.3: two `(kernel)` modules co-load without conflict; both
/// enter the implicit-imports list and both are visible to a
/// consumer that imported neither directly. Property: the filter
/// `modules.values().filter(|m| m.kernel)` walks ALL modules (not
/// just the first match), so every kernel-tier module gets
/// auto-imported.
#[test]
fn two_kernel_tier_modules_coload() {
let dir = tempfile::tempdir().expect("tempdir");
write_module(
dir.path(),
"k_a",
"(module k_a\n (kernel)\n (data A (ctor AC)))\n",
);
write_module(
dir.path(),
"k_b",
"(module k_b\n (kernel)\n (data B (ctor BC)))\n",
);
// bridge imports both kernel modules; consumer transitively
// sees both via the kernel-flag filter without explicit import.
write_module(
dir.path(),
"bridge",
concat!(
"(module bridge\n",
" (import k_a)\n",
" (import k_b)\n",
" (fn anchor\n",
" (type (fn-type (params (con A) (con B)) (ret (con Unit))))\n",
" (params a b) (body unit)))\n",
),
);
let entry = write_module(
dir.path(),
"consumer",
concat!(
"(module consumer\n",
" (import bridge)\n",
" (fn use_ab\n",
" (type (fn-type (params (con A) (con B)) (ret (con Unit))))\n",
" (params a b) (body unit)))\n",
),
);
let ws = load_workspace(&entry).expect("workspace with two kernel modules");
assert!(ws.modules.contains_key("k_a"));
assert!(ws.modules.contains_key("k_b"));
assert!(ws.modules.get("k_a").unwrap().kernel);
assert!(ws.modules.get("k_b").unwrap().kernel);
}
/// prep.3: an explicit `(import …)` for a kernel-tier module
/// coexists with the auto-import — no double-resolution error, no
/// behaviour drift. Property: the implicit-imports list and the
/// explicit-imports list are both consulted by the validator;
/// having the same name in both does not produce a duplicate-
/// import diagnostic.
#[test]
fn explicit_import_takes_precedence_over_auto_import() {
let dir = tempfile::tempdir().expect("tempdir");
write_module(
dir.path(),
"k_mod",
"(module k_mod\n (kernel)\n (data KT (ctor KC)))\n",
);
// consumer explicitly imports k_mod AND uses KT bare.
let entry = write_module(
dir.path(),
"consumer",
concat!(
"(module consumer\n",
" (import k_mod)\n",
" (fn use_kt\n",
" (type (fn-type (params (con KT)) (ret (con Unit))))\n",
" (params k) (body unit)))\n",
),
);
let ws = load_workspace(&entry).expect("explicit + auto coexist");
assert!(ws.modules.contains_key("k_mod"));
assert!(ws.modules.get("k_mod").unwrap().kernel);
}
crates/ailang-kernel-stub/Cargo.toml
+7
View File
@@ -0,0 +1,7 @@
[package]
name = "ailang-kernel-stub"
version.workspace = true
edition.workspace = true
license.workspace = true
[dependencies]
crates/ailang-kernel-stub/src/lib.rs
+27
View File
@@ -0,0 +1,27 @@
//! Kernel-tier stub module — minimal ratifying fixture for the
//! kernel-extension-mechanics milestone (prep.3).
//!
//! The stub exists solely to exercise the shipped mechanisms
//! end-to-end: `Module.kernel`, `TypeDef.param-in`, and type-scoped
//! resolution (the stub's type is visible to every consumer without
//! an `(import …)` declaration).
//!
//! No domain content. The stub may be retired or repositioned when
//! a real second kernel-tier consumer (the `raw-buf` milestone) lands.
//!
//! This crate carries ONLY the embedded Form-A text and the parsed
//! `Module` value. The parse hop itself lives in `ailang-surface`
//! (see `ailang_surface::parse_kernel_stub`) so the
//! crate-dependency graph stays acyclic: `ailang-surface →
//! ailang-kernel-stub → ailang-core` (no back-edge from
//! `ailang-kernel-stub` to `ailang-surface`).
/// Source-of-truth Form-A text for the stub kernel module. Parsed
/// by `ailang_surface::parse_kernel_stub` (and round-trip-pinned by
/// `kernel_stub_module_round_trips` in `design_schema_drift.rs`).
pub const STUB_AIL: &str = r#"(module kernel_stub
(kernel)
(data StubT (vars a)
(ctor Stub a)
(param-in (a Int Float))))
"#;
crates/ailang-prose/src/lib.rs
+9
View File
@@ -1323,6 +1323,7 @@ fn subst_var_with_term(t: &Term, name: &str, replacement: &Term) -> Term {
mod tests {
use super::*;
use ailang_core::ast::{Arm, Ctor, FnDef, Literal, Pattern, Term, Type};
use std::collections::BTreeMap;
fn render_term(t: &Term) -> String {
let mut out = String::new();
@@ -1937,6 +1938,7 @@ mod tests {
}],
doc: Some("line one\nline two".into()),
drop_iterative: false,
param_in: BTreeMap::new(),
};
let mut out = String::new();
write_type_def(&mut out, &td, 0, "");
@@ -1959,6 +1961,7 @@ mod tests {
],
doc: None,
drop_iterative: false,
param_in: BTreeMap::new(),
};
let mut out = String::new();
write_type_def(&mut out, &td, 0, "");
@@ -2154,6 +2157,7 @@ mod tests {
ctors: vec![Ctor { name: "MkFoo".into(), fields: vec![] }],
doc: Some(long),
drop_iterative: false,
param_in: BTreeMap::new(),
};
let mut out = String::new();
write_type_def(&mut out, &td, 0, "");
@@ -2184,6 +2188,7 @@ mod tests {
ctors: vec![Ctor { name: "MkFoo".into(), fields: vec![] }],
doc: Some("Short and snappy.".into()),
drop_iterative: false,
param_in: BTreeMap::new(),
};
let mut out = String::new();
write_type_def(&mut out, &td, 0, "");
@@ -2206,6 +2211,7 @@ mod tests {
ctors: vec![Ctor { name: "MkFoo".into(), fields: vec![] }],
doc: Some(doc),
drop_iterative: false,
param_in: BTreeMap::new(),
};
let mut out = String::new();
write_type_def(&mut out, &td, 0, "");
@@ -2231,6 +2237,7 @@ mod tests {
ctors: vec![Ctor { name: "MkFoo".into(), fields: vec![] }],
doc: Some(doc.into()),
drop_iterative: false,
param_in: BTreeMap::new(),
};
let mut out = String::new();
write_type_def(&mut out, &td, 0, "");
@@ -2323,6 +2330,7 @@ mod tests {
let m = Module {
schema: "ailang/v0".into(),
name: "prelude".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(FnDef {
name: "noop".into(),
@@ -2371,6 +2379,7 @@ mod tests {
let m = Module {
schema: "ailang/v0".into(),
name: "user".into(),
kernel: false,
imports: vec![Import { module: "prelude".into(), alias: None }],
defs: vec![Def::Fn(FnDef {
name: "lt".into(),
crates/ailang-surface/Cargo.toml
+1
View File
@@ -6,6 +6,7 @@ license.workspace = true
[dependencies]
ailang-core.workspace = true
ailang-kernel-stub.workspace = true
serde_json.workspace = true
thiserror.workspace = true
crates/ailang-surface/src/lib.rs
+1 -1
View File
@@ -36,6 +36,6 @@ pub mod loader;
pub mod parse;
pub mod print;
pub use loader::{load_module, load_workspace, parse_prelude, PRELUDE_AIL};
pub use loader::{load_module, load_workspace, parse_kernel_stub, parse_prelude, PRELUDE_AIL};
pub use parse::{parse, parse_term, ParseError};
pub use print::{print, term_to_form_a, type_to_form_a};
crates/ailang-surface/src/loader.rs
+44 -1
View File
@@ -42,6 +42,20 @@ pub fn parse_prelude() -> Module {
crate::parse(PRELUDE_AIL).expect("examples/prelude.ail must parse as a Module")
}
/// prep.3 (kernel-extension-mechanics): parse the embedded
/// kernel-stub bytes into a `Module`. Mirror of [`parse_prelude`].
///
/// Source-of-truth: `ailang_kernel_stub::STUB_AIL`. The stub
/// ratifies the end-to-end kernel-tier path: `Module.kernel`,
/// `TypeDef.param-in`, and auto-import without `(import …)`.
///
/// Panics on parse failure — the stub is build-time-validated by
/// every drift test run.
pub fn parse_kernel_stub() -> Module {
crate::parse(ailang_kernel_stub::STUB_AIL)
.expect("ailang_kernel_stub::STUB_AIL must parse as a Module")
}
fn is_ail_source(path: &Path) -> bool {
path.extension().and_then(|s| s.to_str()) == Some("ail")
}
@@ -95,16 +109,45 @@ pub fn load_module(path: &Path) -> Result<Module, WorkspaceLoadError> {
pub fn load_workspace(entry: &Path) -> Result<Workspace, WorkspaceLoadError> {
let (entry_name, root_dir, mut modules) =
ailang_core::workspace::load_modules_with(entry, load_module)?;
// parse_prelude() injects the built-in prelude into the
// workspace. The prelude module's source carries `(kernel)`, so
// it surfaces in the kernel-tier auto-import set below.
if modules.contains_key("prelude") {
return Err(WorkspaceLoadError::ReservedModuleName {
name: "prelude".to_string(),
});
}
modules.insert("prelude".to_string(), parse_prelude());
// parse_kernel_stub() injects the ratifying stub kernel module —
// exercises Module.kernel + TypeDef.param-in end-to-end. The
// kernel-flag filter below picks it up automatically because its
// source carries `(kernel)`.
if modules.contains_key("kernel_stub") {
return Err(WorkspaceLoadError::ReservedModuleName {
name: "kernel_stub".to_string(),
});
}
modules.insert("kernel_stub".to_string(), parse_kernel_stub());
// Derive the implicit-imports list from `kernel: true` modules.
// Replaces the previous hardcoded `&["prelude"]` literal: any
// workspace-loaded module that carries the kernel flag is now
// auto-imported. See prep.3 of the kernel-extension-mechanics
// milestone.
let kernel_names: Vec<String> = modules
.values()
.filter(|m| m.kernel)
.map(|m| m.name.clone())
.collect();
let implicit_imports: Vec<&str> =
kernel_names.iter().map(String::as_str).collect();
ailang_core::workspace::build_workspace(
entry_name,
root_dir,
modules,
&["prelude"],
&implicit_imports,
)
}
crates/ailang-surface/src/parse.rs
+72 -2
View File
@@ -84,6 +84,8 @@
//! - The `import` form admits an optional `as` alias to round-trip
//! [`ailang_core::ast::Import::alias`].
use std::collections::{BTreeMap, BTreeSet};
use ailang_core::ast::{
Arm, ClassDef, ClassMethod, Constraint, ConstDef, Ctor, Def, FnDef, Import, InstanceDef,
InstanceMethod, Literal, Module, ParamMode, Pattern, SuperclassRef, Suppress, Term,
@@ -284,6 +286,7 @@ impl<'a> Parser<'a> {
self.expect_lparen("module")?;
self.expect_keyword("module")?;
let name = self.expect_ident("module name")?;
let mut kernel = false;
let mut imports: Vec<Import> = Vec::new();
let mut defs: Vec<Def> = Vec::new();
loop {
@@ -307,6 +310,32 @@ impl<'a> Parser<'a> {
}
})?;
match head {
"kernel" => {
// `(kernel)` opt-in attribute — bare flag, no inner content.
// A second `(kernel)` clause is a parse error so the
// JSON schema's `kernel: bool` round-trips unambiguously.
self.expect_lparen("kernel-attr")?;
self.expect_keyword("kernel")?;
if !matches!(self.peek(), Some(Token { tok: Tok::RParen, .. })) {
let pos = self.peek().map(|t| t.span.start).unwrap_or(0);
return Err(ParseError::Production {
production: "module",
message: "kernel takes no arguments; expected `)`"
.into(),
pos,
});
}
self.expect_rparen("kernel-attr")?;
if kernel {
let pos = self.peek().map(|t| t.span.start).unwrap_or(0);
return Err(ParseError::Production {
production: "module",
message: "duplicate `kernel` attribute".into(),
pos,
});
}
kernel = true;
}
"import" => imports.push(self.parse_import()?),
"data" => defs.push(Def::Type(self.parse_data()?)),
"fn" => defs.push(Def::Fn(self.parse_fn()?)),
@@ -318,7 +347,7 @@ impl<'a> Parser<'a> {
return Err(ParseError::Production {
production: "module",
message: format!(
"unknown def head `{other}`; expected `data`, `fn`, `const`, `class`, `instance`, or `import`"
"unknown def head `{other}`; expected `data`, `fn`, `const`, `class`, `instance`, `import`, or `kernel`"
),
pos,
});
@@ -329,6 +358,7 @@ impl<'a> Parser<'a> {
Ok(Module {
schema: SCHEMA.to_string(),
name,
kernel,
imports,
defs,
})
@@ -371,6 +401,7 @@ impl<'a> Parser<'a> {
let mut doc: Option<String> = None;
let mut ctors: Vec<Ctor> = Vec::new();
let mut drop_iterative = false;
let mut param_in: BTreeMap<String, BTreeSet<String>> = BTreeMap::new();
loop {
match self.peek_head_ident() {
Some("doc") => {
@@ -382,6 +413,44 @@ impl<'a> Parser<'a> {
Some("ctor") => {
ctors.push(self.parse_ctor()?);
}
Some("param-in") => {
// `(param-in (a Int Float) (b Str) ...)` — one
// outer clause carrying one or more inner
// var-lists. Mirrors the `(ctors ...)` nested
// shape (one outer attribute, list-of-inner).
// A duplicate inner var binding (`(a ...) (a ...)`)
// is a parse error so the BTreeMap round-trips
// unambiguously.
if !param_in.is_empty() {
return Err(self.duplicate_clause_err(
"data-def",
&format!("data `{name}`"),
"param-in",
));
}
self.expect_lparen("param-in-attr")?;
self.expect_keyword("param-in")?;
while !matches!(self.peek(), Some(Token { tok: Tok::RParen, .. })) {
self.expect_lparen("param-in-inner-var-list")?;
let var = self.expect_ident("type-variable name")?;
let mut allowed: BTreeSet<String> = BTreeSet::new();
while !matches!(self.peek(), Some(Token { tok: Tok::RParen, .. })) {
allowed.insert(self.expect_ident("allowed type-name")?);
}
self.expect_rparen("param-in-inner-var-list")?;
if param_in.insert(var.clone(), allowed).is_some() {
let pos = self.peek().map(|t| t.span.start).unwrap_or(0);
return Err(ParseError::Production {
production: "data-def",
message: format!(
"param-in: duplicate var binding `{var}`"
),
pos,
});
}
}
self.expect_rparen("param-in-attr")?;
}
Some("drop-iterative") => {
// `(drop-iterative)` opt-in annotation.
// Takes no arguments — it is a flag. A second
@@ -417,7 +486,7 @@ impl<'a> Parser<'a> {
return Err(ParseError::Production {
production: "data-def",
message: format!(
"unknown data attribute `{other}`; expected `doc`, `ctor`, or `drop-iterative`"
"unknown data attribute `{other}`; expected `doc`, `ctor`, `drop-iterative`, or `param-in`"
),
pos,
});
@@ -432,6 +501,7 @@ impl<'a> Parser<'a> {
ctors,
doc,
drop_iterative,
param_in,
})
}
crates/ailang-surface/src/print.rs
+29
View File
@@ -19,6 +19,11 @@ pub fn print(module: &Module) -> String {
out.push('(');
out.push_str("module ");
out.push_str(&module.name);
if module.kernel {
out.push('\n');
indent(&mut out, 1);
out.push_str("(kernel)");
}
for imp in &module.imports {
out.push('\n');
write_import(&mut out, imp, 1);
@@ -131,6 +136,25 @@ fn write_type_def(out: &mut String, td: &TypeDef, level: usize) {
indent(out, level + 1);
out.push_str("(drop-iterative)");
}
// `(param-in (a Int Float) (b Str) ...)` — BTreeMap/BTreeSet
// give deterministic alphabetical iteration order. Omitted when
// empty so the canonical Form-A bytes are bit-stable for every
// TypeDef that does not restrict.
if !td.param_in.is_empty() {
out.push('\n');
indent(out, level + 1);
out.push_str("(param-in");
for (var, allowed) in &td.param_in {
out.push_str(" (");
out.push_str(var);
for tname in allowed {
out.push(' ');
out.push_str(tname);
}
out.push(')');
}
out.push(')');
}
out.push(')');
}
@@ -724,6 +748,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.to_string(),
name: "M".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Class(ClassDef {
name: "Foo".into(),
@@ -751,6 +776,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.to_string(),
name: "M".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Class(ClassDef {
name: "Bar".into(),
@@ -781,6 +807,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.to_string(),
name: "M".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Fn(ailang_core::ast::FnDef {
name: "f".into(),
@@ -816,6 +843,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.to_string(),
name: "M".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Instance(InstanceDef {
class: "Foo".into(),
@@ -854,6 +882,7 @@ mod tests {
let m = Module {
schema: ailang_core::SCHEMA.to_string(),
name: "M".into(),
kernel: false,
imports: vec![],
defs: vec![Def::Const(ConstDef {
name: "k".into(),
crates/ailang-surface/tests/prelude_module_hash_pin.rs
+10 -1
View File
@@ -23,8 +23,17 @@ fn prelude_parse_yields_canonical_hash() {
// canonical-JSON bytes change and the module hash drifts.
// Form-A surface unchanged — only the canonical-JSON byte
// stream differs, which is what the rename targets.
// 2026-05-28 prep.3 (kernel-extension-mechanics) re-pinned
// (prior: 562a03fc57e7e017): prelude becomes kernel-tier —
// `examples/prelude.ail` gains the `(kernel)` module-header
// attribute, which serialises as `"kernel": true` in the
// canonical JSON. This changes the prelude's content hash
// deterministically; the behaviour `prelude_free_fns.rs`
// protects (12 free fns callable bare in every consumer) is
// unchanged — only the code path migrates from the hardcoded
// `&["prelude"]` literal to the kernel-flag filter.
assert_eq!(
h, "562a03fc57e7e017",
h, "af372f28c726f29f",
"prelude module hash drifted; if intentional, capture the new \
hex below + record the why in the commit body."
);
crates/ailang-surface/tests/round_trip.rs
+51
View File
@@ -194,3 +194,54 @@ fn parse_is_deterministic_over_every_ail_fixture() {
}
assert!(checked > 0, "no .ail fixtures found");
}
/// prep.3 (kernel-extension-mechanics): the `(kernel)` module-header
/// attribute round-trips Form-A → JSON → Form-A bit-identical and
/// preserves the parsed bool through both halves.
#[test]
fn kernel_module_header_round_trips() {
let src = "(module k\n (kernel))\n";
let m = ailang_surface::parse(src).expect("Form-A parse of (kernel) module");
assert!(m.kernel, "parsed kernel: true");
let printed = ailang_surface::print(&m);
// Round-trip: print, re-parse, kernel still true.
let m2 = ailang_surface::parse(&printed).expect("re-parse printed form");
assert!(m2.kernel, "kernel: true survives round-trip");
// Default form (no (kernel)) stays kernel: false.
let plain = ailang_surface::parse("(module p)\n").expect("Form-A parse plain module");
assert!(!plain.kernel);
}
/// prep.3 (kernel-extension-mechanics): the `(param-in (var t1 t2 ...))`
/// TypeDef attribute round-trips Form-A → JSON → Form-A bit-
/// identical and preserves the parsed BTreeMap through both halves,
/// including the BTreeSet's deterministic alphabetical iteration
/// order.
#[test]
fn typedef_param_in_round_trips_surface() {
let src = concat!(
"(module m\n",
" (data T (vars a)\n",
" (ctor MkT a)\n",
" (param-in (a Int Float))))\n",
);
let m = ailang_surface::parse(src).expect("Form-A parse of (param-in ...)");
let td = match &m.defs[0] {
ailang_core::ast::Def::Type(t) => t,
_ => panic!("expected Type def"),
};
let allowed = td.param_in.get("a").expect("var `a` bound in param_in");
assert!(allowed.contains("Int"));
assert!(allowed.contains("Float"));
assert_eq!(allowed.len(), 2);
let printed = ailang_surface::print(&m);
let m2 = ailang_surface::parse(&printed).expect("re-parse printed form");
let td2 = match &m2.defs[0] {
ailang_core::ast::Def::Type(t) => t,
_ => panic!("expected Type def after round-trip"),
};
assert_eq!(td2.param_in, td.param_in, "param_in survives round-trip");
}
design/INDEX.md
+1 -1
View File
@@ -108,4 +108,4 @@ is the default.
| authoring-surface | onboarding / evolves | design/models/0001-authoring-surface.md |
| prose-projection | onboarding / evolves | design/models/0006-prose-projection.md |
| pipeline | onboarding / evolves | design/models/0003-pipeline.md |
| kernel-extensions | onboarding / evolves (design accepted 2026-05-28; impl in progress) | design/models/0007-kernel-extensions.md |
| kernel-extensions | onboarding / evolves (mechanisms milestone closed 2026-05-28; raw-buf and series milestones pending) | design/models/0007-kernel-extensions.md |
design/contracts/0002-data-model.md
+3 -1
View File
@@ -17,6 +17,7 @@ contract is what makes growing the schema cheap.
{
"schema": "ailang/v0",
"name": "<id>",
"kernel": true, // optional; omitted when false (hash-stable when omitted). Kernel-tier modules are auto-imported by every consumer. See prep.3 of the kernel-extension-mechanics milestone.
"imports": [{ "module": "<id>", "as": "<id>" }],
"defs": [Def...]
}
@@ -62,7 +63,8 @@ narrative — defaults, superclasses, diagnostics — lives in
...
],
"doc": "<optional string>",
"drop-iterative": true // opt-in; omitted when false (hash-stable when omitted)
"drop-iterative": true, // opt-in; omitted when false (hash-stable when omitted)
"param-in": { "<var>": ["<TypeName>", ...] } // closed-set restriction per type variable; omitted when empty (hash-stable when omitted). See prep.3 of the kernel-extension-mechanics milestone.
}
// class (typeclass declaration; narrative in contracts/0013-typeclasses.md)
design/models/0007-kernel-extensions.md
+31 -27
View File
@@ -1,14 +1,18 @@
# Kernel extensions — plugin-style domain types whitepaper
**STATUS.** Design accepted 2026-05-28. Implementation in progress
across two Gitea milestones: `kernel-extension-mechanics` (the
language-level mechanisms) and `series` (the first concrete
consumer). This whitepaper describes the design as a coherent
whole; the per-milestone specs in `docs/specs/` carry the
implementation-level detail. As each milestone closes, sections of
this whitepaper transition from forward-looking design to
present-state description, per the
[honesty-rule](../contracts/0007-honesty-rule.md).
**STATUS.** Mechanisms milestone closed 2026-05-28
(`kernel-extension-mechanics`; iterations prep.1, prep.2, prep.3
landed). The four language-level mechanisms — type-scoped
namespacing, `Term::New`, kernel-tier modules + auto-import, and
`param-in` — are shipped and ratified by the stub kernel crate
(`crates/ailang-kernel-stub/`). The base-extension and library-
extension milestones (`raw-buf`, `series`) are pending. This
whitepaper describes the design as a coherent whole; the
per-milestone specs in `docs/specs/` carry the implementation-
level detail. Sections describing the now-shipped mechanisms read
in present-state per the
[honesty-rule](../contracts/0007-honesty-rule.md); sections about
the still-pending milestones keep their forward-looking framing.
## The problem
@@ -211,25 +215,25 @@ type lives outside core, but at the call site it feels like a
primitive. Bare `Series` in `(con Series (con Float))` without
seeing `(import series)` somewhere is the ergonomic property.
**Single mechanism.** Auto-injection is *not* a new behaviour
introduced by this design — it exists today, hardcoded to one
module name. `crates/ailang-surface/src/loader.rs:98-108`
unconditionally injects `parse_prelude()` and threads
`&["prelude"]` into `workspace::build_workspace` as the
implicit-imports list. Prelude's 12 free fns (see
`examples/prelude.ail:85-148`) are already callable bare in
every consumer module by virtue of this hardcoded path,
ratified by `crates/ail/tests/prelude_free_fns.rs`.
**Single mechanism.** Auto-injection is a single load-time hop,
generalised from a hardcoded single-name path (prelude only,
pre-prep.3) to a flag-driven multi-module mechanism (since
prep.3 of `kernel-extension-mechanics`). The loader at
`crates/ailang-surface/src/loader.rs::load_workspace` injects
`parse_prelude()` and `parse_kernel_stub()` programmatically,
then derives the implicit-imports list from
`modules.values().filter(|m| m.kernel)`. Every module in the
workspace's modules map that carries `kernel: true` enters the
auto-import set; consumers see those modules' top-level types
bare without an `(import …)` declaration.
The kernel-tier flag *generalises* this existing single-name
auto-injection into a flag-driven multi-module mechanism. After
the kernel-extensions design lands, prelude carries `kernel:
true` and the implicit-imports list is derived from the set of
all kernel-flagged modules. Consumer-observable behaviour for
prelude is unchanged; the code path is rewritten from
"hardcoded one name" to "flag-filtered all modules". Other
kernel-tier modules (the stub, future Series, future Matrix)
become auto-injected through the same path.
Prelude carries `kernel: true` in `examples/prelude.ail`. Its 12
free fns (see `examples/prelude.ail:85-148`) remain callable bare
in every consumer module — ratified by
`crates/ail/tests/prelude_free_fns.rs` across the code-path
migration. The ratifying stub kernel module
(`crates/ailang-kernel-stub/`) and any future kernel-tier
consumers (Series, Matrix) auto-import through the same filter.
Class-method dispatch (a separate mechanism — see
[method dispatch](../contracts/0016-method-dispatch.md)) is
examples/prelude.ail
+1
View File
@@ -1,4 +1,5 @@
(module prelude
(kernel)
(data Ordering
(doc "Result of a three-way comparison: LT (less than), EQ (equal), GT (greater than). Ships in milestone 23 as the codomain of Ord.compare.")
(ctor LT)