;; lib/mod/explain.sx — human-readable proof explanation.
;;
;; Turns a decision (from mod/decide-report, or any audit entry) into a readable
;; multi-line "why": the action, the rule that fired, the evidence in play, and
;; the derivation goal-by-goal with [proved]/[unproved] marks and the unification
;; bindings that satisfied each goal. Pure SX over the Phase-2 proof tree.

(define
  mod/explain-binds
  (fn
    (binds)
    (mod/join-with
      ", "
      (map (fn (k) (str k "=" (dict-get binds k))) (keys binds)))))

(define
  mod/explain-goal
  (fn
    (g)
    (let
      ((mark (if (get g :solved) "  [proved] " "  [unproved] "))
        (binds (get g :bindings)))
      (if
        (empty? (keys binds))
        (str mark (get g :goal))
        (str mark (get g :goal) "  {" (mod/explain-binds binds) "}")))))

(define
  mod/explain-evidence
  (fn
    (evidence)
    (if
      (empty? evidence)
      "Evidence: (none)"
      (str "Evidence: " (mod/join-with ", " evidence)))))

(define
  mod/explain
  (fn
    (decision)
    (let
      ((id (get decision :report-id))
        (action (get decision :action))
        (rule (get decision :rule))
        (proof (get decision :proof)))
      (let
        ((goals (get proof :goals)) (evidence (get proof :evidence)))
        (mod/join-with
          "\n"
          (append
            (list
              (str "Report " id ": " action " (rule: " rule ")")
              (mod/explain-evidence evidence)
              "Because:")
            (map mod/explain-goal goals)))))))