diff --git a/packages/frontend/src/help/logics_help_overview.tsx b/packages/frontend/src/help/logics_help_overview.tsx index 339e3518c..7da3419b9 100644 --- a/packages/frontend/src/help/logics_help_overview.tsx +++ b/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() { Logics - {appTitle} - {([group, theories]) => ( - <> -

{group}

-
- - {(theoryMeta) => ( - <> -
- - {theoryMeta.name} - -
-
{theoryMeta.description}
- - )} - -
- - )} + {([group, groupTheories]) => { + const visible = () => + groupTheories.filter((t) => !theories.isEditorVariant(t.id)); + return ( + 0}> +

{group}

+
+ + {(theoryMeta) => ( + <> +
+ + {theoryMeta.name} + +
+
{theoryMeta.description}
+ + )} + +
+ + ); + }} ); diff --git a/packages/frontend/src/model/document.ts b/packages/frontend/src/model/document.ts index 9cfdcc2e7..ade537161 100644 --- a/packages/frontend/src/model/document.ts +++ b/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(), 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({ diff --git a/packages/frontend/src/model/model_editor.tsx b/packages/frontend/src/model/model_editor.tsx index ad11cdf5f..59a590604 100644 --- a/packages/frontend/src/model/model_editor.tsx +++ b/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) { return ( - {(theory) => ( - 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 ( + void) => + props.changeContent((content) => f(content as ObDecl)) + } + isActive={props.isActive} + actions={props.actions} + theory={theory()} + /> + ); + }} - {(theory) => ( - - 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 ( + void) => + props.changeContent((content) => f(content as MorDecl)) + } + isActive={props.isActive} + actions={props.actions} + theory={theory()} + /> + ); + }} { 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 ( migrateModelDocument(props.liveModel, id, stdTheories)} theories={selectableTheories()} /> diff --git a/packages/frontend/src/model/model_library.ts b/packages/frontend/src/model/model_library.ts index 4f96632f7..54998e480 100644 --- a/packages/frontend/src/model/model_library.ts +++ b/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 { 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; } diff --git a/packages/frontend/src/model/string_diagram_morphism_cell_editor.module.css b/packages/frontend/src/model/string_diagram_morphism_cell_editor.module.css new file mode 100644 index 000000000..5130444ac --- /dev/null +++ b/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 */ diff --git a/packages/frontend/src/model/string_diagram_morphism_cell_editor.tsx b/packages/frontend/src/model/string_diagram_morphism_cell_editor.tsx new file mode 100644 index 000000000..870d0f8e5 --- /dev/null +++ b/packages/frontend/src/model/string_diagram_morphism_cell_editor.tsx @@ -0,0 +1,335 @@ +import { deepEqual } from "fast-equals"; +import { Index, batch, createMemo, createSignal, useContext } from "solid-js"; +import invariant from "tiny-invariant"; + +import { NameInput } from "catcolab-ui-components"; +import type { Modality, MorDecl, Ob, ObOp, QualifiedName } from "catlog-wasm"; +import { ObIdInput } from "../components"; +import type { CellActions } from "../notebook"; +import type { Theory } from "../theory"; +import { deepCopyJSON } from "../util/deepcopy"; +import { LiveModelContext } from "./context"; + +import styles from "./string_diagram_morphism_cell_editor.module.css"; + +type ActiveInput = + | { zone: "name" } + | { zone: "dom"; index: number } + | { zone: "cod"; index: number }; + +/** Unwrap `App(op, ob)` to get the inner `ob`. */ +function unwrapApp(ob: Ob | null, applyOp: ObOp | undefined): Ob | null { + if (!ob || !applyOp) { + return ob; + } + if (ob.tag === "App" && deepEqual(ob.content.op, applyOp)) { + return ob.content.ob; + } + return null; +} + +/** Wrap an `ob` with `App(op, ob)`. */ +function wrapApp(ob: Ob | null, applyOp: ObOp | undefined): Ob | null { + if (!ob || !applyOp) { + return ob; + } + return { tag: "App", content: { op: applyOp, ob } }; +} + +/** Extract the list of objects from a domain/codomain `Ob`. */ +function getObList(ob: Ob | null, applyOp: ObOp | undefined): Array { + const inner = unwrapApp(ob, applyOp); + if (inner?.tag === "List") { + return inner.content.objects; + } + return []; +} + +/** A column of wire inputs, used for both domain (left) and codomain (right). */ +function WireColumn(props: { + obs: Array; + side: "left" | "right"; + isInvalid: boolean; + completions: QualifiedName[] | undefined; + isActive: (index: number) => boolean; + insertWire: (index: number) => void; + updateOb: (index: number, ob: Ob | null) => void; + deleteWire: (index: number) => void; + activateWire: (index: number) => void; + activateName: () => void; + activateAbove: (() => void) | undefined; + activateBelow: (() => void) | undefined; + hasFocused: (() => void) | undefined; +}) { + const liveModel = useContext(LiveModelContext); + invariant(liveModel, "Live model should be provided as context"); + + const wireInput = (ob: () => Ob | null, i: number) => ( + props.updateOb(i, newOb)} + placeholder="..." + completions={props.completions} + idToLabel={(id) => liveModel().elaboratedModel()?.obGeneratorLabel(id)} + labelToId={(label) => liveModel().elaboratedModel()?.obGeneratorWithLabel(label)} + isInvalid={props.isInvalid} + isActive={props.isActive(i)} + deleteBackward={() => { + props.deleteWire(i); + if (props.obs.length === 0) { + props.activateName(); + } else if (i > 0) { + props.activateWire(i - 1); + } + }} + deleteForward={() => { + props.deleteWire(i); + if (props.obs.length === 0) { + props.activateName(); + } + }} + exitBackward={() => { + if (i > 0) { + props.activateWire(i - 1); + } else if (props.side === "left") { + props.activateAbove?.(); + } else { + props.activateName(); + } + }} + exitForward={() => { + if (i < props.obs.length - 1) { + props.activateWire(i + 1); + } else if (props.side === "left") { + props.activateName(); + } else { + props.activateBelow?.(); + } + }} + exitLeft={props.side === "right" ? props.activateName : undefined} + exitRight={props.side === "left" ? props.activateName : undefined} + interceptKeyDown={(evt) => { + if (evt.key === ",") { + props.insertWire(i + 1); + return true; + } + return false; + }} + hasFocused={() => { + props.activateWire(i); + props.hasFocused?.(); + }} + /> + ); + + return ( +
+ + {(ob, i) => ( +
+ {props.side === "left" && wireInput(ob, i)} +
+ {props.side === "right" && wireInput(ob, i)} +
+ )} + +
{ + props.insertWire(props.obs.length); + props.hasFocused?.(); + evt.preventDefault(); + }} + > + {props.side === "left" && +} +
+ {props.side === "right" && +} +
+
+ ); +} + +/** Editor for a morphism declaration cell in string diagram style. + +Renders the transition as a box with input wires on the left and output wires +on the right, where each wire is a separate input field for a domain/codomain +element. + */ +export default function StringDiagramMorphismCellEditor(props: { + morphism: MorDecl; + modifyMorphism: (f: (decl: MorDecl) => void) => void; + isActive: boolean; + actions: CellActions; + theory: Theory; +}) { + const liveModel = useContext(LiveModelContext); + invariant(liveModel, "Live model should be provided as context"); + + const [active, setActive] = createSignal({ zone: "name" }); + + const morTypeMeta = () => props.theory.modelMorTypeMeta(props.morphism.morType); + const domApplyOp = () => morTypeMeta()?.domain?.apply; + const codApplyOp = () => morTypeMeta()?.codomain?.apply; + + /** Rebuild a domain/codomain Ob from a list of objects. */ + const makeObList = (objects: Array, applyOp: ObOp | undefined): Ob | null => { + if (!applyOp) { + return null; + } + const domObjType = props.theory.theory.dom(applyOp); + const modality: Modality = + domObjType?.tag === "ModeApp" ? domObjType.content.modality : "SymmetricList"; + return wrapApp({ tag: "List", content: { modality, objects } }, applyOp); + }; + + const domType = createMemo(() => { + const op = domApplyOp(); + return op === undefined + ? props.theory.theory.src(props.morphism.morType) + : props.theory.theory.dom(op); + }); + + /** The inner element type (unwrapped from ModeApp) for completions. */ + const elementObType = createMemo(() => { + const dt = domType(); + return dt?.tag === "ModeApp" ? dt.content.obType : dt; + }); + + const domObs = () => getObList(props.morphism.dom, domApplyOp()); + const codObs = () => getObList(props.morphism.cod, codApplyOp()); + + const setDomObs = (objects: Array) => { + const ob = makeObList(objects, domApplyOp()); + props.modifyMorphism((mor) => { + mor.dom = ob; + }); + }; + + const setCodObs = (objects: Array) => { + const ob = makeObList(objects, codApplyOp()); + props.modifyMorphism((mor) => { + mor.cod = ob; + }); + }; + + const updateDomObs = (f: (objects: Array) => void) => { + const objects = deepCopyJSON(domObs()); + f(objects); + setDomObs(objects); + }; + + const updateCodObs = (f: (objects: Array) => void) => { + const objects = deepCopyJSON(codObs()); + f(objects); + setCodObs(objects); + }; + + const insertDom = (i: number) => { + batch(() => { + updateDomObs((objects) => objects.splice(i, 0, null)); + setActive({ zone: "dom", index: i }); + }); + }; + + const insertCod = (i: number) => { + batch(() => { + updateCodObs((objects) => objects.splice(i, 0, null)); + setActive({ zone: "cod", index: i }); + }); + }; + + const completions = () => liveModel().elaboratedModel()?.obGeneratorsWithType(elementObType()); + + const errors = () => { + const validated = liveModel().validatedModel(); + if (validated?.tag !== "Invalid") { + return []; + } + return validated.errors.filter((err) => err.content === props.morphism.id); + }; + + return ( +
+ err.tag === "Dom" || err.tag === "DomType")} + completions={completions()} + isActive={(i) => { + const a = active(); + return props.isActive && a.zone === "dom" && a.index === i; + }} + insertWire={insertDom} + updateOb={(i, ob) => + updateDomObs((objects) => { + objects[i] = ob; + }) + } + deleteWire={(i) => updateDomObs((objects) => objects.splice(i, 1))} + activateWire={(i) => setActive({ zone: "dom", index: i })} + activateName={() => setActive({ zone: "name" })} + activateAbove={props.actions.activateAbove} + activateBelow={props.actions.activateBelow} + hasFocused={props.actions.hasFocused} + /> +
+ { + props.modifyMorphism((mor) => { + mor.name = name; + }); + }} + isActive={props.isActive && active().zone === "name"} + deleteBackward={props.actions.deleteBackward} + deleteForward={props.actions.deleteForward} + exitBackward={props.actions.activateAbove} + exitForward={props.actions.activateBelow} + exitUp={props.actions.activateAbove} + exitDown={props.actions.activateBelow} + exitLeft={() => { + if (domObs().length > 0) { + setActive({ zone: "dom", index: domObs().length - 1 }); + } else { + insertDom(0); + } + }} + exitRight={() => { + if (codObs().length > 0) { + setActive({ zone: "cod", index: 0 }); + } else { + insertCod(0); + } + }} + hasFocused={() => { + setActive({ zone: "name" }); + props.actions.hasFocused?.(); + }} + /> +
+ err.tag === "Cod" || err.tag === "CodType")} + completions={completions()} + isActive={(i) => { + const a = active(); + return props.isActive && a.zone === "cod" && a.index === i; + }} + insertWire={insertCod} + updateOb={(i, ob) => + updateCodObs((objects) => { + objects[i] = ob; + }) + } + deleteWire={(i) => updateCodObs((objects) => objects.splice(i, 1))} + activateWire={(i) => setActive({ zone: "cod", index: i })} + activateName={() => setActive({ zone: "name" })} + activateAbove={props.actions.activateAbove} + activateBelow={props.actions.activateBelow} + hasFocused={props.actions.hasFocused} + /> +
+ ); +} diff --git a/packages/frontend/src/page/document_page_sidebar.tsx b/packages/frontend/src/page/document_page_sidebar.tsx index e08994c69..c74ee474f 100644 --- a/packages/frontend/src/page/document_page_sidebar.tsx +++ b/packages/frontend/src/page/document_page_sidebar.tsx @@ -196,8 +196,8 @@ function DocumentsTreeLeaf(props: { const iconLetters = createMemo(() => { const doc = props.doc.liveDoc.doc; - const theoryId = doc.type === "model" ? doc.theory : undefined; - if (theoryId && theories && props.doc.liveDoc.doc.type === "model") { + if (doc.type === "model" && theories) { + const theoryId = doc.editorVariant ?? doc.theory; try { const theoryMeta = theories.getMetadata(theoryId); return theoryMeta.iconLetters; diff --git a/packages/frontend/src/page/toolbar.tsx b/packages/frontend/src/page/toolbar.tsx index 2bc5b9a31..d0e86b199 100644 --- a/packages/frontend/src/page/toolbar.tsx +++ b/packages/frontend/src/page/toolbar.tsx @@ -1,9 +1,10 @@ import { A, useNavigate } from "@solidjs/router"; import CircleHelp from "lucide-solid/icons/circle-help"; -import type { JSX } from "solid-js"; +import { type JSX, useContext } from "solid-js"; +import invariant from "tiny-invariant"; import { IconButton } from "catcolab-ui-components"; -import type { TheoryMeta } from "../theory"; +import { TheoryLibraryContext, type TheoryMeta } from "../theory"; import { DefaultAppMenu } from "./menubar"; import "./toolbar.css"; @@ -58,10 +59,14 @@ function theoryHelpTooltip(meta: TheoryMeta) { export function TheoryHelpButton(props: { meta: TheoryMeta }) { const navigate = useNavigate(); + const theories = useContext(TheoryLibraryContext); + invariant(theories, "Library of theories must be provided as context"); + + const helpId = () => theories.getBaseTheoryId(props.meta.id) ?? props.meta.id; return ( navigate(`/help/logics/${props.meta.id}`)} + onClick={() => navigate(`/help/logics/${helpId()}`)} tooltip={theoryHelpTooltip(props.meta)} > diff --git a/packages/frontend/src/stdlib/theories.ts b/packages/frontend/src/stdlib/theories.ts index e2466255d..0bd45b134 100644 --- a/packages/frontend/src/stdlib/theories.ts +++ b/packages/frontend/src/stdlib/theories.ts @@ -1,3 +1,5 @@ +import { lazy } from "solid-js"; + import { TheoryLibrary } from "../theory"; import { compositionPattern } from "./generic_analyses"; @@ -50,6 +52,28 @@ stdTheories.add( description: "Place/transition networks", iconLetters: ["P", "n"], group: "Systems", + editorVariants: [ + { + id: "petri-net-string-diagram", + name: "Petri net (string diagram transitions)", + description: "Petri net with a string diagram style transition editor", + iconLetters: ["P", "n"], + group: "Systems", + editorOverrides: { + morEditors: [ + { + morType: { + tag: "Hom" as const, + content: { tag: "Basic" as const, content: "Object" }, + }, + editor: lazy( + () => import("../model/string_diagram_morphism_cell_editor"), + ), + }, + ], + }, + }, + ], }, async () => (await import("./theories/petri-net")).default, ); diff --git a/packages/frontend/src/theory/theory.ts b/packages/frontend/src/theory/theory.ts index ca6ed0bc0..3557a81c0 100644 --- a/packages/frontend/src/theory/theory.ts +++ b/packages/frontend/src/theory/theory.ts @@ -1,8 +1,13 @@ +import { deepEqual } from "fast-equals"; +import type { Component } from "solid-js"; + import type { KbdKey } from "catcolab-ui-components"; -import type { DblModel, DblTheory, MorType, ObOp, ObType } from "catlog-wasm"; +import type { DblModel, DblTheory, MorDecl, MorType, ObDecl, ObOp, ObType } from "catlog-wasm"; import type { DiagramAnalysisComponent, ModelAnalysisComponent } from "../analysis"; +import type { CellActions } from "../notebook"; import { uniqueIndexArray } from "../util/indexing"; import type { ArrowStyle } from "../visualization"; +import type { TheoryMeta } from "./theory_library"; import { MorTypeMap, ObTypeMap } from "./types"; /** A double theory configured for the frontend. @@ -134,7 +139,49 @@ export class Theory { /** List of IDs of theories to which models of this theory can be migrated. */ get migrationTargets(): Array { - return this.inclusions.concat(this.pushforwards.map((m) => m.target)); + return [...this.inclusions, ...this.pushforwards.map((m) => m.target)]; + } + + /** Create a derived theory by applying editor overrides for a named editor variant. + + The derived theory shares the same underlying double theory, analyses, + instance types, and other configuration. Only the editor components on + the specified model types are replaced. + */ + deriveEditorVariant(editorVariantMeta: TheoryMeta, overrides: EditorVariantOverrides): Theory { + // Clone modelTypes with editor overrides applied. + const modelTypes = this.modelTypes.map((meta): ModelTypeMeta => { + if (meta.tag === "ObType" && overrides.obEditors) { + const override = overrides.obEditors.find((o) => deepEqual(o.obType, meta.obType)); + if (override) { + return { ...meta, editor: override.editor }; + } + } else if (meta.tag === "MorType" && overrides.morEditors) { + const override = overrides.morEditors.find((o) => + deepEqual(o.morType, meta.morType), + ); + if (override) { + return { ...meta, editor: override.editor }; + } + } + return meta; + }); + + return new Theory({ + id: editorVariantMeta.id, + theory: this.theory, + help: this.help, + name: editorVariantMeta.name, + description: editorVariantMeta.description, + inclusions: this.inclusions, + pushforwards: this.pushforwards, + modelTypes, + modelAnalyses: this.modelAnalyses, + onlyFreeModels: this.onlyFreeModels, + instanceOfName: this.instanceOfName, + instanceTypes: this.instanceTypes, + diagramAnalyses: this.diagramAnalyses, + }); } /** Get metadata for an object type as used in models. */ @@ -218,10 +265,45 @@ export type ModelTypeMeta = | ({ tag: "ObType" } & ModelObTypeMeta) | ({ tag: "MorType" } & ModelMorTypeMeta); +/** Editor overrides for an editor variant of a theory. + +Specifies which editor components should replace the defaults for particular +object or morphism types. + */ +export type EditorVariantOverrides = { + obEditors?: Array<{ obType: ObType; editor: Component }>; + morEditors?: Array<{ morType: MorType; editor: Component }>; +}; + +/** Props for a custom object cell editor component. */ +export type ObjectEditorProps = { + object: ObDecl; + modifyObject: (f: (decl: ObDecl) => void) => void; + isActive: boolean; + actions: CellActions; + theory: Theory; +}; + +/** Props for a custom morphism cell editor component. */ +export type MorphismEditorProps = { + morphism: MorDecl; + modifyMorphism: (f: (decl: MorDecl) => void) => void; + isActive: boolean; + actions: CellActions; + theory: Theory; +}; + /** Metadata for an object type as used in models. */ export type ModelObTypeMeta = BaseTypeMeta & { /** Object type in the underlying double theory. */ obType: ObType; + + /** Custom editor component for objects of this type. + + When set, this component is used instead of the default object editor. + It must accept the same props interface as the default editor. + */ + editor?: Component; }; /** Metadata for a morphism type as used in models. */ @@ -244,6 +326,13 @@ export type ModelMorTypeMeta = BaseTypeMeta & { /** Metadata for codomain of morphism of this type. */ codomain?: MorDomainMeta; + + /** Custom editor component for morphisms of this type. + + When set, this component is used instead of the default morphism editor. + It must accept the same props interface as the default editor. + */ + editor?: Component; }; /** Metadata controlling the domain or codomain of a morphism. */ diff --git a/packages/frontend/src/theory/theory_library.ts b/packages/frontend/src/theory/theory_library.ts index 68647a0b8..1b0394259 100644 --- a/packages/frontend/src/theory/theory_library.ts +++ b/packages/frontend/src/theory/theory_library.ts @@ -1,4 +1,33 @@ -import { type ModelAnalysisMeta, Theory } from "./theory"; +import { type EditorVariantOverrides, type ModelAnalysisMeta, Theory } from "./theory"; + +/** Display metadata for an editor variant of a theory. + +An editor variant shares the same underlying double theory but uses different +editor components for some types (e.g., a string diagram editor for morphisms). + */ +export type EditorVariantMeta = { + /** Unique identifier of the editor variant. */ + id: string; + + /** Human-readable name for the editor variant. */ + name: string; + + /** Short description of the editor variant. */ + description: string; + + /** Two-letter icon abbreviation for the editor variant. */ + iconLetters: [string, string]; + + /** Group to which the editor variant belongs. */ + group?: string; + + /** Editor component overrides for this editor variant. + + Specifies which editor components replace the defaults for particular types. + Components can be wrapped with SolidJS `lazy()` to defer loading. + */ + editorOverrides?: EditorVariantOverrides; +}; /** Frontend metadata for a double theory. @@ -27,6 +56,15 @@ export type TheoryMeta = { /** Group to which the theory belongs. */ group?: string; + + /** Editor variants of this theory. + + Each editor variant appears as a separate selectable option in the theory + picker but shares the same underlying theory — only the editors differ. + Editor variants share the base theory's help page and are hidden from + the help overview. + */ + editorVariants?: EditorVariantMeta[]; }; type TheoryConstructor = (meta: TheoryMeta) => Theory; @@ -49,12 +87,31 @@ type GenericModelAnalysis = { Theories are lazy loaded. */ export class TheoryLibrary { - /** Map from theory ID to metadata about the theory. */ + /** Map from theory ID to metadata about the theory. + + Contains entries for both base theories and their editor variants. + */ private readonly metaMap: Map; - /** Map from theory ID to the theory itself or the constructor for it. */ + /** Map from theory ID to the theory itself or the constructor for it. + + Only contains entries for base theories, not editor variants. Editor + variants are derived from their base theory on demand. + */ private readonly theoryMap: Map Promise)>; + /** Map from editor variant ID to its metadata and base theory ID. */ + private readonly editorVariantMetaMap: Map< + string, + { editorVariant: EditorVariantMeta; baseId: string } + >; + + /** Map from base theory ID to the IDs of its editor variants. */ + private readonly baseToEditorVariants: Map; + + /** Map from editor variant or base theory ID to its cached derived Theory. */ + private readonly editorVariantCache: Map; + /** ID of the default theory for new models. */ private defaultTheoryId: string | undefined; @@ -63,10 +120,18 @@ export class TheoryLibrary { constructor() { this.metaMap = new Map(); this.theoryMap = new Map(); + this.editorVariantMetaMap = new Map(); + this.baseToEditorVariants = new Map(); + this.editorVariantCache = new Map(); this.genericModelAnalyses = []; } - /** Add a theory to the library. */ + /** Add a theory to the library. + + If the metadata includes `editorVariants`, each editor variant is + automatically registered as a selectable entry that shares the same + underlying theory. + */ add(meta: TheoryMeta, cons: () => Promise) { if (!meta.id) { throw new Error("The ID of a theory must be a non-empty string"); @@ -83,6 +148,31 @@ export class TheoryLibrary { } this.defaultTheoryId = meta.id; } + + // Register editor variants. + if (meta.editorVariants) { + const editorVariantIds: string[] = []; + for (const editorVariant of meta.editorVariants) { + if (this.metaMap.has(editorVariant.id)) { + throw new Error(`Theory with ID ${editorVariant.id} already defined`); + } + // Store editor variant metadata as a TheoryMeta entry so it + // appears in the theory picker alongside regular theories. + this.metaMap.set(editorVariant.id, { + id: editorVariant.id, + name: editorVariant.name, + description: editorVariant.description, + iconLetters: editorVariant.iconLetters, + group: editorVariant.group, + }); + this.editorVariantMetaMap.set(editorVariant.id, { + editorVariant, + baseId: meta.id, + }); + editorVariantIds.push(editorVariant.id); + } + this.baseToEditorVariants.set(meta.id, editorVariantIds); + } } /** Is there a theory with the given ID? */ @@ -93,9 +183,35 @@ export class TheoryLibrary { /** Get a theory by ID. A theory is instantiated and cached the first time it is retrieved. + For editor variants, the base theory is loaded and the editor variant is + derived from it by applying editor overrides. */ async get(id: string): Promise { - // Attempt to retrieve cached theory. + // Check for cached editor variant. + const cachedEditorVariant = this.editorVariantCache.get(id); + if (cachedEditorVariant) { + return cachedEditorVariant; + } + + // If this is an editor variant, load the base theory and derive. + const editorVariantEntry = this.editorVariantMetaMap.get(id); + if (editorVariantEntry !== undefined) { + const base = await this.get(editorVariantEntry.baseId); + const editorVariantMeta = this.metaMap.get(id); + if (!editorVariantMeta) { + throw new Error(`No metadata for editor variant ${id}`); + } + const editorVariant = base.deriveEditorVariant( + editorVariantMeta, + editorVariantEntry.editorVariant.editorOverrides ?? {}, + ); + // Generic analyses are inherited from the base via modelAnalyses, + // so we don't add them again here. + this.editorVariantCache.set(id, editorVariant); + return editorVariant; + } + + // Attempt to retrieve cached base theory. const meta = this.metaMap.get(id); const theoryOrCons = this.theoryMap.get(id); if (meta === undefined || theoryOrCons === undefined) { @@ -124,6 +240,24 @@ export class TheoryLibrary { return meta; } + /** Gets the base theory ID for an editor variant, if the given ID is an editor variant. */ + getBaseTheoryId(id: string): string | undefined { + return this.editorVariantMetaMap.get(id)?.baseId; + } + + /** Whether the given ID is an editor variant of another theory. */ + isEditorVariant(id: string): boolean { + return this.editorVariantMetaMap.has(id); + } + + /** Gets the IDs of all editor variants of the given theory. + + Returns an empty array if the theory has no editor variants. + */ + getEditorVariantIds(id: string): string[] { + return this.baseToEditorVariants.get(id) ?? []; + } + /** Gets metadata for the default theory for new models. Throws an error if no default has been set. diff --git a/packages/notebook-types/src/v1/document.rs b/packages/notebook-types/src/v1/document.rs index 019a14447..080cece79 100644 --- a/packages/notebook-types/src/v1/document.rs +++ b/packages/notebook-types/src/v1/document.rs @@ -1,6 +1,6 @@ use crate::v0; -use crate::v0::AnalysisType; pub use crate::v0::document::DocumentType; +use crate::v0::AnalysisType; use super::analysis::Analysis; use super::api::Link; @@ -16,6 +16,12 @@ use tsify::Tsify; pub struct ModelDocumentContent { pub name: String, pub theory: String, + #[serde( + default, + skip_serializing_if = "Option::is_none", + rename = "editorVariant" + )] + pub editor_variant: Option, pub notebook: Notebook, pub version: String, } @@ -60,6 +66,7 @@ impl Document { v0::Document::Model(old) => Document::Model(ModelDocumentContent { name: old.name, theory: old.theory, + editor_variant: None, notebook: Notebook::migrate_from_v0(old.notebook), version: "1".to_string(), }),