OBEE-18 Action API: Implementation for basic model notebooks

.github/workflows/ci.yml

@@ -122,6 +122,14 @@ jobs:
           pnpm --filter "./packages/*" run build:deps
           pnpm --filter "./packages/*" run ci
 
+      - name: Typescript documents package tests
+        run: |
+          pnpm --filter catcolab-documents exec vitest run test/creating-and-editing.test.ts test/definitions.test.ts
+
+      - name: Typescript logic package tests
+        run: |
+          pnpm --filter catcolab-logics exec vitest run test/simple-olog.test.ts
+
   build_nixos_system:
     name: build NixOS system
     runs-on: ubuntu-latest

packages/documents/package.json

@@ -5,8 +5,7 @@
     "license": "MIT",
     "type": "module",
     "exports": {
-        ".": "./src/index.ts",
-        "./*": "./src/*"
+        ".": "./src/index.ts"
     },
     "scripts": {
         "format": "oxfmt .",
@@ -18,9 +17,9 @@
         "ci": "oxlint --deny-warnings && oxfmt --check ."
     },
     "dependencies": {
+        "catcolab-document-methods": "link:../document-methods",
         "catcolab-document-types": "link:../document-types/pkg",
-        "catlog-wasm": "link:../catlog-wasm/dist/pkg-browser",
-        "uuid": "^13.0.0"
+        "catlog-wasm": "link:../catlog-wasm/dist/pkg-browser"
     },
     "devDependencies": {
         "@automerge/automerge": "^3.3.1",
@@ -32,15 +31,15 @@
         "@tsconfig/strictest": "^2.0.8",
         "@types/node": "^24.0.0",
         "@types/uuid": "^10.0.0",
-        "catcolab-documents": "workspace:*",
-        "catcolab-logics": "workspace:*",
+        "catcolab-logics": "link:../logics",
         "fast-check": "^4.9.0",
         "happy-dom": "^20.0.0",
         "prosemirror-model": "^1.25.9",
         "prosemirror-state": "^1.4.4",
         "prosemirror-view": "^1.41.9",
         "solid-js": "^1.9.10",
         "typescript": "^6.0.3",
+        "uuid": "^13.0.0",
         "vite": "^7.2.2",
         "vite-plugin-solid": "^2.11.10",
         "vite-plugin-wasm": "^3.5.0",

packages/documents/src/binder.ts

@@ -0,0 +1,25 @@
+import { Model } from "catcolab-document-methods";
+import type { ModelDocument } from "./model/document";
+import { modelNotebookFromDoc, type Notebook } from "./model/notebook";
+import type { Shape } from "./shape";
+
+export interface Binder {
+    createNotebook<S extends Shape & { readonly theory: string }>(
+        shape: S,
+        options: { title: string },
+    ): Promise<Notebook<S, ModelDocument>>;
+}
+
+export function createBinder(): Binder {
+    return {
+        async createNotebook<S extends Shape & { readonly theory: string }>(
+            shape: S,
+            options: { title: string },
+        ) {
+            const document = Model.newModelDocument({ theory: shape.theory });
+            document.name = options.title;
+
+            return modelNotebookFromDoc(shape, document);
+        },
+    };
+}

packages/documents/src/index.ts

@@ -0,0 +1,10 @@
+export { createBinder } from "./binder";
+export type { Binder } from "./binder";
+export type { MorphismCell, ObjectCell } from "./model/cell";
+export type { ModelDocument } from "./model/document";
+export { modelNotebookFromDoc as notebookFromModel } from "./model/notebook";
+export type { Notebook } from "./model/notebook";
+export type { NotebookDocument } from "./notebook-document";
+export type { RichTextCell } from "./rich-text";
+export { defineMorphism, defineObject, defineShape, RichText } from "./shape";
+export type { MorphismEndpoint, MorphismEndpoints, MorphismType, ObjectType, Shape } from "./shape";

packages/documents/src/model/cell.ts

@@ -0,0 +1,201 @@
+import { Nb } from "catcolab-document-methods";
+import type { Ob } from "catcolab-document-types";
+import { getRichTextCell, type RichTextCell } from "../rich-text";
+import { findMorphismType, findObjectType } from "../shape";
+import type {
+    CodomainObjectTypesOf,
+    DomainObjectTypesOf,
+    MorphismType,
+    MorphismTypesOf,
+    ObjectType,
+    ObjectTypesOf,
+    Shape,
+} from "../shape";
+import { getModelJudgment, type ModelDocument } from "./document";
+
+export interface ObjectCell<O extends ObjectType> {
+    readonly kind: "object";
+    readonly id: string;
+    readonly type: O;
+    readonly label: string;
+
+    update(patch: Partial<{ label: string | null }>): void;
+}
+
+export interface MorphismCell<S extends Shape, M extends MorphismType> {
+    readonly kind: "morphism";
+    readonly id: string;
+    readonly type: M;
+    readonly label: string;
+    readonly from: ObjectCell<DomainObjectTypesOf<S, M>> | null;
+    readonly to: ObjectCell<CodomainObjectTypesOf<S, M>> | null;
+
+    update(
+        patch: Partial<{
+            label: string | null;
+            from: ObjectCell<DomainObjectTypesOf<S, M>> | null;
+            to: ObjectCell<CodomainObjectTypesOf<S, M>> | null;
+        }>,
+    ): void;
+}
+
+export type CellOf<S extends Shape> =
+    | RichTextCell
+    | ObjectCell<ObjectTypesOf<S>>
+    | MorphismCell<S, MorphismTypesOf<S>>;
+
+export function getObjectCell<O extends ObjectType>(
+    document: ModelDocument,
+    cellId: string,
+    type: O,
+): ObjectCell<O> {
+    return {
+        kind: "object",
+        id: cellId,
+        type,
+        get label() {
+            const judgment = getModelJudgment(document, cellId);
+            if (judgment.tag !== "object") {
+                throw new Error(`Cell ${cellId} is not an object.`);
+            }
+            return judgment.name;
+        },
+        update(patch) {
+            if (patch.label === undefined) {
+                return;
+            }
+            const judgment = getModelJudgment(document, cellId);
+            if (judgment.tag !== "object") {
+                throw new Error(`Cell ${cellId} is not an object.`);
+            }
+            judgment.name = patch.label ?? "";
+        },
+    };
+}
+
+function objectCellFromOb<S extends Shape>(
+    shape: S,
+    document: ModelDocument,
+    endpoint: Ob | null,
+): ObjectCell<ObjectTypesOf<S>> | null {
+    if (endpoint?.tag !== "Basic") {
+        return null;
+    }
+
+    for (const cellId of document.notebook.cellOrder) {
+        const cell = Nb.getCellById(document.notebook, cellId);
+        if (cell.tag !== "formal" || cell.content.tag !== "object") {
+            continue;
+        }
+        if (cell.content.id === endpoint.content) {
+            const type = findObjectType(shape, cell.content.obType);
+            return type ? getObjectCell(document, cellId, type) : null;
+        }
+    }
+
+    return null;
+}
+
+export function obFromObjectCell(
+    document: ModelDocument,
+    endpoint: ObjectCell<ObjectType> | null,
+): Ob | null {
+    if (!endpoint) {
+        return null;
+    }
+    const judgment = getModelJudgment(document, endpoint.id);
+    if (judgment.tag !== "object") {
+        throw new Error(`Cell ${endpoint.id} is not an object.`);
+    }
+    return { tag: "Basic", content: judgment.id };
+}
+
+export function getMorphismCell<S extends Shape, M extends MorphismTypesOf<S>>(
+    shape: S,
+    document: ModelDocument,
+    cellId: string,
+    type: M,
+): MorphismCell<S, M> {
+    return {
+        kind: "morphism",
+        id: cellId,
+        type,
+        get label() {
+            const judgment = getModelJudgment(document, cellId);
+            if (judgment.tag !== "morphism") {
+                throw new Error(`Cell ${cellId} is not a morphism.`);
+            }
+            return judgment.name;
+        },
+        get from() {
+            const judgment = getModelJudgment(document, cellId);
+            if (judgment.tag !== "morphism") {
+                throw new Error(`Cell ${cellId} is not a morphism.`);
+            }
+            return objectCellFromOb(shape, document, judgment.dom) as ObjectCell<
+                DomainObjectTypesOf<S, M>
+            > | null;
+        },
+        get to() {
+            const judgment = getModelJudgment(document, cellId);
+            if (judgment.tag !== "morphism") {
+                throw new Error(`Cell ${cellId} is not a morphism.`);
+            }
+            return objectCellFromOb(shape, document, judgment.cod) as ObjectCell<
+                CodomainObjectTypesOf<S, M>
+            > | null;
+        },
+        update(patch) {
+            const judgment = getModelJudgment(document, cellId);
+            if (judgment.tag !== "morphism") {
+                throw new Error(`Cell ${cellId} is not a morphism.`);
+            }
+            const dom = Object.hasOwn(patch, "from")
+                ? obFromObjectCell(document, patch.from ?? null)
+                : undefined;
+            const cod = Object.hasOwn(patch, "to")
+                ? obFromObjectCell(document, patch.to ?? null)
+                : undefined;
+
+            if (patch.label !== undefined) {
+                judgment.name = patch.label ?? "";
+            }
+            if (dom !== undefined) {
+                judgment.dom = dom;
+            }
+            if (cod !== undefined) {
+                judgment.cod = cod;
+            }
+        },
+    };
+}
+
+export function getModelCell<S extends Shape>(
+    shape: S,
+    document: ModelDocument,
+    cellId: string,
+): CellOf<S> {
+    const cell = Nb.getCellById(document.notebook, cellId);
+    if (cell.tag === "rich-text") {
+        return getRichTextCell(document, cellId);
+    }
+
+    switch (cell.content.tag) {
+        case "object": {
+            const type = findObjectType(shape, cell.content.obType);
+            if (!type) {
+                throw new Error(`Object cell ${cellId} is not supported by the notebook shape.`);
+            }
+            return getObjectCell(document, cellId, type);
+        }
+        case "morphism": {
+            const type = findMorphismType(shape, cell.content.morType);
+            if (!type) {
+                throw new Error(`Morphism cell ${cellId} is not supported by the notebook shape.`);
+            }
+            return getMorphismCell(shape, document, cellId, type);
+        }
+        default:
+            throw new Error(`Formal cell ${cellId} is not supported yet.`);
+    }
+}

packages/documents/src/model/document.ts

@@ -0,0 +1,12 @@
+import { Nb, type ModelDocument } from "catcolab-document-methods";
+import type { ModelJudgment } from "catcolab-document-types";
+
+export type { ModelDocument } from "catcolab-document-methods";
+
+export function getModelJudgment(document: ModelDocument, cellId: string): ModelJudgment {
+    const cell = Nb.getCellById(document.notebook, cellId);
+    if (cell.tag !== "formal") {
+        throw new Error(`Cell ${cellId} is not formal.`);
+    }
+    return cell.content;
+}

packages/documents/src/model/equality.ts

@@ -0,0 +1,42 @@
+import type { MorType, ObType } from "catcolab-document-types";
+import { assertExhaustive } from "../util/assert_exhaustive";
+
+export function objectTypesEqual(left: ObType, right: ObType): boolean {
+    switch (left.tag) {
+        case "Basic":
+            return right.tag === "Basic" && left.content === right.content;
+        case "Tabulator":
+            return right.tag === "Tabulator" && morphismTypesEqual(left.content, right.content);
+        case "ModeApp":
+            return (
+                right.tag === "ModeApp" &&
+                left.content.modality === right.content.modality &&
+                objectTypesEqual(left.content.obType, right.content.obType)
+            );
+        default:
+            return assertExhaustive(left);
+    }
+}
+
+export function morphismTypesEqual(left: MorType, right: MorType): boolean {
+    switch (left.tag) {
+        case "Basic":
+            return right.tag === "Basic" && left.content === right.content;
+        case "Hom":
+            return right.tag === "Hom" && objectTypesEqual(left.content, right.content);
+        case "Composite":
+            return (
+                right.tag === "Composite" &&
+                left.content.length === right.content.length &&
+                left.content.every((type, index) => morphismTypesEqual(type, right.content[index]!))
+            );
+        case "ModeApp":
+            return (
+                right.tag === "ModeApp" &&
+                left.content.modality === right.content.modality &&
+                morphismTypesEqual(left.content.morType, right.content.morType)
+            );
+        default:
+            return assertExhaustive(left);
+    }
+}