iter raw-buf.6 kernel-stub-retirement (DONE 5/5): retire the stub, raw_buf is the sole base extension (refs #7)

Closes the raw-buf milestone. raw_buf (shipped raw-buf.1-.5; the
owned-drop resolution landed under bug #42/#43) has subsumed every
ratification role kernel_stub held -- Term::New end-to-end, the
param-in reject, kernel-tier auto-import, the monomorphic intrinsic
path, and the type-scoped polymorphic intrinsic mechanism (RawBuf's
four ops). The stub is now redundant; this iteration removes it.

Pure removal (-636/+49 across 22 files, 7 deleted):
- Rust surface: drop `mod kernel_stub` + `STUB_AIL` re-export
  (ailang-kernel), `parse_kernel_stub` + its workspace injection
  (ailang-surface), the `answer` + two `StubT_peek__{Int,Float}`
  INTERCEPTS entries + their three emit fns (ailang-codegen). The
  (intrinsic) markers leave with the deleted source, so the
  marker<->entry bijection holds in lockstep.
- Source + tests: delete crates/ailang-kernel/src/kernel_stub/,
  kernel_stub_module_round_trips, the two stub-consumer e2e tests,
  and mono_scoped_symbol.rs (its scope-qualified-mono mechanism is
  now pinned by RawBuf's ops + the intercepts bijection).
- Fixtures: delete kernel_answer.ail, new_stubt_smoke.ail,
  peek_mono_pin_smoke.ail, and fieldtest kem_3_stub_consumer.ail
  (referenced the deleted StubT; documented a since-fixed bug).
- Pins: re-baseline both workspace-count content-pins 5 -> 4
  (workspace_pin.rs + the e2e.rs twin) and regenerate all five IR
  snapshots (400 stub-IR lines removed; no user IR changed -- the
  stub auto-injected into every build).
- Ledger: design/INDEX.md + design/models/0007 to present-state
  (raw_buf is the live ratifier; raw-buf milestone shipped, series
  pending), plus architecture-comment sweep across workspace.rs,
  mono.rs, check/codegen lib.rs, workspace_kernel.rs.

Scope decisions (orchestrator, pre-plan): the self-contained inline
serde_json check-layer fixtures in ailang-check/src/lib.rs keep their
incidental StubT/kernel_stub sample names (they construct what they
reference; not stub-ratification) -- the one permitted residual.
kem_4 fieldtest kept (uses a user NumBox ADT, comment-only edit).
hash.rs `name: "answer"` left (generic serde doc example).

Plan-gap caught at implement: the planner's verbatim edit list
under-enumerated four honesty sites; one (mono.rs:562) carried a
literal `StubT_peek__Int` -- a hard-gate symbol the verbatim list
missed, which would have failed Task 4's removal gate. Filled
(comment-only, no behaviour). Confirms the planner self-review
filter-completeness risk; the implement gate caught it.

Verification: full workspace suite green (0 failed); hard symbol gate
(STUB_AIL|parse_kernel_stub|emit_answer|emit_stubt_peek|StubT_peek__)
zero matches across crates/ examples/ design/; soft gate residual only
the kept inline fixtures; kernel crate is lib.rs + raw_buf/ only.
Regression: compile_check 24/24 stable (exit 0; uniform downward
check_ms within tol -- stub no longer parsed per compile), cross_lang
25/25, check 34/34 stable (exit 0; an earlier exit-1 on
rc_over_bump was machine-load ratio noise -- denominator bump_s got
faster, rc_s also improved -- confirmed green on re-run, not
baselined).
This commit is contained in:
2026-05-30 16:07:29 +02:00
parent fb0dd92a6c
commit 13e590cb46
27 changed files with 49 additions and 764 deletions
+4 -30
View File
@@ -82,30 +82,6 @@ fn sum_1_to_10_is_55() {
assert_eq!(stdout.trim(), "55");
}
/// Property protected: a kernel-tier `(intrinsic)` fn builds and runs
/// from source to native via the codegen intercept registry. The
/// `kernel_stub.answer` intrinsic (body `Term::Intrinsic`, intercept
/// `emit_answer` → `ret i64 42`) is consumed by a user module and its
/// value reaches stdout. This is the end-to-end ratifier for the whole
/// Term::Intrinsic mechanism: parse → signature-only typecheck →
/// mono-skip → intercept-routed codegen → native 42.
#[test]
fn answer_intrinsic_builds_and_runs_printing_42() {
let out = build_and_run("kernel_answer.ail");
assert_eq!(out.trim(), "42");
}
/// raw-buf.4: the general `Term::New` desugar. `(new StubT 42)`
/// desugars to `(app StubT.new 42)` (StubT.new has a real
/// `(term-ctor StubT Stub x)` body, so it builds independent of
/// RawBuf), the Int is matched back out and printed. Ratifies the
/// desugar + the removal of both codegen `Term::New` deferral arms.
#[test]
fn new_stubt_builds_and_runs() {
let out = build_and_run("new_stubt_smoke.ail");
assert_eq!(out.trim(), "42");
}
#[test]
fn loop_recur_sum_to_runs_to_value() {
let stdout = build_and_run("loop_sum_to_run.ail");
@@ -875,11 +851,10 @@ fn workspace_lists_imported_modules() {
let modules = v["modules"].as_array().expect("modules must be array");
// the loader auto-injects every built-in kernel-tier module
// (`prelude`; since prep.3 of the kernel-extension-mechanics
// milestone, the ratifying `kernel_stub`; and since raw-buf.4 the
// first real-payload kernel extension `raw_buf`), so the count is
// the user's two modules plus the three built-ins.
assert_eq!(modules.len(), 5, "expected 5 modules: {stdout}");
// (`prelude` and, since raw-buf.4, the first real-payload kernel
// extension `raw_buf`), 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()
@@ -888,7 +863,6 @@ 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:?}");
assert!(names.contains(&"raw_buf"), "raw_buf missing: {names:?}");
}
-49
View File
@@ -1,49 +0,0 @@
//! raw-buf.3: a type-scoped polymorphic intrinsic call `StubT.peek`
//! monomorphises to the scope-qualified symbol `StubT_peek__<elem>`
//! (not the bare `peek__<elem>`). Proves the scope threads
//! resolution → FreeFnCall → MonoTarget → mint. No codegen / no
//! Term::New: assertion is on the monomorphised def names.
use ailang_core::ast::Def;
use ailang_surface::load_workspace;
use std::path::PathBuf;
fn fixture_path() -> PathBuf {
let mut d = PathBuf::from(env!("CARGO_MANIFEST_DIR"));
d.pop();
d.pop();
d.join("examples").join("peek_mono_pin_smoke.ail")
}
#[test]
fn stubt_peek_monomorphises_to_scope_qualified_symbols() {
let ws = load_workspace(&fixture_path()).expect("workspace loads");
let diags = ailang_check::check_workspace(&ws);
assert!(diags.is_empty(), "typecheck diagnostics: {diags:?}");
let post_mono = ailang_check::monomorphise_workspace(&ws).expect("mono green");
// Free-fn mono defs are appended to the polymorphic source's
// defining module — `kernel_stub`, where `peek` lives.
let names: Vec<String> = post_mono
.modules
.values()
.flat_map(|m| m.defs.iter())
.filter_map(|d| match d {
Def::Fn(f) => Some(f.name.clone()),
_ => None,
})
.collect();
assert!(
names.iter().any(|n| n == "StubT_peek__Int"),
"expected scope-qualified StubT_peek__Int; got: {names:?}"
);
assert!(
names.iter().any(|n| n == "StubT_peek__Float"),
"expected scope-qualified StubT_peek__Float; got: {names:?}"
);
assert!(
!names.iter().any(|n| n == "peek__Int"),
"bare peek__Int must NOT be minted (scope-qualified only)"
);
}
-80
View File
@@ -25,8 +25,6 @@ declare ptr @ailang_str_concat(ptr, ptr)
declare i64 @llvm.fptosi.sat.i64.f64(double)
@ail_hello_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_hello_main_adapter, ptr null }
@ail_kernel_stub_new_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_kernel_stub_new_adapter, ptr null }
@ail_kernel_stub_answer_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_kernel_stub_answer_adapter, ptr null }
@ail_prelude_float_eq_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_eq_adapter, ptr null }
@ail_prelude_float_ne_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_ne_adapter, ptr null }
@ail_prelude_float_lt_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_lt_adapter, ptr null }
@@ -47,84 +45,6 @@ entry:
ret i8 %r
}
define ptr @ail_kernel_stub_new(i64 %arg_x) {
entry:
%v1 = call ptr @ailang_rc_alloc(i64 16)
store i64 0, ptr %v1, align 8
%v2 = getelementptr inbounds i8, ptr %v1, i64 8
store i64 %arg_x, ptr %v2, align 8
ret ptr %v1
}
define ptr @ail_kernel_stub_new_adapter(ptr %_env, i64 %a0) {
entry:
%r = call ptr @ail_kernel_stub_new(i64 %a0)
ret ptr %r
}
define i64 @ail_kernel_stub_answer() {
entry:
ret i64 42
}
define i64 @ail_kernel_stub_answer_adapter(ptr %_env) {
entry:
%r = call i64 @ail_kernel_stub_answer()
ret i64 %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
-80
View File
@@ -22,8 +22,6 @@ declare ptr @ailang_str_clone(ptr)
declare ptr @ailang_str_concat(ptr, ptr)
declare i64 @llvm.fptosi.sat.i64.f64(double)
@ail_kernel_stub_new_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_kernel_stub_new_adapter, ptr null }
@ail_kernel_stub_answer_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_kernel_stub_answer_adapter, ptr null }
@ail_list_sum_list_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_list_sum_list_adapter, ptr null }
@ail_list_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_list_main_adapter, ptr null }
@ail_prelude_float_eq_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_eq_adapter, ptr null }
@@ -34,84 +32,6 @@ 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 ptr @ail_kernel_stub_new(i64 %arg_x) {
entry:
%v1 = call ptr @ailang_rc_alloc(i64 16)
store i64 0, ptr %v1, align 8
%v2 = getelementptr inbounds i8, ptr %v1, i64 8
store i64 %arg_x, ptr %v2, align 8
ret ptr %v1
}
define ptr @ail_kernel_stub_new_adapter(ptr %_env, i64 %a0) {
entry:
%r = call ptr @ail_kernel_stub_new(i64 %a0)
ret ptr %r
}
define i64 @ail_kernel_stub_answer() {
entry:
ret i64 42
}
define i64 @ail_kernel_stub_answer_adapter(ptr %_env) {
entry:
%r = call i64 @ail_kernel_stub_answer()
ret i64 %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 i64 @ail_list_sum_list(ptr %arg_xs) {
entry:
%v1 = load i64, ptr %arg_xs, align 8
-80
View File
@@ -22,8 +22,6 @@ declare ptr @ailang_str_clone(ptr)
declare ptr @ailang_str_concat(ptr, ptr)
declare i64 @llvm.fptosi.sat.i64.f64(double)
@ail_kernel_stub_new_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_kernel_stub_new_adapter, ptr null }
@ail_kernel_stub_answer_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_kernel_stub_answer_adapter, ptr null }
@ail_max3_max_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_max3_max_adapter, ptr null }
@ail_max3_max3_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_max3_max3_adapter, ptr null }
@ail_max3_main_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_max3_main_adapter, ptr null }
@@ -37,84 +35,6 @@ 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 ptr @ail_kernel_stub_new(i64 %arg_x) {
entry:
%v1 = call ptr @ailang_rc_alloc(i64 16)
store i64 0, ptr %v1, align 8
%v2 = getelementptr inbounds i8, ptr %v1, i64 8
store i64 %arg_x, ptr %v2, align 8
ret ptr %v1
}
define ptr @ail_kernel_stub_new_adapter(ptr %_env, i64 %a0) {
entry:
%r = call ptr @ail_kernel_stub_new(i64 %a0)
ret ptr %r
}
define i64 @ail_kernel_stub_answer() {
entry:
ret i64 42
}
define i64 @ail_kernel_stub_answer_adapter(ptr %_env) {
entry:
%r = call i64 @ail_kernel_stub_answer()
ret i64 %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 i64 @ail_max3_max(i64 %arg_a, i64 %arg_b) {
entry:
%v1 = call i1 @ail_prelude_gt__Int(i64 %arg_a, i64 %arg_b)
-80
View File
@@ -22,8 +22,6 @@ declare ptr @ailang_str_clone(ptr)
declare ptr @ailang_str_concat(ptr, ptr)
declare i64 @llvm.fptosi.sat.i64.f64(double)
@ail_kernel_stub_new_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_kernel_stub_new_adapter, ptr null }
@ail_kernel_stub_answer_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_kernel_stub_answer_adapter, ptr null }
@ail_prelude_float_eq_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_eq_adapter, ptr null }
@ail_prelude_float_ne_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_ne_adapter, ptr null }
@ail_prelude_float_lt_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_lt_adapter, ptr null }
@@ -35,84 +33,6 @@ 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 ptr @ail_kernel_stub_new(i64 %arg_x) {
entry:
%v1 = call ptr @ailang_rc_alloc(i64 16)
store i64 0, ptr %v1, align 8
%v2 = getelementptr inbounds i8, ptr %v1, i64 8
store i64 %arg_x, ptr %v2, align 8
ret ptr %v1
}
define ptr @ail_kernel_stub_new_adapter(ptr %_env, i64 %a0) {
entry:
%r = call ptr @ail_kernel_stub_new(i64 %a0)
ret ptr %r
}
define i64 @ail_kernel_stub_answer() {
entry:
ret i64 42
}
define i64 @ail_kernel_stub_answer_adapter(ptr %_env) {
entry:
%r = call i64 @ail_kernel_stub_answer()
ret i64 %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
-80
View File
@@ -22,8 +22,6 @@ declare ptr @ailang_str_clone(ptr)
declare ptr @ailang_str_concat(ptr, ptr)
declare i64 @llvm.fptosi.sat.i64.f64(double)
@ail_kernel_stub_new_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_kernel_stub_new_adapter, ptr null }
@ail_kernel_stub_answer_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_kernel_stub_answer_adapter, ptr null }
@ail_prelude_float_eq_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_eq_adapter, ptr null }
@ail_prelude_float_ne_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_ne_adapter, ptr null }
@ail_prelude_float_lt_clos = private unnamed_addr constant { ptr, ptr } { ptr @ail_prelude_float_lt_adapter, ptr null }
@@ -34,84 +32,6 @@ 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 ptr @ail_kernel_stub_new(i64 %arg_x) {
entry:
%v1 = call ptr @ailang_rc_alloc(i64 16)
store i64 0, ptr %v1, align 8
%v2 = getelementptr inbounds i8, ptr %v1, i64 8
store i64 %arg_x, ptr %v2, align 8
ret ptr %v1
}
define ptr @ail_kernel_stub_new_adapter(ptr %_env, i64 %a0) {
entry:
%r = call ptr @ail_kernel_stub_new(i64 %a0)
ret ptr %r
}
define i64 @ail_kernel_stub_answer() {
entry:
ret i64 42
}
define i64 @ail_kernel_stub_answer_adapter(ptr %_env) {
entry:
%r = call i64 @ail_kernel_stub_answer()
ret i64 %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
+8 -8
View File
@@ -1083,7 +1083,7 @@ pub fn prepare_workspace_for_check(ws: &Workspace) -> Workspace {
.collect();
// raw-buf.4: per-module set of *monomorphic* (non-`Forall`)
// top-level fn names. A type-scoped call `T.f` to a monomorphic
// op (e.g. the `kernel_stub.StubT.new` produced by the Term::New
// op (e.g. the `raw_buf.RawBuf.new` produced by the Term::New
// desugar) is normalised to the module-qualified `<home>.f` form
// by `qualify_workspace_term` — codegen recognises that spelling
// directly. Polymorphic type-scoped ops stay in the `T.f` form so
@@ -1701,11 +1701,11 @@ pub fn build_check_env(ws: &Workspace) -> Env {
// (`modules.filter(|m| m.kernel)`) that drives
// `implicit_imports` into `build_workspace`. The pre-pass
// `qualify_workspace_types` freely produces qualifiers like
// `kernel_stub.StubT`; without this injection the type-
// validity check at ~line 1968 would reject `kernel_stub` as
// `raw_buf.RawBuf`; without this injection the type-
// validity check at ~line 1968 would reject `raw_buf` as
// an unknown module prefix. Fieldtest F3 surfaced the gap
// (the previous code force-injected only `prelude`, leaving
// `kernel_stub` and any future kernel-tier module unreachable
// `raw_buf` and any future kernel-tier module unreachable
// from consumers). The production prelude carries
// `kernel: true`, so the two halves are idempotent for it; the
// `"prelude"` literal stays so unit-test workspaces that
@@ -1865,7 +1865,7 @@ fn check_in_workspace(
// explicit `import` of the same name is idempotent via
// `entry`. A module is not auto-imported into its own body.
// Fieldtest F3 surfaced that the previous code force-injected
// only `prelude`, leaving `kernel_stub` and any future
// only `prelude`, leaving `raw_buf` and any future
// kernel-tier module unreachable from consumers even though
// the pre-pass freely produces such qualifiers.
if m.name != "prelude" {
@@ -2782,8 +2782,8 @@ pub struct FreeFnCall {
/// substitution was fully pinned.
pub metas: Vec<Type>,
/// The TypeDef scope the call resolved through, when it was
/// spelled type-scoped (`T.f`, prep.1) — `Some("StubT")` for
/// `StubT.peek`, `Some("RawBuf")` for `RawBuf.get`. `None` for a
/// spelled type-scoped (`T.f`, prep.1) — `Some("RawBuf")` for
/// `RawBuf.new`, `Some("RawBuf")` for `RawBuf.get`. `None` for a
/// bare / dot-qualified / local resolution. raw-buf.3: drives the
/// scope-qualified mono symbol `T_f__<elem>` so two types' ops
/// of the same name never collide.
@@ -4615,7 +4615,7 @@ pub(crate) fn qualify_workspace_term(
// `T.f` to a *monomorphic* op into the module-qualified
// `<home>.f` form. The Term::New desugar emits
// `(app T.new …)` for every type; for a cross-module
// monomorphic `new` (e.g. kernel_stub's StubT.new) nothing
// monomorphic `new` (e.g. raw_buf's RawBuf.new) nothing
// downstream rewrites the `T.new` callee, so codegen would
// hit `unknown variable`. Three carve-outs:
// - a same-module type (`own_local_types`) keeps `T.f` —
+6 -6
View File
@@ -366,9 +366,9 @@ fn poly_free_fn_names_for_module(
// local def, not the imported poly fn. Adding the bare name here
// anyway would make `rewrite_mono_calls` treat the local call as a
// poly-free-fn site and over-advance the slot cursor (surfaced when
// kernel_stub gained a `peek` colliding with a fixture-local
// monomorphic `peek`). The dot-qualified / type-scoped spellings
// are unambiguous and stay unconditional.
// a kernel-tier type-scoped op collided with a fixture-local
// monomorphic fn of the same bare name). The dot-qualified /
// type-scoped spellings are unambiguous and stay unconditional.
let local_global_names: BTreeSet<String> = env
.module_globals
.get(mname)
@@ -558,8 +558,8 @@ pub fn mono_symbol_n(base: &str, types: &[Type]) -> String {
}
/// raw-buf.3: the symbol base for a free-fn mono target. A
/// type-scoped op (`scope = Some("StubT")`, name `"peek"`) bases on
/// `"StubT_peek"`, so `mono_symbol_n` mints `StubT_peek__Int`; a
/// type-scoped op (`scope = Some("RawBuf")`, name `"get"`) bases on
/// `"RawBuf_get"`, so `mono_symbol_n` mints `RawBuf_get__Int`; a
/// bare free fn (`scope = None`) keeps its bare base.
pub fn scoped_base(scope: &Option<String>, name: &str) -> String {
match scope {
@@ -622,7 +622,7 @@ pub enum MonoTarget {
/// Module in which the polymorphic source `Def::Fn` is declared;
/// the synthesised mono `Def::Fn` is appended there.
defining_module: String,
/// The TypeDef scope (`Some("StubT")`) when the call resolved
/// The TypeDef scope (`Some("RawBuf")`) when the call resolved
/// type-scoped; `None` for a bare free fn. Part of the dedup
/// key and the minted symbol base.
scope: Option<String>,
+2 -62
View File
@@ -164,27 +164,6 @@ pub(crate) static INTERCEPTS: &[Intercept] = &[
wants_alwaysinline: true,
emit: emit_ne_int,
},
Intercept {
name: "answer",
expected_params: &[],
expected_ret: "i64",
wants_alwaysinline: false,
emit: emit_answer,
},
Intercept {
name: "StubT_peek__Int",
expected_params: &["ptr"], // borrow (con StubT Int) lowers to ptr
expected_ret: "i64",
wants_alwaysinline: false,
emit: emit_stubt_peek_int,
},
Intercept {
name: "StubT_peek__Float",
expected_params: &["ptr"],
expected_ret: "double",
wants_alwaysinline: false,
emit: emit_stubt_peek_float,
},
// raw-buf.4: the 12 scope-qualified RawBuf ops. Symbols are
// `RawBuf_{new,get,set,size}__{Int,Float,Bool}` (raw-buf.3
// scope-qualified mono mangling). Slab layout:
@@ -552,44 +531,6 @@ pub(crate) fn emit_ne_int(emitter: &mut Emitter<'_>) -> Result<()> {
.map(|_| ())
}
/// Ratifier intrinsic for intrinsic-bodies.1: `answer : () -> Int`
/// returns the constant 42. Exercises the Term::Intrinsic → registry
/// route end-to-end. May be retired once a real kernel-tier intrinsic
/// (raw-buf) lands.
pub(crate) fn emit_answer(emitter: &mut Emitter<'_>) -> Result<()> {
emitter.body.push_str(" ret i64 42\n");
emitter.body.push_str("}\n\n");
emitter.block_terminated = true;
Ok(())
}
/// raw-buf.3 ratifier emit. NOTE: never instantiated to codegen this
/// iteration (no Term::New to build a StubT; unit-test-ratified only).
/// The load offset/correctness is exercised end-to-end only by
/// raw-buf.4's RawBuf path; here the entry exists to satisfy the
/// bijection. Retires with the stub in raw-buf.5.
pub(crate) fn emit_stubt_peek_int(emitter: &mut Emitter<'_>) -> Result<()> {
let n = emitter.locals.len();
let s = emitter.locals[n - 1].1.clone();
let v = emitter.fresh_ssa();
emitter.body.push_str(&format!(" {v} = load i64, ptr {s}\n"));
emitter.body.push_str(&format!(" ret i64 {v}\n"));
emitter.body.push_str("}\n\n");
emitter.block_terminated = true;
Ok(())
}
pub(crate) fn emit_stubt_peek_float(emitter: &mut Emitter<'_>) -> Result<()> {
let n = emitter.locals.len();
let s = emitter.locals[n - 1].1.clone();
let v = emitter.fresh_ssa();
emitter.body.push_str(&format!(" {v} = load double, ptr {s}\n"));
emitter.body.push_str(&format!(" ret double {v}\n"));
emitter.body.push_str("}\n\n");
emitter.block_terminated = true;
Ok(())
}
// ---------------------------------------------------------------
// raw-buf.4: RawBuf op emits over an `@ailang_rc_alloc` slab.
// Slab layout `[ size:i64 @0 ][ elem_0 @8 ][ elem_1 @8+w ]…`. The
@@ -808,13 +749,12 @@ mod tests {
&["lt__Int", "le__Int", "gt__Int", "ge__Int", "ne__Int"];
/// Collect the mangled name of every `(intrinsic)` marker reachable
/// in the kernel-tier source modules (prelude + kernel_stub — the
/// in the kernel-tier source modules (prelude + raw_buf — the
/// only modules where an intrinsic body is legal today).
fn workspace_intrinsic_markers() -> BTreeSet<String> {
let mut markers = BTreeSet::new();
for module in [
ailang_surface::parse_prelude(),
ailang_surface::parse_kernel_stub(),
ailang_surface::parse_raw_buf(),
] {
for def in &module.defs {
@@ -848,7 +788,7 @@ mod tests {
}
}
// Top-level intrinsic fn: name is already the symbol
// (float_eq, answer, ...).
// (float_eq, ...).
Def::Fn(f) if matches!(f.body, Term::Intrinsic) => {
markers.insert(f.name.clone());
}
+5 -3
View File
@@ -1109,9 +1109,11 @@ impl<'a> Emitter<'a> {
// drop instead: a single rc-dec on the slab pointer
// (primitive elements carry no recursive drops).
// This distinguishes RawBuf (intrinsic `new`) from
// StubT (real-body `new` → generic ADT drop), where
// a param_in heuristic would misclassify StubT
// (also param_in). A matching flat partial-drop is
// an ordinary param_in user ADT (real-body `new` →
// generic ADT drop), where a param_in heuristic
// would misclassify the user ADT (also param_in).
// The intrinsic-`new` test is the load-bearing
// signal, not param_in. A matching flat partial-drop is
// emitted for symbol-resolution parity with the
// generic path (no carve-out site can actually
// target it — the sole field is a primitive).
+3 -4
View File
@@ -306,10 +306,9 @@ pub enum WorkspaceLoadError {
/// 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).
/// The current built-in set is `prelude` and `raw_buf` (the
/// `raw_buf` base extension is injected unconditionally in all
/// builds; future base extensions may add more).
/// 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.
@@ -733,48 +733,10 @@ fn typedef_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"));
// raw-buf.3: the type-scoped polymorphic intrinsic ratifier op
// round-trips and is an `(intrinsic)` marker.
let peek = recovered.defs.iter().find_map(|d| match d {
Def::Fn(f) if f.name == "peek" => Some(f),
_ => None,
}).expect("kernel_stub ships the peek ratifier op (raw-buf.3)");
assert!(matches!(peek.body, Term::Intrinsic), "peek is an (intrinsic) marker");
}
/// raw-buf.4: pin the JSON byte-shape of the raw_buf kernel-tier
/// base-extension module. Mirror of `kernel_stub_module_round_trips`.
/// base-extension module. Exercises all three additive schema items
/// in a single fixture (`Module.kernel = true`, one TypeDef with
/// `param-in`, one ctor).
#[test]
fn raw_buf_module_round_trips() {
let m = ailang_surface::parse_raw_buf();
+1 -1
View File
@@ -11,7 +11,7 @@
//! (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
//! built-in `prelude` and `raw_buf` are always loaded because
//! the loader injects them programmatically; user kernel-tier
//! modules need a path from the entry.
+5 -7
View File
@@ -49,14 +49,12 @@ fn loads_example_workspace_happy_path() {
assert_eq!(ws.entry, "ws_main");
assert!(ws.modules.contains_key("ws_main"));
assert!(ws.modules.contains_key("ws_lib"));
// the loader auto-injects three built-in kernel-tier modules
// (`prelude`, `kernel_stub` — see prep.3 of the
// kernel-extension-mechanics milestone — and `raw_buf`, the
// first real-payload kernel extension, raw-buf.4), so the count
// is the user's two modules plus those three.
assert_eq!(ws.modules.len(), 5);
// the loader auto-injects two built-in kernel-tier modules
// (`prelude` and `raw_buf`, the first real-payload kernel
// extension, raw-buf.4), so the count is the user's two modules
// plus those two.
assert_eq!(ws.modules.len(), 4);
assert!(ws.modules.contains_key("prelude"));
assert!(ws.modules.contains_key("kernel_stub"));
assert!(ws.modules.contains_key("raw_buf"));
}
@@ -1,16 +0,0 @@
//! Kernel-stub submodule — minimal ratifying fixture for the
//! kernel-extension-mechanics milestone (prep.3). The Form-A text
//! lives in the sibling `source.ail`.
//!
//! No domain content. Retired when the `raw-buf` milestone lands
//! its real kernel-tier consumer (raw-buf.4); until then it stays
//! as the ratifying-fixture anchor.
/// 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`).
///
/// Ships a `(fn new ...)` def so consumers can spell `(new StubT 42)`
/// (Term::New end-to-end, per prep.3 fieldtest F4) and an `answer`
/// `(intrinsic)` fn whose `INTERCEPTS` entry the bijection test pins.
pub const SOURCE: &str = include_str!("source.ail");
@@ -1,20 +0,0 @@
(module kernel_stub
(kernel)
(data StubT (vars a)
(ctor Stub a)
(param-in (a Int Float)))
(fn new
(doc "Construct StubT<Int> from an Int. Exercises Term::New end-to-end.")
(type (fn-type (params (con Int)) (ret (con StubT (con Int)))))
(params x)
(body (term-ctor StubT Stub x)))
(fn answer
(doc "Ratifies the intrinsic mechanism end-to-end: codegen intercept answer emits ret i64 42.")
(type (fn-type (params) (ret (con Int))))
(params)
(intrinsic))
(fn peek
(doc "Ratifies the type-scoped polymorphic intrinsic mechanism: StubT.peek is polymorphic over a (param-in {Int,Float}) and type-scoped to StubT. Codegen intercepts StubT_peek__Int / StubT_peek__Float emit a load of the Stub payload. Retires with the stub in raw-buf.5.")
(type (forall (vars a) (fn-type (params (borrow (con StubT a))) (ret a))))
(params s)
(intrinsic)))
+1 -3
View File
@@ -5,11 +5,9 @@
//!
//! The acyclic dependency chain is preserved:
//! `ailang-surface → ailang-kernel → ailang-core`. Per-module parse
//! hops live in `ailang-surface` (`parse_kernel_stub`, …) so this
//! hops live in `ailang-surface` (`parse_raw_buf`, …) so this
//! crate carries zero parser code.
mod kernel_stub;
mod raw_buf;
pub use kernel_stub::SOURCE as STUB_AIL;
pub use raw_buf::SOURCE as RAW_BUF_AIL;
+1 -1
View File
@@ -37,7 +37,7 @@ pub mod parse;
pub mod print;
pub use loader::{
load_module, load_workspace, parse_kernel_stub, parse_prelude, parse_raw_buf, PRELUDE_AIL,
load_module, load_workspace, parse_prelude, parse_raw_buf, PRELUDE_AIL,
};
pub use parse::{parse, parse_term, ParseError};
pub use print::{print, term_to_form_a, type_to_form_a};
+1 -26
View File
@@ -42,22 +42,8 @@ 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_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_AIL)
.expect("ailang_kernel::STUB_AIL must parse as a Module")
}
/// raw-buf.4: parse the embedded raw_buf kernel-tier base-extension
/// module bytes into a `Module`. Mirror of [`parse_kernel_stub`].
/// module bytes into a `Module`. Mirror of [`parse_prelude`].
///
/// Source-of-truth: `ailang_kernel::RAW_BUF_AIL`. Declares the
/// `RawBuf` TypeDef with `param-in (a Int Float Bool)` and the four
@@ -134,17 +120,6 @@ pub fn load_workspace(entry: &Path) -> Result<Workspace, WorkspaceLoadError> {
}
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());
// parse_raw_buf() injects the raw_buf kernel-tier base-extension
// module — RawBuf, the first real-payload kernel extension. Its
// source carries `(kernel)`, so the kernel-flag filter below
+1 -1
View File
@@ -109,4 +109,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 (mechanisms milestone closed 2026-05-28; ratified end-to-end by the `ailang-kernel/src/kernel_stub` fixture, planned for retirement when raw-buf lands a real second consumer; raw-buf and series milestones pending) | design/models/0007-kernel-extensions.md |
| kernel-extensions | onboarding / evolves (mechanisms milestone closed 2026-05-28; ratified end-to-end by the `ailang-kernel/src/raw_buf` base extension; series milestone pending) | design/models/0007-kernel-extensions.md |
+7 -6
View File
@@ -4,9 +4,10 @@
(`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 module
(`crates/ailang-kernel/src/kernel_stub/`). The base-extension and library-
extension milestones (`raw-buf`, `series`) are pending. This
`param-in` — are shipped and ratified by the `raw_buf` base
extension (`crates/ailang-kernel/src/raw_buf/`). The base-extension
milestone (`raw-buf`) has shipped; the library-extension milestone
(`series`) is 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
@@ -220,7 +221,7 @@ 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,
`parse_prelude()` and `parse_raw_buf()` 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
@@ -231,8 +232,8 @@ 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/src/kernel_stub/`) and any future kernel-tier
migration. The `raw_buf` base-extension kernel module
(`crates/ailang-kernel/src/raw_buf/`) and any future kernel-tier
consumers (Series, Matrix) auto-import through the same filter.
Class-method dispatch (a separate mechanism — see
@@ -1,51 +0,0 @@
; Fieldtest kem.3 (Axis 3, kernel-tier modules + auto-import) — a
; consumer that references `kernel_stub`'s TypeDef without an
; `(import kernel_stub)` declaration. Per spec § "Iteration prep.3":
;
; - The module's top-level defs are accessible bare in every other
; module of the workspace, with no `(import ...)` declaration
; required.
; - The module's types are accessible bare in type position.
;
; Outcome: `ail check` fails with
;
; [unknown-module] unwrap_int: unknown module prefix
; `kernel_stub` in qualified reference
;
; The workspace pre-pass rewrites bare `StubT` to qualified
; `kernel_stub.StubT` (correct per prep.1's `qualify_workspace_term`);
; but the resolver does not accept `kernel_stub` as a valid module
; prefix because the consumer has no explicit `(import kernel_stub)`.
; That is, the qualification pre-pass and the auto-import scope are
; not cooperating — the auto-import does NOT add the kernel module
; to the resolver's known-prefixes set.
;
; Workarounds attempted:
;
; - Adding `(import kernel_stub)`: fails earlier with
; [module-not-found] expected at <sibling>/kernel_stub.ail.json
; — the kernel stub has no on-disk file, it is built into the
; compiler binary.
; - Bare `StubT` everywhere: same outcome as above (the pre-pass
; qualifies it before the resolver sees it).
;
; Prelude's bare fns (`print`, `lt`, etc.) DO work — prelude_free_fns
; ratifies that. So the bug is specifically about TypeDefs in type
; position for kernel-tier modules other than prelude. The shipped
; kernel_stub TypeDef appears unreachable from any consumer in
; practice.
(module kem_3_stub_consumer
(fn unwrap_int
(doc "Project the Int back out of a StubT<Int>. Bare `StubT` in the type slot exercises the kernel-tier auto-import — and currently fails to resolve.")
(type (fn-type (params (con StubT (con Int))) (ret (con Int))))
(params s)
(body (match s (case (pat-ctor Stub x) x))))
(fn main
(type (fn-type (params) (ret (con Unit)) (effects IO)))
(params)
(body
(let s (term-ctor StubT Stub 7)
(seq (app print (app unwrap_int s)) (do io/print_str "\n"))))))
@@ -6,7 +6,7 @@
; Per spec § "Iteration prep.3 — Kernel-tier modules + param-in":
; the param-in restriction is a generic, data-driven check; nothing
; in the checker mentions any specific extension. So a user TypeDef
; can declare it just as the stub kernel_stub.StubT does.
; can declare it just as the raw_buf.RawBuf base extension does.
(module kem_4_paramin_box_green
-6
View File
@@ -1,6 +0,0 @@
(module kernel_answer
(fn main
(doc "E2E ratifier: prints the intrinsic answer (42).")
(type (fn-type (params) (ret (con Unit)) (effects IO)))
(params)
(body (app print (app kernel_stub.answer)))))
-13
View File
@@ -1,13 +0,0 @@
(module new_stubt_smoke
(fn unwrap_int
(doc "Project the Int back out of a StubT<Int>.")
(type (fn-type (params (con StubT (con Int))) (ret (con Int))))
(params s)
(body (match s (case (pat-ctor Stub x) x))))
(fn main
(doc "raw-buf.4 desugar ratifier: (new StubT 42) desugars to (app StubT.new 42), builds, and prints 42.")
(type (fn-type (params) (ret (con Unit)) (effects IO)))
(params)
(body
(let s (new StubT 42)
(app print (app unwrap_int s))))))
-9
View File
@@ -1,9 +0,0 @@
(module peek_mono_pin_smoke
(fn at_int
(type (fn-type (params (own (con StubT (con Int)))) (ret (con Int))))
(params s)
(body (app StubT.peek s)))
(fn at_float
(type (fn-type (params (own (con StubT (con Float)))) (ret (con Float))))
(params s)
(body (app StubT.peek s))))