import fc, { type Arbitrary } from "fast-check";
import {
  PROPERTY_INVARIANT_CLASSES,
  type PropertyExecutionRecord,
  type PropertyInvariantClass,
  type PropertyInvariantResult,
} from "./types.js";

const DEFAULT_NUM_RUNS = 100;
const DEFAULT_SEED = 0x1a2b_3c4d;

export type PropertyInvariantSpec<TInput, TState, TAction = never> = {
  id: string;
  invariantClass: PropertyInvariantClass;
  arbitrary: Arbitrary<TInput>;
  initialState: (input: TInput) => TState;
  check: (state: TState, input: TInput) => void;
  actions?: Arbitrary<TAction[]>;
  apply?: (state: TState, action: TAction, input: TInput) => TState;
  numRuns?: number;
  seed?: number;
  path?: string;
};

function assertNonEmptyString(value: string, field: string): void {
  if (value.trim().length === 0) {
    throw new Error(`${field} must be a non-empty string`);
  }
}

function assertInvariantClass(value: string): asserts value is PropertyInvariantClass {
  if (!(PROPERTY_INVARIANT_CLASSES as readonly string[]).includes(value)) {
    throw new Error(`unknown invariant class: ${value}`);
  }
}

function validatePropertySpec<TInput, TState, TAction>(
  spec: PropertyInvariantSpec<TInput, TState, TAction>,
): void {
  assertNonEmptyString(spec.id, "id");
  assertInvariantClass(spec.invariantClass);
  if (spec.actions !== undefined && spec.apply === undefined) {
    throw new Error("apply is required when actions are provided");
  }
  if (spec.apply !== undefined && spec.actions === undefined) {
    throw new Error("actions are required when apply is provided");
  }
}

function cloneValue<T>(value: T): T {
  if (typeof structuredClone === "function") {
    return structuredClone(value);
  }
  return JSON.parse(JSON.stringify(value)) as T;
}

function applyActions<TInput, TState, TAction>(
  initialState: TState,
  input: TInput,
  actions: TAction[],
  apply: (state: TState, action: TAction, input: TInput) => TState,
): TState {
  let state = initialState;
  for (const action of actions) {
    state = apply(state, action, input);
  }
  return state;
}

function buildExecutionRecord(
  input: unknown,
  initialState: unknown,
  actions: unknown[],
  finalState: unknown,
  seed: number,
  shrinkPath: string | null,
  counterexample: unknown,
): PropertyExecutionRecord {
  return {
    generatedInput: cloneValue(input),
    initialState: cloneValue(initialState),
    actionSequence: cloneValue(actions),
    finalState: cloneValue(finalState),
    seed,
    shrinkPath,
    minimalCounterexample: cloneValue(counterexample),
  };
}

function runDetailsToRecord<TInput, TState, TAction>(
  counterexample: [TInput, TAction[]],
  spec: PropertyInvariantSpec<TInput, TState, TAction>,
  seed: number,
  shrinkPath: string | null,
): PropertyExecutionRecord {
  const [input, actions] = counterexample;
  const initialState = spec.initialState(input);
  const finalState =
    spec.apply !== undefined
      ? applyActions(initialState, input, actions, spec.apply)
      : initialState;
  return buildExecutionRecord(
    input,
    initialState,
    actions,
    finalState,
    seed,
    shrinkPath,
    counterexample,
  );
}

function successRecord(
  input: unknown,
  initialState: unknown,
  actions: unknown[],
  finalState: unknown,
  seed: number,
): PropertyExecutionRecord {
  return {
    generatedInput: cloneValue(input),
    initialState: cloneValue(initialState),
    actionSequence: cloneValue(actions),
    finalState: cloneValue(finalState),
    seed,
    shrinkPath: null,
    minimalCounterexample: null,
  };
}

export function runPropertyInvariant<TInput, TState, TAction = never>(
  spec: PropertyInvariantSpec<TInput, TState, TAction>,
): PropertyInvariantResult {
  validatePropertySpec(spec);

  const seed = spec.seed ?? DEFAULT_SEED;
  const numRuns = spec.numRuns ?? DEFAULT_NUM_RUNS;
  const actionsArbitrary = spec.actions ?? fc.constant([] as TAction[]);

  const property = fc.property(
    spec.arbitrary,
    actionsArbitrary,
    (input, actions) => {
      const initialState = spec.initialState(input);
      const finalState =
        spec.apply !== undefined
          ? applyActions(initialState, input, actions, spec.apply)
          : initialState;
      spec.check(finalState, input);
    },
  );

  const details = fc.check(property, {
    numRuns,
    seed,
    ...(spec.path !== undefined ? { path: spec.path } : {}),
  });

  if (details.failed) {
    const counterexample = details.counterexample as [TInput, TAction[]];
    const executionRecord = runDetailsToRecord(
      counterexample,
      spec,
      details.seed,
      details.counterexamplePath,
    );
    const error =
      details.errorInstance instanceof Error
        ? details.errorInstance.message
        : String(details.errorInstance);
    return {
      id: spec.id,
      invariantClass: spec.invariantClass,
      holds: false,
      executionRecord,
      error,
    };
  }

  const sample = fc.sample(
    fc.tuple(spec.arbitrary, actionsArbitrary),
    { numRuns: 1, seed },
  )[0];
  const input = sample?.[0];
  if (input === undefined) {
    throw new Error("property invariant produced no sample input");
  }
  const actions = sample?.[1] ?? ([] as TAction[]);
  const initialState = spec.initialState(input);
  const finalState =
    spec.apply !== undefined
      ? applyActions(initialState, input, actions, spec.apply)
      : initialState;

  return {
    id: spec.id,
    invariantClass: spec.invariantClass,
    holds: true,
    executionRecord: successRecord(input, initialState, actions, finalState, details.seed),
  };
}

export function replayPropertyExecution<TInput, TState, TAction = never>(
  spec: PropertyInvariantSpec<TInput, TState, TAction>,
  record: PropertyExecutionRecord,
): PropertyInvariantResult {
  validatePropertySpec(spec);
  if (record.shrinkPath === null || record.shrinkPath.length === 0) {
    throw new Error("execution record is missing shrink path required for replay");
  }

  return runPropertyInvariant({
    ...spec,
    seed: record.seed,
    path: record.shrinkPath,
    numRuns: 1,
  });
}