Start supporting printing unifications

crates/compiler/checkmate/www/src/engine/engine.tsx

@@ -0,0 +1,142 @@
+import { Event, Variable } from "../schema";
+import { assertExhaustive } from "../utils/exhaustive";
+import {
+  ChangeEvent,
+  makeDeleteVariable,
+  makeRevertVariable,
+  RollbackChange,
+  Subs,
+} from "./subs";
+
+export type EventIndex = number & { __eventIndex: never };
+
+function* flattenEvents(events: Event[]): Generator<Event> {
+  for (const event of events) {
+    yield event;
+    switch (event.type) {
+      case "Unification": {
+        yield* flattenEvents(event.subevents);
+        break;
+      }
+      case "VariableUnified":
+      case "VariableSetDescriptor":
+        break;
+      default:
+        assertExhaustive(event);
+    }
+  }
+}
+
+function getFlatEvents(events: Event[]): {
+  flatEvents: Event[];
+  map: Map<Event, EventIndex>;
+} {
+  const map = new Map<Event, EventIndex>();
+  const flatEvents = Array.from(flattenEvents(events));
+  let i = 0;
+  for (const event of flatEvents) {
+    map.set(event, i as EventIndex);
+    i++;
+  }
+  return { flatEvents, map };
+}
+
+export class Engine {
+  #eventIndexMap: Map<Event, EventIndex>;
+  #events: Event[];
+  #subs: Subs = new Subs();
+  #reverseEvents: Map<EventIndex, RollbackChange> = new Map();
+
+  #nextIndexForward: EventIndex = 0 as EventIndex;
+
+  constructor(events: Event[]) {
+    const { flatEvents, map } = getFlatEvents(events);
+    this.#eventIndexMap = map;
+    this.#events = flatEvents;
+  }
+
+  getEventIndex(event: Event): EventIndex {
+    const index = this.#eventIndexMap.get(event);
+    if (index === undefined) {
+      throw new Error("Event not found");
+    }
+    return index;
+  }
+
+  get step(): EventIndex {
+    return this.#nextIndexForward;
+  }
+
+  stepTo(eventIndex: EventIndex): void {
+    while (this.#nextIndexForward <= eventIndex) {
+      this.stepForward(this.#nextIndexForward);
+      ++this.#nextIndexForward;
+    }
+    while (this.#nextIndexForward > eventIndex) {
+      --this.#nextIndexForward;
+      this.stepBackward(this.#nextIndexForward);
+    }
+  }
+
+  get subs(): Readonly<Subs> {
+    return this.#subs;
+  }
+
+  private stepForward(eventIndex: EventIndex): void {
+    const event = this.#events[eventIndex];
+    if (!isApplicable(event)) {
+      return;
+    }
+
+    if (!this.#reverseEvents.has(eventIndex)) {
+      const variable = applicableVariable(event);
+      const current = this.#subs.get(variable);
+      let revert: RollbackChange;
+      if (!current) {
+        revert = makeDeleteVariable({ variable });
+      } else {
+        revert = makeRevertVariable({ variable, to: current });
+      }
+      this.#reverseEvents.set(eventIndex, revert);
+    }
+
+    this.#subs.apply(event);
+  }
+
+  private stepBackward(eventIndex: EventIndex): void {
+    const event = this.#events[eventIndex];
+    if (!isApplicable(event)) {
+      return;
+    }
+
+    const revert = this.#reverseEvents.get(eventIndex);
+    if (!revert) {
+      throw new Error("No revert found");
+    }
+
+    this.#subs.apply(revert);
+  }
+}
+
+function isApplicable(event: Event): event is ChangeEvent {
+  switch (event.type) {
+    case "VariableUnified":
+    case "VariableSetDescriptor":
+      return true;
+    case "Unification":
+      return false;
+    default:
+      assertExhaustive(event);
+  }
+}
+
+function applicableVariable(event: ChangeEvent): Variable {
+  switch (event.type) {
+    case "VariableUnified":
+      return event.from;
+    case "VariableSetDescriptor":
+      return event.variable;
+    default:
+      assertExhaustive(event);
+  }
+}

crates/compiler/checkmate/www/src/engine/event_util.tsx

@@ -0,0 +1,19 @@
+import { Event } from "../schema";
+
+export function lastSubEvent(event: Event): Event {
+  switch (event.type) {
+    case "Unification": {
+      const subevents = event.subevents;
+      if (subevents.length === 0) {
+        return event;
+      }
+      return lastSubEvent(event.subevents[event.subevents.length - 1]);
+    }
+    case "VariableUnified": {
+      return event;
+    }
+    case "VariableSetDescriptor": {
+      return event;
+    }
+  }
+}

crates/compiler/checkmate/www/src/engine/subs.tsx

@@ -0,0 +1,121 @@
+import { Content, Rank, Variable, Event } from "../schema";
+import { assertExhaustive } from "../utils/exhaustive";
+import { Refine } from "../utils/refine";
+
+export type TypeLink = {
+  type: "link";
+  to: Variable;
+};
+
+function link({ to }: Omit<TypeLink, "type">): TypeLink {
+  return { type: "link", to };
+}
+
+export type TypeDescriptor = {
+  type: "descriptor";
+  rank: Rank;
+  content: Content;
+};
+
+function descriptor({
+  rank,
+  content,
+}: Omit<TypeDescriptor, "type">): TypeDescriptor {
+  return { type: "descriptor", rank, content };
+}
+
+export type VarType = TypeLink | TypeDescriptor;
+
+export type RevertVariableChange = {
+  type: "revertTo";
+  variable: Variable;
+  to: VarType;
+};
+
+export type DeleteVariableChange = {
+  type: "delete";
+  variable: Variable;
+};
+
+export type RollbackChange = RevertVariableChange | DeleteVariableChange;
+
+export function makeRevertVariable({
+  variable,
+  to,
+}: Omit<RevertVariableChange, "type">): RevertVariableChange {
+  return { type: "revertTo", variable, to: { ...to } };
+}
+
+export function makeDeleteVariable({
+  variable,
+}: Omit<DeleteVariableChange, "type">): DeleteVariableChange {
+  return { type: "delete", variable };
+}
+
+export type ChangeEvent =
+  | Refine<Event, "VariableUnified">
+  | Refine<Event, "VariableSetDescriptor">;
+
+export type Change = ChangeEvent | RollbackChange;
+
+export class Subs {
+  #map: Map<Variable, VarType> = new Map();
+
+  get(variable: Variable): VarType | undefined {
+    return this.#map.get(variable);
+  }
+
+  get_root(variable: Variable): TypeDescriptor | undefined {
+    const type = this.get(variable);
+    if (type === undefined) {
+      return undefined;
+    }
+    switch (type.type) {
+      case "descriptor":
+        return type;
+      case "link":
+        return this.get_root(type.to);
+      default:
+        assertExhaustive(type);
+    }
+  }
+
+  apply(change: Change): void {
+    switch (change.type) {
+      case "VariableUnified": {
+        const { from, to } = change;
+        if (from !== to) {
+          this.#map.set(from, link({ to }));
+        }
+        break;
+      }
+      case "VariableSetDescriptor": {
+        const { variable, rank, content } = change;
+        const existing = this.get_root(variable);
+        if (existing !== undefined) {
+          const nu = descriptor({ ...existing });
+          if (rank) nu.rank = rank;
+          if (content) nu.content = content;
+          this.#map.set(variable, nu);
+        } else {
+          if (typeof rank !== "number") throw new Error("rank is required");
+          if (!content) throw new Error("content is required");
+          this.#map.set(variable, descriptor({ rank, content }));
+        }
+        break;
+      }
+      case "revertTo": {
+        const { variable, to } = change;
+        this.#map.set(variable, { ...to });
+        break;
+      }
+      case "delete": {
+        const { variable } = change;
+        this.#map.delete(variable);
+        break;
+      }
+      default:
+        assertExhaustive(change);
+    }
+  }
+}