maude: mark roadmap + extensions complete (254/254, saturated)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 38s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 38s
Plan: Phase 8 blocked on a 2nd consumer (matching+fire+strategy identified as extraction candidates); roadmap + 7 extensions done, end-state goal met. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
@@ -136,6 +136,27 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2
|
|||||||
- [ ] Extract strategy combinators.
|
- [ ] Extract strategy combinators.
|
||||||
- [ ] Wait for second consumer before extracting.
|
- [ ] 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
|
## lib/guest feedback loop
|
||||||
|
|
||||||
**Consumes:** `core/lex`, `core/pratt`, `core/ast`, `core/match` (with proposed extension for equational matching).
|
**Consumes:** `core/lex`, `core/pratt`, `core/ast`, `core/match` (with proposed extension for equational matching).
|
||||||
|
|||||||
Reference in New Issue
Block a user