unify

tcmts.core.shape.unify · #gyghu4nl · term · runs anywhere

import { key } from "#codebase/tcmts/core/shape";
import type { Shape, Subst } from "#codebase/tcmts/core/shape";

export function unify(a: Shape, b: Shape, s: Subst): boolean {
  if (a.k === "var" && b.k === "var") {
    const qa = s.q.get(a.i);
    const db = s.d.get(b.i);
    if (qa) return qa.k === "var" && qa.i === b.i;
    if (db) return db.k === "var" && db.i === a.i;
    s.q.set(a.i, b);
    s.d.set(b.i, a);
    return true;
  }
  if (a.k === "var") {
    const bound = s.q.get(a.i);
    if (bound) return key(bound) === key(b);
    s.q.set(a.i, b);
    s.cost += 2;
    s.notes.add("more specific");
    return true;
  }
  if (b.k === "var") {
    const bound = s.d.get(b.i);
    if (bound) return key(bound) === key(a);
    s.d.set(b.i, a);
    s.cost += 2;
    s.notes.add("more general");
    return true;
  }
  // a type too deep to describe (or a conditional or mapped type) only matches another one
  if (a.k === "opaque" || b.k === "opaque") {
    if (a.k !== b.k) return false;
    s.cost += 1;
    s.notes.add("partly compared");
    return true;
  }
  if (a.k !== b.k) return false;
  const all = (xs: Shape[], ys: Shape[]) => xs.length === ys.length && xs.every((x, i) => unify(x, ys[i]!, s));
  switch (a.k) {
    case "prim":
      return a.name === (b as typeof a).name;
    case "lit":
      return a.value === (b as typeof a).value;
    case "array":
      return unify(a.of, (b as typeof a).of, s);
    case "tuple":
    case "union":
    case "inter":
      return all(a.of, (b as typeof a).of);
    case "obj": {
      const bp = (b as typeof a).props;
      return a.props.length === bp.length && a.props.every(([n, t, o], i) => n === bp[i]![0] && o === bp[i]![2] && unify(t, bp[i]![1], s));
    }
    case "ref":
      return a.hash === (b as typeof a).hash && all(a.args, (b as typeof a).args);
    case "named":
      return a.name === (b as typeof a).name && all(a.args, (b as typeof a).args);
    case "fn": {
      const bf = b as typeof a;
      if (!!a.rest !== !!bf.rest || (a.rest && !unify(a.rest, bf.rest!, s))) return false;
      return all(a.params, bf.params) && unify(a.ret, bf.ret, s);
    }
  }
  return false;
}

uses

used by