ISO predicates: succ/2 + plus/3 + between/3 + length/2 + last/2 + nth0/3 + nth1/3 + max/min arith (+29 tests, 317 total)
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Has been cancelled

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This commit is contained in:
2026-04-25 10:31:28 +00:00
parent 25a4ce4a05
commit 8ee0928a3d
6 changed files with 532 additions and 10 deletions

View File

@@ -595,6 +595,95 @@
pl-cut?
(fn (t) (and (list? t) (not (empty? t)) (= (first t) "cut"))))
(define
pl-list-length
(fn
(t)
(let
((w (pl-walk t)))
(cond
((and (pl-atom? w) (= (pl-atom-name w) "[]")) 0)
((and (pl-compound? w) (= (pl-fun w) ".") (= (len (pl-args w)) 2))
(+ 1 (pl-list-length (nth (pl-args w) 1))))
(true -1)))))
(define
pl-make-list-of-vars
(fn
(n)
(cond
((= n 0) (list "atom" "[]"))
(true
(list
"compound"
"."
(list (pl-mk-rt-var "_") (pl-make-list-of-vars (- n 1))))))))
(define
pl-between-loop!
(fn
(i hi x-rt trail k)
(cond
((> i hi) false)
(true
(let
((mark (pl-trail-mark trail)))
(cond
((pl-unify! x-rt (list "num" i) trail)
(let
((r (k)))
(cond
(r true)
(true
(begin
(pl-trail-undo-to! trail mark)
(pl-between-loop! (+ i 1) hi x-rt trail k))))))
(true
(begin
(pl-trail-undo-to! trail mark)
(pl-between-loop! (+ i 1) hi x-rt trail k)))))))))
(define
pl-solve-between!
(fn
(low-rt high-rt x-rt trail k)
(let
((wl (pl-walk low-rt)) (wh (pl-walk high-rt)))
(if
(and (pl-num? wl) (pl-num? wh))
(pl-between-loop! (pl-num-val wl) (pl-num-val wh) x-rt trail k)
false))))
(define
pl-solve-last!
(fn
(list-rt elem-rt trail k)
(let
((w (pl-walk list-rt)))
(cond
((and (pl-compound? w) (= (pl-fun w) ".") (= (len (pl-args w)) 2))
(let
((tail (pl-walk (nth (pl-args w) 1))))
(cond
((and (pl-atom? tail) (= (pl-atom-name tail) "[]"))
(pl-solve-eq! elem-rt (first (pl-args w)) trail k))
(true (pl-solve-last! (nth (pl-args w) 1) elem-rt trail k)))))
(true false)))))
(define
pl-solve-nth0!
(fn
(n list-rt elem-rt trail k)
(let
((w (pl-walk list-rt)))
(cond
((and (pl-compound? w) (= (pl-fun w) ".") (= (len (pl-args w)) 2))
(cond
((= n 0) (pl-solve-eq! elem-rt (first (pl-args w)) trail k))
(true
(pl-solve-nth0! (- n 1) (nth (pl-args w) 1) elem-rt trail k))))
(true false)))))
(define
pl-list-to-prolog
(fn
@@ -1002,6 +1091,106 @@
trail
k)
false)))
((and (pl-compound? g) (= (pl-fun g) "succ") (= (len (pl-args g)) 2))
(let
((wa (pl-walk (first (pl-args g))))
(wb (pl-walk (nth (pl-args g) 1))))
(cond
((pl-num? wa)
(pl-solve-eq!
(nth (pl-args g) 1)
(list "num" (+ (pl-num-val wa) 1))
trail
k))
((pl-num? wb)
(if
(> (pl-num-val wb) 0)
(pl-solve-eq!
(first (pl-args g))
(list "num" (- (pl-num-val wb) 1))
trail
k)
false))
(true false))))
((and (pl-compound? g) (= (pl-fun g) "plus") (= (len (pl-args g)) 3))
(let
((wa (pl-walk (first (pl-args g))))
(wb (pl-walk (nth (pl-args g) 1)))
(wc (pl-walk (nth (pl-args g) 2))))
(cond
((and (pl-num? wa) (pl-num? wb))
(pl-solve-eq!
(nth (pl-args g) 2)
(list "num" (+ (pl-num-val wa) (pl-num-val wb)))
trail
k))
((and (pl-num? wa) (pl-num? wc))
(pl-solve-eq!
(nth (pl-args g) 1)
(list "num" (- (pl-num-val wc) (pl-num-val wa)))
trail
k))
((and (pl-num? wb) (pl-num? wc))
(pl-solve-eq!
(first (pl-args g))
(list "num" (- (pl-num-val wc) (pl-num-val wb)))
trail
k))
(true false))))
((and (pl-compound? g) (= (pl-fun g) "between") (= (len (pl-args g)) 3))
(pl-solve-between!
(first (pl-args g))
(nth (pl-args g) 1)
(nth (pl-args g) 2)
trail
k))
((and (pl-compound? g) (= (pl-fun g) "length") (= (len (pl-args g)) 2))
(let
((wl (pl-walk (first (pl-args g))))
(wn (pl-walk (nth (pl-args g) 1))))
(cond
((pl-proper-list? (first (pl-args g)))
(pl-solve-eq!
(nth (pl-args g) 1)
(list "num" (pl-list-length (first (pl-args g))))
trail
k))
((and (pl-var? wl) (pl-num? wn))
(if
(>= (pl-num-val wn) 0)
(pl-solve-eq!
(first (pl-args g))
(pl-make-list-of-vars (pl-num-val wn))
trail
k)
false))
(true false))))
((and (pl-compound? g) (= (pl-fun g) "last") (= (len (pl-args g)) 2))
(pl-solve-last! (first (pl-args g)) (nth (pl-args g) 1) trail k))
((and (pl-compound? g) (= (pl-fun g) "nth0") (= (len (pl-args g)) 3))
(let
((wn (pl-walk (first (pl-args g)))))
(if
(pl-num? wn)
(pl-solve-nth0!
(pl-num-val wn)
(nth (pl-args g) 1)
(nth (pl-args g) 2)
trail
k)
false)))
((and (pl-compound? g) (= (pl-fun g) "nth1") (= (len (pl-args g)) 3))
(let
((wn (pl-walk (first (pl-args g)))))
(if
(and (pl-num? wn) (> (pl-num-val wn) 0))
(pl-solve-nth0!
(- (pl-num-val wn) 1)
(nth (pl-args g) 1)
(nth (pl-args g) 2)
trail
k)
false)))
(true (pl-solve-user! db g trail cut-box k))))))
(define
@@ -1128,6 +1317,16 @@
(let
((v (pl-eval-arith (first args))))
(cond ((< v 0) (- 0 v)) (true v))))
((and (= f "max") (= (len args) 2))
(let
((va (pl-eval-arith (first args)))
(vb (pl-eval-arith (nth args 1))))
(cond ((> va vb) va) (true vb))))
((and (= f "min") (= (len args) 2))
(let
((va (pl-eval-arith (first args)))
(vb (pl-eval-arith (nth args 1))))
(cond ((< va vb) va) (true vb))))
(true 0))))
(true 0)))))