From 5e94204c218c410d44fbb8e658b677a7294744b0 Mon Sep 17 00:00:00 2001 From: Brummel Date: Wed, 13 May 2026 12:18:28 +0200 Subject: [PATCH] =?UTF-8?q?plan:=20form-a.tidy=20=E2=80=94=20form=5Fa.md?= =?UTF-8?q?=20class/instance/constraints=20+=203=20audit=20drift=20items?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- docs/plans/2026-05-13-iter-form-a.tidy.md | 506 ++++++++++++++++++++++ 1 file changed, 506 insertions(+) create mode 100644 docs/plans/2026-05-13-iter-form-a.tidy.md diff --git a/docs/plans/2026-05-13-iter-form-a.tidy.md b/docs/plans/2026-05-13-iter-form-a.tidy.md new file mode 100644 index 0000000..f1c2bf7 --- /dev/null +++ b/docs/plans/2026-05-13-iter-form-a.tidy.md @@ -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. 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.