From 2fc8c241630c385c28d15a069f8a0350bbbeec37 Mon Sep 17 00:00:00 2001 From: giles Date: Tue, 30 Jun 2026 12:32:58 +0000 Subject: [PATCH] =?UTF-8?q?maude:=20Phase=208=20design=20proposal=20?= =?UTF-8?q?=E2=80=94=20gate=20met,=20thin-kernel=20cut=20rejected=20on=20c?= =?UTF-8?q?onsumer=20evidence=20(facade=20recommended)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 4.8 --- plans/maude-on-sx.md | 67 ++++++++++++++++++++++++++++++++++++-------- 1 file changed, 56 insertions(+), 11 deletions(-) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index 3f20931a..755c3926 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -130,18 +130,63 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 nothing else applies, regardless of declaration order. Parser also reads `label`/`prec`/`owise`/`id:` eq+op attrs. 8 tests. -### Phase 8 — Propose `lib/guest/rewriting/` -- [ ] Extract equational matching engine (the most reusable piece). -- [ ] Extract normal-form-by-equations infrastructure. -- [ ] Extract strategy combinators. -- [ ] Wait for second consumer before extracting. +### Phase 8 — `lib/guest/rewriting/` extraction — DESIGN PROPOSAL (gate satisfied; thin-kernel cut REJECTED on evidence) +- [x] Wait for second consumer before extracting. **SATISFIED** — `lib/artdag` + is a live, saturated consumer (Phase-7 maude optimiser: `optimize-rules.sx` + parses a `fmod`, reduces, and gates on `mau/confluent?`). It is the only + external consumer; zero Blockers were filed against `lib/maude`, so the API + held under real use. +- [~] Extract equational matching engine — **DO NOT, as specified.** See below. +- [~] Extract normal-form-by-equations infrastructure — folds into the facade. +- [~] Extract strategy combinators — **DO NOT.** Zero external consumers. -**Status: BLOCKED — no second consumer yet.** The reusable core is identified: -`lib/maude/matching.sx` (AC matching + canon) + `lib/maude/fire.sx` -(short-circuit firing) are the prime extraction candidates; `lib/maude/strategy.sx` -(combinators) is the third. Keep them separable. Do not extract until a Pure/ -CafeOBJ/term-rewriting playground consumer appears (or artdag-on-sx's effect -optimiser, per the chisel note). +**Status: gate met, mechanical extraction NOT recommended.** Before cutting, +the consumer was measured. The result overturns the pre-registered plan. + +**What the plan assumed:** the reusable core is `matching.sx` (AC matching + +canon) + `fire.sx` (short-circuit firing), with `strategy.sx` third. + +**What the second consumer actually imports** (measured across `lib/artdag/*.sx`): + +| Layer | Symbols artdag uses | In planned kernel? | +|-------|--------------------|--------------------| +| `term.sx` | `mau/app` `mau/app?` `mau/const` `mau/op` `mau/args` | yes | +| `parser.sx` | `mau/parse-module` (artdag writes rules as `fmod … endfm` text) | **no — left in surface** | +| `conditional.sx` | `mau/creduce` `mau/creduce-term` `mau/creduce->str` `mau/ccanon` | partial | +| `confluence.sx` | `mau/confluent?` `mau/non-joinable-pairs` `mau/cp->str` | **no — added post-plan** | +| `matching.sx` / `fire.sx` / `strategy.sx` | **none directly** | the whole planned kernel | + +So the consumer reuses a **vertical** (term → parser → conditional → confluence), +not the horizontal AC kernel the plan named. It touches **none** of +matching/fire/strategy directly, and `strategy.sx` has **no consumer at all**. +Extracting matching+fire+strategy would produce a "reusable kernel" with nobody +reusing it — extraction-for-its-own-sake, exactly what the gate existed to prevent. + +**Why the vertical can't be cleanly thinned into a kernel:** the kernel +candidates' only coupling to the front-end is 7 parser symbols — +list utils `mau/take` `mau/drop` `mau/append2` (relocatable, theory-agnostic) and +module accessors `mau/module-eqs` `mau/module-ops` `mau/module-rules` +`mau/parse-term-in` (the eqs/ops/rules feed + in-signature term parsing). But the +real consumer *wants* the `fmod` parser — it authors rules as Maude text. A thin +term-rewriting kernel that excludes the parser does not serve it; a "kernel" that +includes the parser is just `lib/maude` renamed. + +**Recommended move (cheap, low-risk, real) — a public API facade, not a relocation:** +add `lib/maude/api.sx` re-exporting exactly the ~12 consumed symbols as the +supported surface (`mau/parse-module`, `mau/creduce*`/`mau/ccanon`, +`mau/confluent?`/`mau/non-joinable-pairs`/`mau/cp->str`, term ctors/accessors). +artdag imports the facade instead of nine `load "lib/maude/.sx"` lines; +the internal file layout becomes free to change without breaking the consumer. +This delivers the *encapsulation* value of extraction (a named, stable boundary) +without moving files across three trees (`lib/guest/` + `lib/maude/` + +`lib/artdag/`) or risking the two green suites (maude 274, artdag 225). + +**Defer the physical `lib/guest/rewriting/` split** until a *third* consumer +appears whose needs actually diverge from artdag's — at that point the boundary +will be drawn by two real shapes, not one plus a guess. The data dependency DAG +and the 7-symbol coupling set above are recorded so that cut is a 1-session job +when justified. **Sole remaining action if desired: the `api.sx` facade (in +scope: `lib/maude/**` only); coordinate artdag's import-side change separately.** ### SATURATION (post-roadmap)