895ba846e8
Atomic completion of spec iteration mir.1 (docs/specs/0060-typed-mir.md): codegen now consumes the typed MIR produced by `lower_to_mir` instead of re-deriving types from the bare `ast::Term`. Every codegen helper that took `&Term` (lower_term, lower_app, drop.rs, match_lower.rs) takes `&MTerm` and reads each node's checker-proved type off `MTerm::ty()`. The build path is `Workspace -> elaborate_workspace -> MirWorkspace -> lower_workspace`; the public `lower_workspace*` entry points and their 18 call sites thread `&MirWorkspace`. The codegen-side type re-derivers `synth_with_extras` + `synth_arg_type` (and the `builtin_ail_type` / `builtin_effect_op_ret` mirror tables) are deleted — grep-clean. The three re-derivers the spec keeps until mir.2/mir.3 (`type_home_module`, `is_static_callee`, the second `infer_module_with_cross`) stay. The mechanical Term->MTerm match-arm conversion was straightforward and compiler-enforced. The substance was a set of producer-side correctness gaps that only surface once codegen reads `MTerm::ty()` and once the build path re-synthesises the post-mono AST through the canonical `synth` (which, unlike the old codegen, fully re-unifies). Each was root-caused against a failing e2e fixture: 1. `qualify_local_types` stripped fn-type modes (rebuilt `Type::Fn` with empty `param_modes` / `Implicit` `ret_mode`), so a monomorphised polymorphic intrinsic (`RawBuf.set`) lost its `Own` ret-mode and the owned temporary leaked at the call site. Made mode-preserving, like its sister `qualify_workspace_types` and `Subst::apply` (449df13). 2. `lower_to_mir::synth_pure` synthesises each node in isolation, so a nullary polymorphic ctor (`Nil : List<a>`) left its element type an unbound `$m` metavar that the canonical synth never pins. Codegen's mono unifier (`unify_for_subst`) already has a wildcard for exactly this — `$u`, the spelling the now-deleted codegen synth used — so the typed-MIR boundary normalises every residual `$m` to `$u` once (`wildcard_residual_metavars`), rather than teaching each consumer to tolerate a raw metavar. 3. The class-method mono arm (`synthesise_mono_fn`) substituted the registry-canonical *qualified* instance type into a method appended to the instance's own module, minting a `show_user_adt.IntBox` param against a bare-`IntBox` body. Localised to bare before substitution, symmetric to the free-fn arm (600565d). 4. Monomorphisation synthesises *downward* class-dispatch references — prelude's `print__<IntBox>` names the instance module `show_user_adt` that prelude never imports. The post-mono re-synth in `lower_module` seeds every workspace module name as an identity import (excluding the current module, to keep own types bare) so the qualified-var path resolves these; the canonical `synth` used by `check_workspace` stays strict. 5. Post-mono, a cross-module callee can name the consumer's *own* ADT qualified (`show_user_adt.IntBox`) where the consumer synthesises it bare — a spelling split that cannot exist pre-mono (the param is polymorphic there). synth's App arm strips the current module's own qualifier from both sides before unifying (`strip_own_module_qual`), a no-op pre-mono. Acceptance: whole workspace suite green (698 tests); `e2e` 98/98 and `show_print_e2e` 3/3; `synth_with_extras`/`synth_arg_type` grep-clean in codegen; #51/#53 fixtures build and run; lower_to_mir_ty pins green. The #49 heap-Str loop-binder leak remains ignored (lifts at mir.4). Builds on the standalone producer fix (600565d, free-fn own-ADT localisation) and the two standalone mode-preservation fixes (449df13Subst::apply); those landed separately as they are independently correct and inert on the old codegen.
78 lines
2.8 KiB
Rust
78 lines
2.8 KiB
Rust
//! Eq-primitive codegen pin tests, relocated from
|
|
//! `ailang-codegen/src/lib.rs` `#[cfg(test)] mod tests` to a `tests/*`
|
|
//! integration crate in iter form-a.1 Task 5. The relocation switches
|
|
//! workspace loading from `ailang_core::load_workspace` (the JSON-only
|
|
//! loader) to `ailang_surface::load_workspace` (the
|
|
//! extension-dispatching superset), so the post-iter `.ail` corpus is
|
|
//! loaded from Form A rather than the deleted `.ail.json` siblings.
|
|
|
|
use ailang_check::elaborate_workspace;
|
|
use ailang_codegen::lower_workspace;
|
|
use ailang_surface::load_workspace;
|
|
use std::path::Path;
|
|
|
|
fn eq_primitives_smoke_path() -> std::path::PathBuf {
|
|
let manifest = env!("CARGO_MANIFEST_DIR");
|
|
Path::new(manifest)
|
|
.parent().unwrap().parent().unwrap()
|
|
.join("examples").join("eq_primitives_smoke.ail")
|
|
}
|
|
|
|
fn lower_eq_primitives_smoke() -> String {
|
|
let entry = eq_primitives_smoke_path();
|
|
let ws = load_workspace(&entry).expect("load workspace");
|
|
let mir = elaborate_workspace(&ws).expect("elaborates");
|
|
lower_workspace(&mir).expect("lower")
|
|
}
|
|
|
|
/// integration with the auto-loaded prelude. Compiling a
|
|
/// workspace that calls `eq` on an Int pair must produce a
|
|
/// mono-synthesised `@ail_prelude_eq__Int` whose body lowers to
|
|
/// `icmp eq i64`. Full pipeline: end-of-typecheck → monomorphise →
|
|
/// codegen, then substring-shape assertions on the IR.
|
|
#[test]
|
|
fn eq_int_call_produces_icmp_i64_mono_fn() {
|
|
let ir = lower_eq_primitives_smoke();
|
|
assert!(
|
|
ir.contains("@ail_prelude_eq__Int"),
|
|
"ir must contain mono-synthesised @ail_prelude_eq__Int; ir was:\n{ir}"
|
|
);
|
|
assert!(
|
|
ir.contains("icmp eq i64"),
|
|
"eq__Int body must lower to icmp eq i64; ir was:\n{ir}"
|
|
);
|
|
}
|
|
|
|
/// same shape as `eq_int_call_produces_icmp_i64_mono_fn`
|
|
/// for Bool. Asserts the mono-synthesised `@ail_prelude_eq__Bool`
|
|
/// lowers to `icmp eq i1`.
|
|
#[test]
|
|
fn eq_bool_call_produces_icmp_i1_mono_fn() {
|
|
let ir = lower_eq_primitives_smoke();
|
|
assert!(
|
|
ir.contains("@ail_prelude_eq__Bool"),
|
|
"ir must contain mono-synthesised @ail_prelude_eq__Bool; ir was:\n{ir}"
|
|
);
|
|
assert!(
|
|
ir.contains("icmp eq i1"),
|
|
"eq__Bool body must lower to icmp eq i1; ir was:\n{ir}"
|
|
);
|
|
}
|
|
|
|
/// Str's mono-symbol body is hand-rolled by the
|
|
/// `try_emit_primitive_instance_body` intercept. Asserts the intercept
|
|
/// fires for the prelude-loaded `eq__Str` synthesised against a real
|
|
/// user fixture that calls `eq` on Str.
|
|
#[test]
|
|
fn eq_str_call_produces_ail_str_eq_call_mono_fn() {
|
|
let ir = lower_eq_primitives_smoke();
|
|
assert!(
|
|
ir.contains("@ail_prelude_eq__Str"),
|
|
"ir must contain mono-synthesised @ail_prelude_eq__Str; ir was:\n{ir}"
|
|
);
|
|
assert!(
|
|
ir.contains("call zeroext i1 @ail_str_eq("),
|
|
"eq__Str body must call @ail_str_eq; ir was:\n{ir}"
|
|
);
|
|
}
|