test(series): RED pin for polymorphic RawBuf element-var forwarding
Base-tier enabling RED for the `series` milestone step 1 (#61). A polymorphic fn that allocates `(new RawBuf n)` with no explicit type-arg — element var solved purely from the enclosing ctor-field type `(con RawBuf a)`, never from a value argument — checks clean but fails `ail build --alloc=rc`: mono drops the check-phase solution for `a`, defaults it to Unit, and codegen mints the unregistered `RawBuf_new__Unit`. The fixture reads the element back via `RawBuf.get` so a wrong specialisation is observable (the program must print the stored `1.0`). This is the precondition the user picked (option B) so Series can ship as a pure AILang library extension over RawBuf while keeping the model-0007 `(new Series (con Float) 3)` caller surface. The #51 fix carried a WRITTEN `(con Int)` type-arg through mono; the variable-via-expected-type case is the untouched gap. RED: `ail check` exits 0; `ail build --alloc=rc` aborts with `RawBuf_new__Unit has no registered intercept`. GREEN target: builds, runs, prints `1.0`. The mono fix must not break the INTERCEPTS↔ (intrinsic) bijection or the Term::New↔pre_desugar_validation lockstep. refs #61
This commit is contained in:
@@ -0,0 +1,83 @@
|
|||||||
|
//! RED-pin for the series-step-1 enabling fix (#61, base-tier): a
|
||||||
|
//! polymorphic function may allocate a `RawBuf a` over its OWN forall
|
||||||
|
//! type variable via `new` with NO explicit type-arg — the element
|
||||||
|
//! type is solved purely from the expected ctor-field context
|
||||||
|
//! `(con RawBuf a)` — and under monomorphisation the buffer must
|
||||||
|
//! specialise to the CALLER's concrete element type, NOT default to
|
||||||
|
//! Unit.
|
||||||
|
//!
|
||||||
|
//! Property protected: a check-time-solved element var on
|
||||||
|
//! `(new RawBuf n)` survives monomorphisation. When the only carrier
|
||||||
|
//! of the buffer's element type is the enclosing ADT ctor-field type
|
||||||
|
//! `(con RawBuf a)` (the builder `mk` takes only the size, never a
|
||||||
|
//! value of type `a`), mono must propagate the check-phase solution
|
||||||
|
//! for `a` to the caller's concrete instantiation. Today it drops
|
||||||
|
//! that solution, defaults `a` to Unit, and codegen mints
|
||||||
|
//! `RawBuf_new__Unit`, which has no registered intercept
|
||||||
|
//! (crates/ailang-codegen/src/intercepts.rs registers only
|
||||||
|
//! Int/Float/Bool). The fix lives in mono substitution propagation to
|
||||||
|
//! Term::New lowering (crates/ailang-check/src/lower_to_mir.rs:501,
|
||||||
|
//! `elem: None`). Precedent: the #51 explicit-`(con Int)`-type-arg
|
||||||
|
//! fix carried a WRITTEN annotation through mono; the
|
||||||
|
//! variable-via-expected-type case here is the untouched gap.
|
||||||
|
//!
|
||||||
|
//! This is a CLI-boundary E2E test because the defect spans the
|
||||||
|
//! check -> mono -> codegen pipeline and the symptom is the exit
|
||||||
|
//! behaviour of `ail build` itself. The element is read back via
|
||||||
|
//! `first` (RawBuf.get) so the specialisation is OBSERVABLE: a wrong
|
||||||
|
//! specialisation could not print the stored Float.
|
||||||
|
|
||||||
|
use std::path::{Path, PathBuf};
|
||||||
|
use std::process::Command;
|
||||||
|
|
||||||
|
fn repo_root() -> PathBuf {
|
||||||
|
let manifest_dir = env!("CARGO_MANIFEST_DIR");
|
||||||
|
Path::new(manifest_dir)
|
||||||
|
.parent()
|
||||||
|
.unwrap()
|
||||||
|
.parent()
|
||||||
|
.unwrap()
|
||||||
|
.to_path_buf()
|
||||||
|
}
|
||||||
|
|
||||||
|
/// A polymorphic `Box a` whose builder `mk` allocates `(new RawBuf n)`
|
||||||
|
/// over its own forall var `a` (no type-arg, element solved from the
|
||||||
|
/// `(con RawBuf a)` ctor-field context). Instantiated by the caller at
|
||||||
|
/// `Float`, it must build under `--alloc=rc` and print the stored
|
||||||
|
/// `1.0` — proving the inner buffer specialised to the caller's
|
||||||
|
/// element type rather than defaulting to Unit.
|
||||||
|
#[test]
|
||||||
|
fn rawbuf_new_poly_elem_specialises_to_caller_type() {
|
||||||
|
let fixture = repo_root().join("examples/raw_buf_new_poly_elem.ail");
|
||||||
|
let tmp = std::env::temp_dir().join(format!(
|
||||||
|
"ailang_rawbuf_new_poly_elem_{}",
|
||||||
|
std::process::id()
|
||||||
|
));
|
||||||
|
std::fs::create_dir_all(&tmp).unwrap();
|
||||||
|
let out = tmp.join("bin");
|
||||||
|
|
||||||
|
let build = Command::new(env!("CARGO_BIN_EXE_ail"))
|
||||||
|
.args(["build", fixture.to_str().unwrap(), "--alloc=rc", "-o"])
|
||||||
|
.arg(&out)
|
||||||
|
.output()
|
||||||
|
.expect("ail build failed to spawn");
|
||||||
|
assert!(
|
||||||
|
build.status.success(),
|
||||||
|
"ail build --alloc=rc failed for polymorphic RawBuf<a> over a \
|
||||||
|
forall var solved from the ctor-field context: stderr={}",
|
||||||
|
String::from_utf8_lossy(&build.stderr)
|
||||||
|
);
|
||||||
|
|
||||||
|
let run = Command::new(&out).output().expect("execute binary");
|
||||||
|
assert!(
|
||||||
|
run.status.success(),
|
||||||
|
"binary exited non-zero: {:?}",
|
||||||
|
run.status
|
||||||
|
);
|
||||||
|
let stdout = String::from_utf8_lossy(&run.stdout);
|
||||||
|
assert!(
|
||||||
|
stdout.trim() == "1.0",
|
||||||
|
"expected the program to print the stored Float `1.0` (buffer \
|
||||||
|
specialised to the caller's element type Float), got: {stdout:?}"
|
||||||
|
);
|
||||||
|
}
|
||||||
@@ -0,0 +1,19 @@
|
|||||||
|
(module raw_buf_new_poly_elem
|
||||||
|
(data Box (vars a) (param-in (a Int Float)) (ctor B (con RawBuf a)))
|
||||||
|
(fn mk
|
||||||
|
(doc "RED-pin fixture for the series-step-1 enabling fix (#61 base-tier). `mk` allocates a `(new RawBuf n)` with NO explicit element type-arg: the buffer's element var is solved at check-time PURELY from the expected ctor-field type `(con RawBuf a)`, never from a value argument (mk takes only the size). Under monomorphisation the buffer must specialise to the CALLER's concrete element type. Today `ail check` passes (the element var `a` unifies cleanly via the ctor-field context) but `ail build --alloc=rc` aborts: mono drops the check-time solution for `a`, defaults it to Unit, and mints `RawBuf_new__Unit`, which has no registered intercept (crates/ailang-codegen/src/intercepts.rs registers only Int/Float/Bool). Diagnosis pointer (NOT the test's concern): the check phase solves `a`; mono must propagate that solution to Term::New lowering (crates/ailang-check/src/lower_to_mir.rs:501, `elem: None`) instead of defaulting to Unit. Precedent is the #51 explicit-`(con Int)`-type-arg fix; the variable-via-expected-type case is the untouched gap. Expected post-fix: the buffer specialises to the caller's element type (Float here), build succeeds, the program prints the stored Float `1.0`.")
|
||||||
|
(type (forall (vars a) (fn-type (params (own (con Int))) (ret (own (con Box a))))))
|
||||||
|
(params n)
|
||||||
|
(body (let buf (new RawBuf n) (term-ctor Box B buf))))
|
||||||
|
(fn store
|
||||||
|
(type (forall (vars a) (fn-type (params (own (con Box a)) (own a)) (ret (own (con Box a))))))
|
||||||
|
(params b v)
|
||||||
|
(body (match b (case (pat-ctor B buf) (term-ctor Box B (app RawBuf.set buf 0 v))))))
|
||||||
|
(fn first
|
||||||
|
(type (forall (vars a) (fn-type (params (borrow (con Box a))) (ret (own a)))))
|
||||||
|
(params b)
|
||||||
|
(body (match b (case (pat-ctor B buf) (app RawBuf.get buf 0)))))
|
||||||
|
(fn main
|
||||||
|
(type (fn-type (params) (ret (own (con Unit))) (effects IO)))
|
||||||
|
(params)
|
||||||
|
(body (let b (app store (app mk 1) 1.0) (app print (app first b))))))
|
||||||
Reference in New Issue
Block a user