maude: Phase 3 — equational matching modulo assoc/comm/id (28 tests, 119 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 47s
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 47s
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) <noreply@anthropic.com>
This commit is contained in:
@@ -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!)"
|
||||
)
|
||||
|
||||
565
lib/maude/matching.sx
Normal file
565
lib/maude/matching.sx
Normal file
@@ -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))))
|
||||
@@ -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"
|
||||
}
|
||||
|
||||
@@ -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 |
|
||||
|
||||
170
lib/maude/tests/matching.sx
Normal file
170
lib/maude/tests/matching.sx
Normal file
@@ -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}))
|
||||
@@ -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)_
|
||||
|
||||
Reference in New Issue
Block a user