giles
6ea9ecf9a4
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Failing after 36s
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) <noreply@anthropic.com>
133 lines
3.8 KiB
Plaintext
133 lines
3.8 KiB
Plaintext
;; 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
|
|
;; 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). 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
|
|
(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))))))
|
|
|
|
(define
|
|
mau/strip-in
|
|
(fn
|
|
(toks)
|
|
(if
|
|
(and (not (empty? toks)) (= (first toks) "in"))
|
|
(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)))
|
|
(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
|
|
(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)))))))
|
|
|
|
;; 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))))
|