Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

plan: form-a.tidy — form_a.md class/instance/constraints + 3 audit drift items

Browse Source 
Post-fieldtest documentary tidy. Six tasks: T1-3 add three new
sections to crates/ailang-core/specs/form_a.md (Class, Instance,
Constraints on polymorphic fns) anchored against the live corpus
(test_22c_user_class_e2e for class-decl, show_user_adt +
mq3_class_eq_vs_fn_eq_classmod for instance, cmp_max_smoke for
constraints), each with EBNF + canonical-form-rule paragraph +
verified example. T4 fixes 5 contradictory "seven carve-outs"
sites in docs/specs/2026-05-13-form-a-default-authoring.md (the
audit-form-a journal flagged 3 sections; recon expanded to 5
total). T5 deletes the empty mod tests {} placeholder + its
6-line explanatory comment in crates/ailang-core/src/hash.rs
(form-a.1 T5 relocated the unit tests; placeholder serves no
purpose). T6 rewrites round_trip.rs module + inner test
docstrings to use the post-T10 four-property framing
(parse-determinism + idempotency + CLI-pipeline-idempotency +
carve-out-anchor) instead of retired Direction-1/Direction-2
language.

Drift item B2 (plan-file "seven carve-outs") dropped from this
iter per recon: the docs/plans/2026-05-13-iter-form-a.1.md file
contains zero defective sites; all four "seven" mentions are
internally scoped to §C4(a), arithmetic, or future-state. The
audit-form-a journal "two sites" claim does not match what is
in the plan file at HEAD.

All tasks are pure docs/comment changes. cargo test --workspace
stays at 559 green at every task boundary.
This commit is contained in:
Brummel
2026-05-13 12:18:28 +02:00
parent 1e20b18eba
commit 5e94204c21
1 changed files with 506 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files
docs/plans/2026-05-13-iter-form-a.tidy.md
+506
View File
@@ -0,0 +1,506 @@
# form-a.tidy — Implementation Plan
> **Parent specs:**
> - `docs/specs/2026-05-13-fieldtest-form-a.md` §Findings 2-3 (spec_gap: form_a.md missing class/instance/constraint sections + canonical-form qualifier rule)
> - `docs/journals/2026-05-13-audit-form-a.md` §"Drift items" (3 of 4 documentary items; item #2 dropped per recon — see Architecture)
>
> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement` to run this plan. Steps use `- [ ]` checkboxes for tracking.
**Goal:** Tighten `crates/ailang-core/specs/form_a.md` with three new sections (Class, Instance, Constraints on polymorphic fns) anchored against the schema and the live corpus, and close 3 of the 4 documentary drift items from audit-form-a (the 4th — "plan seven-orphans" — was found by recon to not exist).
**Architecture:** Pure documentation + comment tidy. No production-code behaviour changes. Six tasks. Tasks 1-3 land form_a.md additions one logical section at a time so each section is its own reviewable unit. Task 4 sweeps 5 contradictory `seven carve-outs` sites in the form-a spec; the analogous plan-file sweep is deliberately NOT scheduled because recon verified the plan's four `seven` mentions are all internally scoped (§C4(a) scope, arithmetic, or future state) and never contradict the §C4(b) amendment. Task 5 deletes the empty `mod tests {}` placeholder + its 6-line explanatory comment in `hash.rs` (form-a.1 T5 relocated the unit tests to `crates/ailang-core/tests/hash_pin.rs`; the placeholder serves no purpose and there is no doctest depending on it). Task 6 rewrites the `round_trip.rs` module docstring + inner test docstring to use the post-T10 four-property framing (parse-determinism + idempotency + CLI-pipeline-idempotency + carve-out-anchor) instead of the retired Direction-1/Direction-2 language.
**Tech Stack:** Markdown (form_a.md, the form-a spec). Rust comment edits (hash.rs, round_trip.rs). No code logic changes, no test additions, no test retirements.
---
**Files this plan creates or modifies:**
- Modify: `crates/ailang-core/specs/form_a.md` — three new sections (Tasks 1-3) + line 66 intro update (Task 1)
- Modify: `docs/specs/2026-05-13-form-a-default-authoring.md` — 5 site edits (Task 4)
- Modify: `crates/ailang-core/src/hash.rs:50-57` — delete 8 lines (Task 5)
- Modify: `crates/ailang-surface/tests/round_trip.rs` — module docstring + test inner docstring rewrite (Task 6)
---
### Task 1: form_a.md — Class declarations section
**Files:**
- Modify: `crates/ailang-core/specs/form_a.md:66` (intro line)
- Modify: `crates/ailang-core/specs/form_a.md:113` (insertion point after `### Constant — (const ...)`)
- [ ] **Step 1: Update §Definitions intro from "Three kinds" to "Five kinds"**
Replace at `crates/ailang-core/specs/form_a.md:66`:
```
Three kinds, matched on the leading keyword:
```
with:
```
Five kinds, matched on the leading keyword:
```
- [ ] **Step 2: Insert `### Class — (class ...)` subsection after Constant**
After the existing `### Constant — (const ...)` block (ends at `crates/ailang-core/specs/form_a.md:113`), insert:
```markdown
### Class — `(class ...)`
```
(class NAME
(param TYVAR)
(doc STRING)?
(superclass (class CLASS-REF) (type TYVAR))?
(method NAME (type FN-TYPE) (default TERM)?)*)
```
A class declaration introduces a typeclass with one type parameter (`param`)
and a list of method signatures.
`CLASS-REF` in the optional `superclass` clause follows the canonical-form
rule (see *Types* below): bare for same-module, `MODULE.CLASS` for
cross-module. The `superclass` slot is at most one — multi-superclass
chains are not yet supported.
Each `method` carries a function-typed signature. The bound type variable
named in `param` is in scope throughout the method's `(type ...)`. A
`(default ...)` clause provides a fallback implementation; absent means
the method is abstract-required (every instance MUST implement it).
Example (`examples/test_22c_user_class_e2e.ail`):
```
(class Foo
(param a)
(method foo
(type (fn-type (params (borrow a)) (ret (con Int))))))
```
```
- [ ] **Step 3: Verify the form_a.md sample example parses + checks**
Run: `./target/debug/ail check examples/test_22c_user_class_e2e.ail`
Expected output: `ok (24 symbols across 2 modules)` (per recon report Scope A4).
Run: `cargo test --workspace --quiet 2>&1 | tail -5`
Expected: total `559 passed` (matches baseline post-bugfix-instance-body-unbound-var).
### Task 2: form_a.md — Instance declarations section
**Files:**
- Modify: `crates/ailang-core/specs/form_a.md` — insertion point after the `### Class` block landed by Task 1
- [ ] **Step 1: Insert `### Instance — (instance ...)` subsection after Class**
Immediately after the `### Class — (class ...)` block landed in Task 1, insert:
```markdown
### Instance — `(instance ...)`
```
(instance
(class CLASS-REF)
(type TYPE)
(doc STRING)?
(method NAME (body LAM-TERM))*)
```
An instance declaration provides method implementations of `CLASS-REF` at
the concrete `TYPE`.
`CLASS-REF` follows the canonical-form rule: bare for same-module-to-
class (the instance and the class live in the same module), `MODULE.CLASS`
for cross-module (the class lives in another module — most commonly
`prelude.Show`, `prelude.Eq`, etc.).
Each `method` body is a `(lam ...)` term. The class's type parameter is
substituted for `TYPE` throughout the method body's parameter types and
return type; method bodies are type-checked under that substitution and
walk through the same identifier-resolution path as `(fn ...)` bodies,
so an unbound name inside a method body fires `[unbound-var]` at
`ail check`.
Two examples.
Same-module class + instance (`examples/mq3_class_eq_vs_fn_eq_classmod.ail`,
abbreviated):
```
(class MyEq (param a)
(method myeq (type (fn-type (params (borrow a) (borrow a)) (ret (con Bool))))))
(instance
(class MyEq)
(type (con Int))
(method myeq
(body (lam (params (typed x (con Int)) (typed y (con Int))) (ret (con Bool)) (body true)))))
```
Cross-module qualified class (`examples/show_user_adt.ail`, abbreviated):
```
(instance
(class prelude.Show)
(type (con IntBox))
(method show
(body (lam (params (typed x (con IntBox))) (ret (con Str))
(body (match x (case (pat-ctor MkIntBox n) (app int_to_str n))))))))
```
The `prelude.Show` qualifier is required here because `Show` is declared
in the `prelude` module, not the entry module. Writing `(class Show)`
bare would fail with `bare-cross-module-class-ref`.
```
- [ ] **Step 2: Verify the two cited fixtures `ail check` cleanly**
Run: `./target/debug/ail check examples/mq3_class_eq_vs_fn_eq_classmod.ail`
Expected output: `ok (22 symbols across 2 modules)`.
Run: `./target/debug/ail check examples/show_user_adt.ail`
Expected output: `ok (23 symbols across 2 modules)`.
Run: `cargo test --workspace --quiet 2>&1 | tail -5`
Expected: total `559 passed`.
### Task 3: form_a.md — Constraints on polymorphic fns
**Files:**
- Modify: `crates/ailang-core/specs/form_a.md:117-126` (the "Four shapes" EBNF block) and surrounding examples
- [ ] **Step 1: Extend the `(forall ...)` line in the four-shapes EBNF to carry the optional `(constraints ...)` clause**
Replace at `crates/ailang-core/specs/form_a.md:125`:
```
(forall (vars TYVAR+) BODY-TYPE) ; polymorphic schema
```
with:
```
(forall (vars TYVAR+)
(constraints (constraint CLASS-REF TYPE)+)?
BODY-TYPE) ; polymorphic schema with optional constraints
```
- [ ] **Step 2: Append a paragraph after the "Built-in type-constructors" line explaining constraints**
After `crates/ailang-core/specs/form_a.md:141` (the line ending
`use the name from the (data ...) def.`), insert a new paragraph
immediately before the `Examples:` block at line 143:
```markdown
A `(forall ...)` may carry an optional `(constraints ...)` clause whose
inner items are `(constraint CLASS-REF TYPE)` pairs. Each constraint
requires the named class to have an instance at the given type; `TYPE`
is typically a type variable bound by the same `forall`. `CLASS-REF`
follows the canonical-form rule (bare for same-module, `MODULE.CLASS`
for cross-module). At a call site, every constraint must discharge — by
a matching instance in the workspace or by another constraint in the
caller's own schema. An undischargeable constraint fires `no-instance`
at `ail check`.
```
- [ ] **Step 3: Add one example to the existing Examples block at line 145-150**
After the existing fourth example at `crates/ailang-core/specs/form_a.md:149`
(the line beginning `(forall (vars a) (fn-type ...))`), add a fifth
example showing a constrained forall:
```
(forall (vars a) (constraints (constraint prelude.Ord a))
(fn-type (params a a) (ret a)))
```
The block should now have five example lines, the new one anchored to
`examples/cmp_max_smoke.ail` (`fn cmp_max`).
- [ ] **Step 4: Verify the cited fixture `ail check` clean**
Run: `./target/debug/ail check examples/cmp_max_smoke.ail`
Expected output: `ok (22 symbols across 2 modules)` (Boss-verified
empirically at plan-write time, 2026-05-13).
Run: `cargo test --workspace --quiet 2>&1 | tail -5`
Expected: total `559 passed`.
### Task 4: form-a spec — fix 5 contradictory "seven carve-outs" sites
**Files:**
- Modify: `docs/specs/2026-05-13-form-a-default-authoring.md` at five line ranges
The audit-form-a journal flagged three sections (§C1, §C2, §"Data flow")
contradicting the §C4(b) amendment. Recon expanded the find to 5 sites
total (the additional sites are the preamble at line 11 and §C3 at line
218, which the audit summary missed). Sites verified by recon are
listed below.
Per recon, the §C2 line 191 "The seven carve-outs continue to use the
.ail.json path" is ambiguous — it can be read as "the §C4(a) seven
fixtures continue to use the .ail.json path" (correct) OR as "the
seven total carve-outs" (incorrect post-amendment). Treat it as
defective and tighten to "the eight carve-outs" to match AC #1 and
the §"Data flow" diagram.
- [ ] **Step 1: Fix preamble line 11**
Replace at `docs/specs/2026-05-13-form-a-default-authoring.md:11`:
```
that remain in the repository are seven specific negative-test
```
with:
```
that remain in the repository are eight specific negative-test
```
- [ ] **Step 2: Fix §C1 line 170**
Replace at `docs/specs/2026-05-13-form-a-default-authoring.md:170`:
```
walks examples/*.ail.json, skips the seven carve-outs (named
```
with:
```
walks examples/*.ail.json, skips the eight carve-outs (named
```
- [ ] **Step 3: Fix §C2 line 191**
Replace at `docs/specs/2026-05-13-form-a-default-authoring.md:191`:
```
`ailang_surface::parse_module_from_str`. The seven carve-outs
```
with:
```
`ailang_surface::parse_module_from_str`. The eight carve-outs
```
- [ ] **Step 4: Fix §C3 line 218**
Replace at `docs/specs/2026-05-13-form-a-default-authoring.md:218`:
```
**Carve-out anchor.** The seven .ail.json-only fixtures are
```
with:
```
**Carve-out anchor.** The eight .ail.json-only fixtures are
```
- [ ] **Step 5: Fix §"Data flow" lines 363, 374**
Replace at `docs/specs/2026-05-13-form-a-default-authoring.md:363`:
```
except for the seven carve-outs:
```
with:
```
except for the eight carve-outs:
```
Replace at `docs/specs/2026-05-13-form-a-default-authoring.md:374`:
```
only by the seven carve-outs (and by any test that explicitly mixes
```
with:
```
only by the eight carve-outs (and by any test that explicitly mixes
```
- [ ] **Step 6: Sanity-check no other "seven" → "eight" candidates were missed**
Run: `grep -n 'seven' docs/specs/2026-05-13-form-a-default-authoring.md`
Expected output (post-edit; verbatim — these surviving "seven" sites
are correct under §C4(a) scope or are arithmetic / future-state, not
defects):
```
233:and (b) **compile-time-embed** carve-outs (one
238:**(a) Subject-matter carve-outs (immutable, seven files):**
463:examples/*.ail.json after milestone close (seven from §C4 (a) +
469:drops to seven once the prelude-embed-refactor milestone retires
```
(Line 233 doesn't contain "seven" by itself — it's the §C4 header
context. The recon-mapped survivors are lines 238, 463, 469 — three
remaining `seven` mentions, all correctly scoped. If `grep -n 'seven'`
surfaces more than three matches post-edit, an edit missed a site.)
- [ ] **Step 7: Run cargo test --workspace as a no-regression smoke**
Run: `cargo test --workspace --quiet 2>&1 | tail -5`
Expected: total `559 passed`.
### Task 5: hash.rs — delete empty `mod tests {}` placeholder
**Files:**
- Modify: `crates/ailang-core/src/hash.rs:50-57` (delete 8 lines)
Recon verified: the `#[cfg(test)] mod tests {}` is literally empty,
gated by `#[cfg(test)]`, with a 6-line comment block above explaining
the form-a.1 T5 relocation. No doctest depends on the `tests` module
(the file's only `///` doc-example sits much earlier and does not
reference `tests`). No external code references `ailang_core::hash::tests`.
The placeholder is deletable.
- [ ] **Step 1: Delete lines 50-57**
Read the file first to confirm the exact current contents at those
lines, then use Edit to delete the 8-line block. The block to delete
(exactly as on disk per recon Scope B3):
```rust
// `#[cfg(test)] mod tests` block relocated to
// `crates/ailang-core/tests/hash_pin.rs` in iter form-a.1 Task 5. The
// integration-test crate has `ailang-surface` as a dev-dependency so
// the schema-stability pins can load `.ail` fixtures via
// `ailang_surface::load_module`, eliminating the production-source
// dependency on `.ail.json` fixture reads.
#[cfg(test)]
mod tests {}
```
After deletion, the file should end at the line that previously
preceded the comment block (no trailing blank line if the file
didn't have one before; Rust's formatter would normalise this
anyway, but explicit).
- [ ] **Step 2: Verify the file still compiles**
Run: `cargo build -p ailang-core --quiet`
Expected: build succeeds with no errors.
- [ ] **Step 3: Verify the relocated integration tests still pass**
Run: `cargo test --manifest-path Cargo.toml -p ailang-core --test hash_pin --quiet 2>&1 | tail -3`
Expected: `test result: ok. <N> passed`.
- [ ] **Step 4: Full workspace test as a no-regression smoke**
Run: `cargo test --workspace --quiet 2>&1 | tail -5`
Expected: total `559 passed`.
### Task 6: round_trip.rs — replace Direction-2 framing with four-property framing
**Files:**
- Modify: `crates/ailang-surface/tests/round_trip.rs:1-26` (module-level `//!` docstring)
- Modify: `crates/ailang-surface/tests/round_trip.rs:63-72` (inner `///` docstring on `parse_then_print_then_parse_is_idempotent_on_every_ail_fixture`)
The post-T10 Roundtrip Invariant has four named properties (DESIGN.md
§"Roundtrip Invariant"): parse-determinism, idempotency-under-print,
CLI-pipeline-idempotency, carve-out-anchor. The first two are pinned
by tests in this file; the latter two live in sibling test crates
(`crates/ail/tests/roundtrip_cli.rs` for CLI-pipeline-idempotency;
`crates/ailang-core/tests/carve_out_inventory.rs` for carve-out-anchor).
The current docstring still uses the retired Direction-1/Direction-2
framing.
- [ ] **Step 1: Rewrite the module docstring at lines 1-26**
Replace the entire block from line 1 through the end of the retirement
note at line 26 with:
```rust
//! Roundtrip Invariant gate (in-process) for the form-(A) projection.
//!
//! Two complementary checks over `examples/*.ail`, each gathering
//! fixtures dynamically via `read_dir` (no hardcoded lists). The
//! tests are pure readers — they do not write into the working
//! tree.
//!
//! 1. `parse_is_deterministic_over_every_ail_fixture` — pins
//! **parse-determinism** (property 1 of the post-form-a Roundtrip
//! Invariant, DESIGN.md §"Roundtrip Invariant"). For every
//! well-formed `.ail` text `t`, `parse(t)` produces the same
//! canonical bytes every invocation. The parser is a pure
//! function of input — no randomness, no time dependence, no
//! environment leak. Hashing `canonical::to_bytes(parse(t))` is
//! therefore well-defined for any `.ail` source.
//!
//! 2. `parse_then_print_then_parse_is_idempotent_on_every_ail_fixture`
//! — pins **idempotency-under-print** (property 2). For every
//! well-formed `.ail` text `t`, asserts
//! `canonical_bytes(parse(t))` equals
//! `canonical_bytes(parse(print(parse(t))))`. The printer is a
//! left-inverse of the parser modulo canonical form.
//!
//! The other two properties of the post-form-a Roundtrip Invariant
//! live in sibling test crates: **CLI-pipeline-idempotency** is
//! pinned by `crates/ail/tests/roundtrip_cli.rs::cli_parse_then_render_then_parse_is_idempotent`,
//! and **carve-out-anchor** is pinned by
//! `crates/ailang-core/tests/carve_out_inventory.rs::examples_ail_json_inventory_matches_carve_outs`.
//!
//! Retired iter form-a.1 T9: `print_then_parse_round_trips_every_fixture`
//! (corpus shrunk to 8 carve-outs post-iter) and
//! `every_ail_fixture_matches_its_json_counterpart` (no longer
//! expressible: only one form is hand-authored post-iter).
```
- [ ] **Step 2: Rewrite the inner test docstring at lines 63-72**
Replace the inner `///` block immediately preceding
`parse_then_print_then_parse_is_idempotent_on_every_ail_fixture`
(lines 63-72) with:
```rust
/// Pins **idempotency-under-print** (property 2 of the post-form-a
/// Roundtrip Invariant, DESIGN.md §"Roundtrip Invariant"): for every
/// well-formed `.ail` text `t`, the composition `parse → print → parse`
/// is idempotent on the AST.
///
/// Direct enforcement complements the parse-determinism gate above
/// (which alone does not constrain the printer). Together they pin
/// `parse → print` as a left-inverse modulo canonical form for every
/// `.ail` fixture in the corpus.
```
- [ ] **Step 3: Verify the file still compiles and the tests still pass**
Run: `cargo test --manifest-path Cargo.toml -p ailang-surface --test round_trip --quiet 2>&1 | tail -3`
Expected: `test result: ok. 2 passed; 0 failed`.
- [ ] **Step 4: Full workspace test as a no-regression smoke**
Run: `cargo test --workspace --quiet 2>&1 | tail -5`
Expected: total `559 passed`.
- [ ] **Step 5: Verify no surviving "Direction 1" or "Direction 2" references in round_trip.rs**
Run: `grep -n 'Direction [12]' crates/ailang-surface/tests/round_trip.rs`
Expected output: empty (zero hits).
---
## Decision recorded — Drift item B2 (plan-file "seven carve-outs" orphans)
Recon verified that `docs/plans/2026-05-13-iter-form-a.1.md` contains
**zero** defective `seven` mentions; the four hits are all internally
scoped to §C4(a) (which IS seven), arithmetic, or future-state. The
audit-form-a journal's "two sites" claim against this file does not
match the file's current contents. **No plan-file edit is included
in this iter.** The form-a.tidy journal entry must record this
finding for future-reader visibility.