Merge pull request #1247 from ToposInstitute/kb/equations-ui

UI for editing path equations in schemas and ologs

Author: kasbah

packages/document-methods/src/model.ts

@@ -38,6 +38,15 @@ export const newMorphismDecl = (morType: MorType): ModelJudgment & { tag: "morph
     cod: null,
 });
 
+/** Create a new equation declaration. */
+export const newEquationDecl = (): ModelJudgment & { tag: "equation" } => ({
+    tag: "equation",
+    id: v7(),
+    name: "",
+    lhs: null,
+    rhs: null,
+});
+
 /** Create a new instantiation of an existing model. */
 export const newInstantiatedModel = (
     model?: Link | null,

packages/document-types/src/v0/model.rs

@@ -33,7 +33,7 @@ pub enum Mor {
     Basic(String),
 
     /// Composite of morphisms.
-    Composite(Box<Path<Ob, Mor>>),
+    Composite(#[tsify(type = "Path<Ob, Mor>")] Box<Path<Ob, Mor>>),
 
     /// Morphism between tabulated morphisms, a commutative square.
     TabulatorSquare {

packages/frontend/src/model/editors.ts

@@ -1,7 +1,7 @@
 import type { Component } from "solid-js";
 
 import type { FocusHandle } from "catcolab-ui-components";
-import type { MorDecl, ObDecl } from "catlog-wasm";
+import type { EqnDecl, MorDecl, ObDecl } from "catlog-wasm";
 import type { CellActions } from "../notebook";
 import type { Theory } from "../theory";
 import type { MorTypeMap, ObTypeMap } from "../theory/types";
@@ -33,3 +33,12 @@ export type MorphismEditorProps = {
     actions: CellActions;
     theory: Theory;
 };
+
+/** Props for an equation cell editor component in a model. */
+export type EquationEditorProps = {
+    equation: EqnDecl;
+    modifyEquation: (f: (decl: EqnDecl) => void) => void;
+    focus: FocusHandle;
+    actions: CellActions;
+    theory: Theory;
+};

packages/frontend/src/model/equation_cell_editor.module.css

@@ -0,0 +1,52 @@
+.decl {
+    display: flex;
+    flex-direction: row;
+    align-items: center;
+    gap: 0.125rem;
+    margin-top: 0.25rem;
+    margin-bottom: 0.25rem;
+}
+
+.name {
+    display: inline-flex;
+    align-items: baseline;
+}
+
+.nameSeparator {
+    color: var(--color-gray-800);
+    padding-left: 0.375rem;
+    padding-right: 0.625rem;
+}
+
+/* Lay the two sides out horizontally, but allow them to wrap onto separate
+   lines when there is not enough horizontal space. */
+.equation {
+    display: flex;
+    flex-direction: row;
+    flex-wrap: wrap;
+    align-items: center;
+    justify-content: flex-start;
+    gap: 0.125rem 0.5rem;
+    min-width: 0;
+}
+
+.equals {
+    font-size: 1.5em;
+    text-align: center;
+    line-height: 1;
+    color: var(--color-gray-950);
+    margin: 0 0.25rem;
+}
+
+.morList {
+    display: flex;
+    min-width: 0;
+
+    ul {
+        flex-wrap: wrap;
+    }
+}
+
+.separator {
+    padding: 0 0.25em;
+}

packages/frontend/src/model/equation_cell_editor.tsx

@@ -0,0 +1,285 @@
+import { deepEqual } from "fast-equals";
+import { createEffect, createMemo, createSignal, useContext } from "solid-js";
+import invariant from "tiny-invariant";
+import { P, match } from "ts-pattern";
+
+import {
+    type FocusHandle,
+    InlineListEditor,
+    NameInput,
+    useChildFocus,
+} from "catcolab-ui-components";
+import type { DblModel, Mor, Ob, QualifiedName, Uuid } from "catlog-wasm";
+import { removeProxyAndCopy } from "../util/remove_proxy_and_copy";
+import { LiveModelContext } from "./context";
+import type { EquationEditorProps } from "./editors";
+import { PathMorInput } from "./path_mor_input";
+
+import styles from "./equation_cell_editor.module.css";
+
+type EquationCellInput = "name" | "lhs" | "rhs";
+
+/** Editor for an equation cell in a model. */
+export default function EquationCellEditor(props: EquationEditorProps) {
+    const liveModel = useContext(LiveModelContext);
+    invariant(liveModel, "Live model should be provided as context");
+
+    // oxlint-disable-next-line solid/reactivity -- Focus handles are stable for a mounted cell.
+    const focus = useChildFocus<EquationCellInput>(props.focus, { default: "name" });
+
+    const completions = (): QualifiedName[] | undefined =>
+        liveModel().elaboratedModel()?.morGenerators();
+
+    const lhs = createMemo(() => morToList(props.equation.lhs));
+    const rhs = createMemo(() => morToList(props.equation.rhs));
+
+    // The domain of the left-hand side, used to require that the right-hand side
+    // begins on the same object so the two sides remain parallel.
+    const lhsDom = createMemo((): Ob | null => {
+        const model = liveModel().elaboratedModel();
+        const first = lhs().find((mor): mor is Mor => mor != null);
+        if (!model || !first) {
+            return null;
+        }
+        return morDom(model, first);
+    });
+
+    const setLhs = (mors: Array<Mor | null>) =>
+        props.modifyEquation((eqn) => {
+            eqn.lhs = removeProxyAndCopy(listToMor(mors));
+        });
+
+    const setRhs = (mors: Array<Mor | null>) =>
+        props.modifyEquation((eqn) => {
+            eqn.rhs = removeProxyAndCopy(listToMor(mors));
+        });
+
+    const setName = (name: string) =>
+        props.modifyEquation((eqn) => {
+            eqn.name = name;
+        });
+
+    return (
+        <div class={`formal-judgment ${styles.decl}`}>
+            <div class={styles.name}>
+                <NameInput
+                    placeholder="Unnamed"
+                    name={props.equation.name}
+                    setName={setName}
+                    focus={focus.childFocus("name")}
+                    deleteBackward={props.actions.deleteBackward}
+                    deleteForward={props.actions.deleteForward}
+                    exitBackward={props.actions.activateAbove}
+                    exitForward={() => focus.setActiveChild("lhs")}
+                    exitUp={props.actions.activateAbove}
+                    exitDown={() => focus.setActiveChild("lhs")}
+                    exitRight={() => focus.setActiveChild("lhs")}
+                    createBelow={() => focus.setActiveChild("lhs")}
+                />
+            </div>
+            <div class={styles.nameSeparator}>:</div>
+            <div class={styles.equation}>
+                <MorListEditor
+                    mors={lhs()}
+                    setMors={setLhs}
+                    completions={completions()}
+                    focus={focus.childFocus("lhs")}
+                    exitBackward={() => focus.setActiveChild("name")}
+                    exitForward={() => focus.setActiveChild("rhs")}
+                    exitLeft={() => focus.setActiveChild("name")}
+                    exitRight={() => focus.setActiveChild("rhs")}
+                    deleteBackward={() => focus.setActiveChild("name")}
+                    deleteForward={() => focus.setActiveChild("rhs")}
+                />
+                <div class={styles.equals}>{"="}</div>
+                <MorListEditor
+                    mors={rhs()}
+                    setMors={setRhs}
+                    completions={completions()}
+                    baseDom={lhsDom()}
+                    focus={focus.childFocus("rhs")}
+                    exitBackward={() => focus.setActiveChild("lhs")}
+                    exitForward={props.actions.activateBelow}
+                    exitLeft={() => focus.setActiveChild("lhs")}
+                    exitRight={props.actions.activateBelow}
+                    deleteBackward={() => focus.setActiveChild("lhs")}
+                    deleteForward={props.actions.activateBelow}
+                />
+            </div>
+        </div>
+    );
+}
+
+function MorListEditor(props: {
+    mors: Array<Mor | null>;
+    setMors: (mors: Array<Mor | null>) => void;
+    completions: QualifiedName[] | undefined;
+    /** Required domain for the first morphism in the path, if constrained. */
+    baseDom?: Ob | null;
+    focus: FocusHandle;
+    exitBackward: () => void;
+    exitForward: () => void;
+    exitLeft: () => void;
+    exitRight: () => void;
+    deleteBackward: () => void;
+    deleteForward: () => void;
+}) {
+    const liveModel = useContext(LiveModelContext);
+    invariant(liveModel, "Live model should be provided as context");
+
+    const [editMors, setEditMors] = createSignal<Array<Mor | null> | null>(null);
+
+    const mors = () => editMors() ?? props.mors;
+
+    const setMors = (mors: Array<Mor | null>) => {
+        setEditMors(mors);
+        props.setMors(mors);
+    };
+
+    createEffect(() => {
+        if (!props.focus.hasFocus()) {
+            setEditMors(null);
+        }
+    });
+
+    // The object that a morphism at `index` must have as its domain in order to
+    // extend the path: the codomain of the preceding morphism, or `baseDom` for
+    // the first morphism. `null` means there is no constraint.
+    const requiredDom = (index: number): Ob | null => {
+        const model = liveModel().elaboratedModel();
+        if (!model) {
+            return null;
+        }
+        const items = mors();
+        for (let i = index - 1; i >= 0; i--) {
+            const prev = items[i];
+            if (prev != null) {
+                return morCod(model, prev);
+            }
+        }
+        return props.baseDom ?? null;
+    };
+
+    // Morphism generators whose domain matches the required domain at `index`.
+    const morCompletions = (index: number): Uuid[] | undefined => {
+        const all = props.completions;
+        if (!all) {
+            return all;
+        }
+        const dom = requiredDom(index);
+        if (dom === null) {
+            return all;
+        }
+        const model = liveModel().elaboratedModel();
+        return all.filter((id) => {
+            const gen = model?.morPresentation(id);
+            return gen != null && obsEqual(gen.dom, dom);
+        });
+    };
+
+    // Object generators on which the identity morphism composes at `index`, i.e.
+    // those equal to the required domain (since `id(X)` has domain and codomain X).
+    const obCompletions = (index: number): Uuid[] | undefined => {
+        const model = liveModel().elaboratedModel();
+        const all = model?.obGenerators();
+        if (!all) {
+            return all;
+        }
+        const dom = requiredDom(index);
+        if (dom === null) {
+            return all;
+        }
+        return all.filter((id) => obsEqual(basicOb(id), dom));
+    };
+
+    return (
+        <div class={styles.morList}>
+            <InlineListEditor<Mor>
+                items={mors()}
+                setItems={setMors}
+                insertKey=";"
+                startDelimiter={""}
+                endDelimiter={""}
+                separator={() => <div class={styles.separator}>{";"}</div>}
+                focus={props.focus}
+                exitBackward={props.exitBackward}
+                exitForward={props.exitForward}
+                exitLeft={props.exitLeft}
+                exitRight={props.exitRight}
+                deleteBackward={props.deleteBackward}
+                deleteForward={props.deleteForward}
+            >
+                {(mor, setMor, options, index) => (
+                    <PathMorInput
+                        mor={mor()}
+                        setMor={setMor}
+                        placeholder="..."
+                        morCompletions={morCompletions(index)}
+                        obCompletions={obCompletions(index)}
+                        {...options}
+                    />
+                )}
+            </InlineListEditor>
+        </div>
+    );
+}
+
+/** Build a basic object from its generator id. */
+function basicOb(id: Uuid): Ob {
+    return { tag: "Basic", content: id };
+}
+
+/** Domain of a morphism in the model, or `null` if it cannot be computed. */
+function morDom(model: DblModel, mor: Mor): Ob | null {
+    if (model.hasMor(mor)) {
+        return model.dom(mor);
+    } else {
+        return null;
+    }
+}
+
+/** Codomain of a morphism in the model, or `null` if it cannot be computed. */
+function morCod(model: DblModel, mor: Mor): Ob | null {
+    if (model.hasMor(mor)) {
+        return model.cod(mor);
+    } else {
+        return null;
+    }
+}
+
+/** Structural equality of objects, sufficient for comparing model objects. */
+function obsEqual(a: Ob | null, b: Ob | null): boolean {
+    if (a === null || b === null) {
+        return a === b;
+    }
+    return deepEqual(a, b);
+}
+
+/** Convert the stored morphism into the editable list shape. */
+function morToList(mor: Mor | null): Array<Mor | null> {
+    if (mor === null) {
+        return [];
+    }
+    const seq = match(mor)
+        .with({ tag: "Composite", content: { tag: "Seq", content: P.select() } }, (xs) => xs)
+        .otherwise(() => null);
+    return seq ?? [mor];
+}
+
+/** Convert the editable list into the stored equation side. */
+function listToMor(mors: Array<Mor | null>): Mor | null {
+    const present = mors.filter((mor): mor is Mor => mor !== null);
+    if (present.length === 0) {
+        return null;
+    }
+    if (present.length === 1) {
+        return present[0] ?? null;
+    }
+    return {
+        tag: "Composite",
+        content: {
+            tag: "Seq",
+            content: present,
+        },
+    };
+}