;; 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 "/")
                      (cond
                        ((= b 0)
                          (error
                            (str "datalog arith: division by zero in "
                                 w)))
                        (else (/ a b))))
                    (else (error (str "datalog arith: unknown op " rel)))))))))
        (else (error (str "datalog arith: not a number — " w)))))))

;; Comparable types — both operands must be the same primitive type
;; (both numbers, both strings). `!=` is the exception: it's defined
;; for any pair (returns true iff not equal) since dl-tuple-equal?
;; handles type-mixed comparisons.
(define
  dl-compare-typeok?
  (fn
    (rel a b)
    (cond
      ((= rel "!=") true)
      ((and (number? a) (number? b)) true)
      ((and (string? a) (string? b)) true)
      (else false))))

(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")))
        ((not (dl-compare-typeok? rel a b))
          (error
            (str "datalog: comparison " rel " requires same-type "
                 "operands (both numbers or both strings), got "
                 a " and " b)))
        (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))))

;; Filter a list of variable-name strings to exclude anonymous-renamed
;; vars (`_` in source → `_anon*` by dl-rename-anon-term). Used by
;; the negation safety check, where anonymous vars are existential
;; within the negated literal.
(define
  dl-non-anon-vars
  (fn
    (vs)
    (let
      ((out (list)))
      (do
        (for-each
          (fn
            (v)
            (when
              (not (and (>= (len v) 5)
                        (= (slice v 0 5) "_anon")))
              (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
              ((inner (get lit :neg)))
              (let
                ((inner-rn
                   (cond
                     ((and (list? inner) (> (len inner) 0))
                       (dl-rel-name inner))
                     (else nil)))
                  ;; Anonymous variables (`_` in source → `_anon*` after
                  ;; renaming) are existentially quantified within the
                  ;; negated literal — they don't need to be bound by
                  ;; an earlier body lit, since `not p(X, _)` is a
                  ;; valid idiom for "no Y exists s.t. p(X, Y)". Filter
                  ;; them out of the safety check.
                  (needed (dl-non-anon-vars (dl-vars-of inner)))
                  (missing (dl-vars-not-in needed bound)))
                (cond
                  ((and (not (nil? inner-rn)) (dl-reserved-rel? inner-rn))
                    (set! err
                      (str "negated literal uses reserved name '"
                           inner-rn
                           "' — nested `not(...)` / negated built-ins are "
                           "not supported; introduce an intermediate "
                           "relation and negate that")))
                  ((> (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))
                ;; A bare dict that is not a recognised negation is
                ;; almost certainly a typo (e.g. `{:negs ...}` instead
                ;; of `{:neg ...}`). Without this guard the dict would
                ;; silently fall through every clause; the head safety
                ;; check would then flag the head variables as unbound
                ;; even though the real bug is the malformed body lit.
                ((dict? lit)
                  (set! err
                    (str "body literal is a dict but lacks :neg — "
                         "the only dict-shaped body lit recognised is "
                         "{:neg <positive-lit>} for stratified "
                         "negation, got " 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))
                  (let ((rn (dl-rel-name lit)))
                    (cond
                      ((and (not (nil? rn)) (dl-reserved-rel? rn))
                        (set! err
                          (str "body literal uses reserved name '" rn
                               "' — built-ins / aggregates have their own "
                               "syntax; nested `not(...)` is not supported "
                               "(use stratified negation via an "
                               "intermediate relation)")))
                      (else (dl-add-bound! (dl-vars-of lit))))))
                (else
                  ;; Anything that's not a dict, not a list, or an
                  ;; empty list. Numbers / strings / symbols as body
                  ;; lits don't make sense — surface the type.
                  (set! err
                    (str "body literal must be a positive lit, "
                         "built-in, aggregate, or {:neg ...} dict, "
                         "got " 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))))
