// feynman <command> [specs…] [flags]
import { parseArgs } from "node:util";
import type { Bounds } from "../check/index.ts";
import { checkCommand, type CheckOptions } from "./check.ts";
import { context, diffCommand, list, lockCommand, runCommand } from "./commands.ts";
import { conformCommand } from "./conform.ts";
import { red } from "./format.ts";
import manifest from "../../package.json" with { type: "json" };

export const USAGE = `feynman: executable specs of how a system behaves.

Usage: feynman <command> [spec…] [flags]

Specs are TypeScript files in specs/ next to any package.json (or listed in
feynman.config.ts). Name them by path or by file name; by default all of them.

Commands:
  version                  The version of feynman (also --version, -v).
  list                     The specs in this repository.
  run [spec] [--scenario NAME | --all]
                           Run scenarios: one prints its trace; several, how each ended
                           (--all prints every trace).
  check [spec]             Explore every interleaving within bounds; check properties
                           (safety and liveness), that nothing gets stuck, scenarios,
                           and that every source still resolves.
      --depth N --max-states N --time-limit SECONDS
      --memory-limit GB          stop, keeping the verdicts so far, past this much memory (50% of the machine's)
      --instances Actor=N,Actor=N
      --walks N --walk-depth N   random runs past the depth (0 to turn off)
      --no-symmetry              keep interchangeable instances apart
      --symmetry-checks N        merged twins to test a symmetry claim on (2000; 0 trusts it)
      --only P,Q                 check and show only these properties
      --without R,S              the design without these rules (check and run; RFD0010)
      --set NAME=VALUE           start a model variable at another value: --set faults=2 raises a budget (check and run)
      --no-rules                 skip checking that each rule is needed
      --brief                    verdicts and counterexample sizes, without traces
      --json                     the whole result as JSON, for scripts and agents
      --as-scenario              with --only P: P's counterexample as defineScenario code
  conform <spec> <log.jsonl>
                           Whether a log of what the system did is a run of the spec: the
                           reading that fits, and the properties it breaks; or the line
                           where it leaves the spec. One JSON event per line (RFD0016).
      --gap N                    steps the log does not show, between two it does (4)
      --unlogged A,B             actors whose steps the log does not record
      --logs-faults              the log records faults too (by default, a loss leaves no line)
      --instances, --set, --max-states, --json as for check
      --as-scenario              the run the log is, as defineScenario code
    A trace works too: OpenTelemetry (OTLP JSON, as the collector's file exporter writes and
    Tempo answers), Jaeger's JSON, or Zipkin's. A span with a feynman.step attribute is a step.
      --map map.ts               a module mapping the other spans to steps (defineTraceMapping)
      --trace ID                 only this trace, of the ones in the file
      --order time               trust the clocks; by default, only each instance's order and
                                 what caused what, and any order of the steps that keeps both
  lock                     Record the code each source stands for in feynman.lock.
  diff [spec] [--base REF] Compare every scenario's trace with REF (default: main).
  dev [--port N]           Serve the explorer on the first free port from N (default: 4321).
  build [--out FILE|DIR/]  Write the explorer as one self-contained HTML file, with .gz
                           and .br next to it (default: .feynman/index.html; a directory
                           gets index.html).
  open                     Build, then open that file.
`;

const ARGS = {
  allowPositionals: true,
  options: {
    help: { type: "boolean", short: "h" },
    scenario: { type: "string" },
    all: { type: "boolean" },
    without: { type: "string" },
    set: { type: "string", multiple: true },
    "no-rules": { type: "boolean" },
    depth: { type: "string" },
    "max-states": { type: "string" },
    "memory-limit": { type: "string" },
    "time-limit": { type: "string" },
    walks: { type: "string" },
    "walk-depth": { type: "string" },
    "no-symmetry": { type: "boolean" },
    "symmetry-checks": { type: "string" },
    instances: { type: "string" },
    base: { type: "string" },
    port: { type: "string" },
    out: { type: "string" },
    only: { type: "string" },
    brief: { type: "boolean" },
    json: { type: "boolean" },
    "as-scenario": { type: "boolean" },
    gap: { type: "string" },
    unlogged: { type: "string" },
    "logs-faults": { type: "boolean" },
    map: { type: "string" },
    trace: { type: "string" },
    order: { type: "string" },
  },
} as const;

/** The command line after the command; a mistyped option is the user's error, not a crash. */
function parsed(args: string[]) {
  try {
    return parseArgs({ args, ...ARGS });
  } catch (error) {
    const code = (error as { code?: string }).code;
    if (!code?.startsWith("ERR_PARSE_ARGS")) throw error;
    const option = /'(-[^']*)'/.exec((error as Error).message)?.[1];
    throw new Error(code === "ERR_PARSE_ARGS_UNKNOWN_OPTION" && option ? `Unknown option ${option}. \`feynman help\` lists the options.` : `${(error as Error).message.split(". ")[0]}. \`feynman help\` lists the options.`);
  }
}

export async function main(argv: string[], cwd = process.cwd()): Promise<number> {
  const [command, ...rest] = argv;
  if (!command || command === "help" || command === "--help" || command === "-h") {
    console.log(USAGE);
    return 0;
  }
  if (command === "version" || command === "--version" || command === "-v") {
    console.log(manifest.version);
    return 0;
  }
  const { values, positionals } = parsed(rest);
  if (values.help) {
    console.log(USAGE);
    return 0;
  }
  const ctx = await context(cwd);

  switch (command) {
    case "list":
      return list(ctx);
    case "run":
      return runCommand(ctx, positionals, values.scenario, values.all === true, ids(values.without), settings(values.set));
    case "check":
      return checkCommand(ctx, positionals, { bounds: bounds(values), only: ids(values.only), output: output(values), without: ids(values.without), set: settings(values.set), rules: values["no-rules"] !== true });
    case "conform": {
      const b = bounds(values);
      const out = output(values);
      if (out === "brief") throw new Error("--brief is for check; conform's text is brief already");
      const gap = values.gap === undefined ? undefined : Number(values.gap);
      if (gap !== undefined && (!Number.isInteger(gap) || gap < 0)) throw new Error(`--gap takes a whole number, not ${values.gap}`);
      return conformCommand(ctx, positionals, { instances: b.instances, maxStates: b.maxStates, gap, unlogged: ids(values.unlogged), logsFaults: values["logs-faults"] === true, set: settings(values.set), output: out, map: values.map, trace: values.trace, order: orderOf(values.order) });
    }
    case "lock":
      return lockCommand(ctx);
    case "diff":
      return diffCommand(ctx, positionals, values.base ?? "main");
    case "dev":
      return (await serve()).devCommand(ctx, { port: Number(values.port ?? 4321), base: values.base });
    case "build":
      return (await serve()).buildCommand(ctx, { out: values.out, base: values.base });
    case "open":
      return (await serve()).buildCommand(ctx, { out: values.out, base: values.base, open: true });
    default:
      console.error(red(`Unknown command ${command}.`));
      console.error(USAGE);
      return 2;
  }
}

/** `--set faults=2 --set mode=fast`: each value as JSON when it is JSON (2, true, "x", [1]), else as text. */
function settings(raw: string[] | undefined): Record<string, unknown> {
  const out: Record<string, unknown> = {};
  for (const item of raw ?? []) {
    const at = item.indexOf("=");
    if (at <= 0) throw new Error(`--set takes name=value, like --set faults=2: not ${item}`);
    const text = item.slice(at + 1);
    let value: unknown = text;
    try {
      value = JSON.parse(text);
    } catch {
      // Not JSON: the text itself.
    }
    out[item.slice(0, at)] = value;
  }
  return out;
}

function ids(raw: string | undefined): string[] {
  return (raw ?? "").split(",").map((s) => s.trim()).filter(Boolean);
}

function output(values: { brief?: boolean; json?: boolean; "as-scenario"?: boolean }): CheckOptions["output"] {
  const chosen = (["brief", "json", "as-scenario"] as const).filter((flag) => values[flag]);
  if (chosen.length > 1) throw new Error(`--${chosen.join(" and --")} are different outputs: choose one`);
  return ({ brief: "brief", json: "json", "as-scenario": "scenario" } as const)[chosen[0]] ?? "text";
}

function bounds(values: Record<string, string | string[] | boolean | undefined>): Partial<Bounds> {
  const out: Partial<Bounds> = {};
  const int = (name: string) => {
    const raw = values[name];
    if (raw === undefined) return undefined;
    const n = Number(raw);
    if (!Number.isInteger(n) || n < 0) throw new Error(`--${name} takes a whole number, not ${raw}`);
    return n;
  };
  if (int("depth") !== undefined) out.depth = int("depth");
  if (int("max-states") !== undefined) out.maxStates = int("max-states");
  if (int("time-limit") !== undefined) out.timeLimit = int("time-limit")! * 1000;
  if (values["memory-limit"] !== undefined) {
    const gb = Number(values["memory-limit"]);
    if (!(gb > 0)) throw new Error(`--memory-limit takes gigabytes, like --memory-limit 16: got ${values["memory-limit"]}`);
    out.memoryLimit = Math.floor(gb * 1024);
  }
  if (int("walks") !== undefined) out.walks = int("walks");
  if (int("walk-depth") !== undefined) out.walkDepth = int("walk-depth");
  if (values["no-symmetry"]) out.symmetry = false;
  if (int("symmetry-checks") !== undefined) out.symmetryChecks = int("symmetry-checks");
  if (typeof values.instances === "string") {
    out.instances = Object.fromEntries(
      values.instances.split(",").map((pair) => {
        const [actor, n] = pair.split("=");
        if (!actor?.trim() || n === undefined || n.trim() === "" || !Number.isInteger(Number(n)) || Number(n) < 0) throw new Error(`--instances takes Actor=N pairs, N a whole number, like --instances Person=3: not ${pair}`);
        return [actor.trim(), Number(n)];
      }),
    );
  }
  return out;
}

/** The explorer's commands, loaded when one runs: they bring Vite, compression and a file watcher, which check and run do without. */
const serve = () => import("./serve.ts");

function orderOf(value: string | undefined): "causal" | "time" | undefined {
  if (value === undefined || value === "causal" || value === "time") return value;
  throw new Error(`--order is causal or time, not ${value}`);
}