// V2b / V2b-T — the type-compatibility engine (`⊑`) seam.
//
// This module owns the single normative compatibility relation `T₁ ⊑ T₂` of
// type-system.md §"Type compatibility" (TYPE-1…TYPE-11) and the per-site
// parse-time diagnostics that report a static mismatch (TYPE-9). The relation
// is the structural-cases engine the parser must decide without falling back
// to AJV; the cases it recognises are closed for theta 1.0 (type-system.md
// §"Structural cases the parser must recognise").
//
// The engine operates over a small `CompatType` model — the resolved shape of
// a type expression for compatibility purposes — and a `TypeEnv` that resolves
// `NamedType`s to their declarations. The declaration kind drives the nominal
// vs transparent split:
//
//   - an object schema (`schema X { ... }`) is **nominal** (TYPE-10): it is
//     `⊑`-related only by name identity (reflexivity), variant-to-union
//     membership, and union widening/distribution — never structurally across
//     the inline/named boundary or across two distinct named schemas;
//   - a type-alias schema (`schema X = R`) is **transparent** (TYPE-11): it is
//     replaced by its right-hand side `R` and the check re-evaluated, recursing
//     through nested aliases until a non-alias form is reached. Aliasing an
//     object schema unfolds to that object schema, which re-enters TYPE-10.
//
// V2b implements the decision procedure: `checkCompatible` decides the
// directed relation `T₁ ⊑ T₂` over the `CompatType` model (TYPE-1…TYPE-11) and
// the three per-site checkers report the parse-time mismatch diagnostics
// (TYPE-9). An operand past the parser's static view (an unresolvable `named`
// reference) yields `"unknown"`, at which point the per-site checkers emit no
// diagnostic and the runtime AJV check is the safety net (type-system.md
// §"Unresolvable operands").

import { type Diagnostic, type SourceRange } from "../diagnostics/diagnostic";

/** The JSON-native primitive type names (type-system.md §"Type System"). */
export type PrimitiveName = "string" | "number" | "integer" | "boolean" | "null";

/**
 * The resolved type shape the compatibility engine operates over. This is a
 * compatibility-purpose projection of a parsed type expression, not the full
 * type AST:
 *
 *   - `prim`    — a primitive type (`string`, `number`, `integer`, `boolean`,
 *                 `null`).
 *   - `literal` — a literal type (`"foo"`, `42`, `true`, `null`); `typesAs`
 *                 records the primitive the literal value statically types as
 *                 in expression position, which drives TYPE-3.
 *   - `named`   — a `NamedType` reference, resolved through `TypeEnv`; an
 *                 object-schema declaration is nominal (TYPE-10), an alias
 *                 declaration is transparent (TYPE-11).
 *   - `array`   — `array<T>`, covariant in its `element` (TYPE-7).
 *   - `union`   — `T₁ | T₂ | …`, widening (TYPE-5) and distributive (TYPE-6).
 *   - `object`  — an inline anonymous object type `{ f: T, … }`, field-wise
 *                 with an exact field set (TYPE-8).
 */
export type CompatType =
  | { readonly kind: "prim"; readonly name: PrimitiveName }
  | { readonly kind: "literal"; readonly typesAs: PrimitiveName }
  | { readonly kind: "named"; readonly name: string }
  | { readonly kind: "array"; readonly element: CompatType }
  | { readonly kind: "union"; readonly arms: readonly CompatType[] }
  | {
      readonly kind: "object";
      readonly fields: readonly { readonly name: string; readonly type: CompatType }[];
    };

/**
 * A `NamedType` declaration, as seen by the compatibility engine:
 *
 *   - `object-schema` — `schema X { ... }`. Nominal (TYPE-10): related only by
 *     name identity, variant-to-union, and union widening/distribution.
 *   - `alias`         — `schema X = R`. Transparent (TYPE-11): replaced by `rhs`
 *     and the check re-evaluated, recursing through nested aliases. The alias
 *     is identified solely by the `=` form, not by what `rhs` resolves to.
 */
export type NamedDecl =
  | { readonly kind: "object-schema" }
  | { readonly kind: "alias"; readonly rhs: CompatType };

/** Resolves a `NamedType` name to its declaration; `undefined` if unresolvable. */
export type TypeEnv = Readonly<Record<string, NamedDecl>>;

/**
 * The outcome of a directed compatibility check `sub ⊑ sup`:
 *
 *   - `"compatible"`        — the relation holds.
 *   - `"incompatible"`      — a static mismatch (`sub ⋢ sup`), both operands
 *                             statically resolvable.
 *   - `"integer-narrowing"` — a static mismatch specifically because a `number`
 *                             appears where an `integer` is expected; the
 *                             `integer → number` widening is one-way (TYPE-2),
 *                             and the reverse is the `theta/parse/integer-narrowing`
 *                             case.
 *   - `"unknown"`           — the V2b-T stub sentinel. The paired V2b engine
 *                             never returns this; it exists only so every
 *                             relation test reds on its own primary assertion
 *                             (no expected outcome equals `"unknown"`).
 */
export type Compatibility =
  | "compatible"
  | "incompatible"
  | "integer-narrowing"
  | "unknown";

/**
 * Decide the directed compatibility relation `sub ⊑ sup` over the resolved
 * `CompatType` model, per type-system.md §"Type compatibility" TYPE-1…TYPE-11.
 * `env` resolves `NamedType`s to their declarations (nominal object schema vs
 * transparent alias).
 *
 * V2b-T stubs this as an inert sentinel returning `"unknown"`; the paired V2b
 * implementation leaf computes the relation.
 */
export function checkCompatible(
  sub: CompatType,
  sup: CompatType,
  env: TypeEnv,
): Compatibility {
  return decide(unfoldAlias(sub, env), unfoldAlias(sup, env), env);
}

/**
 * TYPE-11 — transparently unfold a `named` type whose declaration is a
 * type-alias schema (`schema X = R`) to its right-hand side, recursing through
 * nested aliases until a non-alias form is reached. A `named` that resolves to
 * an object schema stays `named` (nominal, TYPE-10); an unresolvable `named`
 * (past the parser's static view) stays `named` so the relation reports
 * `"unknown"` and the runtime AJV safety net applies.
 */
function unfoldAlias(type: CompatType, env: TypeEnv): CompatType {
  let current = type;
  // Bounded by the alias chain length; alias cycles are rejected upstream
  // (`theta/parse/type-alias-cycle`) before any compatibility question arises.
  while (current.kind === "named") {
    const decl = env[current.name];
    if (decl === undefined || decl.kind !== "alias") {
      return current;
    }
    current = decl.rhs;
  }
  return current;
}

/**
 * The directed decision procedure over alias-unfolded operands. Implements
 * TYPE-1…TYPE-10 (TYPE-11 transparency is applied by `unfoldAlias` before and
 * during recursion). Returns `"unknown"` when an operand is an unresolvable
 * `named` reference past the parser's static view.
 */
function decide(sub: CompatType, sup: CompatType, env: TypeEnv): Compatibility {
  // TYPE-6 — union-distributive on the left: `T₁ | T₂ ⊑ T₃` iff each arm is.
  if (sub.kind === "union") {
    let sawUnknown = false;
    for (const arm of sub.arms) {
      const r = decide(unfoldAlias(arm, env), sup, env);
      if (r === "unknown") {
        sawUnknown = true;
      } else if (r !== "compatible") {
        return "incompatible";
      }
    }
    return sawUnknown ? "unknown" : "compatible";
  }

  // TYPE-5 — union-widening on the right: `T ⊑ T | U` iff `T ⊑` some arm.
  if (sup.kind === "union") {
    let sawUnknown = false;
    for (const arm of sup.arms) {
      const r = decide(sub, unfoldAlias(arm, env), env);
      if (r === "compatible") {
        return "compatible";
      }
      if (r === "unknown") {
        sawUnknown = true;
      }
    }
    return sawUnknown ? "unknown" : "incompatible";
  }

  // TYPE-7 — element-wise covariance on arrays: `array<T₁> ⊑ array<T₂>` iff
  // `T₁ ⊑ T₂`.
  if (sup.kind === "array") {
    if (sub.kind !== "array") {
      return "incompatible";
    }
    return decide(unfoldAlias(sub.element, env), unfoldAlias(sup.element, env), env);
  }

  // TYPE-8 — field-wise on inline object types with an exact field set
  // (`additionalProperties:false` ⇒ no excess-property widening), field order
  // irrelevant. Never crosses the inline/named boundary (TYPE-10).
  if (sup.kind === "object") {
    if (sub.kind !== "object") {
      return "incompatible";
    }
    if (sub.fields.length !== sup.fields.length) {
      return "incompatible";
    }
    let sawUnknown = false;
    for (const supField of sup.fields) {
      const subField = sub.fields.find((f) => f.name === supField.name);
      if (subField === undefined) {
        return "incompatible";
      }
      const r = decide(
        unfoldAlias(subField.type, env),
        unfoldAlias(supField.type, env),
        env,
      );
      if (r === "unknown") {
        sawUnknown = true;
      } else if (r !== "compatible") {
        return "incompatible";
      }
    }
    return sawUnknown ? "unknown" : "compatible";
  }

  // TYPE-10 — object-schema named types are nominal: a `named` (resolved to an
  // object schema, since aliases are unfolded) is `⊑` only the same named
  // schema by name identity (TYPE-1). It never relates structurally to an
  // inline object or to a distinct named schema.
  if (sup.kind === "named") {
    if (env[sup.name] === undefined) {
      return "unknown";
    }
    if (sub.kind === "named") {
      if (env[sub.name] === undefined) {
        return "unknown";
      }
      return sub.name === sup.name ? "compatible" : "incompatible";
    }
    return "incompatible";
  }

  // A `named` sub against a non-named, non-union sup: nominal, never structural.
  if (sub.kind === "named") {
    return env[sub.name] === undefined ? "unknown" : "incompatible";
  }

  // TYPE-2 / TYPE-3 — primitive and literal-to-primitive against a primitive
  // target. A literal types as its `typesAs` primitive in expression position.
  if (sup.kind === "prim") {
    if (sub.kind === "prim") {
      return decidePrimitive(sub.name, sup.name);
    }
    if (sub.kind === "literal") {
      return decidePrimitive(sub.typesAs, sup.name);
    }
    return "incompatible";
  }

  // TYPE-1 reflexivity for a literal target: a literal is `⊑` a literal that
  // types as the same primitive.
  if (sup.kind === "literal") {
    if (sub.kind === "literal") {
      return decidePrimitive(sub.typesAs, sup.typesAs);
    }
    return "incompatible";
  }

  return "incompatible";
}

/**
 * Decide compatibility between two primitive type names (TYPE-1 reflexivity,
 * TYPE-2 one-way `integer ⊑ number` widening, and the reverse
 * `number ⊑ integer` `integer-narrowing` case).
 */
function decidePrimitive(sub: PrimitiveName, sup: PrimitiveName): Compatibility {
  if (sub === sup) {
    return "compatible";
  }
  if (sub === "integer" && sup === "number") {
    return "compatible";
  }
  if (sub === "number" && sup === "integer") {
    return "integer-narrowing";
  }
  return "incompatible";
}

/**
 * Render a `CompatType` to the display name the per-site mismatch messages
 * interpolate (the `<expected>` / `<actual>` fields of the
 * diagnostics/code-registry-parse.md *Message* strings).
 */
export function displayType(type: CompatType): string {
  switch (type.kind) {
    case "prim":
      return type.name;
    case "literal":
      return type.typesAs;
    case "named":
      return type.name;
    case "array":
      return `array<${displayType(type.element)}>`;
    case "union":
      return type.arms.map(displayType).join(" | ");
    case "object":
      return `{ ${type.fields.map((f) => `${f.name}: ${displayType(f.type)}`).join(", ")} }`;
  }
}

/** A located site at which a compatibility check reports a parse-time diagnostic. */
export interface CompatSite {
  readonly file: string;
  readonly range: SourceRange;
}

/**
 * How an indexed-access receiver `a` in `a[k]` types statically
 * (expressions.md §"Supported forms"): only `array<T>` and object values are
 * indexable.
 *
 *   - `"array"`     — an `array<T>`, indexable by integer position;
 *   - `"object"`    — an object value (a nominal `object-schema` `NamedType`,
 *                     an alias transparently resolving to one, or an inline
 *                     object type), indexable by `string` theta-side name;
 *   - `"primitive"` — a `string` / `number` / `integer` / `boolean` / `null`
 *                     receiver, which is not indexable
 *                     (`theta/parse/non-indexable-receiver`);
 *   - `"unknown"`   — statically unresolvable past the parser's view (an
 *                     unresolved `NamedType`, a union): deferred to the runtime
 *                     safety net, raising no `type`-phase diagnostic.
 */
export type IndexReceiverKind = "array" | "object" | "primitive" | "unknown";

/**
 * Classify an indexed-access receiver's static type as `array<T>`, an object
 * value, a non-indexable primitive, or statically-unknown. A `NamedType`
 * resolves through `env`: a nominal `object-schema` declaration is an object
 * value, a transparent `alias` is classified by its RHS (TYPE-11), and an
 * unresolved name is `"unknown"` (deferred to the runtime safety net).
 */
export function classifyIndexReceiver(
  type: CompatType,
  env: TypeEnv,
): IndexReceiverKind {
  switch (type.kind) {
    case "array":
      return "array";
    case "object":
      return "object";
    case "prim":
    case "literal":
      return "primitive";
    case "union":
      return "unknown";
    case "named": {
      const decl = env[type.name];
      if (decl === undefined) {
        return "unknown";
      }
      if (decl.kind === "object-schema") {
        return "object";
      }
      // A transparent alias: classify its resolved RHS (TYPE-11).
      return classifyIndexReceiver(decl.rhs, env);
    }
  }
}

/**
 * TYPE-9 — the RHS of a typed binding `let x: T = expr`. Reports
 * `theta/parse/let-rhs-type-mismatch` when the RHS static type is not `⊑` the
 * annotation `T` (both statically resolvable), or `theta/parse/integer-narrowing`
 * when the failure is specifically a `number` RHS under an `integer` annotation
 * (TYPE-2's one-way widening). Returns no diagnostic when the relation holds.
 *
 * V2b-T stubs this inert (no diagnostics); the paired V2b leaf fills it in.
 */
export function checkLetRhsCompat(opts: {
  readonly name: string;
  readonly annotation: CompatType;
  readonly rhs: CompatType;
  readonly env: TypeEnv;
  readonly site: CompatSite;
}): Diagnostic[] {
  const { name, annotation, rhs, env, site } = opts;
  const r = checkCompatible(rhs, annotation, env);
  if (r === "compatible" || r === "unknown") {
    // Compatible, or statically unresolvable — the latter defers to the runtime
    // AJV safety net (type-system.md §"Unresolvable operands").
    return [];
  }
  if (r === "integer-narrowing") {
    // TYPE-2 — a `number` RHS under an `integer` annotation. Message from
    // diagnostics/code-registry-parse.md.
    return [
      {
        severity: "error",
        code: "theta/parse/integer-narrowing",
        file: site.file,
        range: site.range,
        message: "cannot narrow number to integer",
      },
    ];
  }
  // TYPE-9 — incompatible RHS. Message from diagnostics/code-registry-parse.md.
  return [
    {
      severity: "error",
      code: "theta/parse/let-rhs-type-mismatch",
      file: site.file,
      range: site.range,
      message: `let binding '${name}' initialiser type mismatch: expected ${displayType(
        annotation,
      )}, got ${displayType(rhs)}`,
    },
  ];
}

/**
 * TYPE-9 — a plain top-level `fn` argument slot. Reports
 * `theta/parse/fn-arg-type-mismatch` when the argument's static type is not `⊑`
 * the matched parameter's declared type (both statically resolvable). Returns
 * no diagnostic when the relation holds.
 *
 * V2b-T stubs this inert (no diagnostics); the paired V2b leaf fills it in.
 */
export function checkFnArgCompat(opts: {
  readonly fnName: string;
  readonly index: number;
  readonly paramName: string;
  readonly paramType: CompatType;
  readonly argType: CompatType;
  readonly env: TypeEnv;
  readonly site: CompatSite;
}): Diagnostic[] {
  const { fnName, index, paramName, paramType, argType, env, site } = opts;
  const r = checkCompatible(argType, paramType, env);
  if (r === "compatible" || r === "unknown") {
    return [];
  }
  // TYPE-9 — a plain `fn` argument slot mismatch (a `number⊑integer` narrowing
  // is equally a mismatch here; TYPE-9 routes both through fn-arg-type-mismatch).
  // Message from diagnostics/code-registry-parse.md.
  return [
    {
      severity: "error",
      code: "theta/parse/fn-arg-type-mismatch",
      file: site.file,
      range: site.range,
      message: `fn '${fnName}' argument ${index} ('${paramName}') type mismatch: expected ${displayType(
        paramType,
      )}, got ${displayType(argType)}`,
    },
  ];
}

/**
 * TYPE-9 — the array-and-ternary common-type machinery. Given the branch
 * element types (ternary branches or array-literal elements) and an optional
 * in-scope element `sink`:
 *
 *   - with a `sink`: reports `theta/parse/array-element-type-mismatch` at the
 *     first branch whose type is not `⊑` the sink's element type;
 *   - without a `sink`: reports `theta/parse/array-no-common-type` when the
 *     branches share no common type that narrows them.
 *
 * Returns no diagnostic when the branches resolve against the sink (or share a
 * common type). V2b-T stubs this inert (no diagnostics); the paired V2b leaf
 * fills it in.
 */
export function checkCommonType(opts: {
  readonly branches: readonly CompatType[];
  readonly sink: CompatType | undefined;
  readonly env: TypeEnv;
  readonly site: CompatSite;
}): Diagnostic[] {
  const { branches, sink, env, site } = opts;

  // With an in-scope sink: each branch must be `⊑` the sink's element type.
  // Report the first branch that fails (skipping statically-unresolvable
  // branches, which the runtime AJV safety net covers).
  if (sink !== undefined) {
    for (let i = 0; i < branches.length; i++) {
      const branch = branches[i] as CompatType;
      const r = checkCompatible(branch, sink, env);
      if (r === "compatible" || r === "unknown") {
        continue;
      }
      // Message from diagnostics/code-registry-parse.md.
      return [
        {
          severity: "error",
          code: "theta/parse/array-element-type-mismatch",
          file: site.file,
          range: site.range,
          message: `array element type mismatch at index ${i}: expected ${displayType(
            sink,
          )}, got ${displayType(branch)}`,
        },
      ];
    }
    return [];
  }

  // Without a sink: the branches need a common type — a branch every other
  // branch is `⊑` (the array/ternary LUB). Fewer than two branches trivially
  // share one.
  if (branches.length < 2 || hasCommonType(branches, env)) {
    return [];
  }
  // Message from diagnostics/code-registry-parse.md.
  return [
    {
      severity: "error",
      code: "theta/parse/array-no-common-type",
      file: site.file,
      range: site.range,
      message:
        "array elements have no common type; annotate the binding with array<A | B> or use a single schema",
    },
  ];
}

/**
 * Whether the branch types share a common type that narrows them: some branch
 * `C` such that every branch is `⊑ C`. A statically-unresolvable branch is
 * treated as not blocking a candidate (deferred to the runtime AJV safety net).
 */
function hasCommonType(branches: readonly CompatType[], env: TypeEnv): boolean {
  return branches.some((candidate) =>
    branches.every((branch) => {
      const r = checkCompatible(branch, candidate, env);
      return r === "compatible" || r === "unknown";
    }),
  );
}