Meta-call predicates: forall/2, maplist/2, maplist/3, include/3, exclude/3
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Has been cancelled
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Has been cancelled
Adds pl-apply-goal helper for safe call/N goal construction (atom or compound), five solver helpers (pl-solve-forall!, pl-solve-maplist2!, pl-solve-maplist3!, pl-solve-include!, pl-solve-exclude!), five cond clauses in pl-solve!, and a new test suite (15/15 passing). Total conformance: 390/390. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
This commit is contained in:
@@ -1034,6 +1034,141 @@
|
||||
(first strs)
|
||||
(rest strs)))))
|
||||
|
||||
(define
|
||||
pl-apply-goal
|
||||
(fn
|
||||
(goal args)
|
||||
(let
|
||||
((w (pl-walk-deep goal)))
|
||||
(cond
|
||||
((pl-atom? w) (list "compound" (pl-atom-name w) args))
|
||||
((pl-compound? w)
|
||||
(list "compound" (pl-fun w) (append (pl-args w) args)))
|
||||
(else w)))))
|
||||
|
||||
(define
|
||||
pl-solve-forall!
|
||||
(fn
|
||||
(db cond-g action-g trail cut-box k)
|
||||
(let
|
||||
((mark (pl-trail-mark trail)))
|
||||
(let
|
||||
((found-counterexample (pl-solve! db cond-g trail {:cut false} (fn () (let ((mark2 (pl-trail-mark trail))) (let ((action-ok (pl-solve-once! db action-g trail))) (pl-trail-undo-to! trail mark2) (if action-ok false true)))))))
|
||||
(pl-trail-undo-to! trail mark)
|
||||
(if found-counterexample false (k))))))
|
||||
|
||||
(define
|
||||
pl-solve-maplist2!
|
||||
(fn
|
||||
(db goal lst trail k)
|
||||
(let
|
||||
((l (pl-walk-deep lst)))
|
||||
(cond
|
||||
((and (pl-atom? l) (= (pl-atom-name l) "[]")) (k))
|
||||
((and (pl-compound? l) (= (pl-fun l) "."))
|
||||
(let
|
||||
((head (first (pl-args l))) (tail (nth (pl-args l) 1)))
|
||||
(let
|
||||
((call-goal (pl-apply-goal goal (list head))))
|
||||
(if
|
||||
(pl-solve-once! db call-goal trail)
|
||||
(pl-solve-maplist2! db goal tail trail k)
|
||||
false))))
|
||||
(else false)))))
|
||||
|
||||
(define
|
||||
pl-solve-maplist3!
|
||||
(fn
|
||||
(db goal list1 list2 trail k)
|
||||
(let
|
||||
((l1 (pl-walk-deep list1)) (l2 (pl-walk-deep list2)))
|
||||
(cond
|
||||
((and (pl-atom? l1) (= (pl-atom-name l1) "[]"))
|
||||
(let
|
||||
((nil-atom (list "atom" "[]")))
|
||||
(if (pl-unify! l2 nil-atom trail) (k) false)))
|
||||
((and (pl-compound? l1) (= (pl-fun l1) "."))
|
||||
(let
|
||||
((h1 (first (pl-args l1))) (t1 (nth (pl-args l1) 1)))
|
||||
(let
|
||||
((h2-var (pl-mk-rt-var "_M")))
|
||||
(let
|
||||
((call-goal (pl-apply-goal goal (list h1 h2-var))))
|
||||
(if
|
||||
(pl-solve-once! db call-goal trail)
|
||||
(let
|
||||
((t2-var (pl-mk-rt-var "_MT")))
|
||||
(let
|
||||
((cons2 (list "compound" "." (list h2-var t2-var))))
|
||||
(if
|
||||
(pl-unify! l2 cons2 trail)
|
||||
(pl-solve-maplist3! db goal t1 t2-var trail k)
|
||||
false)))
|
||||
false)))))
|
||||
(else false)))))
|
||||
|
||||
(define
|
||||
pl-solve-include!
|
||||
(fn
|
||||
(db goal lst result trail k)
|
||||
(let
|
||||
((l (pl-walk-deep lst)))
|
||||
(cond
|
||||
((and (pl-atom? l) (= (pl-atom-name l) "[]"))
|
||||
(let
|
||||
((nil-atom (list "atom" "[]")))
|
||||
(if (pl-unify! result nil-atom trail) (k) false)))
|
||||
((and (pl-compound? l) (= (pl-fun l) "."))
|
||||
(let
|
||||
((head (first (pl-args l))) (tail (nth (pl-args l) 1)))
|
||||
(let
|
||||
((call-goal (pl-apply-goal goal (list head))))
|
||||
(let
|
||||
((included (pl-solve-once! db call-goal trail)))
|
||||
(if
|
||||
included
|
||||
(let
|
||||
((rest-var (pl-mk-rt-var "_IR")))
|
||||
(let
|
||||
((cons-res (list "compound" "." (list head rest-var))))
|
||||
(if
|
||||
(pl-unify! result cons-res trail)
|
||||
(pl-solve-include! db goal tail rest-var trail k)
|
||||
false)))
|
||||
(pl-solve-include! db goal tail result trail k))))))
|
||||
(else false)))))
|
||||
|
||||
(define
|
||||
pl-solve-exclude!
|
||||
(fn
|
||||
(db goal lst result trail k)
|
||||
(let
|
||||
((l (pl-walk-deep lst)))
|
||||
(cond
|
||||
((and (pl-atom? l) (= (pl-atom-name l) "[]"))
|
||||
(let
|
||||
((nil-atom (list "atom" "[]")))
|
||||
(if (pl-unify! result nil-atom trail) (k) false)))
|
||||
((and (pl-compound? l) (= (pl-fun l) "."))
|
||||
(let
|
||||
((head (first (pl-args l))) (tail (nth (pl-args l) 1)))
|
||||
(let
|
||||
((call-goal (pl-apply-goal goal (list head))))
|
||||
(let
|
||||
((excluded (pl-solve-once! db call-goal trail)))
|
||||
(if
|
||||
excluded
|
||||
(pl-solve-exclude! db goal tail result trail k)
|
||||
(let
|
||||
((rest-var (pl-mk-rt-var "_ER")))
|
||||
(let
|
||||
((cons-res (list "compound" "." (list head rest-var))))
|
||||
(if
|
||||
(pl-unify! result cons-res trail)
|
||||
(pl-solve-exclude! db goal tail rest-var trail k)
|
||||
false))))))))
|
||||
(else false)))))
|
||||
|
||||
(define
|
||||
pl-solve!
|
||||
(fn
|
||||
@@ -1474,22 +1609,16 @@
|
||||
k)))
|
||||
false))
|
||||
(true false))))
|
||||
|
||||
;; ==/2 — structural equality (no binding)
|
||||
((and (pl-compound? g) (= (pl-fun g) "==") (= (len (pl-args g)) 2))
|
||||
(let
|
||||
((a (pl-walk-deep (first (pl-args g))))
|
||||
(b (pl-walk-deep (nth (pl-args g) 1))))
|
||||
(if (pl-struct-eq? a b) (k) false)))
|
||||
|
||||
;; \==/2 — structural inequality
|
||||
((and (pl-compound? g) (= (pl-fun g) "\\==") (= (len (pl-args g)) 2))
|
||||
(let
|
||||
((a (pl-walk-deep (first (pl-args g))))
|
||||
(b (pl-walk-deep (nth (pl-args g) 1))))
|
||||
(if (pl-struct-eq? a b) false (k))))
|
||||
|
||||
;; flatten/2
|
||||
((and (pl-compound? g) (= (pl-fun g) "flatten") (= (len (pl-args g)) 2))
|
||||
(let
|
||||
((lst-rt (pl-walk (first (pl-args g)))))
|
||||
@@ -1503,8 +1632,6 @@
|
||||
trail
|
||||
k))
|
||||
false)))
|
||||
|
||||
;; numlist/3
|
||||
((and (pl-compound? g) (= (pl-fun g) "numlist") (= (len (pl-args g)) 3))
|
||||
(let
|
||||
((wlo (pl-walk-deep (first (pl-args g))))
|
||||
@@ -1522,12 +1649,7 @@
|
||||
trail
|
||||
k)))
|
||||
false)))
|
||||
|
||||
;; atomic_list_concat/2 — no separator
|
||||
((and
|
||||
(pl-compound? g)
|
||||
(= (pl-fun g) "atomic_list_concat")
|
||||
(= (len (pl-args g)) 2))
|
||||
((and (pl-compound? g) (= (pl-fun g) "atomic_list_concat") (= (len (pl-args g)) 2))
|
||||
(let
|
||||
((lst-rt (pl-walk (first (pl-args g)))))
|
||||
(if
|
||||
@@ -1540,12 +1662,7 @@
|
||||
trail
|
||||
k))
|
||||
false)))
|
||||
|
||||
;; atomic_list_concat/3 — with separator
|
||||
((and
|
||||
(pl-compound? g)
|
||||
(= (pl-fun g) "atomic_list_concat")
|
||||
(= (len (pl-args g)) 3))
|
||||
((and (pl-compound? g) (= (pl-fun g) "atomic_list_concat") (= (len (pl-args g)) 3))
|
||||
(let
|
||||
((lst-rt (pl-walk (first (pl-args g))))
|
||||
(sep-rt (pl-walk-deep (nth (pl-args g) 1))))
|
||||
@@ -1560,8 +1677,6 @@
|
||||
trail
|
||||
k))
|
||||
false)))
|
||||
|
||||
;; sum_list/2
|
||||
((and (pl-compound? g) (= (pl-fun g) "sum_list") (= (len (pl-args g)) 2))
|
||||
(let
|
||||
((lst-rt (pl-walk (first (pl-args g)))))
|
||||
@@ -1573,34 +1688,34 @@
|
||||
trail
|
||||
k)
|
||||
false)))
|
||||
|
||||
;; max_list/2
|
||||
((and (pl-compound? g) (= (pl-fun g) "max_list") (= (len (pl-args g)) 2))
|
||||
(let
|
||||
((lst-rt (pl-walk (first (pl-args g)))))
|
||||
(if
|
||||
(and (pl-proper-list? lst-rt) (not (and (pl-atom? lst-rt) (= (pl-atom-name lst-rt) "[]"))))
|
||||
(and
|
||||
(pl-proper-list? lst-rt)
|
||||
(not
|
||||
(and (pl-atom? lst-rt) (= (pl-atom-name lst-rt) "[]"))))
|
||||
(pl-solve-eq!
|
||||
(nth (pl-args g) 1)
|
||||
(list "num" (pl-max-list-sx lst-rt))
|
||||
trail
|
||||
k)
|
||||
false)))
|
||||
|
||||
;; min_list/2
|
||||
((and (pl-compound? g) (= (pl-fun g) "min_list") (= (len (pl-args g)) 2))
|
||||
(let
|
||||
((lst-rt (pl-walk (first (pl-args g)))))
|
||||
(if
|
||||
(and (pl-proper-list? lst-rt) (not (and (pl-atom? lst-rt) (= (pl-atom-name lst-rt) "[]"))))
|
||||
(and
|
||||
(pl-proper-list? lst-rt)
|
||||
(not
|
||||
(and (pl-atom? lst-rt) (= (pl-atom-name lst-rt) "[]"))))
|
||||
(pl-solve-eq!
|
||||
(nth (pl-args g) 1)
|
||||
(list "num" (pl-min-list-sx lst-rt))
|
||||
trail
|
||||
k)
|
||||
false)))
|
||||
|
||||
;; delete/3
|
||||
((and (pl-compound? g) (= (pl-fun g) "delete") (= (len (pl-args g)) 3))
|
||||
(let
|
||||
((lst-rt (pl-walk (first (pl-args g))))
|
||||
@@ -1615,7 +1730,34 @@
|
||||
trail
|
||||
k))
|
||||
false)))
|
||||
|
||||
((and (pl-compound? g) (= (pl-fun g) "exclude") (= (len (pl-args g)) 3))
|
||||
(let
|
||||
((exc-goal (pl-walk (first (pl-args g))))
|
||||
(exc-lst (pl-walk (nth (pl-args g) 1)))
|
||||
(exc-res (pl-walk (nth (pl-args g) 2))))
|
||||
(pl-solve-exclude! db exc-goal exc-lst exc-res trail k)))
|
||||
((and (pl-compound? g) (= (pl-fun g) "include") (= (len (pl-args g)) 3))
|
||||
(let
|
||||
((inc-goal (pl-walk (first (pl-args g))))
|
||||
(inc-lst (pl-walk (nth (pl-args g) 1)))
|
||||
(inc-res (pl-walk (nth (pl-args g) 2))))
|
||||
(pl-solve-include! db inc-goal inc-lst inc-res trail k)))
|
||||
((and (pl-compound? g) (= (pl-fun g) "maplist") (= (len (pl-args g)) 3))
|
||||
(let
|
||||
((ml-goal (pl-walk (first (pl-args g))))
|
||||
(ml-l1 (pl-walk (nth (pl-args g) 1)))
|
||||
(ml-l2 (pl-walk (nth (pl-args g) 2))))
|
||||
(pl-solve-maplist3! db ml-goal ml-l1 ml-l2 trail k)))
|
||||
((and (pl-compound? g) (= (pl-fun g) "maplist") (= (len (pl-args g)) 2))
|
||||
(let
|
||||
((ml-goal (pl-walk (first (pl-args g))))
|
||||
(ml-lst (pl-walk (nth (pl-args g) 1))))
|
||||
(pl-solve-maplist2! db ml-goal ml-lst trail k)))
|
||||
((and (pl-compound? g) (= (pl-fun g) "forall") (= (len (pl-args g)) 2))
|
||||
(let
|
||||
((cond-g (pl-walk (first (pl-args g))))
|
||||
(action-g (pl-walk (nth (pl-args g) 1))))
|
||||
(pl-solve-forall! db cond-g action-g trail cut-box k)))
|
||||
(true (pl-solve-user! db g trail cut-box k))))))
|
||||
|
||||
(define
|
||||
|
||||
Reference in New Issue
Block a user