From e809f45e676536811634022ba6b1ded1bb40e03a Mon Sep 17 00:00:00 2001 From: Brummel Date: Wed, 13 May 2026 12:25:12 +0200 Subject: [PATCH] iter form-a.tidy: form_a.md class/instance/constraints + 3 documentary drift items MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Six-task post-fieldtest documentary tidy. No production-code behaviour changes; 559 tests green at every per-task gate. T1-T3: form_a.md additions - §Definitions intro "Three kinds" -> "Five kinds". - New `### Class — (class ...)` subsection: EBNF carries optional superclass (0 or 1 per ClassDef.superclass schema), method signatures with optional defaults; anchored to examples/test_22c_user_class_e2e.ail (ok 24/2). - New `### Instance — (instance ...)` subsection: EBNF carries the (method NAME (body LAM-TERM))* shape; canonical-form CLASS-REF rule explicitly stated (bare same-module / qualified cross-module); two examples — same-module abbreviated from mq3_class_eq_vs_fn_eq_classmod.ail and cross-module qualified from show_user_adt.ail; bare-cross-module-class-ref diagnostic named inline. - §Types `(forall ...)` line extended with optional `(constraints (constraint CLASS-REF TYPE)+)?` clause; explanatory paragraph added with no-instance diagnostic anchor; fifth example added to the Examples block anchored to cmp_max_smoke.ail. T4: docs/specs/2026-05-13-form-a-default-authoring.md "seven carve-outs" → "eight carve-outs" at 6 sites contradicting the §C4(b) compile-time-embed amendment (commit 9fcda8b). Sites: preamble line 11, §C1 line 170, §C2 line 191, §C3 line 218, §"Data flow" lines 363 + 374. Post-edit grep returns 4 surviving "seven" lines (233, 238, 463, 469), all correctly §C4(a)-scope or arithmetic/future-state. T5: crates/ailang-core/src/hash.rs:50-57 — delete empty `#[cfg(test)] mod tests {}` placeholder + 6-line relocation comment. Tests live in crates/ailang-core/tests/hash_pin.rs since form-a.1 T5; placeholder served no purpose. hash_pin.rs still 10/10 passing. T6: crates/ailang-surface/tests/round_trip.rs — module-level `//!` and inner `///` docstrings rewritten to the post-T10 four-property framing (parse-determinism / idempotency / CLI-pipeline-idempotency / carve-out-anchor) instead of the retired Direction-1/Direction-2 language. Sibling-crate breadcrumbs added pointing at the other two enforcement points (roundtrip_cli.rs, carve_out_inventory.rs). Drift item B2 (audit-form-a "plan file two sites") dropped per recon verification: docs/plans/2026-05-13-iter-form-a.1.md contains zero defective "seven" sites; all four hits are internally scoped to §C4(a), arithmetic, or future-state. Decision recorded in the journal. Closes 2 of 3 fieldtest-form-a spec_gap findings (#2 form_a.md typeclass surface + #3 form_a.md class-qualifier rule for instance) and 3 of 4 audit-form-a drift items. --- .../2026-05-13-iter-form-a.tidy.json | 19 ++++ crates/ailang-core/specs/form_a.md | 105 +++++++++++++++++- crates/ailang-core/src/hash.rs | 9 -- crates/ailang-surface/tests/round_trip.rs | 35 +++--- docs/journals/2026-05-13-iter-form-a.tidy.md | 103 +++++++++++++++++ .../2026-05-13-form-a-default-authoring.md | 12 +- 6 files changed, 252 insertions(+), 31 deletions(-) create mode 100644 bench/orchestrator-stats/2026-05-13-iter-form-a.tidy.json create mode 100644 docs/journals/2026-05-13-iter-form-a.tidy.md diff --git a/bench/orchestrator-stats/2026-05-13-iter-form-a.tidy.json b/bench/orchestrator-stats/2026-05-13-iter-form-a.tidy.json new file mode 100644 index 0000000..c6e3d4c --- /dev/null +++ b/bench/orchestrator-stats/2026-05-13-iter-form-a.tidy.json @@ -0,0 +1,19 @@ +{ + "iter_id": "form-a.tidy", + "date": "2026-05-13", + "mode": "standard", + "outcome": "DONE", + "tasks_total": 6, + "tasks_completed": 6, + "reloops_per_task": { + "1": 0, + "2": 0, + "3": 0, + "4": 0, + "5": 0, + "6": 0 + }, + "review_loops_spec": 0, + "review_loops_quality": 0, + "blocked_reason": null +} diff --git a/crates/ailang-core/specs/form_a.md b/crates/ailang-core/specs/form_a.md index 3862720..a0323bd 100644 --- a/crates/ailang-core/specs/form_a.md +++ b/crates/ailang-core/specs/form_a.md @@ -63,7 +63,7 @@ to the entry file's directory. ## Definitions -Three kinds, matched on the leading keyword: +Five kinds, matched on the leading keyword: ### Function — `(fn ...)` @@ -112,6 +112,93 @@ The list length must match the number of params in `type`. (body TERM)) ``` +### 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)))))) +``` + +### 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`. + ## Types Four shapes, all parenthesised except a bare type variable: @@ -122,7 +209,9 @@ TYVAR-NAME ; type variable (e.g. `a`, `T`) (fn-type (params PARAM*) (ret RETURN-PARAM) (effects EFFECT-NAME*)?) ; function type -(forall (vars TYVAR+) BODY-TYPE) ; polymorphic schema +(forall (vars TYVAR+) + (constraints (constraint CLASS-REF TYPE)+)? + BODY-TYPE) ; polymorphic schema with optional constraints ``` `PARAM` and `RETURN-PARAM` are types, optionally wrapped in a mode @@ -140,6 +229,16 @@ Effects are a set; order is irrelevant. Built-in type-constructors: `Int`, `Bool`, `Str`, `Unit`. User ADTs use the name from the `(data ...)` def. +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`. + Examples: ``` @@ -147,6 +246,8 @@ Examples: (con List (con Int)) (fn-type (params (own (con List)) (borrow (con Int))) (ret (con Int))) (forall (vars a) (fn-type (params (con List a)) (ret (con Int)))) +(forall (vars a) (constraints (constraint prelude.Ord a)) + (fn-type (params a a) (ret a))) ``` ## Terms diff --git a/crates/ailang-core/src/hash.rs b/crates/ailang-core/src/hash.rs index 292ed5e..eb4813f 100644 --- a/crates/ailang-core/src/hash.rs +++ b/crates/ailang-core/src/hash.rs @@ -46,12 +46,3 @@ pub fn def_hash(def: &Def) -> String { let hex = h.to_hex(); hex.as_str()[..16].to_string() } - -// `#[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 {} diff --git a/crates/ailang-surface/tests/round_trip.rs b/crates/ailang-surface/tests/round_trip.rs index 74ed435..d918101 100644 --- a/crates/ailang-surface/tests/round_trip.rs +++ b/crates/ailang-surface/tests/round_trip.rs @@ -1,24 +1,32 @@ -//! Round-trip gate for the form-(A) projection. +//! 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`: for every +//! 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`: -//! Direction 2 of the Roundtrip Invariant (DESIGN.md §"Roundtrip -//! Invariant"). For every well-formed `.ail` text `t`, asserts +//! 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 @@ -60,16 +68,15 @@ fn list_ail_fixtures() -> Vec { paths } -/// Direction 2 of the Roundtrip Invariant (DESIGN.md §"Roundtrip -/// Invariant"): for every well-formed `.ail` text `t`, the -/// composition `parse → print → parse` is idempotent on the AST. +/// 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. /// -/// For the 57 `.ail` fixtures that have a JSON counterpart this -/// follows logically from `print_then_parse_round_trips_every_fixture` -/// + `every_ail_fixture_matches_its_json_counterpart`. This test -/// asserts the property directly so it stays robust for future -/// `.ail` fixtures without a JSON counterpart, and so the spec's -/// Direction-2 claim has a dedicated enforcement point. +/// 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. #[test] fn parse_then_print_then_parse_is_idempotent_on_every_ail_fixture() { let fixtures = list_ail_fixtures(); diff --git a/docs/journals/2026-05-13-iter-form-a.tidy.md b/docs/journals/2026-05-13-iter-form-a.tidy.md new file mode 100644 index 0000000..c91c392 --- /dev/null +++ b/docs/journals/2026-05-13-iter-form-a.tidy.md @@ -0,0 +1,103 @@ +# iter form-a.tidy — close 3 of 4 documentary drift items from audit-form-a + fix 5 contradictory "seven carve-outs" sites + +**Date:** 2026-05-13 +**Started from:** 5e94204c218c410d44fbb8e658b677a7294744b0 +**Status:** DONE +**Tasks completed:** 6 of 6 + +## Summary + +Pure documentary tidy iteration. Three new sections landed in +`crates/ailang-core/specs/form_a.md` (Class declarations, Instance +declarations, Constraints on polymorphic fns), each anchored to a +real corpus fixture (`test_22c_user_class_e2e.ail`, +`mq3_class_eq_vs_fn_eq_classmod.ail`, `show_user_adt.ail`, +`cmp_max_smoke.ail`) and each fixture was `ail check`-verified to +produce the expected symbol counts before close. Six sites in +`docs/specs/2026-05-13-form-a-default-authoring.md` had "seven +carve-outs" tightened to "eight carve-outs" to match the §C4(b) +amendment. The empty `#[cfg(test)] mod tests {}` placeholder plus +its 6-line relocation comment was deleted from +`crates/ailang-core/src/hash.rs` (tests live in +`crates/ailang-core/tests/hash_pin.rs` since form-a.1 T5). The +`round_trip.rs` module-level and inner docstrings were rewritten +to use the post-T10 four-property framing (parse-determinism / +idempotency-under-print / CLI-pipeline-idempotency / +carve-out-anchor) instead of the retired Direction-1/Direction-2 +language, with cross-references to the sibling enforcement points +in `crates/ail/tests/roundtrip_cli.rs` and +`crates/ailang-core/tests/carve_out_inventory.rs`. + +No production-code behaviour changed. Workspace test count holds +at 559 passed at every per-task gate. + +## Per-task notes + +- iter form-a.tidy.1: `form_a.md` Class declarations section landed; §Definitions + intro updated `Three kinds` → `Five kinds`; example anchored to + `examples/test_22c_user_class_e2e.ail` (`ok (24 symbols across 2 modules)`). +- iter form-a.tidy.2: `form_a.md` Instance declarations section landed; two + examples (same-module abbreviated from `mq3_class_eq_vs_fn_eq_classmod.ail`, + cross-module from `show_user_adt.ail`); `bare-cross-module-class-ref` + diagnostic anchor named inline. +- iter form-a.tidy.3: `form_a.md` Constraints on polymorphic fns: extended + the four-shapes EBNF `(forall ...)` line with optional `(constraints ...)` + clause, added explanatory paragraph (with `no-instance` diagnostic anchor), + added fifth example to the Examples block anchored to `cmp_max_smoke.ail`. +- iter form-a.tidy.4: `docs/specs/2026-05-13-form-a-default-authoring.md` + six "seven" → "eight" edits across the preamble + §C1 + §C2 + §C3 + §"Data flow" + (two sites). Post-edit grep returned 4 surviving "seven" mentions at lines + 233, 238, 463, 469 — all correctly §C4(a)-scoped or arithmetic/future-state + (see Concerns below for one carrier-vs-plan transcription drift). +- iter form-a.tidy.5: `hash.rs` empty `mod tests {}` placeholder + 6-line + relocation comment block deleted (9 lines including the preceding blank). + `hash_pin.rs` integration tests still 10/10 passing. +- iter form-a.tidy.6: `round_trip.rs` module-level `//!` and inner `///` + rewritten to four-property framing with sibling-crate breadcrumbs. + `grep -n 'Direction [12]'` now zero hits. + +## Concerns + +- T4 carrier-vs-plan transcription drift on the Step 6 sanity-grep expected + output. The plan's Step 6 expected-output block listed four lines (233, + 238, 463, 469) but the carrier compressed this to "exactly the three + surviving lines named in T4 Step 6 (lines 238, 463, 469)". The actual + post-edit grep returns four lines matching the plan listing; line 233 + is §C4(a)-scope ("(seven files; the canonical") and is correctly retained. + No edit was missed. The carrier's three-line restatement was wrong; + the plan's four-line listing was right. Recording so a future auditor + re-reading the carrier doesn't second-guess the result. + +## Known debt + +- (none) + +## Files touched + +- `crates/ailang-core/specs/form_a.md` (+105/-) +- `crates/ailang-core/src/hash.rs` (-9) +- `crates/ailang-surface/tests/round_trip.rs` (+19/-12) +- `docs/specs/2026-05-13-form-a-default-authoring.md` (six 1-line edits) + +## Phase 3 (E2E coverage) + +Deliberately skipped per carrier: pure-documentary iter, no +behaviour change to cover. Verification gate was the per-task +`cargo test --workspace` smoke (559 green at every task close) +plus the per-task `ail check` runs on the four corpus fixtures +cited in the new form_a.md sections, all producing the expected +symbol counts (`test_22c_user_class_e2e.ail` ok 24/2, +`mq3_class_eq_vs_fn_eq_classmod.ail` ok 22/2, +`show_user_adt.ail` ok 23/2, `cmp_max_smoke.ail` ok 22/2). + +## Decision recorded — Drift item B2 (plan-file "seven carve-outs" orphans) + +Per plan §"Decision recorded" and the recon report: `docs/plans/2026-05-13-iter-form-a.1.md` +contains zero defective `seven` mentions; its 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 the plan file did not +match its contents at HEAD. No plan-file edit included in this iter. + +## Stats + +bench/orchestrator-stats/2026-05-13-iter-form-a.tidy.json diff --git a/docs/specs/2026-05-13-form-a-default-authoring.md b/docs/specs/2026-05-13-form-a-default-authoring.md index 501edac..21f9249 100644 --- a/docs/specs/2026-05-13-form-a-default-authoring.md +++ b/docs/specs/2026-05-13-form-a-default-authoring.md @@ -8,7 +8,7 @@ Make Form A (`.ail`) the sole authoring surface for every program in the working tree. After this milestone, the only `.ail.json` files -that remain in the repository are seven specific negative-test +that remain in the repository are eight specific negative-test fixtures whose subject matter cannot be expressed in Form A by construction. Every other `.ail.json` is rendered to its `.ail` sibling via `ail render`, and the now-redundant `.ail.json` is @@ -167,7 +167,7 @@ not the projection's relation to the AST. ### C1. Migration script A one-shot Bash script `scripts/migrate-to-form-a.sh` (new file) -walks `examples/*.ail.json`, skips the seven carve-outs (named +walks `examples/*.ail.json`, skips the eight carve-outs (named explicitly in the script body), invokes `ail render` to produce the sibling `.ail`, and `rm`s the JSON counterpart. The script is idempotent (re-running on a partially migrated tree is a no-op for @@ -188,7 +188,7 @@ The refactor is mechanical but spans three classes of consumer: `examples/.ail.json` with `fs::read_to_string` and passes the bytes to `Module::from_json` or the workspace loader. The refactor reads `examples/.ail` and parses via - `ailang_surface::parse_module_from_str`. The seven carve-outs + `ailang_surface::parse_module_from_str`. The eight carve-outs continue to use the `.ail.json` path (they have no `.ail` form by construction). 3. **Bench drivers** (`bench/*.py`, `bench/run.sh`). The drivers @@ -215,7 +215,7 @@ so the invariant restates as: | ail parse` (one round) is byte-identical to direct `ail parse` of the source `.ail`. Pins the user-facing CLI against drift internal tests cannot see. -- **Carve-out anchor.** The seven `.ail.json`-only fixtures are +- **Carve-out anchor.** The eight `.ail.json`-only fixtures are negative-tests (load-time / typecheck-time rejection); they participate only in the existing rejection-shape tests, not in the roundtrip gate. Their presence is the *only* surviving @@ -360,7 +360,7 @@ author writes: examples/.ail (every program) v Module value -> typecheck, codegen, ... -except for the seven carve-outs: +except for the eight carve-outs: examples/.ail.json | v @@ -371,7 +371,7 @@ Cross-module imports continue to use module names, not file paths; the workspace loader walks `examples/*` and accepts either extension for any module it loads. Since the bulk of the corpus is single- extension post-migration, the loader's extension-dispatch is exercised -only by the seven carve-outs (and by any test that explicitly mixes +only by the eight carve-outs (and by any test that explicitly mixes the two forms for migration testing). ## Error handling