giles
4018671087
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 31s
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>
105 lines
3.1 KiB
Plaintext
105 lines
3.1 KiB
Plaintext
;; 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))))
|