;; lib/datalog/builtins.sx — comparison + arithmetic body literals.
;;
;; Built-in predicates filter / extend candidate substitutions during
;; rule evaluation. They are not stored facts and do not participate in
;; the Herbrand base.
;;
;;   (< a b)  (<= a b)  (> a b)  (>= a b)   ; numeric (or string) compare
;;   (= a b)                                  ; unify (binds vars)
;;   (!= a b)                                ; ground-only inequality
;;   (is X expr)                              ; bind X to expr's value
;;
;; Arithmetic expressions are SX-list compounds:
;;   (+ a b)  (- a b)  (* a b)  (/ a b)
;; or numbers / variables (must be bound at evaluation time).

(define
  dl-comparison?
  (fn
    (lit)
    (and
      (list? lit)
      (> (len lit) 0)
      (let
        ((rel (dl-rel-name lit)))
        (cond
          ((nil? rel) false)
          (else (dl-member-string? rel (list "<" "<=" ">" ">=" "!="))))))))

(define
  dl-eq?
  (fn
    (lit)
    (and
      (list? lit)
      (> (len lit) 0)
      (let ((rel (dl-rel-name lit))) (and (not (nil? rel)) (= rel "=")))))) 

(define
  dl-is?
  (fn
    (lit)
    (and
      (list? lit)
      (> (len lit) 0)
      (let
        ((rel (dl-rel-name lit)))
        (and (not (nil? rel)) (= rel "is")))))) 

;; Evaluate an arithmetic expression under subst. Returns the numeric
;; result, or raises if any operand is unbound or non-numeric.
(define
  dl-eval-arith
  (fn
    (expr subst)
    (let
      ((w (dl-walk expr subst)))
      (cond
        ((number? w) w)
        ((dl-var? w)
          (error (str "datalog arith: unbound variable " (symbol->string w))))
        ((list? w)
          (let
            ((rel (dl-rel-name w)) (args (rest w)))
            (cond
              ((not (= (len args) 2))
                (error (str "datalog arith: need 2 args, got " w)))
              (else
                (let
                  ((a (dl-eval-arith (first args) subst))
                    (b (dl-eval-arith (nth args 1) subst)))
                  (cond
                    ((= rel "+") (+ a b))
                    ((= rel "-") (- a b))
                    ((= rel "*") (* a b))
                    ((= rel "/") (/ a b))
                    (else (error (str "datalog arith: unknown op " rel)))))))))
        (else (error (str "datalog arith: not a number — " w)))))))

(define
  dl-eval-compare
  (fn
    (lit subst)
    (let
      ((rel (dl-rel-name lit))
        (a (dl-walk (nth lit 1) subst))
        (b (dl-walk (nth lit 2) subst)))
      (cond
        ((or (dl-var? a) (dl-var? b))
          (error
            (str
              "datalog: comparison "
              rel
              " has unbound argument; "
              "ensure prior body literal binds the variable")))
        (else
          (let
            ((ok (cond ((= rel "<") (< a b)) ((= rel "<=") (<= a b)) ((= rel ">") (> a b)) ((= rel ">=") (>= a b)) ((= rel "!=") (not (dl-tuple-equal? a b))) (else (error (str "datalog: unknown compare " rel))))))
            (if ok subst nil)))))))

(define
  dl-eval-eq
  (fn
    (lit subst)
    (dl-unify (nth lit 1) (nth lit 2) subst)))

(define
  dl-eval-is
  (fn
    (lit subst)
    (let
      ((target (nth lit 1)) (expr (nth lit 2)))
      (let
        ((value (dl-eval-arith expr subst)))
        (dl-unify target value subst)))))

(define
  dl-eval-builtin
  (fn
    (lit subst)
    (cond
      ((dl-comparison? lit) (dl-eval-compare lit subst))
      ((dl-eq? lit) (dl-eval-eq lit subst))
      ((dl-is? lit) (dl-eval-is lit subst))
      (else (error (str "dl-eval-builtin: not a built-in: " lit))))))

;; ── Safety analysis ──────────────────────────────────────────────
;;
;; Walks body literals left-to-right tracking a "bound" set. The check
;; understands these literal kinds:
;;
;;   positive non-built-in    → adds its vars to bound
;;   (is X expr)              → vars(expr) ⊆ bound, then add X (if var)
;;   <,<=,>,>=,!=             → all vars ⊆ bound (no binding)
;;   (= a b) where:
;;       both non-vars        → constraint check, no binding
;;       a var, b not         → bind a
;;       b var, a not         → bind b
;;       both vars            → at least one in bound; bind the other
;;   {:neg lit}               → all vars ⊆ bound (Phase 7 enforces fully)
;;
;; At end, head vars (minus `_`) must be ⊆ bound.

(define
  dl-vars-not-in
  (fn
    (vs bound)
    (let
      ((out (list)))
      (do
        (for-each
          (fn
            (v)
            (when (not (dl-member-string? v bound)) (append! out v)))
          vs)
        out))))

(define
  dl-rule-check-safety
  (fn
    (rule)
    (let
      ((head (get rule :head))
        (body (get rule :body))
        (bound (list))
        (err nil))
      (do
        (define
          dl-add-bound!
          (fn
            (vs)
            (for-each
              (fn
                (v)
                (when (not (dl-member-string? v bound)) (append! bound v)))
              vs)))
        (define
          dl-process-eq!
          (fn
            (lit)
            (let
              ((a (nth lit 1)) (b (nth lit 2)))
              (let
                ((va (dl-var? a)) (vb (dl-var? b)))
                (cond
                  ((and (not va) (not vb)) nil)
                  ((and va (not vb))
                    (dl-add-bound! (list (symbol->string a))))
                  ((and (not va) vb)
                    (dl-add-bound! (list (symbol->string b))))
                  (else
                    (let
                      ((sa (symbol->string a)) (sb (symbol->string b)))
                      (cond
                        ((dl-member-string? sa bound)
                          (dl-add-bound! (list sb)))
                        ((dl-member-string? sb bound)
                          (dl-add-bound! (list sa)))
                        (else
                          (set!
                            err
                            (str
                              "= between two unbound variables "
                              (list sa sb)
                              " — at least one must be bound by an "
                              "earlier positive body literal")))))))))))
        (define
          dl-process-cmp!
          (fn
            (lit)
            (let
              ((needed (dl-vars-of (list (nth lit 1) (nth lit 2)))))
              (let
                ((missing (dl-vars-not-in needed bound)))
                (when
                  (> (len missing) 0)
                  (set!
                    err
                    (str
                      "comparison "
                      (dl-rel-name lit)
                      " requires bound variable(s) "
                      missing
                      " (must be bound by an earlier positive "
                      "body literal)")))))))
        (define
          dl-process-is!
          (fn
            (lit)
            (let
              ((tgt (nth lit 1)) (expr (nth lit 2)))
              (let
                ((needed (dl-vars-of expr)))
                (let
                  ((missing (dl-vars-not-in needed bound)))
                  (cond
                    ((> (len missing) 0)
                      (set!
                        err
                        (str
                          "is RHS uses unbound variable(s) "
                          missing
                          " — bind them via a prior positive body "
                          "literal")))
                    (else
                      (when
                        (dl-var? tgt)
                        (dl-add-bound! (list (symbol->string tgt)))))))))))
        (define
          dl-process-neg!
          (fn
            (lit)
            (let
              ((needed (dl-vars-of (get lit :neg))))
              (let
                ((missing (dl-vars-not-in needed bound)))
                (when
                  (> (len missing) 0)
                  (set!
                    err
                    (str
                      "negation refers to unbound variable(s) "
                      missing
                      " — they must be bound by an earlier "
                      "positive body literal")))))))
        (define
          dl-process-agg!
          (fn
            (lit)
            (let
              ((result-var (nth lit 1)))
              ;; Aggregate goal vars are existentially quantified within
              ;; the aggregate; nothing required from outer context. The
              ;; result var becomes bound after the aggregate fires.
              (when
                (dl-var? result-var)
                (dl-add-bound! (list (symbol->string result-var)))))))

        (define
          dl-process-lit!
          (fn
            (lit)
            (when
              (nil? err)
              (cond
                ((and (dict? lit) (has-key? lit :neg))
                  (dl-process-neg! lit))
                ((dl-aggregate? lit) (dl-process-agg! lit))
                ((dl-eq? lit) (dl-process-eq! lit))
                ((dl-is? lit) (dl-process-is! lit))
                ((dl-comparison? lit) (dl-process-cmp! lit))
                ((and (list? lit) (> (len lit) 0))
                  (dl-add-bound! (dl-vars-of lit)))))))
        (for-each dl-process-lit! body)
        (when
          (nil? err)
          (let
            ((head-vars (dl-vars-of head)) (missing (list)))
            (do
              (for-each
                (fn
                  (v)
                  (when
                    (and (not (dl-member-string? v bound)) (not (= v "_")))
                    (append! missing v)))
                head-vars)
              (when
                (> (len missing) 0)
                (set!
                  err
                  (str
                    "head variable(s) "
                    missing
                    " do not appear in any positive body literal"))))))
        err))))