import { createHash } from "node:crypto";
import {
  capabilityId,
  type AtomId,
  type Conformance,
  type InterfaceRevision,
  type InterfaceRevisionId,
} from "./types.js";
import {
  GenericTypeError,
  TypeSubstitution,
  bindTypeParameters,
  canonicalTypeArgument,
  type ClosedTypeArgument,
  type GenericTypeEnvironment,
  type InterfaceApplicationExpression,
  type TypeParameter,
} from "./generics.js";

/** Compiler input only. Runtime plans contain ordinary closed conformances. */
export interface ConformanceRule {
  id: string;
  parameters: TypeParameter[];
  source: InterfaceApplicationExpression;
  target: InterfaceApplicationExpression;
}
export interface RuleApplication {
  rule: ConformanceRule;
  atomId: AtomId;
  sourceId: InterfaceRevisionId;
  targetId: InterfaceRevisionId;
  bindings: Map<string, ClosedTypeArgument>;
  id: Conformance["id"];
}
const parameterId = (argument: ConformanceRule["source"]["arguments"][number]) => {
  const value = argument.kind === "value" ? argument.type : argument.target;
  return value.kind === "parameter" ? value.parameterId : undefined;
};
const hasParameter = (node: unknown): boolean =>
  !!node &&
  typeof node === "object" &&
  (("kind" in node && node.kind === "parameter") || Object.values(node).some(hasParameter));

export function validateConformanceRules(
  rules: readonly ConformanceRule[],
  definitions: ReadonlyMap<string, InterfaceRevision>,
) {
  const ids = new Set<string>();
  const graph = new Map<string, ConformanceRule[]>();
  for (const rule of rules) {
    if (ids.has(rule.id)) throw new GenericTypeError("duplicate-rule-id", rule.id, `Duplicate rule ID ${rule.id}`);
    ids.add(rule.id);
    for (const application of [
      rule.source,
      rule.target,
      ...rule.parameters.flatMap((p) => (p.kind === "object" ? p.implements : [])),
    ]) {
      const definition = definitions.get(application.definitionId);
      if (!definition)
        throw new GenericTypeError("unknown-interface", rule.id, `Unknown interface ${application.definitionId}`);
      const parameters = definition.template?.parameters ?? [];
      if (parameters.length !== application.arguments.length)
        throw new GenericTypeError("type-arity", rule.id, `Wrong arity for ${definition.displayName}`);
      parameters.forEach((p, i) => {
        if (p.kind !== application.arguments[i].kind)
          throw new GenericTypeError(
            "parameter-kind",
            rule.id,
            `Wrong argument kind for ${definition.displayName}.${p.name}`,
          );
      });
    }
    const captured = new Set<string>();
    for (const argument of rule.source.arguments) {
      const id = parameterId(argument);
      if (id) captured.add(id);
      else if (hasParameter(argument))
        throw new GenericTypeError(
          "unsupported-rule-pattern",
          rule.id,
          "Capture whole source arguments, not nested type patterns",
        );
    }
    for (const p of rule.parameters)
      if (!captured.has(p.id))
        throw new GenericTypeError(
          "uncaptured-rule-parameter",
          rule.id,
          `Parameter ${p.name} must occur in the source application`,
        );
    graph.set(rule.source.definitionId, [...(graph.get(rule.source.definitionId) ?? []), rule]);
  }
  const visited = new Set<string>();
  const active = new Set<string>();
  const visit = (id: string, trail: string[]) => {
    if (active.has(id))
      throw new GenericTypeError(
        "recursive-conformance-rule",
        trail.at(-1) ?? id,
        `Recursive conformance rules: ${trail.join(" -> ")}`,
      );
    if (visited.has(id)) return;
    active.add(id);
    for (const rule of graph.get(id) ?? []) visit(rule.target.definitionId, [...trail, rule.id]);
    active.delete(id);
    visited.add(id);
  };
  for (const id of graph.keys()) visit(id, []);
}

/** Monotone closure: bounds only enable applications, never invent evidence. */
export function expandConformanceRules(
  rules: readonly ConformanceRule[],
  initial: readonly Pick<Conformance, "atomId" | "interfaceRevisionId">[],
  definitions: ReadonlyMap<string, InterfaceRevision>,
  environment: (atom: AtomId, bindings: Map<string, ClosedTypeArgument>) => GenericTypeEnvironment,
): RuleApplication[] {
  validateConformanceRules(rules, definitions);
  const key = (atom: string, iface: string) => JSON.stringify([atom, iface]);
  const facts = new Map(initial.map((f) => [key(f.atomId, f.interfaceRevisionId), f]));
  const applications = new Map<string, RuleApplication>();
  const implies = (actual: InterfaceRevisionId, required: InterfaceRevisionId, seen = new Set<string>()): boolean => {
    if (actual === required) return true;
    if (seen.has(actual)) return false;
    seen.add(actual);
    return (definitions.get(actual)?.requiredInterfaces ?? []).some((id) => implies(id, required, seen));
  };
  const bySource = new Map<string, ConformanceRule[]>();
  for (const rule of [...rules].sort((a, b) => a.id.localeCompare(b.id)))
    bySource.set(rule.source.definitionId, [...(bySource.get(rule.source.definitionId) ?? []), rule]);
  let changed = true;
  while (changed) {
    changed = false;
    for (const fact of [...facts.values()].sort((a, b) =>
      key(a.atomId, a.interfaceRevisionId).localeCompare(key(b.atomId, b.interfaceRevisionId)),
    )) {
      const definition = definitions.get(fact.interfaceRevisionId);
      if (!definition) continue;
      for (const rule of bySource.get(definition.application?.definitionId ?? definition.revisionId) ?? []) {
        const arguments_ = definition.application?.arguments ?? [];
        const bindings = new Map<string, ClosedTypeArgument>();
        const env = environment(fact.atomId, bindings);
        const substitution = new TypeSubstitution(env);
        if (
          !rule.source.arguments.every((pattern, i) => {
            const actual = arguments_[i];
            if (!actual || actual.kind !== pattern.kind) return false;
            const id = parameterId(pattern);
            if (!id) return canonicalTypeArgument(substitution.argument(pattern)) === canonicalTypeArgument(actual);
            const previous = bindings.get(id);
            if (previous && canonicalTypeArgument(previous) !== canonicalTypeArgument(actual)) return false;
            bindings.set(id, actual);
            return true;
          })
        )
          continue;
        try {
          bindTypeParameters(
            rule.parameters,
            rule.parameters.map((p) => bindings.get(p.id)!),
            {
              ...env,
              implementsInterface: (target, required) =>
                target.kind === "atom"
                  ? facts.has(key(target.atomId, required))
                  : implies(target.interfaceRevisionId, required),
            },
            rule.id,
          );
        } catch (error) {
          if (error instanceof GenericTypeError && ["unsatisfied-bound", "non-storable-argument"].includes(error.code))
            continue;
          throw error;
        }
        const applicationKey = JSON.stringify([rule.id, fact.atomId, fact.interfaceRevisionId]);
        if (applications.has(applicationKey)) continue;
        if (applications.size >= 10000)
          throw new GenericTypeError(
            "rule-expansion-limit",
            rule.id,
            "Conformance rule expansion exceeds 10000 applications",
          );
        const targetId = substitution.application(rule.target);
        const id = capabilityId.conformance(
          `conformance-rule:sha256:${createHash("sha256")
            .update(
              JSON.stringify(["quixos-conformance-rule-v1", rule.id, fact.atomId, fact.interfaceRevisionId, targetId]),
            )
            .digest("hex")}`,
        );
        applications.set(applicationKey, {
          rule,
          atomId: fact.atomId,
          sourceId: fact.interfaceRevisionId,
          targetId,
          bindings,
          id,
        });
        const targetKey = key(fact.atomId, targetId);
        if (!facts.has(targetKey)) {
          facts.set(targetKey, { atomId: fact.atomId, interfaceRevisionId: targetId });
          changed = true;
        }
      }
    }
  }
  return [...applications.values()];
}