package gudusoft.gsqlparser.dlineage.dynamicsql;

import gudusoft.gsqlparser.DynamicSqlProofHarness;
import gudusoft.gsqlparser.EDbVendor;
import gudusoft.gsqlparser.TSourceToken;
import gudusoft.gsqlparser.nodes.TParseTreeNode;
import gudusoft.gsqlparser.resolver2.binding.BindingTrace;
import gudusoft.gsqlparser.resolver2.binding.BindingTraceRegistry;

import java.util.ArrayList;
import java.util.Collections;
import java.util.List;

/**
 * Historical per-edge classifier experiment for dynamic SQL (design:
 * {@code docs/designs/sp/dynamic-sql-fragment-provenance-design.md}, Layer 3 /
 * R4 step 4).
 *
 * <p>This class is not a publication authority. It checks three useful evidence
 * conditions, but its P2 approximation is known to accept a JOIN/ON-tail
 * counterexample. A true publication proof additionally requires the LR
 * commitment check and staged model construction described in
 * {@code dynamic-sql-commitment-check-design.md}.
 * The historical conditions are:
 *
 * <ul>
 *   <li><b>P1 literal evidence</b> — every evidence token's character span maps
 *       to {@link SqlFragment.Kind#LITERAL} fragments (step 1's fragment IR).
 *       A hole never contributes identifier text, so a fabricated object cannot
 *       be published by construction.</li>
 *   <li><b>P2 stability</b> — every evidence token lies before the first hole,
 *       and the literal prefix up to that hole is a safe lexical boundary
 *       ({@link DynamicSqlProofHarness#checkLexBoundary}, step 2), and the
 *       whole materialized text is proof-grade parseable
 *       ({@link DynamicSqlProofHarness#proofParse}) — no recovery, no syntax
 *       errors.</li>
 *   <li><b>P3 binding-chain independence</b> — every evidence reference carries
 *       a COMPLETE {@link BindingTrace} (step 3). A missing or incomplete trace
 *       refuses: an omitted binder never looks complete.</li>
 * </ul>
 *
 * <p><b>Phase status: built, unwired.</b> No analysis path calls this yet;
 * staged publication and a sound LR commitment check are prerequisites for
 * any filtered publication mode. Its historical P2 token-adjacency check has
 * a pinned counterexample and must be treated as SHADOW evidence only.
 */
public final class DynamicSqlEdgeProof {

    private DynamicSqlEdgeProof() {
    }

    /** Outcome of proving one candidate edge. */
    public static final class Verdict {
        /** Historical classifier acceptance; not permission to publish. */
        public final boolean publishable;
        /** Refusal cause, tagged with the failing condition; {@code null} when publishable. */
        public final String reason;
        /** Origin of the hole that blocked the edge, when P1/P2 failed on one. */
        public final SqlFragment.HoleOrigin blockingHole;
        /** Name of the variable / call / expression behind {@link #blockingHole}. */
        public final String blockingHoleName;
        Verdict(boolean publishable, String reason, SqlFragment.HoleOrigin blockingHole,
                String blockingHoleName) {
            this.publishable = publishable;
            this.reason = reason;
            this.blockingHole = blockingHole;
            this.blockingHoleName = blockingHoleName;
        }

        static Verdict publish() {
            return new Verdict(true, null, null, null);
        }

        static Verdict refuse(String reason) {
            return new Verdict(false, reason, null, null);
        }

        static Verdict refuse(String reason, SqlFragment hole) {
            return new Verdict(false, reason, hole == null ? null : hole.origin,
                    hole == null ? null : hole.originName);
        }

        @Override
        public String toString() {
            return publishable ? "publish" : "refuse: " + reason
                    + (blockingHoleName != null ? " [" + blockingHole + " " + blockingHoleName + "]" : "");
        }
    }

    /**
     * The evidence set of one candidate edge: the AST nodes whose tokens spell
     * the source object, the target object, and the column references binding
     * them. Callers assemble it from the sentinel parse; an edge kind whose
     * evidence cannot be enumerated must not be offered here (fail closed by
     * not publishing it at all).
     */
    public static final class EdgeEvidence {
        private TParseTreeNode sourceTable;
        private TParseTreeNode targetTable;
        private final List<gudusoft.gsqlparser.nodes.TObjectName> references =
                new ArrayList<gudusoft.gsqlparser.nodes.TObjectName>();
        private final List<gudusoft.gsqlparser.nodes.TObjectName> sourceSideReferences =
                new ArrayList<gudusoft.gsqlparser.nodes.TObjectName>();
        private final List<gudusoft.gsqlparser.nodes.TObjectName> targetSideReferences =
                new ArrayList<gudusoft.gsqlparser.nodes.TObjectName>();
        private final List<TParseTreeNode> extraNodes = new ArrayList<TParseTreeNode>();

        /**
         * The edge's source relation node (a {@code TTable}, an INTO clause,
         * a derived-table node). Mandatory. Must NOT be a {@code TObjectName} —
         * names go through {@link #reference} so they cannot skip P3.
         */
        public EdgeEvidence source(TParseTreeNode relation) {
            this.sourceTable = relation;
            return this;
        }

        /** The edge's target relation node. Mandatory. Same rule as {@link #source}. */
        public EdgeEvidence target(TParseTreeNode relation) {
            this.targetTable = relation;
            return this;
        }

        /**
         * A column reference on the SOURCE side: it must bind to the source
         * relation. Span-checked (P1/P2) AND binding-checked (P3).
         */
        public EdgeEvidence sourceReference(gudusoft.gsqlparser.nodes.TObjectName reference) {
            if (reference != null) {
                references.add(reference);
                sourceSideReferences.add(reference);
            }
            return this;
        }

        /**
         * A column reference on the TARGET side: it must bind to the target
         * relation. Span-checked (P1/P2) AND binding-checked (P3).
         *
         * <p>Roles are directional on purpose: "binds to either endpoint" would
         * certify the reverse edge, e.g. {@code source(d).target(t)} over
         * {@code INSERT INTO d(x) SELECT t.a FROM t}.
         */
        public EdgeEvidence targetReference(gudusoft.gsqlparser.nodes.TObjectName reference) {
            if (reference != null) {
                references.add(reference);
                targetSideReferences.add(reference);
            }
            return this;
        }

        /**
         * An additional structural node whose span must also be literal and
         * stable (a clause node, a join condition). Names must NOT come in
         * this way — {@code TObjectName} passed here is rejected, because it
         * would skip the P3 binding check.
         */
        public EdgeEvidence structure(TParseTreeNode node) {
            if (node != null) {
                extraNodes.add(node);
            }
            return this;
        }

        /** Roles that must be present for the evidence set to be admissible. */
        String missingRole() {
            if (sourceTable == null) {
                return "source relation";
            }
            if (targetTable == null) {
                return "target relation";
            }
            if (sourceSideReferences.isEmpty()) {
                return "source-side column reference";
            }
            // No name may enter through a span-only role: that would skip P3.
            if (sourceTable instanceof gudusoft.gsqlparser.nodes.TObjectName
                    || targetTable instanceof gudusoft.gsqlparser.nodes.TObjectName) {
                return "a name was supplied as a relation endpoint (would skip the binding check)";
            }
            for (TParseTreeNode n : extraNodes) {
                if (n instanceof gudusoft.gsqlparser.nodes.TObjectName) {
                    return "a name was supplied as structure (would skip the binding check)";
                }
            }
            return null;
        }

        /** Every node whose span must be literal and stable. */
        List<TParseTreeNode> spanNodes() {
            List<TParseTreeNode> all = new ArrayList<TParseTreeNode>();
            all.add(sourceTable);
            all.add(targetTable);
            all.addAll(references);
            all.addAll(extraNodes);
            return all;
        }
    }

    /**
     * Prove one candidate edge against a materialized site.
     *
     * @param site      the materialized dynamic SQL, carrying fragment provenance
     * @param evidence  the edge's evidence set, from the parse of {@code site.sqlText}
     * @param traces    binding traces from the resolver run over that parse;
     *                  {@code null} means no trace information ⇒ refuse
     * @param vendor    dialect, for the lexical boundary checks
     */
    public static Verdict prove(DynamicSqlLineageResolver.MaterializedSite site,
            gudusoft.gsqlparser.TCustomSqlStatement statement,
            EdgeEvidence evidence, BindingTraceRegistry traces, EDbVendor vendor) {
        if (statement == null || statement.sourcetokenlist == null) {
            return Verdict.refuse("P0: no owning statement supplied");
        }
        if (site == null || site.sqlText == null) {
            return Verdict.refuse("P0: no materialized text");
        }
        if (evidence == null) {
            return Verdict.refuse("P0: no evidence");
        }
        String missing = evidence.missingRole();
        if (missing != null) {
            return Verdict.refuse("P0: evidence set incomplete — " + missing);
        }
        if (site.fragments.isEmpty()) {
            return Verdict.refuse("P0: no fragment provenance (producer channel carries none)");
        }

        // --- P0b: fragment/text consistency ---------------------------------
        // The span→fragment mapping is only meaningful if the fragments really
        // render this text. (SqlStringValue enforces this at construction; a
        // MaterializedSite built by another channel might not.)
        StringBuilder rendered = new StringBuilder(site.sqlText.length());
        for (SqlFragment f : site.fragments) {
            rendered.append(f.text);
        }
        if (!rendered.toString().equals(site.sqlText)) {
            return Verdict.refuse("P0: fragments do not render the site text");
        }

        // The statement (and therefore the traces taken from its resolution) must
        // be THE parse of this site text. Without this, evidence from a parse of
        // a DIFFERENT but prefix-compatible text passes every later check: the
        // early spans match and the tokens are that statement's own, yet the
        // real site may bind those names differently (an extra JOIN makes them
        // ambiguous). Require the statement's tokens to render the site text.
        StringBuilder stmtText = new StringBuilder(site.sqlText.length());
        for (int i = 0; i < statement.sourcetokenlist.size(); i++) {
            stmtText.append(statement.sourcetokenlist.get(i).toString());
        }
        if (!stmtText.toString().equals(site.sqlText)) {
            return Verdict.refuse("P0: the supplied statement is not the parse of this site text");
        }

        // --- P1: every evidence span is literal ------------------------------
        List<int[]> holeSpans = holeSpansOf(site);
        List<SqlFragment> holes = holesOf(site);
        int firstHoleStart = holeSpans.isEmpty() ? -1 : holeSpans.get(0)[0];

        List<TParseTreeNode> spanNodes = evidence.spanNodes();
        for (TParseTreeNode node : spanNodes) {
            // Ownership is established by TOKEN IDENTITY, on BOTH endpoints of
            // the span. A node from a different parse (e.g. a separately
            // re-parsed second statement, whose offsets restart at 0) is
            // rejected because its tokens are not these tokens — identity
            // cannot be forged by identical text at identical offsets. Pinning
            // both ends, rather than only the start, is what makes the span a
            // provable interval of THIS statement's own token stream.
            //
            // Deliberately NOT a comparison against the rendered text: an
            // earlier version required site.sqlText.substring(span) to equal
            // node.toString(), which silently deleted provable edges whenever a
            // node's rendering differs from its source span. An aliased table
            // spans `src AS s` but renders `src`, so every aliased source table
            // — one of the commonest shapes in real SQL — lost its edge. Token
            // identity is both stronger (text equality cannot prove AST
            // provenance) and rendering-independent.
            if (!ownsToken(statement, node.getStartToken())
                    || !ownsToken(statement, node.getEndToken())) {
                return Verdict.refuse("P1: evidence node does not belong to this statement");
            }
            int[] span = spanOf(node);
            if (span == null) {
                return Verdict.refuse("P1: evidence node has no source span");
            }
            // P0 already proved the statement's tokens render site.sqlText, so
            // an owned token's offset indexes that text; keep the bound check as
            // a hard assertion rather than an assumption.
            if (span[0] < 0 || span[1] > site.sqlText.length()) {
                return Verdict.refuse("P1: evidence span is outside the site text");
            }
            for (int i = 0; i < holeSpans.size(); i++) {
                int[] h = holeSpans.get(i);
                if (span[0] < h[1] && h[0] < span[1]) {
                    return Verdict.refuse("P1: evidence overlaps a hole", holes.get(i));
                }
            }
        }

        // A fully concrete site has no holes: P2's prefix reasoning is vacuous,
        // but the text must still be proof-grade parseable.
        if (firstHoleStart < 0) {
            DynamicSqlProofHarness.ProofParseResult parse =
                    DynamicSqlProofHarness.proofParse(site.sqlText, vendor);
            if (!parse.ok) {
                return Verdict.refuse("P2: " + parse.reason);
            }
            return proveBindings(evidence, traces);
        }

        // --- P2: stability ---------------------------------------------------
        // Nothing after the first hole is stable: a hole can open a comment or a
        // string and swallow the literal text that follows it.
        for (TParseTreeNode node : spanNodes) {
            int[] span = spanOf(node);
            if (span[1] > firstHoleStart) {
                return Verdict.refuse("P2: evidence lies after the first hole",
                        holes.get(0));
            }
        }

        // P2 commitment: preceding the hole is NOT enough. If the hole abuts the
        // binder region, its runtime text can EXTEND that region and rebind the
        // evidence — `... SELECT a FROM t` + hole `JOIN u ON 1=1` moves `a` from
        // t to u without touching a single evidence token. The construct is
        // committed only when a literal token that terminates the binder region
        // sits between the source relation and the hole (the `where ` in the
        // motivating case). Conservative: any solid literal token in between.
        int[] sourceSpan = spanOf(evidence.sourceTable);
        if (!hasSolidTokenBetween(statement, sourceSpan[1], firstHoleStart)) {
            return Verdict.refuse(
                    "P2: hole abuts the binder region; runtime text could extend it",
                    holes.get(0));
        }
        // P2 containment: the edge's ENTIRE structure must precede the hole.
        // If any query structure follows it, the edge depends on text a runtime
        // instantiation can neutralise — e.g.
        //   INSERT INTO d(x) WITH c AS (SELECT a FROM t WHERE <hole>) SELECT a FROM c
        // where "<hole> = TRUE) SELECT 0; --" leaves c unused and t -> d gone.
        // Only a predicate/expression tail may follow the hole.
        String structural = structuralTokenAfter(statement, firstHoleStart);
        if (structural != null) {
            return Verdict.refuse(
                    "P2: query structure ('" + structural + "') follows the hole", holes.get(0));
        }
        DynamicSqlProofHarness.BoundaryVerdict boundary = DynamicSqlProofHarness.checkLexBoundary(
                site.sqlText.substring(0, firstHoleStart), vendor);
        if (!boundary.clean) {
            return Verdict.refuse("P2: " + boundary.reason, holes.get(0));
        }
        DynamicSqlProofHarness.ProofParseResult parse =
                DynamicSqlProofHarness.proofParse(site.sqlText, vendor);
        if (!parse.ok) {
            return Verdict.refuse("P2: " + parse.reason);
        }

        return proveBindings(evidence, traces);
    }

    /**
     * P3: every evidence reference must carry a complete binding trace WHOSE
     * ENDPOINT is one of the edge's own relations. Completeness alone does not
     * tie a reference to this edge — without the endpoint check, a correctly
     * bound column of some other relation would certify an edge it has nothing
     * to do with.
     */
    private static Verdict proveBindings(EdgeEvidence evidence, BindingTraceRegistry traces) {
        if (traces == null) {
            return Verdict.refuse("P3: no binding traces available");
        }
        for (gudusoft.gsqlparser.nodes.TObjectName ref : evidence.references) {
            BindingTrace t = traces.traceFor(ref);
            if (t == null) {
                return Verdict.refuse("P3: no binding trace for " + ref);
            }
            if (!t.complete) {
                return Verdict.refuse("P3: incomplete binding chain for " + ref + " (" + t + ")");
            }
            Object required = evidence.sourceSideReferences.contains(ref)
                    ? evidence.sourceTable : evidence.targetTable;
            if (!bindsTo(t, required)) {
                return Verdict.refuse("P3: " + ref + " does not bind to its declared endpoint");
            }
        }
        return Verdict.publish();
    }

    /** True when the trace's binder is exactly {@code relation}. */
    private static boolean bindsTo(BindingTrace t, Object relation) {
        if (relation == null) {
            return false;
        }
        Object[] binders = { t.observedSourceTable, t.definitionNode, t.directTarget };
        for (Object b : binders) {
            if (b == relation) {
                return true;
            }
        }
        return false;
    }

    /** Identity check: is this token one of the statement's own tokens? */
    private static boolean ownsToken(gudusoft.gsqlparser.TCustomSqlStatement statement,
            gudusoft.gsqlparser.TSourceToken token) {
        if (token == null) {
            return false;
        }
        gudusoft.gsqlparser.TSourceTokenList tokens = statement.sourcetokenlist;
        for (int i = 0; i < tokens.size(); i++) {
            if (tokens.get(i) == token) {
                return true;
            }
        }
        return false;
    }

    /**
     * The first query-structure keyword among the statement's own tokens at or
     * after {@code fromOffset}, or null when only predicate/expression material
     * follows.
     *
     * <p>The scan walks the REAL token stream rather than the raw text: comments,
     * string literals and delimited identifiers are already classified by the
     * vendor lexer, so a keyword spelled inside any of them is a value or a name
     * and cannot be mistaken for structure — and conversely no line-ending,
     * nested-comment or dollar-quoting subtlety can hide structure from the scan.
     */
    private static String structuralTokenAfter(gudusoft.gsqlparser.TCustomSqlStatement statement,
            int fromOffset) {
        gudusoft.gsqlparser.TSourceTokenList tokens = statement.sourcetokenlist;
        for (int i = 0; i < tokens.size(); i++) {
            gudusoft.gsqlparser.TSourceToken tok = tokens.get(i);
            if (tok.offset < fromOffset) {
                continue;
            }
            gudusoft.gsqlparser.ETokenType type = tok.tokentype;
            // Only real keywords can introduce structure. Identifiers (including
            // every delimited form), literals, comments and punctuation cannot.
            if (type != gudusoft.gsqlparser.ETokenType.ttkeyword
                    && type != gudusoft.gsqlparser.ETokenType.ttnonreservedkeyword) {
                continue;
            }
            String text = tok.toString().toLowerCase(); // non-identifier-compare: SQL keyword classification
            if (STRUCTURAL_KEYWORDS.contains(text)) {
                return text;
            }
        }
        return null;
    }

    /** Keywords that can introduce or re-shape query structure. */
    private static final java.util.Set<String> STRUCTURAL_KEYWORDS =
            new java.util.HashSet<String>(java.util.Arrays.asList(
                    "select", "from", "join", "insert", "update", "delete", "merge",
                    "union", "except", "intersect", "with", "into", "exec", "execute",
                    "apply", "pivot", "unpivot", "values", "table", "using", "cross",
                    "outer", "inner", "full", "lateral", "go"));

    /**
     * True when at least one solid token of the statement sits strictly between
     * {@code from} and {@code to} — the "a literal token closes the binder
     * region before the hole" test. Comments and whitespace close nothing, so
     * the lexer's own classification is used rather than raw text.
     */
    private static boolean hasSolidTokenBetween(gudusoft.gsqlparser.TCustomSqlStatement statement,
            int from, int to) {
        if (from < 0 || from >= to) {
            return false;
        }
        gudusoft.gsqlparser.TSourceTokenList tokens = statement.sourcetokenlist;
        for (int i = 0; i < tokens.size(); i++) {
            gudusoft.gsqlparser.TSourceToken tok = tokens.get(i);
            if (tok.offset >= from && tok.offset < to && tok.issolidtoken()) {
                return true;
            }
        }
        return false;
    }

    /** Character span [start, end) of a node in the parsed text, or null. */
    private static int[] spanOf(TParseTreeNode node) {
        TSourceToken start = node.getStartToken();
        TSourceToken end = node.getEndToken();
        if (start == null || end == null) {
            return null;
        }
        long from = start.offset;
        long to = end.offset + end.toString().length();
        if (from < 0 || to < from) {
            return null;
        }
        return new int[] { (int) from, (int) to };
    }

    /**
     * Character spans {@code [start, end)} of every non-literal fragment of {@code site},
     * in fragment order — index-aligned with {@link #holesOf}. Empty when the site carries
     * no provenance, or when its fragments do not render its text (in which case the spans
     * would describe a DIFFERENT string and must not be used to locate anything).
     *
     * <p>A zero-length hole still yields a span: arbitrary text can be spliced at that
     * point, so it bounds the stable region exactly like a non-empty one.
     */
    public static List<int[]> holeSpansOf(DynamicSqlLineageResolver.MaterializedSite site) {
        if (site == null || site.sqlText == null || site.fragments.isEmpty()) {
            return Collections.emptyList();
        }
        StringBuilder rendered = new StringBuilder(site.sqlText.length());
        for (SqlFragment f : site.fragments) {
            rendered.append(f.text);
        }
        if (!rendered.toString().equals(site.sqlText)) {
            return Collections.emptyList();
        }
        List<int[]> spans = new ArrayList<int[]>();
        int cursor = 0;
        for (SqlFragment f : site.fragments) {
            if (!f.isLiteral()) {
                spans.add(new int[] { cursor, cursor + f.text.length() });
            }
            cursor += f.text.length();
        }
        return spans;
    }

    /** Hole diagnostics for a site, for the "which variable blocked what" report. */
    public static List<SqlFragment> holesOf(DynamicSqlLineageResolver.MaterializedSite site) {
        if (site == null || site.fragments.isEmpty()) {
            return Collections.emptyList();
        }
        List<SqlFragment> out = new ArrayList<SqlFragment>();
        for (SqlFragment f : site.fragments) {
            if (!f.isLiteral()) {
                out.add(f);
            }
        }
        return out;
    }
}