//! The human-readable report rendering (the `Display for Report` path).
use super::json::status_name;
use super::{CoreItem, FixKind, ProveOutcome, Report, Status, TraceReason, TraceStep, TryOutcome};
use alloc::string::String;
use alloc::vec::Vec;
use core::fmt;
use elenchus_compiler::{Origin, PlaceholderStatus, Value, kw};

/// The verified `flip` alternative for a core / retract item, as a nested line —
/// present only when the engine confirmed that asserting the opposite value restores
/// consistency (so `(checked)` is never a promise the engine did not test). `None`
/// when the only repair is `drop`.
fn flip_line(it: &CoreItem) -> Option<String> {
    it.fixes
        .iter()
        .find(|fx| fx.kind == FixKind::Flip)
        .map(|fx| alloc::format!("or flip it to: {}   (checked)", fx.target))
}

impl fmt::Display for Status {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        f.write_str(status_name(*self))
    }
}

/// Format provenance as `name (KIND)  [source:line]` for the human report.
pub(crate) fn premise_tag(o: &Origin) -> String {
    let name = o.premise.as_deref().unwrap_or("-");
    alloc::format!("{} ({})  [{}:{}]", name, o.kind, o.source, o.line)
}

/// One derivation-trace line for the human report.
pub(crate) fn trace_line(step: &TraceStep) -> String {
    let v = match step.value {
        Value::True => "TRUE",
        Value::False => "FALSE",
    };
    match &step.reason {
        TraceReason::Asserted(o) => {
            alloc::format!(
                "{} = {}   [{} {}:{}]",
                step.atom,
                v,
                o.kind,
                o.source,
                o.line
            )
        }
        TraceReason::Derived { origin, from } => alloc::format!(
            "{} = {}   from {} ({})  [{}:{}]  <= {}",
            step.atom,
            v,
            origin.premise.as_deref().unwrap_or("-"),
            origin.kind,
            origin.source,
            origin.line,
            from.join(", ")
        ),
    }
}

/// Indentation levels for the human report. This module is the **single** place
/// leading whitespace is defined: every line is emitted through
/// [`ReportWriter::line`] with one of these as the `indent` argument, so no
/// format string ever carries leading spaces. To restyle the report, change a
/// number here — not spaces scattered across `write!` calls.
mod indent {
    /// `RESULT:` / `SUMMARY:` / `EXIT_CODE:` — flush left.
    pub const ROOT: usize = 0;
    /// A section header: `CONFLICT` / `WARNING` / `CORE` / `RETRACT` / `DERIVED`
    /// / `HINT` / `UNDERDETERMINED`.
    pub const SECTION: usize = 2;
    /// A line belonging to a section (conflict atoms, `blocked by:`, an `ASSUME`).
    pub const ITEM: usize = 6;
    /// A line nested under an item (a `why:` trace step, a `CORE` member).
    pub const NESTED: usize = 8;
    /// The tag column on a section line: a one-word verdict tag (`WARNING`,
    /// `DERIVED`, `TRY`, `PROVE`, …) is left-justified and padded to this width
    /// so every payload starts in the same column. This is the **single** place
    /// that column is defined — emit these lines through [`section!`] with the
    /// bare keyword, never a hand-counted run of trailing spaces. (Long prose
    /// headers — `CORE`, `RETRACT`, `UNDERDETERMINED`, `UNUSED IMPORT` — do not
    /// use this column; they are a keyword and a two-space separator, so they
    /// stay on [`emit!`].)
    pub const TAG: usize = 10;
}

/// The human report's one output primitive. It owns the indentation rule so
/// callers pass a semantic [`indent`] level and the text — never raw spaces.
struct ReportWriter<'a, 'b> {
    f: &'a mut fmt::Formatter<'b>,
}

impl ReportWriter<'_, '_> {
    /// Write `indent` leading spaces, the formatted text, then a newline.
    fn line(&mut self, indent: usize, args: fmt::Arguments<'_>) -> fmt::Result {
        write!(self.f, "{:width$}{}", "", args, width = indent)?;
        self.f.write_str("\n")
    }

    /// Like [`line`](Self::line) but without the trailing newline — for the final
    /// `EXIT_CODE` line, so the report ends exactly as it always has.
    fn tail(&mut self, indent: usize, args: fmt::Arguments<'_>) -> fmt::Result {
        write!(self.f, "{:width$}{}", "", args, width = indent)
    }

    /// Write a verdict section line: the [`SECTION`](indent::SECTION) indent, then
    /// the `tag` keyword left-justified to the [`TAG`](indent::TAG) column so the
    /// payload lines up with every other section, then the formatted payload and a
    /// newline. The single place the tag column is applied — callers pass the bare
    /// keyword and never hand-count the spaces after it.
    fn section(&mut self, tag: &str, args: fmt::Arguments<'_>) -> fmt::Result {
        write!(
            self.f,
            "{:si$}{:tag$}{}",
            "",
            tag,
            args,
            si = indent::SECTION,
            tag = indent::TAG
        )?;
        self.f.write_str("\n")
    }
}

/// `emit!(out, LEVEL, "fmt", args…)` — one indented report line. A thin wrapper
/// over [`ReportWriter::line`] so call sites read `emit!(out, SECTION, …)` with
/// the indent as an explicit parameter and zero leading spaces in the string.
macro_rules! emit {
    ($out:expr, $indent:expr, $($arg:tt)*) => {
        $out.line($indent, format_args!($($arg)*))
    };
}

/// `section!(out, "WARNING", "fmt", args…)` — one verdict section line whose tag
/// column is applied automatically by [`ReportWriter::section`]. The format string
/// carries only the payload; the keyword is a separate argument and the spaces
/// after it are computed, never typed. Use this for every aligned tag line
/// (`CONFLICT`, `WARNING`, `DERIVED`, `TRY`, `PROVE`, `HENCE`, …); the wider prose
/// headers stay on [`emit!`].
macro_rules! section {
    ($out:expr, $tag:expr, $($arg:tt)*) => {
        $out.section($tag, format_args!($($arg)*))
    };
}

impl Report {
    /// Render the full human report. `show_placeholders` toggles the PLACEHOLDERS
    /// section; the `Display` impl passes `true`, the CLI `--hide-params` flag
    /// passes `false` to print only the verdict (the JSON form always keeps it).
    fn render(&self, f: &mut fmt::Formatter<'_>, show_placeholders: bool) -> fmt::Result {
        use indent::{ITEM, NESTED, ROOT, SECTION};
        let mut out = ReportWriter { f };

        emit!(out, ROOT, "RESULT: {}", self.status)?;

        // A pure assumption clash: lead with the one action a small model needs
        // and suppress the raw conflict / CORE pools (they would only echo the
        // ASSUME clause). The verdict is still CONFLICT (exit code 2).
        if !self.retract.is_empty() {
            // Spell out what is wrong and why — this report is the debugger a
            // small model reads. The commitments are sound; the hypotheses are
            // the only dial to turn, so say so explicitly before listing them.
            emit!(out, SECTION, "RETRACT  your FACTs and PREMISEs are fine.")?;
            emit!(
                out,
                ITEM,
                "But these ASSUME guesses cannot all be true together."
            )?;
            emit!(out, ITEM, "Remove ONE of them, then check again:")?;
            for it in &self.retract {
                emit!(
                    out,
                    ITEM,
                    "ASSUME {}   [{}:{}]",
                    it.label,
                    it.origin.source,
                    it.origin.line
                )?;
                if let Some(flip) = flip_line(it) {
                    emit!(out, NESTED, "{flip}")?;
                }
            }
        } else {
            for c in &self.conflicts {
                section!(out, "CONFLICT", "{}", premise_tag(&c.origin))?;
                for a in &c.atoms {
                    emit!(out, ITEM, "{}", a)?;
                }
                if !c.trace.is_empty() {
                    emit!(out, ITEM, "why:")?;
                    for step in &c.trace {
                        emit!(out, NESTED, "{}", trace_line(step))?;
                    }
                }
            }
            if !self.unsat_core.is_empty() {
                emit!(
                    out,
                    SECTION,
                    "CORE  these {} cannot all hold — drop ONE, then check again:",
                    self.unsat_core.len()
                )?;
                for it in &self.unsat_core {
                    let name = if it.label.is_empty() { "-" } else { &it.label };
                    emit!(
                        out,
                        NESTED,
                        "{} ({})  [{}:{}]",
                        name,
                        it.origin.kind,
                        it.origin.source,
                        it.origin.line
                    )?;
                    if let Some(flip) = flip_line(it) {
                        emit!(out, NESTED, "{flip}")?;
                    }
                }
            }
        }

        // Many warnings often share one root cause (e.g. the same missing FACT),
        // so the `fix:` line is deduped in the human report — each distinct fix
        // prints once — to keep a wall of warnings readable. The full per-warning
        // hint is still in the JSON for tools that select/filter programmatically.
        let mut shown_fixes: Vec<&str> = Vec::new();
        for w in &self.warnings {
            section!(out, "WARNING", "{}", premise_tag(&w.origin))?;
            emit!(out, ITEM, "blocked by: {}", w.blocked_by.join(", "))?;
            if let Some(hint) = &w.hint
                && !shown_fixes.contains(&hint.as_str())
            {
                shown_fixes.push(hint);
                emit!(out, ITEM, "fix: {hint}")?;
            }
        }
        // The epistemic (L6) false-belief voice: an agent `BELIEVES` a claim the world
        // establishes FALSE. Belief is non-factive, so this is an informational note (exit
        // 0, like DEFEATED) — never a CONFLICT (that is reserved for `KNOWS` — you cannot
        // *know* a falsehood) and it never raises the verdict.
        for b in &self.beliefs {
            section!(
                out,
                "BELIEF",
                "{} believes {} — but it is FALSE (a false belief)   [{}:{}]",
                b.agent,
                b.claim,
                b.origin.source,
                b.origin.line
            )?;
        }
        if let Some(atom) = &self.underdetermined {
            emit!(out, SECTION, "UNDERDETERMINED  an alternative model exists")?;
            emit!(
                out,
                ITEM,
                "fix: add FACT {atom} (or NOT {atom}) to pin the model"
            )?;
        }
        // The abduction (L5) voice: each `TRY <literal>` hypothesis, with the engine's
        // checked verdict on whether asserting it would close the open gap. Advisory —
        // the candidate was never committed, so this never changed the result above.
        for t in &self.tried {
            match &t.goal {
                Some(g) => section!(out, "TRY", "{} FOR {}", t.label, g)?,
                None => section!(out, "TRY", "{}", t.label)?,
            }
            let verdict = match t.outcome {
                TryOutcome::Closes => "closes the gap: the model is now pinned",
                TryOutcome::Conflicts => "conflicts: it clashes with what is already established",
                TryOutcome::StillOpen => "still open: it does not pin the model",
                TryOutcome::Explains => {
                    "explains the goal: consistent, and theory + hypothesis entails it"
                }
                TryOutcome::NotExplaining => {
                    "does not explain: the goal still does not follow with the hypothesis"
                }
            };
            emit!(out, ITEM, "{verdict}   (checked)")?;
        }
        // The checked-derivation (proof kernel) voice: each `HENCE` step with the
        // engine's per-step verdict — the first `does not follow` line is the gap.
        // Advisory — steps were never committed, the result above is untouched.
        for h in &self.derivation {
            section!(out, "HENCE", "{} FROM {}", h.conclusion, h.from.join(", "))?;
            if h.holds {
                emit!(out, ITEM, "holds: the cited premises entail it   (checked)")?;
            } else {
                emit!(
                    out,
                    ITEM,
                    "does not follow from what it cites — the gap is here   (checked)"
                )?;
            }
        }
        // The entailment (⊨) voice: each `PROVE <literal>` goal, with the engine's
        // refutation-checked verdict on whether the theory entails it. Advisory —
        // the goal was never committed, so this never changed the result above.
        for g in &self.goals {
            section!(out, "PROVE", "{}", g.label)?;
            let verdict = match g.outcome {
                ProveOutcome::Proved => "PROVED: it follows from the theory",
                ProveOutcome::Refuted => "REFUTED: its negation follows from the theory",
                ProveOutcome::Open => "OPEN: the theory pins neither it nor its negation",
                ProveOutcome::Vacuous => {
                    "VACUOUS: the theory is inconsistent — it entails everything"
                }
            };
            emit!(out, ITEM, "{verdict}   (checked)")?;
        }
        for d in &self.derived {
            let v = match d.value {
                Value::True => "TRUE",
                Value::False => "FALSE",
            };
            section!(
                out,
                "DERIVED",
                "{} = {}   from {}",
                d.atom,
                v,
                premise_tag(&d.origin)
            )?;
        }
        for d in &self.defeated {
            section!(
                out,
                "DEFEATED",
                "{}   default {} suppressed by {}",
                premise_tag(&d.origin),
                d.consequent,
                d.blocked_by.join(", ")
            )?;
        }
        for h in &self.hints {
            section!(
                out,
                "HINT",
                "possible typo — '{}' and '{}' look like the same atom ({})",
                h.a,
                h.b,
                h.reason
            )?;
        }
        for o in &self.orphans {
            // Reconstruct the surface line; `kind` already carries the polarity
            // except for `ASSUME NOT`, where the value supplies it.
            let surface = if o.origin.kind == kw::ASSUME && matches!(o.value, Value::False) {
                alloc::format!("{} {} {}", kw::ASSUME, kw::NOT, o.atom)
            } else {
                alloc::format!("{} {}", o.origin.kind, o.atom)
            };
            section!(
                out,
                "ORPHAN",
                "{} — not used by any premise or rule (no effect on the result)",
                surface
            )?;
        }
        for u in &self.unused_imports {
            let via = match &u.alias {
                Some(a) => alloc::format!("{} AS {}", u.domain, a),
                None => u.domain.clone(),
            };
            emit!(
                out,
                SECTION,
                "UNUSED IMPORT  {} — imported in {}:{} but never referenced (no effect on the result)",
                via,
                u.file,
                u.line
            )?;
        }
        // The PLACEHOLDERS section: every declared VAR port, how it resolved. A
        // debugging aid for whoever wires the values; suppressed by `--hide-params`.
        if show_placeholders {
            for p in &self.placeholders {
                match p.status {
                    PlaceholderStatus::Supplied => section!(
                        out,
                        "PARAM",
                        "{} = {}   (supplied{})",
                        p.key,
                        bool_word(p.value),
                        p.origin
                            .as_deref()
                            .map(|o| alloc::format!(": {o}"))
                            .unwrap_or_default()
                    )?,
                    PlaceholderStatus::DefaultUsed => section!(
                        out,
                        "PARAM",
                        "{} = {}   (DEFAULT)",
                        p.key,
                        bool_word(p.value)
                    )?,
                    PlaceholderStatus::Unset => section!(
                        out,
                        "PARAM",
                        "{} = UNKNOWN   (no value supplied, no DEFAULT)",
                        p.key
                    )?,
                }
            }
        }

        let underdetermined = usize::from(self.status == Status::Underdetermined);
        // Append the defeated count only when non-zero, so programs without any
        // defeasible defeat keep their exact summary line.
        let defeated = if self.defeated.is_empty() {
            String::new()
        } else {
            alloc::format!(", {} defeated", self.defeated.len())
        };
        // A false belief is informational (exit 0), so it is not a `warnings` entry; name
        // its count here (only when non-zero), appended like `defeated`, so the visible
        // BELIEF lines are accounted for while programs with no false belief keep their
        // exact summary line.
        let beliefs = if self.beliefs.is_empty() {
            String::new()
        } else {
            alloc::format!(", {} false beliefs", self.beliefs.len())
        };
        emit!(
            out,
            ROOT,
            "SUMMARY: {} conflicts, {} underdetermined, {} warnings, {} derived{}{}",
            self.conflicts.len(),
            underdetermined,
            self.warnings.len(),
            self.derived.len(),
            defeated,
            beliefs
        )?;
        out.tail(ROOT, format_args!("EXIT_CODE: {}", self.exit_code()))
    }

    /// The full human report as an owned string. `show_placeholders = false`
    /// (the CLI `--hide-params` flag) prints only the verdict, exactly as before
    /// the ports feature. The JSON form (`to_json`) always keeps the section.
    pub fn render_human(&self, show_placeholders: bool) -> String {
        alloc::format!(
            "{}",
            HumanReport {
                report: self,
                show_placeholders
            }
        )
    }
}

/// A `Display` adapter that renders a [`Report`] with a chosen `show_placeholders`
/// flag (the plain `Display` impl always shows them).
struct HumanReport<'a> {
    report: &'a Report,
    show_placeholders: bool,
}

impl fmt::Display for HumanReport<'_> {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        self.report.render(f, self.show_placeholders)
    }
}

impl fmt::Display for Report {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        self.render(f, true)
    }
}

/// `true`/`false` for a resolved port value (a supplied/default port is always
/// `Some`); an unset port renders `UNKNOWN` at its own call site.
pub(crate) fn bool_word(v: Option<bool>) -> &'static str {
    match v {
        Some(true) => "true",
        Some(false) => "false",
        None => "UNKNOWN",
    }
}
