#!/usr/bin/env node
// Check the proofs of the SpellGrid levels (Module 10) with the solver (tools/solver/solve.ts).
//
//   node tools/verify-levels.mjs [level ...] [--proofs <file>] [--dir <dir>]
//   npm run verify:levels
//
// Reads course/10-spellgrid/levels/proofs.json (or --proofs), a list of entries
//   { "level": "l1-double-tap", "shortest": 10, "neverRule": "DEATHRATTLE IS DOUBLE" }
// with `neverRule` and `naiveUnsolvable: true` optional, and checks for each one:
// - a solution exists with exactly `shortest` inputs, and none with fewer;
// - with `neverRule`, the search exhausts every reachable position without a win when
//   every position in which that rule is in force is thrown away (within 60 inputs);
// - with `naiveUnsolvable`, the search exhausts without a win on the engine with the
//   naive aura timing (`--naive`), within 60 inputs.
// `level` arguments pick proofs by level name or prefix (`l4`). The Module 10 TypeScript
// reference is staged once, as solve-spellgrid does, into --dir or a temp directory, and
// the solver runs there, one process per check, several at a time. Prints one line per
// proof; exits 1 if any proof fails.
import { readFileSync } from "node:fs";
import { spawn } from "node:child_process";
import { availableParallelism } from "node:os";
import { join } from "node:path";
import { courseRoot, fail, isMain } from "./lib.mjs";
import { resolveLevel } from "./play-spellgrid.mjs";
import { stageSolver } from "./solve-spellgrid.mjs";

/** How deep a "the search exhausts" check may go before it counts as cut off. */
export const EXHAUST_MAX = 60;
const KEYS = ["level", "shortest", "neverRule", "naiveUnsolvable"];

export function parseArgs(argv) {
  const opts = { levels: [], proofs: null, dir: null };
  for (let i = 0; i < argv.length; i++) {
    if (argv[i] === "--proofs") opts.proofs = argv[++i];
    else if (argv[i] === "--dir") opts.dir = argv[++i];
    else if (argv[i].startsWith("--")) fail(`verify-levels: unknown option ${argv[i]}\nusage: verify-levels.mjs [level ...] [--proofs <file>] [--dir <dir>]`);
    else opts.levels.push(argv[i]);
  }
  return opts;
}

/** What is wrong with a proof entry's shape, or [] if nothing. */
export function proofProblems(proof) {
  const problems = [];
  if (typeof proof !== "object" || proof === null || Array.isArray(proof)) return ["a proof must be an object"];
  for (const key of Object.keys(proof)) if (!KEYS.includes(key)) problems.push(`unknown key "${key}"`);
  if (typeof proof.level !== "string" || proof.level === "") problems.push("level must be a level name");
  if (!Number.isInteger(proof.shortest) || proof.shortest < 1) problems.push("shortest must be a whole number of inputs, at least 1");
  if ("neverRule" in proof && !/^[A-Z]+ IS (NOT )?[A-Z]+$/.test(proof.neverRule)) problems.push('neverRule must be a rule such as "X IS Y"');
  if ("naiveUnsolvable" in proof && proof.naiveUnsolvable !== true) problems.push("naiveUnsolvable must be true or absent");
  return problems;
}

/** The first "solution in N" depth the solver printed, or null. */
const firstSolution = (out) => {
  const m = /^solution in (\d+): (.*)$/m.exec(out);
  return m ? { depth: Number(m[1]), line: m[2] } : null;
};

/** A check that the search ran out of positions without a win; `what` names the restriction. */
const exhausts = (what) => ({ code, out }) => {
  const won = firstSolution(out);
  if (won) return `solved ${what} in ${won.depth} inputs: ${won.line}`;
  if (code === 1 && /^no solution: every reachable position was searched$/m.test(out)) return null;
  if (/^no solution within/m.test(out)) return `the search ${what} was cut off at ${EXHAUST_MAX} inputs, not exhausted`;
  return `the solver failed ${what} (exit ${code}): ${out.trim().split("\n").pop()}`;
};

/** The solver runs a proof needs: the solver's arguments, and a check of its result (an error, or null). */
export function solverRuns(proof) {
  const runs = [
    {
      args: ["--max", String(proof.shortest)],
      check: ({ code, out }) => {
        const won = firstSolution(out);
        if (won === null) return `no solution within ${proof.shortest} inputs${code > 1 ? ` (solver exit ${code})` : ""}`;
        if (won.depth !== proof.shortest) return `a solution in ${won.depth} inputs, shorter than ${proof.shortest}: ${won.line}`;
        return null;
      },
    },
  ];
  if (proof.neverRule !== undefined) {
    runs.push({ args: ["--max", String(EXHAUST_MAX), "--never-rule", proof.neverRule], check: exhausts(`without ${proof.neverRule}`) });
  }
  if (proof.naiveUnsolvable) runs.push({ args: ["--max", String(EXHAUST_MAX), "--naive"], check: exhausts("under --naive") });
  return runs;
}

/** Check one proof. `run(args)` runs the solver on the proof's level and resolves to { code, out }. Resolves to the failures. */
export async function checkProof(proof, run) {
  const problems = proofProblems(proof);
  if (problems.length > 0) return problems;
  const results = await Promise.all(solverRuns(proof).map(async ({ args, check }) => check(await run(args))));
  return results.filter((r) => r !== null);
}

/** One line saying what a proof claims. */
export function describe(proof) {
  const parts = [`shortest ${proof.shortest}`];
  if (proof.neverRule !== undefined) parts.push(`none without ${proof.neverRule}`);
  if (proof.naiveUnsolvable) parts.push("none under --naive");
  return parts.join("; ");
}

/** A function that runs async jobs, at most `n` at a time. */
function limiter(n) {
  let running = 0;
  const waiting = [];
  const next = () => {
    if (running >= n || waiting.length === 0) return;
    running++;
    const { job, done } = waiting.shift();
    job().then((r) => {
      running--;
      done(r);
      next();
    });
  };
  return (job) => new Promise((done) => {
    waiting.push({ job, done });
    next();
  });
}

/** Run the solver in the staged `dir` on the level at `path`. Resolves to { code, out }. */
function solve(dir, path, args) {
  return new Promise((done) => {
    const child = spawn("npx", ["tsx", "solve.ts", path, ...args], { cwd: dir });
    let out = "";
    child.stdout.on("data", (d) => (out += d));
    child.stderr.on("data", (d) => (out += d));
    child.on("close", (code) => done({ code: code ?? 1, out }));
  });
}

async function main() {
  const opts = parseArgs(process.argv.slice(2));
  const proofsPath = opts.proofs ?? join(courseRoot(), "10-spellgrid", "levels", "proofs.json");
  let proofs = JSON.parse(readFileSync(proofsPath, "utf8"));
  if (!Array.isArray(proofs)) fail(`${proofsPath}: expected a list of proofs`);
  if (opts.levels.length > 0) {
    proofs = proofs.filter((p) => opts.levels.some((l) => p.level === l || String(p.level).startsWith(`${l}-`)));
    if (proofs.length === 0) fail(`no proof for ${opts.levels.join(", ")} in ${proofsPath}`);
  }
  const dir = stageSolver(opts.dir);
  const limit = limiter(availableParallelism());
  const checks = proofs.map((proof) => {
    const level = typeof proof.level === "string" ? resolveLevel(join(dir, "levels"), proof.level) : null;
    if (proofProblems(proof).length === 0 && level === null) return [`no level "${proof.level}"`];
    return checkProof(proof, (args) => limit(() => solve(dir, level.path, args)));
  });
  let failed = 0;
  for (const [i, failures] of (await Promise.all(checks)).entries()) {
    const proof = proofs[i];
    if (failures.length === 0) console.log(`ok   ${proof.level}: ${describe(proof)}`);
    else {
      failed++;
      console.log(`FAIL ${proof.level ?? "(no level)"}: ${failures.join("; ")}`);
    }
  }
  console.log(failed === 0 ? `${proofs.length} proofs hold` : `${failed} of ${proofs.length} proofs fail`);
  process.exit(failed === 0 ? 0 : 1);
}

if (isMain(import.meta.url)) main();