diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index e401f1a6..adaf76ea 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -136,6 +136,27 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 - [ ] Extract strategy combinators. - [ ] Wait for second consumer before extracting. +**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). + +### SATURATION (post-roadmap) + +All 7 roadmap phases + 7 extensions (pretty / run / search-path / owise / +gather / order-sorted least-sort / search-command + result-sort) DONE, **254/254 +across 13 suites.** The end-state goal — a faithful Maude 3 functional+system +core that runs idiomatic programs and proves equational identities — is met: +sorts/subsorts/overloading, equational reduction modulo assoc/comm/id, +conditional eqs + owise, system rules (rew + BFS search with witness paths), +a strategy language, and META-LEVEL reflection, with a mixfix surface printer +and an end-to-end `.maude` runner (reduce/rewrite/search commands, sort-annotated +output). Pacing down to hardening. Possible niche future work: membership +axioms (`mb`/`cmb`), critical-pair / confluence checking, meta-search, full +mixfix (multi-`_` ops, juxtaposition `__`). + ## lib/guest feedback loop **Consumes:** `core/lex`, `core/pratt`, `core/ast`, `core/match` (with proposed extension for equational matching).