Brummel
832375f2ac
All 176 files in the four accumulating directories now use a zero-padded 4-digit counter prefix that reflects creation order (`NNNN-slug.md`). The counter is assigned per directory in strict git-log creation order; ties broken alphabetically by original name. The old `YYYY-MM-DD-` prefix on docs/specs/ and docs/plans/ files is dropped — the date is recoverable from git log and the counter carries the ordering. A file's counter is stable for the life of the file: never reassigned, never reused, never compacted. Deleted files retire their counter; subsequent files do not fill the gap. This is the property that lets cross-references stay literal — refs use the full filename including the counter (`design/contracts/0007-honesty-rule.md`) so they grep cleanly and resolve directly without a glob step. 313 cross-references updated across .md/.rs/.toml/.c/.json files (test pins, include_str! paths, design-INDEX entries, baseline notes, runtime C comments, inter-contract markdown links incl. bare basename and `../models/foo.md` forms). CLAUDE.md gets a new "File-naming convention" section spelling out the rule and rationale. skills/brainstorm/SKILL.md and skills/planner/SKILL.md updated so new spec/plan creation produces counter-prefixed names from the start. The full test suite (cargo test --workspace) passes.
243 lines
8.9 KiB
Markdown
243 lines
8.9 KiB
Markdown
# Env-construction unify — Design Spec
|
|
|
|
**Date:** 2026-05-10
|
|
**Status:** Draft — awaiting user spec review
|
|
**Authors:** Brummel (orchestrator) + Claude
|
|
|
|
## Goal
|
|
|
|
Eliminate the structural drift between `check_in_workspace`
|
|
(`crates/ailang-check/src/lib.rs`, near line 1059) and
|
|
`mono::build_workspace_env` (`crates/ailang-check/src/mono.rs`,
|
|
near line 367) — two paths that construct the same `Env` shape
|
|
and have repeatedly diverged under feature pressure.
|
|
|
|
The empirical motivation is three consecutive bug fixes patching
|
|
the same drift class at three different fields:
|
|
|
|
| Commit | Field forgotten by mono path | Iter |
|
|
|--------|------------------------------|------|
|
|
| `5c5180f` | `env.types`, `env.ctor_index` | 22c |
|
|
| `13b36cc` | `env.globals` | post-22 debug |
|
|
| `a9c685d` | `env.imports` | post-22 audit |
|
|
|
|
Each bug shipped as `ail check` passes / `ail build` fails with
|
|
an env-table-miss in `monomorphise_workspace`. The pattern says a
|
|
fourth field is one feature away.
|
|
|
|
## Architecture
|
|
|
|
A single source-of-truth function
|
|
|
|
```rust
|
|
pub fn build_check_env(ws: &Workspace) -> Env
|
|
```
|
|
|
|
in `crates/ailang-check/src/lib.rs` populates every workspace-flat
|
|
`Env` field — that is, every field whose contents do not depend on
|
|
a `current_module` overlay. Both existing entry points become thin
|
|
consumers of this helper:
|
|
|
|
- `check_in_workspace` calls `build_check_env(ws)`, then applies
|
|
the per-module overlay for the module it is checking
|
|
(`current_module`, `globals` from `module_globals[m.name]`,
|
|
`imports` from `m.imports`).
|
|
- `mono::build_workspace_env` is a thin wrapper:
|
|
`pub fn build_workspace_env(ws: &Workspace) -> Env { build_check_env(ws) }`.
|
|
No additional seeding lives here. The per-module overlays in
|
|
`collect_mono_targets` and `collect_residuals_ordered` (added in
|
|
`13b36cc` and `a9c685d`) are already correctly placed at the
|
|
per-fn call sites — they are not duplicated by this milestone,
|
|
they stay where they are.
|
|
|
|
The split mirrors the semantic distinction:
|
|
|
|
- **Workspace-flat fields** are derivable from `Workspace` alone
|
|
and do not change per call. They go in `build_check_env`.
|
|
- **Per-module / per-fn overlay fields** depend on the call's
|
|
`current_module` (or rigid vars). They stay at the call site.
|
|
|
|
After this refactor, when `synth` learns to read a new `Env`
|
|
field, exactly one place needs the seeding edit.
|
|
|
|
## Components
|
|
|
|
**Files modified:**
|
|
|
|
- `crates/ailang-check/src/lib.rs` — adds
|
|
`pub fn build_check_env(ws: &Workspace) -> Env`. Refactors
|
|
`check_in_workspace` to call it and delete the now-duplicated
|
|
inline seeding (effect_ops install, types, ctor_index,
|
|
module_globals, module_types, class_methods,
|
|
class_superclasses, workspace_registry, module_imports).
|
|
`check_in_workspace` retains its per-module overlay logic
|
|
(current_module, globals, imports for the module it is
|
|
checking).
|
|
- `crates/ailang-check/src/mono.rs` — `build_workspace_env`
|
|
becomes a one-line wrapper around `build_check_env`. The
|
|
drift-risk comment ("If `synth` starts reading a new `Env`
|
|
field, update both paths") is deleted — there is no longer a
|
|
pair of paths to keep in sync.
|
|
|
|
**Files added:**
|
|
|
|
- `crates/ailang-check/tests/env_construction_pin.rs` — a new
|
|
integration test that pins the drift-shape invariant. See
|
|
Testing strategy.
|
|
|
|
**Fields seeded by `build_check_env` (workspace-flat):**
|
|
|
|
- `effect_ops` — via `builtins::install`
|
|
- `types` — workspace-flat from every `Def::Type`
|
|
- `ctor_index` — workspace-flat from every `Def::Type`'s ctors
|
|
- `module_globals` — per-module index built from
|
|
`build_module_globals(ws)`
|
|
- `module_types` — via `build_module_types(ws)`
|
|
- `module_imports` — per-module index built from each
|
|
`Workspace::modules.values().imports`
|
|
- `class_methods` — workspace-merged from each module's
|
|
`ModuleGlobals::class_methods`
|
|
- `class_superclasses` — walk every `Def::Class` for
|
|
`superclass`
|
|
- `workspace_registry` — clone of `ws.registry`
|
|
|
|
**Fields not seeded by `build_check_env` (per-call overlay,
|
|
applied by callers):**
|
|
|
|
- `current_module`
|
|
- `globals`
|
|
- `imports`
|
|
- `rigid_vars`
|
|
|
|
## Data flow
|
|
|
|
```
|
|
ws: &Workspace
|
|
│
|
|
▼
|
|
build_check_env(ws) ─► Env (workspace-flat seeded)
|
|
│
|
|
├─► check_in_workspace(m: &Module):
|
|
│ env.current_module = m.name
|
|
│ seed env.globals from env.module_globals[m.name]
|
|
│ build env.imports from m.imports
|
|
│ run check on each Def in m
|
|
│
|
|
└─► mono::build_workspace_env(ws):
|
|
return build_check_env(ws) verbatim
|
|
(callers apply per-fn overlay)
|
|
│
|
|
▼
|
|
collect_mono_targets / collect_residuals_ordered (per-fn):
|
|
env.clone()
|
|
env.current_module = module_name
|
|
seed env.globals from env.module_globals[module_name]
|
|
seed env.imports from env.module_imports[module_name]
|
|
for v in fn rigids: env.rigid_vars.insert(v)
|
|
run synth on body
|
|
```
|
|
|
|
One construction; two consumers; per-fn overlays at the per-fn call sites.
|
|
|
|
## Error handling
|
|
|
|
No new error variants. The existing
|
|
`build_module_globals(ws).expect(...)` call (used by
|
|
`build_workspace_env` today) is a caller-contract panic that
|
|
fires only if the mono pass is invoked on a workspace that has
|
|
not passed typecheck — a programmer error, not a user error.
|
|
That panic moves into `build_check_env` unchanged.
|
|
|
|
`build_check_env` has no fallible operations: every seeding step
|
|
is a `clone` + `insert` into `BTreeMap` / `IndexMap`, all
|
|
infallible.
|
|
|
|
User-facing diagnostics (`UnknownIdent`, `UnknownModule`,
|
|
`UnknownType`, `UnknownCtor`) continue to fire at the same call
|
|
sites in `synth`; the refactor changes the construction of `Env`,
|
|
not its read paths.
|
|
|
|
## Testing strategy
|
|
|
|
**Existing regression suite (drift class):** the three RED tests
|
|
that pinned today's drift-class bugs run automatically and stay
|
|
green:
|
|
|
|
- `crates/ail/tests/typeclass_22c.rs` — covers
|
|
`env.types` / `env.ctor_index` (5c5180f).
|
|
- `crates/ail/tests/mono_recursive_fn.rs` — covers
|
|
`env.globals` (13b36cc).
|
|
- `crates/ail/tests/mono_xmod_qualified_ref.rs` — covers
|
|
`env.imports` (a9c685d).
|
|
|
|
If any of these regress after the refactor, the unify is broken
|
|
and must not ship.
|
|
|
|
**New drift-shape pin test
|
|
(`crates/ailang-check/tests/env_construction_pin.rs`):** a single
|
|
integration test that:
|
|
|
|
1. Builds a representative class-bearing workspace fixture
|
|
covering at least one `Def::Class`, one `Def::Instance`,
|
|
one user ADT, and one cross-module import.
|
|
2. Computes `env_a = build_check_env(&ws)` (the new helper).
|
|
3. Computes `env_b` by running the inline construction the way
|
|
`check_in_workspace` did pre-refactor — captured by reading
|
|
the same code path and reproducing it inline in the test.
|
|
(Practically: a small in-test helper that mirrors the
|
|
pre-refactor seeding so the assertion has something to
|
|
compare against.)
|
|
4. Asserts that `env_a` and `env_b` agree on every workspace-flat
|
|
field — same key-set, same per-key value (or, where types do
|
|
not implement `PartialEq`, same key set).
|
|
|
|
The test serves as a tripwire: any future change that adds a new
|
|
workspace-flat seed to one path but not the helper fails the
|
|
test before it can ship a real bug.
|
|
|
|
**Bench gates:** `bench/check.py`, `bench/compile_check.py`,
|
|
`bench/cross_lang.py` must each report 0 regressed. Performance
|
|
of the refactor must be neutral — `build_check_env` is logically
|
|
the same work as the pre-refactor inline.
|
|
|
|
**Workspace test suite:** `cargo test --workspace` must remain
|
|
fully green (~344 tests).
|
|
|
|
## Acceptance criteria
|
|
|
|
1. `pub fn build_check_env(ws: &Workspace) -> Env` exists in
|
|
`crates/ailang-check/src/lib.rs`.
|
|
2. `mono::build_workspace_env` is a one-line wrapper: it calls
|
|
`build_check_env(ws)` and returns the result. No inline
|
|
seeding remains in this function.
|
|
3. `check_in_workspace` calls `build_check_env(ws)` instead of
|
|
inline workspace-flat seeding. Per-module overlay logic
|
|
(current_module, globals, imports for the module being
|
|
checked) remains.
|
|
4. The drift-shape pin test
|
|
(`crates/ailang-check/tests/env_construction_pin.rs`) is
|
|
green.
|
|
5. The three existing RED tests
|
|
(`typeclass_22c`, `mono_recursive_fn`, `mono_xmod_qualified_ref`)
|
|
remain green.
|
|
6. `cargo test --workspace` is fully green.
|
|
7. `bench/check.py`, `bench/compile_check.py`, `bench/cross_lang.py`
|
|
each report 0 regressed.
|
|
8. The `// Drift risk: this fn and `crate::check_in_workspace` both
|
|
populate `crate::Env`. If `synth` starts reading a new `Env`
|
|
field, update both paths.` comment in `mono.rs::build_workspace_env`
|
|
is deleted (it no longer applies).
|
|
|
|
## Out of scope
|
|
|
|
- Pipeline-topology changes (e.g. moving the mono pass inside
|
|
`check_workspace`). The pass-decomposition invariant — mono is
|
|
post-typecheck / pre-codegen — stays.
|
|
- Refactoring the per-module overlay shape. The
|
|
`current_module` / `globals` / `imports` / `rigid_vars` overlay
|
|
is semantically correct as it is and stays at the call site.
|
|
- Primitive-name-set consolidation (still queued from 22-tidy).
|
|
Different drift class, different milestone.
|
|
- New env fields. This milestone preserves the current shape; it
|
|
only changes who constructs it.
|