;; lib/acl/explain.sx — proof-tree reconstruction over the saturated db.
;;
;; lib/datalog/ records derived facts but not their provenance, so the proof is
;; reconstructed here by goal-directed search over the *saturated* db: for a
;; ground goal we find the first ACL rule (in rule order) whose body holds, take
;; the first solution binding its remaining variables, and recurse on each body
;; literal. Negated literals are recorded as verified `:neg-ok` leaves.
;;
;; CANONICAL DERIVATION: the Datalog derivation graph is a DAG (a fact may hold
;; many ways). We pick ONE canonical proof — first matching rule, first solution
;; — matching the rule order in lib/acl/engine.sx (direct/EDB rules first). A
;; depth cap guards against pathological cyclic data producing unbounded search.
;;
;; A proof node is one of:
;;   {:fact <lit> :via "edb"}                       — base EDB fact
;;   {:fact <lit> :rule <head> :body (<node|negleaf> ...)}  — derived
;;   {:neg-ok <lit>}                                — negation verified to fail
;;   {:fact <lit> :truncated true}                  — depth cap hit

(define acl-proof-max-depth 64)

;; Substitute a body literal, descending into {:neg ...} dicts (dl-apply-subst
;; does not recurse into dicts, which would leak the neg's free vars).
(define
  acl-subst-lit
  (fn
    (lit s)
    (if
      (and (dict? lit) (has-key? lit :neg))
      {:neg (dl-apply-subst (get lit :neg) s)}
      (dl-apply-subst lit s))))

(define
  acl-lit-edb?
  (fn
    (lit)
    (and
      (list? lit)
      (> (len lit) 0)
      (symbol? (first lit))
      (has-key? acl-edb-arity (symbol->string (first lit))))))

(define
  acl-subst-zip!
  (fn
    (d ks vs)
    (when
      (> (len ks) 0)
      (do
        (dict-set! d (symbol->string (first ks)) (first vs))
        (acl-subst-zip! d (rest ks) (rest vs))))))

;; Bind a rule head's variables to a ground goal's arguments (positional).
(define
  acl-bind-head
  (fn
    (head goal)
    (let
      ((d {}))
      (do (acl-subst-zip! d (rest head) (rest goal)) d))))

(define
  acl-subst-union
  (fn
    (a b)
    (let
      ((d {}))
      (do
        (for-each (fn (k) (dict-set! d k (get a k))) (keys a))
        (for-each (fn (k) (dict-set! d k (get b k))) (keys b))
        d))))

(define acl-prove (fn (db goal) (acl-prove-d db goal 0)))

(define
  acl-prove-d
  (fn
    (db goal depth)
    (cond
      ((> depth acl-proof-max-depth) {:truncated true :fact goal})
      ((acl-lit-edb? goal)
        (if (> (len (dl-query db goal)) 0) {:via "edb" :fact goal} nil))
      (else (acl-prove-rules db goal acl-rules depth)))))

(define
  acl-prove-rules
  (fn
    (db goal rules depth)
    (if
      (= (len rules) 0)
      nil
      (let
        ((p (dl-rule-from-list (first rules))))
        (if
          (= (first (get p :head)) (first goal))
          (let
            ((hs (acl-bind-head (get p :head) goal)))
            (let
              ((qbody (map (fn (l) (acl-subst-lit l hs)) (get p :body))))
              (let
                ((sols (dl-query db qbody)))
                (if
                  (> (len sols) 0)
                  (acl-prove-build db goal p hs (first sols) depth)
                  (acl-prove-rules db goal (rest rules) depth)))))
          (acl-prove-rules db goal (rest rules) depth))))))

(define
  acl-prove-build
  (fn
    (db goal p hs sol depth)
    (let ((full (acl-subst-union hs sol))) {:body (map (fn (l) (let ((g (acl-subst-lit l full))) (if (and (dict? g) (has-key? g :neg)) {:neg-ok (get g :neg)} (acl-prove-d db g (+ depth 1))))) (get p :body)) :rule (get p :head) :fact goal})))

;; Public decision-with-proof. Returns:
;;   {:allowed? <bool> :proof <node|nil> :reason <eff_deny proof|nil>}
;; When permitted, :proof is the permit derivation. When denied, :proof is nil
;; and :reason carries the blocking eff_deny proof if one exists (an explicit or
;; inherited deny), else nil (simply no grant).
(define
  acl-explain
  (fn
    (db subj act res)
    (let
      ((proof (acl-prove db (list (quote permit) subj act res))))
      (if (= proof nil) {:allowed? false :proof nil :reason (acl-prove db (list (quote eff_deny) subj act res))} {:allowed? true :proof proof :reason nil}))))
