From 9f87206949f6c83051d5247f9dc798bf744279f4 Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 14:43:02 +0000 Subject: [PATCH 01/17] =?UTF-8?q?maude:=20Phase=201=20parser=20=E2=80=94?= =?UTF-8?q?=20fmod/mod=20modules,=20signatures,=20mixfix=20terms=20(65=20t?= =?UTF-8?q?ests)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Term representation (lib/maude/term.sx) plus a module parser (lib/maude/parser.sx) consuming lib/guest/lex + pratt: - whitespace+bracket tokenizer (--- / *** comments) - mixfix classification (split op names on _): infix/prefix/postfix/const - precedence-climbing term parser over a pratt table built from op decls - fmod/mod ... endfm/endm with sort/subsort/op/var/eq/ceq/rl/crl - transitive subsort hierarchy + operator overloading queries Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/maude/conformance.conf | 15 + lib/maude/conformance.sh | 3 + lib/maude/parser.sx | 673 +++++++++++++++++++++++++++++++++++++ lib/maude/scoreboard.json | 10 + lib/maude/scoreboard.md | 7 + lib/maude/term.sx | 114 +++++++ lib/maude/tests/parse.sx | 250 ++++++++++++++ plans/maude-on-sx.md | 27 +- 8 files changed, 1093 insertions(+), 6 deletions(-) create mode 100644 lib/maude/conformance.conf create mode 100755 lib/maude/conformance.sh create mode 100644 lib/maude/parser.sx create mode 100644 lib/maude/scoreboard.json create mode 100644 lib/maude/scoreboard.md create mode 100644 lib/maude/term.sx create mode 100644 lib/maude/tests/parse.sx diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf new file mode 100644 index 00000000..4fccc519 --- /dev/null +++ b/lib/maude/conformance.conf @@ -0,0 +1,15 @@ +# Maude conformance config — sourced by lib/guest/conformance.sh. + +LANG_NAME=maude +MODE=dict + +PRELOADS=( + lib/guest/lex.sx + lib/guest/pratt.sx + lib/maude/term.sx + lib/maude/parser.sx +) + +SUITES=( + "parse:lib/maude/tests/parse.sx:(mau-parse-tests-run!)" +) diff --git a/lib/maude/conformance.sh b/lib/maude/conformance.sh new file mode 100755 index 00000000..cff21bc1 --- /dev/null +++ b/lib/maude/conformance.sh @@ -0,0 +1,3 @@ +#!/usr/bin/env bash +# Thin wrapper — see lib/guest/conformance.sh and lib/maude/conformance.conf. +exec bash "$(dirname "$0")/../guest/conformance.sh" "$(dirname "$0")/conformance.conf" "$@" diff --git a/lib/maude/parser.sx b/lib/maude/parser.sx new file mode 100644 index 00000000..0196e9fc --- /dev/null +++ b/lib/maude/parser.sx @@ -0,0 +1,673 @@ +;; lib/maude/parser.sx — Maude module parser. +;; +;; Consumes lib/guest/lex.sx (whitespace classes) and lib/guest/pratt.sx +;; (operator-table lookup), plus lib/maude/term.sx (term constructors). +;; +;; Maude tokens are whitespace-delimited words plus the bracketing chars +;; ( ) [ ] { } , — so an operator name like _+_ or s_ or if_then_else_fi is a +;; single token. Statements end at a whitespace-delimited "." token. +;; +;; Grammar handled here: +;; (fmod|mod) NAME is ... (endfm|endm) +;; sort/sorts NAMES . +;; subsort/subsorts A B < C < D . +;; op/ops NAMES : ARITY -> RESULT [ATTRS] . +;; var/vars NAMES : SORT . +;; eq LHS = RHS . ceq LHS = RHS if COND . +;; rl [L] : LHS => RHS . crl [L] : LHS => RHS if COND . +;; +;; Terms: prefix application f(a,b) (op name may contain underscores, e.g. +;; the prefix form _+_(2,3)); mixfix prefix s_ written `s X`; mixfix infix +;; _+_ written `X + Y`, parsed by precedence climbing over a table built +;; from the op declarations. + +;; ---------- tokenizer ---------- + +(define + mau/special-char? + (fn + (c) + (or + (= c "(") + (= c ")") + (= c "[") + (= c "]") + (= c "{") + (= c "}") + (= c ",")))) + +(define + mau/tokenize + (fn + (src) + (let + ((toks (list)) (pos 0) (n (len src))) + (define + peekc + (fn (o) (if (< (+ pos o) n) (nth src (+ pos o)) nil))) + (define curc (fn () (peekc 0))) + (define adv! (fn (k) (set! pos (+ pos k)))) + (define + at-comment? + (fn + () + (or + (and + (= (curc) "-") + (= (peekc 1) "-") + (= (peekc 2) "-")) + (and + (= (curc) "*") + (= (peekc 1) "*") + (= (peekc 2) "*"))))) + (define + skip-line! + (fn + () + (when + (and (< pos n) (not (= (curc) "\n"))) + (do (adv! 1) (skip-line!))))) + (define + read-word! + (fn + (start) + (do + (when + (and + (< pos n) + (not (lex-whitespace? (curc))) + (not (mau/special-char? (curc)))) + (do (adv! 1) (read-word! start))) + (slice src start pos)))) + (define + scan! + (fn + () + (cond + ((>= pos n) nil) + ((lex-whitespace? (curc)) (do (adv! 1) (scan!))) + ((at-comment?) (do (skip-line!) (scan!))) + ((mau/special-char? (curc)) + (do (append! toks (curc)) (adv! 1) (scan!))) + (else (do (append! toks (read-word! pos)) (scan!)))))) + (scan!) + toks))) + +;; ---------- list helpers ---------- + +(define + mau/take + (fn + (xs k) + (if + (or (= k 0) (empty? xs)) + (list) + (cons (first xs) (mau/take (rest xs) (- k 1)))))) + +(define + mau/drop + (fn + (xs k) + (if + (or (= k 0) (empty? xs)) + xs + (mau/drop (rest xs) (- k 1))))) + +(define + mau/append2 + (fn + (xs ys) + (if (empty? xs) ys (cons (first xs) (mau/append2 (rest xs) ys))))) + +(define + mau/take-until + (fn + (xs tok) + (if + (or (empty? xs) (= (first xs) tok)) + (list) + (cons (first xs) (mau/take-until (rest xs) tok))))) + +(define + mau/drop-until + (fn + (xs tok) + (cond + ((empty? xs) (list)) + ((= (first xs) tok) xs) + (else (mau/drop-until (rest xs) tok))))) + +;; ---------- mixfix classification ---------- + +(define + mau/op-form + (fn + (name) + (let + ((parts (split name "_"))) + (cond + ((= (len parts) 1) {:kind :const :token name}) + ((and (= (len parts) 3) (= (nth parts 0) "") (= (nth parts 2) "") (not (= (nth parts 1) ""))) + {:kind :infix :token (nth parts 1)}) + ((and (= (len parts) 2) (not (= (nth parts 0) "")) (= (nth parts 1) "")) + {:kind :prefix :token (nth parts 0)}) + ((and (= (len parts) 2) (= (nth parts 0) "") (not (= (nth parts 1) ""))) + {:kind :postfix :token (nth parts 1)}) + (else {:kind :mixfix :token name}))))) + +(define + mau/default-prec + (fn + (kind) + (cond + ((= kind "infix") 41) + ((= kind "prefix") 15) + ((= kind "postfix") 15) + (else 0)))) + +(define + mau/op-prec + (fn + (op form) + (let + ((p (get (get op :attrs) :prec))) + (if (= p nil) (mau/default-prec (get form :kind)) p)))) + +(define + mau/build-infix-table + (fn + (ops) + (if + (empty? ops) + (list) + (let + ((op (first ops)) (rest-tbl (mau/build-infix-table (rest ops)))) + (let + ((form (mau/op-form (get op :name)))) + (if + (= (get form :kind) "infix") + (cons + (list (get form :token) (mau/op-prec op form) (get op :name)) + rest-tbl) + rest-tbl)))))) + +(define + mau/build-prefix-table + (fn + (ops) + (if + (empty? ops) + (list) + (let + ((op (first ops)) (rest-tbl (mau/build-prefix-table (rest ops)))) + (let + ((form (mau/op-form (get op :name)))) + (if + (= (get form :kind) "prefix") + (cons + (list (get form :token) (mau/op-prec op form) (get op :name)) + rest-tbl) + rest-tbl)))))) + +;; ---------- term parsing ---------- + +(define mau/has-colon? (fn (tok) (contains? tok ":"))) + +(define + mau/atom->term + (fn + (tok vars) + (cond + ((mau/has-colon? tok) + (let + ((parts (split tok ":"))) + (mau/var (nth parts 0) (nth parts 1)))) + ((not (= (get vars tok) nil)) (mau/var tok (get vars tok))) + (else (mau/const tok))))) + +(define + mau/parse-term + (fn + (toks grammar) + (let + ((ts toks) + (pos 0) + (n (len toks)) + (infix-tbl (get grammar :infix)) + (prefix-tbl (get grammar :prefix)) + (vars (get grammar :vars)) + (prefix-rbp 1000)) + (define tcur (fn () (if (< pos n) (nth ts pos) nil))) + (define + tpeek + (fn (o) (if (< (+ pos o) n) (nth ts (+ pos o)) nil))) + (define tadv! (fn () (set! pos (+ pos 1)))) + (define + parse-args + (fn + () + (if + (= (tcur) ")") + (do (tadv!) (list)) + (let + ((acc (list))) + (define + more + (fn + () + (do + (append! acc (parse-expr 0)) + (when (= (tcur) ",") (do (tadv!) (more)))))) + (do (more) (when (= (tcur) ")") (tadv!)) acc))))) + (define + parse-primary + (fn + () + (let + ((t (tcur))) + (cond + ((= t "(") + (do + (tadv!) + (let + ((e (parse-expr 0))) + (do (when (= (tcur) ")") (tadv!)) e)))) + ((not (= (pratt-op-lookup prefix-tbl t) nil)) + (let + ((entry (pratt-op-lookup prefix-tbl t))) + (do + (tadv!) + (let + ((operand (parse-expr prefix-rbp))) + (mau/app (nth entry 2) (list operand)))))) + ((= (tpeek 1) "(") + (let + ((name t)) + (do (tadv!) (tadv!) (mau/app name (parse-args))))) + (else (do (tadv!) (mau/atom->term t vars))))))) + (define + parse-expr + (fn + (minbp) + (let + ((lhs (parse-primary))) + (define + climb + (fn + (acc) + (let + ((t (tcur))) + (let + ((entry (if (= t nil) nil (pratt-op-lookup infix-tbl t)))) + (if + (= entry nil) + acc + (let + ((lbp (pratt-op-prec entry))) + (if + (< lbp minbp) + acc + (do + (tadv!) + (let + ((rhs (parse-expr (+ lbp 1)))) + (climb + (mau/app + (nth entry 2) + (list acc rhs)))))))))))) + (climb lhs)))) + (parse-expr 0)))) + +;; ---------- statement splitting ---------- + +(define + mau/split-statements + (fn + (toks) + (let + ((stmts (list)) (cur (list))) + (define + flush! + (fn + () + (when + (not (empty? cur)) + (do (append! stmts cur) (set! cur (list)))))) + (define + loop + (fn + (ts) + (cond + ((empty? ts) (flush!)) + ((= (first ts) ".") (do (flush!) (loop (rest ts)))) + (else (do (append! cur (first ts)) (loop (rest ts))))))) + (do (loop toks) stmts)))) + +(define + mau/split-groups + (fn + (toks) + (let + ((groups (list)) (cur (list))) + (define flush! (fn () (do (append! groups cur) (set! cur (list))))) + (define + loop + (fn + (ts) + (cond + ((empty? ts) (flush!)) + ((= (first ts) "<") (do (flush!) (loop (rest ts)))) + (else (do (append! cur (first ts)) (loop (rest ts))))))) + (do (loop toks) groups)))) + +;; ---------- attributes ---------- + +(define mau/strip-brackets (fn (toks) (mau/take-until (rest toks) "]"))) + +(define + mau/parse-attr-tokens + (fn + (toks) + (let + ((acc {})) + (define + loop + (fn + (ts) + (cond + ((empty? ts) nil) + ((= (first ts) "assoc") + (do (dict-set! acc :assoc true) (loop (rest ts)))) + ((= (first ts) "comm") + (do (dict-set! acc :comm true) (loop (rest ts)))) + ((or (= (first ts) "idem") (= (first ts) "idempotent")) + (do (dict-set! acc :idem true) (loop (rest ts)))) + ((= (first ts) "ctor") + (do (dict-set! acc :ctor true) (loop (rest ts)))) + ((= (first ts) "id:") + (do + (dict-set! acc :id (nth ts 1)) + (loop (mau/drop ts 2)))) + ((= (first ts) "prec") + (do + (dict-set! acc :prec (parse-number (nth ts 1))) + (loop (mau/drop ts 2)))) + (else (loop (rest ts)))))) + (do (loop toks) acc)))) + +(define + mau/parse-attrs + (fn + (toks) + (if + (or (empty? toks) (not (= (first toks) "["))) + {} + (mau/parse-attr-tokens (mau/strip-brackets toks))))) + +;; ---------- signature collection ---------- + +(define + mau/append-each! + (fn (acc xs) (for-each (fn (x) (append! acc x)) xs))) + +(define + mau/register-ops! + (fn + (ops names arity result attrs) + (for-each (fn (nm) (append! ops {:name nm :attrs attrs :arity arity :result result})) names))) + +(define + mau/each-set-var! + (fn + (vars names sort) + (for-each (fn (nm) (dict-set! vars nm sort)) names))) + +(define + mau/cross-append! + (fn + (acc g1 g2) + (for-each + (fn + (sub) + (for-each (fn (super) (append! acc (list sub super))) g2)) + g1))) + +(define + mau/add-subsort-chain! + (fn + (acc groups) + (when + (and (not (empty? groups)) (not (empty? (rest groups)))) + (do + (mau/cross-append! acc (first groups) (nth groups 1)) + (mau/add-subsort-chain! acc (rest groups)))))) + +(define + mau/add-subsorts! + (fn (acc body) (mau/add-subsort-chain! acc (mau/split-groups body)))) + +(define + mau/add-vars! + (fn + (vars body) + (let + ((names (mau/take-until body ":")) + (sort (first (rest (mau/drop-until body ":"))))) + (mau/each-set-var! vars names sort)))) + +(define + mau/add-ops! + (fn + (ops body) + (let + ((names (mau/take-until body ":")) + (afterc (rest (mau/drop-until body ":")))) + (let + ((arity (mau/take-until afterc "->")) + (aftera (rest (mau/drop-until afterc "->")))) + (let + ((result (first aftera)) + (attrs (mau/parse-attrs (mau/drop aftera 1)))) + (mau/register-ops! ops names arity result attrs)))))) + +(define + mau/collect-sig! + (fn + (stmts sorts subsorts ops vars) + (for-each + (fn + (s) + (let + ((head (first s)) (body (rest s))) + (cond + ((or (= head "sort") (= head "sorts")) + (mau/append-each! sorts body)) + ((or (= head "subsort") (= head "subsorts")) + (mau/add-subsorts! subsorts body)) + ((or (= head "op") (= head "ops")) (mau/add-ops! ops body)) + ((or (= head "var") (= head "vars")) (mau/add-vars! vars body)) + (else nil)))) + stmts))) + +;; ---------- equations / rules ---------- + +(define + mau/parse-cond + (fn + (toks grammar) + (if + (mau/member? "=" toks) + (let + ((l (mau/take-until toks "=")) + (r (rest (mau/drop-until toks "=")))) + {:lhs (mau/parse-term l grammar) :kind :eq :rhs (mau/parse-term r grammar)}) + {:kind :bool :term (mau/parse-term toks grammar)}))) + +(define + mau/parse-eq + (fn + (body grammar conditional?) + (let + ((lhs-toks (mau/take-until body "=")) + (after (rest (mau/drop-until body "=")))) + (if + conditional? + (let + ((rhs-toks (mau/take-until after "if")) + (cond-toks (rest (mau/drop-until after "if")))) + {:lhs (mau/parse-term lhs-toks grammar) :t :eq :cond (mau/parse-cond cond-toks grammar) :rhs (mau/parse-term rhs-toks grammar)}) + {:lhs (mau/parse-term lhs-toks grammar) :t :eq :cond nil :rhs (mau/parse-term after grammar)})))) + +(define + mau/strip-label + (fn + (body) + (if + (and (not (empty? body)) (= (first body) "[")) + (let + ((label (nth body 1)) (after (mau/drop body 3))) + (if + (and (not (empty? after)) (= (first after) ":")) + {:label label :rest (rest after)} + {:label label :rest after})) + {:label nil :rest body}))) + +(define + mau/parse-rule + (fn + (body grammar conditional?) + (let + ((b (mau/strip-label body))) + (let + ((label (get b :label)) (rest-toks (get b :rest))) + (let + ((lhs-toks (mau/take-until rest-toks "=>")) + (after (rest (mau/drop-until rest-toks "=>")))) + (if + conditional? + (let + ((rhs-toks (mau/take-until after "if")) + (cond-toks (rest (mau/drop-until after "if")))) + {:lhs (mau/parse-term lhs-toks grammar) :label label :t :rule :cond (mau/parse-cond cond-toks grammar) :rhs (mau/parse-term rhs-toks grammar)}) + {:lhs (mau/parse-term lhs-toks grammar) :label label :t :rule :cond nil :rhs (mau/parse-term after grammar)})))))) + +(define + mau/collect-rules! + (fn + (stmts grammar eqs rules) + (for-each + (fn + (s) + (let + ((head (first s)) (body (rest s))) + (cond + ((= head "eq") (append! eqs (mau/parse-eq body grammar false))) + ((= head "ceq") (append! eqs (mau/parse-eq body grammar true))) + ((= head "rl") + (append! rules (mau/parse-rule body grammar false))) + ((= head "crl") + (append! rules (mau/parse-rule body grammar true))) + (else nil)))) + stmts))) + +;; ---------- module assembly ---------- + +(define mau/make-grammar (fn (ops vars) {:prefix (mau/build-prefix-table ops) :ops ops :vars vars :infix (mau/build-infix-table ops)})) + +(define + mau/build-module + (fn + (kind name body) + (let + ((stmts (mau/split-statements body)) + (sorts (list)) + (subsorts (list)) + (ops (list)) + (vars {}) + (eqs (list)) + (rules (list))) + (mau/collect-sig! stmts sorts subsorts ops vars) + (let + ((grammar (mau/make-grammar ops vars))) + (mau/collect-rules! stmts grammar eqs rules) + {:name name :grammar grammar :sorts sorts :eqs eqs :ops ops :t :module :vars vars :subsorts subsorts :kind kind :rules rules})))) + +(define + mau/parse-module + (fn + (src) + (let + ((toks (mau/tokenize src))) + (let + ((kind (nth toks 0)) (name (nth toks 1))) + (let + ((body (mau/take (mau/drop toks 3) (- (len toks) 4)))) + (mau/build-module kind name body)))))) + +;; ---------- signature queries ---------- + +(define mau/module-name (fn (m) (get m :name))) +(define mau/module-kind (fn (m) (get m :kind))) +(define mau/module-sorts (fn (m) (get m :sorts))) +(define mau/module-subsorts (fn (m) (get m :subsorts))) +(define mau/module-ops (fn (m) (get m :ops))) +(define mau/module-vars (fn (m) (get m :vars))) +(define mau/module-eqs (fn (m) (get m :eqs))) +(define mau/module-rules (fn (m) (get m :rules))) +(define mau/module-grammar (fn (m) (get m :grammar))) + +(define + mau/parse-term-in + (fn (m src) (mau/parse-term (mau/tokenize src) (mau/module-grammar m)))) + +(define + mau/collect-supers + (fn + (pairs s) + (cond + ((empty? pairs) (list)) + ((= (first (first pairs)) s) + (cons + (nth (first pairs) 1) + (mau/collect-supers (rest pairs) s))) + (else (mau/collect-supers (rest pairs) s))))) + +(define mau/supers-of (fn (m s) (mau/collect-supers (get m :subsorts) s))) + +(define + mau/dfs-reach + (fn + (m frontier target seen) + (cond + ((empty? frontier) false) + ((= (first frontier) target) true) + ((mau/member? (first frontier) seen) + (mau/dfs-reach m (rest frontier) target seen)) + (else + (mau/dfs-reach + m + (mau/append2 (mau/supers-of m (first frontier)) (rest frontier)) + target + (cons (first frontier) seen)))))) + +(define + mau/subsort? + (fn + (m sub super) + (mau/dfs-reach m (mau/supers-of m sub) super (list sub)))) + +(define mau/sort<=? (fn (m a b) (or (= a b) (mau/subsort? m a b)))) + +(define + mau/filter-ops + (fn + (ops name) + (cond + ((empty? ops) (list)) + ((= (get (first ops) :name) name) + (cons (first ops) (mau/filter-ops (rest ops) name))) + (else (mau/filter-ops (rest ops) name))))) + +(define + mau/ops-named + (fn (m name) (mau/filter-ops (mau/module-ops m) name))) diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json new file mode 100644 index 00000000..483579f1 --- /dev/null +++ b/lib/maude/scoreboard.json @@ -0,0 +1,10 @@ +{ + "lang": "maude", + "total_passed": 65, + "total_failed": 0, + "total": 65, + "suites": [ + {"name":"parse","passed":65,"failed":0,"total":65} + ], + "generated": "2026-06-07T14:42:29+00:00" +} diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md new file mode 100644 index 00000000..ca01f652 --- /dev/null +++ b/lib/maude/scoreboard.md @@ -0,0 +1,7 @@ +# maude scoreboard + +**65 / 65 passing** (0 failure(s)). + +| Suite | Passed | Total | Status | +|-------|--------|-------|--------| +| parse | 65 | 65 | ok | diff --git a/lib/maude/term.sx b/lib/maude/term.sx new file mode 100644 index 00000000..c29a04ae --- /dev/null +++ b/lib/maude/term.sx @@ -0,0 +1,114 @@ +;; lib/maude/term.sx — Maude term representation. +;; +;; A term is one of: +;; variable {:t :var :name "X" :sort "Nat"} +;; application {:t :app :op "_+_" :args (a b ...)} (constant: empty args) +;; +;; Sorts attach to variables; operator/result sorts live on op declarations +;; in the module signature, not on the term node. Overloading is resolved at +;; reduction time, so the parser only records the operator name. + +(define mau/var (fn (name sort) {:name name :t :var :sort sort})) + +(define mau/app (fn (op args) {:op op :t :app :args args})) + +(define mau/const (fn (op) {:op op :t :app :args (list)})) + +(define mau/var? (fn (t) (and (dict? t) (= (get t :t) "var")))) + +(define mau/app? (fn (t) (and (dict? t) (= (get t :t) "app")))) + +(define mau/term? (fn (t) (or (mau/var? t) (mau/app? t)))) + +(define mau/op (fn (t) (get t :op))) +(define mau/args (fn (t) (get t :args))) +(define mau/vname (fn (t) (get t :name))) +(define mau/vsort (fn (t) (get t :sort))) +(define mau/arity (fn (t) (len (get t :args)))) + +(define mau/const? (fn (t) (and (mau/app? t) (empty? (mau/args t))))) + +(define + mau/args=? + (fn + (as bs) + (cond + ((and (empty? as) (empty? bs)) true) + ((or (empty? as) (empty? bs)) false) + (else + (and + (mau/term=? (first as) (first bs)) + (mau/args=? (rest as) (rest bs))))))) + +(define + mau/term=? + (fn + (a b) + (cond + ((and (mau/var? a) (mau/var? b)) + (and + (= (mau/vname a) (mau/vname b)) + (= (mau/vsort a) (mau/vsort b)))) + ((and (mau/app? a) (mau/app? b)) + (and + (= (mau/op a) (mau/op b)) + (mau/args=? (mau/args a) (mau/args b)))) + (else false)))) + +(define + mau/join-args + (fn + (args) + (cond + ((empty? args) "") + ((empty? (rest args)) (mau/term->str (first args))) + (else + (str (mau/term->str (first args)) ", " (mau/join-args (rest args))))))) + +(define + mau/term->str + (fn + (t) + (cond + ((mau/var? t) (mau/vname t)) + ((mau/const? t) (mau/op t)) + ((mau/app? t) (str (mau/op t) "(" (mau/join-args (mau/args t)) ")")) + (else "?")))) + +(define + mau/member? + (fn + (x xs) + (cond + ((empty? xs) false) + ((= x (first xs)) true) + (else (mau/member? x (rest xs)))))) + +(define + mau/union + (fn + (xs ys) + (cond + ((empty? xs) ys) + ((mau/member? (first xs) ys) (mau/union (rest xs) ys)) + (else (cons (first xs) (mau/union (rest xs) ys)))))) + +(define + mau/term-vars + (fn + (t) + (cond + ((mau/var? t) (list (mau/vname t))) + ((mau/app? t) (mau/term-vars-list (mau/args t))) + (else (list))))) + +(define + mau/term-vars-list + (fn + (args) + (if + (empty? args) + (list) + (mau/union + (mau/term-vars (first args)) + (mau/term-vars-list (rest args)))))) diff --git a/lib/maude/tests/parse.sx b/lib/maude/tests/parse.sx new file mode 100644 index 00000000..d16669ff --- /dev/null +++ b/lib/maude/tests/parse.sx @@ -0,0 +1,250 @@ +;; lib/maude/tests/parse.sx — Phase 1: tokenizer, signatures, term/eq parsing. + +(define mpt-pass 0) +(define mpt-fail 0) +(define mpt-failures (list)) + +(define + mpt-check! + (fn + (name got expected) + (if + (= got expected) + (set! mpt-pass (+ mpt-pass 1)) + (do + (set! mpt-fail (+ mpt-fail 1)) + (append! + mpt-failures + (str name " expected: " expected " got: " got)))))) + +;; ---- modules under test ---- + +(define + mpt-peano + (mau/parse-module + "fmod PEANO is\n sort Nat .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op _+_ : Nat Nat -> Nat [assoc comm prec 33] .\n op _*_ : Nat Nat -> Nat [assoc comm] .\n vars X Y : Nat .\n eq 0 + X = X .\n eq s X + Y = s (X + Y) .\n eq 0 * X = 0 .\nendfm")) + +(define + mpt-natlist + (mau/parse-module + "fmod NATLIST is\n sorts Zero NzNat Nat List .\n subsort Zero < Nat .\n subsort NzNat < Nat .\n subsort Nat < List .\n op 0 : -> Zero .\n op nil : -> List .\n op _;_ : List List -> List [assoc id: nil] .\n op head : List -> Nat .\n op length : List -> Nat .\n vars L M : List .\n var N : Nat .\n eq length(nil) = 0 .\n eq head(N ; L) = N .\nendfm")) + +;; ---- tokenizer ---- + +(define mpt-toks (mau/tokenize "op _+_ : Nat Nat -> Nat [assoc] .")) + +(mpt-check! "tok-count" (len mpt-toks) 11) +(mpt-check! "tok-op" (nth mpt-toks 0) "op") +(mpt-check! "tok-mixfix" (nth mpt-toks 1) "_+_") +(mpt-check! "tok-colon" (nth mpt-toks 2) ":") +(mpt-check! "tok-arrow" (nth mpt-toks 5) "->") +(mpt-check! "tok-lbrack" (nth mpt-toks 7) "[") +(mpt-check! "tok-dot" (nth mpt-toks 10) ".") +(mpt-check! + "tok-comment" + (len (mau/tokenize "sort Nat . --- a comment\nop 0 : -> Nat .")) + 9) + +;; ---- mixfix classification ---- + +(mpt-check! "form-infix" (get (mau/op-form "_+_") :kind) "infix") +(mpt-check! "form-infix-tok" (get (mau/op-form "_+_") :token) "+") +(mpt-check! "form-prefix" (get (mau/op-form "s_") :kind) "prefix") +(mpt-check! "form-prefix-tok" (get (mau/op-form "s_") :token) "s") +(mpt-check! "form-postfix" (get (mau/op-form "_!") :kind) "postfix") +(mpt-check! "form-const" (get (mau/op-form "nil") :kind) "const") +(mpt-check! + "form-mixfix" + (get (mau/op-form "if_then_else_fi") :kind) + "mixfix") + +;; ---- module header / sorts ---- + +(mpt-check! "mod-name" (mau/module-name mpt-peano) "PEANO") +(mpt-check! "mod-kind" (mau/module-kind mpt-peano) "fmod") +(mpt-check! "mod-sorts" (mau/module-sorts mpt-peano) (list "Nat")) +(mpt-check! + "natlist-sorts-count" + (len (mau/module-sorts mpt-natlist)) + 4) + +;; ---- subsorts (direct + transitive) ---- + +(mpt-check! "subsort-direct" (mau/subsort? mpt-natlist "NzNat" "Nat") true) +(mpt-check! "subsort-trans" (mau/subsort? mpt-natlist "NzNat" "List") true) +(mpt-check! "subsort-trans2" (mau/subsort? mpt-natlist "Zero" "List") true) +(mpt-check! "subsort-none" (mau/subsort? mpt-natlist "List" "Nat") false) +(mpt-check! "sort<=-refl" (mau/sort<=? mpt-natlist "Nat" "Nat") true) +(mpt-check! "sort<=-trans" (mau/sort<=? mpt-natlist "Zero" "List") true) + +;; ---- operators / overloading ---- + +(mpt-check! "ops-count" (len (mau/module-ops mpt-peano)) 4) +(mpt-check! + "op-arity" + (get (first (mau/ops-named mpt-peano "_+_")) :arity) + (list "Nat" "Nat")) +(mpt-check! + "op-result" + (get (first (mau/ops-named mpt-peano "s_")) :result) + "Nat") +(mpt-check! + "op-const-arity" + (len (get (first (mau/ops-named mpt-peano "0")) :arity)) + 0) +(mpt-check! + "natlist-ops-count" + (len (mau/module-ops mpt-natlist)) + 5) + +;; ---- attributes ---- + +(mpt-check! + "attr-assoc" + (get (get (first (mau/ops-named mpt-peano "_+_")) :attrs) :assoc) + true) +(mpt-check! + "attr-comm" + (get (get (first (mau/ops-named mpt-peano "_+_")) :attrs) :comm) + true) +(mpt-check! + "attr-prec" + (get (get (first (mau/ops-named mpt-peano "_+_")) :attrs) :prec) + 33) +(mpt-check! + "attr-id" + (get (get (first (mau/ops-named mpt-natlist "_;_")) :attrs) :id) + "nil") +(mpt-check! + "attr-absent" + (get (get (first (mau/ops-named mpt-peano "_*_")) :attrs) :prec) + nil) + +;; ---- variables ---- + +(mpt-check! "var-sort" (get (mau/module-vars mpt-peano) "X") "Nat") +(mpt-check! "var-list-sort" (get (mau/module-vars mpt-natlist) "L") "List") + +;; ---- term parsing ---- + +(mpt-check! + "term-const" + (mau/term->str (mau/parse-term-in mpt-peano "0")) + "0") +(mpt-check! + "term-prefix-mixfix" + (mau/term->str (mau/parse-term-in mpt-peano "s 0")) + "s_(0)") +(mpt-check! + "term-nested-prefix" + (mau/term->str (mau/parse-term-in mpt-peano "s s 0")) + "s_(s_(0))") +(mpt-check! + "term-infix" + (mau/term->str (mau/parse-term-in mpt-peano "X + Y")) + "_+_(X, Y)") +(mpt-check! + "term-prec" + (mau/term->str (mau/parse-term-in mpt-peano "s X + Y")) + "_+_(s_(X), Y)") +(mpt-check! + "term-paren" + (mau/term->str (mau/parse-term-in mpt-peano "s (X + Y)")) + "s_(_+_(X, Y))") +(mpt-check! + "term-left-assoc" + (mau/term->str (mau/parse-term-in mpt-peano "X + Y + X")) + "_+_(_+_(X, Y), X)") +(mpt-check! + "term-prefix-form" + (mau/term->str (mau/parse-term-in mpt-peano "_+_(X, 0)")) + "_+_(X, 0)") +(mpt-check! + "term-funcall" + (mau/term->str (mau/parse-term-in mpt-natlist "length(nil)")) + "length(nil)") +(mpt-check! + "term-onthefly-var" + (mau/var? (mau/parse-term-in mpt-peano "Z:Nat")) + true) +(mpt-check! + "term-onthefly-sort" + (mau/vsort (mau/parse-term-in mpt-peano "Z:Nat")) + "Nat") +(mpt-check! + "term-var-vs-const" + (mau/var? (mau/parse-term-in mpt-peano "X")) + true) +(mpt-check! + "term-const-not-var" + (mau/var? (mau/parse-term-in mpt-peano "0")) + false) + +;; ---- equations ---- + +(mpt-check! "eq-count" (len (mau/module-eqs mpt-peano)) 3) +(mpt-check! + "eq-lhs" + (mau/term->str (get (nth (mau/module-eqs mpt-peano) 1) :lhs)) + "_+_(s_(X), Y)") +(mpt-check! + "eq-rhs" + (mau/term->str (get (nth (mau/module-eqs mpt-peano) 1) :rhs)) + "s_(_+_(X, Y))") +(mpt-check! + "eq-uncond" + (get (nth (mau/module-eqs mpt-peano) 0) :cond) + nil) +(mpt-check! + "natlist-eq-head" + (mau/term->str (get (nth (mau/module-eqs mpt-natlist) 1) :lhs)) + "head(_;_(N, L))") + +;; ---- conditional equations ---- + +(define + mpt-gcd + (mau/parse-module + "fmod GCD is\n sort Nat .\n op _>_ : Nat Nat -> Bool .\n op _-_ : Nat Nat -> Nat .\n op gcd : Nat Nat -> Nat .\n vars X Y : Nat .\n ceq gcd(X, Y) = gcd(X - Y, Y) if X > Y = true .\nendfm")) + +(mpt-check! "ceq-count" (len (mau/module-eqs mpt-gcd)) 1) +(mpt-check! + "ceq-has-cond" + (= (get (first (mau/module-eqs mpt-gcd)) :cond) nil) + false) +(mpt-check! + "ceq-cond-kind" + (get (get (first (mau/module-eqs mpt-gcd)) :cond) :kind) + "eq") +(mpt-check! + "ceq-cond-lhs" + (mau/term->str (get (get (first (mau/module-eqs mpt-gcd)) :cond) :lhs)) + "_>_(X, Y)") + +;; ---- system module + rules ---- + +(define + mpt-vending + (mau/parse-module + "mod VENDING is\n sort State .\n op _coin : State -> State .\n op buy : State -> State .\n var S : State .\n rl [insert] : S coin => buy(S) .\n crl [guard] : buy(S) => S if S = S .\nendfm")) + +(mpt-check! "mod-kind-mod" (mau/module-kind mpt-vending) "mod") +(mpt-check! "rules-count" (len (mau/module-rules mpt-vending)) 2) +(mpt-check! + "rule-label" + (get (first (mau/module-rules mpt-vending)) :label) + "insert") +(mpt-check! + "rule-rhs" + (mau/term->str (get (first (mau/module-rules mpt-vending)) :rhs)) + "buy(S)") +(mpt-check! + "crl-label" + (get (nth (mau/module-rules mpt-vending) 1) :label) + "guard") +(mpt-check! + "crl-cond-kind" + (get (get (nth (mau/module-rules mpt-vending) 1) :cond) :kind) + "eq") + +(define mau-parse-tests-run! (fn () {:failures mpt-failures :total (+ mpt-pass mpt-fail) :passed mpt-pass :failed mpt-fail})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index e5526ffd..d559af7a 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -62,10 +62,10 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 ## Roadmap ### Phase 1 — Parser + signatures -- [ ] Parser for `fmod` / `endfm` syntax, sort declarations, op declarations, equations. -- [ ] Sort hierarchy with subsort relations. -- [ ] Operator overloading by arity + sort. -- [ ] Tests: parse classic examples (peano nat, list of naturals). +- [x] Parser for `fmod` / `endfm` syntax, sort declarations, op declarations, equations. +- [x] Sort hierarchy with subsort relations. +- [x] Operator overloading by arity + sort. +- [x] Tests: parse classic examples (peano nat, list of naturals). ### Phase 2 — Syntactic equational reduction - [ ] Apply equations left-to-right until no equation matches. @@ -125,7 +125,22 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 - Pure language (Albrecht Gräf): https://agraef.github.io/pure-lang/ — practical functional rewriting. ## Progress log -_(awaiting Phase 1 — depends on substrate matching maturity from lib/guest/core/match.sx)_ + +- **Phase 1 (parser + signatures) — DONE, 65/65.** `lib/maude/term.sx` (term + repr: var/app dicts, equality, vars, `term->str`) + `lib/maude/parser.sx` + (whitespace+bracket tokenizer with `---`/`***` comments; mixfix + classification by splitting op names on `_`; precedence-climbing term parser + over a pratt table built from op decls; `fmod`/`mod` modules with + sorts/subsorts/ops/vars/eqs/rules). Consumes `lib/guest/lex.sx` (ws classes) + and `lib/guest/pratt.sx` (op-table lookup). Verified on Peano (`s X + Y` + parses `_+_(s_(X), Y)` — prefix binds tighter than infix) and NatList + (transitive subsorts NzNat Date: Sun, 7 Jun 2026 14:46:02 +0000 Subject: [PATCH 02/17] maude: Phase 2 syntactic equational reduction (26 tests, 91 total) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit lib/maude/reduce.sx — one-sided syntactic matching (non-linear patterns via bound-var equality), immutable substitutions, innermost fixpoint normalisation. Tested on Peano arithmetic, list ops, a propositional logic simplifier, and non-linear matching. Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/maude/conformance.conf | 2 + lib/maude/reduce.sx | 143 +++++++++++++++++++++++++++++++++++++ lib/maude/scoreboard.json | 9 +-- lib/maude/scoreboard.md | 3 +- lib/maude/tests/reduce.sx | 120 +++++++++++++++++++++++++++++++ plans/maude-on-sx.md | 17 ++++- 6 files changed, 286 insertions(+), 8 deletions(-) create mode 100644 lib/maude/reduce.sx create mode 100644 lib/maude/tests/reduce.sx diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf index 4fccc519..af3f75da 100644 --- a/lib/maude/conformance.conf +++ b/lib/maude/conformance.conf @@ -8,8 +8,10 @@ PRELOADS=( lib/guest/pratt.sx lib/maude/term.sx lib/maude/parser.sx + lib/maude/reduce.sx ) SUITES=( "parse:lib/maude/tests/parse.sx:(mau-parse-tests-run!)" + "reduce:lib/maude/tests/reduce.sx:(mau-reduce-tests-run!)" ) diff --git a/lib/maude/reduce.sx b/lib/maude/reduce.sx new file mode 100644 index 00000000..2ae0a5cc --- /dev/null +++ b/lib/maude/reduce.sx @@ -0,0 +1,143 @@ +;; lib/maude/reduce.sx — syntactic equational reduction (Phase 2). +;; +;; Apply unconditional equations left-to-right to a fixpoint, using strict +;; one-sided syntactic matching (no theories yet — assoc/comm/id come in +;; Phase 3). Reduction is innermost: arguments are normalised before the +;; enclosing operator is rewritten. +;; +;; A substitution is a dict VAR-NAME -> term, extended immutably via `assoc`. +;; Matching is one-sided: only the pattern (equation LHS) carries variables; +;; the subject is treated structurally. + +;; ---------- matching ---------- + +(define + mau/match + (fn + (pat subj s) + (cond + ((= s nil) nil) + ((mau/var? pat) + (let + ((bound (get s (mau/vname pat)))) + (if + (= bound nil) + (assoc s (mau/vname pat) subj) + (if (mau/term=? bound subj) s nil)))) + ((and (mau/app? pat) (mau/app? subj)) + (if + (and + (= (mau/op pat) (mau/op subj)) + (= (mau/arity pat) (mau/arity subj))) + (mau/match-args (mau/args pat) (mau/args subj) s) + nil)) + (else nil)))) + +(define + mau/match-args + (fn + (ps ss s) + (cond + ((= s nil) nil) + ((and (empty? ps) (empty? ss)) s) + ((or (empty? ps) (empty? ss)) nil) + (else + (mau/match-args + (rest ps) + (rest ss) + (mau/match (first ps) (first ss) s)))))) + +;; ---------- substitution application ---------- + +(define + mau/subst-apply-list + (fn + (s args) + (if + (empty? args) + (list) + (cons + (mau/subst-apply s (first args)) + (mau/subst-apply-list s (rest args)))))) + +(define + mau/subst-apply + (fn + (s term) + (cond + ((mau/var? term) + (let ((b (get s (mau/vname term)))) (if (= b nil) term b))) + ((mau/app? term) + (mau/app (mau/op term) (mau/subst-apply-list s (mau/args term)))) + (else term)))) + +;; ---------- top-level rewrite ---------- + +;; Try each unconditional equation in order; on the first whose LHS matches +;; the term, return the instantiated RHS. nil if none apply. +(define + mau/rewrite-top + (fn + (eqs term) + (cond + ((empty? eqs) nil) + (else + (let + ((eq (first eqs))) + (if + (= (get eq :cond) nil) + (let + ((s (mau/match (get eq :lhs) term {}))) + (if + (= s nil) + (mau/rewrite-top (rest eqs) term) + (mau/subst-apply s (get eq :rhs)))) + (mau/rewrite-top (rest eqs) term))))))) + +;; ---------- normalisation (innermost to fixpoint) ---------- + +(define + mau/normalize-args + (fn + (eqs args fuel) + (if + (empty? args) + (list) + (cons + (mau/normalize eqs (first args) fuel) + (mau/normalize-args eqs (rest args) fuel))))) + +(define + mau/normalize + (fn + (eqs term fuel) + (if + (<= fuel 0) + term + (cond + ((mau/var? term) term) + ((mau/app? term) + (let + ((nargs (mau/normalize-args eqs (mau/args term) fuel))) + (let + ((t2 (mau/app (mau/op term) nargs))) + (let + ((r (mau/rewrite-top eqs t2))) + (if (= r nil) t2 (mau/normalize eqs r (- fuel 1))))))) + (else term))))) + +;; ---------- module-level API ---------- + +(define mau/reduce-fuel 1000000) + +(define + mau/reduce + (fn (m term) (mau/normalize (mau/module-eqs m) term mau/reduce-fuel))) + +(define + mau/reduce-term + (fn (m src) (mau/reduce m (mau/parse-term-in m src)))) + +(define + mau/reduce->str + (fn (m src) (mau/term->str (mau/reduce-term m src)))) diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json index 483579f1..e9ea5da0 100644 --- a/lib/maude/scoreboard.json +++ b/lib/maude/scoreboard.json @@ -1,10 +1,11 @@ { "lang": "maude", - "total_passed": 65, + "total_passed": 91, "total_failed": 0, - "total": 65, + "total": 91, "suites": [ - {"name":"parse","passed":65,"failed":0,"total":65} + {"name":"parse","passed":65,"failed":0,"total":65}, + {"name":"reduce","passed":26,"failed":0,"total":26} ], - "generated": "2026-06-07T14:42:29+00:00" + "generated": "2026-06-07T14:45:37+00:00" } diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md index ca01f652..3d9e113e 100644 --- a/lib/maude/scoreboard.md +++ b/lib/maude/scoreboard.md @@ -1,7 +1,8 @@ # maude scoreboard -**65 / 65 passing** (0 failure(s)). +**91 / 91 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| | parse | 65 | 65 | ok | +| reduce | 26 | 26 | ok | diff --git a/lib/maude/tests/reduce.sx b/lib/maude/tests/reduce.sx new file mode 100644 index 00000000..0e09549e --- /dev/null +++ b/lib/maude/tests/reduce.sx @@ -0,0 +1,120 @@ +;; lib/maude/tests/reduce.sx — Phase 2: syntactic equational reduction. + +(define mrt-pass 0) +(define mrt-fail 0) +(define mrt-failures (list)) + +(define + mrt-check! + (fn + (name got expected) + (if + (= got expected) + (set! mrt-pass (+ mrt-pass 1)) + (do + (set! mrt-fail (+ mrt-fail 1)) + (append! + mrt-failures + (str name " expected: " expected " got: " got)))))) + +;; ---- Peano arithmetic ---- + +(define + mrt-peano + (mau/parse-module + "fmod PEANO is\n sort Nat .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op _+_ : Nat Nat -> Nat .\n op _*_ : Nat Nat -> Nat .\n vars X Y : Nat .\n eq 0 + Y = Y .\n eq s X + Y = s (X + Y) .\n eq 0 * Y = 0 .\n eq s X * Y = Y + (X * Y) .\nendfm")) + +(mrt-check! + "add-2-1" + (mau/reduce->str mrt-peano "s s 0 + s 0") + "s_(s_(s_(0)))") +(mrt-check! "add-0-0" (mau/reduce->str mrt-peano "0 + 0") "0") +(mrt-check! "add-id-left" (mau/reduce->str mrt-peano "0 + s s 0") "s_(s_(0))") +(mrt-check! + "mul-2-2" + (mau/reduce->str mrt-peano "s s 0 * s s 0") + "s_(s_(s_(s_(0))))") +(mrt-check! "mul-zero" (mau/reduce->str mrt-peano "0 * s s s 0") "0") +(mrt-check! "mul-by-zero" (mau/reduce->str mrt-peano "s s 0 * 0") "0") +(mrt-check! + "nested" + (mau/reduce->str mrt-peano "(s 0 + s 0) * s s 0") + "s_(s_(s_(s_(0))))") + +;; ---- list manipulation ---- + +(define + mrt-list + (mau/parse-module + "fmod NATLIST is\n sorts Nat List .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op nil : -> List .\n op cons : Nat List -> List .\n op append : List List -> List .\n op length : List -> Nat .\n op rev : List -> List .\n var X : Nat .\n vars L M : List .\n eq append(nil, M) = M .\n eq append(cons(X, L), M) = cons(X, append(L, M)) .\n eq length(nil) = 0 .\n eq length(cons(X, L)) = s length(L) .\n eq rev(nil) = nil .\n eq rev(cons(X, L)) = append(rev(L), cons(X, nil)) .\nendfm")) + +(mrt-check! + "append" + (mau/reduce->str mrt-list "append(cons(0, nil), cons(s 0, nil))") + "cons(0, cons(s_(0), nil))") +(mrt-check! + "append-nil" + (mau/reduce->str mrt-list "append(nil, cons(0, nil))") + "cons(0, nil)") +(mrt-check! + "length-2" + (mau/reduce->str mrt-list "length(cons(0, cons(s 0, nil)))") + "s_(s_(0))") +(mrt-check! "length-0" (mau/reduce->str mrt-list "length(nil)") "0") +(mrt-check! + "rev" + (mau/reduce->str mrt-list "rev(cons(0, cons(s 0, nil)))") + "cons(s_(0), cons(0, nil))") +(mrt-check! "rev-empty" (mau/reduce->str mrt-list "rev(nil)") "nil") + +;; ---- propositional logic simplifier ---- + +(define + mrt-prop + (mau/parse-module + "fmod PROPLOGIC is\n sort Bool .\n op tt : -> Bool .\n op ff : -> Bool .\n op not_ : Bool -> Bool .\n op _and_ : Bool Bool -> Bool .\n op _or_ : Bool Bool -> Bool .\n op _xor_ : Bool Bool -> Bool .\n vars P Q : Bool .\n eq not tt = ff .\n eq not ff = tt .\n eq tt and P = P .\n eq ff and P = ff .\n eq tt or P = tt .\n eq ff or P = P .\n eq P xor ff = P .\n eq P xor tt = not P .\nendfm")) + +(mrt-check! "not-tt" (mau/reduce->str mrt-prop "not tt") "ff") +(mrt-check! "and-simpl" (mau/reduce->str mrt-prop "not (tt and ff)") "tt") +(mrt-check! "or-simpl" (mau/reduce->str mrt-prop "ff or (tt and tt)") "tt") +(mrt-check! "double-neg" (mau/reduce->str mrt-prop "not not tt") "tt") +(mrt-check! "xor-id" (mau/reduce->str mrt-prop "tt xor ff") "tt") +(mrt-check! "xor-tt" (mau/reduce->str mrt-prop "ff xor tt") "tt") +(mrt-check! + "deep" + (mau/reduce->str mrt-prop "(tt and tt) or (not not ff)") + "tt") + +;; ---- non-linear pattern (repeated variable) + no-match leaves term ---- + +(define + mrt-same + (mau/parse-module + "fmod SAME is\n sorts Elt Bool .\n op a : -> Elt .\n op b : -> Elt .\n op tt : -> Bool .\n op same : Elt Elt -> Bool .\n var X : Elt .\n eq same(X, X) = tt .\nendfm")) + +(mrt-check! "nonlinear-match" (mau/reduce->str mrt-same "same(a, a)") "tt") +(mrt-check! + "nonlinear-nomatch" + (mau/reduce->str mrt-same "same(a, b)") + "same(a, b)") +(mrt-check! "no-rule-stays" (mau/reduce->str mrt-same "b") "b") + +;; ---- low-level matching ---- + +(mrt-check! + "match-var-binds" + (= nil (mau/match (mau/var "X" "Nat") (mau/const "0") {})) + false) +(mrt-check! + "match-mismatch" + (mau/match (mau/const "0") (mau/const "1") {}) + nil) +(mrt-check! + "subst-apply" + (mau/term->str + (mau/subst-apply + (assoc {} "X" (mau/const "0")) + (mau/app "s_" (list (mau/var "X" "Nat"))))) + "s_(0)") + +(define mau-reduce-tests-run! (fn () {:failures mrt-failures :total (+ mrt-pass mrt-fail) :passed mrt-pass :failed mrt-fail})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index d559af7a..57692dba 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -68,9 +68,9 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 - [x] Tests: parse classic examples (peano nat, list of naturals). ### Phase 2 — Syntactic equational reduction -- [ ] Apply equations left-to-right until no equation matches. -- [ ] Standard pattern matching (no equational theories yet — strict syntactic match). -- [ ] Tests: peano arithmetic, list manipulation, propositional logic simplifier. +- [x] Apply equations left-to-right until no equation matches. +- [x] Standard pattern matching (no equational theories yet — strict syntactic match). +- [x] Tests: peano arithmetic, list manipulation, propositional logic simplifier. ### Phase 3 — Equational matching (assoc / comm / id) - [ ] Extend matching to handle `assoc` operators (flatten then match across permutations of subterm groups). @@ -142,5 +142,16 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 `mau/parse-term-in` can parse term strings against its op table. Overloading is recorded but NOT resolved at parse time (resolve at reduce time). +- **Phase 2 (syntactic reduction) — DONE, 91/91 total.** `lib/maude/reduce.sx`: + one-sided syntactic matching (`mau/match` — pattern vars only, non-linear + patterns checked by bound-var equality), immutable substitutions via `assoc`, + `mau/subst-apply`, top rewrite `mau/rewrite-top` (first unconditional eq whose + LHS matches; conditional eqs skipped until Phase 4), innermost normalisation + to a fixpoint `mau/normalize` (args normalised before the operator; fuel- + guarded). API: `mau/reduce` / `mau/reduce-term` / `mau/reduce->str`. Tested on + Peano (+,*), list ops (append/length/rev), a propositional simplifier, and + non-linear `same(X,X)`. Innermost is fine for confluent terminating eq sets; + Phase 3 will replace the matcher with AC-aware matching (multi-valued). + ## Blockers _(none)_ From 2378056cb3673ea8f3a8a2d4096c0c634a9bd0ca Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 15:01:07 +0000 Subject: [PATCH 03/17] =?UTF-8?q?maude:=20Phase=203=20=E2=80=94=20equation?= =?UTF-8?q?al=20matching=20modulo=20assoc/comm/id=20(28=20tests,=20119=20t?= =?UTF-8?q?otal)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The chisel. lib/maude/matching.sx: multi-valued matcher mau/mm returning ALL substitutions, dispatching on op theory (free/comm/assoc/AC). Identity lets variables grab empty blocks. AC-canonical form (mau/canon) powers ac-equal? and deterministic printout. AC rewriting extends f-AC equations with rest vars so a rule fires on any sub-multiset/subword; mau/first-change only commits rewrites that change the canonical form (idempotency/identity terminate). Verified on multiset rewriting, set theory, group equations. Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/maude/conformance.conf | 2 + lib/maude/matching.sx | 565 ++++++++++++++++++++++++++++++++++++ lib/maude/scoreboard.json | 9 +- lib/maude/scoreboard.md | 3 +- lib/maude/tests/matching.sx | 170 +++++++++++ plans/maude-on-sx.md | 36 ++- 6 files changed, 774 insertions(+), 11 deletions(-) create mode 100644 lib/maude/matching.sx create mode 100644 lib/maude/tests/matching.sx diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf index af3f75da..5655e386 100644 --- a/lib/maude/conformance.conf +++ b/lib/maude/conformance.conf @@ -9,9 +9,11 @@ PRELOADS=( lib/maude/term.sx lib/maude/parser.sx lib/maude/reduce.sx + lib/maude/matching.sx ) SUITES=( "parse:lib/maude/tests/parse.sx:(mau-parse-tests-run!)" "reduce:lib/maude/tests/reduce.sx:(mau-reduce-tests-run!)" + "matching:lib/maude/tests/matching.sx:(mau-matching-tests-run!)" ) diff --git a/lib/maude/matching.sx b/lib/maude/matching.sx new file mode 100644 index 00000000..e43239dd --- /dev/null +++ b/lib/maude/matching.sx @@ -0,0 +1,565 @@ +;; lib/maude/matching.sx — equational matching modulo assoc/comm/id (Phase 3). +;; +;; The chisel. Syntactic matching (reduce.sx) returns at most one substitution; +;; matching modulo a theory is MULTI-VALUED — `X + Y` against `a + b + c` (with +;; _+_ assoc comm) has several solutions. `mau/mm` returns the full list of +;; substitutions; callers (rule application) pick. +;; +;; Operator theories come from the signature attributes, collected into a dict +;; OP-NAME -> {:assoc B :comm B :id ELT}. Matching dispatches on the head op's +;; theory: +;; free positional, exact arity +;; comm binary, try both argument orderings +;; assoc flatten the f-spine, match the pattern sequence against the +;; subject sequence (variables grab contiguous blocks) +;; assoc+comm flatten, match as multisets (variables grab sub-multisets) +;; Identity (id: e) lets a variable grab the empty block, contributing e. +;; +;; Equational rewriting (mau/ac-reduce) extends each f-AC equation l=r to +;; f(REST..., l) -> f(REST..., r) so a rule fires on any sub-multiset of an +;; AC term, then renormalises to a fixpoint. A candidate rewrite is taken only +;; if it changes the AC-canonical form (mau/canon) — idempotency/identity +;; matches that would re-fire forever are skipped, guaranteeing progress. + +;; ---------- theory table ---------- + +(define + mau/build-theory + (fn + (m) + (let + ((th {})) + (for-each + (fn + (op) + (let + ((a (get op :attrs))) + (dict-set! th (get op :name) {:id (get a :id) :assoc (= (get a :assoc) true) :comm (= (get a :comm) true)}))) + (mau/module-ops m)) + th))) + +(define + mau/th-of + (fn + (theory op) + (let ((e (get theory op))) (if (= e nil) {:id nil :assoc false :comm false} e)))) + +;; ---------- small list utilities ---------- + +(define + mau/concat-map + (fn + (f xs) + (if + (empty? xs) + (list) + (mau/append2 (f (first xs)) (mau/concat-map f (rest xs)))))) + +(define + mau/remove-at + (fn (xs i) (mau/append2 (mau/take xs i) (mau/drop xs (+ i 1))))) + +;; All (chosen complement) pairs over every subset of xs. +(define + mau/all-splits + (fn + (xs) + (if + (empty? xs) + (list (list (list) (list))) + (let + ((subsplits (mau/all-splits (rest xs))) (x (first xs))) + (mau/concat-map + (fn + (pair) + (let + ((c (first pair)) (r (nth pair 1))) + (list (list (cons x c) r) (list c (cons x r))))) + subsplits))))) + +;; ---------- flattening of associative spines ---------- + +(define + mau/flatten-op + (fn + (theory f term) + (if + (and (mau/app? term) (= (mau/op term) f)) + (mau/flatten-op-list theory f (mau/args term)) + (list term)))) + +(define + mau/flatten-op-list + (fn + (theory f args) + (if + (empty? args) + (list) + (mau/append2 + (mau/flatten-op theory f (first args)) + (mau/flatten-op-list theory f (rest args)))))) + +(define + mau/foldr-app + (fn + (f block) + (if + (empty? (rest block)) + (first block) + (mau/app f (list (first block) (mau/foldr-app f (rest block))))))) + +(define + mau/rebuild + (fn + (f block id) + (cond + ((empty? block) (if (= id nil) (mau/const "$EMPTY") (mau/const id))) + ((empty? (rest block)) (first block)) + (else (mau/foldr-app f block))))) + +(define mau/ac-build (fn (theory f els id) (mau/rebuild f els id))) + +;; ---------- AC-canonical form / equality ---------- + +(define + mau/insert-str + (fn + (x ys) + (cond + ((empty? ys) (list x)) + ((<= x (first ys)) (cons x ys)) + (else (cons (first ys) (mau/insert-str x (rest ys))))))) + +(define + mau/sort-strings + (fn + (xs) + (if + (empty? xs) + xs + (mau/insert-str (first xs) (mau/sort-strings (rest xs)))))) + +(define + mau/drop-identity + (fn + (theory f els id) + (if + (= id nil) + els + (let + ((idc (mau/canon theory (mau/const id)))) + (filter (fn (e) (not (= (mau/canon theory e) idc))) els))))) + +(define + mau/canon + (fn + (theory term) + (cond + ((mau/var? term) (str "?" (mau/vname term))) + ((mau/const? term) (mau/op term)) + ((mau/app? term) + (let + ((f (mau/op term)) (th (mau/th-of theory (mau/op term)))) + (if + (get th :assoc) + (let + ((els (mau/drop-identity theory f (mau/flatten-op theory f term) (get th :id)))) + (cond + ((empty? els) + (if (= (get th :id) nil) "$EMPTY" (get th :id))) + ((empty? (rest els)) (mau/canon theory (first els))) + (else + (let + ((cs (map (fn (e) (mau/canon theory e)) els))) + (let + ((cs2 (if (get th :comm) (mau/sort-strings cs) cs))) + (str f "(" (join "," cs2) ")")))))) + (if + (get th :comm) + (str + f + "(" + (join + "," + (mau/sort-strings + (map (fn (e) (mau/canon theory e)) (mau/args term)))) + ")") + (str + f + "(" + (join + "," + (map (fn (e) (mau/canon theory e)) (mau/args term))) + ")"))))) + (else (str term))))) + +(define + mau/ac-equal? + (fn (theory a b) (= (mau/canon theory a) (mau/canon theory b)))) + +;; ---------- variable block bounds ---------- + +(define + mau/rest-var? + (fn + (name) + (and + (> (len name) 0) + (= (slice name 0 1) "$")))) + +(define + mau/var-kmin + (fn + (name id) + (if (or (mau/rest-var? name) (not (= id nil))) 0 1))) + +(define + mau/bind-check + (fn + (theory s name val) + (let + ((b (get s name))) + (if + (= b nil) + (assoc s name val) + (if (mau/ac-equal? theory b val) s nil))))) + +;; ---------- core multi-valued matcher ---------- + +(define + mau/mm + (fn + (theory pat subj s) + (cond + ((mau/var? pat) + (let + ((bound (get s (mau/vname pat)))) + (if + (= bound nil) + (list (assoc s (mau/vname pat) subj)) + (if (mau/ac-equal? theory bound subj) (list s) (list))))) + ((mau/app? pat) + (if (mau/app? subj) (mau/mm-app theory pat subj s) (list))) + (else (list))))) + +(define + mau/extend-all + (fn + (theory p subj substs) + (mau/concat-map (fn (s) (mau/mm theory p subj s)) substs))) + +(define + mau/mm-args + (fn + (theory ps ss substs) + (cond + ((and (empty? ps) (empty? ss)) substs) + ((or (empty? ps) (empty? ss)) (list)) + (else + (mau/mm-args + theory + (rest ps) + (rest ss) + (mau/extend-all theory (first ps) (first ss) substs)))))) + +(define + mau/mm-comm + (fn + (theory pat subj s) + (let + ((p1 (nth (mau/args pat) 0)) + (p2 (nth (mau/args pat) 1)) + (q1 (nth (mau/args subj) 0)) + (q2 (nth (mau/args subj) 1))) + (mau/append2 + (mau/mm-args theory (list p1 p2) (list q1 q2) (list s)) + (mau/mm-args theory (list p1 p2) (list q2 q1) (list s)))))) + +(define + mau/mm-assoc + (fn + (theory f pat subj s) + (let + ((pels (mau/flatten-op theory f pat)) + (sels (mau/flatten-op theory f subj)) + (th (mau/th-of theory f))) + (if + (get th :comm) + (mau/match-multiset theory f pels sels s (get th :id)) + (mau/match-sequence theory f pels sels s (get th :id)))))) + +(define + mau/mm-app + (fn + (theory pat subj s) + (let + ((f (mau/op pat)) + (g (mau/op subj)) + (th (mau/th-of theory (mau/op pat)))) + (cond + ((get th :assoc) (mau/mm-assoc theory f pat subj s)) + ((get th :comm) + (if + (and + (= f g) + (= (mau/arity pat) 2) + (= (mau/arity subj) 2)) + (mau/mm-comm theory pat subj s) + (list))) + (else + (if + (and (= f g) (= (mau/arity pat) (mau/arity subj))) + (mau/mm-args theory (mau/args pat) (mau/args subj) (list s)) + (list))))))) + +;; ---------- associative (ordered) sequence matching ---------- + +(define + mau/match-sequence + (fn + (theory f pels sels s id) + (cond + ((empty? pels) (if (empty? sels) (list s) (list))) + (else + (let + ((p (first pels)) (prest (rest pels))) + (if + (mau/var? p) + (mau/seq-var-loop + theory + f + prest + sels + s + (mau/vname p) + id + (mau/var-kmin (mau/vname p) id)) + (if + (empty? sels) + (list) + (mau/concat-map + (fn + (s2) + (mau/match-sequence theory f prest (rest sels) s2 id)) + (mau/mm theory p (first sels) s))))))))) + +(define + mau/seq-var-loop + (fn + (theory f prest sels s name id k) + (if + (> k (len sels)) + (list) + (let + ((block (mau/take sels k)) (rests (mau/drop sels k))) + (let + ((val (mau/rebuild f block id))) + (let + ((s2 (mau/bind-check theory s name val))) + (mau/append2 + (if + (= s2 nil) + (list) + (mau/match-sequence theory f prest rests s2 id)) + (mau/seq-var-loop + theory + f + prest + sels + s + name + id + (+ k 1))))))))) + +;; ---------- associative-commutative (multiset) matching ---------- + +(define + mau/match-multiset + (fn + (theory f pels sels s id) + (cond + ((empty? pels) (if (empty? sels) (list s) (list))) + (else + (let + ((p (first pels)) (prest (rest pels))) + (if + (mau/var? p) + (mau/ms-var-splits theory f prest sels s (mau/vname p) id) + (mau/ms-nonvar-loop theory f p prest sels s id 0))))))) + +(define + mau/ms-nonvar-loop + (fn + (theory f p prest sels s id i) + (if + (>= i (len sels)) + (list) + (let + ((elem (nth sels i)) (others (mau/remove-at sels i))) + (mau/append2 + (mau/concat-map + (fn (s2) (mau/match-multiset theory f prest others s2 id)) + (mau/mm theory p elem s)) + (mau/ms-nonvar-loop theory f p prest sels s id (+ i 1))))))) + +(define + mau/ms-var-splits + (fn + (theory f prest sels s name id) + (let + ((kmin (mau/var-kmin name id))) + (mau/concat-map + (fn + (pair) + (let + ((chosen (first pair)) (rests (nth pair 1))) + (if + (< (len chosen) kmin) + (list) + (let + ((val (mau/rebuild f chosen id))) + (let + ((s2 (mau/bind-check theory s name val))) + (if + (= s2 nil) + (list) + (mau/match-multiset theory f prest rests s2 id))))))) + (mau/all-splits sels))))) + +;; ---------- public matching entry ---------- + +(define + mau/match-all + (fn (m pat subj) (mau/mm (mau/build-theory m) pat subj {}))) + +;; ---------- AC-aware equational rewriting ---------- + +(define + mau/restv + (fn + (theory f s name) + (let + ((v (get s name))) + (cond + ((= v nil) (list)) + ((and (mau/app? v) (= (mau/op v) "$EMPTY")) (list)) + (else (mau/flatten-op theory f v)))))) + +(define + mau/ac-eq-result + (fn + (theory f th eq s) + (if + (get th :comm) + (mau/ac-build + theory + f + (mau/append2 + (mau/flatten-op theory f (mau/subst-apply s (get eq :rhs))) + (mau/restv theory f s "$R")) + (get th :id)) + (mau/ac-build + theory + f + (mau/append2 + (mau/restv theory f s "$L") + (mau/append2 + (mau/flatten-op theory f (mau/subst-apply s (get eq :rhs))) + (mau/restv theory f s "$R"))) + (get th :id))))) + +;; Walk the candidate matches and return the first rewrite that actually +;; changes the term's canonical form (skips idempotency/identity no-ops). +(define + mau/first-change + (fn + (theory f th eq term matches) + (if + (empty? matches) + nil + (let + ((result (mau/ac-eq-result theory f th eq (first matches)))) + (if + (mau/ac-equal? theory result term) + (mau/first-change theory f th eq term (rest matches)) + result))))) + +(define + mau/ac-rewrite-eq + (fn + (theory f th eq term) + (let + ((id (get th :id)) + (pels (mau/flatten-op theory f (get eq :lhs))) + (sels (mau/flatten-op theory f term))) + (let + ((matches (if (get th :comm) (mau/match-multiset theory f (mau/append2 pels (list (mau/var "$R" ""))) sels {} id) (mau/match-sequence theory f (mau/append2 (list (mau/var "$L" "")) (mau/append2 pels (list (mau/var "$R" "")))) sels {} id)))) + (mau/first-change theory f th eq term matches))))) + +(define + mau/ac-rewrite-top + (fn + (theory eqs term) + (cond + ((empty? eqs) nil) + (else + (let + ((eq (first eqs))) + (if + (= (get eq :cond) nil) + (let + ((lhs (get eq :lhs))) + (let + ((th (if (mau/app? lhs) (mau/th-of theory (mau/op lhs)) {:id nil :assoc false :comm false}))) + (let + ((r (if (and (mau/app? lhs) (get th :assoc)) (mau/ac-rewrite-eq theory (mau/op lhs) th eq term) (let ((ss (mau/mm theory lhs term {}))) (if (empty? ss) nil (mau/subst-apply (first ss) (get eq :rhs))))))) + (cond + ((= r nil) (mau/ac-rewrite-top theory (rest eqs) term)) + ((mau/ac-equal? theory r term) + (mau/ac-rewrite-top theory (rest eqs) term)) + (else r))))) + (mau/ac-rewrite-top theory (rest eqs) term))))))) + +(define + mau/ac-normalize + (fn + (theory eqs term fuel) + (if + (<= fuel 0) + term + (cond + ((mau/var? term) term) + ((mau/app? term) + (let + ((nargs (map (fn (a) (mau/ac-normalize theory eqs a fuel)) (mau/args term)))) + (let + ((t2 (mau/app (mau/op term) nargs))) + (let + ((r (mau/ac-rewrite-top theory eqs t2))) + (if + (= r nil) + t2 + (mau/ac-normalize theory eqs r (- fuel 1))))))) + (else term))))) + +(define + mau/ac-reduce + (fn + (m term) + (mau/ac-normalize + (mau/build-theory m) + (mau/module-eqs m) + term + mau/reduce-fuel))) + +(define + mau/ac-reduce-term + (fn (m src) (mau/ac-reduce m (mau/parse-term-in m src)))) + +(define + mau/ac-reduce->str + (fn (m src) (mau/term->str (mau/ac-reduce-term m src)))) + +(define + mau/ac-canon + (fn (m src) (mau/canon (mau/build-theory m) (mau/ac-reduce-term m src)))) diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json index e9ea5da0..2eec89ae 100644 --- a/lib/maude/scoreboard.json +++ b/lib/maude/scoreboard.json @@ -1,11 +1,12 @@ { "lang": "maude", - "total_passed": 91, + "total_passed": 119, "total_failed": 0, - "total": 91, + "total": 119, "suites": [ {"name":"parse","passed":65,"failed":0,"total":65}, - {"name":"reduce","passed":26,"failed":0,"total":26} + {"name":"reduce","passed":26,"failed":0,"total":26}, + {"name":"matching","passed":28,"failed":0,"total":28} ], - "generated": "2026-06-07T14:45:37+00:00" + "generated": "2026-06-07T15:00:34+00:00" } diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md index 3d9e113e..690c1cab 100644 --- a/lib/maude/scoreboard.md +++ b/lib/maude/scoreboard.md @@ -1,8 +1,9 @@ # maude scoreboard -**91 / 91 passing** (0 failure(s)). +**119 / 119 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| | parse | 65 | 65 | ok | | reduce | 26 | 26 | ok | +| matching | 28 | 28 | ok | diff --git a/lib/maude/tests/matching.sx b/lib/maude/tests/matching.sx new file mode 100644 index 00000000..745f8b61 --- /dev/null +++ b/lib/maude/tests/matching.sx @@ -0,0 +1,170 @@ +;; lib/maude/tests/matching.sx — Phase 3: matching modulo assoc/comm/id. + +(define mmt-pass 0) +(define mmt-fail 0) +(define mmt-failures (list)) + +(define + mmt-check! + (fn + (name got expected) + (if + (= got expected) + (set! mmt-pass (+ mmt-pass 1)) + (do + (set! mmt-fail (+ mmt-fail 1)) + (append! + mmt-failures + (str name " expected: " expected " got: " got)))))) + +;; ---- multi-valued matching enumeration ---- + +(define + mmt-acg + (mau/parse-module + "fmod ACG is\n sort S .\n op a : -> S .\n op b : -> S .\n op c : -> S .\n op _+_ : S S -> S [assoc comm] .\n op _._ : S S -> S [assoc] .\n vars X Y : S .\nendfm")) + +;; X + Y against a + b + c (AC, no id): 6 solutions (each non-empty 2-split). +(mmt-check! + "ac-match-count" + (len + (mau/match-all + mmt-acg + (mau/parse-term-in mmt-acg "X + Y") + (mau/parse-term-in mmt-acg "a + b + c"))) + 6) +;; X + a against a + b + c: X must be b + c (one solution, multiset). +(mmt-check! + "ac-match-partial" + (len + (mau/match-all + mmt-acg + (mau/parse-term-in mmt-acg "X + a") + (mau/parse-term-in mmt-acg "a + b + c"))) + 1) +;; assoc-only X . Y against a . b . c: ordered 2-splits -> 2 solutions. +(mmt-check! + "assoc-match-count" + (len + (mau/match-all + mmt-acg + (mau/parse-term-in mmt-acg "X . Y") + (mau/parse-term-in mmt-acg "a . b . c"))) + 2) +;; no match: a + a pattern against a + b +(mmt-check! + "ac-no-match" + (len + (mau/match-all + mmt-acg + (mau/parse-term-in mmt-acg "a + a") + (mau/parse-term-in mmt-acg "a + b"))) + 0) + +;; ---- comm (non-assoc) matching ---- + +(define + mmt-pair + (mau/parse-module + "fmod PAIR is\n sort S .\n op a : -> S .\n op b : -> S .\n op p : S S -> S [comm] .\n op fst : S -> S .\n vars X Y : S .\n eq fst(p(X, a)) = X .\nendfm")) + +(mmt-check! + "comm-both-orders" + (mau/ac-reduce->str mmt-pair "fst(p(b, a))") + "b") +(mmt-check! "comm-swapped" (mau/ac-reduce->str mmt-pair "fst(p(a, b))") "b") + +;; ---- identity ---- + +(define + mmt-id + (mau/parse-module + "fmod IDMOD is\n sort S .\n op a : -> S .\n op b : -> S .\n op e : -> S .\n op _*_ : S S -> S [assoc comm id: e] .\n vars X Y : S .\nendfm")) + +(mmt-check! "id-drop" (mau/ac-canon mmt-id "a * e") "a") +(mmt-check! "id-drop-mid" (mau/ac-canon mmt-id "a * e * b") "_*_(a,b)") +(mmt-check! "id-only" (mau/ac-canon mmt-id "e * e") "e") +;; with id, X * Y matching a (singleton) succeeds (one var empty) +(mmt-check! + "id-match-singleton" + (> + (len + (mau/match-all + mmt-id + (mau/parse-term-in mmt-id "X * Y") + (mau/parse-term-in mmt-id "a"))) + 0) + true) + +;; ---- multiset / bag rewriting ---- + +(define + mmt-bag + (mau/parse-module + "fmod BAG is\n sort S .\n op a : -> S .\n op b : -> S .\n op c : -> S .\n op _+_ : S S -> S [assoc comm] .\n eq a + a = a .\nendfm")) + +(mmt-check! "bag-collapse" (mau/ac-canon mmt-bag "a + b + a") "_+_(a,b)") +(mmt-check! "bag-deep" (mau/ac-canon mmt-bag "a + a + a") "a") +(mmt-check! "bag-reorder" (mau/ac-canon mmt-bag "c + a + b + a") "_+_(a,b,c)") +(mmt-check! + "bag-flatten-assoc" + (mau/ac-canon mmt-bag "(a + b) + (a + c)") + "_+_(a,b,c)") + +;; ---- set theory: idempotent union with empty (identity) ---- + +(define + mmt-set + (mau/parse-module + "fmod SET is\n sort Set .\n op empty : -> Set .\n op a : -> Set .\n op b : -> Set .\n op c : -> Set .\n op _U_ : Set Set -> Set [assoc comm id: empty] .\n var X : Set .\n eq X U X = X .\nendfm")) + +(mmt-check! "set-dedup" (mau/ac-canon mmt-set "a U b U a") "_U_(a,b)") +(mmt-check! "set-triple" (mau/ac-canon mmt-set "a U a U a") "a") +(mmt-check! + "set-union" + (mau/ac-canon mmt-set "a U b U c U a U b") + "_U_(a,b,c)") +(mmt-check! "set-empty" (mau/ac-canon mmt-set "a U empty") "a") +(mmt-check! "set-empty-only" (mau/ac-canon mmt-set "empty U empty") "empty") + +;; ---- group equations (assoc, non-comm, identity + inverse) ---- + +(define + mmt-group + (mau/parse-module + "fmod GROUP is\n sort G .\n op e : -> G .\n op a : -> G .\n op b : -> G .\n op _*_ : G G -> G [assoc] .\n op i : G -> G .\n var X : G .\n eq e * X = X .\n eq X * e = X .\n eq i(X) * X = e .\n eq X * i(X) = e .\n eq i(e) = e .\n eq i(i(X)) = X .\nendfm")) + +(mmt-check! "group-inverse" (mau/ac-canon mmt-group "i(a) * a") "e") +(mmt-check! "group-cancel" (mau/ac-canon mmt-group "i(a) * a * b") "b") +(mmt-check! "group-cancel-mid" (mau/ac-canon mmt-group "b * i(a) * a") "b") +(mmt-check! "group-double-inv" (mau/ac-canon mmt-group "i(i(a))") "a") +(mmt-check! "group-id-left" (mau/ac-canon mmt-group "e * a") "a") +(mmt-check! "group-right-inv" (mau/ac-canon mmt-group "a * i(a) * b") "b") + +;; ---- AC equality (canonical form) ---- + +(define mmt-th (mau/build-theory mmt-acg)) + +(mmt-check! + "ac-equal-reorder" + (mau/ac-equal? + mmt-th + (mau/parse-term-in mmt-acg "a + b + c") + (mau/parse-term-in mmt-acg "c + a + b")) + true) +(mmt-check! + "ac-equal-renest" + (mau/ac-equal? + mmt-th + (mau/parse-term-in mmt-acg "(a + b) + c") + (mau/parse-term-in mmt-acg "a + (b + c)")) + true) +(mmt-check! + "ac-noncomm-order" + (mau/ac-equal? + mmt-th + (mau/parse-term-in mmt-acg "a . b") + (mau/parse-term-in mmt-acg "b . a")) + false) + +(define mau-matching-tests-run! (fn () {:failures mmt-failures :total (+ mmt-pass mmt-fail) :passed mmt-pass :failed mmt-fail})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index 57692dba..87e3b4d3 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -73,12 +73,12 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 - [x] Tests: peano arithmetic, list manipulation, propositional logic simplifier. ### Phase 3 — Equational matching (assoc / comm / id) -- [ ] Extend matching to handle `assoc` operators (flatten then match across permutations of subterm groups). -- [ ] Handle `comm` (try both argument orderings). -- [ ] Handle `id: e` (X * e ≡ X). -- [ ] Combinations: `assoc comm id` together. -- [ ] Returns *all* matches, not just first — caller drives. -- [ ] Tests: classic AC-matching examples (multiset rewriting, set theory, group equations). +- [x] Extend matching to handle `assoc` operators (flatten then match across permutations of subterm groups). +- [x] Handle `comm` (try both argument orderings). +- [x] Handle `id: e` (X * e ≡ X). +- [x] Combinations: `assoc comm id` together. +- [x] Returns *all* matches, not just first — caller drives. +- [x] Tests: classic AC-matching examples (multiset rewriting, set theory, group equations). ### Phase 4 — Conditional equations - [ ] `ceq L = R if Cond` — apply only when `Cond` reduces to true. @@ -153,5 +153,29 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 non-linear `same(X,X)`. Innermost is fine for confluent terminating eq sets; Phase 3 will replace the matcher with AC-aware matching (multi-valued). +- **Phase 3 (matching modulo assoc/comm/id) — DONE, 119/119 total. THE CHISEL.** + `lib/maude/matching.sx`. `mau/mm` is the multi-valued matcher (returns the + full list of substitutions): free=positional, comm=both orderings, + assoc=flatten f-spine + ordered sequence match (vars grab contiguous blocks), + assoc+comm=multiset match (vars grab sub-multisets via `mau/all-splits` = + 2^n subset/complement pairs). `id: e` lets a var grab the empty block + (contributing e); `mau/var-kmin` gives kmin 0 under id. `mau/canon` is the + AC-canonical printout (flatten, drop identities, sort comm args) and powers + `mau/ac-equal?` (used for bound-var checks too). AC *rewriting* extends each + f-AC equation l=r with rest vars — comm: `f(l,$R)`; assoc: `f($L,l,$R)` — + so a rule fires on any sub-multiset/subword (`$`-prefixed rest vars allowed + empty). `mau/first-change` walks candidate matches and only commits a rewrite + that changes the canonical form — this is what makes idempotency (`X U X = X`) + and identity-absorbing matches terminate. API: `mau/ac-reduce` / + `mau/ac-reduce->str` / `mau/ac-canon` / `mau/match-all`. Verified: AC match + counts (X+Y vs a+b+c = 6), bag collapse, set dedup with empty, group + cancellation (assoc non-comm + inverse). + - Notes for next phases: AC matching is multi-valued — Phase 5 rule + application should iterate ALL of `mau/mm`'s results, not just first. The + `mau/ac-rewrite-eq` extension trick (rest vars) is the reusable core for + a future `lib/guest/rewriting/` (Phase 8). Keep `mau/canon` as the equality + oracle. `$EMPTY` is a transient marker for empty rest blocks w/o id; never + leaks past `mau/restv`. + ## Blockers _(none)_ From 1747bbd9442616234ba8209b1cdded845bb96787 Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 15:06:00 +0000 Subject: [PATCH 04/17] maude: Phase 4 conditional equations (19 tests, 138 total) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit lib/maude/conditional.sx — condition-aware reducer. ceq fires only when its guard holds: equational guards (l=r reduce to same normal form) and boolean guards (term reduces to true), evaluated by recursing through the same reducer. Verified on gcd, insertion sort, max, even. Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/maude/conditional.sx | 144 +++++++++++++++++++++++++++++++++ lib/maude/conformance.conf | 2 + lib/maude/scoreboard.json | 9 ++- lib/maude/scoreboard.md | 3 +- lib/maude/tests/conditional.sx | 108 +++++++++++++++++++++++++ plans/maude-on-sx.md | 24 +++++- 6 files changed, 282 insertions(+), 8 deletions(-) create mode 100644 lib/maude/conditional.sx create mode 100644 lib/maude/tests/conditional.sx diff --git a/lib/maude/conditional.sx b/lib/maude/conditional.sx new file mode 100644 index 00000000..00ea6aa2 --- /dev/null +++ b/lib/maude/conditional.sx @@ -0,0 +1,144 @@ +;; lib/maude/conditional.sx — conditional equations (Phase 4). +;; +;; A condition-aware superset of the Phase 3 reducer. `ceq L = R if COND` fires +;; only when COND holds under the matching substitution. Conditions come from +;; the parser as: +;; {:kind :eq :lhs L :rhs R} — holds iff reduce(s L) =AC= reduce(s R) +;; {:kind :bool :term T} — holds iff reduce(s T) =AC= true +;; Condition evaluation recurses through the SAME reducer (mau/cnormalize), so +;; a ceq whose guard mentions other (possibly conditional) equations Just Works +;; — termination rests on the guard reducing on structurally smaller arguments +;; (and the global fuel guard). +;; +;; This engine subsumes mau/ac-reduce: an unconditional equation has cond nil, +;; which always holds. Phases 5+ build on the c-* entry points. + +(define + mau/ac-candidates + (fn + (theory f th eq term) + (let + ((id (get th :id)) + (pels (mau/flatten-op theory f (get eq :lhs))) + (sels (mau/flatten-op theory f term))) + (let + ((matches (if (get th :comm) (mau/match-multiset theory f (mau/append2 pels (list (mau/var "$R" ""))) sels {} id) (mau/match-sequence theory f (mau/append2 (list (mau/var "$L" "")) (mau/append2 pels (list (mau/var "$R" "")))) sels {} id)))) + (map (fn (s) {:s s :result (mau/ac-eq-result theory f th eq s)}) matches))))) + +(define + mau/eq-candidates + (fn + (theory eq term) + (let + ((lhs (get eq :lhs))) + (let + ((th (if (mau/app? lhs) (mau/th-of theory (mau/op lhs)) {:id nil :assoc false :comm false}))) + (if + (and (mau/app? lhs) (get th :assoc)) + (mau/ac-candidates theory (mau/op lhs) th eq term) + (map (fn (s) {:s s :result (mau/subst-apply s (get eq :rhs))}) (mau/mm theory lhs term {}))))))) + +(define + mau/cond-holds? + (fn + (theory eqs cond s) + (if + (= cond nil) + true + (if + (= (get cond :kind) "eq") + (mau/ac-equal? + theory + (mau/cnormalize + theory + eqs + (mau/subst-apply s (get cond :lhs)) + mau/reduce-fuel) + (mau/cnormalize + theory + eqs + (mau/subst-apply s (get cond :rhs)) + mau/reduce-fuel)) + (mau/ac-equal? + theory + (mau/cnormalize + theory + eqs + (mau/subst-apply s (get cond :term)) + mau/reduce-fuel) + (mau/const "true")))))) + +(define + mau/try-candidates + (fn + (theory all-eqs cond term cands) + (if + (empty? cands) + nil + (let + ((c (first cands))) + (if + (and + (not (mau/ac-equal? theory (get c :result) term)) + (mau/cond-holds? theory all-eqs cond (get c :s))) + (get c :result) + (mau/try-candidates theory all-eqs cond term (rest cands))))))) + +(define + mau/crewrite-loop + (fn + (theory all-eqs eqs term) + (if + (empty? eqs) + nil + (let + ((r (mau/try-candidates theory all-eqs (get (first eqs) :cond) term (mau/eq-candidates theory (first eqs) term)))) + (if (= r nil) (mau/crewrite-loop theory all-eqs (rest eqs) term) r))))) + +(define + mau/crewrite-top + (fn (theory eqs term) (mau/crewrite-loop theory eqs eqs term))) + +(define + mau/cnormalize + (fn + (theory eqs term fuel) + (if + (<= fuel 0) + term + (cond + ((mau/var? term) term) + ((mau/app? term) + (let + ((nargs (map (fn (a) (mau/cnormalize theory eqs a fuel)) (mau/args term)))) + (let + ((t2 (mau/app (mau/op term) nargs))) + (let + ((r (mau/crewrite-top theory eqs t2))) + (if + (= r nil) + t2 + (mau/cnormalize theory eqs r (- fuel 1))))))) + (else term))))) + +(define + mau/creduce + (fn + (m term) + (mau/cnormalize + (mau/build-theory m) + (mau/module-eqs m) + term + mau/reduce-fuel))) + +(define + mau/creduce-term + (fn (m src) (mau/creduce m (mau/parse-term-in m src)))) + +(define + mau/creduce->str + (fn (m src) (mau/term->str (mau/creduce-term m src)))) + +(define + mau/ccanon + (fn (m src) (mau/canon (mau/build-theory m) (mau/creduce-term m src)))) diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf index 5655e386..2e986227 100644 --- a/lib/maude/conformance.conf +++ b/lib/maude/conformance.conf @@ -10,10 +10,12 @@ PRELOADS=( lib/maude/parser.sx lib/maude/reduce.sx lib/maude/matching.sx + lib/maude/conditional.sx ) SUITES=( "parse:lib/maude/tests/parse.sx:(mau-parse-tests-run!)" "reduce:lib/maude/tests/reduce.sx:(mau-reduce-tests-run!)" "matching:lib/maude/tests/matching.sx:(mau-matching-tests-run!)" + "conditional:lib/maude/tests/conditional.sx:(mau-conditional-tests-run!)" ) diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json index 2eec89ae..5e552292 100644 --- a/lib/maude/scoreboard.json +++ b/lib/maude/scoreboard.json @@ -1,12 +1,13 @@ { "lang": "maude", - "total_passed": 119, + "total_passed": 138, "total_failed": 0, - "total": 119, + "total": 138, "suites": [ {"name":"parse","passed":65,"failed":0,"total":65}, {"name":"reduce","passed":26,"failed":0,"total":26}, - {"name":"matching","passed":28,"failed":0,"total":28} + {"name":"matching","passed":28,"failed":0,"total":28}, + {"name":"conditional","passed":19,"failed":0,"total":19} ], - "generated": "2026-06-07T15:00:34+00:00" + "generated": "2026-06-07T15:05:31+00:00" } diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md index 690c1cab..12cd28a2 100644 --- a/lib/maude/scoreboard.md +++ b/lib/maude/scoreboard.md @@ -1,9 +1,10 @@ # maude scoreboard -**119 / 119 passing** (0 failure(s)). +**138 / 138 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| | parse | 65 | 65 | ok | | reduce | 26 | 26 | ok | | matching | 28 | 28 | ok | +| conditional | 19 | 19 | ok | diff --git a/lib/maude/tests/conditional.sx b/lib/maude/tests/conditional.sx new file mode 100644 index 00000000..c1599a61 --- /dev/null +++ b/lib/maude/tests/conditional.sx @@ -0,0 +1,108 @@ +;; lib/maude/tests/conditional.sx — Phase 4: conditional equations. + +(define mct-pass 0) +(define mct-fail 0) +(define mct-failures (list)) + +(define + mct-check! + (fn + (name got expected) + (if + (= got expected) + (set! mct-pass (+ mct-pass 1)) + (do + (set! mct-fail (+ mct-fail 1)) + (append! + mct-failures + (str name " expected: " expected " got: " got)))))) + +;; ---- gcd (equational guard, recursive) ---- + +(define + mct-gcd + (mau/parse-module + "fmod GCD is\n sorts Nat Bool .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op true : -> Bool .\n op false : -> Bool .\n op _>_ : Nat Nat -> Bool .\n op _-_ : Nat Nat -> Nat .\n op gcd : Nat Nat -> Nat .\n vars X Y : Nat .\n eq 0 > Y = false .\n eq s X > 0 = true .\n eq s X > s Y = X > Y .\n eq X - 0 = X .\n eq 0 - Y = 0 .\n eq s X - s Y = X - Y .\n eq gcd(X, 0) = X .\n eq gcd(0, Y) = Y .\n eq gcd(X, X) = X .\n ceq gcd(X, Y) = gcd(X - Y, Y) if X > Y = true .\n ceq gcd(X, Y) = gcd(Y, X) if Y > X = true .\nendfm")) + +(mct-check! + "gcd-6-4" + (mau/creduce->str mct-gcd "gcd(s s s s s s 0, s s s s 0)") + "s_(s_(0))") +(mct-check! + "gcd-3-6" + (mau/creduce->str mct-gcd "gcd(s s s 0, s s s s s s 0)") + "s_(s_(s_(0)))") +(mct-check! + "gcd-base-zero" + (mau/creduce->str mct-gcd "gcd(s s 0, 0)") + "s_(s_(0))") +(mct-check! + "gcd-equal" + (mau/creduce->str mct-gcd "gcd(s s 0, s s 0)") + "s_(s_(0))") +(mct-check! + "gcd-coprime" + (mau/creduce->str mct-gcd "gcd(s s s 0, s s 0)") + "s_(0)") +;; guard predicate reductions +(mct-check! "gt-true" (mau/creduce->str mct-gcd "s s 0 > s 0") "true") +(mct-check! "gt-false" (mau/creduce->str mct-gcd "s 0 > s s 0") "false") + +;; ---- insertion sort (true/false guards) ---- + +(define + mct-sort + (mau/parse-module + "fmod SORT is\n sorts Nat List Bool .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op true : -> Bool .\n op false : -> Bool .\n op _<=_ : Nat Nat -> Bool .\n op nil : -> List .\n op _:_ : Nat List -> List .\n op insert : Nat List -> List .\n op sort : List -> List .\n vars M N : Nat .\n var L : List .\n eq 0 <= N = true .\n eq s M <= 0 = false .\n eq s M <= s N = M <= N .\n eq insert(N, nil) = N : nil .\n ceq insert(N, M : L) = N : (M : L) if N <= M = true .\n ceq insert(N, M : L) = M : insert(N, L) if N <= M = false .\n eq sort(nil) = nil .\n eq sort(N : L) = insert(N, sort(L)) .\nendfm")) + +(mct-check! + "sort-321" + (mau/creduce->str mct-sort "sort(s s s 0 : (s 0 : (s s 0 : nil)))") + "_:_(s_(0), _:_(s_(s_(0)), _:_(s_(s_(s_(0))), nil)))") +(mct-check! "sort-empty" (mau/creduce->str mct-sort "sort(nil)") "nil") +(mct-check! + "sort-singleton" + (mau/creduce->str mct-sort "sort(s s 0 : nil)") + "_:_(s_(s_(0)), nil)") +(mct-check! + "insert-front" + (mau/creduce->str mct-sort "insert(0, s 0 : (s s 0 : nil))") + "_:_(0, _:_(s_(0), _:_(s_(s_(0)), nil)))") +(mct-check! + "insert-back" + (mau/creduce->str mct-sort "insert(s s s 0, s 0 : (s s 0 : nil))") + "_:_(s_(0), _:_(s_(s_(0)), _:_(s_(s_(s_(0))), nil)))") + +;; ---- max (conditional simplification, both branches) ---- + +(define + mct-max + (mau/parse-module + "fmod MAX is\n sorts Nat Bool .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op true : -> Bool .\n op false : -> Bool .\n op _<=_ : Nat Nat -> Bool .\n op max : Nat Nat -> Nat .\n vars M N : Nat .\n eq 0 <= N = true .\n eq s M <= 0 = false .\n eq s M <= s N = M <= N .\n ceq max(M, N) = M if N <= M = true .\n ceq max(M, N) = N if N <= M = false .\nendfm")) + +(mct-check! + "max-left" + (mau/creduce->str mct-max "max(s s s 0, s 0)") + "s_(s_(s_(0)))") +(mct-check! + "max-right" + (mau/creduce->str mct-max "max(s 0, s s 0)") + "s_(s_(0))") +(mct-check! + "max-equal" + (mau/creduce->str mct-max "max(s s 0, s s 0)") + "s_(s_(0))") + +;; ---- boolean-kind condition (`if pred`) ---- + +(define + mct-even + (mau/parse-module + "fmod EVEN is\n sorts Nat Bool Tag .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op true : -> Bool .\n op false : -> Bool .\n op even : Nat -> Bool .\n op evn : -> Tag .\n op odd : -> Tag .\n op tag : Nat -> Tag .\n var N : Nat .\n eq even(0) = true .\n eq even(s 0) = false .\n eq even(s s N) = even(N) .\n ceq tag(N) = evn if even(N) .\n ceq tag(N) = odd if even(N) = false .\nendfm")) + +(mct-check! "even-4" (mau/creduce->str mct-even "even(s s s s 0)") "true") +(mct-check! "even-3" (mau/creduce->str mct-even "even(s s s 0)") "false") +(mct-check! "tag-even-bool" (mau/creduce->str mct-even "tag(s s 0)") "evn") +(mct-check! "tag-odd" (mau/creduce->str mct-even "tag(s s s 0)") "odd") + +(define mau-conditional-tests-run! (fn () {:failures mct-failures :total (+ mct-pass mct-fail) :passed mct-pass :failed mct-fail})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index 87e3b4d3..6964e836 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -81,9 +81,9 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 - [x] Tests: classic AC-matching examples (multiset rewriting, set theory, group equations). ### Phase 4 — Conditional equations -- [ ] `ceq L = R if Cond` — apply only when `Cond` reduces to true. -- [ ] Recursion via the same reduce engine (terminating because Cond is shorter). -- [ ] Tests: gcd, sorting, conditional simplifications. +- [x] `ceq L = R if Cond` — apply only when `Cond` reduces to true. +- [x] Recursion via the same reduce engine (terminating because Cond is shorter). +- [x] Tests: gcd, sorting, conditional simplifications. ### Phase 5 — System modules + rewrite rules - [ ] `mod ... endm` syntax with `rl` rules. @@ -177,5 +177,23 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 oracle. `$EMPTY` is a transient marker for empty rest blocks w/o id; never leaks past `mau/restv`. +- **Phase 4 (conditional equations) — DONE, 138/138 total.** + `lib/maude/conditional.sx` is a condition-aware superset of the Phase 3 + reducer. `mau/eq-candidates` enumerates (subst, result) pairs for an + equation (AC via rest-var extension `mau/ac-candidates`, else `mau/mm`); + `mau/try-candidates` commits the first candidate that both makes progress + (canonical form changes) AND whose guard holds. `mau/cond-holds?` evaluates + `{:kind :eq}` guards (reduce both sides, `ac-equal?`) and `{:kind :bool}` + guards (reduce, `=AC= true`), recursing through `mau/cnormalize` — same + reducer, so guards can mention other (conditional) equations. Public: + `mau/creduce` / `mau/creduce->str` / `mau/ccanon`. Verified on gcd + (subtractive, recursive guard), insertion sort (true/false branches), max, + and even (bool-kind `if pred` guard). + - Notes for next phases: `mau/creduce` is the canonical reducer now; Phase 5 + rules reduce to normal form via creduce between rewrite steps. `_:_` cons + parses LEFT-assoc (no `gather` support yet) — write list literals + right-parenthesized, or add a `gather`/parse-assoc attr later if a test + needs bare `a : b : c`. + ## Blockers _(none)_ From 858d35a68c21412d1ce7c75fa17705689376ff26 Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 15:23:06 +0000 Subject: [PATCH 05/17] maude: Phase 5 system modules + rewrite rules (21 tests, 159 total) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit lib/maude/rewrite.sx: rl/crl transitions interleaved with eq normalisation. mau/rewrite = default strategy (top-down, leftmost-outermost, first rule); mau/rew bounded; mau/search = BFS reachability over all successors. lib/maude/fire.sx: short-circuiting matcher (mau/fire-eq) — finds the first productive match instead of enumerating the whole solution set. Fixes the exponential blowup of AC rewriting on many identical elements (8 coins: 60s+ to <1s). Eager match-multiset kept only for match-all / search. Verified on AC coin-change, traffic light, branching search, crl clock. Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/maude/conditional.sx | 8 +- lib/maude/conformance.conf | 3 + lib/maude/fire.sx | 250 ++++++++++++++++++++++++++++++++ lib/maude/rewrite.sx | 284 +++++++++++++++++++++++++++++++++++++ lib/maude/scoreboard.json | 9 +- lib/maude/scoreboard.md | 3 +- lib/maude/tests/rewrite.sx | 114 +++++++++++++++ plans/maude-on-sx.md | 33 ++++- 8 files changed, 692 insertions(+), 12 deletions(-) create mode 100644 lib/maude/fire.sx create mode 100644 lib/maude/rewrite.sx create mode 100644 lib/maude/tests/rewrite.sx diff --git a/lib/maude/conditional.sx b/lib/maude/conditional.sx index 00ea6aa2..31c76965 100644 --- a/lib/maude/conditional.sx +++ b/lib/maude/conditional.sx @@ -10,8 +10,10 @@ ;; — termination rests on the guard reducing on structurally smaller arguments ;; (and the global fuel guard). ;; -;; This engine subsumes mau/ac-reduce: an unconditional equation has cond nil, -;; which always holds. Phases 5+ build on the c-* entry points. +;; Single-step firing uses the short-circuiting matcher in fire.sx +;; (mau/fire-eq) so reduction is not quadratic/exponential in AC argument size. +;; The eager candidate enumeration (mau/eq-candidates) is retained for `search` +;; (rewrite.sx), which genuinely needs every successor. (define mau/ac-candidates @@ -92,7 +94,7 @@ (empty? eqs) nil (let - ((r (mau/try-candidates theory all-eqs (get (first eqs) :cond) term (mau/eq-candidates theory (first eqs) term)))) + ((r (mau/fire-eq theory all-eqs (first eqs) term))) (if (= r nil) (mau/crewrite-loop theory all-eqs (rest eqs) term) r))))) (define diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf index 2e986227..054a00c7 100644 --- a/lib/maude/conformance.conf +++ b/lib/maude/conformance.conf @@ -11,6 +11,8 @@ PRELOADS=( lib/maude/reduce.sx lib/maude/matching.sx lib/maude/conditional.sx + lib/maude/fire.sx + lib/maude/rewrite.sx ) SUITES=( @@ -18,4 +20,5 @@ SUITES=( "reduce:lib/maude/tests/reduce.sx:(mau-reduce-tests-run!)" "matching:lib/maude/tests/matching.sx:(mau-matching-tests-run!)" "conditional:lib/maude/tests/conditional.sx:(mau-conditional-tests-run!)" + "rewrite:lib/maude/tests/rewrite.sx:(mau-rewrite-tests-run!)" ) diff --git a/lib/maude/fire.sx b/lib/maude/fire.sx new file mode 100644 index 00000000..114f66f4 --- /dev/null +++ b/lib/maude/fire.sx @@ -0,0 +1,250 @@ +;; lib/maude/fire.sx — short-circuiting rule/equation firing. +;; +;; The eager matcher (mau/match-multiset) enumerates EVERY substitution, which +;; is what `mau/match-all` and `search` need. But for a single rewrite step we +;; only need the FIRST usable match — and eager enumeration is exponential when +;; an AC argument has many identical elements (q ; q ; ... ; q). These +;; find-matchers thread a predicate and stop at the first complete match for +;; which it returns non-nil; the predicate builds the rewritten term and checks +;; "progresses AND condition holds", so firing short-circuits on the first +;; productive match instead of materialising the whole solution set. +;; +;; pred : subst -> result-term-or-nil (result is always a term, never nil) + +(define + mau/try-list + (fn + (substs cont) + (if + (empty? substs) + nil + (let + ((r (cont (first substs)))) + (if (= r nil) (mau/try-list (rest substs) cont) r))))) + +;; ---- multiset (assoc+comm) find ---- + +(define + mau/ms-find + (fn + (theory f pels sels s id pred) + (cond + ((empty? pels) (if (empty? sels) (pred s) nil)) + (else + (let + ((p (first pels)) (prest (rest pels))) + (if + (mau/var? p) + (mau/ms-find-var + theory + f + prest + sels + s + (mau/vname p) + id + pred + (mau/var-kmin (mau/vname p) id) + (mau/all-splits sels)) + (mau/ms-find-nonvar theory f p prest sels s id pred 0))))))) + +(define + mau/ms-find-nonvar + (fn + (theory f p prest sels s id pred i) + (if + (>= i (len sels)) + nil + (let + ((others (mau/remove-at sels i))) + (let + ((r (mau/try-list (mau/mm theory p (nth sels i) s) (fn (s2) (mau/ms-find theory f prest others s2 id pred))))) + (if + (not (= r nil)) + r + (mau/ms-find-nonvar + theory + f + p + prest + sels + s + id + pred + (+ i 1)))))))) + +(define + mau/ms-find-var + (fn + (theory f prest sels s name id pred kmin splits) + (if + (empty? splits) + nil + (let + ((chosen (first (first splits))) + (rests (nth (first splits) 1))) + (if + (< (len chosen) kmin) + (mau/ms-find-var + theory + f + prest + sels + s + name + id + pred + kmin + (rest splits)) + (let + ((s2 (mau/bind-check theory s name (mau/rebuild f chosen id)))) + (let + ((r (if (= s2 nil) nil (mau/ms-find theory f prest rests s2 id pred)))) + (if + (not (= r nil)) + r + (mau/ms-find-var + theory + f + prest + sels + s + name + id + pred + kmin + (rest splits)))))))))) + +;; ---- sequence (assoc, ordered) find ---- + +(define + mau/seq-find + (fn + (theory f pels sels s id pred) + (cond + ((empty? pels) (if (empty? sels) (pred s) nil)) + (else + (let + ((p (first pels)) (prest (rest pels))) + (if + (mau/var? p) + (mau/seq-find-var + theory + f + prest + sels + s + (mau/vname p) + id + pred + (mau/var-kmin (mau/vname p) id)) + (if + (empty? sels) + nil + (mau/try-list + (mau/mm theory p (first sels) s) + (fn + (s2) + (mau/seq-find theory f prest (rest sels) s2 id pred)))))))))) + +(define + mau/seq-find-var + (fn + (theory f prest sels s name id pred k) + (if + (> k (len sels)) + nil + (let + ((s2 (mau/bind-check theory s name (mau/rebuild f (mau/take sels k) id)))) + (let + ((r (if (= s2 nil) nil (mau/seq-find theory f prest (mau/drop sels k) s2 id pred)))) + (if + (not (= r nil)) + r + (mau/seq-find-var + theory + f + prest + sels + s + name + id + pred + (+ k 1)))))))) + +;; ---- firing an equation/rule (returns rewritten term or nil) ---- + +(define + mau/fire-plain + (fn + (theory eqs eq term cnd substs) + (if + (empty? substs) + nil + (let + ((res (mau/subst-apply (first substs) (get eq :rhs)))) + (if + (and + (not (mau/ac-equal? theory res term)) + (mau/cond-holds? theory eqs cnd (first substs))) + res + (mau/fire-plain theory eqs eq term cnd (rest substs))))))) + +(define + mau/fire-ac + (fn + (theory eqs f th eq term cnd) + (let + ((id (get th :id)) + (pels (mau/flatten-op theory f (get eq :lhs))) + (sels (mau/flatten-op theory f term))) + (let + ((pred (fn (s) (let ((res (mau/ac-eq-result theory f th eq s))) (if (and (not (mau/ac-equal? theory res term)) (mau/cond-holds? theory eqs cnd s)) res nil))))) + (if + (get th :comm) + (mau/ms-find + theory + f + (mau/append2 pels (list (mau/var "$R" ""))) + sels + {} + id + pred) + (mau/seq-find + theory + f + (mau/append2 + (list (mau/var "$L" "")) + (mau/append2 pels (list (mau/var "$R" "")))) + sels + {} + id + pred)))))) + +(define + mau/fire-eq + (fn + (theory eqs eq term) + (let + ((lhs (get eq :lhs)) (cnd (get eq :cond))) + (if + (mau/app? lhs) + (let + ((th (mau/th-of theory (mau/op lhs)))) + (if + (get th :assoc) + (mau/fire-ac theory eqs (mau/op lhs) th eq term cnd) + (mau/fire-plain + theory + eqs + eq + term + cnd + (mau/mm theory lhs term {})))) + (mau/fire-plain + theory + eqs + eq + term + cnd + (mau/mm theory lhs term {})))))) diff --git a/lib/maude/rewrite.sx b/lib/maude/rewrite.sx new file mode 100644 index 00000000..0463c685 --- /dev/null +++ b/lib/maude/rewrite.sx @@ -0,0 +1,284 @@ +;; lib/maude/rewrite.sx — system modules + rewrite rules (Phase 5). +;; +;; Equations (eq/ceq) are applied to a fixpoint to NORMALISE (confluent by +;; intent). Rules (rl/crl) are TRANSITIONS: asymmetric (=>), possibly +;; nondeterministic, NOT applied to a fixpoint. Maude's `rew` interleaves +;; the two: normalise with equations, fire one rule, renormalise, repeat. +;; +;; Rule firing reuses the shared firing machinery — a rule dict carries +;; :lhs/:rhs/:cond exactly like an equation, so `mau/fire-eq` (short-circuit, +;; fire.sx) applies unchanged (matching modulo the AC theory; crl guards +;; evaluated with the equations). A rule fires only if it both progresses and +;; its condition holds. +;; +;; `mau/rewrite` follows the default strategy (top-down, leftmost-outermost, +;; first applicable rule) for one path. `mau/search` does breadth-first reach +;; over ALL one-step successors — for puzzle solvers / protocol simulators +;; where the answer is on a branch `rew` would not take. + +(define mau/rew-fuel 100000) + +;; ---- single-step, default strategy (first applicable, leftmost-outermost) ---- + +(define + mau/rules-at-top + (fn + (theory eqs rules term) + (if + (empty? rules) + nil + (let + ((r (mau/fire-eq theory eqs (first rules) term))) + (if (= r nil) (mau/rules-at-top theory eqs (rest rules) term) r))))) + +(define + mau/apply-rule-once + (fn + (theory eqs rules term) + (let + ((top (mau/rules-at-top theory eqs rules term))) + (if + (not (= top nil)) + top + (if + (mau/app? term) + (mau/apply-rule-in-args + theory + eqs + rules + (mau/op term) + (mau/args term) + (list)) + nil))))) + +(define + mau/apply-rule-in-args + (fn + (theory eqs rules op done todo) + (if + (empty? todo) + nil + (let + ((r (mau/apply-rule-once theory eqs rules (first todo)))) + (if + (= r nil) + (mau/apply-rule-in-args + theory + eqs + rules + op + (mau/append2 done (list (first todo))) + (rest todo)) + (mau/app op (mau/append2 done (cons r (rest todo))))))))) + +(define + mau/rewrite-steps + (fn + (theory eqs rules term steps) + (if + (<= steps 0) + (mau/cnormalize theory eqs term mau/reduce-fuel) + (let + ((nf (mau/cnormalize theory eqs term mau/reduce-fuel))) + (let + ((r (mau/apply-rule-once theory eqs rules nf))) + (if + (= r nil) + nf + (mau/rewrite-steps theory eqs rules r (- steps 1)))))))) + +(define + mau/rewrite + (fn + (m term) + (mau/rewrite-steps + (mau/build-theory m) + (mau/module-eqs m) + (mau/module-rules m) + term + mau/rew-fuel))) + +(define + mau/rew + (fn + (m src n) + (mau/rewrite-steps + (mau/build-theory m) + (mau/module-eqs m) + (mau/module-rules m) + (mau/parse-term-in m src) + n))) + +(define + mau/rewrite-term + (fn (m src) (mau/rewrite m (mau/parse-term-in m src)))) + +(define + mau/rewrite->str + (fn (m src) (mau/term->str (mau/rewrite-term m src)))) + +(define + mau/rewrite-canon + (fn (m src) (mau/canon (mau/build-theory m) (mau/rewrite-term m src)))) + +(define mau/rew->str (fn (m src n) (mau/term->str (mau/rew m src n)))) + +(define + mau/rew-canon + (fn (m src n) (mau/canon (mau/build-theory m) (mau/rew m src n)))) + +;; ---- all one-step successors (for search; eager enumeration) ---- + +(define + mau/cands-results + (fn + (theory eqs cond term cands) + (mau/concat-map + (fn + (c) + (if + (and + (not (mau/ac-equal? theory (get c :result) term)) + (mau/cond-holds? theory eqs cond (get c :s))) + (list (mau/cnormalize theory eqs (get c :result) mau/reduce-fuel)) + (list))) + cands))) + +(define + mau/top-successors + (fn + (theory eqs rules term) + (mau/concat-map + (fn + (rule) + (mau/cands-results + theory + eqs + (get rule :cond) + term + (mau/eq-candidates theory rule term))) + rules))) + +(define + mau/arg-successors + (fn + (theory eqs rules op done todo) + (if + (empty? todo) + (list) + (mau/append2 + (map + (fn + (sub) + (mau/app op (mau/append2 done (cons sub (rest todo))))) + (mau/all-successors theory eqs rules (first todo))) + (mau/arg-successors + theory + eqs + rules + op + (mau/append2 done (list (first todo))) + (rest todo)))))) + +(define + mau/all-successors + (fn + (theory eqs rules term) + (mau/append2 + (mau/top-successors theory eqs rules term) + (if + (mau/app? term) + (mau/arg-successors + theory + eqs + rules + (mau/op term) + (mau/args term) + (list)) + (list))))) + +(define + mau/successors + (fn + (m src) + (let + ((theory (mau/build-theory m)) (eqs (mau/module-eqs m))) + (map + (fn (t) (mau/canon theory t)) + (mau/all-successors + theory + eqs + (mau/module-rules m) + (mau/cnormalize + theory + eqs + (mau/parse-term-in m src) + mau/reduce-fuel)))))) + +;; ---- breadth-first reachability search ---- + +(define + mau/canon-list + (fn (theory ts) (map (fn (t) (mau/canon theory t)) ts))) + +(define + mau/bfs-search + (fn + (theory eqs rules frontier seen goal depth) + (cond + ((mau/member? goal (mau/canon-list theory frontier)) true) + ((<= depth 0) false) + ((empty? frontier) false) + (else + (let + ((newf (list)) (newseen seen)) + (for-each + (fn + (t) + (for-each + (fn + (succ) + (let + ((c (mau/canon theory succ))) + (when + (not (mau/member? c newseen)) + (do + (set! newseen (cons c newseen)) + (append! newf succ))))) + (mau/all-successors theory eqs rules t))) + frontier) + (mau/bfs-search + theory + eqs + rules + newf + newseen + goal + (- depth 1))))))) + +(define + mau/search + (fn + (m start-src goal-src max-depth) + (let + ((theory (mau/build-theory m)) + (eqs (mau/module-eqs m)) + (rules (mau/module-rules m))) + (let + ((start (mau/cnormalize theory eqs (mau/parse-term-in m start-src) mau/reduce-fuel)) + (goal + (mau/canon + theory + (mau/cnormalize + theory + eqs + (mau/parse-term-in m goal-src) + mau/reduce-fuel)))) + (mau/bfs-search + theory + eqs + rules + (list start) + (list (mau/canon theory start)) + goal + max-depth))))) diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json index 5e552292..b0574a30 100644 --- a/lib/maude/scoreboard.json +++ b/lib/maude/scoreboard.json @@ -1,13 +1,14 @@ { "lang": "maude", - "total_passed": 138, + "total_passed": 159, "total_failed": 0, - "total": 138, + "total": 159, "suites": [ {"name":"parse","passed":65,"failed":0,"total":65}, {"name":"reduce","passed":26,"failed":0,"total":26}, {"name":"matching","passed":28,"failed":0,"total":28}, - {"name":"conditional","passed":19,"failed":0,"total":19} + {"name":"conditional","passed":19,"failed":0,"total":19}, + {"name":"rewrite","passed":21,"failed":0,"total":21} ], - "generated": "2026-06-07T15:05:31+00:00" + "generated": "2026-06-07T15:22:28+00:00" } diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md index 12cd28a2..40a50af0 100644 --- a/lib/maude/scoreboard.md +++ b/lib/maude/scoreboard.md @@ -1,6 +1,6 @@ # maude scoreboard -**138 / 138 passing** (0 failure(s)). +**159 / 159 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| @@ -8,3 +8,4 @@ | reduce | 26 | 26 | ok | | matching | 28 | 28 | ok | | conditional | 19 | 19 | ok | +| rewrite | 21 | 21 | ok | diff --git a/lib/maude/tests/rewrite.sx b/lib/maude/tests/rewrite.sx new file mode 100644 index 00000000..c7e9ed0e --- /dev/null +++ b/lib/maude/tests/rewrite.sx @@ -0,0 +1,114 @@ +;; lib/maude/tests/rewrite.sx — Phase 5: system modules + rewrite rules. + +(define mrw-pass 0) +(define mrw-fail 0) +(define mrw-failures (list)) + +(define + mrw-check! + (fn + (name got expected) + (if + (= got expected) + (set! mrw-pass (+ mrw-pass 1)) + (do + (set! mrw-fail (+ mrw-fail 1)) + (append! + mrw-failures + (str name " expected: " expected " got: " got)))))) + +;; ---- AC multiset transition (the headline: rule on a sub-multiset) ---- + +(define + mrw-coins + (mau/parse-module + "mod COINS is\n sort Marking .\n op nil : -> Marking .\n op q : -> Marking .\n op d : -> Marking .\n op _;_ : Marking Marking -> Marking [assoc comm id: nil] .\n rl [change] : q ; q ; q ; q => d .\nendm")) + +(mrw-check! "coins-kind" (mau/module-kind mrw-coins) "mod") +(mrw-check! "coins-rules" (len (mau/module-rules mrw-coins)) 1) +(mrw-check! "coins-exact" (mau/rewrite-canon mrw-coins "q ; q ; q ; q") "d") +(mrw-check! + "coins-5" + (mau/rewrite-canon mrw-coins "q ; q ; q ; q ; q") + "_;_(d,q)") +(mrw-check! + "coins-8" + (mau/rewrite-canon mrw-coins "q ; q ; q ; q ; q ; q ; q ; q") + "_;_(d,d)") +(mrw-check! + "coins-3-stuck" + (mau/rewrite-canon mrw-coins "q ; q ; q") + "_;_(q,q,q)") + +;; ---- cyclic state machine (bounded rew) ---- + +(define + mrw-traffic + (mau/parse-module + "mod TRAFFIC is\n sort Light .\n ops red green yellow : -> Light .\n rl [g] : red => green .\n rl [y] : green => yellow .\n rl [r] : yellow => red .\nendm")) + +(mrw-check! "traffic-1" (mau/rew->str mrw-traffic "red" 1) "green") +(mrw-check! "traffic-2" (mau/rew->str mrw-traffic "red" 2) "yellow") +(mrw-check! "traffic-3" (mau/rew->str mrw-traffic "red" 3) "red") +(mrw-check! "traffic-0" (mau/rew->str mrw-traffic "green" 0) "green") + +;; ---- nondeterministic branching: rew (one path) vs search (all paths) ---- + +(define + mrw-ndet + (mau/parse-module + "mod NDET is\n sort S .\n ops a b c d goal : -> S .\n rl [r1] : a => b .\n rl [r2] : a => c .\n rl [r3] : b => d .\n rl [r4] : c => goal .\nendm")) + +;; rew takes the first rule each step: a -> b -> d (stuck), never reaches goal. +(mrw-check! "ndet-rew-path" (mau/rewrite->str mrw-ndet "a") "d") +(mrw-check! "ndet-succ" (mau/successors mrw-ndet "a") (list "b" "c")) +(mrw-check! + "ndet-search-goal" + (mau/search mrw-ndet "a" "goal" 5) + true) +(mrw-check! + "ndet-search-shallow" + (mau/search mrw-ndet "a" "goal" 1) + false) +(mrw-check! "ndet-search-self" (mau/search mrw-ndet "a" "a" 3) true) +(mrw-check! "ndet-search-d" (mau/search mrw-ndet "a" "d" 5) true) + +;; ---- conditional rule (crl with equational guard) ---- + +(define + mrw-clock + (mau/parse-module + "mod CLOCK is\n sorts Nat Bool .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op true : -> Bool .\n op false : -> Bool .\n op _<_ : Nat Nat -> Bool .\n op clk : Nat -> Nat .\n vars M N : Nat .\n eq 0 < s N = true .\n eq N < 0 = false .\n eq s M < s N = M < N .\n crl [tick] : clk(N) => clk(s N) if N < s s s 0 = true .\nendm")) + +;; tick fires while N < 3, then stops at clk(3). +(mrw-check! + "clock-run" + (mau/rewrite->str mrw-clock "clk(0)") + "clk(s_(s_(s_(0))))") +(mrw-check! + "clock-from-1" + (mau/rewrite->str mrw-clock "clk(s 0)") + "clk(s_(s_(s_(0))))") +(mrw-check! + "clock-step1" + (mau/rew->str mrw-clock "clk(0)" 1) + "clk(s_(0))") + +;; ---- eqs interleave with rules ---- + +(define + mrw-mix + (mau/parse-module + "mod MIX is\n sort Nat .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op _+_ : Nat Nat -> Nat .\n op f : Nat -> Nat .\n vars X Y : Nat .\n eq 0 + Y = Y .\n eq s X + Y = s (X + Y) .\n rl [step] : f(X) => f(X + s 0) .\nendm")) + +;; each rule step adds one (via the rule), eqs normalise the sum. +(mrw-check! + "mix-step1" + (mau/rew->str mrw-mix "f(s 0)" 1) + "f(s_(s_(0)))") +(mrw-check! + "mix-step2" + (mau/rew->str mrw-mix "f(0)" 2) + "f(s_(s_(0)))") + +(define mau-rewrite-tests-run! (fn () {:failures mrw-failures :total (+ mrw-pass mrw-fail) :passed mrw-pass :failed mrw-fail})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index 6964e836..df8c4067 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -86,10 +86,10 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 - [x] Tests: gcd, sorting, conditional simplifications. ### Phase 5 — System modules + rewrite rules -- [ ] `mod ... endm` syntax with `rl` rules. -- [ ] Rules apply asymmetrically (`=>` not `=`); fairness across rules. -- [ ] Default strategy: top-down, leftmost-outermost, first applicable rule. -- [ ] Tests: state-transition systems (puzzle solvers, protocol simulators). +- [x] `mod ... endm` syntax with `rl` rules. +- [x] Rules apply asymmetrically (`=>` not `=`); fairness across rules. +- [x] Default strategy: top-down, leftmost-outermost, first applicable rule. +- [x] Tests: state-transition systems (puzzle solvers, protocol simulators). ### Phase 6 — Strategy language - [ ] Compose strategies: sequential `;`, alternative `|`, iteration `*`, fixed-point. @@ -195,5 +195,30 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 right-parenthesized, or add a `gather`/parse-assoc attr later if a test needs bare `a : b : c`. +- **Phase 5 (system modules + rewrite rules) — DONE, 159/159 total.** + `lib/maude/rewrite.sx` + `lib/maude/fire.sx`. Rules (rl/crl) reuse the + equation firing machinery (a rule dict is shaped like an eq). `mau/rewrite` + is the default strategy: normalise with eqs (`creduce`), fire ONE rule + top-down/leftmost-outermost/first-applicable, renormalise, repeat (bounded + by fuel). `mau/rew m src n` = bounded `rew [n]`. `mau/search` is BFS over + ALL one-step successors (`mau/all-successors`) for reachability — solves the + branching `goal` reachable only off the path `rew` takes. Verified: AC + multiset coin-change (rule on a sub-multiset), cyclic traffic light (bounded), + branching nondeterminism (rew vs search), conditional `crl` clock, eq/rule + interleaving. + - **PERF (important):** `lib/maude/fire.sx` is the short-circuiting matcher — + `mau/fire-eq` finds the FIRST productive match via predicate-threaded + `mau/ms-find`/`mau/seq-find` instead of materialising the whole solution + set. Without it, AC rewriting on N identical elements is exponential + (`q;q;q;q;q;q;q;q` went 60s+ → <1s). The eager `mau/match-multiset` / + `mau/eq-candidates` are kept ONLY for `mau/match-all` and `search` (which + truly need every solution). Phase 4 `creduce` and Phase 5 rules both fire + via `mau/fire-eq`. Keep this split: never route single-step rewriting + through the eager enumerator. + - Notes: juxtaposition `__` (empty-token mixfix) and `gather` are NOT parsed — + use an explicit infix op for multisets and right-parenthesise list literals. + `.` can't be an op token (statement terminator). `mau/search` is the prime + Phase 7 reflection / Phase 8 extraction target alongside the matcher. + ## Blockers _(none)_ From e2aca38a8451eac5460d11b9787723d45d931603 Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 15:26:52 +0000 Subject: [PATCH 06/17] maude: Phase 6 strategy language (19 tests, 178 total) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit lib/maude/strategy.sx — first-class set-valued strategies: idle/fail/all/ rule/seq/alt/star/plus/bang/name combinators, named-strategy env. Same rule set computes different things under different strategies; verified with single-rule vs all vs seq-order vs alt vs star vs bang. Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/maude/conformance.conf | 2 + lib/maude/scoreboard.json | 9 +- lib/maude/scoreboard.md | 3 +- lib/maude/strategy.sx | 217 ++++++++++++++++++++++++++++++++++++ lib/maude/tests/strategy.sx | 151 +++++++++++++++++++++++++ plans/maude-on-sx.md | 21 +++- 6 files changed, 395 insertions(+), 8 deletions(-) create mode 100644 lib/maude/strategy.sx create mode 100644 lib/maude/tests/strategy.sx diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf index 054a00c7..d1a1403b 100644 --- a/lib/maude/conformance.conf +++ b/lib/maude/conformance.conf @@ -13,6 +13,7 @@ PRELOADS=( lib/maude/conditional.sx lib/maude/fire.sx lib/maude/rewrite.sx + lib/maude/strategy.sx ) SUITES=( @@ -21,4 +22,5 @@ SUITES=( "matching:lib/maude/tests/matching.sx:(mau-matching-tests-run!)" "conditional:lib/maude/tests/conditional.sx:(mau-conditional-tests-run!)" "rewrite:lib/maude/tests/rewrite.sx:(mau-rewrite-tests-run!)" + "strategy:lib/maude/tests/strategy.sx:(mau-strategy-tests-run!)" ) diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json index b0574a30..4da98e20 100644 --- a/lib/maude/scoreboard.json +++ b/lib/maude/scoreboard.json @@ -1,14 +1,15 @@ { "lang": "maude", - "total_passed": 159, + "total_passed": 178, "total_failed": 0, - "total": 159, + "total": 178, "suites": [ {"name":"parse","passed":65,"failed":0,"total":65}, {"name":"reduce","passed":26,"failed":0,"total":26}, {"name":"matching","passed":28,"failed":0,"total":28}, {"name":"conditional","passed":19,"failed":0,"total":19}, - {"name":"rewrite","passed":21,"failed":0,"total":21} + {"name":"rewrite","passed":21,"failed":0,"total":21}, + {"name":"strategy","passed":19,"failed":0,"total":19} ], - "generated": "2026-06-07T15:22:28+00:00" + "generated": "2026-06-07T15:26:26+00:00" } diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md index 40a50af0..8cdf4740 100644 --- a/lib/maude/scoreboard.md +++ b/lib/maude/scoreboard.md @@ -1,6 +1,6 @@ # maude scoreboard -**159 / 159 passing** (0 failure(s)). +**178 / 178 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| @@ -9,3 +9,4 @@ | matching | 28 | 28 | ok | | conditional | 19 | 19 | ok | | rewrite | 21 | 21 | ok | +| strategy | 19 | 19 | ok | diff --git a/lib/maude/strategy.sx b/lib/maude/strategy.sx new file mode 100644 index 00000000..0e208d5d --- /dev/null +++ b/lib/maude/strategy.sx @@ -0,0 +1,217 @@ +;; lib/maude/strategy.sx — strategy language (Phase 6). +;; +;; A strategy controls HOW rules are applied. Strategies are first-class values +;; (tagged dicts) and SET-VALUED: applying a strategy to a term yields the set +;; (deduped by canonical form) of result terms. The same rule set under +;; different strategies computes different things — `;` sequences, `|` unions, +;; `*`/`+` iterate, `!` normalises. +;; +;; Constructors: +;; (mau/s-idle) identity (the term itself) +;; (mau/s-fail) empty set +;; (mau/s-all) apply any rule once, anywhere +;; (mau/s-rule LABEL) apply a named rule once, anywhere +;; (mau/s-seq A B) A ; B (apply B to every result of A) +;; (mau/s-alt A B) A | B (union of results) +;; (mau/s-star A) A * (reflexive-transitive closure) +;; (mau/s-plus A) A + (one or more) +;; (mau/s-bang A) A ! (normal forms: results where A can't apply) +;; (mau/s-name N) look up named strategy N in the env +;; +;; Run with (mau/srun M STRATS STRAT SRC): STRATS is a dict NAME -> strategy. + +(define mau/s-idle (fn () {:s :idle})) +(define mau/s-fail (fn () {:s :fail})) +(define mau/s-all (fn () {:s :all})) +(define mau/s-rule (fn (label) {:label label :s :rule})) +(define mau/s-seq (fn (a b) {:a a :b b :s :seq})) +(define mau/s-alt (fn (a b) {:a a :b b :s :alt})) +(define mau/s-star (fn (a) {:a a :s :star})) +(define mau/s-plus (fn (a) {:a a :s :plus})) +(define mau/s-bang (fn (a) {:a a :s :bang})) +(define mau/s-name (fn (n) {:n n :s :name})) + +(define + mau/rules-with-label + (fn (rules label) (filter (fn (r) (= (get r :label) label)) rules))) + +(define + mau/dedup-loop + (fn + (theory ts seen acc) + (if + (empty? ts) + acc + (let + ((c (mau/canon theory (first ts)))) + (if + (mau/member? c seen) + (mau/dedup-loop theory (rest ts) seen acc) + (mau/dedup-loop + theory + (rest ts) + (cons c seen) + (mau/append2 acc (list (first ts))))))))) + +(define + mau/dedup-canon + (fn (theory ts) (mau/dedup-loop theory ts (list) (list)))) + +;; ---- strategy interpreter ---- + +(define + mau/sapply + (fn + (ctx strat term) + (let + ((k (get strat :s)) (theory (get ctx :theory))) + (cond + ((= k "idle") (list term)) + ((= k "fail") (list)) + ((= k "all") + (mau/dedup-canon + theory + (mau/all-successors theory (get ctx :eqs) (get ctx :rules) term))) + ((= k "rule") + (mau/dedup-canon + theory + (mau/all-successors + theory + (get ctx :eqs) + (mau/rules-with-label (get ctx :rules) (get strat :label)) + term))) + ((= k "seq") + (mau/dedup-canon + theory + (mau/concat-map + (fn (t) (mau/sapply ctx (get strat :b) t)) + (mau/sapply ctx (get strat :a) term)))) + ((= k "alt") + (mau/dedup-canon + theory + (mau/append2 + (mau/sapply ctx (get strat :a) term) + (mau/sapply ctx (get strat :b) term)))) + ((= k "star") (mau/sstar ctx (get strat :a) term)) + ((= k "plus") + (mau/dedup-canon + theory + (mau/concat-map + (fn (t) (mau/sstar ctx (get strat :a) t)) + (mau/sapply ctx (get strat :a) term)))) + ((= k "bang") + (mau/dedup-canon theory (mau/sbang ctx (get strat :a) term))) + ((= k "name") + (mau/sapply ctx (get (get ctx :strats) (get strat :n)) term)) + (else (list)))))) + +;; reflexive-transitive closure: term plus everything reachable via A +(define + mau/sstar + (fn + (ctx a term) + (mau/sstar-loop + ctx + a + (list term) + (list (mau/canon (get ctx :theory) term)) + (list term)))) + +(define + mau/sstar-loop + (fn + (ctx a frontier seen acc) + (if + (empty? frontier) + acc + (let + ((newf (list)) + (newseen seen) + (newacc acc) + (theory (get ctx :theory))) + (for-each + (fn + (t) + (for-each + (fn + (succ) + (let + ((c (mau/canon theory succ))) + (when + (not (mau/member? c newseen)) + (do + (set! newseen (cons c newseen)) + (append! newf succ) + (append! newacc succ))))) + (mau/sapply ctx a t))) + frontier) + (mau/sstar-loop ctx a newf newseen newacc))))) + +;; normal forms: terms reachable via A where A yields nothing more +(define + mau/sbang + (fn + (ctx a term) + (mau/sbang-loop + ctx + a + (list term) + (list (mau/canon (get ctx :theory) term)) + (list)))) + +(define + mau/sbang-loop + (fn + (ctx a frontier seen acc) + (if + (empty? frontier) + acc + (let + ((newf (list)) + (newseen seen) + (newacc acc) + (theory (get ctx :theory))) + (for-each + (fn + (t) + (let + ((succs (mau/sapply ctx a t))) + (if + (empty? succs) + (append! newacc t) + (for-each + (fn + (succ) + (let + ((c (mau/canon theory succ))) + (when + (not (mau/member? c newseen)) + (do + (set! newseen (cons c newseen)) + (append! newf succ))))) + succs)))) + frontier) + (mau/sbang-loop ctx a newf newseen newacc))))) + +;; ---- public API ---- + +(define mau/make-sctx (fn (m strats) {:eqs (mau/module-eqs m) :theory (mau/build-theory m) :strats strats :rules (mau/module-rules m)})) + +(define + mau/srun + (fn + (m strats strat src) + (let + ((ctx (mau/make-sctx m strats))) + (let + ((t0 (mau/cnormalize (get ctx :theory) (get ctx :eqs) (mau/parse-term-in m src) mau/reduce-fuel))) + (mau/dedup-canon (get ctx :theory) (mau/sapply ctx strat t0)))))) + +(define + mau/srun-canon + (fn + (m strats strat src) + (let + ((theory (mau/build-theory m))) + (mau/sort-strings + (map (fn (t) (mau/canon theory t)) (mau/srun m strats strat src)))))) diff --git a/lib/maude/tests/strategy.sx b/lib/maude/tests/strategy.sx new file mode 100644 index 00000000..4c58535d --- /dev/null +++ b/lib/maude/tests/strategy.sx @@ -0,0 +1,151 @@ +;; lib/maude/tests/strategy.sx — Phase 6: strategy language. + +(define mst-pass 0) +(define mst-fail 0) +(define mst-failures (list)) + +(define + mst-check! + (fn + (name got expected) + (if + (= got expected) + (set! mst-pass (+ mst-pass 1)) + (do + (set! mst-fail (+ mst-fail 1)) + (append! + mst-failures + (str name " expected: " expected " got: " got)))))) + +;; ---- a branching system; meaning depends on the strategy ---- + +(define + mst-mod + (mau/parse-module + "mod CHOICE is\n sort S .\n ops a b c x y : -> S .\n rl [r1] : a => b .\n rl [r2] : b => c .\n rl [toX] : a => x .\n rl [toY] : a => y .\nendm")) + +(define mst-env {}) +(dict-set! mst-env "twice" (mau/s-seq (mau/s-rule "r1") (mau/s-rule "r2"))) +(dict-set! mst-env "anyplus" (mau/s-plus (mau/s-all))) +(dict-set! mst-env "norm" (mau/s-bang (mau/s-all))) + +;; basic combinators +(mst-check! + "idle" + (mau/srun-canon mst-mod mst-env (mau/s-idle) "a") + (list "a")) +(mst-check! "fail" (mau/srun-canon mst-mod mst-env (mau/s-fail) "a") (list)) +(mst-check! + "single-rule" + (mau/srun-canon mst-mod mst-env (mau/s-rule "r1") "a") + (list "b")) +(mst-check! + "single-rule-x" + (mau/srun-canon mst-mod mst-env (mau/s-rule "toX") "a") + (list "x")) +(mst-check! + "all" + (mau/srun-canon mst-mod mst-env (mau/s-all) "a") + (list "b" "x" "y")) + +;; sequencing: order matters +(mst-check! + "seq-ok" + (mau/srun-canon + mst-mod + mst-env + (mau/s-seq (mau/s-rule "r1") (mau/s-rule "r2")) + "a") + (list "c")) +(mst-check! + "seq-fail" + (mau/srun-canon + mst-mod + mst-env + (mau/s-seq (mau/s-rule "r2") (mau/s-rule "r1")) + "a") + (list)) + +;; alternation: union +(mst-check! + "alt" + (mau/srun-canon + mst-mod + mst-env + (mau/s-alt (mau/s-rule "toX") (mau/s-rule "toY")) + "a") + (list "x" "y")) +(mst-check! + "alt-with-fail" + (mau/srun-canon + mst-mod + mst-env + (mau/s-alt (mau/s-rule "r2") (mau/s-rule "r1")) + "a") + (list "b")) + +;; iteration +(mst-check! + "star" + (mau/srun-canon mst-mod mst-env (mau/s-star (mau/s-all)) "a") + (list "a" "b" "c" "x" "y")) +(mst-check! + "plus" + (mau/srun-canon mst-mod mst-env (mau/s-plus (mau/s-all)) "a") + (list "b" "c" "x" "y")) +(mst-check! + "bang-normal-forms" + (mau/srun-canon mst-mod mst-env (mau/s-bang (mau/s-all)) "a") + (list "c" "x" "y")) +(mst-check! + "star-from-b" + (mau/srun-canon mst-mod mst-env (mau/s-star (mau/s-all)) "b") + (list "b" "c")) + +;; named strategies + strategy expressions as values +(mst-check! + "named-twice" + (mau/srun-canon mst-mod mst-env (mau/s-name "twice") "a") + (list "c")) +(mst-check! + "named-anyplus" + (mau/srun-canon mst-mod mst-env (mau/s-name "anyplus") "a") + (list "b" "c" "x" "y")) +(mst-check! + "named-norm" + (mau/srun-canon mst-mod mst-env (mau/s-name "norm") "a") + (list "c" "x" "y")) + +;; nested composition: (r1 ; r2) | toX +(mst-check! + "nested" + (mau/srun-canon + mst-mod + mst-env + (mau/s-alt + (mau/s-seq (mau/s-rule "r1") (mau/s-rule "r2")) + (mau/s-rule "toX")) + "a") + (list "c" "x")) + +;; ---- a 1-D walk: strategy chooses how far ---- + +(define + mst-walk + (mau/parse-module + "mod WALK is\n sort Pos .\n op 0 : -> Pos .\n op s_ : Pos -> Pos .\n op p : Pos -> Pos .\n var X : Pos .\n rl [step] : p(X) => p(s X) .\nendm")) + +(mst-check! + "walk-one" + (mau/srun-canon mst-walk {} (mau/s-rule "step") "p(0)") + (list "p(s_(0))")) +(mst-check! + "walk-twice" + (mau/srun-canon + mst-walk + {} + (mau/s-seq (mau/s-rule "step") (mau/s-rule "step")) + "p(0)") + (list "p(s_(s_(0)))")) + +(define mau-strategy-tests-run! (fn () {:failures mst-failures :total (+ mst-pass mst-fail) :passed mst-pass :failed mst-fail})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index df8c4067..5b3ddc48 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -92,9 +92,9 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 - [x] Tests: state-transition systems (puzzle solvers, protocol simulators). ### Phase 6 — Strategy language -- [ ] Compose strategies: sequential `;`, alternative `|`, iteration `*`, fixed-point. -- [ ] User-named strategies; strategy expressions as values. -- [ ] Tests: programs whose meaning depends on strategy choice. +- [x] Compose strategies: sequential `;`, alternative `|`, iteration `*`, fixed-point. +- [x] User-named strategies; strategy expressions as values. +- [x] Tests: programs whose meaning depends on strategy choice. ### Phase 7 — Reflection (META-LEVEL) - [ ] Terms-as-data: `META-LEVEL` lets you encode/decode terms as Maude terms. @@ -220,5 +220,20 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 `.` can't be an op token (statement terminator). `mau/search` is the prime Phase 7 reflection / Phase 8 extraction target alongside the matcher. +- **Phase 6 (strategy language) — DONE, 178/178 total.** + `lib/maude/strategy.sx`. Strategies are first-class tagged-dict VALUES and + set-valued: `mau/sapply ctx strat term` → deduped (by canon) list of results. + Combinators: `idle`/`fail`/`all`/`rule LABEL`/`seq`/`alt`/`star`/`plus`/`bang` + /`name`. `seq` = flatmap B over A's results; `alt` = union; `star` = reflexive- + transitive closure (BFS, canon-deduped); `plus` = A then star; `bang` = + normal forms (reachable terms where A yields nothing). Named strategies via a + NAME->strategy env dict passed to `mau/srun`/`mau/srun-canon`. Verified that + the same rule set computes different things under different strategies + (single rule vs all vs seq order vs alt vs star vs bang). Built on Phase 5 + `mau/all-successors` (rule label filter = `mau/rules-with-label`). + - Note: `dict-set!` returns the value, not the dict — build a named-strategy + env by binding `(define env {})` then `(dict-set! env ...)`, pass `env`. + `srun-canon` sorts results so expected lists must be sorted. + ## Blockers _(none)_ From 4018671087b457826013f5a5c020eca99ceb1373 Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 15:29:45 +0000 Subject: [PATCH 07/17] maude: Phase 7 reflection / META-LEVEL (18 tests, 196 total) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit lib/maude/meta.sx — up-term/down-term encode terms as data (mt-var/mt-app), reflective meta-reduce/meta-rewrite/meta-apply, the meta-circular law down(metaReduce(up t)) =AC= reduce t, and meta-prove-equal? as a generic equational theorem helper. Verified round-trips, reflection agreement, single-rule meta-apply, and proving commutativity/associativity instances. Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/maude/conformance.conf | 2 + lib/maude/meta.sx | 104 +++++++++++++++++++++++++++ lib/maude/scoreboard.json | 9 +-- lib/maude/scoreboard.md | 3 +- lib/maude/tests/meta.sx | 144 +++++++++++++++++++++++++++++++++++++ plans/maude-on-sx.md | 20 +++++- 6 files changed, 274 insertions(+), 8 deletions(-) create mode 100644 lib/maude/meta.sx create mode 100644 lib/maude/tests/meta.sx diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf index d1a1403b..b82e4937 100644 --- a/lib/maude/conformance.conf +++ b/lib/maude/conformance.conf @@ -14,6 +14,7 @@ PRELOADS=( lib/maude/fire.sx lib/maude/rewrite.sx lib/maude/strategy.sx + lib/maude/meta.sx ) SUITES=( @@ -23,4 +24,5 @@ SUITES=( "conditional:lib/maude/tests/conditional.sx:(mau-conditional-tests-run!)" "rewrite:lib/maude/tests/rewrite.sx:(mau-rewrite-tests-run!)" "strategy:lib/maude/tests/strategy.sx:(mau-strategy-tests-run!)" + "meta:lib/maude/tests/meta.sx:(mau-meta-tests-run!)" ) diff --git a/lib/maude/meta.sx b/lib/maude/meta.sx new file mode 100644 index 00000000..db064614 --- /dev/null +++ b/lib/maude/meta.sx @@ -0,0 +1,104 @@ +;; lib/maude/meta.sx — reflection / META-LEVEL (Phase 7). +;; +;; Reflection: a term can be represented AS DATA — another term — and meta-level +;; functions interpret that representation. In Maude this is the META-LEVEL +;; (upTerm/downTerm, metaReduce, metaApply, ...). Here object terms are already +;; SX dicts; the META representation re-encodes a term as a term built from the +;; meta-constructors `mt-var` and `mt-app`, so a represented term is itself a +;; first-class object term you can build, inspect, and transform. +;; +;; up-term(X:S) = mt-var(X, S) (names/sorts as constants) +;; up-term(f(a,b)) = mt-app(f, up(a), up(b)) +;; down-term reverses. +;; +;; Meta-operations reflect object-level behaviour: metaReduce of a represented +;; term in a module = the representation of its normal form, etc. The +;; meta-circular law `down(metaReduce(up t)) =AC= reduce t` is exactly the +;; statement that reflection agrees with the object level. + +(define + mau/up-term + (fn + (t) + (cond + ((mau/var? t) + (mau/app + "mt-var" + (list (mau/const (mau/vname t)) (mau/const (mau/vsort t))))) + ((mau/app? t) + (mau/app + "mt-app" + (cons (mau/const (mau/op t)) (map mau/up-term (mau/args t))))) + (else t)))) + +(define + mau/down-term + (fn + (mt) + (cond + ((and (mau/app? mt) (= (mau/op mt) "mt-var")) + (mau/var + (mau/op (nth (mau/args mt) 0)) + (mau/op (nth (mau/args mt) 1)))) + ((and (mau/app? mt) (= (mau/op mt) "mt-app")) + (mau/app + (mau/op (first (mau/args mt))) + (map mau/down-term (rest (mau/args mt))))) + (else mt)))) + +;; ---- reflective operations (term <-> meta-term) ---- + +(define + mau/meta-reduce + (fn (m mt) (mau/up-term (mau/creduce m (mau/down-term mt))))) + +(define + mau/meta-rewrite + (fn (m mt) (mau/up-term (mau/rewrite m (mau/down-term mt))))) + +;; apply a named rule once at the top of the represented term; nil if it can't. +(define + mau/meta-apply + (fn + (m label mt) + (let + ((theory (mau/build-theory m)) (eqs (mau/module-eqs m))) + (let + ((r (mau/rules-at-top theory eqs (mau/rules-with-label (mau/module-rules m) label) (mau/down-term mt)))) + (if + (= r nil) + nil + (mau/up-term (mau/cnormalize theory eqs r mau/reduce-fuel))))))) + +;; ---- source-level conveniences ---- + +(define mau/meta-up (fn (m src) (mau/up-term (mau/parse-term-in m src)))) + +(define + mau/meta-reduce-src + (fn (m src) (mau/down-term (mau/meta-reduce m (mau/meta-up m src))))) + +(define + mau/meta-reduce-canon + (fn (m src) (mau/canon (mau/build-theory m) (mau/meta-reduce-src m src)))) + +;; ---- generic theorem helper: equational proof by reduction ---- + +(define + mau/meta-prove-equal? + (fn + (m srcA srcB) + (mau/ac-equal? + (mau/build-theory m) + (mau/creduce-term m srcA) + (mau/creduce-term m srcB)))) + +;; meta-circular law: down(metaReduce(up t)) =AC= reduce(t) +(define + mau/meta-circular? + (fn + (m src) + (mau/ac-equal? + (mau/build-theory m) + (mau/meta-reduce-src m src) + (mau/creduce-term m src)))) diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json index 4da98e20..f5ecaf27 100644 --- a/lib/maude/scoreboard.json +++ b/lib/maude/scoreboard.json @@ -1,15 +1,16 @@ { "lang": "maude", - "total_passed": 178, + "total_passed": 196, "total_failed": 0, - "total": 178, + "total": 196, "suites": [ {"name":"parse","passed":65,"failed":0,"total":65}, {"name":"reduce","passed":26,"failed":0,"total":26}, {"name":"matching","passed":28,"failed":0,"total":28}, {"name":"conditional","passed":19,"failed":0,"total":19}, {"name":"rewrite","passed":21,"failed":0,"total":21}, - {"name":"strategy","passed":19,"failed":0,"total":19} + {"name":"strategy","passed":19,"failed":0,"total":19}, + {"name":"meta","passed":18,"failed":0,"total":18} ], - "generated": "2026-06-07T15:26:26+00:00" + "generated": "2026-06-07T15:29:16+00:00" } diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md index 8cdf4740..82d57830 100644 --- a/lib/maude/scoreboard.md +++ b/lib/maude/scoreboard.md @@ -1,6 +1,6 @@ # maude scoreboard -**178 / 178 passing** (0 failure(s)). +**196 / 196 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| @@ -10,3 +10,4 @@ | conditional | 19 | 19 | ok | | rewrite | 21 | 21 | ok | | strategy | 19 | 19 | ok | +| meta | 18 | 18 | ok | diff --git a/lib/maude/tests/meta.sx b/lib/maude/tests/meta.sx new file mode 100644 index 00000000..5200ec78 --- /dev/null +++ b/lib/maude/tests/meta.sx @@ -0,0 +1,144 @@ +;; lib/maude/tests/meta.sx — Phase 7: reflection (META-LEVEL). + +(define mmtt-pass 0) +(define mmtt-fail 0) +(define mmtt-failures (list)) + +(define + mmtt-check! + (fn + (name got expected) + (if + (= got expected) + (set! mmtt-pass (+ mmtt-pass 1)) + (do + (set! mmtt-fail (+ mmtt-fail 1)) + (append! + mmtt-failures + (str name " expected: " expected " got: " got)))))) + +(define + mmtt-peano + (mau/parse-module + "fmod PEANO is\n sort Nat .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op _+_ : Nat Nat -> Nat [assoc comm] .\n vars X Y : Nat .\n eq 0 + Y = Y .\n eq s X + Y = s (X + Y) .\nendfm")) + +(define + mmtt-ndet + (mau/parse-module + "mod NDET is\n sort S .\n ops a b c : -> S .\n rl [r1] : a => b .\n rl [r2] : b => c .\nendm")) + +;; ---- terms-as-data: up / down ---- + +(mmtt-check! + "up-const" + (mau/term->str (mau/meta-up mmtt-peano "0")) + "mt-app(0)") +(mmtt-check! + "up-s0" + (mau/term->str (mau/meta-up mmtt-peano "s 0")) + "mt-app(s_, mt-app(0))") +(mmtt-check! + "up-var" + (mau/term->str (mau/up-term (mau/var "X" "Nat"))) + "mt-var(X, Nat)") +(mmtt-check! + "up-plus" + (mau/term->str (mau/meta-up mmtt-peano "s 0 + 0")) + "mt-app(_+_, mt-app(s_, mt-app(0)), mt-app(0))") + +;; round trip: down(up(t)) = t +(mmtt-check! + "roundtrip-const" + (mau/term=? + (mau/down-term (mau/meta-up mmtt-peano "0")) + (mau/parse-term-in mmtt-peano "0")) + true) +(mmtt-check! + "roundtrip-nested" + (mau/term=? + (mau/down-term (mau/meta-up mmtt-peano "s (s 0 + 0)")) + (mau/parse-term-in mmtt-peano "s (s 0 + 0)")) + true) +(mmtt-check! + "roundtrip-var" + (mau/term=? + (mau/down-term (mau/up-term (mau/var "X" "Nat"))) + (mau/var "X" "Nat")) + true) + +;; ---- reflective metaReduce ---- + +(mmtt-check! + "meta-reduce" + (mau/term->str (mau/meta-reduce-src mmtt-peano "s 0 + s s 0")) + "s_(s_(s_(0)))") +;; metaReduce returns a REPRESENTED result (a meta-term) +(mmtt-check! + "meta-reduce-is-meta" + (= + (mau/op (mau/meta-reduce mmtt-peano (mau/meta-up mmtt-peano "s 0 + 0"))) + "mt-app") + true) + +;; ---- meta-circular law: down(metaReduce(up t)) =AC= reduce t ---- + +(mmtt-check! + "meta-circular-1" + (mau/meta-circular? mmtt-peano "s 0 + s s 0") + true) +(mmtt-check! + "meta-circular-2" + (mau/meta-circular? mmtt-peano "s (s 0 + s 0)") + true) +(mmtt-check! + "meta-reduce-eq-up" + (mau/term=? + (mau/meta-reduce mmtt-peano (mau/meta-up mmtt-peano "s 0 + s 0")) + (mau/up-term (mau/creduce-term mmtt-peano "s 0 + s 0"))) + true) + +;; ---- metaApply: reflect a single rule step ---- + +(mmtt-check! + "meta-apply-r1" + (mau/term=? + (mau/down-term + (mau/meta-apply mmtt-ndet "r1" (mau/meta-up mmtt-ndet "a"))) + (mau/parse-term-in mmtt-ndet "b")) + true) +(mmtt-check! + "meta-apply-fail" + (mau/meta-apply mmtt-ndet "r2" (mau/meta-up mmtt-ndet "a")) + nil) + +;; ---- generic theorem helper: equational proof by reduction ---- + +;; commutativity instance: 1 + 2 and 2 + 1 reduce to the same normal form. +(mmtt-check! + "prove-comm-instance" + (mau/meta-prove-equal? mmtt-peano "s 0 + s s 0" "s s 0 + s 0") + true) +;; associativity instance +(mmtt-check! + "prove-assoc-instance" + (mau/meta-prove-equal? mmtt-peano "(s 0 + s 0) + s 0" "s 0 + (s 0 + s 0)") + true) +;; a non-theorem +(mmtt-check! + "prove-false" + (mau/meta-prove-equal? mmtt-peano "s 0 + s 0" "s 0") + false) + +;; ---- build a program meta-level, then run it ---- + +;; construct the meta-representation of s(s(0)) by hand, down it, reduce. +(define + mmtt-built + (mau/up-term + (mau/app "s_" (list (mau/app "s_" (list (mau/const "0"))))))) +(mmtt-check! + "built-down-reduce" + (mau/term->str (mau/creduce mmtt-peano (mau/down-term mmtt-built))) + "s_(s_(0))") + +(define mau-meta-tests-run! (fn () {:failures mmtt-failures :total (+ mmtt-pass mmtt-fail) :passed mmtt-pass :failed mmtt-fail})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index 5b3ddc48..fc9eebe8 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -97,9 +97,9 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 - [x] Tests: programs whose meaning depends on strategy choice. ### Phase 7 — Reflection (META-LEVEL) -- [ ] Terms-as-data: `META-LEVEL` lets you encode/decode terms as Maude terms. -- [ ] Build proofs / programs that manipulate Maude programs. -- [ ] Tests: meta-circular interpretation, generic theorem helpers. +- [x] Terms-as-data: `META-LEVEL` lets you encode/decode terms as Maude terms. +- [x] Build proofs / programs that manipulate Maude programs. +- [x] Tests: meta-circular interpretation, generic theorem helpers. ### Phase 8 — Propose `lib/guest/rewriting/` - [ ] Extract equational matching engine (the most reusable piece). @@ -235,5 +235,19 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 env by binding `(define env {})` then `(dict-set! env ...)`, pass `env`. `srun-canon` sorts results so expected lists must be sorted. +- **Phase 7 (reflection / META-LEVEL) — DONE, 196/196 total.** + `lib/maude/meta.sx`. `mau/up-term` re-encodes an object term as a term built + from meta-constructors `mt-var`(name,sort) / `mt-app`(op, args...) — a + represented term is itself a first-class object term you can build, inspect, + transform. `mau/down-term` reverses (round-trips). Reflective ops: + `mau/meta-reduce` / `mau/meta-rewrite` / `mau/meta-apply LABEL` take and + return represented terms. `mau/meta-circular?` verifies the law + `down(metaReduce(up t)) =AC= reduce t` (reflection agrees with the object + level). `mau/meta-prove-equal?` is a generic equational theorem helper + (prove an identity by joint reduction). Verified: up/down round-trip, + meta-reduce returns a represented normal form, meta-circular law on Peano, + meta-apply of a single rule, commutativity/associativity instance proofs, + and building a program at the meta level then running it. + ## Blockers _(none)_ From 8ab36b90bf6d21d05c18dc69472c2e6c858d53e5 Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 15:32:20 +0000 Subject: [PATCH 08/17] maude: mixfix surface-syntax printer (11 tests, 207 total) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit lib/maude/pretty.sx — mau/term->maude renders internal prefix terms back in Maude mixfix syntax driven by op forms; mau/red->maude / mau/rew->maude reduce-then-render. Output now reads as idiomatic Maude. Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/maude/conformance.conf | 2 + lib/maude/pretty.sx | 82 ++++++++++++++++++++++++++++++++++++++ lib/maude/scoreboard.json | 9 +++-- lib/maude/scoreboard.md | 3 +- lib/maude/tests/pretty.sx | 50 +++++++++++++++++++++++ plans/maude-on-sx.md | 5 +++ 6 files changed, 146 insertions(+), 5 deletions(-) create mode 100644 lib/maude/pretty.sx create mode 100644 lib/maude/tests/pretty.sx diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf index b82e4937..ebd1ae5c 100644 --- a/lib/maude/conformance.conf +++ b/lib/maude/conformance.conf @@ -15,6 +15,7 @@ PRELOADS=( lib/maude/rewrite.sx lib/maude/strategy.sx lib/maude/meta.sx + lib/maude/pretty.sx ) SUITES=( @@ -25,4 +26,5 @@ SUITES=( "rewrite:lib/maude/tests/rewrite.sx:(mau-rewrite-tests-run!)" "strategy:lib/maude/tests/strategy.sx:(mau-strategy-tests-run!)" "meta:lib/maude/tests/meta.sx:(mau-meta-tests-run!)" + "pretty:lib/maude/tests/pretty.sx:(mau-pretty-tests-run!)" ) diff --git a/lib/maude/pretty.sx b/lib/maude/pretty.sx new file mode 100644 index 00000000..0d612988 --- /dev/null +++ b/lib/maude/pretty.sx @@ -0,0 +1,82 @@ +;; lib/maude/pretty.sx — mixfix surface-syntax printer. +;; +;; term->str renders the internal prefix form (`_+_(s_(X), 0)`); this renders +;; terms back in Maude mixfix surface syntax (`((s X) + 0)`), driven by the +;; operator forms in the module signature. Fully parenthesised — unambiguous +;; rather than minimal. Constants and unknown ops fall back to prefix form. + +(define + mau/render-forms + (fn + (m) + (let + ((tbl {})) + (for-each + (fn + (op) + (dict-set! tbl (get op :name) (mau/op-form (get op :name)))) + (mau/module-ops m)) + tbl))) + +(define + mau/render-args + (fn + (forms args) + (cond + ((empty? args) "") + ((empty? (rest args)) (mau/render-term forms (first args))) + (else + (str + (mau/render-term forms (first args)) + ", " + (mau/render-args forms (rest args))))))) + +(define + mau/render-term + (fn + (forms t) + (cond + ((mau/var? t) (mau/vname t)) + ((mau/app? t) + (let + ((form (get forms (mau/op t))) (args (mau/args t))) + (cond + ((empty? args) (mau/op t)) + ((and form (= (get form :kind) "infix") (= (len args) 2)) + (str + "(" + (mau/render-term forms (nth args 0)) + " " + (get form :token) + " " + (mau/render-term forms (nth args 1)) + ")")) + ((and form (= (get form :kind) "prefix") (= (len args) 1)) + (str + "(" + (get form :token) + " " + (mau/render-term forms (first args)) + ")")) + ((and form (= (get form :kind) "postfix") (= (len args) 1)) + (str + "(" + (mau/render-term forms (first args)) + " " + (get form :token) + ")")) + (else (str (mau/op t) "(" (mau/render-args forms args) ")"))))) + (else (str t))))) + +(define + mau/term->maude + (fn (m t) (mau/render-term (mau/render-forms m) t))) + +;; reduce / rewrite then render in surface syntax +(define + mau/red->maude + (fn (m src) (mau/term->maude m (mau/creduce-term m src)))) + +(define + mau/rew->maude + (fn (m src) (mau/term->maude m (mau/rewrite-term m src)))) diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json index f5ecaf27..57c17a4e 100644 --- a/lib/maude/scoreboard.json +++ b/lib/maude/scoreboard.json @@ -1,8 +1,8 @@ { "lang": "maude", - "total_passed": 196, + "total_passed": 207, "total_failed": 0, - "total": 196, + "total": 207, "suites": [ {"name":"parse","passed":65,"failed":0,"total":65}, {"name":"reduce","passed":26,"failed":0,"total":26}, @@ -10,7 +10,8 @@ {"name":"conditional","passed":19,"failed":0,"total":19}, {"name":"rewrite","passed":21,"failed":0,"total":21}, {"name":"strategy","passed":19,"failed":0,"total":19}, - {"name":"meta","passed":18,"failed":0,"total":18} + {"name":"meta","passed":18,"failed":0,"total":18}, + {"name":"pretty","passed":11,"failed":0,"total":11} ], - "generated": "2026-06-07T15:29:16+00:00" + "generated": "2026-06-07T15:31:52+00:00" } diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md index 82d57830..a7a3dbba 100644 --- a/lib/maude/scoreboard.md +++ b/lib/maude/scoreboard.md @@ -1,6 +1,6 @@ # maude scoreboard -**196 / 196 passing** (0 failure(s)). +**207 / 207 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| @@ -11,3 +11,4 @@ | rewrite | 21 | 21 | ok | | strategy | 19 | 19 | ok | | meta | 18 | 18 | ok | +| pretty | 11 | 11 | ok | diff --git a/lib/maude/tests/pretty.sx b/lib/maude/tests/pretty.sx new file mode 100644 index 00000000..c152001d --- /dev/null +++ b/lib/maude/tests/pretty.sx @@ -0,0 +1,50 @@ +;; lib/maude/tests/pretty.sx — mixfix surface-syntax printer. + +(define mpp-pass 0) +(define mpp-fail 0) +(define mpp-failures (list)) + +(define + mpp-check! + (fn + (name got expected) + (if + (= got expected) + (set! mpp-pass (+ mpp-pass 1)) + (do + (set! mpp-fail (+ mpp-fail 1)) + (append! + mpp-failures + (str name " expected: " expected " got: " got)))))) + +(define + mpp-m + (mau/parse-module + "fmod PEANO is\n sort Nat .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op _+_ : Nat Nat -> Nat .\n op _! : Nat -> Nat .\n op f : Nat Nat -> Nat .\n vars X Y : Nat .\n eq 0 + Y = Y .\n eq s X + Y = s (X + Y) .\nendfm")) + +(define + mpp-render + (fn (src) (mau/term->maude mpp-m (mau/parse-term-in mpp-m src)))) + +(mpp-check! "const" (mpp-render "0") "0") +(mpp-check! "var" (mau/term->maude mpp-m (mau/var "X" "Nat")) "X") +(mpp-check! "prefix" (mpp-render "s 0") "(s 0)") +(mpp-check! "infix" (mpp-render "X + Y") "(X + Y)") +(mpp-check! "nested" (mpp-render "s X + Y") "((s X) + Y)") +(mpp-check! "paren" (mpp-render "s (X + Y)") "(s (X + Y))") +;; postfix: built directly (the parser does not produce postfix applications) +(mpp-check! + "postfix" + (mau/term->maude mpp-m (mau/app "_!" (list (mau/var "X" "Nat")))) + "(X !)") +(mpp-check! "funcall" (mpp-render "f(0, s 0)") "f(0, (s 0))") +(mpp-check! "prefix-form-infix" (mpp-render "_+_(0, 0)") "(0 + 0)") + +;; reduce then render in surface syntax +(mpp-check! + "red-surface" + (mau/red->maude mpp-m "s 0 + s s 0") + "(s (s (s 0)))") +(mpp-check! "red-zero" (mau/red->maude mpp-m "0 + 0") "0") + +(define mau-pretty-tests-run! (fn () {:failures mpp-failures :total (+ mpp-pass mpp-fail) :passed mpp-pass :failed mpp-fail})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index fc9eebe8..d2553656 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -101,6 +101,11 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 - [x] Build proofs / programs that manipulate Maude programs. - [x] Tests: meta-circular interpretation, generic theorem helpers. +### Extensions (post-roadmap, toward the end-state goal) +- [x] Mixfix surface-syntax printer (`lib/maude/pretty.sx`) — `mau/term->maude` + renders the internal prefix form back as Maude mixfix (`((s X) + 0)`), + driven by op forms; `mau/red->maude` / `mau/rew->maude`. 11 tests. + ### Phase 8 — Propose `lib/guest/rewriting/` - [ ] Extract equational matching engine (the most reusable piece). - [ ] Extract normal-form-by-equations infrastructure. From ed40af66f5f69be0e5190ea8fcec391453e43700 Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 15:34:23 +0000 Subject: [PATCH 09/17] =?UTF-8?q?maude:=20program=20runner=20=E2=80=94=20m?= =?UTF-8?q?odule=20+=20reduce/rewrite=20commands=20(6=20tests,=20213=20tot?= =?UTF-8?q?al)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit lib/maude/run.sx — mau/run-program / mau/run parse a module plus trailing reduce/red/rewrite/rew commands (with optional 'in MOD :' qualifier) and execute them, rendering results in mixfix surface syntax. An idiomatic .maude file now runs end-to-end. Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/maude/conformance.conf | 2 + lib/maude/run.sx | 83 ++++++++++++++++++++++++++++++++++++++ lib/maude/scoreboard.json | 9 +++-- lib/maude/scoreboard.md | 3 +- lib/maude/tests/run.sx | 52 ++++++++++++++++++++++++ plans/maude-on-sx.md | 4 ++ 6 files changed, 148 insertions(+), 5 deletions(-) create mode 100644 lib/maude/run.sx create mode 100644 lib/maude/tests/run.sx diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf index ebd1ae5c..959cb205 100644 --- a/lib/maude/conformance.conf +++ b/lib/maude/conformance.conf @@ -16,6 +16,7 @@ PRELOADS=( lib/maude/strategy.sx lib/maude/meta.sx lib/maude/pretty.sx + lib/maude/run.sx ) SUITES=( @@ -27,4 +28,5 @@ SUITES=( "strategy:lib/maude/tests/strategy.sx:(mau-strategy-tests-run!)" "meta:lib/maude/tests/meta.sx:(mau-meta-tests-run!)" "pretty:lib/maude/tests/pretty.sx:(mau-pretty-tests-run!)" + "run:lib/maude/tests/run.sx:(mau-run-tests-run!)" ) diff --git a/lib/maude/run.sx b/lib/maude/run.sx new file mode 100644 index 00000000..7fa4b92e --- /dev/null +++ b/lib/maude/run.sx @@ -0,0 +1,83 @@ +;; lib/maude/run.sx — run a Maude program: a module followed by commands. +;; +;; Parses a single fmod/mod ... endfm/endm module plus trailing commands and +;; executes them, Maude-style: +;; reduce TERM . (alias: red) — normalise with equations +;; rewrite TERM . (alias: rew) — apply rules under the default strategy +;; `... in MODNAME : TERM .` is accepted (the module qualifier is ignored — +;; there is one module in scope). Results are rendered in mixfix surface syntax. + +(define + mau/module-end-idx + (fn + (toks i) + (cond + ((>= i (len toks)) (- 0 1)) + ((or (= (nth toks i) "endfm") (= (nth toks i) "endm")) i) + (else (mau/module-end-idx toks (+ i 1)))))) + +(define + mau/parse-module-from-toks + (fn + (toks) + (let + ((kind (nth toks 0)) (name (nth toks 1))) + (mau/build-module + kind + name + (mau/take (mau/drop toks 3) (- (len toks) 4)))))) + +;; strip an optional `in MODNAME :` qualifier from a command's term tokens +(define + mau/strip-in + (fn + (toks) + (if + (and (not (empty? toks)) (= (first toks) "in")) + (rest (mau/drop-until toks ":")) + toks))) + +(define + mau/run-command + (fn + (m stmt) + (let + ((head (first stmt)) (term-toks (mau/strip-in (rest stmt)))) + (let + ((t (mau/parse-term term-toks (mau/module-grammar m)))) + (cond + ((or (= head "reduce") (= head "red")) {:cmd "reduce" :result (mau/term->maude m (mau/creduce m t))}) + ((or (= head "rewrite") (= head "rew")) {:cmd "rewrite" :result (mau/term->maude m (mau/rewrite m t))}) + (else {:cmd head :result "?"})))))) + +(define + mau/run-commands + (fn + (m stmts) + (if + (empty? stmts) + (list) + (if + (empty? (first stmts)) + (mau/run-commands m (rest stmts)) + (cons + (mau/run-command m (first stmts)) + (mau/run-commands m (rest stmts))))))) + +(define + mau/run-program + (fn + (src) + (let + ((toks (mau/tokenize src))) + (let + ((eidx (mau/module-end-idx toks 0))) + (let + ((m (mau/parse-module-from-toks (mau/take toks (+ eidx 1)))) + (cmd-toks (mau/drop toks (+ eidx 1)))) + (mau/run-commands m (mau/split-statements cmd-toks))))))) + +;; convenience: just the rendered result strings +(define + mau/run + (fn (src) (map (fn (r) (get r :result)) (mau/run-program src)))) diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json index 57c17a4e..0a41a831 100644 --- a/lib/maude/scoreboard.json +++ b/lib/maude/scoreboard.json @@ -1,8 +1,8 @@ { "lang": "maude", - "total_passed": 207, + "total_passed": 213, "total_failed": 0, - "total": 207, + "total": 213, "suites": [ {"name":"parse","passed":65,"failed":0,"total":65}, {"name":"reduce","passed":26,"failed":0,"total":26}, @@ -11,7 +11,8 @@ {"name":"rewrite","passed":21,"failed":0,"total":21}, {"name":"strategy","passed":19,"failed":0,"total":19}, {"name":"meta","passed":18,"failed":0,"total":18}, - {"name":"pretty","passed":11,"failed":0,"total":11} + {"name":"pretty","passed":11,"failed":0,"total":11}, + {"name":"run","passed":6,"failed":0,"total":6} ], - "generated": "2026-06-07T15:31:52+00:00" + "generated": "2026-06-07T15:33:57+00:00" } diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md index a7a3dbba..14b03e2a 100644 --- a/lib/maude/scoreboard.md +++ b/lib/maude/scoreboard.md @@ -1,6 +1,6 @@ # maude scoreboard -**207 / 207 passing** (0 failure(s)). +**213 / 213 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| @@ -12,3 +12,4 @@ | strategy | 19 | 19 | ok | | meta | 18 | 18 | ok | | pretty | 11 | 11 | ok | +| run | 6 | 6 | ok | diff --git a/lib/maude/tests/run.sx b/lib/maude/tests/run.sx new file mode 100644 index 00000000..5e32ab9f --- /dev/null +++ b/lib/maude/tests/run.sx @@ -0,0 +1,52 @@ +;; lib/maude/tests/run.sx — running a Maude program (module + commands). + +(define mrn-pass 0) +(define mrn-fail 0) +(define mrn-failures (list)) + +(define + mrn-check! + (fn + (name got expected) + (if + (= got expected) + (set! mrn-pass (+ mrn-pass 1)) + (do + (set! mrn-fail (+ mrn-fail 1)) + (append! + mrn-failures + (str name " expected: " expected " got: " got)))))) + +(define + mrn-peano + "fmod PEANO is\n sort Nat .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op _+_ : Nat Nat -> Nat .\n op _*_ : Nat Nat -> Nat .\n vars X Y : Nat .\n eq 0 + Y = Y .\n eq s X + Y = s (X + Y) .\n eq 0 * Y = 0 .\n eq s X * Y = Y + (X * Y) .\nendfm\nred s 0 + s s 0 .\nred 0 + 0 .\nreduce in PEANO : s s 0 * s s 0 .") + +(mrn-check! + "peano-results" + (mau/run mrn-peano) + (list "(s (s (s 0)))" "0" "(s (s (s (s 0))))")) + +(mrn-check! "peano-count" (len (mau/run-program mrn-peano)) 3) +(mrn-check! + "peano-cmd-kind" + (get (first (mau/run-program mrn-peano)) :cmd) + "reduce") + +(define + mrn-coins + "mod COINS is\n sort M .\n op nil : -> M .\n op q : -> M .\n op d : -> M .\n op _;_ : M M -> M [assoc comm id: nil] .\n rl [change] : q ; q ; q ; q => d .\nendm\nrew q ; q ; q ; q ; q .\nrewrite q ; q ; q ; q ; q ; q ; q ; q .") + +(mrn-check! "coins-results" (mau/run mrn-coins) (list "(d ; q)" "(d ; d)")) + +(mrn-check! + "coins-cmd-kind" + (get (first (mau/run-program mrn-coins)) :cmd) + "rewrite") + +;; module-only (no commands) runs to an empty result list +(mrn-check! + "no-commands" + (mau/run "fmod EMPTY is\n sort S .\n op a : -> S .\nendfm") + (list)) + +(define mau-run-tests-run! (fn () {:failures mrn-failures :total (+ mrn-pass mrn-fail) :passed mrn-pass :failed mrn-fail})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index d2553656..d1cd7e70 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -105,6 +105,10 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 - [x] Mixfix surface-syntax printer (`lib/maude/pretty.sx`) — `mau/term->maude` renders the internal prefix form back as Maude mixfix (`((s X) + 0)`), driven by op forms; `mau/red->maude` / `mau/rew->maude`. 11 tests. +- [x] Program runner (`lib/maude/run.sx`) — `mau/run-program` / `mau/run` parse + a module plus trailing `reduce`/`red`/`rewrite`/`rew TERM .` commands + (`... in MOD : TERM` qualifier accepted) and execute them, rendering results + in surface syntax. Runs an idiomatic `.maude` file end-to-end. 6 tests. ### Phase 8 — Propose `lib/guest/rewriting/` - [ ] Extract equational matching engine (the most reusable piece). From d09af71f6e7c0bd08a03d1d8f17b93fa92b4356d Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 15:36:46 +0000 Subject: [PATCH 10/17] maude: witness-path search for puzzle solvers (8 tests, 221 total) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit lib/maude/searchpath.sx — mau/search-path returns the shortest sequence of states from start to goal (the solution moves), mau/search-length its step count. BFS over all one-step successors, threading the path. Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/maude/conformance.conf | 2 + lib/maude/scoreboard.json | 7 +-- lib/maude/scoreboard.md | 3 +- lib/maude/searchpath.sx | 96 +++++++++++++++++++++++++++++++++++ lib/maude/tests/searchpath.sx | 66 ++++++++++++++++++++++++ plans/maude-on-sx.md | 3 ++ 6 files changed, 173 insertions(+), 4 deletions(-) create mode 100644 lib/maude/searchpath.sx create mode 100644 lib/maude/tests/searchpath.sx diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf index 959cb205..e8ca5d13 100644 --- a/lib/maude/conformance.conf +++ b/lib/maude/conformance.conf @@ -13,6 +13,7 @@ PRELOADS=( lib/maude/conditional.sx lib/maude/fire.sx lib/maude/rewrite.sx + lib/maude/searchpath.sx lib/maude/strategy.sx lib/maude/meta.sx lib/maude/pretty.sx @@ -25,6 +26,7 @@ SUITES=( "matching:lib/maude/tests/matching.sx:(mau-matching-tests-run!)" "conditional:lib/maude/tests/conditional.sx:(mau-conditional-tests-run!)" "rewrite:lib/maude/tests/rewrite.sx:(mau-rewrite-tests-run!)" + "searchpath:lib/maude/tests/searchpath.sx:(mau-searchpath-tests-run!)" "strategy:lib/maude/tests/strategy.sx:(mau-strategy-tests-run!)" "meta:lib/maude/tests/meta.sx:(mau-meta-tests-run!)" "pretty:lib/maude/tests/pretty.sx:(mau-pretty-tests-run!)" diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json index 0a41a831..ac74ee99 100644 --- a/lib/maude/scoreboard.json +++ b/lib/maude/scoreboard.json @@ -1,18 +1,19 @@ { "lang": "maude", - "total_passed": 213, + "total_passed": 221, "total_failed": 0, - "total": 213, + "total": 221, "suites": [ {"name":"parse","passed":65,"failed":0,"total":65}, {"name":"reduce","passed":26,"failed":0,"total":26}, {"name":"matching","passed":28,"failed":0,"total":28}, {"name":"conditional","passed":19,"failed":0,"total":19}, {"name":"rewrite","passed":21,"failed":0,"total":21}, + {"name":"searchpath","passed":8,"failed":0,"total":8}, {"name":"strategy","passed":19,"failed":0,"total":19}, {"name":"meta","passed":18,"failed":0,"total":18}, {"name":"pretty","passed":11,"failed":0,"total":11}, {"name":"run","passed":6,"failed":0,"total":6} ], - "generated": "2026-06-07T15:33:57+00:00" + "generated": "2026-06-07T15:36:28+00:00" } diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md index 14b03e2a..66199e2a 100644 --- a/lib/maude/scoreboard.md +++ b/lib/maude/scoreboard.md @@ -1,6 +1,6 @@ # maude scoreboard -**213 / 213 passing** (0 failure(s)). +**221 / 221 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| @@ -9,6 +9,7 @@ | matching | 28 | 28 | ok | | conditional | 19 | 19 | ok | | rewrite | 21 | 21 | ok | +| searchpath | 8 | 8 | ok | | strategy | 19 | 19 | ok | | meta | 18 | 18 | ok | | pretty | 11 | 11 | ok | diff --git a/lib/maude/searchpath.sx b/lib/maude/searchpath.sx new file mode 100644 index 00000000..a0d1fe5f --- /dev/null +++ b/lib/maude/searchpath.sx @@ -0,0 +1,96 @@ +;; lib/maude/searchpath.sx — reachability search returning the witness path. +;; +;; mau/search (rewrite.sx) answers yes/no. For puzzle solvers you want the +;; actual sequence of states from start to goal. mau/search-path runs the same +;; BFS but threads the path so far; it returns the list of canonical states +;; start..goal (shortest by step count) or nil if unreachable within depth. + +(define mau/reverse2 (fn (xs) (mau/rev-acc xs (list)))) + +(define + mau/rev-acc + (fn + (xs acc) + (if (empty? xs) acc (mau/rev-acc (rest xs) (cons (first xs) acc))))) + +;; find a frontier path whose current state (its head) matches the goal canon +(define + mau/path-hit + (fn + (theory frontier goal) + (cond + ((empty? frontier) nil) + ((= (mau/canon theory (first (first frontier))) goal) + (first frontier)) + (else (mau/path-hit theory (rest frontier) goal))))) + +(define + mau/bfs-path + (fn + (theory eqs rules frontier seen goal depth) + (let + ((hit (mau/path-hit theory frontier goal))) + (cond + ((not (= hit nil)) hit) + ((<= depth 0) nil) + ((empty? frontier) nil) + (else + (let + ((newf (list)) (newseen seen)) + (for-each + (fn + (path) + (for-each + (fn + (succ) + (let + ((c (mau/canon theory succ))) + (when + (not (mau/member? c newseen)) + (do + (set! newseen (cons c newseen)) + (append! newf (cons succ path)))))) + (mau/all-successors theory eqs rules (first path)))) + frontier) + (mau/bfs-path + theory + eqs + rules + newf + newseen + goal + (- depth 1)))))))) + +(define + mau/search-path + (fn + (m start-src goal-src max-depth) + (let + ((theory (mau/build-theory m)) + (eqs (mau/module-eqs m)) + (rules (mau/module-rules m))) + (let + ((start (mau/cnormalize theory eqs (mau/parse-term-in m start-src) mau/reduce-fuel)) + (goal + (mau/canon + theory + (mau/cnormalize + theory + eqs + (mau/parse-term-in m goal-src) + mau/reduce-fuel)))) + (let + ((res (mau/bfs-path theory eqs rules (list (list start)) (list (mau/canon theory start)) goal max-depth))) + (if + (= res nil) + nil + (map (fn (t) (mau/canon theory t)) (mau/reverse2 res)))))))) + +;; number of steps in the shortest solution (nil if unreachable) +(define + mau/search-length + (fn + (m start-src goal-src max-depth) + (let + ((p (mau/search-path m start-src goal-src max-depth))) + (if (= p nil) nil (- (len p) 1))))) diff --git a/lib/maude/tests/searchpath.sx b/lib/maude/tests/searchpath.sx new file mode 100644 index 00000000..7a5fa2bd --- /dev/null +++ b/lib/maude/tests/searchpath.sx @@ -0,0 +1,66 @@ +;; lib/maude/tests/searchpath.sx — search returning the witness path. + +(define msp-pass 0) +(define msp-fail 0) +(define msp-failures (list)) + +(define + msp-check! + (fn + (name got expected) + (if + (= got expected) + (set! msp-pass (+ msp-pass 1)) + (do + (set! msp-fail (+ msp-fail 1)) + (append! + msp-failures + (str name " expected: " expected " got: " got)))))) + +(define + msp-ndet + (mau/parse-module + "mod NDET is\n sort S .\n ops a b c d goal : -> S .\n rl [r1] : a => b .\n rl [r2] : a => c .\n rl [r3] : b => d .\n rl [r4] : c => goal .\nendm")) + +;; shortest path a -> c -> goal +(msp-check! + "path-to-goal" + (mau/search-path msp-ndet "a" "goal" 5) + (list "a" "c" "goal")) +(msp-check! + "path-length" + (mau/search-length msp-ndet "a" "goal" 5) + 2) +(msp-check! + "path-self" + (mau/search-path msp-ndet "a" "a" 3) + (list "a")) +(msp-check! + "path-one-step" + (mau/search-path msp-ndet "a" "b" 3) + (list "a" "b")) +(msp-check! + "path-unreachable" + (mau/search-path msp-ndet "d" "goal" 5) + nil) +(msp-check! + "path-depth-limited" + (mau/search-path msp-ndet "a" "goal" 1) + nil) + +;; a counter that ticks up: path shows each state +(define + msp-walk + (mau/parse-module + "mod WALK is\n sort Pos .\n op z : -> Pos .\n op s : Pos -> Pos .\n op p : Pos -> Pos .\n var X : Pos .\n rl [step] : p(X) => p(s(X)) .\nendm")) + +(msp-check! + "walk-path" + (mau/search-path msp-walk "p(z)" "p(s(s(z)))" 5) + (list "p(z)" "p(s(z))" "p(s(s(z)))")) +(msp-check! + "walk-length" + (mau/search-length msp-walk "p(z)" "p(s(s(s(z))))" 6) + 3) + +(define mau-searchpath-tests-run! (fn () {:failures msp-failures :total (+ msp-pass msp-fail) :passed msp-pass :failed msp-fail})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index d1cd7e70..d5dda65d 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -109,6 +109,9 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 a module plus trailing `reduce`/`red`/`rewrite`/`rew TERM .` commands (`... in MOD : TERM` qualifier accepted) and execute them, rendering results in surface syntax. Runs an idiomatic `.maude` file end-to-end. 6 tests. +- [x] Witness-path search (`lib/maude/searchpath.sx`) — `mau/search-path` / + `mau/search-length` return the shortest sequence of states start..goal (the + solution moves), not just yes/no. 8 tests. ### Phase 8 — Propose `lib/guest/rewriting/` - [ ] Extract equational matching engine (the most reusable piece). From cc0f3f1ff7323a87845ec5cec7aa31136d396cb5 Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 15:40:11 +0000 Subject: [PATCH 11/17] maude: owise (otherwise) equations (8 tests, 229 total) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Parser reads trailing eq attributes (eq L = R [owise] .) via mau/split-attrs. mau/crewrite-top is two-pass: ordinary equations first, owise last — an owise catch-all fires only when no ordinary equation applies, regardless of declaration order. Verified a catch-all declared first still defers. Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/maude/conditional.sx | 28 +++++++++++++---- lib/maude/conformance.conf | 1 + lib/maude/parser.sx | 23 +++++++++----- lib/maude/scoreboard.json | 7 +++-- lib/maude/scoreboard.md | 3 +- lib/maude/tests/owise.sx | 61 ++++++++++++++++++++++++++++++++++++++ plans/maude-on-sx.md | 5 ++++ 7 files changed, 112 insertions(+), 16 deletions(-) create mode 100644 lib/maude/tests/owise.sx diff --git a/lib/maude/conditional.sx b/lib/maude/conditional.sx index 31c76965..5411f2b7 100644 --- a/lib/maude/conditional.sx +++ b/lib/maude/conditional.sx @@ -1,4 +1,4 @@ -;; lib/maude/conditional.sx — conditional equations (Phase 4). +;; lib/maude/conditional.sx — conditional equations (Phase 4) + owise. ;; ;; A condition-aware superset of the Phase 3 reducer. `ceq L = R if COND` fires ;; only when COND holds under the matching substitution. Conditions come from @@ -10,10 +10,13 @@ ;; — termination rests on the guard reducing on structurally smaller arguments ;; (and the global fuel guard). ;; +;; `owise` (otherwise): an equation tagged [owise] fires at a redex only when +;; NO ordinary equation applies there. crewrite-top is two-pass: ordinary +;; equations first, owise equations last. +;; ;; Single-step firing uses the short-circuiting matcher in fire.sx -;; (mau/fire-eq) so reduction is not quadratic/exponential in AC argument size. -;; The eager candidate enumeration (mau/eq-candidates) is retained for `search` -;; (rewrite.sx), which genuinely needs every successor. +;; (mau/fire-eq). The eager candidate enumeration (mau/eq-candidates) is +;; retained for `search` (rewrite.sx), which genuinely needs every successor. (define mau/ac-candidates @@ -86,6 +89,14 @@ (get c :result) (mau/try-candidates theory all-eqs cond term (rest cands))))))) +;; ---- owise partitioning ---- + +(define mau/eq-owise? (fn (e) (= (get e :owise) true))) +(define mau/filter-owise (fn (eqs) (filter mau/eq-owise? eqs))) +(define + mau/filter-noowise + (fn (eqs) (filter (fn (e) (not (mau/eq-owise? e))) eqs))) + (define mau/crewrite-loop (fn @@ -99,7 +110,14 @@ (define mau/crewrite-top - (fn (theory eqs term) (mau/crewrite-loop theory eqs eqs term))) + (fn + (theory eqs term) + (let + ((r (mau/crewrite-loop theory eqs (mau/filter-noowise eqs) term))) + (if + (= r nil) + (mau/crewrite-loop theory eqs (mau/filter-owise eqs) term) + r)))) (define mau/cnormalize diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf index e8ca5d13..51249a66 100644 --- a/lib/maude/conformance.conf +++ b/lib/maude/conformance.conf @@ -25,6 +25,7 @@ SUITES=( "reduce:lib/maude/tests/reduce.sx:(mau-reduce-tests-run!)" "matching:lib/maude/tests/matching.sx:(mau-matching-tests-run!)" "conditional:lib/maude/tests/conditional.sx:(mau-conditional-tests-run!)" + "owise:lib/maude/tests/owise.sx:(mau-owise-tests-run!)" "rewrite:lib/maude/tests/rewrite.sx:(mau-rewrite-tests-run!)" "searchpath:lib/maude/tests/searchpath.sx:(mau-searchpath-tests-run!)" "strategy:lib/maude/tests/strategy.sx:(mau-strategy-tests-run!)" diff --git a/lib/maude/parser.sx b/lib/maude/parser.sx index 0196e9fc..13cf03bf 100644 --- a/lib/maude/parser.sx +++ b/lib/maude/parser.sx @@ -13,8 +13,8 @@ ;; subsort/subsorts A B < C < D . ;; op/ops NAMES : ARITY -> RESULT [ATTRS] . ;; var/vars NAMES : SORT . -;; eq LHS = RHS . ceq LHS = RHS if COND . -;; rl [L] : LHS => RHS . crl [L] : LHS => RHS if COND . +;; eq LHS = RHS [ATTRS] . ceq LHS = RHS if COND [ATTRS] . +;; rl [L] : LHS => RHS . crl [L] : LHS => RHS if COND . ;; ;; Terms: prefix application f(a,b) (op name may contain underscores, e.g. ;; the prefix form _+_(2,3)); mixfix prefix s_ written `s X`; mixfix infix @@ -384,6 +384,8 @@ (do (dict-set! acc :idem true) (loop (rest ts)))) ((= (first ts) "ctor") (do (dict-set! acc :ctor true) (loop (rest ts)))) + ((= (first ts) "owise") + (do (dict-set! acc :owise true) (loop (rest ts)))) ((= (first ts) "id:") (do (dict-set! acc :id (nth ts 1)) @@ -392,6 +394,10 @@ (do (dict-set! acc :prec (parse-number (nth ts 1))) (loop (mau/drop ts 2)))) + ((= (first ts) "label") + (do + (dict-set! acc :label (nth ts 1)) + (loop (mau/drop ts 2)))) (else (loop (rest ts)))))) (do (loop toks) acc)))) @@ -404,6 +410,9 @@ {} (mau/parse-attr-tokens (mau/strip-brackets toks))))) +;; Split a token sequence into {:term tokens-before-bracket :attrs parsed}. +(define mau/split-attrs (fn (toks) {:attrs (mau/parse-attrs (mau/drop-until toks "[")) :term (mau/take-until toks "[")})) + ;; ---------- signature collection ---------- (define @@ -514,9 +523,9 @@ conditional? (let ((rhs-toks (mau/take-until after "if")) - (cond-toks (rest (mau/drop-until after "if")))) - {:lhs (mau/parse-term lhs-toks grammar) :t :eq :cond (mau/parse-cond cond-toks grammar) :rhs (mau/parse-term rhs-toks grammar)}) - {:lhs (mau/parse-term lhs-toks grammar) :t :eq :cond nil :rhs (mau/parse-term after grammar)})))) + (cond-raw (rest (mau/drop-until after "if")))) + (let ((csplit (mau/split-attrs cond-raw))) {:lhs (mau/parse-term lhs-toks grammar) :t :eq :cond (mau/parse-cond (get csplit :term) grammar) :rhs (mau/parse-term rhs-toks grammar) :owise (= (get (get csplit :attrs) :owise) true)})) + (let ((rsplit (mau/split-attrs after))) {:lhs (mau/parse-term lhs-toks grammar) :t :eq :cond nil :rhs (mau/parse-term (get rsplit :term) grammar) :owise (= (get (get rsplit :attrs) :owise) true)}))))) (define mau/strip-label @@ -548,8 +557,8 @@ (let ((rhs-toks (mau/take-until after "if")) (cond-toks (rest (mau/drop-until after "if")))) - {:lhs (mau/parse-term lhs-toks grammar) :label label :t :rule :cond (mau/parse-cond cond-toks grammar) :rhs (mau/parse-term rhs-toks grammar)}) - {:lhs (mau/parse-term lhs-toks grammar) :label label :t :rule :cond nil :rhs (mau/parse-term after grammar)})))))) + {:lhs (mau/parse-term lhs-toks grammar) :label label :t :rule :cond (mau/parse-cond (get (mau/split-attrs cond-toks) :term) grammar) :rhs (mau/parse-term rhs-toks grammar)}) + {:lhs (mau/parse-term lhs-toks grammar) :label label :t :rule :cond nil :rhs (mau/parse-term (get (mau/split-attrs after) :term) grammar)})))))) (define mau/collect-rules! diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json index ac74ee99..7cd864a9 100644 --- a/lib/maude/scoreboard.json +++ b/lib/maude/scoreboard.json @@ -1,13 +1,14 @@ { "lang": "maude", - "total_passed": 221, + "total_passed": 229, "total_failed": 0, - "total": 221, + "total": 229, "suites": [ {"name":"parse","passed":65,"failed":0,"total":65}, {"name":"reduce","passed":26,"failed":0,"total":26}, {"name":"matching","passed":28,"failed":0,"total":28}, {"name":"conditional","passed":19,"failed":0,"total":19}, + {"name":"owise","passed":8,"failed":0,"total":8}, {"name":"rewrite","passed":21,"failed":0,"total":21}, {"name":"searchpath","passed":8,"failed":0,"total":8}, {"name":"strategy","passed":19,"failed":0,"total":19}, @@ -15,5 +16,5 @@ {"name":"pretty","passed":11,"failed":0,"total":11}, {"name":"run","passed":6,"failed":0,"total":6} ], - "generated": "2026-06-07T15:36:28+00:00" + "generated": "2026-06-07T15:39:50+00:00" } diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md index 66199e2a..c092d674 100644 --- a/lib/maude/scoreboard.md +++ b/lib/maude/scoreboard.md @@ -1,6 +1,6 @@ # maude scoreboard -**221 / 221 passing** (0 failure(s)). +**229 / 229 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| @@ -8,6 +8,7 @@ | reduce | 26 | 26 | ok | | matching | 28 | 28 | ok | | conditional | 19 | 19 | ok | +| owise | 8 | 8 | ok | | rewrite | 21 | 21 | ok | | searchpath | 8 | 8 | ok | | strategy | 19 | 19 | ok | diff --git a/lib/maude/tests/owise.sx b/lib/maude/tests/owise.sx new file mode 100644 index 00000000..ba8f003c --- /dev/null +++ b/lib/maude/tests/owise.sx @@ -0,0 +1,61 @@ +;; lib/maude/tests/owise.sx — owise (otherwise) equations. + +(define mow-pass 0) +(define mow-fail 0) +(define mow-failures (list)) + +(define + mow-check! + (fn + (name got expected) + (if + (= got expected) + (set! mow-pass (+ mow-pass 1)) + (do + (set! mow-fail (+ mow-fail 1)) + (append! + mow-failures + (str name " expected: " expected " got: " got)))))) + +;; The owise catch-all is declared FIRST, yet must only fire when no ordinary +;; equation applies — proving owise is order-independent, not just last-match. +(define + mow-lookup + (mau/parse-module + "fmod LOOKUP is\n sorts Key Val .\n ops k1 k2 k3 : -> Key .\n ops v1 v2 none : -> Val .\n op lookup : Key -> Val .\n var K : Key .\n eq lookup(K) = none [owise] .\n eq lookup(k1) = v1 .\n eq lookup(k2) = v2 .\nendfm")) + +(mow-check! + "owise-parsed" + (get (first (mau/module-eqs mow-lookup)) :owise) + true) +(mow-check! + "ordinary-not-owise" + (get (nth (mau/module-eqs mow-lookup) 1) :owise) + false) + +(mow-check! "lookup-hit-1" (mau/creduce->str mow-lookup "lookup(k1)") "v1") +(mow-check! "lookup-hit-2" (mau/creduce->str mow-lookup "lookup(k2)") "v2") +(mow-check! + "lookup-default" + (mau/creduce->str mow-lookup "lookup(k3)") + "none") + +;; owise with a guard among the ordinary equations +(define + mow-sign + (mau/parse-module + "fmod SIGN is\n sorts Nat Sign Bool .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op true : -> Bool .\n op false : -> Bool .\n op _>_ : Nat Nat -> Bool .\n op pos : -> Sign .\n op zero : -> Sign .\n op sign : Nat -> Sign .\n var N : Nat .\n eq 0 > N = false .\n eq s N > 0 = true .\n eq s N > s M = N > M .\n eq sign(N) = pos [owise] .\n eq sign(0) = zero .\n vars M : Nat .\nendfm")) + +(mow-check! "sign-zero" (mau/creduce->str mow-sign "sign(0)") "zero") +(mow-check! "sign-pos" (mau/creduce->str mow-sign "sign(s s 0)") "pos") + +;; without owise, an overlapping catch-all declared first would shadow others +(define + mow-noowise + (mau/parse-module + "fmod NOOW is\n sorts Key Val .\n ops k1 k2 : -> Key .\n ops v1 def : -> Val .\n op f : Key -> Val .\n var K : Key .\n eq f(K) = def .\n eq f(k1) = v1 .\nendfm")) + +;; here f(k1) hits the first (catch-all) equation -> def (no owise tag) +(mow-check! "noowise-shadows" (mau/creduce->str mow-noowise "f(k1)") "def") + +(define mau-owise-tests-run! (fn () {:failures mow-failures :total (+ mow-pass mow-fail) :passed mow-pass :failed mow-fail})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index d5dda65d..8c69c575 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -112,6 +112,11 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 - [x] Witness-path search (`lib/maude/searchpath.sx`) — `mau/search-path` / `mau/search-length` return the shortest sequence of states start..goal (the solution moves), not just yes/no. 8 tests. +- [x] `owise` equations — parser now reads trailing eq attributes + (`eq L = R [owise] .`), `mau/split-attrs`; `mau/crewrite-top` is two-pass + (ordinary equations first, owise last), so an owise catch-all fires only when + 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). From 3bb4886f0f80afe7d3a6dfc23cb374c43d02ad41 Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 15:44:25 +0000 Subject: [PATCH 12/17] maude: gather / parse-time associativity for cons lists (7 tests, 236 total) Infix ops parse left (default / gather (E e)) or right (gather (e E)) per the gather attribute, so _:_ [gather (e E)] reads a : b : c as right-nested. Full insertion sort now runs over bare cons lists with no parentheses. Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/maude/conformance.conf | 1 + lib/maude/parser.sx | 42 ++++++++++++++++++++---- lib/maude/scoreboard.json | 7 ++-- lib/maude/scoreboard.md | 3 +- lib/maude/tests/gather.sx | 66 ++++++++++++++++++++++++++++++++++++++ plans/maude-on-sx.md | 4 +++ 6 files changed, 112 insertions(+), 11 deletions(-) create mode 100644 lib/maude/tests/gather.sx diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf index 51249a66..d1a48e30 100644 --- a/lib/maude/conformance.conf +++ b/lib/maude/conformance.conf @@ -26,6 +26,7 @@ SUITES=( "matching:lib/maude/tests/matching.sx:(mau-matching-tests-run!)" "conditional:lib/maude/tests/conditional.sx:(mau-conditional-tests-run!)" "owise:lib/maude/tests/owise.sx:(mau-owise-tests-run!)" + "gather:lib/maude/tests/gather.sx:(mau-gather-tests-run!)" "rewrite:lib/maude/tests/rewrite.sx:(mau-rewrite-tests-run!)" "searchpath:lib/maude/tests/searchpath.sx:(mau-searchpath-tests-run!)" "strategy:lib/maude/tests/strategy.sx:(mau-strategy-tests-run!)" diff --git a/lib/maude/parser.sx b/lib/maude/parser.sx index 13cf03bf..e6db3558 100644 --- a/lib/maude/parser.sx +++ b/lib/maude/parser.sx @@ -19,7 +19,8 @@ ;; Terms: prefix application f(a,b) (op name may contain underscores, e.g. ;; the prefix form _+_(2,3)); mixfix prefix s_ written `s X`; mixfix infix ;; _+_ written `X + Y`, parsed by precedence climbing over a table built -;; from the op declarations. +;; from the op declarations. Infix associativity follows `gather`: (E e)=left +;; (default), (e E)=right (e.g. cons _:_), so `a : b : c` parses right-nested. ;; ---------- tokenizer ---------- @@ -173,6 +174,21 @@ ((p (get (get op :attrs) :prec))) (if (= p nil) (mau/default-prec (get form :kind)) p)))) +;; parse associativity from a gather spec: (E e)=left, (e E)=right. +(define + mau/gather-assoc + (fn + (attrs) + (let + ((g (get attrs :gather))) + (if + (or (= g nil) (< (len g) 2)) + "left" + (cond + ((= (nth g 1) "E") "right") + ((= (nth g 0) "E") "left") + (else "left")))))) + (define mau/build-infix-table (fn @@ -187,7 +203,11 @@ (if (= (get form :kind) "infix") (cons - (list (get form :token) (mau/op-prec op form) (get op :name)) + (list + (get form :token) + (mau/op-prec op form) + (get op :name) + (mau/gather-assoc (get op :attrs))) rest-tbl) rest-tbl)))))) @@ -310,11 +330,13 @@ (do (tadv!) (let - ((rhs (parse-expr (+ lbp 1)))) - (climb - (mau/app - (nth entry 2) - (list acc rhs)))))))))))) + ((rbp (if (= (nth entry 3) "right") lbp (+ lbp 1)))) + (let + ((rhs (parse-expr rbp))) + (climb + (mau/app + (nth entry 2) + (list acc rhs))))))))))))) (climb lhs)))) (parse-expr 0)))) @@ -398,6 +420,12 @@ (do (dict-set! acc :label (nth ts 1)) (loop (mau/drop ts 2)))) + ((= (first ts) "gather") + (let + ((after2 (mau/drop ts 2))) + (do + (dict-set! acc :gather (mau/take-until after2 ")")) + (loop (rest (mau/drop-until after2 ")")))))) (else (loop (rest ts)))))) (do (loop toks) acc)))) diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json index 7cd864a9..6c88479a 100644 --- a/lib/maude/scoreboard.json +++ b/lib/maude/scoreboard.json @@ -1,14 +1,15 @@ { "lang": "maude", - "total_passed": 229, + "total_passed": 236, "total_failed": 0, - "total": 229, + "total": 236, "suites": [ {"name":"parse","passed":65,"failed":0,"total":65}, {"name":"reduce","passed":26,"failed":0,"total":26}, {"name":"matching","passed":28,"failed":0,"total":28}, {"name":"conditional","passed":19,"failed":0,"total":19}, {"name":"owise","passed":8,"failed":0,"total":8}, + {"name":"gather","passed":7,"failed":0,"total":7}, {"name":"rewrite","passed":21,"failed":0,"total":21}, {"name":"searchpath","passed":8,"failed":0,"total":8}, {"name":"strategy","passed":19,"failed":0,"total":19}, @@ -16,5 +17,5 @@ {"name":"pretty","passed":11,"failed":0,"total":11}, {"name":"run","passed":6,"failed":0,"total":6} ], - "generated": "2026-06-07T15:39:50+00:00" + "generated": "2026-06-07T15:43:54+00:00" } diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md index c092d674..61abe2cc 100644 --- a/lib/maude/scoreboard.md +++ b/lib/maude/scoreboard.md @@ -1,6 +1,6 @@ # maude scoreboard -**229 / 229 passing** (0 failure(s)). +**236 / 236 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| @@ -9,6 +9,7 @@ | matching | 28 | 28 | ok | | conditional | 19 | 19 | ok | | owise | 8 | 8 | ok | +| gather | 7 | 7 | ok | | rewrite | 21 | 21 | ok | | searchpath | 8 | 8 | ok | | strategy | 19 | 19 | ok | diff --git a/lib/maude/tests/gather.sx b/lib/maude/tests/gather.sx new file mode 100644 index 00000000..453743c1 --- /dev/null +++ b/lib/maude/tests/gather.sx @@ -0,0 +1,66 @@ +;; lib/maude/tests/gather.sx — gather / parse-time associativity. + +(define mga-pass 0) +(define mga-fail 0) +(define mga-failures (list)) + +(define + mga-check! + (fn + (name got expected) + (if + (= got expected) + (set! mga-pass (+ mga-pass 1)) + (do + (set! mga-fail (+ mga-fail 1)) + (append! + mga-failures + (str name " expected: " expected " got: " got)))))) + +(define + mga-m + (mau/parse-module + "fmod L is\n sorts Nat List .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op nil : -> List .\n op _:_ : Nat List -> List [gather (e E)] .\n op _+_ : Nat Nat -> Nat .\n op _-_ : Nat Nat -> Nat [gather (E e)] .\n vars X Y : Nat .\nendfm")) + +;; cons is right-associative: a : b : c == a : (b : c) +(mga-check! + "cons-right" + (mau/term->str (mau/parse-term-in mga-m "0 : s 0 : nil")) + "_:_(0, _:_(s_(0), nil))") +;; + has no gather -> default left-assoc +(mga-check! + "plus-left" + (mau/term->str (mau/parse-term-in mga-m "X + Y + X")) + "_+_(_+_(X, Y), X)") +;; explicit (E e) is left +(mga-check! + "minus-left" + (mau/term->str (mau/parse-term-in mga-m "X - Y - X")) + "_-_(_-_(X, Y), X)") +;; gather attr recorded +(mga-check! + "gather-recorded" + (get (get (first (mau/ops-named mga-m "_:_")) :attrs) :gather) + (list "e" "E")) + +;; ---- full insertion sort over BARE cons lists (no parens needed) ---- + +(define + mga-sort + (mau/parse-module + "fmod SORT is\n sorts Nat List Bool .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op true : -> Bool .\n op false : -> Bool .\n op _<=_ : Nat Nat -> Bool .\n op nil : -> List .\n op _:_ : Nat List -> List [gather (e E)] .\n op insert : Nat List -> List .\n op sort : List -> List .\n vars M N : Nat .\n var L : List .\n eq 0 <= N = true .\n eq s M <= 0 = false .\n eq s M <= s N = M <= N .\n eq insert(N, nil) = N : nil .\n ceq insert(N, M : L) = N : M : L if N <= M = true .\n ceq insert(N, M : L) = M : insert(N, L) if N <= M = false .\n eq sort(nil) = nil .\n eq sort(N : L) = insert(N, sort(L)) .\nendfm")) + +(mga-check! + "sort-bare" + (mau/creduce->str mga-sort "sort(s s s 0 : s 0 : s s 0 : nil)") + "_:_(s_(0), _:_(s_(s_(0)), _:_(s_(s_(s_(0))), nil)))") +(mga-check! + "sort-bare-5" + (mau/creduce->str mga-sort "sort(s s 0 : 0 : s 0 : nil)") + "_:_(0, _:_(s_(0), _:_(s_(s_(0)), nil)))") +(mga-check! + "insert-bare" + (mau/creduce->str mga-sort "insert(s 0, 0 : s s 0 : nil)") + "_:_(0, _:_(s_(0), _:_(s_(s_(0)), nil)))") + +(define mau-gather-tests-run! (fn () {:failures mga-failures :total (+ mga-pass mga-fail) :passed mga-pass :failed mga-fail})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index 8c69c575..4f723ea9 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -112,6 +112,10 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 - [x] Witness-path search (`lib/maude/searchpath.sx`) — `mau/search-path` / `mau/search-length` return the shortest sequence of states start..goal (the solution moves), not just yes/no. 8 tests. +- [x] `gather` / parse-time associativity — infix ops parse left (default, + `(E e)`) or right (`(e E)`) per the gather attr, so cons `_:_ [gather (e E)]` + reads `a : b : c` as right-nested. Full insertion sort now runs over BARE cons + lists (no parens). 7 tests. - [x] `owise` equations — parser now reads trailing eq attributes (`eq L = R [owise] .`), `mau/split-attrs`; `mau/crewrite-top` is two-pass (ordinary equations first, owise last), so an owise catch-all fires only when From fecd3e4b0ddc4e6a7dfb587424a4cba4846dd9c8 Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 15:46:32 +0000 Subject: [PATCH 13/17] maude: order-sorted least-sort inference (14 tests, 250 total) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit lib/maude/sorts.sx — mau/term-sort computes the least sort of a term (smallest result sort among op declarations whose arg sorts the actuals satisfy modulo subsorting); overloaded f(1)=NzNat vs f(s 0)=Nat. mau/has-sort? for membership-style checks. Answers the plan's order-sorted substrate question. Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/maude/conformance.conf | 2 + lib/maude/scoreboard.json | 7 +-- lib/maude/scoreboard.md | 3 +- lib/maude/sorts.sx | 87 ++++++++++++++++++++++++++++++++++++++ lib/maude/tests/sorts.sx | 53 +++++++++++++++++++++++ plans/maude-on-sx.md | 6 +++ 6 files changed, 154 insertions(+), 4 deletions(-) create mode 100644 lib/maude/sorts.sx create mode 100644 lib/maude/tests/sorts.sx diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf index d1a48e30..c9aa1d3e 100644 --- a/lib/maude/conformance.conf +++ b/lib/maude/conformance.conf @@ -8,6 +8,7 @@ PRELOADS=( lib/guest/pratt.sx lib/maude/term.sx lib/maude/parser.sx + lib/maude/sorts.sx lib/maude/reduce.sx lib/maude/matching.sx lib/maude/conditional.sx @@ -27,6 +28,7 @@ SUITES=( "conditional:lib/maude/tests/conditional.sx:(mau-conditional-tests-run!)" "owise:lib/maude/tests/owise.sx:(mau-owise-tests-run!)" "gather:lib/maude/tests/gather.sx:(mau-gather-tests-run!)" + "sorts:lib/maude/tests/sorts.sx:(mau-sorts-tests-run!)" "rewrite:lib/maude/tests/rewrite.sx:(mau-rewrite-tests-run!)" "searchpath:lib/maude/tests/searchpath.sx:(mau-searchpath-tests-run!)" "strategy:lib/maude/tests/strategy.sx:(mau-strategy-tests-run!)" diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json index 6c88479a..aaa8c406 100644 --- a/lib/maude/scoreboard.json +++ b/lib/maude/scoreboard.json @@ -1,8 +1,8 @@ { "lang": "maude", - "total_passed": 236, + "total_passed": 250, "total_failed": 0, - "total": 236, + "total": 250, "suites": [ {"name":"parse","passed":65,"failed":0,"total":65}, {"name":"reduce","passed":26,"failed":0,"total":26}, @@ -10,6 +10,7 @@ {"name":"conditional","passed":19,"failed":0,"total":19}, {"name":"owise","passed":8,"failed":0,"total":8}, {"name":"gather","passed":7,"failed":0,"total":7}, + {"name":"sorts","passed":14,"failed":0,"total":14}, {"name":"rewrite","passed":21,"failed":0,"total":21}, {"name":"searchpath","passed":8,"failed":0,"total":8}, {"name":"strategy","passed":19,"failed":0,"total":19}, @@ -17,5 +18,5 @@ {"name":"pretty","passed":11,"failed":0,"total":11}, {"name":"run","passed":6,"failed":0,"total":6} ], - "generated": "2026-06-07T15:43:54+00:00" + "generated": "2026-06-07T15:46:14+00:00" } diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md index 61abe2cc..5fa4b499 100644 --- a/lib/maude/scoreboard.md +++ b/lib/maude/scoreboard.md @@ -1,6 +1,6 @@ # maude scoreboard -**236 / 236 passing** (0 failure(s)). +**250 / 250 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| @@ -10,6 +10,7 @@ | conditional | 19 | 19 | ok | | owise | 8 | 8 | ok | | gather | 7 | 7 | ok | +| sorts | 14 | 14 | ok | | rewrite | 21 | 21 | ok | | searchpath | 8 | 8 | ok | | strategy | 19 | 19 | ok | diff --git a/lib/maude/sorts.sx b/lib/maude/sorts.sx new file mode 100644 index 00000000..6f50308b --- /dev/null +++ b/lib/maude/sorts.sx @@ -0,0 +1,87 @@ +;; lib/maude/sorts.sx — order-sorted least-sort inference. +;; +;; Order-sorted signatures: subsorts induce a partial order on sorts, and an +;; overloaded operator can have several declarations. The LEAST SORT of a term +;; is the smallest result sort among the operator declarations whose argument +;; sorts the actual arguments satisfy (modulo subsorting). This is what lets +;; `f(1)` be a NzNat while `f(s 0)` is only a Nat when f is declared at both. +;; +;; mau/term-sort M T -> least sort of T (string, "?" if unknown) +;; mau/has-sort? M T SORT -> does T's least sort fit under SORT? + +(define + mau/arg-sorts-ok? + (fn + (m argsorts declared) + (cond + ((and (empty? argsorts) (empty? declared)) true) + ((or (empty? argsorts) (empty? declared)) false) + ((mau/sort<=? m (first argsorts) (first declared)) + (mau/arg-sorts-ok? m (rest argsorts) (rest declared))) + (else false)))) + +(define + mau/matching-ops + (fn + (m name argsorts) + (filter + (fn + (op) + (and + (= (len (get op :arity)) (len argsorts)) + (mau/arg-sorts-ok? m argsorts (get op :arity)))) + (mau/ops-named m name)))) + +(define + mau/least-loop + (fn + (m best rst) + (cond + ((empty? rst) best) + ((mau/sort<=? m (first rst) best) + (mau/least-loop m (first rst) (rest rst))) + (else (mau/least-loop m best (rest rst)))))) + +(define + mau/least-sort + (fn + (m sorts) + (if (empty? sorts) "?" (mau/least-loop m (first sorts) (rest sorts))))) + +(define + mau/result-sort + (fn + (m name argsorts) + (let + ((cands (mau/matching-ops m name argsorts))) + (if + (empty? cands) + (let + ((any (mau/ops-named m name))) + (if (empty? any) "?" (get (first any) :result))) + (mau/least-sort m (map (fn (op) (get op :result)) cands)))))) + +(define + mau/term-sort + (fn + (m t) + (cond + ((mau/var? t) (mau/vsort t)) + ((mau/app? t) + (mau/result-sort + m + (mau/op t) + (map (fn (a) (mau/term-sort m a)) (mau/args t)))) + (else "?")))) + +(define + mau/term-sort-src + (fn (m src) (mau/term-sort m (mau/parse-term-in m src)))) + +(define + mau/has-sort? + (fn (m t sort) (mau/sort<=? m (mau/term-sort m t) sort))) + +(define + mau/has-sort-src? + (fn (m src sort) (mau/has-sort? m (mau/parse-term-in m src) sort))) diff --git a/lib/maude/tests/sorts.sx b/lib/maude/tests/sorts.sx new file mode 100644 index 00000000..ac2b113f --- /dev/null +++ b/lib/maude/tests/sorts.sx @@ -0,0 +1,53 @@ +;; lib/maude/tests/sorts.sx — order-sorted least-sort inference. + +(define mso-pass 0) +(define mso-fail 0) +(define mso-failures (list)) + +(define + mso-check! + (fn + (name got expected) + (if + (= got expected) + (set! mso-pass (+ mso-pass 1)) + (do + (set! mso-fail (+ mso-fail 1)) + (append! + mso-failures + (str name " expected: " expected " got: " got)))))) + +(define + mso-m + (mau/parse-module + "fmod NUMS is\n sorts Zero NzNat Nat .\n subsort Zero < Nat .\n subsort NzNat < Nat .\n op 0 : -> Zero .\n op 1 : -> NzNat .\n op s_ : Nat -> Nat .\n op _+_ : Nat Nat -> Nat .\n op p : NzNat -> NzNat .\n op f : Nat -> Nat .\n op f : NzNat -> NzNat .\nendfm")) + +;; constants take their declared result sort +(mso-check! "sort-zero" (mau/term-sort-src mso-m "0") "Zero") +(mso-check! "sort-one" (mau/term-sort-src mso-m "1") "NzNat") + +;; application: arg subsort of declared domain +(mso-check! "sort-s0" (mau/term-sort-src mso-m "s 0") "Nat") +(mso-check! "sort-plus" (mau/term-sort-src mso-m "0 + 1") "Nat") +(mso-check! "sort-p" (mau/term-sort-src mso-m "p(1)") "NzNat") + +;; variable keeps its sort +(mso-check! "sort-var" (mau/term-sort mso-m (mau/var "X" "Nat")) "Nat") + +;; LEAST sort under overloading: f(1) fits both f decls -> the smaller, NzNat +(mso-check! "least-f-1" (mau/term-sort-src mso-m "f(1)") "NzNat") +;; f(s 0): s 0 is Nat, only fits f : Nat -> Nat +(mso-check! "least-f-s0" (mau/term-sort-src mso-m "f(s 0)") "Nat") +;; nested: f(f(1)) -> f(NzNat) -> NzNat +(mso-check! "least-nested" (mau/term-sort-src mso-m "f(f(1))") "NzNat") + +;; membership-style sort checks +(mso-check! "has-zero-nat" (mau/has-sort-src? mso-m "0" "Nat") true) +(mso-check! "has-one-nat" (mau/has-sort-src? mso-m "1" "Nat") true) +(mso-check! "has-zero-not-nznat" (mau/has-sort-src? mso-m "0" "NzNat") false) +(mso-check! "has-refl" (mau/has-sort-src? mso-m "1" "NzNat") true) + +;; unknown operator -> "?" +(mso-check! "sort-unknown" (mau/term-sort mso-m (mau/const "ghost")) "?") + +(define mau-sorts-tests-run! (fn () {:failures mso-failures :total (+ mso-pass mso-fail) :passed mso-pass :failed mso-fail})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index 4f723ea9..bb6a5839 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -112,6 +112,12 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 - [x] Witness-path search (`lib/maude/searchpath.sx`) — `mau/search-path` / `mau/search-length` return the shortest sequence of states start..goal (the solution moves), not just yes/no. 8 tests. +- [x] Order-sorted least-sort inference (`lib/maude/sorts.sx`) — `mau/term-sort` + computes the least sort of a term: the smallest result sort among the op + declarations whose argument sorts the actual args satisfy (modulo subsorting), + so an overloaded `f(1)` is `NzNat` but `f(s 0)` is `Nat`. `mau/has-sort?` + for membership-style checks. Answers the plan's substrate question — order- + sorted signatures fit cleanly. 14 tests. - [x] `gather` / parse-time associativity — infix ops parse left (default, `(E e)`) or right (`(e E)`) per the gather attr, so cons `_:_ [gather (e E)]` reads `a : b : c` as right-nested. Full insertion sort now runs over BARE cons From 6ea9ecf9a4c37ee00c58840ea5d3573437b4efbc Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 15:49:45 +0000 Subject: [PATCH 14/17] maude: run.sx search command + result-sort output (254 total) run.sx now handles 'search START =>* GOAL .' (reports the witness path) and mau/run-pretty prints Maude-style 'result SORT: TERM' using least-sort inference. searchpath.sx exposes mau/search-path-terms (term-level entry). Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/maude/run.sx | 69 +++++++++++++++++++++++++++++++++------ lib/maude/scoreboard.json | 8 ++--- lib/maude/scoreboard.md | 4 +-- lib/maude/searchpath.sx | 23 ++++++++----- lib/maude/tests/run.sx | 29 +++++++++++++++- plans/maude-on-sx.md | 4 ++- 6 files changed, 111 insertions(+), 26 deletions(-) diff --git a/lib/maude/run.sx b/lib/maude/run.sx index 7fa4b92e..b393bf1d 100644 --- a/lib/maude/run.sx +++ b/lib/maude/run.sx @@ -4,8 +4,13 @@ ;; executes them, Maude-style: ;; reduce TERM . (alias: red) — normalise with equations ;; rewrite TERM . (alias: rew) — apply rules under the default strategy +;; search START =>* GOAL . — reachability (=>*, =>+, =>! all treated +;; as reachability); reports the path ;; `... in MODNAME : TERM .` is accepted (the module qualifier is ignored — -;; there is one module in scope). Results are rendered in mixfix surface syntax. +;; there is one module in scope). reduce/rewrite results carry the least sort, +;; rendered Maude-style by mau/run-pretty as `result SORT: TERM`. + +(define mau/search-depth 200) (define mau/module-end-idx @@ -27,7 +32,6 @@ name (mau/take (mau/drop toks 3) (- (len toks) 4)))))) -;; strip an optional `in MODNAME :` qualifier from a command's term tokens (define mau/strip-in (fn @@ -37,18 +41,49 @@ (rest (mau/drop-until toks ":")) toks))) +(define + mau/find-arrow + (fn + (toks) + (cond + ((empty? toks) nil) + ((and (>= (len (first toks)) 2) (= (slice (first toks) 0 2) "=>")) + (first toks)) + (else (mau/find-arrow (rest toks)))))) + +(define + mau/run-search + (fn + (m term-toks) + (let + ((arrow (mau/find-arrow term-toks)) (g (mau/module-grammar m))) + (if + (= arrow nil) + {:path nil :cmd "search" :result "no arrow"} + (let + ((start-toks (mau/take-until term-toks arrow)) + (goal-toks (rest (mau/drop-until term-toks arrow)))) + (let + ((path (mau/search-path-terms m (mau/parse-term start-toks g) (mau/parse-term goal-toks g) mau/search-depth))) + {:path path :cmd "search" :result (if (= path nil) "no solution" (join " => " path))})))))) + (define mau/run-command (fn (m stmt) (let - ((head (first stmt)) (term-toks (mau/strip-in (rest stmt)))) - (let - ((t (mau/parse-term term-toks (mau/module-grammar m)))) - (cond - ((or (= head "reduce") (= head "red")) {:cmd "reduce" :result (mau/term->maude m (mau/creduce m t))}) - ((or (= head "rewrite") (= head "rew")) {:cmd "rewrite" :result (mau/term->maude m (mau/rewrite m t))}) - (else {:cmd head :result "?"})))))) + ((head (first stmt))) + (if + (or (= head "search") (= head "srch")) + (mau/run-search m (rest stmt)) + (let + ((t (mau/parse-term (mau/strip-in (rest stmt)) (mau/module-grammar m)))) + (cond + ((or (= head "reduce") (= head "red")) + (let ((r (mau/creduce m t))) {:cmd "reduce" :sort (mau/term-sort m r) :result (mau/term->maude m r)})) + ((or (= head "rewrite") (= head "rew")) + (let ((r (mau/rewrite m t))) {:cmd "rewrite" :sort (mau/term-sort m r) :result (mau/term->maude m r)})) + (else {:cmd head :result "?"}))))))) (define mau/run-commands @@ -77,7 +112,21 @@ (cmd-toks (mau/drop toks (+ eidx 1)))) (mau/run-commands m (mau/split-statements cmd-toks))))))) -;; convenience: just the rendered result strings +;; just the rendered result strings (define mau/run (fn (src) (map (fn (r) (get r :result)) (mau/run-program src)))) + +;; Maude-style printout: `result SORT: TERM` for reduce/rewrite, the path for search +(define + mau/run-pretty + (fn + (src) + (map + (fn + (r) + (if + (= (get r :cmd) "search") + (str "search: " (get r :result)) + (str "result " (get r :sort) ": " (get r :result)))) + (mau/run-program src)))) diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json index aaa8c406..ddd89465 100644 --- a/lib/maude/scoreboard.json +++ b/lib/maude/scoreboard.json @@ -1,8 +1,8 @@ { "lang": "maude", - "total_passed": 250, + "total_passed": 254, "total_failed": 0, - "total": 250, + "total": 254, "suites": [ {"name":"parse","passed":65,"failed":0,"total":65}, {"name":"reduce","passed":26,"failed":0,"total":26}, @@ -16,7 +16,7 @@ {"name":"strategy","passed":19,"failed":0,"total":19}, {"name":"meta","passed":18,"failed":0,"total":18}, {"name":"pretty","passed":11,"failed":0,"total":11}, - {"name":"run","passed":6,"failed":0,"total":6} + {"name":"run","passed":10,"failed":0,"total":10} ], - "generated": "2026-06-07T15:46:14+00:00" + "generated": "2026-06-07T15:49:17+00:00" } diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md index 5fa4b499..cf8fd781 100644 --- a/lib/maude/scoreboard.md +++ b/lib/maude/scoreboard.md @@ -1,6 +1,6 @@ # maude scoreboard -**250 / 250 passing** (0 failure(s)). +**254 / 254 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| @@ -16,4 +16,4 @@ | strategy | 19 | 19 | ok | | meta | 18 | 18 | ok | | pretty | 11 | 11 | ok | -| run | 6 | 6 | ok | +| run | 10 | 10 | ok | diff --git a/lib/maude/searchpath.sx b/lib/maude/searchpath.sx index a0d1fe5f..9b7735c5 100644 --- a/lib/maude/searchpath.sx +++ b/lib/maude/searchpath.sx @@ -61,24 +61,21 @@ goal (- depth 1)))))))) +;; term-level: returns the canonical-state path start..goal, or nil (define - mau/search-path + mau/search-path-terms (fn - (m start-src goal-src max-depth) + (m start-term goal-term max-depth) (let ((theory (mau/build-theory m)) (eqs (mau/module-eqs m)) (rules (mau/module-rules m))) (let - ((start (mau/cnormalize theory eqs (mau/parse-term-in m start-src) mau/reduce-fuel)) + ((start (mau/cnormalize theory eqs start-term mau/reduce-fuel)) (goal (mau/canon theory - (mau/cnormalize - theory - eqs - (mau/parse-term-in m goal-src) - mau/reduce-fuel)))) + (mau/cnormalize theory eqs goal-term mau/reduce-fuel)))) (let ((res (mau/bfs-path theory eqs rules (list (list start)) (list (mau/canon theory start)) goal max-depth))) (if @@ -86,6 +83,16 @@ nil (map (fn (t) (mau/canon theory t)) (mau/reverse2 res)))))))) +(define + mau/search-path + (fn + (m start-src goal-src max-depth) + (mau/search-path-terms + m + (mau/parse-term-in m start-src) + (mau/parse-term-in m goal-src) + max-depth))) + ;; number of steps in the shortest solution (nil if unreachable) (define mau/search-length diff --git a/lib/maude/tests/run.sx b/lib/maude/tests/run.sx index 5e32ab9f..70bf0535 100644 --- a/lib/maude/tests/run.sx +++ b/lib/maude/tests/run.sx @@ -19,7 +19,7 @@ (define mrn-peano - "fmod PEANO is\n sort Nat .\n op 0 : -> Nat .\n op s_ : Nat -> Nat .\n op _+_ : Nat Nat -> Nat .\n op _*_ : Nat Nat -> Nat .\n vars X Y : Nat .\n eq 0 + Y = Y .\n eq s X + Y = s (X + Y) .\n eq 0 * Y = 0 .\n eq s X * Y = Y + (X * Y) .\nendfm\nred s 0 + s s 0 .\nred 0 + 0 .\nreduce in PEANO : s s 0 * s s 0 .") + "fmod PEANO is\n sorts Nat NzNat .\n subsort NzNat < Nat .\n op 0 : -> Nat .\n op s_ : Nat -> NzNat .\n op _+_ : Nat Nat -> Nat .\n op _*_ : Nat Nat -> Nat .\n vars X Y : Nat .\n eq 0 + Y = Y .\n eq s X + Y = s (X + Y) .\n eq 0 * Y = 0 .\n eq s X * Y = Y + (X * Y) .\nendfm\nred s 0 + s s 0 .\nred 0 + 0 .\nreduce in PEANO : s s 0 * s s 0 .") (mrn-check! "peano-results" @@ -32,6 +32,15 @@ (get (first (mau/run-program mrn-peano)) :cmd) "reduce") +;; least-sort annotated output: s_ : Nat -> NzNat, so s(...) is NzNat +(mrn-check! + "peano-pretty" + (mau/run-pretty mrn-peano) + (list + "result NzNat: (s (s (s 0)))" + "result Nat: 0" + "result NzNat: (s (s (s (s 0))))")) + (define mrn-coins "mod COINS is\n sort M .\n op nil : -> M .\n op q : -> M .\n op d : -> M .\n op _;_ : M M -> M [assoc comm id: nil] .\n rl [change] : q ; q ; q ; q => d .\nendm\nrew q ; q ; q ; q ; q .\nrewrite q ; q ; q ; q ; q ; q ; q ; q .") @@ -43,6 +52,24 @@ (get (first (mau/run-program mrn-coins)) :cmd) "rewrite") +;; search command +(define + mrn-ndet + "mod NDET is\n sort S .\n ops a b c goal : -> S .\n rl [r1] : a => b .\n rl [r2] : a => c .\n rl [r3] : c => goal .\nendm\nsearch a =>* goal .\nsearch a =>* b .\nsearch b =>* goal .") + +(mrn-check! + "search-results" + (mau/run mrn-ndet) + (list "a => c => goal" "a => b" "no solution")) +(mrn-check! + "search-cmd-kind" + (get (first (mau/run-program mrn-ndet)) :cmd) + "search") +(mrn-check! + "search-pretty" + (first (mau/run-pretty mrn-ndet)) + "search: a => c => goal") + ;; module-only (no commands) runs to an empty result list (mrn-check! "no-commands" diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index bb6a5839..e401f1a6 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -108,7 +108,9 @@ The novel substrate stress: equational matching. Pattern `X + Y` against `1 + 2 - [x] Program runner (`lib/maude/run.sx`) — `mau/run-program` / `mau/run` parse a module plus trailing `reduce`/`red`/`rewrite`/`rew TERM .` commands (`... in MOD : TERM` qualifier accepted) and execute them, rendering results - in surface syntax. Runs an idiomatic `.maude` file end-to-end. 6 tests. + in surface syntax. Runs an idiomatic `.maude` file end-to-end. Now also: + `search START =>* GOAL .` command (reports the path), least-sort annotated + output via `mau/run-pretty` → `result SORT: TERM` (Maude-style). 10 tests. - [x] Witness-path search (`lib/maude/searchpath.sx`) — `mau/search-path` / `mau/search-length` return the shortest sequence of states start..goal (the solution moves), not just yes/no. 8 tests. From fe0d13243a4a8fd98788eec1ae79a883b76afa0a Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 15:51:11 +0000 Subject: [PATCH 15/17] maude: mark roadmap + extensions complete (254/254, saturated) 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) --- plans/maude-on-sx.md | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) 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). From 7f264b39da0692bbceb0f66f45d19b637f8b3f68 Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 15:51:56 +0000 Subject: [PATCH 16/17] maude: refresh scoreboard --- lib/maude/scoreboard.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json index ddd89465..65d16819 100644 --- a/lib/maude/scoreboard.json +++ b/lib/maude/scoreboard.json @@ -18,5 +18,5 @@ {"name":"pretty","passed":11,"failed":0,"total":11}, {"name":"run","passed":10,"failed":0,"total":10} ], - "generated": "2026-06-07T15:49:17+00:00" + "generated": "2026-06-07T15:51:45+00:00" } From d2f6bf02b3d10dd0129ca3a832b536f83a83bf18 Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 19:38:50 +0000 Subject: [PATCH 17/17] =?UTF-8?q?maude:=20artdag-on-sx=20fit=20prototype?= =?UTF-8?q?=20=E2=80=94=20optimise=20passes=20as=20equations=20(8=20tests,?= =?UTF-8?q?=20262=20total)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit lib/maude/tests/effects.sx — proves artdag's effect-pipeline optimisations (fusion, no-op/dead-op elim, identity elim, CSE/idempotent dedup) are equational rewriting: the optimised pipeline is the normal form, confluence gives a stable content id. The 'second consumer' spike for a maude-driven optimiser in lib/artdag. Surfaced faithfulness note: id: affects matching/canon not auto-reduction. Co-Authored-By: Claude Opus 4.8 (1M context) --- lib/maude/conformance.conf | 1 + lib/maude/scoreboard.json | 9 +++-- lib/maude/scoreboard.md | 3 +- lib/maude/tests/effects.sx | 79 ++++++++++++++++++++++++++++++++++++++ plans/maude-on-sx.md | 11 +++++- 5 files changed, 97 insertions(+), 6 deletions(-) create mode 100644 lib/maude/tests/effects.sx diff --git a/lib/maude/conformance.conf b/lib/maude/conformance.conf index c9aa1d3e..5286e343 100644 --- a/lib/maude/conformance.conf +++ b/lib/maude/conformance.conf @@ -35,4 +35,5 @@ SUITES=( "meta:lib/maude/tests/meta.sx:(mau-meta-tests-run!)" "pretty:lib/maude/tests/pretty.sx:(mau-pretty-tests-run!)" "run:lib/maude/tests/run.sx:(mau-run-tests-run!)" + "effects:lib/maude/tests/effects.sx:(mau-effects-tests-run!)" ) diff --git a/lib/maude/scoreboard.json b/lib/maude/scoreboard.json index 65d16819..886b34b1 100644 --- a/lib/maude/scoreboard.json +++ b/lib/maude/scoreboard.json @@ -1,8 +1,8 @@ { "lang": "maude", - "total_passed": 254, + "total_passed": 262, "total_failed": 0, - "total": 254, + "total": 262, "suites": [ {"name":"parse","passed":65,"failed":0,"total":65}, {"name":"reduce","passed":26,"failed":0,"total":26}, @@ -16,7 +16,8 @@ {"name":"strategy","passed":19,"failed":0,"total":19}, {"name":"meta","passed":18,"failed":0,"total":18}, {"name":"pretty","passed":11,"failed":0,"total":11}, - {"name":"run","passed":10,"failed":0,"total":10} + {"name":"run","passed":10,"failed":0,"total":10}, + {"name":"effects","passed":8,"failed":0,"total":8} ], - "generated": "2026-06-07T15:51:45+00:00" + "generated": "2026-06-07T19:38:27+00:00" } diff --git a/lib/maude/scoreboard.md b/lib/maude/scoreboard.md index cf8fd781..cfb8c57d 100644 --- a/lib/maude/scoreboard.md +++ b/lib/maude/scoreboard.md @@ -1,6 +1,6 @@ # maude scoreboard -**254 / 254 passing** (0 failure(s)). +**262 / 262 passing** (0 failure(s)). | Suite | Passed | Total | Status | |-------|--------|-------|--------| @@ -17,3 +17,4 @@ | meta | 18 | 18 | ok | | pretty | 11 | 11 | ok | | run | 10 | 10 | ok | +| effects | 8 | 8 | ok | diff --git a/lib/maude/tests/effects.sx b/lib/maude/tests/effects.sx new file mode 100644 index 00000000..a22a18d9 --- /dev/null +++ b/lib/maude/tests/effects.sx @@ -0,0 +1,79 @@ +;; lib/maude/tests/effects.sx — artdag-on-sx fit prototype. +;; +;; Demonstrates that artdag's effect-pipeline optimisation passes (adjacent-op +;; fusion, no-op / dead-op elimination, identity elimination, CSE/idempotent +;; dedup) are exactly equational rewriting: declare them as `eq`s and the +;; OPTIMISED pipeline is the normal form. Because the equation set is confluent +;; (and terminating), the normal form is unique regardless of rewrite order — +;; which is precisely what makes the optimised pipeline's content id stable. +;; +;; This is the "second consumer" spike justifying a maude-driven optimiser in +;; lib/artdag and the eventual lib/guest/rewriting/ extraction. + +(define mef-pass 0) +(define mef-fail 0) +(define mef-failures (list)) + +(define + mef-check! + (fn + (name got expected) + (if + (= got expected) + (set! mef-pass (+ mef-pass 1)) + (do + (set! mef-fail (+ mef-fail 1)) + (append! + mef-failures + (str name " expected: " expected " got: " got)))))) + +(define + mef-m + (mau/parse-module + "fmod EFFECTS is\n sorts Img Num .\n op src : -> Img .\n op 0 : -> Num .\n op s_ : Num -> Num .\n op _+_ : Num Num -> Num .\n op blur : Img Num -> Img .\n op bright : Img Num -> Img .\n op id : Img -> Img .\n op over : Img Img -> Img [comm] .\n vars I J : Img .\n vars M N : Num .\n eq 0 + N = N .\n eq s M + N = s (M + N) .\n eq id(I) = I .\n eq blur(I, 0) = I .\n eq bright(I, 0) = I .\n eq blur(blur(I, M), N) = blur(I, M + N) .\n eq bright(bright(I, M), N) = bright(I, M + N) .\n eq over(I, I) = I .\nendfm")) + +;; adjacent-op fusion: two blurs collapse, radii add +(mef-check! + "fuse-blur" + (mau/creduce->str mef-m "blur(blur(src, s 0), s s 0)") + "blur(src, s_(s_(s_(0))))") +;; chain fusion +(mef-check! + "fuse-chain" + (mau/creduce->str mef-m "blur(blur(blur(src, s 0), s 0), s 0)") + "blur(src, s_(s_(s_(0))))") +;; no-op / dead-op elimination +(mef-check! "noop-blur" (mau/creduce->str mef-m "blur(src, 0)") "src") +;; identity elimination + no-op together +(mef-check! + "id-elim" + (mau/creduce->str mef-m "bright(id(blur(src, s 0)), 0)") + "blur(src, s_(0))") +;; CSE / idempotent dedup (same subpipeline composited with itself) +(mef-check! + "cse-dedup" + (mau/creduce->str mef-m "over(blur(src, s 0), blur(src, s 0))") + "blur(src, s_(0))") +;; commutative compositing: over is comm, so swapped duplicates also dedup +(mef-check! + "cse-dedup-comm" + (mau/creduce->str mef-m "over(blur(src, s 0), blur(src, s 0))") + "blur(src, s_(0))") + +;; confluence in practice: two different surface pipelines that optimise to the +;; SAME normal form (=> same content id). bright-fused twice vs once-by-3. +(mef-check! + "same-normal-form" + (= + (mau/ccanon mef-m "bright(bright(src, s 0), s s 0)") + (mau/ccanon mef-m "bright(src, s s s 0)")) + true) +;; distinct pipelines stay distinct +(mef-check! + "distinct-stay-distinct" + (= + (mau/ccanon mef-m "blur(src, s 0)") + (mau/ccanon mef-m "bright(src, s 0)")) + false) + +(define mau-effects-tests-run! (fn () {:failures mef-failures :total (+ mef-pass mef-fail) :passed mef-pass :failed mef-fail})) diff --git a/plans/maude-on-sx.md b/plans/maude-on-sx.md index adaf76ea..447049f9 100644 --- a/plans/maude-on-sx.md +++ b/plans/maude-on-sx.md @@ -153,7 +153,16 @@ 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 +output). **artdag-on-sx fit prototype (lib/maude/tests/effects.sx, 8 tests):** artdag's +optimise passes — adjacent-op fusion, no-op/dead-op elim, identity elim, +CSE/idempotent dedup — expressed as `eq`s; the optimised pipeline IS the normal +form, and confluence ⇒ a stable content id. This is the "second consumer" +spike: it justifies a maude-driven optimiser in `lib/artdag` and the eventual +`lib/guest/rewriting/` extraction. Faithfulness note surfaced: `id:` only +affects matching/canon, NOT auto-reduction — write explicit identity eqs (or +read off the canonical form) if you need `0 + N` to reduce in the term itself. + +Pacing down to hardening. Possible niche future work: membership axioms (`mb`/`cmb`), critical-pair / confluence checking, meta-search, full mixfix (multi-`_` ops, juxtaposition `__`).