giles
8ef05514b5
Some checks failed
Test, Build, and Deploy / test-build-deploy (push) Has been cancelled
33 new tests, all 375/375 conformance tests passing. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1868 lines
56 KiB
Plaintext
1868 lines
56 KiB
Plaintext
;; lib/prolog/runtime.sx — unification, trail, and (later) solver
|
|
;;
|
|
;; Phase 2 focus: runtime terms + unification + trail.
|
|
;;
|
|
;; Term representation at runtime:
|
|
;; atom ("atom" name) -- immutable tagged list, same as parse AST
|
|
;; num ("num" n) -- likewise
|
|
;; str ("str" s) -- likewise
|
|
;; compound ("compound" fun args) -- args is a regular list of terms
|
|
;; var {:tag "var" -- MUTABLE dict; :binding = nil (unbound) or term
|
|
;; :name "X"
|
|
;; :id <int>
|
|
;; :binding <term-or-nil>}
|
|
;;
|
|
;; Parse-time ("var" name) tokens must be instantiated into runtime vars
|
|
;; before unification. Fresh renaming happens per clause resolution so
|
|
;; that two separate calls to the same clause don't share variables.
|
|
;;
|
|
;; Trail:
|
|
;; {:entries (<var> <var> ...) :len N} -- stack of vars that got bound
|
|
;; Mark = integer length of the entries list at checkpoint time.
|
|
;; trail-undo-to! pops entries pushed since the mark, nil'ing :binding.
|
|
;;
|
|
;; Occurs-check: off by default; configurable via trail :occurs-check flag.
|
|
|
|
;; ── Var id counter ─────────────────────────────────────────────────
|
|
(define pl-var-counter {:n 0})
|
|
|
|
(define
|
|
pl-fresh-id
|
|
(fn
|
|
()
|
|
(let
|
|
((n (dict-get pl-var-counter :n)))
|
|
(dict-set! pl-var-counter :n (+ n 1))
|
|
n)))
|
|
|
|
;; ── Term constructors / predicates ─────────────────────────────────
|
|
(define pl-mk-rt-var (fn (name) {:tag "var" :id (pl-fresh-id) :name name :binding nil}))
|
|
|
|
(define pl-var? (fn (t) (and (dict? t) (= (dict-get t :tag) "var"))))
|
|
|
|
(define
|
|
pl-atom?
|
|
(fn (t) (and (list? t) (not (empty? t)) (= (first t) "atom"))))
|
|
|
|
(define
|
|
pl-num?
|
|
(fn (t) (and (list? t) (not (empty? t)) (= (first t) "num"))))
|
|
|
|
(define
|
|
pl-str?
|
|
(fn (t) (and (list? t) (not (empty? t)) (= (first t) "str"))))
|
|
|
|
(define
|
|
pl-compound?
|
|
(fn (t) (and (list? t) (not (empty? t)) (= (first t) "compound"))))
|
|
|
|
(define pl-var-name (fn (v) (dict-get v :name)))
|
|
(define pl-var-id (fn (v) (dict-get v :id)))
|
|
(define pl-var-binding (fn (v) (dict-get v :binding)))
|
|
(define pl-var-bound? (fn (v) (not (nil? (dict-get v :binding)))))
|
|
|
|
(define pl-atom-name (fn (t) (nth t 1)))
|
|
(define pl-num-val (fn (t) (nth t 1)))
|
|
(define pl-str-val (fn (t) (nth t 1)))
|
|
(define pl-fun (fn (t) (nth t 1)))
|
|
(define pl-args (fn (t) (nth t 2)))
|
|
|
|
;; ── Instantiate parse AST into runtime terms ──────────────────────
|
|
;; Walk a parser AST term, replacing ("var" name) occurrences with fresh
|
|
;; runtime vars. A name->var dict is threaded so that repeated uses of
|
|
;; the same variable within a clause share the same runtime var.
|
|
;; "_" is anonymous: each occurrence gets a NEW fresh var (never shared).
|
|
|
|
(define
|
|
pl-instantiate
|
|
(fn
|
|
(ast var-env)
|
|
(cond
|
|
((pl-var? ast) ast)
|
|
((not (list? ast)) ast)
|
|
((empty? ast) ast)
|
|
((= (first ast) "var")
|
|
(let
|
|
((name (nth ast 1)))
|
|
(if
|
|
(= name "_")
|
|
(pl-mk-rt-var "_")
|
|
(if
|
|
(dict-has? var-env name)
|
|
(dict-get var-env name)
|
|
(let ((v (pl-mk-rt-var name))) (dict-set! var-env name v) v)))))
|
|
((= (first ast) "compound")
|
|
(let
|
|
((fun (nth ast 1)) (args (nth ast 2)))
|
|
(list
|
|
"compound"
|
|
fun
|
|
(map (fn (a) (pl-instantiate a var-env)) args))))
|
|
((= (first ast) "clause")
|
|
(let
|
|
((h (pl-instantiate (nth ast 1) var-env))
|
|
(b (pl-instantiate (nth ast 2) var-env)))
|
|
(list "clause" h b)))
|
|
(true ast))))
|
|
|
|
(define pl-instantiate-fresh (fn (ast) (pl-instantiate ast {})))
|
|
|
|
;; ── Walk: follow binding chain ─────────────────────────────────────
|
|
(define
|
|
pl-walk
|
|
(fn
|
|
(t)
|
|
(if
|
|
(pl-var? t)
|
|
(if (pl-var-bound? t) (pl-walk (pl-var-binding t)) t)
|
|
t)))
|
|
|
|
;; Deep-walk: recursively resolve variables inside compound terms.
|
|
(define
|
|
pl-walk-deep
|
|
(fn
|
|
(t)
|
|
(let
|
|
((w (pl-walk t)))
|
|
(if
|
|
(pl-compound? w)
|
|
(list "compound" (pl-fun w) (map pl-walk-deep (pl-args w)))
|
|
w))))
|
|
|
|
;; ── Trail ─────────────────────────────────────────────────────────
|
|
(define pl-mk-trail (fn () {:entries () :len 0 :occurs-check false}))
|
|
|
|
(define pl-trail-mark (fn (trail) (dict-get trail :len)))
|
|
|
|
(define
|
|
pl-trail-push!
|
|
(fn
|
|
(trail v)
|
|
(dict-set! trail :entries (cons v (dict-get trail :entries)))
|
|
(dict-set! trail :len (+ 1 (dict-get trail :len)))))
|
|
|
|
(define
|
|
pl-trail-undo-to!
|
|
(fn
|
|
(trail mark)
|
|
(let
|
|
loop
|
|
()
|
|
(when
|
|
(> (dict-get trail :len) mark)
|
|
(let
|
|
((entries (dict-get trail :entries)))
|
|
(let
|
|
((top (first entries)) (rest (rest entries)))
|
|
(dict-set! top :binding nil)
|
|
(dict-set! trail :entries rest)
|
|
(dict-set! trail :len (- (dict-get trail :len) 1))
|
|
(loop)))))))
|
|
|
|
;; Bind variable v to term t, recording on the trail.
|
|
(define
|
|
pl-bind!
|
|
(fn (v t trail) (dict-set! v :binding t) (pl-trail-push! trail v)))
|
|
|
|
;; ── Occurs check ──────────────────────────────────────────────────
|
|
(define
|
|
pl-occurs?
|
|
(fn
|
|
(v t)
|
|
(let
|
|
((w (pl-walk t)))
|
|
(cond
|
|
((pl-var? w) (= (pl-var-id v) (pl-var-id w)))
|
|
((pl-compound? w) (some (fn (a) (pl-occurs? v a)) (pl-args w)))
|
|
(true false)))))
|
|
|
|
;; ── Unify ─────────────────────────────────────────────────────────
|
|
;; Unify two terms, mutating trail. Returns true on success.
|
|
;; On failure, the caller must undo to a pre-unify mark.
|
|
(define
|
|
pl-unify!
|
|
(fn
|
|
(t1 t2 trail)
|
|
(let
|
|
((a (pl-walk t1)) (b (pl-walk t2)))
|
|
(cond
|
|
((and (pl-var? a) (pl-var? b) (= (pl-var-id a) (pl-var-id b)))
|
|
true)
|
|
((pl-var? a)
|
|
(if
|
|
(and (dict-get trail :occurs-check) (pl-occurs? a b))
|
|
false
|
|
(do (pl-bind! a b trail) true)))
|
|
((pl-var? b)
|
|
(if
|
|
(and (dict-get trail :occurs-check) (pl-occurs? b a))
|
|
false
|
|
(do (pl-bind! b a trail) true)))
|
|
((and (pl-atom? a) (pl-atom? b))
|
|
(= (pl-atom-name a) (pl-atom-name b)))
|
|
((and (pl-num? a) (pl-num? b)) (= (pl-num-val a) (pl-num-val b)))
|
|
((and (pl-str? a) (pl-str? b)) (= (pl-str-val a) (pl-str-val b)))
|
|
((and (pl-compound? a) (pl-compound? b))
|
|
(if
|
|
(and
|
|
(= (pl-fun a) (pl-fun b))
|
|
(= (len (pl-args a)) (len (pl-args b))))
|
|
(pl-unify-lists! (pl-args a) (pl-args b) trail)
|
|
false))
|
|
(true false)))))
|
|
|
|
(define
|
|
pl-unify-lists!
|
|
(fn
|
|
(xs ys trail)
|
|
(cond
|
|
((and (empty? xs) (empty? ys)) true)
|
|
((or (empty? xs) (empty? ys)) false)
|
|
(true
|
|
(if
|
|
(pl-unify! (first xs) (first ys) trail)
|
|
(pl-unify-lists! (rest xs) (rest ys) trail)
|
|
false)))))
|
|
|
|
;; Convenience: try-unify with auto-undo on failure.
|
|
(define
|
|
pl-try-unify!
|
|
(fn
|
|
(t1 t2 trail)
|
|
(let
|
|
((mark (pl-trail-mark trail)))
|
|
(if
|
|
(pl-unify! t1 t2 trail)
|
|
true
|
|
(do (pl-trail-undo-to! trail mark) false)))))
|
|
|
|
(define pl-mk-db (fn () {:clauses {}}))
|
|
|
|
(define
|
|
pl-head-key
|
|
(fn
|
|
(head)
|
|
(cond
|
|
((pl-compound? head) (str (pl-fun head) "/" (len (pl-args head))))
|
|
((pl-atom? head) (str (pl-atom-name head) "/0"))
|
|
(true (error "pl-head-key: invalid head")))))
|
|
|
|
(define pl-clause-key (fn (clause) (pl-head-key (nth clause 1))))
|
|
|
|
(define pl-goal-key (fn (goal) (pl-head-key goal)))
|
|
|
|
(define
|
|
pl-db-add!
|
|
(fn
|
|
(db clause)
|
|
(let
|
|
((key (pl-clause-key clause)) (table (dict-get db :clauses)))
|
|
(cond
|
|
((nil? (dict-get table key)) (dict-set! table key (list clause)))
|
|
(true (begin (append! (dict-get table key) clause) nil))))))
|
|
|
|
(define
|
|
pl-db-load!
|
|
(fn
|
|
(db program)
|
|
(cond
|
|
((empty? program) nil)
|
|
(true
|
|
(begin
|
|
(pl-db-add! db (first program))
|
|
(pl-db-load! db (rest program)))))))
|
|
|
|
(define
|
|
pl-db-lookup
|
|
(fn
|
|
(db key)
|
|
(let
|
|
((v (dict-get (dict-get db :clauses) key)))
|
|
(cond ((nil? v) (list)) (true v)))))
|
|
|
|
(define
|
|
pl-db-lookup-goal
|
|
(fn (db goal) (pl-db-lookup db (pl-goal-key goal))))
|
|
|
|
(define
|
|
pl-rt-walk-to-ast
|
|
(fn
|
|
(w)
|
|
(cond
|
|
((pl-var? w) (list "var" (str "_G" (pl-var-id w))))
|
|
((and (list? w) (not (empty? w)) (= (first w) "compound"))
|
|
(list "compound" (nth w 1) (map pl-rt-walk-to-ast (nth w 2))))
|
|
(true w))))
|
|
|
|
(define pl-rt-to-ast (fn (t) (pl-rt-walk-to-ast (pl-walk-deep t))))
|
|
|
|
(define
|
|
pl-build-clause
|
|
(fn
|
|
(ast)
|
|
(cond
|
|
((and (list? ast) (= (first ast) "compound") (= (nth ast 1) ":-") (= (len (nth ast 2)) 2))
|
|
(list "clause" (first (nth ast 2)) (nth (nth ast 2) 1)))
|
|
(true (list "clause" ast (list "atom" "true"))))))
|
|
|
|
(define
|
|
pl-db-prepend!
|
|
(fn
|
|
(db clause)
|
|
(let
|
|
((key (pl-clause-key clause)) (table (dict-get db :clauses)))
|
|
(cond
|
|
((nil? (dict-get table key)) (dict-set! table key (list clause)))
|
|
(true (dict-set! table key (cons clause (dict-get table key))))))))
|
|
|
|
(define
|
|
pl-list-without
|
|
(fn
|
|
(lst i)
|
|
(cond
|
|
((empty? lst) (list))
|
|
((= i 0) (rest lst))
|
|
(true (cons (first lst) (pl-list-without (rest lst) (- i 1)))))))
|
|
|
|
(define
|
|
pl-solve-assertz!
|
|
(fn
|
|
(db term k)
|
|
(begin (pl-db-add! db (pl-build-clause (pl-rt-to-ast term))) (k))))
|
|
|
|
(define
|
|
pl-solve-asserta!
|
|
(fn
|
|
(db term k)
|
|
(begin (pl-db-prepend! db (pl-build-clause (pl-rt-to-ast term))) (k))))
|
|
|
|
(define
|
|
pl-solve-retract!
|
|
(fn
|
|
(db term trail k)
|
|
(let
|
|
((head-runtime (cond ((and (pl-compound? term) (= (pl-fun term) ":-") (= (len (pl-args term)) 2)) (first (pl-args term))) (true term)))
|
|
(body-runtime
|
|
(cond
|
|
((and (pl-compound? term) (= (pl-fun term) ":-") (= (len (pl-args term)) 2))
|
|
(nth (pl-args term) 1))
|
|
(true (list "atom" "true")))))
|
|
(let
|
|
((wh (pl-walk head-runtime)))
|
|
(cond
|
|
((pl-var? wh) false)
|
|
(true
|
|
(let
|
|
((key (pl-head-key wh)))
|
|
(pl-retract-try-each
|
|
db
|
|
key
|
|
(pl-db-lookup db key)
|
|
head-runtime
|
|
body-runtime
|
|
0
|
|
trail
|
|
k))))))))
|
|
|
|
(define
|
|
pl-deep-copy
|
|
(fn
|
|
(t var-map)
|
|
(let
|
|
((w (pl-walk t)))
|
|
(cond
|
|
((pl-var? w)
|
|
(let
|
|
((id-key (str (pl-var-id w))))
|
|
(cond
|
|
((dict-has? var-map id-key) (dict-get var-map id-key))
|
|
(true
|
|
(let
|
|
((nv (pl-mk-rt-var (dict-get w :name))))
|
|
(begin (dict-set! var-map id-key nv) nv))))))
|
|
((pl-compound? w)
|
|
(list
|
|
"compound"
|
|
(pl-fun w)
|
|
(map (fn (a) (pl-deep-copy a var-map)) (pl-args w))))
|
|
(true w)))))
|
|
|
|
(define
|
|
pl-each-into-dict!
|
|
(fn
|
|
(terms d)
|
|
(cond
|
|
((empty? terms) nil)
|
|
(true
|
|
(begin
|
|
(dict-set! d (pl-format-term (first terms)) (first terms))
|
|
(pl-each-into-dict! (rest terms) d))))))
|
|
|
|
(define
|
|
pl-sort-uniq-terms
|
|
(fn
|
|
(terms)
|
|
(let
|
|
((kv {}))
|
|
(begin
|
|
(pl-each-into-dict! terms kv)
|
|
(let
|
|
((sorted-keys (sort (keys kv))))
|
|
(map (fn (k) (dict-get kv k)) sorted-keys))))))
|
|
|
|
(define
|
|
pl-collect-solutions
|
|
(fn
|
|
(db template-rt goal-rt trail)
|
|
(let
|
|
((box {:results (list)}) (mark (pl-trail-mark trail)))
|
|
(begin
|
|
(pl-solve!
|
|
db
|
|
goal-rt
|
|
trail
|
|
{:cut false}
|
|
(fn
|
|
()
|
|
(begin
|
|
(append!
|
|
(dict-get box :results)
|
|
(pl-deep-copy template-rt {}))
|
|
false)))
|
|
(pl-trail-undo-to! trail mark)
|
|
(dict-get box :results)))))
|
|
|
|
(define
|
|
pl-solve-findall!
|
|
(fn
|
|
(db template-rt goal-rt third-rt trail k)
|
|
(let
|
|
((items (pl-collect-solutions db template-rt goal-rt trail)))
|
|
(let
|
|
((rl (pl-mk-list-term items (pl-nil-term))))
|
|
(pl-solve-eq! third-rt rl trail k)))))
|
|
|
|
(define
|
|
pl-solve-bagof!
|
|
(fn
|
|
(db template-rt goal-rt third-rt trail k)
|
|
(let
|
|
((items (pl-collect-solutions db template-rt goal-rt trail)))
|
|
(cond
|
|
((empty? items) false)
|
|
(true
|
|
(let
|
|
((rl (pl-mk-list-term items (pl-nil-term))))
|
|
(pl-solve-eq! third-rt rl trail k)))))))
|
|
|
|
(define
|
|
pl-solve-setof!
|
|
(fn
|
|
(db template-rt goal-rt third-rt trail k)
|
|
(let
|
|
((items (pl-collect-solutions db template-rt goal-rt trail)))
|
|
(cond
|
|
((empty? items) false)
|
|
(true
|
|
(let
|
|
((sorted (pl-sort-uniq-terms items)))
|
|
(let
|
|
((rl (pl-mk-list-term sorted (pl-nil-term))))
|
|
(pl-solve-eq! third-rt rl trail k))))))))
|
|
|
|
(define
|
|
pl-solve-eq2!
|
|
(fn
|
|
(a1 b1 a2 b2 trail k)
|
|
(let
|
|
((mark (pl-trail-mark trail)))
|
|
(cond
|
|
((and (pl-unify! a1 b1 trail) (pl-unify! a2 b2 trail))
|
|
(let
|
|
((r (k)))
|
|
(cond
|
|
(r true)
|
|
(true (begin (pl-trail-undo-to! trail mark) false)))))
|
|
(true (begin (pl-trail-undo-to! trail mark) false))))))
|
|
|
|
(define
|
|
pl-make-fresh-args
|
|
(fn
|
|
(n)
|
|
(cond
|
|
((<= n 0) (list))
|
|
(true (cons (pl-mk-rt-var "_") (pl-make-fresh-args (- n 1)))))))
|
|
|
|
(define
|
|
pl-solve-functor-construct!
|
|
(fn
|
|
(term-rt name-rt arity-rt trail k)
|
|
(let
|
|
((wn (pl-walk name-rt)) (wa (pl-walk arity-rt)))
|
|
(cond
|
|
((and (pl-num? wa) (= (pl-num-val wa) 0))
|
|
(cond
|
|
((or (pl-atom? wn) (pl-num? wn))
|
|
(pl-solve-eq! term-rt wn trail k))
|
|
(true false)))
|
|
((and (pl-num? wa) (> (pl-num-val wa) 0) (pl-atom? wn))
|
|
(let
|
|
((new-args (pl-make-fresh-args (pl-num-val wa))))
|
|
(pl-solve-eq!
|
|
term-rt
|
|
(list "compound" (pl-atom-name wn) new-args)
|
|
trail
|
|
k)))
|
|
(true false)))))
|
|
|
|
(define
|
|
pl-solve-functor!
|
|
(fn
|
|
(term-rt name-rt arity-rt trail k)
|
|
(let
|
|
((wt (pl-walk term-rt)))
|
|
(cond
|
|
((pl-var? wt)
|
|
(pl-solve-functor-construct! term-rt name-rt arity-rt trail k))
|
|
((pl-atom? wt)
|
|
(pl-solve-eq2! name-rt wt arity-rt (list "num" 0) trail k))
|
|
((pl-num? wt)
|
|
(pl-solve-eq2! name-rt wt arity-rt (list "num" 0) trail k))
|
|
((pl-compound? wt)
|
|
(pl-solve-eq2!
|
|
name-rt
|
|
(list "atom" (pl-fun wt))
|
|
arity-rt
|
|
(list "num" (len (pl-args wt)))
|
|
trail
|
|
k))
|
|
(true false)))))
|
|
|
|
(define
|
|
pl-solve-arg!
|
|
(fn
|
|
(n-rt term-rt arg-rt trail k)
|
|
(let
|
|
((wn (pl-walk n-rt)) (wt (pl-walk term-rt)))
|
|
(cond
|
|
((and (pl-num? wn) (pl-compound? wt))
|
|
(let
|
|
((idx (pl-num-val wn)) (args (pl-args wt)))
|
|
(cond
|
|
((and (>= idx 1) (<= idx (len args)))
|
|
(pl-solve-eq! arg-rt (nth args (- idx 1)) trail k))
|
|
(true false))))
|
|
(true false)))))
|
|
|
|
(define
|
|
pl-retract-try-each
|
|
(fn
|
|
(db key remaining head-rt body-rt idx trail k)
|
|
(cond
|
|
((empty? remaining) false)
|
|
(true
|
|
(let
|
|
((mark (pl-trail-mark trail))
|
|
(cl (pl-instantiate-fresh (first remaining))))
|
|
(cond
|
|
((and (pl-unify! head-rt (nth cl 1) trail) (pl-unify! body-rt (nth cl 2) trail))
|
|
(begin
|
|
(let
|
|
((all (pl-db-lookup db key)))
|
|
(dict-set!
|
|
(dict-get db :clauses)
|
|
key
|
|
(pl-list-without all idx)))
|
|
(let
|
|
((r (k)))
|
|
(cond
|
|
(r true)
|
|
(true (begin (pl-trail-undo-to! trail mark) false))))))
|
|
(true
|
|
(begin
|
|
(pl-trail-undo-to! trail mark)
|
|
(pl-retract-try-each
|
|
db
|
|
key
|
|
(rest remaining)
|
|
head-rt
|
|
body-rt
|
|
(+ idx 1)
|
|
trail
|
|
k)))))))))
|
|
|
|
(define
|
|
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-ground?
|
|
(fn
|
|
(t)
|
|
(let
|
|
((w (pl-walk t)))
|
|
(cond
|
|
((pl-var? w) false)
|
|
((pl-atom? w) true)
|
|
((pl-num? w) true)
|
|
((pl-str? w) true)
|
|
((pl-compound? w)
|
|
(reduce (fn (acc a) (and acc (pl-ground? a))) true (pl-args w)))
|
|
(true false)))))
|
|
|
|
(define
|
|
pl-sort-pairs-dedup
|
|
(fn
|
|
(pairs)
|
|
(cond
|
|
((empty? pairs) (list))
|
|
((= (len pairs) 1) pairs)
|
|
((= (first (first pairs)) (first (nth pairs 1)))
|
|
(pl-sort-pairs-dedup (cons (first pairs) (rest (rest pairs)))))
|
|
(true (cons (first pairs) (pl-sort-pairs-dedup (rest pairs)))))))
|
|
|
|
(define
|
|
pl-list-to-prolog
|
|
(fn
|
|
(xs)
|
|
(if
|
|
(empty? xs)
|
|
(list "atom" "[]")
|
|
(list "compound" "." (list (first xs) (pl-list-to-prolog (rest xs)))))))
|
|
|
|
(define
|
|
pl-proper-list?
|
|
(fn
|
|
(t)
|
|
(let
|
|
((w (pl-walk t)))
|
|
(cond
|
|
((and (pl-atom? w) (= (pl-atom-name w) "[]")) true)
|
|
((and (pl-compound? w) (= (pl-fun w) ".") (= (len (pl-args w)) 2))
|
|
(pl-proper-list? (nth (pl-args w) 1)))
|
|
(true false)))))
|
|
|
|
(define
|
|
pl-prolog-list-to-sx
|
|
(fn
|
|
(t)
|
|
(let
|
|
((w (pl-walk t)))
|
|
(cond
|
|
((and (pl-atom? w) (= (pl-atom-name w) "[]")) (list))
|
|
((and (pl-compound? w) (= (pl-fun w) ".") (= (len (pl-args w)) 2))
|
|
(cons
|
|
(pl-walk (first (pl-args w)))
|
|
(pl-prolog-list-to-sx (nth (pl-args w) 1))))
|
|
(true (list))))))
|
|
|
|
(define
|
|
pl-solve-atom-concat!
|
|
(fn
|
|
(a1-rt a2-rt a3-rt trail k)
|
|
(let
|
|
((a1 (pl-walk a1-rt)) (a2 (pl-walk a2-rt)) (a3 (pl-walk a3-rt)))
|
|
(cond
|
|
((and (pl-atom? a1) (pl-atom? a2))
|
|
(pl-solve-eq!
|
|
a3-rt
|
|
(list "atom" (str (pl-atom-name a1) (pl-atom-name a2)))
|
|
trail
|
|
k))
|
|
((and (pl-atom? a3) (pl-atom? a1))
|
|
(let
|
|
((s3 (pl-atom-name a3)) (s1 (pl-atom-name a1)))
|
|
(if
|
|
(starts-with? s3 s1)
|
|
(pl-solve-eq!
|
|
a2-rt
|
|
(list "atom" (substring s3 (len s1) (len s3)))
|
|
trail
|
|
k)
|
|
false)))
|
|
((and (pl-atom? a3) (pl-atom? a2))
|
|
(let
|
|
((s3 (pl-atom-name a3)) (s2 (pl-atom-name a2)))
|
|
(if
|
|
(ends-with? s3 s2)
|
|
(pl-solve-eq!
|
|
a1-rt
|
|
(list "atom" (substring s3 0 (- (len s3) (len s2))))
|
|
trail
|
|
k)
|
|
false)))
|
|
(true false)))))
|
|
|
|
(define
|
|
pl-solve-atom-chars!
|
|
(fn
|
|
(atom-rt chars-rt trail k)
|
|
(let
|
|
((a (pl-walk atom-rt)))
|
|
(cond
|
|
((pl-atom? a)
|
|
(pl-solve-eq!
|
|
chars-rt
|
|
(pl-list-to-prolog
|
|
(map (fn (c) (list "atom" c)) (split (pl-atom-name a) "")))
|
|
trail
|
|
k))
|
|
((pl-num? a)
|
|
(pl-solve-eq!
|
|
chars-rt
|
|
(pl-list-to-prolog
|
|
(map
|
|
(fn (c) (list "atom" c))
|
|
(split (str (pl-num-val a)) "")))
|
|
trail
|
|
k))
|
|
((pl-var? a)
|
|
(if
|
|
(pl-proper-list? chars-rt)
|
|
(let
|
|
((char-terms (pl-prolog-list-to-sx chars-rt)))
|
|
(pl-solve-eq!
|
|
atom-rt
|
|
(list
|
|
"atom"
|
|
(join "" (map (fn (t) (pl-atom-name t)) char-terms)))
|
|
trail
|
|
k))
|
|
false))
|
|
(true false)))))
|
|
|
|
(define
|
|
pl-solve-atom-codes!
|
|
(fn
|
|
(atom-rt codes-rt trail k)
|
|
(let
|
|
((a (pl-walk atom-rt)))
|
|
(cond
|
|
((pl-atom? a)
|
|
(pl-solve-eq!
|
|
codes-rt
|
|
(pl-list-to-prolog
|
|
(map
|
|
(fn (c) (list "num" (char-code c)))
|
|
(split (pl-atom-name a) "")))
|
|
trail
|
|
k))
|
|
((pl-num? a)
|
|
(pl-solve-eq!
|
|
codes-rt
|
|
(pl-list-to-prolog
|
|
(map
|
|
(fn (c) (list "num" (char-code c)))
|
|
(split (str (pl-num-val a)) "")))
|
|
trail
|
|
k))
|
|
((pl-var? a)
|
|
(if
|
|
(pl-proper-list? codes-rt)
|
|
(let
|
|
((code-terms (pl-prolog-list-to-sx codes-rt)))
|
|
(pl-solve-eq!
|
|
atom-rt
|
|
(list
|
|
"atom"
|
|
(join
|
|
""
|
|
(map
|
|
(fn (t) (char-from-code (pl-num-val t)))
|
|
code-terms)))
|
|
trail
|
|
k))
|
|
false))
|
|
(true false)))))
|
|
|
|
(define
|
|
pl-solve-char-code!
|
|
(fn
|
|
(char-rt code-rt trail k)
|
|
(let
|
|
((c (pl-walk char-rt)) (n (pl-walk code-rt)))
|
|
(cond
|
|
((pl-atom? c)
|
|
(let
|
|
((s (pl-atom-name c)))
|
|
(if
|
|
(= (len s) 1)
|
|
(pl-solve-eq! code-rt (list "num" (char-code s)) trail k)
|
|
false)))
|
|
((pl-num? n)
|
|
(pl-solve-eq!
|
|
char-rt
|
|
(list "atom" (char-from-code (pl-num-val n)))
|
|
trail
|
|
k))
|
|
(true false)))))
|
|
|
|
;; ── Structural equality helper (for ==/2, \==/2, delete/3) ────────
|
|
(define
|
|
pl-struct-eq?
|
|
(fn
|
|
(a b)
|
|
(cond
|
|
((and (pl-var? a) (pl-var? b))
|
|
(= (dict-get a :id) (dict-get b :id)))
|
|
((and (pl-atom? a) (pl-atom? b))
|
|
(= (pl-atom-name a) (pl-atom-name b)))
|
|
((and (pl-num? a) (pl-num? b))
|
|
(= (pl-num-val a) (pl-num-val b)))
|
|
((and (pl-compound? a) (pl-compound? b))
|
|
(if
|
|
(and
|
|
(= (pl-fun a) (pl-fun b))
|
|
(= (len (pl-args a)) (len (pl-args b))))
|
|
(let
|
|
((all-eq true)
|
|
(i 0))
|
|
(begin
|
|
(for-each
|
|
(fn (ai)
|
|
(begin
|
|
(if
|
|
(not (pl-struct-eq? ai (nth (pl-args b) i)))
|
|
(set! all-eq false)
|
|
nil)
|
|
(set! i (+ i 1))))
|
|
(pl-args a))
|
|
all-eq))
|
|
false))
|
|
(true false))))
|
|
|
|
;; ── Flatten helper: collect all non-list leaves into SX list ───────
|
|
(define
|
|
pl-flatten-prolog
|
|
(fn
|
|
(t)
|
|
(let
|
|
((w (pl-walk-deep t)))
|
|
(cond
|
|
((and (pl-atom? w) (= (pl-atom-name w) "[]")) (list))
|
|
((and (pl-compound? w) (= (pl-fun w) ".") (= (len (pl-args w)) 2))
|
|
(let
|
|
((h (pl-walk-deep (first (pl-args w))))
|
|
(tl (nth (pl-args w) 1)))
|
|
(if
|
|
(or
|
|
(and (pl-atom? h) (= (pl-atom-name h) "[]"))
|
|
(and (pl-compound? h) (= (pl-fun h) ".")))
|
|
(append (pl-flatten-prolog h) (pl-flatten-prolog tl))
|
|
(cons h (pl-flatten-prolog tl)))))
|
|
(true (list w))))))
|
|
|
|
;; ── numlist helper: build SX list of ("num" i) for i in [lo..hi] ──
|
|
(define
|
|
pl-numlist-build
|
|
(fn
|
|
(lo hi)
|
|
(if
|
|
(> lo hi)
|
|
(list)
|
|
(cons (list "num" lo) (pl-numlist-build (+ lo 1) hi)))))
|
|
|
|
;; ── atomic_list_concat helper: collect atom names / num vals ───────
|
|
(define
|
|
pl-atomic-list-collect
|
|
(fn
|
|
(prolog-list)
|
|
(let
|
|
((items (pl-prolog-list-to-sx prolog-list)))
|
|
(map
|
|
(fn (item)
|
|
(let
|
|
((w (pl-walk-deep item)))
|
|
(cond
|
|
((pl-atom? w) (pl-atom-name w))
|
|
((pl-num? w) (str (pl-num-val w)))
|
|
(true ""))))
|
|
items))))
|
|
|
|
;; ── sum_list helper ────────────────────────────────────────────────
|
|
(define
|
|
pl-sum-list-sx
|
|
(fn
|
|
(prolog-list)
|
|
(let
|
|
((items (pl-prolog-list-to-sx prolog-list)))
|
|
(reduce
|
|
(fn (acc item)
|
|
(+ acc (pl-num-val (pl-walk-deep item))))
|
|
0
|
|
items))))
|
|
|
|
;; ── max_list / min_list helpers ────────────────────────────────────
|
|
(define
|
|
pl-max-list-sx
|
|
(fn
|
|
(prolog-list)
|
|
(let
|
|
((items (pl-prolog-list-to-sx prolog-list)))
|
|
(reduce
|
|
(fn (acc item)
|
|
(let ((v (pl-num-val (pl-walk-deep item))))
|
|
(if (> v acc) v acc)))
|
|
(pl-num-val (pl-walk-deep (first items)))
|
|
(rest items)))))
|
|
|
|
(define
|
|
pl-min-list-sx
|
|
(fn
|
|
(prolog-list)
|
|
(let
|
|
((items (pl-prolog-list-to-sx prolog-list)))
|
|
(reduce
|
|
(fn (acc item)
|
|
(let ((v (pl-num-val (pl-walk-deep item))))
|
|
(if (< v acc) v acc)))
|
|
(pl-num-val (pl-walk-deep (first items)))
|
|
(rest items)))))
|
|
|
|
;; ── delete/3 helper: remove elements struct-equal to elem ──────────
|
|
(define
|
|
pl-delete-sx
|
|
(fn
|
|
(prolog-list elem)
|
|
(let
|
|
((items (pl-prolog-list-to-sx prolog-list))
|
|
(ew (pl-walk-deep elem)))
|
|
(filter
|
|
(fn (item)
|
|
(not (pl-struct-eq? (pl-walk-deep item) ew)))
|
|
items))))
|
|
|
|
;; ── join string list with separator ────────────────────────────────
|
|
(define
|
|
pl-join-strings
|
|
(fn
|
|
(strs sep)
|
|
(if
|
|
(empty? strs)
|
|
""
|
|
(reduce
|
|
(fn (acc s) (str acc sep s))
|
|
(first strs)
|
|
(rest strs)))))
|
|
|
|
(define
|
|
pl-solve!
|
|
(fn
|
|
(db goal trail cut-box k)
|
|
(let
|
|
((g (pl-walk goal)))
|
|
(cond
|
|
((pl-var? g) false)
|
|
((pl-cut? g) (begin (dict-set! cut-box :cut true) (k)))
|
|
((and (pl-atom? g) (= (pl-atom-name g) "true")) (k))
|
|
((and (pl-atom? g) (= (pl-atom-name g) "fail")) false)
|
|
((and (pl-atom? g) (= (pl-atom-name g) "nl"))
|
|
(begin (pl-output-write! "\n") (k)))
|
|
((and (pl-compound? g) (= (pl-fun g) "=") (= (len (pl-args g)) 2))
|
|
(pl-solve-eq! (first (pl-args g)) (nth (pl-args g) 1) trail k))
|
|
((and (pl-compound? g) (= (pl-fun g) "\\=") (= (len (pl-args g)) 2))
|
|
(pl-solve-not-eq!
|
|
(first (pl-args g))
|
|
(nth (pl-args g) 1)
|
|
trail
|
|
k))
|
|
((and (pl-compound? g) (= (pl-fun g) "is") (= (len (pl-args g)) 2))
|
|
(pl-solve-eq!
|
|
(first (pl-args g))
|
|
(list "num" (pl-eval-arith (nth (pl-args g) 1)))
|
|
trail
|
|
k))
|
|
((and (pl-compound? g) (= (pl-fun g) "<") (= (len (pl-args g)) 2))
|
|
(cond
|
|
((< (pl-eval-arith (first (pl-args g))) (pl-eval-arith (nth (pl-args g) 1)))
|
|
(k))
|
|
(true false)))
|
|
((and (pl-compound? g) (= (pl-fun g) ">") (= (len (pl-args g)) 2))
|
|
(cond
|
|
((> (pl-eval-arith (first (pl-args g))) (pl-eval-arith (nth (pl-args g) 1)))
|
|
(k))
|
|
(true false)))
|
|
((and (pl-compound? g) (= (pl-fun g) "=<") (= (len (pl-args g)) 2))
|
|
(cond
|
|
((<= (pl-eval-arith (first (pl-args g))) (pl-eval-arith (nth (pl-args g) 1)))
|
|
(k))
|
|
(true false)))
|
|
((and (pl-compound? g) (= (pl-fun g) ">=") (= (len (pl-args g)) 2))
|
|
(cond
|
|
((>= (pl-eval-arith (first (pl-args g))) (pl-eval-arith (nth (pl-args g) 1)))
|
|
(k))
|
|
(true false)))
|
|
((and (pl-compound? g) (= (pl-fun g) ",") (= (len (pl-args g)) 2))
|
|
(pl-solve!
|
|
db
|
|
(first (pl-args g))
|
|
trail
|
|
cut-box
|
|
(fn () (pl-solve! db (nth (pl-args g) 1) trail cut-box k))))
|
|
((and (pl-compound? g) (= (pl-fun g) ";") (= (len (pl-args g)) 2))
|
|
(pl-solve-or!
|
|
db
|
|
(first (pl-args g))
|
|
(nth (pl-args g) 1)
|
|
trail
|
|
cut-box
|
|
k))
|
|
((and (pl-compound? g) (= (pl-fun g) "->") (= (len (pl-args g)) 2))
|
|
(pl-solve-if-then-else!
|
|
db
|
|
(first (pl-args g))
|
|
(nth (pl-args g) 1)
|
|
(list "atom" "fail")
|
|
trail
|
|
cut-box
|
|
k))
|
|
((and (pl-compound? g) (= (pl-fun g) "call") (= (len (pl-args g)) 1))
|
|
(let
|
|
((call-cb {:cut false}))
|
|
(pl-solve! db (first (pl-args g)) trail call-cb k)))
|
|
((and (pl-compound? g) (= (pl-fun g) "write") (= (len (pl-args g)) 1))
|
|
(begin
|
|
(pl-output-write! (pl-format-term (first (pl-args g))))
|
|
(k)))
|
|
((and (pl-compound? g) (= (pl-fun g) "assertz") (= (len (pl-args g)) 1))
|
|
(pl-solve-assertz! db (first (pl-args g)) k))
|
|
((and (pl-compound? g) (= (pl-fun g) "assert") (= (len (pl-args g)) 1))
|
|
(pl-solve-assertz! db (first (pl-args g)) k))
|
|
((and (pl-compound? g) (= (pl-fun g) "asserta") (= (len (pl-args g)) 1))
|
|
(pl-solve-asserta! db (first (pl-args g)) k))
|
|
((and (pl-compound? g) (= (pl-fun g) "retract") (= (len (pl-args g)) 1))
|
|
(pl-solve-retract! db (first (pl-args g)) trail k))
|
|
((and (pl-compound? g) (= (pl-fun g) "findall") (= (len (pl-args g)) 3))
|
|
(pl-solve-findall!
|
|
db
|
|
(first (pl-args g))
|
|
(nth (pl-args g) 1)
|
|
(nth (pl-args g) 2)
|
|
trail
|
|
k))
|
|
((and (pl-compound? g) (= (pl-fun g) "bagof") (= (len (pl-args g)) 3))
|
|
(pl-solve-bagof!
|
|
db
|
|
(first (pl-args g))
|
|
(nth (pl-args g) 1)
|
|
(nth (pl-args g) 2)
|
|
trail
|
|
k))
|
|
((and (pl-compound? g) (= (pl-fun g) "setof") (= (len (pl-args g)) 3))
|
|
(pl-solve-setof!
|
|
db
|
|
(first (pl-args g))
|
|
(nth (pl-args g) 1)
|
|
(nth (pl-args g) 2)
|
|
trail
|
|
k))
|
|
((and (pl-compound? g) (= (pl-fun g) "copy_term") (= (len (pl-args g)) 2))
|
|
(pl-solve-eq!
|
|
(nth (pl-args g) 1)
|
|
(pl-deep-copy (first (pl-args g)) {})
|
|
trail
|
|
k))
|
|
((and (pl-compound? g) (= (pl-fun g) "functor") (= (len (pl-args g)) 3))
|
|
(pl-solve-functor!
|
|
(first (pl-args g))
|
|
(nth (pl-args g) 1)
|
|
(nth (pl-args g) 2)
|
|
trail
|
|
k))
|
|
((and (pl-compound? g) (= (pl-fun g) "arg") (= (len (pl-args g)) 3))
|
|
(pl-solve-arg!
|
|
(first (pl-args g))
|
|
(nth (pl-args g) 1)
|
|
(nth (pl-args g) 2)
|
|
trail
|
|
k))
|
|
((and (pl-compound? g) (= (pl-fun g) "var") (= (len (pl-args g)) 1))
|
|
(let
|
|
((a (pl-walk (first (pl-args g)))))
|
|
(if (pl-var? a) (k) false)))
|
|
((and (pl-compound? g) (= (pl-fun g) "nonvar") (= (len (pl-args g)) 1))
|
|
(let
|
|
((a (pl-walk (first (pl-args g)))))
|
|
(if (not (pl-var? a)) (k) false)))
|
|
((and (pl-compound? g) (= (pl-fun g) "atom") (= (len (pl-args g)) 1))
|
|
(let
|
|
((a (pl-walk (first (pl-args g)))))
|
|
(if (pl-atom? a) (k) false)))
|
|
((and (pl-compound? g) (= (pl-fun g) "number") (= (len (pl-args g)) 1))
|
|
(let
|
|
((a (pl-walk (first (pl-args g)))))
|
|
(if (pl-num? a) (k) false)))
|
|
((and (pl-compound? g) (= (pl-fun g) "integer") (= (len (pl-args g)) 1))
|
|
(let
|
|
((a (pl-walk (first (pl-args g)))))
|
|
(if (pl-num? a) (k) false)))
|
|
((and (pl-compound? g) (= (pl-fun g) "float") (= (len (pl-args g)) 1))
|
|
false)
|
|
((and (pl-compound? g) (= (pl-fun g) "compound") (= (len (pl-args g)) 1))
|
|
(let
|
|
((a (pl-walk (first (pl-args g)))))
|
|
(if (pl-compound? a) (k) false)))
|
|
((and (pl-compound? g) (= (pl-fun g) "callable") (= (len (pl-args g)) 1))
|
|
(let
|
|
((a (pl-walk (first (pl-args g)))))
|
|
(if (or (pl-atom? a) (pl-compound? a)) (k) false)))
|
|
((and (pl-compound? g) (= (pl-fun g) "atomic") (= (len (pl-args g)) 1))
|
|
(let
|
|
((a (pl-walk (first (pl-args g)))))
|
|
(if (or (pl-atom? a) (or (pl-num? a) (pl-str? a))) (k) false)))
|
|
((and (pl-compound? g) (= (pl-fun g) "is_list") (= (len (pl-args g)) 1))
|
|
(if (pl-proper-list? (first (pl-args g))) (k) false))
|
|
((and (pl-compound? g) (= (pl-fun g) "atom_length") (= (len (pl-args g)) 2))
|
|
(let
|
|
((a (pl-walk (first (pl-args g)))))
|
|
(if
|
|
(pl-atom? a)
|
|
(pl-solve-eq!
|
|
(nth (pl-args g) 1)
|
|
(list "num" (len (pl-atom-name a)))
|
|
trail
|
|
k)
|
|
false)))
|
|
((and (pl-compound? g) (= (pl-fun g) "atom_concat") (= (len (pl-args g)) 3))
|
|
(pl-solve-atom-concat!
|
|
(first (pl-args g))
|
|
(nth (pl-args g) 1)
|
|
(nth (pl-args g) 2)
|
|
trail
|
|
k))
|
|
((and (pl-compound? g) (= (pl-fun g) "atom_chars") (= (len (pl-args g)) 2))
|
|
(pl-solve-atom-chars!
|
|
(first (pl-args g))
|
|
(nth (pl-args g) 1)
|
|
trail
|
|
k))
|
|
((and (pl-compound? g) (= (pl-fun g) "atom_codes") (= (len (pl-args g)) 2))
|
|
(pl-solve-atom-codes!
|
|
(first (pl-args g))
|
|
(nth (pl-args g) 1)
|
|
trail
|
|
k))
|
|
((and (pl-compound? g) (= (pl-fun g) "char_code") (= (len (pl-args g)) 2))
|
|
(pl-solve-char-code!
|
|
(first (pl-args g))
|
|
(nth (pl-args g) 1)
|
|
trail
|
|
k))
|
|
((and (pl-compound? g) (= (pl-fun g) "number_codes") (= (len (pl-args g)) 2))
|
|
(let
|
|
((a (pl-walk (first (pl-args g)))))
|
|
(if
|
|
(pl-num? a)
|
|
(pl-solve-eq!
|
|
(nth (pl-args g) 1)
|
|
(pl-list-to-prolog
|
|
(map
|
|
(fn (c) (list "num" (char-code c)))
|
|
(split (str (pl-num-val a)) "")))
|
|
trail
|
|
k)
|
|
false)))
|
|
((and (pl-compound? g) (= (pl-fun g) "number_chars") (= (len (pl-args g)) 2))
|
|
(let
|
|
((a (pl-walk (first (pl-args g)))))
|
|
(if
|
|
(pl-num? a)
|
|
(pl-solve-eq!
|
|
(nth (pl-args g) 1)
|
|
(pl-list-to-prolog
|
|
(map
|
|
(fn (c) (list "atom" c))
|
|
(split (str (pl-num-val a)) "")))
|
|
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)))
|
|
((and (pl-compound? g) (= (pl-fun g) "\\+") (= (len (pl-args g)) 1))
|
|
(let
|
|
((mark (pl-trail-mark trail)))
|
|
(let
|
|
((r (pl-solve! db (first (pl-args g)) trail {:cut false} (fn () true))))
|
|
(pl-trail-undo-to! trail mark)
|
|
(if r false (k)))))
|
|
((and (pl-compound? g) (= (pl-fun g) "not") (= (len (pl-args g)) 1))
|
|
(let
|
|
((mark (pl-trail-mark trail)))
|
|
(let
|
|
((r (pl-solve! db (first (pl-args g)) trail {:cut false} (fn () true))))
|
|
(pl-trail-undo-to! trail mark)
|
|
(if r false (k)))))
|
|
((and (pl-compound? g) (= (pl-fun g) "once") (= (len (pl-args g)) 1))
|
|
(pl-solve-if-then-else!
|
|
db
|
|
(first (pl-args g))
|
|
(list "atom" "true")
|
|
(list "atom" "fail")
|
|
trail
|
|
cut-box
|
|
k))
|
|
((and (pl-compound? g) (= (pl-fun g) "ignore") (= (len (pl-args g)) 1))
|
|
(pl-solve-if-then-else!
|
|
db
|
|
(first (pl-args g))
|
|
(list "atom" "true")
|
|
(list "atom" "true")
|
|
trail
|
|
cut-box
|
|
k))
|
|
((and (pl-compound? g) (= (pl-fun g) "ground") (= (len (pl-args g)) 1))
|
|
(if (pl-ground? (first (pl-args g))) (k) false))
|
|
((and (pl-compound? g) (= (pl-fun g) "sort") (= (len (pl-args g)) 2))
|
|
(let
|
|
((elems (pl-prolog-list-to-sx (first (pl-args g)))))
|
|
(let
|
|
((keyed (map (fn (e) (list (pl-format-term e) e)) elems)))
|
|
(let
|
|
((sorted (sort keyed)))
|
|
(let
|
|
((deduped (pl-sort-pairs-dedup sorted)))
|
|
(pl-solve-eq!
|
|
(nth (pl-args g) 1)
|
|
(pl-list-to-prolog (map (fn (p) (nth p 1)) deduped))
|
|
trail
|
|
k))))))
|
|
((and (pl-compound? g) (= (pl-fun g) "msort") (= (len (pl-args g)) 2))
|
|
(let
|
|
((elems (pl-prolog-list-to-sx (first (pl-args g)))))
|
|
(let
|
|
((keyed (map (fn (e) (list (pl-format-term e) e)) elems)))
|
|
(let
|
|
((sorted (sort keyed)))
|
|
(pl-solve-eq!
|
|
(nth (pl-args g) 1)
|
|
(pl-list-to-prolog (map (fn (p) (nth p 1)) sorted))
|
|
trail
|
|
k)))))
|
|
((and (pl-compound? g) (= (pl-fun g) "atom_number") (= (len (pl-args g)) 2))
|
|
(let
|
|
((wa (pl-walk (first (pl-args g))))
|
|
(wb (pl-walk (nth (pl-args g) 1))))
|
|
(cond
|
|
((pl-atom? wa)
|
|
(let
|
|
((n (parse-number (pl-atom-name wa))))
|
|
(if
|
|
(nil? n)
|
|
false
|
|
(pl-solve-eq!
|
|
(nth (pl-args g) 1)
|
|
(list "num" n)
|
|
trail
|
|
k))))
|
|
((pl-num? wb)
|
|
(pl-solve-eq!
|
|
(first (pl-args g))
|
|
(list "atom" (str (pl-num-val wb)))
|
|
trail
|
|
k))
|
|
(true false))))
|
|
((and (pl-compound? g) (= (pl-fun g) "number_string") (= (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 "atom" (str (pl-num-val wa)))
|
|
trail
|
|
k))
|
|
((pl-var? wa)
|
|
(if
|
|
(pl-atom? wb)
|
|
(let
|
|
((n (parse-number (pl-atom-name wb))))
|
|
(if
|
|
(nil? n)
|
|
false
|
|
(pl-solve-eq!
|
|
(first (pl-args g))
|
|
(list "num" n)
|
|
trail
|
|
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)))))
|
|
(if
|
|
(pl-proper-list? lst-rt)
|
|
(let
|
|
((flat-sx (pl-flatten-prolog lst-rt)))
|
|
(pl-solve-eq!
|
|
(nth (pl-args g) 1)
|
|
(pl-list-to-prolog flat-sx)
|
|
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))))
|
|
(whi (pl-walk-deep (nth (pl-args g) 1))))
|
|
(if
|
|
(and (pl-num? wlo) (pl-num? whi))
|
|
(let
|
|
((lo (pl-num-val wlo)) (hi (pl-num-val whi)))
|
|
(if
|
|
(> lo hi)
|
|
false
|
|
(pl-solve-eq!
|
|
(nth (pl-args g) 2)
|
|
(pl-list-to-prolog (pl-numlist-build lo hi))
|
|
trail
|
|
k)))
|
|
false)))
|
|
|
|
;; atomic_list_concat/2 — no separator
|
|
((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
|
|
(pl-proper-list? lst-rt)
|
|
(let
|
|
((strs (pl-atomic-list-collect lst-rt)))
|
|
(pl-solve-eq!
|
|
(nth (pl-args g) 1)
|
|
(list "atom" (reduce (fn (a b) (str a b)) "" strs))
|
|
trail
|
|
k))
|
|
false)))
|
|
|
|
;; atomic_list_concat/3 — with separator
|
|
((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))))
|
|
(if
|
|
(and (pl-proper-list? lst-rt) (pl-atom? sep-rt))
|
|
(let
|
|
((strs (pl-atomic-list-collect lst-rt))
|
|
(sep (pl-atom-name sep-rt)))
|
|
(pl-solve-eq!
|
|
(nth (pl-args g) 2)
|
|
(list "atom" (pl-join-strings strs sep))
|
|
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)))))
|
|
(if
|
|
(pl-proper-list? lst-rt)
|
|
(pl-solve-eq!
|
|
(nth (pl-args g) 1)
|
|
(list "num" (pl-sum-list-sx lst-rt))
|
|
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) "[]"))))
|
|
(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) "[]"))))
|
|
(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))))
|
|
(elem-rt (nth (pl-args g) 1)))
|
|
(if
|
|
(pl-proper-list? lst-rt)
|
|
(let
|
|
((filtered (pl-delete-sx lst-rt elem-rt)))
|
|
(pl-solve-eq!
|
|
(nth (pl-args g) 2)
|
|
(pl-list-to-prolog filtered)
|
|
trail
|
|
k))
|
|
false)))
|
|
|
|
(true (pl-solve-user! db g trail cut-box k))))))
|
|
|
|
(define
|
|
pl-solve-or!
|
|
(fn
|
|
(db a b trail cut-box k)
|
|
(cond
|
|
((and (pl-compound? a) (= (pl-fun a) "->") (= (len (pl-args a)) 2))
|
|
(pl-solve-if-then-else!
|
|
db
|
|
(first (pl-args a))
|
|
(nth (pl-args a) 1)
|
|
b
|
|
trail
|
|
cut-box
|
|
k))
|
|
(true
|
|
(let
|
|
((mark (pl-trail-mark trail)))
|
|
(let
|
|
((r (pl-solve! db a trail cut-box k)))
|
|
(cond
|
|
(r true)
|
|
((dict-get cut-box :cut) false)
|
|
(true
|
|
(begin
|
|
(pl-trail-undo-to! trail mark)
|
|
(pl-solve! db b trail cut-box k))))))))))
|
|
|
|
(define
|
|
pl-solve-if-then-else!
|
|
(fn
|
|
(db cond-goal then-goal else-goal trail cut-box k)
|
|
(let
|
|
((mark (pl-trail-mark trail)))
|
|
(let
|
|
((local-cb {:cut false}))
|
|
(let
|
|
((found {:val false}))
|
|
(pl-solve!
|
|
db
|
|
cond-goal
|
|
trail
|
|
local-cb
|
|
(fn () (begin (dict-set! found :val true) true)))
|
|
(cond
|
|
((dict-get found :val) (pl-solve! db then-goal trail cut-box k))
|
|
(true
|
|
(begin
|
|
(pl-trail-undo-to! trail mark)
|
|
(pl-solve! db else-goal trail cut-box k)))))))))
|
|
|
|
(define pl-output-buffer "")
|
|
|
|
(define pl-output-clear! (fn () (set! pl-output-buffer "")))
|
|
|
|
(define
|
|
pl-output-write!
|
|
(fn (s) (begin (set! pl-output-buffer (str pl-output-buffer s)) nil)))
|
|
|
|
(define
|
|
pl-format-args
|
|
(fn
|
|
(args)
|
|
(cond
|
|
((empty? args) "")
|
|
((= (len args) 1) (pl-format-term (first args)))
|
|
(true
|
|
(str
|
|
(pl-format-term (first args))
|
|
", "
|
|
(pl-format-args (rest args)))))))
|
|
|
|
(define
|
|
pl-format-term
|
|
(fn
|
|
(t)
|
|
(let
|
|
((w (pl-walk-deep t)))
|
|
(cond
|
|
((pl-var? w) (str "_" (pl-var-id w)))
|
|
((pl-atom? w) (pl-atom-name w))
|
|
((pl-num? w) (str (pl-num-val w)))
|
|
((pl-str? w) (pl-str-val w))
|
|
((pl-compound? w)
|
|
(str (pl-fun w) "(" (pl-format-args (pl-args w)) ")"))
|
|
(true (str w))))))
|
|
|
|
(define
|
|
pl-eval-arith
|
|
(fn
|
|
(t)
|
|
(let
|
|
((w (pl-walk-deep t)))
|
|
(cond
|
|
((pl-num? w) (pl-num-val w))
|
|
((pl-compound? w)
|
|
(let
|
|
((f (pl-fun w)) (args (pl-args w)))
|
|
(cond
|
|
((and (= f "+") (= (len args) 2))
|
|
(+
|
|
(pl-eval-arith (first args))
|
|
(pl-eval-arith (nth args 1))))
|
|
((and (= f "-") (= (len args) 2))
|
|
(-
|
|
(pl-eval-arith (first args))
|
|
(pl-eval-arith (nth args 1))))
|
|
((and (= f "-") (= (len args) 1))
|
|
(- 0 (pl-eval-arith (first args))))
|
|
((and (= f "*") (= (len args) 2))
|
|
(*
|
|
(pl-eval-arith (first args))
|
|
(pl-eval-arith (nth args 1))))
|
|
((and (= f "/") (= (len args) 2))
|
|
(/
|
|
(pl-eval-arith (first args))
|
|
(pl-eval-arith (nth args 1))))
|
|
((and (= f "mod") (= (len args) 2))
|
|
(mod
|
|
(pl-eval-arith (first args))
|
|
(pl-eval-arith (nth args 1))))
|
|
((and (= f "abs") (= (len args) 1))
|
|
(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)))))
|
|
|
|
(define
|
|
pl-solve-not-eq!
|
|
(fn
|
|
(a b trail k)
|
|
(let
|
|
((mark (pl-trail-mark trail)))
|
|
(let
|
|
((unified (pl-unify! a b trail)))
|
|
(begin
|
|
(pl-trail-undo-to! trail mark)
|
|
(cond (unified false) (true (k))))))))
|
|
|
|
(define
|
|
pl-solve-eq!
|
|
(fn
|
|
(a b trail k)
|
|
(let
|
|
((mark (pl-trail-mark trail)))
|
|
(cond
|
|
((pl-unify! a b trail)
|
|
(let
|
|
((r (k)))
|
|
(cond
|
|
(r true)
|
|
(true (begin (pl-trail-undo-to! trail mark) false)))))
|
|
(true (begin (pl-trail-undo-to! trail mark) false))))))
|
|
|
|
(define
|
|
pl-solve-user!
|
|
(fn
|
|
(db goal trail outer-cut-box k)
|
|
(let
|
|
((inner-cut-box {:cut false}))
|
|
(let
|
|
((outer-was-cut (dict-get outer-cut-box :cut)))
|
|
(pl-try-clauses!
|
|
db
|
|
goal
|
|
trail
|
|
(pl-db-lookup-goal db goal)
|
|
outer-cut-box
|
|
outer-was-cut
|
|
inner-cut-box
|
|
k)))))
|
|
|
|
(define
|
|
pl-try-clauses!
|
|
(fn
|
|
(db goal trail clauses outer-cut-box outer-was-cut inner-cut-box k)
|
|
(cond
|
|
((empty? clauses) false)
|
|
(true
|
|
(let
|
|
((mark (pl-trail-mark trail)))
|
|
(let
|
|
((clause (pl-instantiate-fresh (first clauses))))
|
|
(let
|
|
((head (nth clause 1)) (body (nth clause 2)))
|
|
(cond
|
|
((pl-unify! goal head trail)
|
|
(let
|
|
((r (pl-solve! db body trail inner-cut-box k)))
|
|
(cond
|
|
(r true)
|
|
((dict-get inner-cut-box :cut)
|
|
(begin (pl-trail-undo-to! trail mark) false))
|
|
((and (not outer-was-cut) (dict-get outer-cut-box :cut))
|
|
(begin (pl-trail-undo-to! trail mark) false))
|
|
(true
|
|
(begin
|
|
(pl-trail-undo-to! trail mark)
|
|
(pl-try-clauses!
|
|
db
|
|
goal
|
|
trail
|
|
(rest clauses)
|
|
outer-cut-box
|
|
outer-was-cut
|
|
inner-cut-box
|
|
k))))))
|
|
(true
|
|
(begin
|
|
(pl-trail-undo-to! trail mark)
|
|
(pl-try-clauses!
|
|
db
|
|
goal
|
|
trail
|
|
(rest clauses)
|
|
outer-cut-box
|
|
outer-was-cut
|
|
inner-cut-box
|
|
k)))))))))))
|
|
|
|
(define
|
|
pl-solve-once!
|
|
(fn (db goal trail) (pl-solve! db goal trail {:cut false} (fn () true))))
|
|
|
|
(define
|
|
pl-solve-count!
|
|
(fn
|
|
(db goal trail)
|
|
(let
|
|
((box {:n 0}))
|
|
(pl-solve!
|
|
db
|
|
goal
|
|
trail
|
|
{:cut false}
|
|
(fn () (begin (dict-set! box :n (+ (dict-get box :n) 1)) false)))
|
|
(dict-get box :n))))
|