Editor variants and a Petri net string diagram editor variant

packages/frontend/src/help/logics_help_overview.tsx

@@ -1,6 +1,6 @@
 import { Title } from "@solidjs/meta";
 import { A } from "@solidjs/router";
-import { For, useContext } from "solid-js";
+import { For, Show, useContext } from "solid-js";
 import invariant from "tiny-invariant";
 
 import { TheoryLibraryContext } from "../theory";
@@ -17,25 +17,29 @@ export default function LogicsHelpOverview() {
             <Title>Logics - {appTitle}</Title>
             <LogicsHelpOverviewContent />
             <For each={Array.from(theories.groupedMetadata().entries())}>
-                {([group, theories]) => (
-                    <>
-                        <h2>{group}</h2>
-                        <dl>
-                            <For each={theories}>
-                                {(theoryMeta) => (
-                                    <>
-                                        <dt>
-                                            <A href={`../logics/${theoryMeta.id}`}>
-                                                {theoryMeta.name}
-                                            </A>
-                                        </dt>
-                                        <dd>{theoryMeta.description}</dd>
-                                    </>
-                                )}
-                            </For>
-                        </dl>
-                    </>
-                )}
+                {([group, groupTheories]) => {
+                    const visible = () =>
+                        groupTheories.filter((t) => !theories.isEditorVariant(t.id));
+                    return (
+                        <Show when={visible().length > 0}>
+                            <h2>{group}</h2>
+                            <dl>
+                                <For each={visible()}>
+                                    {(theoryMeta) => (
+                                        <>
+                                            <dt>
+                                                <A href={`../logics/${theoryMeta.id}`}>
+                                                    {theoryMeta.name}
+                                                </A>
+                                            </dt>
+                                            <dd>{theoryMeta.description}</dd>
+                                        </>
+                                    )}
+                                </For>
+                            </dl>
+                        </Show>
+                    );
+                }}
             </For>
         </>
     );

packages/frontend/src/model/document.ts

@@ -11,10 +11,11 @@ import type { ValidatedModel } from "./model_library";
 export type ModelDocument = Document & { type: "model" };
 
 /** Create an empty model document. */
-export const newModelDocument = (theory: string): ModelDocument => ({
+export const newModelDocument = (theory: string, editorVariant?: string): ModelDocument => ({
     name: "",
     type: "model",
     theory,
+    ...(editorVariant ? { editorVariant } : {}),
     notebook: newNotebook<ModelJudgment>(),
     version: currentVersion(),
 });
@@ -57,37 +58,79 @@ export async function createModel(
     return api.createDoc(init);
 }
 
-/** Migrate a model document from one theory to another. */
+/** The effective theory ID for a model document.
+
+Combines the base theory with the editor variant, if any.
+ */
+export function effectiveTheoryId(doc: ModelDocument): string {
+    return doc.editorVariant ?? doc.theory;
+}
+
+/** Migrate a model document to a different theory, or switch its editor variant.
+
+When the target is an editor variant of the current base theory, only the
+`editorVariant` field is updated. For real theory migrations (inclusions or
+pushforwards), the `theory` field is updated and `editorVariant` is cleared
+or set depending on whether the target is an editor variant.
+ */
 export async function migrateModelDocument(
     liveModel: LiveModelDoc,
-    targetTheoryId: string,
+    targetId: string,
     theories: TheoryLibrary,
 ) {
     const { doc, changeDoc } = liveModel.liveDoc;
-    const targetTheory = await theories.get(targetTheoryId);
+
+    // Resolve target: is it an editor variant or a base theory?
+    const targetBaseId = theories.getBaseTheoryId(targetId) ?? targetId;
+    const targetEditorVariant = theories.isEditorVariant(targetId) ? targetId : undefined;
+
+    // If only the editor variant is changing (same base theory), just flip the field.
+    if (targetBaseId === doc.theory) {
+        changeDoc((doc) => {
+            if (targetEditorVariant) {
+                doc.editorVariant = targetEditorVariant;
+            } else {
+                delete doc.editorVariant;
+            }
+        });
+        return;
+    }
+
+    // Real theory migration below.
+    const targetTheory = await theories.get(targetBaseId);
     const theory = liveModel.theory();
     let model = liveModel.elaboratedModel();
     invariant(theory && model); // FIXME: Should fail gracefully.
 
-    // Trivial migration.
-    if (!NotebookUtils.hasFormalCells(doc.notebook) || theory.inclusions.includes(targetTheoryId)) {
+    // Trivial migration (no formal cells or inclusion).
+    if (!NotebookUtils.hasFormalCells(doc.notebook) || theory.inclusions.includes(targetBaseId)) {
         changeDoc((doc) => {
-            doc.theory = targetTheoryId;
+            doc.theory = targetBaseId;
+            if (targetEditorVariant) {
+                doc.editorVariant = targetEditorVariant;
+            } else {
+                delete doc.editorVariant;
+            }
         });
         return;
     }
 
     // Pushforward migration.
-    const migration = theory.pushforwards.find((m) => m.target === targetTheoryId);
+    const migration = theory.pushforwards.find((m) => m.target === targetBaseId);
     if (!migration) {
-        throw new Error(`No migration defined from ${theory.id} to ${targetTheoryId}`);
+        throw new Error(`No migration defined from ${theory.id} to ${targetBaseId}`);
     }
     // TODO: We need a general method to propagate changes from catlog models to
     // notebooks. This stop-gap solution only works because pushforward
     // migration doesn't have to create/delete cells, only update types.
     model = migration.migrate(model, targetTheory.theory);
     changeDoc((doc) => {
-        doc.theory = targetTheoryId;
+        doc.theory = targetBaseId;
+        if (targetEditorVariant) {
+            doc.editorVariant = targetEditorVariant;
+        } else {
+            delete doc.editorVariant;
+        }
         for (const judgment of NotebookUtils.getFormalContent(doc.notebook)) {
             if (judgment.tag === "object") {
                 judgment.obType = model.obType({

packages/frontend/src/model/model_editor.tsx

@@ -1,4 +1,5 @@
 import { Match, Switch, useContext } from "solid-js";
+import { Dynamic } from "solid-js/web";
 import invariant from "tiny-invariant";
 
 import type { InstantiatedModel, ModelJudgment, MorDecl, ObDecl } from "catlog-wasm";
@@ -58,28 +59,42 @@ export function ModelCellEditor(props: FormalCellEditorProps<ModelJudgment>) {
     return (
         <Switch>
             <Match when={props.content.tag === "object" && liveModel().theory()}>
-                {(theory) => (
-                    <ObjectCellEditor
-                        object={props.content as ObDecl}
-                        modifyObject={(f) => props.changeContent((content) => f(content as ObDecl))}
-                        isActive={props.isActive}
-                        actions={props.actions}
-                        theory={theory()}
-                    />
-                )}
+                {(theory) => {
+                    const obDecl = () => props.content as ObDecl;
+                    const editor = () =>
+                        theory().modelObTypeMeta(obDecl().obType)?.editor ?? ObjectCellEditor;
+                    return (
+                        <Dynamic
+                            component={editor()}
+                            object={obDecl()}
+                            modifyObject={(f: (decl: ObDecl) => void) =>
+                                props.changeContent((content) => f(content as ObDecl))
+                            }
+                            isActive={props.isActive}
+                            actions={props.actions}
+                            theory={theory()}
+                        />
+                    );
+                }}
             </Match>
             <Match when={props.content.tag === "morphism" && liveModel().theory()}>
-                {(theory) => (
-                    <MorphismCellEditor
-                        morphism={props.content as MorDecl}
-                        modifyMorphism={(f) =>
-                            props.changeContent((content) => f(content as MorDecl))
-                        }
-                        isActive={props.isActive}
-                        actions={props.actions}
-                        theory={theory()}
-                    />
-                )}
+                {(theory) => {
+                    const morDecl = () => props.content as MorDecl;
+                    const editor = () =>
+                        theory().modelMorTypeMeta(morDecl().morType)?.editor ?? MorphismCellEditor;
+                    return (
+                        <Dynamic
+                            component={editor()}
+                            morphism={morDecl()}
+                            modifyMorphism={(f: (decl: MorDecl) => void) =>
+                                props.changeContent((content) => f(content as MorDecl))
+                            }
+                            isActive={props.isActive}
+                            actions={props.actions}
+                            theory={theory()}
+                        />
+                    );
+                }}
             </Match>
             <Match when={props.content.tag === "instantiation"}>
                 <InstantiationCellEditor

packages/frontend/src/model/model_info.tsx

@@ -1,7 +1,7 @@
 import { NotebookUtils } from "../notebook";
 import { stdTheories } from "../stdlib";
 import { TheorySelectorDialog } from "../theory/theory_selector";
-import { type LiveModelDoc, migrateModelDocument } from "./document";
+import { type LiveModelDoc, effectiveTheoryId, migrateModelDocument } from "./document";
 
 /** Widget in the top right corner of a model document pane.
  */
@@ -10,7 +10,11 @@ export function ModelInfo(props: { liveModel: LiveModelDoc }) {
 
     const selectableTheories = () => {
         if (NotebookUtils.hasFormalCells(liveDoc().doc.notebook)) {
-            return props.liveModel.theory()?.migrationTargets ?? [];
+            const theory = props.liveModel.theory();
+            if (!theory) return [];
+            const baseId = liveDoc().doc.theory;
+            const editorVariantIds = stdTheories.getEditorVariantIds(baseId);
+            return [baseId, ...editorVariantIds, ...theory.migrationTargets];
         } else {
             // If the model has no formal cells, allow any theory to be selected.
             return undefined;
@@ -19,7 +23,7 @@ export function ModelInfo(props: { liveModel: LiveModelDoc }) {
 
     return (
         <TheorySelectorDialog
-            theoryMeta={stdTheories.getMetadata(liveDoc().doc.theory)}
+            theoryMeta={stdTheories.getMetadata(effectiveTheoryId(liveDoc().doc))}
             setTheory={(id) => migrateModelDocument(props.liveModel, id, stdTheories)}
             theories={selectableTheories()}
         />

packages/frontend/src/model/model_library.ts

@@ -24,7 +24,7 @@ import {
 import { type Api, findAndMigrate, type LiveDoc, makeLiveDoc } from "../api";
 import { NotebookUtils } from "../notebook/types";
 import type { Theory, TheoryLibrary } from "../theory";
-import type { LiveModelDoc, ModelDocument } from "./document";
+import { type LiveModelDoc, type ModelDocument, effectiveTheoryId } from "./document";
 
 /** An elaborated model along with its validation status. */
 export type ValidatedModel =
@@ -241,7 +241,7 @@ export class ModelLibrary<RefId> {
             return [theory, validatedModel];
         }
 
-        const theory = await theories.get(doc.theory);
+        const theory = await theories.get(effectiveTheoryId(doc as ModelDocument));
         let validatedModel: ValidatedModel;
         try {
             if (this.isElaborating.has(key)) {
@@ -312,7 +312,14 @@ function elaborateAndValidateModel(
 /** Does the patch to the model document affect its formal content? */
 function isPatchToFormalContent(doc: Document, patch: Patch): boolean {
     const path = patch.path;
-    if (!(path[0] === "type" || path[0] === "theory" || path[0] === "notebook")) {
+    if (
+        !(
+            path[0] === "type" ||
+            path[0] === "theory" ||
+            path[0] === "editorVariant" ||
+            path[0] === "notebook"
+        )
+    ) {
         // Ignore changes to top-level data like document name.
         return false;
     }

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

@@ -0,0 +1,89 @@
+.morphism {
+    --add-wire-height: 1.2em;
+
+    display: flex;
+    flex-direction: row;
+    align-items: stretch;
+    gap: 0;
+    margin-block: calc(var(--add-wire-height) / 2);
+    transition: margin-block 0.15s;
+}
+
+.wires {
+    display: flex;
+    flex-direction: column;
+    justify-content: center;
+    gap: 2px;
+    min-width: 3em;
+
+    &.left {
+        align-items: flex-end;
+    }
+
+    &.right {
+        align-items: flex-start;
+    }
+}
+
+.wire {
+    display: flex;
+    flex-direction: row;
+    align-items: center;
+    gap: 0;
+}
+
+.wireLine {
+    width: 1.5ex;
+    height: 0;
+    border-top: 2px solid var(--color-foreground);
+    flex-shrink: 0;
+}
+
+.box {
+    border: 2px solid var(--color-foreground);
+    border-radius: 2px;
+    padding: 0.3em 0.6em;
+    min-width: 4em;
+    display: flex;
+    align-items: center;
+    justify-content: center;
+    background: var(--color-background);
+
+    & input {
+        text-align: center;
+    }
+}
+
+.addWire {
+    cursor: pointer;
+    opacity: 0;
+    height: 0;
+    overflow: hidden;
+    pointer-events: none;
+    transition:
+        opacity 0.15s,
+        height 0.15s;
+}
+
+.addWireButton {
+    font-size: 0.85em;
+    user-select: none;
+}
+
+/* stylelint-disable no-descending-specificity -- intentional override on interactive states */
+.morphism:hover,
+.morphism:focus-within {
+    margin-block: 0;
+
+    & .addWire {
+        opacity: 0.3;
+        height: var(--add-wire-height);
+        pointer-events: auto;
+
+        &:hover {
+            opacity: 0.7;
+        }
+    }
+}
+
+/* stylelint-enable no-descending-specificity */