package gudusoft.gsqlparser;

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

/**
 * Proof harness for the dynamic-SQL per-edge publication proof
 * (design: {@code docs/designs/sp/dynamic-sql-fragment-provenance-design.md},
 * Layer 2 / phase "R4 step 2").
 *
 * <p>This class exists in {@code gudusoft.gsqlparser} — NOT in dlineage —
 * because the checks need the real pipeline's internals (lexer accumulation
 * state, parser recovery events), which are package-local here. It is
 * hand-written; it never modifies generated lexer/parser files.
 *
 * <p><b>Phase status: built, unwired.</b> No product path calls it yet; it is
 * exercised only by its isolation tests. Everything it reports errs on the
 * side of refusal: a {@code false}/failed verdict never causes wrong output,
 * only (later, when wired) a smaller published-edge set.
 *
 * <p>Provided checks (design Layer 2):
 * <ol>
 *   <li><b>Boundary lex check</b> — {@link #checkLexBoundary}: the literal
 *       prefix before the first hole must end in a clean lexer state (no
 *       unterminated string/comment/bracketed identifier — observed as
 *       non-empty {@code literalbuf} accumulation and swallowed characters),
 *       with balanced paren depth, a fusion-safe boundary character, and (for
 *       MSSQL) no line-comment-ambiguous {@code --} on the boundary line
 *       (TLexerMssql classifies {@code --} by inspecting the whole current
 *       line, so the hole's same-line content could flip it).</li>
 *   <li><b>Proof-mode parse</b> — {@link #proofParse}: parse with the real
 *       pipeline and refuse when the parse needed ANY recovery
 *       ({@link TCustomParser#getProofRecoveryEvents}) or produced syntax
 *       errors. Silent keyword rollback counts as recovery: a parse that
 *       needed it is not evidence.</li>
 *   <li><b>MSSQL rewrite-horizon audit</b> — {@link MssqlRewriteAudit}: the
 *       per-rule forward-window facts from the review-round-2 audit, replacing
 *       the unsound single global {@code W}.</li>
 * </ol>
 *
 * <p>Deliberately NOT here yet (next increments): the differential
 * prefix+EOF probe and the committed-node (parser commitment) check.
 */
public final class DynamicSqlProofHarness {

    private DynamicSqlProofHarness() {
    }

    /* ------------------------------------------------------ boundary check */

    /** Verdict of {@link #checkLexBoundary}; {@code clean == false} means the proof must refuse. */
    public static final class BoundaryVerdict {
        public final boolean clean;
        /** Human-readable refusal cause; {@code null} when clean. */
        public final String reason;

        BoundaryVerdict(boolean clean, String reason) {
            this.clean = clean;
            this.reason = reason;
        }

        static BoundaryVerdict ok() {
            return new BoundaryVerdict(true, null);
        }

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

        @Override
        public String toString() {
            return clean ? "clean" : "refused: " + reason;
        }
    }

    /**
     * Check that {@code prefix} — the literal text before the first hole — is a
     * safe lexical boundary: every character lexed into complete tokens, no
     * open literal/comment/bracket state, balanced parens/brackets, a
     * fusion-safe final character, and no line-comment ambiguity on the
     * boundary line.
     */
    public static BoundaryVerdict checkLexBoundary(String prefix, EDbVendor vendor) {
        if (prefix == null || prefix.isEmpty()) {
            return BoundaryVerdict.refuse("empty prefix");
        }
        TGSqlParser parser = new TGSqlParser(vendor);
        parser.sqltext = prefix;
        try {
            parser.tokenizeSqltext();
        } catch (Throwable t) {
            return BoundaryVerdict.refuse("tokenization failed: " + t);
        }

        // 1. Coverage: the emitted tokens must reproduce the prefix exactly.
        //    This is the load-bearing unterminatedness detector: an open
        //    string / block comment / bracketed identifier is swallowed into
        //    the lexer's literal buffer instead of being emitted, so the token
        //    stream comes up short (verified empirically for MSSQL: 'abc,
        //    /* xx, [ab; review round 1 additionally verified nested comments,
        //    N'..., smart quotes and double quotes). Lexer end-state fields are
        //    deliberately NOT used: literallen is residual scratch that stays
        //    non-zero after a COMPLETED literal, and yysstate is vacuously 0
        //    because EOF calls yyclear() (TCustomLexer:695).
        StringBuilder covered = new StringBuilder(prefix.length());
        for (int i = 0; i < parser.sourcetokenlist.size(); i++) {
            covered.append(parser.sourcetokenlist.get(i).toString());
        }
        if (!covered.toString().equals(prefix)) {
            return BoundaryVerdict.refuse("token stream does not cover the prefix exactly"
                    + " (unterminated literal/comment/identifier or swallowed text)");
        }

        // 2. Delimiter balance: an unclosed ( or [ lets a hole instantiation
        //    close into prefix structure. Brackets closed within a single
        //    identifier token never appear here — only real punctuation tokens.
        int parenDepth = 0;
        for (int i = 0; i < parser.sourcetokenlist.size(); i++) {
            String t = parser.sourcetokenlist.get(i).toString();
            if ("(".equals(t)) {
                parenDepth++;
            } else if (")".equals(t)) {
                parenDepth--;
            }
            if (parenDepth < 0) {
                return BoundaryVerdict.refuse("unbalanced ')' in prefix");
            }
        }
        if (parenDepth != 0) {
            return BoundaryVerdict.refuse("prefix has " + parenDepth + " unclosed '('");
        }

        // 4. Fusion safety: the hole starts immediately after the prefix, so
        //    the final EMITTED TOKEN must be one the vendor lexer itself
        //    classifies as whitespace/newline, or a comma. Judging by the
        //    lexer's classification, not Character.isWhitespace, closes the
        //    Unicode-whitespace witness from review round 1: ' ' is Java
        //    whitespace but NOT MSSQL lexer whitespace, so 't ' + hole
        //    would fuse into a single identifier.
        // ('(' is intentionally absent: a prefix ending in '(' always fails the
        // balance check above, so it can never be an accepted boundary.)
        TSourceToken lastToken = parser.sourcetokenlist.get(parser.sourcetokenlist.size() - 1);
        boolean lexerBoundary = lastToken.tokentype == ETokenType.ttwhitespace
                || lastToken.tokentype == ETokenType.ttreturn
                || ",".equals(lastToken.toString());
        if (!lexerBoundary) {
            return BoundaryVerdict.refuse("final token '" + lastToken + "' ("
                    + lastToken.tokentype + ") can fuse with hole text");
        }

        // 5. Lexer-mode dependence (design Layer 2, check 7): a double quote
        //    lexes as an identifier or a string depending on the session's
        //    QUOTED_IDENTIFIER setting, which is runtime state we cannot see.
        //    Any double quote in the prefix makes its tokenization
        //    mode-dependent — refuse conservatively.
        if (vendor == EDbVendor.dbvmssql && prefix.indexOf('"') >= 0) {
            return BoundaryVerdict.refuse("double quote in prefix is QUOTED_IDENTIFIER-dependent");
        }

        // 6. MSSQL line-comment ambiguity: TLexerMssql decides whether -- is a
        //    comment or arithmetic by inspecting the WHOLE current line
        //    (TLexerMssql:72), so hole content on the same line can flip the
        //    classification of prefix text. Refuse any -- on the boundary line.
        if (vendor == EDbVendor.dbvmssql) {
            int nl = prefix.lastIndexOf('\n');
            String boundaryLine = nl >= 0 ? prefix.substring(nl + 1) : prefix;
            if (boundaryLine.contains("--")) {
                return BoundaryVerdict.refuse("'--' on the boundary line is hole-content-dependent");
            }
        }
        return BoundaryVerdict.ok();
    }

    /* ---------------------------------------------------- proof-mode parse */

    /** Result of {@link #proofParse}; {@code ok == false} means the proof must refuse. */
    public static final class ProofParseResult {
        public final boolean ok;
        public final int syntaxErrorCount;
        /** Total recovery events: yyparse error handling + CREATE TABLE second-parse recovery. */
        public final int recoveryEvents;
        /**
         * Typed subset of {@link #recoveryEvents}: deterministic
         * keyword-to-identifier rollback attempts. Refused today (sound,
         * conservative); typed separately so a future audited-rewrite
         * refinement can relax it without changing this surface.
         */
        public final int keywordRollbackEvents;
        /** Typed subset: CREATE TABLE / CREATE INDEX trimmed-body reparses (outside yyparse). */
        public final int createTableReparseEvents;
        /** Human-readable refusal cause; {@code null} when ok. */
        public final String reason;

        ProofParseResult(boolean ok, int syntaxErrorCount, int recoveryEvents,
                int keywordRollbackEvents, int createTableReparseEvents, String reason) {
            this.ok = ok;
            this.syntaxErrorCount = syntaxErrorCount;
            this.recoveryEvents = recoveryEvents;
            this.keywordRollbackEvents = keywordRollbackEvents;
            this.createTableReparseEvents = createTableReparseEvents;
            this.reason = reason;
        }

        @Override
        public String toString() {
            return ok ? "ok" : "refused: " + reason
                    + " (errors=" + syntaxErrorCount + ", recovery=" + recoveryEvents
                    + ", keywordRollback=" + keywordRollbackEvents
                    + ", createTableReparse=" + createTableReparseEvents + ")";
        }
    }

    /**
     * Parse {@code sql} with the real vendor pipeline and report whether the
     * parse constitutes proof-grade evidence: zero syntax errors AND zero
     * recovery events. Recovery includes silently-successful keyword rollback
     * — a statement that only parses because a keyword was retried as an
     * identifier is not instantiation-independent evidence.
     */
    public static ProofParseResult proofParse(String sql, EDbVendor vendor) {
        if (sql == null || sql.trim().isEmpty()) {
            return new ProofParseResult(false, 0, 0, 0, 0, "empty sql");
        }
        TGSqlParser parser = new TGSqlParser(vendor);
        parser.sqltext = sql;
        int errors;
        try {
            errors = parser.parse();
        } catch (Throwable t) {
            return new ProofParseResult(false, -1, -1, -1, -1, "parse threw: " + t);
        }
        int recovery = 0;
        int keywordRollback = 0;
        if (parser.fparser != null) {
            recovery += parser.fparser.getProofRecoveryEvents();
            keywordRollback += parser.fparser.getProofKeywordRollbackEvents();
        }
        if (parser.fplsqlparser != null) {
            recovery += parser.fplsqlparser.getProofRecoveryEvents();
            keywordRollback += parser.fplsqlparser.getProofKeywordRollbackEvents();
        }
        int createTableReparse = parser.proofCreateTableReparseEvents;
        recovery += createTableReparse;
        if (errors != 0) {
            return new ProofParseResult(false, errors, recovery, keywordRollback,
                    createTableReparse, "syntax errors");
        }
        if (recovery != 0) {
            return new ProofParseResult(false, errors, recovery, keywordRollback,
                    createTableReparse, "parse needed recovery");
        }
        return new ProofParseResult(true, 0, 0, 0, 0, null);
    }

    /* ------------------------------------------- LR configuration probe */

    /**
     * Run the REAL MSSQL parser over {@code sql} and report the LR automaton's
     * configuration at {@code cutoffOffset} — the state stack the literal
     * prefix committed to, plus every reduction performed before that point.
     *
     * <p>This is the observation half of the commitment check (design R4). It
     * answers "what has the grammar actually committed to here?", which is the
     * question two earlier hand-written schemes got wrong: token adjacency
     * (`hasSolidTokenBetween`) and AST binder-region containment. Neither could
     * see a construct the grammar still allows but the sentinel text does not
     * contain — MSSQL's optional {@code UPDATE ... FROM} being the witness.
     *
     * <p>The real parser is used rather than an offline table simulation on
     * purpose: MSSQL rewrites tokens before the automaton runs
     * ({@code TParserMssqlSql.yyparse}) and reads the token stream from inside
     * semantic actions, so a simulation would diverge precisely on the
     * constructs those hacks exist for.
     *
     * <p>Read-only: the parse proceeds exactly as it otherwise would up to the
     * cutoff, then stops without entering error recovery (recovery unwinds the
     * stack we are reading).
     *
     * @param sql          the materialized site text
     * @param cutoffOffset stop before consuming any token at or beyond this
     *                     character offset — normally the first hole's offset,
     *                     already retreated by the applicable rewrite horizon
     * @return the configuration, or null if the parser never needed a token at
     *         or beyond the cutoff (e.g. the cutoff is past the statement)
     */
    public static TCustomParser.ProofLrConfiguration observeLrConfiguration(String sql,
            long cutoffOffset) {
        if (sql == null || sql.trim().isEmpty()) {
            return null;
        }
        TGSqlParser tokenizer = new TGSqlParser(EDbVendor.dbvmssql);
        tokenizer.sqltext = sql;
        tokenizer.tokenizeSqltext();
        if (tokenizer.sourcetokenlist == null || tokenizer.sourcetokenlist.size() == 0) {
            return null;
        }
        TParserMssqlSql parser = new TParserMssqlSql(tokenizer.sourcetokenlist);
        parser.nf = new gudusoft.gsqlparser.nodes.TNodeFactory(EDbVendor.dbvmssql);
        parser.setProofLrCutoffOffset(cutoffOffset);
        try {
            parser.yyparse();
        } catch (Throwable t) {
            // A throw after the snapshot was taken still yields a usable
            // configuration; before it, null is the honest answer.
            return parser.getProofLrConfiguration();
        }
        return parser.getProofLrConfiguration();
    }

    /* ---------------------------------------------- MSSQL rewrite horizons */

    /**
     * Per-rule forward-window audit of the MSSQL pre-parse machinery (review
     * round 2 replaced the unsound single global {@code W} with this table).
     * A construct reachable by an EXCLUDED rule cannot be proven by token-window
     * retreat at all; the others bound how many solid tokens the stable-region
     * boundary must retreat from the first hole.
     */
    public static final class MssqlRewriteAudit {

        private MssqlRewriteAudit() {
        }

        /** Parser keyword pre-pass (TParserMssqlSql yyparse rewrite): 1 forward solid token. */
        public static final int KEYWORD_PREPASS_WINDOW = 1;
        /** Ordinary raw-statement rewrites (MssqlSqlParser): 1 forward solid token. */
        public static final int RAW_REWRITE_WINDOW = 1;
        /** Statement splitter decisions: up to 2 forward solid tokens. */
        public static final int SPLITTER_WINDOW = 2;
        /**
         * Conservative local constant for the audited ordinary-DML subset:
         * max of the bounded windows above plus one. NOT a global MSSQL
         * constant — constructs reachable by {@link #EXCLUDED_RULES} are out.
         */
        public static final int W_ORDINARY_DML = 3;

        /** How a rule's influence on the token stream is bounded — or not. */
        public enum Enforcement {
            /** Bounded window; covered by the {@code W} retreat. */
            WINDOWED,
            /** Refused today by a harness check (see {@link RewriteRule#note}). */
            REFUSED_BY_HARNESS,
            /**
             * Not yet enforceable here — lands with the commitment check
             * (design R4 step 4). Until then, constructs reachable by this
             * rule must not be treated as provable.
             */
            PENDING_COMMITMENT_CHECK
        }

        /** One audited pre-parse/lexer rule: its forward window, or why it is excluded. */
        public static final class RewriteRule {
            public final String name;
            /** Forward solid-token window; -1 when unbounded/non-token-local. */
            public final int window;
            public final Enforcement enforcement;
            public final String note;

            RewriteRule(String name, int window, Enforcement enforcement, String note) {
                this.name = name;
                this.window = window;
                this.enforcement = enforcement;
                this.note = note;
            }

            public boolean excluded() {
                return window < 0;
            }
        }

        /** The full audited rule table (review round 2). */
        public static final List<RewriteRule> RULES;

        static {
            List<RewriteRule> r = new ArrayList<RewriteRule>();
            r.add(new RewriteRule("parser keyword pre-pass", KEYWORD_PREPASS_WINDOW,
                    Enforcement.WINDOWED, "TParserMssqlSql yyparse rewrite"));
            r.add(new RewriteRule("ordinary raw-statement rewrites", RAW_REWRITE_WINDOW,
                    Enforcement.WINDOWED, "MssqlSqlParser raw pass"));
            r.add(new RewriteRule("statement splitter", SPLITTER_WINDOW,
                    Enforcement.WINDOWED, "raw statement splitting decisions"));
            r.add(new RewriteRule("CREATE TABLE/INDEX second-parse recovery", -1,
                    Enforcement.REFUSED_BY_HARNESS,
                    "outside yyparse; counted via TGSqlParser.proofCreateTableReparseEvents"));
            r.add(new RewriteRule("constraint rewriting", -1,
                    Enforcement.PENDING_COMMITMENT_CHECK,
                    "carries state across unbounded modifier tokens (MssqlSqlParser:408)"));
            r.add(new RewriteRule("EXEC module-number end-of-line scan", -1,
                    Enforcement.PENDING_COMMITMENT_CHECK, "MssqlSqlParser:749"));
            r.add(new RewriteRule("lexer '--' whole-line classification", -1,
                    Enforcement.REFUSED_BY_HARNESS,
                    "TLexerMssql:72; refused by checkLexBoundary boundary-line rule"));
            r.add(new RewriteRule("semantic-action out-of-band reads", -1,
                    Enforcement.PENDING_COMMITMENT_CHECK,
                    "read_to_semicolon / read_to_next_parentheses (TCustomParser:296)"));
            RULES = Collections.unmodifiableList(r);
        }
    }
}