maude: Phase 7 reflection / META-LEVEL (18 tests, 196 total)

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) <noreply@anthropic.com>

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!)"
 )

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))))

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"
 }

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 |

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}))

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)_