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>
104 lines
3.0 KiB
Plaintext
104 lines
3.0 KiB
Plaintext
;; lib/maude/searchpath.sx — reachability search returning the witness path.
|
|
;;
|
|
;; mau/search (rewrite.sx) answers yes/no. For puzzle solvers you want the
|
|
;; actual sequence of states from start to goal. mau/search-path runs the same
|
|
;; BFS but threads the path so far; it returns the list of canonical states
|
|
;; start..goal (shortest by step count) or nil if unreachable within depth.
|
|
|
|
(define mau/reverse2 (fn (xs) (mau/rev-acc xs (list))))
|
|
|
|
(define
|
|
mau/rev-acc
|
|
(fn
|
|
(xs acc)
|
|
(if (empty? xs) acc (mau/rev-acc (rest xs) (cons (first xs) acc)))))
|
|
|
|
;; find a frontier path whose current state (its head) matches the goal canon
|
|
(define
|
|
mau/path-hit
|
|
(fn
|
|
(theory frontier goal)
|
|
(cond
|
|
((empty? frontier) nil)
|
|
((= (mau/canon theory (first (first frontier))) goal)
|
|
(first frontier))
|
|
(else (mau/path-hit theory (rest frontier) goal)))))
|
|
|
|
(define
|
|
mau/bfs-path
|
|
(fn
|
|
(theory eqs rules frontier seen goal depth)
|
|
(let
|
|
((hit (mau/path-hit theory frontier goal)))
|
|
(cond
|
|
((not (= hit nil)) hit)
|
|
((<= depth 0) nil)
|
|
((empty? frontier) nil)
|
|
(else
|
|
(let
|
|
((newf (list)) (newseen seen))
|
|
(for-each
|
|
(fn
|
|
(path)
|
|
(for-each
|
|
(fn
|
|
(succ)
|
|
(let
|
|
((c (mau/canon theory succ)))
|
|
(when
|
|
(not (mau/member? c newseen))
|
|
(do
|
|
(set! newseen (cons c newseen))
|
|
(append! newf (cons succ path))))))
|
|
(mau/all-successors theory eqs rules (first path))))
|
|
frontier)
|
|
(mau/bfs-path
|
|
theory
|
|
eqs
|
|
rules
|
|
newf
|
|
newseen
|
|
goal
|
|
(- depth 1))))))))
|
|
|
|
;; term-level: returns the canonical-state path start..goal, or nil
|
|
(define
|
|
mau/search-path-terms
|
|
(fn
|
|
(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 start-term mau/reduce-fuel))
|
|
(goal
|
|
(mau/canon
|
|
theory
|
|
(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
|
|
(= res nil)
|
|
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
|
|
(fn
|
|
(m start-src goal-src max-depth)
|
|
(let
|
|
((p (mau/search-path m start-src goal-src max-depth)))
|
|
(if (= p nil) nil (- (len p) 1)))))
|