maude: program runner — module + reduce/rewrite commands (6 tests, 213 total)

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) <noreply@anthropic.com>
2026-06-07 15:34:23 +00:00
parent 8ab36b90bf
commit ed40af66f5
6 changed files with 148 additions and 5 deletions
--- a/lib/maude/run.sx
+++ 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))))