From 9339279181e09c74e552df75d97c0369a7c96443 Mon Sep 17 00:00:00 2001 From: Brummel Date: Thu, 28 May 2026 18:43:42 +0200 Subject: [PATCH] =?UTF-8?q?iter=20prep.3-kernel-tier-modules=20(DONE=209/9?= =?UTF-8?q?):=20kernel-tier=20modules=20+=20param-in=20+=20stub=20crate=20?= =?UTF-8?q?=E2=80=94=20closes=20#33?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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>` 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. --- Cargo.lock | 5 + Cargo.toml | 2 + crates/ail/src/main.rs | 12 +- crates/ail/tests/e2e.rs | 9 +- crates/ail/tests/snapshots/hello.ll | 52 +++++ crates/ail/tests/snapshots/list.ll | 52 +++++ crates/ail/tests/snapshots/max3.ll | 52 +++++ crates/ail/tests/snapshots/sum.ll | 52 +++++ crates/ail/tests/snapshots/ws_main.ll | 52 +++++ crates/ailang-check/src/lib.rs | 188 ++++++++++++++++++ crates/ailang-check/src/linearity.rs | 16 ++ crates/ailang-check/src/reuse_shape.rs | 5 + crates/ailang-check/src/suppress_filter.rs | 1 + crates/ailang-check/src/uniqueness.rs | 5 + .../ailang-check/tests/duplicate_ctor_pin.rs | 3 + crates/ailang-check/tests/workspace.rs | 10 + crates/ailang-codegen/src/lib.rs | 22 ++ crates/ailang-core/src/ast.rs | 31 +++ crates/ailang-core/src/desugar.rs | 16 ++ crates/ailang-core/src/pretty.rs | 1 + crates/ailang-core/src/workspace.rs | 25 ++- .../ailang-core/tests/design_schema_drift.rs | 135 ++++++++++++- crates/ailang-core/tests/spec_drift.rs | 3 + crates/ailang-core/tests/workspace_kernel.rs | 162 +++++++++++++++ crates/ailang-kernel-stub/Cargo.toml | 7 + crates/ailang-kernel-stub/src/lib.rs | 27 +++ crates/ailang-prose/src/lib.rs | 9 + crates/ailang-surface/Cargo.toml | 1 + crates/ailang-surface/src/lib.rs | 2 +- crates/ailang-surface/src/loader.rs | 45 ++++- crates/ailang-surface/src/parse.rs | 74 ++++++- crates/ailang-surface/src/print.rs | 29 +++ .../tests/prelude_module_hash_pin.rs | 11 +- crates/ailang-surface/tests/round_trip.rs | 51 +++++ design/INDEX.md | 2 +- design/contracts/0002-data-model.md | 4 +- design/models/0007-kernel-extensions.md | 58 +++--- examples/prelude.ail | 1 + 38 files changed, 1185 insertions(+), 47 deletions(-) create mode 100644 crates/ailang-core/tests/workspace_kernel.rs create mode 100644 crates/ailang-kernel-stub/Cargo.toml create mode 100644 crates/ailang-kernel-stub/src/lib.rs diff --git a/Cargo.lock b/Cargo.lock index 2c135bf..4cc62ab 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -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", diff --git a/Cargo.toml b/Cargo.toml index ae317ff..f26a2ed 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -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" } diff --git a/crates/ail/src/main.rs b/crates/ail/src/main.rs index 29cd808..3f70ae0 100644 --- a/crates/ail/src/main.rs +++ b/crates/ail/src/main.rs @@ -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!({ diff --git a/crates/ail/tests/e2e.rs b/crates/ail/tests/e2e.rs index 0284a3c..4a1fe94 100644 --- a/crates/ail/tests/e2e.rs +++ b/crates/ail/tests/e2e.rs @@ -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 diff --git a/crates/ail/tests/snapshots/hello.ll b/crates/ail/tests/snapshots/hello.ll index 25001ec..35bfdbe 100644 --- a/crates/ail/tests/snapshots/hello.ll +++ b/crates/ail/tests/snapshots/hello.ll @@ -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 diff --git a/crates/ail/tests/snapshots/list.ll b/crates/ail/tests/snapshots/list.ll index 73cf0da..5d5a167 100644 --- a/crates/ail/tests/snapshots/list.ll +++ b/crates/ail/tests/snapshots/list.ll @@ -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 diff --git a/crates/ail/tests/snapshots/max3.ll b/crates/ail/tests/snapshots/max3.ll index d020f5d..56b21d8 100644 --- a/crates/ail/tests/snapshots/max3.ll +++ b/crates/ail/tests/snapshots/max3.ll @@ -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) diff --git a/crates/ail/tests/snapshots/sum.ll b/crates/ail/tests/snapshots/sum.ll index 297620b..e6ccdd9 100644 --- a/crates/ail/tests/snapshots/sum.ll +++ b/crates/ail/tests/snapshots/sum.ll @@ -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 diff --git a/crates/ail/tests/snapshots/ws_main.ll b/crates/ail/tests/snapshots/ws_main.ll index b30876c..f3ec33f 100644 --- a/crates/ail/tests/snapshots/ws_main.ll +++ b/crates/ail/tests/snapshots/ws_main.ll @@ -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 diff --git a/crates/ailang-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 0e94a9b..d40a949 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -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, + }, + /// 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 = 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:?}" + ); + } } diff --git a/crates/ailang-check/src/linearity.rs b/crates/ailang-check/src/linearity.rs index f4ba739..2515c72 100644 --- a/crates/ailang-check/src/linearity.rs +++ b/crates/ailang-check/src/linearity.rs @@ -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, 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], }; diff --git a/crates/ailang-check/src/reuse_shape.rs b/crates/ailang-check/src/reuse_shape.rs index 7acf907..e08415b 100644 --- a/crates/ailang-check/src/reuse_shape.rs +++ b/crates/ailang-check/src/reuse_shape.rs @@ -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()), diff --git a/crates/ailang-check/src/suppress_filter.rs b/crates/ailang-check/src/suppress_filter.rs index 893d51e..422dd4c 100644 --- a/crates/ailang-check/src/suppress_filter.rs +++ b/crates/ailang-check/src/suppress_filter.rs @@ -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(), diff --git a/crates/ailang-check/src/uniqueness.rs b/crates/ailang-check/src/uniqueness.rs index c6994d7..0ed7590 100644 --- a/crates/ailang-check/src/uniqueness.rs +++ b/crates/ailang-check/src/uniqueness.rs @@ -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)], }; diff --git a/crates/ailang-check/tests/duplicate_ctor_pin.rs b/crates/ailang-check/tests/duplicate_ctor_pin.rs index 7116e12..7a64733 100644 --- a/crates/ailang-check/tests/duplicate_ctor_pin.rs +++ b/crates/ailang-check/tests/duplicate_ctor_pin.rs @@ -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(), }), ], }; diff --git a/crates/ailang-check/tests/workspace.rs b/crates/ailang-check/tests/workspace.rs index 2e16dc1..26b1394 100644 --- a/crates/ailang-check/tests/workspace.rs +++ b/crates/ailang-check/tests/workspace.rs @@ -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], }; diff --git a/crates/ailang-codegen/src/lib.rs b/crates/ailang-codegen/src/lib.rs index edcb121..fce5223 100644 --- a/crates/ailang-codegen/src/lib.rs +++ b/crates/ailang-codegen/src/lib.rs @@ -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(), diff --git a/crates/ailang-core/src/ast.rs b/crates/ailang-core/src/ast.rs index 3d9eb1e..c679dab 100644 --- a/crates/ailang-core/src/ast.rs +++ b/crates/ailang-core/src/ast.rs @@ -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 { /// (`.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 /// `/.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: , args }` carries an + /// `args[i]` whose outermost type-name lies in the restricted + /// set for that variable. + /// + /// Serialised as `"param-in": { "": ["", ...] }` + /// (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>, } diff --git a/crates/ailang-core/src/desugar.rs b/crates/ailang-core/src/desugar.rs index 2da44a4..f4e0dbb 100644 --- a/crates/ailang-core/src/desugar.rs +++ b/crates/ailang-core/src/desugar.rs @@ -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(), diff --git a/crates/ailang-core/src/pretty.rs b/crates/ailang-core/src/pretty.rs index 22fc3bc..c44195c 100644 --- a/crates/ailang-core/src/pretty.rs +++ b/crates/ailang-core/src/pretty.rs @@ -169,6 +169,7 @@ mod tests { Module { schema: crate::SCHEMA.into(), name: "sample".into(), + kernel: false, imports: vec![], defs: vec![ Def::Fn(FnDef { diff --git a/crates/ailang-core/src/workspace.rs b/crates/ailang-core/src/workspace.rs index 73428b8..46393d9 100644 --- a/crates/ailang-core/src/workspace.rs +++ b/crates/ailang-core/src/workspace.rs @@ -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) diff --git a/crates/ailang-core/tests/design_schema_drift.rs b/crates/ailang-core/tests/design_schema_drift.rs index d647c01..6c0e8d0 100644 --- a/crates/ailang-core/tests/design_schema_drift.rs +++ b/crates/ailang-core/tests/design_schema_drift.rs @@ -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> = 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")); +} diff --git a/crates/ailang-core/tests/spec_drift.rs b/crates/ailang-core/tests/spec_drift.rs index 6f76d14..528aa02 100644 --- a/crates/ailang-core/tests/spec_drift.rs +++ b/crates/ailang-core/tests/spec_drift.rs @@ -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)), diff --git a/crates/ailang-core/tests/workspace_kernel.rs b/crates/ailang-core/tests/workspace_kernel.rs new file mode 100644 index 0000000..ff32dc8 --- /dev/null +++ b/crates/ailang-core/tests/workspace_kernel.rs @@ -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); +} diff --git a/crates/ailang-kernel-stub/Cargo.toml b/crates/ailang-kernel-stub/Cargo.toml new file mode 100644 index 0000000..599bee4 --- /dev/null +++ b/crates/ailang-kernel-stub/Cargo.toml @@ -0,0 +1,7 @@ +[package] +name = "ailang-kernel-stub" +version.workspace = true +edition.workspace = true +license.workspace = true + +[dependencies] diff --git a/crates/ailang-kernel-stub/src/lib.rs b/crates/ailang-kernel-stub/src/lib.rs new file mode 100644 index 0000000..6509b9e --- /dev/null +++ b/crates/ailang-kernel-stub/src/lib.rs @@ -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)))) +"#; diff --git a/crates/ailang-prose/src/lib.rs b/crates/ailang-prose/src/lib.rs index ec2cf9a..adc0297 100644 --- a/crates/ailang-prose/src/lib.rs +++ b/crates/ailang-prose/src/lib.rs @@ -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(), diff --git a/crates/ailang-surface/Cargo.toml b/crates/ailang-surface/Cargo.toml index 76536d1..edc7277 100644 --- a/crates/ailang-surface/Cargo.toml +++ b/crates/ailang-surface/Cargo.toml @@ -6,6 +6,7 @@ license.workspace = true [dependencies] ailang-core.workspace = true +ailang-kernel-stub.workspace = true serde_json.workspace = true thiserror.workspace = true diff --git a/crates/ailang-surface/src/lib.rs b/crates/ailang-surface/src/lib.rs index 69c8192..581ef01 100644 --- a/crates/ailang-surface/src/lib.rs +++ b/crates/ailang-surface/src/lib.rs @@ -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}; diff --git a/crates/ailang-surface/src/loader.rs b/crates/ailang-surface/src/loader.rs index 0f8d455..5a89f31 100644 --- a/crates/ailang-surface/src/loader.rs +++ b/crates/ailang-surface/src/loader.rs @@ -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 { pub fn load_workspace(entry: &Path) -> Result { 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 = 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, ) } diff --git a/crates/ailang-surface/src/parse.rs b/crates/ailang-surface/src/parse.rs index 7e8f3f5..87f31a4 100644 --- a/crates/ailang-surface/src/parse.rs +++ b/crates/ailang-surface/src/parse.rs @@ -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 = Vec::new(); let mut defs: Vec = 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 = None; let mut ctors: Vec = Vec::new(); let mut drop_iterative = false; + let mut param_in: BTreeMap> = 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 = 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, }) } diff --git a/crates/ailang-surface/src/print.rs b/crates/ailang-surface/src/print.rs index 60bccc3..6d8aa58 100644 --- a/crates/ailang-surface/src/print.rs +++ b/crates/ailang-surface/src/print.rs @@ -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(), diff --git a/crates/ailang-surface/tests/prelude_module_hash_pin.rs b/crates/ailang-surface/tests/prelude_module_hash_pin.rs index 1ee0cc0..622cb96 100644 --- a/crates/ailang-surface/tests/prelude_module_hash_pin.rs +++ b/crates/ailang-surface/tests/prelude_module_hash_pin.rs @@ -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." ); diff --git a/crates/ailang-surface/tests/round_trip.rs b/crates/ailang-surface/tests/round_trip.rs index e27f7fb..258afb5 100644 --- a/crates/ailang-surface/tests/round_trip.rs +++ b/crates/ailang-surface/tests/round_trip.rs @@ -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"); +} diff --git a/design/INDEX.md b/design/INDEX.md index 681ac49..7fe92c9 100644 --- a/design/INDEX.md +++ b/design/INDEX.md @@ -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 | diff --git a/design/contracts/0002-data-model.md b/design/contracts/0002-data-model.md index 01266c1..ce85248 100644 --- a/design/contracts/0002-data-model.md +++ b/design/contracts/0002-data-model.md @@ -17,6 +17,7 @@ contract is what makes growing the schema cheap. { "schema": "ailang/v0", "name": "", + "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": "", "as": "" }], "defs": [Def...] } @@ -62,7 +63,8 @@ narrative — defaults, superclasses, diagnostics — lives in ... ], "doc": "", - "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": { "": ["", ...] } // 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) diff --git a/design/models/0007-kernel-extensions.md b/design/models/0007-kernel-extensions.md index 8b6ea88..d14878a 100644 --- a/design/models/0007-kernel-extensions.md +++ b/design/models/0007-kernel-extensions.md @@ -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 diff --git a/examples/prelude.ail b/examples/prelude.ail index e00283e..139f7ab 100644 --- a/examples/prelude.ail +++ b/examples/prelude.ail @@ -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)