First half of spec iteration mir.1 (docs/specs/0060-typed-mir.md,
plan docs/plans/0114-mir.1a-mir-infrastructure.md). Purely additive: a
new leaf crate plus a post-mono lowering walk plus the front-end entry.
Nothing consumes MIR yet — codegen and the CLI are untouched — so the
whole existing suite stays green (102 test-result-ok lines, 0 failed;
the one ignored is the #49 pin, which lifts at mir.4). mir.1b flips
codegen to consume MIR and deletes the synth_with_extras mirror.
What lands:
- `ailang-mir` (new leaf crate, depends only on ailang-core): MTerm /
MArg / MArm / MLoopBinder / MNewArg / Callee / Mode / StrRep / MirDef
/ MirModule / MirWorkspace, structurally complete over all 17 Term
variants plus the dedicated Str split (MTerm::Str{lit,rep}). Every
later-iteration annotation field exists now at a mir.1 default
(App.callee = Indirect, MArg.mode/consume_count = Owned/1, Str.rep =
Static, New.elem = None); the struct shape will not change across
mir.2–mir.5, only the values. MTerm::ty() reads the carried type.
- `ailang-check::lower_to_mir`: the post-mono walk. Carries no second
type engine — it calls the canonical `synth` per node with fresh
throwaway inference scaffolding (subst/counter/residuals/…), applies
the substitution, and threads only the lexical locals/loop_stack,
maintained by the same push/pop rules synth uses (Let, Loop, Lam,
LetRec, and Match via synth's own type_check_pattern). This is the
"one engine, not two" property the milestone buys, on the producer
side.
- `ailang-check::elaborate_workspace`: the single front-end entry —
check (diagnostics gate) → desugar+lift → monomorphise → lower_to_mir
— transcribed from the CLI build path. check_workspace stays for the
diagnostics-only callers.
- Three ty-fill pins (crates/ailang-check/tests/lower_to_mir_ty.rs)
load the #51/#53/#49 witnesses as fixtures and elaborate the whole
workspace, so lower_to_mir is exercised over the full prelude+kernel,
not just the tiny witness. Two new witness fixtures
(examples/new_{rawbuf_size_only,counter_user_adt}.ail); #49 reuses the
existing loop_recur_str_binder_no_leak_pin.ail.
Deviations from the plan, all forced by ground truth and verified
against the live code before commit:
- FnDef.export is Option<String>, not bool — dropped from MirDef (the
plan's note allowed this fallback). Codegen reads FnDef.export
directly, unaffected.
- fn_param_types did not exist — lifted the param-type extraction into
a shared pub(crate) fn and rewired both mono.rs sites
(collect_mono_targets, collect_rewrite_targets) to it, so the
param-type source cannot drift between mono and lower_to_mir. The
helper unwraps a top-level Forall then reads Type::Fn.params —
identical to the inner_ty extraction it replaces; the early-return
non-fn guard is preserved at both sites. Behaviour-preserving (whole
suite green; this is the only edit to existing mono behaviour).
- lower_module mirrors two more mono.rs scaffolding rules the plan
under-transcribed: skip intrinsic-bodied fns (they are
signature-only; lowering them would hit synth's Term::Intrinsic
guard) and seed env.current_module + env.globals + env.imports per
module so synth's Var lookup resolves post-mono specialisations
(e.g. compare__Int) in the prelude.
- The #53 pin asserts the lowered (new Counter 42) init carries ty
Counter, not that it is an MTerm::New: a monomorphic `new` over a
user ADT is desugared to a dotted call `(app Counter.new 42)` before
lower_to_mir runs (desugar.rs:1078-1098), so it lowers to MTerm::App.
MTerm::New survives only for a polymorphic `new` carrying a written
NewArg::Type (the #51 RawBuf path, covered by the rawbuf pin). The
pin's intent — ty-fill correctness — is preserved; the structural
variant is mir.2/mir.5 territory.
- ailang-mir uses workspace-inherited Cargo fields for consistency with
the existing crates (added it to [workspace.dependencies]).
refs #49
Brummel
135f4ceed7