From 6ea9ecf9a4c37ee00c58840ea5d3573437b4efbc Mon Sep 17 00:00:00 2001 From: giles Date: Sun, 7 Jun 2026 15:49:45 +0000 Subject: [PATCH] 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.