;; 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))))