diff --git a/packages/catlog-wasm/src/model_diagram.rs b/packages/catlog-wasm/src/model_diagram.rs index d0b0b7b97..64cf52256 100644 --- a/packages/catlog-wasm/src/model_diagram.rs +++ b/packages/catlog-wasm/src/model_diagram.rs @@ -3,13 +3,14 @@ use std::rc::Rc; use all_the_same::all_the_same; +use catlog::dbl::theory::Unital; use derive_more::From; use serde::{Deserialize, Serialize}; use tsify::Tsify; use wasm_bindgen::prelude::*; use catcolab_document_types::current::*; -use catlog::dbl::model::{DblModel as _, DiscreteDblModel, FpDblModel, MutDblModel}; +use catlog::dbl::model::{DblModel as _, DiscreteDblModel, FpDblModel, ModalDblModel, MutDblModel}; use catlog::dbl::model_diagram as diagram; use catlog::dbl::model_morphism::DiscreteDblModelMapping; use catlog::one::FgCategory; @@ -25,8 +26,21 @@ use super::theory::{DblTheory, DblTheoryBox}; #[derive(From)] pub enum DblModelDiagramBox { /// A diagram in a model of a discrete double theory. - Discrete(diagram::DblModelDiagram), - // Modal(), # TODO: Not implemented. + Discrete(Rc>), + /// A diagram in a model of a modal double theory. + ModalUnital(Rc>>), +} + +impl From for DblModelDiagramBox { + fn from(value: diagram::DiscreteDblModelDiagram) -> Self { + Self::Discrete(Rc::new(value)) + } +} + +impl From>> for DblModelDiagramBox { + fn from(value: diagram::DblModelDiagram<(), ModalDblModel>) -> Self { + Self::ModalUnital(Rc::new(value)) + } } /// Wasm binding for a diagram in a model of a double theory. @@ -47,6 +61,10 @@ impl DblModelDiagram { let model = DiscreteDblModel::new(theory.clone()); diagram::DblModelDiagram(mapping, model).into() } + DblTheoryBox::ModalUnital(theory) => { + let model = ModalDblModel::new(theory.clone()); + diagram::DblModelDiagram((), model).into() + } _ => panic!("Diagrams only implemented for discrete double theories"), }; Self { @@ -57,16 +75,22 @@ impl DblModelDiagram { /// Adds an object to the diagram. pub fn add_ob(&mut self, decl: &DiagramObDecl) -> Result<(), String> { - all_the_same!(match &mut self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { - let (mapping, model) = diagram.into(); + match &mut self.diagram { + DblModelDiagramBox::Discrete(diagram) => { + let diagram::DblModelDiagram(mapping, model) = Rc::make_mut(diagram); let ob_type: QualifiedName = Elaborator.elab(&decl.ob_type)?; if let Some(over) = decl.over.as_ref().map(|ob| Elaborator.elab(ob)).transpose()? { mapping.assign_ob(decl.id.into(), over); } model.add_ob(decl.id.into(), ob_type); } - }); + DblModelDiagramBox::ModalUnital(diagram) => { + let diagram::DblModelDiagram(_, model) = Rc::make_mut(diagram); + let ob_type = Elaborator.elab(&decl.ob_type)?; + // Ignore decl.over — no mapping. + model.add_ob(decl.id.into(), ob_type); + } + }; if !decl.name.is_empty() { self.ob_namespace.set_label(decl.id, decl.name.as_str().into()); } @@ -75,9 +99,9 @@ impl DblModelDiagram { /// Adds a morphism to the diagram. pub fn add_mor(&mut self, decl: &DiagramMorDecl) -> Result<(), String> { - all_the_same!(match &mut self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { - let (mapping, model) = diagram.into(); + match &mut self.diagram { + DblModelDiagramBox::Discrete(diagram) => { + let diagram::DblModelDiagram(mapping, model) = Rc::make_mut(diagram); let mor_type = Elaborator.elab(&decl.mor_type)?; model.make_mor(decl.id.into(), mor_type); if let Some(dom) = decl.dom.as_ref().map(|ob| Elaborator.elab(ob)).transpose()? { @@ -86,11 +110,24 @@ impl DblModelDiagram { if let Some(cod) = decl.cod.as_ref().map(|ob| Elaborator.elab(ob)).transpose()? { model.set_cod(decl.id.into(), cod); } - if let Some(over) = decl.over.as_ref().map(|mor| Elaborator.elab(mor)).transpose()? { + if let Some(over) = + decl.over.as_ref().map(|mor| Elaborator.elab(mor)).transpose()? + { mapping.assign_mor(decl.id.into(), over); } } - }); + DblModelDiagramBox::ModalUnital(diagram) => { + let diagram::DblModelDiagram(_, model) = Rc::make_mut(diagram); + let mor_type = Elaborator.elab(&decl.mor_type)?; + model.make_mor(decl.id.into(), mor_type); + if let Some(dom) = decl.dom.as_ref().map(|ob| Elaborator.elab(ob)).transpose()? { + model.set_dom(decl.id.into(), dom); + } + if let Some(cod) = decl.cod.as_ref().map(|ob| Elaborator.elab(ob)).transpose()? { + model.set_cod(decl.id.into(), cod); + } + } + }; if decl.name.is_empty() { Ok(()) } else { @@ -106,8 +143,8 @@ impl DblModelDiagram { #[wasm_bindgen(js_name = "obType")] pub fn ob_type(&self, ob: Ob) -> Result { all_the_same!(match &self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { - let (_, model) = diagram.into(); + DblModelDiagramBox::[Discrete, ModalUnital](diagram) => { + let diagram::DblModelDiagram(_, model) = &**diagram; Ok(Quoter.quote(&model.ob_type(&Elaborator.elab(&ob)?))) } }) @@ -117,8 +154,8 @@ impl DblModelDiagram { #[wasm_bindgen(js_name = "morType")] pub fn mor_type(&self, mor: Mor) -> Result { all_the_same!(match &self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { - let (_, model) = diagram.into(); + DblModelDiagramBox::[Discrete, ModalUnital](diagram) => { + let diagram::DblModelDiagram(_, model) = &**diagram; Ok(Quoter.quote(&model.mor_type(&Elaborator.elab(&mor)?))) } }) @@ -128,8 +165,8 @@ impl DblModelDiagram { #[wasm_bindgen(js_name = "obGenerators")] pub fn ob_generators(&self) -> Vec { all_the_same!(match &self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { - let (_, model) = diagram.into(); + DblModelDiagramBox::[Discrete, ModalUnital](diagram) => { + let diagram::DblModelDiagram(_, model) = &**diagram; model.ob_generators().collect() } }) @@ -139,8 +176,8 @@ impl DblModelDiagram { #[wasm_bindgen(js_name = "morGenerators")] pub fn mor_generators(&self) -> Vec { all_the_same!(match &self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { - let (_, model) = diagram.into(); + DblModelDiagramBox::[Discrete, ModalUnital](diagram) => { + let diagram::DblModelDiagram(_, model) = &**diagram; model.mor_generators().collect() } }) @@ -150,8 +187,8 @@ impl DblModelDiagram { #[wasm_bindgen(js_name = "obGeneratorsWithType")] pub fn ob_generators_with_type(&self, ob_type: ObType) -> Result, String> { all_the_same!(match &self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { - let (_, model) = diagram.into(); + DblModelDiagramBox::[Discrete, ModalUnital](diagram) => { + let diagram::DblModelDiagram(_, model) = &**diagram; let ob_type = Elaborator.elab(&ob_type)?; Ok(model.ob_generators_with_type(&ob_type).collect()) } @@ -165,8 +202,8 @@ impl DblModelDiagram { mor_type: MorType, ) -> Result, String> { all_the_same!(match &self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { - let (_, model) = diagram.into(); + DblModelDiagramBox::[Discrete, ModalUnital](diagram) => { + let diagram::DblModelDiagram(_, model) = &**diagram; let mor_type = Elaborator.elab(&mor_type)?; Ok(model.mor_generators_with_type(&mor_type).collect()) } @@ -189,28 +226,42 @@ impl DblModelDiagram { #[wasm_bindgen(js_name = "obPresentation")] pub fn ob_presentation(&self, id: QualifiedName) -> Option { let label = self.ob_generator_label(&id); - let (ob_type, over) = all_the_same!(match &self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { - let (mapping, model) = diagram.into(); - (Quoter.quote(&model.ob_generator_type(&id)), - Quoter.quote(mapping.0.ob_generator_map.get(&id)?)) + let (ob_type, over) = match &self.diagram { + DblModelDiagramBox::Discrete(diagram) => { + let diagram::DblModelDiagram(mapping, model) = &**diagram; + ( + Quoter.quote(&model.ob_generator_type(&id)), + Quoter.quote(mapping.0.ob_generator_map.get(&id)?), + ) + } + // DblModelDiagramBox::ModalUnital(diagram) => { + // let (_, model) = diagram.into(); + // (Quoter.quote(&model.ob_generator_type(&id)), None) + // } + DblModelDiagramBox::ModalUnital(_) => { + return None; } - }); + }; Some(DiagramObGenerator { id, label, ob_type, over }) } /// Gets a morphism generator as it appears in the diagram's presentation. #[wasm_bindgen(js_name = "morPresentation")] pub fn mor_presentation(&self, id: QualifiedName) -> Option { - let (mor_type, over, dom, cod) = all_the_same!(match &self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { - let (mapping, model) = diagram.into(); - (Quoter.quote(&model.mor_generator_type(&id)), - Quoter.quote(mapping.0.mor_generator_map.get(&id)?), - Quoter.quote(model.get_dom(&id)?), - Quoter.quote(model.get_cod(&id)?)) + let (mor_type, over, dom, cod) = match &self.diagram { + DblModelDiagramBox::Discrete(diagram) => { + let diagram::DblModelDiagram(mapping, model) = &**diagram; + ( + Quoter.quote(&model.mor_generator_type(&id)), + Quoter.quote(mapping.0.mor_generator_map.get(&id)?), + Quoter.quote(model.get_dom(&id)?), + Quoter.quote(model.get_cod(&id)?), + ) + } + DblModelDiagramBox::ModalUnital(_) => { + return None; } - }); + }; Some(DiagramMorGenerator { id, mor_type, over, dom, cod }) } @@ -218,8 +269,8 @@ impl DblModelDiagram { #[wasm_bindgen] pub fn presentation(&self) -> ModelDiagramPresentation { all_the_same!(match &self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { - let (_, model) = diagram.into(); + DblModelDiagramBox::[Discrete, ModalUnital](diagram) => { + let diagram::DblModelDiagram(_, model) = &**diagram; ModelDiagramPresentation { ob_generators: { model.ob_generators().filter_map(|id| self.ob_presentation(id)).collect() @@ -235,13 +286,18 @@ impl DblModelDiagram { /// Infers missing data in the diagram from the model, where possible. #[wasm_bindgen(js_name = "inferMissingFrom")] pub fn infer_missing_from(&mut self, model: &DblModel) -> Result<(), String> { - all_the_same!(match &mut self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { - let model: &Rc<_> = (&model.model).try_into().map_err( - |_| "Type of model should match type of diagram")?; + match &mut self.diagram { + DblModelDiagramBox::Discrete(diagram) => { + let model: &Rc<_> = (&model.model) + .try_into() + .map_err(|_| "Type of model should match type of diagram")?; + let diagram = Rc::make_mut(diagram); diagram.infer_missing_from(model); } - }); + DblModelDiagramBox::ModalUnital(_) => { + return Ok(()); + } + }; // Assign numbers to anonymous objects added by inference. let mut nanon = 0; @@ -261,13 +317,18 @@ impl DblModelDiagram { /// Validates that the diagram is well defined in a model. #[wasm_bindgen(js_name = "validateIn")] pub fn validate_in(&self, model: &DblModel) -> Result { - let result = all_the_same!(match &self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { - let model: &Rc<_> = (&model.model).try_into().map_err( - |_| "Type of model should match type of diagram")?; + let result = match &self.diagram { + DblModelDiagramBox::Discrete(diagram) => { + let model: &Rc<_> = (&model.model) + .try_into() + .map_err(|_| "Type of model should match type of diagram")?; diagram.validate_in(model) } - }); + DblModelDiagramBox::ModalUnital(_) => { + return Ok(ModelDiagramValidationResult(JsResult::Ok(()))); + // XXX + } + }; Ok(ModelDiagramValidationResult(result.map_err(|errs| errs.into()).into())) } } diff --git a/packages/frontend/src/components/id_input.tsx b/packages/frontend/src/components/id_input.tsx index 5ffb66c0d..255b72c16 100644 --- a/packages/frontend/src/components/id_input.tsx +++ b/packages/frontend/src/components/id_input.tsx @@ -126,7 +126,12 @@ export function IdInput( return null; }; - const setNewId = () => props.generateId && props.setId(props.generateId()); + const setNewId = () => { + if (props.generateId) { + const newId = props.generateId(); + props.setId(newId); + } + }; const labelType = (id: Uuid | null): "named" | "anonymous" | "undefined" => { if (id == null) { diff --git a/packages/frontend/src/diagram/morphism_cell_editor.tsx b/packages/frontend/src/diagram/morphism_cell_editor.tsx index bd698c0d3..101b3d960 100644 --- a/packages/frontend/src/diagram/morphism_cell_editor.tsx +++ b/packages/frontend/src/diagram/morphism_cell_editor.tsx @@ -1,6 +1,5 @@ -import { useContext } from "solid-js"; +import { createMemo, useContext } from "solid-js"; import invariant from "tiny-invariant"; -import { v7 } from "uuid"; import { type FocusHandle, useChildFocus } from "catcolab-ui-components"; import type { DiagramMorDecl } from "catlog-wasm"; @@ -8,7 +7,7 @@ import { BasicMorInput } from "../model/morphism_input"; import type { CellActions } from "../notebook"; import type { Theory } from "../theory"; import { LiveDiagramContext } from "./context"; -import { BasicObInput } from "./object_input"; +import { ObInput } from "./object_input"; import arrowStyles from "../stdlib/arrow_styles.module.css"; import "./morphism_cell_editor.css"; @@ -27,8 +26,28 @@ export function DiagramMorphismCellEditor(props: { // oxlint-disable-next-line solid/reactivity -- Focus handles are stable for a mounted cell. const focus = useChildFocus(props.focus, { default: "mor" }); - const domType = () => props.theory.theory.src(props.decl.morType); - const codType = () => props.theory.theory.tgt(props.decl.morType); + const morTypeMeta = () => props.theory.modelMorTypeMeta(props.decl.morType); + + const domType = createMemo(() => { + const theory = props.theory.theory; + const op = morTypeMeta()?.domain?.apply; + if (op === undefined) { + return theory.src(props.decl.morType); + } else { + return theory.dom(op); + } + }); + + const codType = createMemo(() => { + const theory = props.theory.theory; + const op = morTypeMeta()?.codomain?.apply; + if (op === undefined) { + return theory.tgt(props.decl.morType); + } else { + // Codomain type for operation should equal target type above. + return theory.dom(op); + } + }); const errors = () => { const validated = liveDiagram().validatedDiagram(); @@ -45,7 +64,7 @@ export function DiagramMorphismCellEditor(props: { return (
- { @@ -54,7 +73,6 @@ export function DiagramMorphismCellEditor(props: { }); }} obType={domType()} - generateId={v7} isInvalid={domInvalid()} focus={focus.childFocus("dom")} deleteForward={() => focus.setActiveChild("mor")} @@ -88,7 +106,7 @@ export function DiagramMorphismCellEditor(props: {
- { @@ -97,7 +115,6 @@ export function DiagramMorphismCellEditor(props: { }); }} obType={codType()} - generateId={v7} isInvalid={codInvalid()} focus={focus.childFocus("cod")} deleteBackward={() => focus.setActiveChild("mor")} diff --git a/packages/frontend/src/diagram/object_input.tsx b/packages/frontend/src/diagram/object_input.tsx index aaf9da5d8..32108b467 100644 --- a/packages/frontend/src/diagram/object_input.tsx +++ b/packages/frontend/src/diagram/object_input.tsx @@ -1,9 +1,100 @@ -import { useContext } from "solid-js"; +import { deepEqual } from "fast-equals"; +import { type Component, splitProps, useContext } from "solid-js"; +import { Dynamic } from "solid-js/web"; import invariant from "tiny-invariant"; -import type { Ob, ObType, QualifiedName } from "catlog-wasm"; +import type { TextInputOptions } from "catcolab-ui-components"; +import type { Ob, ObOp, ObType, QualifiedName } from "catlog-wasm"; import { type IdInputOptions, ObIdInput } from "../components"; import { LiveDiagramContext } from "./context"; +import { ObListEditor } from "./object_list_editor"; + +/** Props passed to any object input component. */ +export type ObInputProps = { + /** Current value of object, if any. */ + ob: Ob | null; + + /** Handler to set a new value of the object. */ + setOb: (ob: Ob | null) => void; + + /** Type of object being edited. */ + obType: ObType; + + /** Placeholder text to show when no object has been chosen. */ + placeholder?: string; + + /** Whether the choice of object is invalid, say by having wrong type. + + This is a stub; we should propagate error messages from the core. + */ + isInvalid?: boolean; +}; + +/** Input an object that already exists in a model. */ +export function ObInput( + allProps: ObInputProps & + TextInputOptions & { + /** Operation to apply to the object afterwards, if any. */ + applyOp?: ObOp; + }, +) { + const [props, otherProps] = splitProps(allProps, ["ob", "setOb", "obType", "applyOp"]); + + const ob = () => { + if (props.applyOp) { + return props.ob?.tag === "App" && deepEqual(props.ob.content.op, props.applyOp) + ? props.ob.content.ob + : null; + } else { + return props.ob; + } + }; + + const setOb = (ob: Ob | null) => { + if (ob && props.applyOp) { + props.setOb({ + tag: "App", + content: { + op: props.applyOp, + ob, + }, + }); + } else { + props.setOb(ob); + } + }; + + return ( + + ); +} + +function obEditorForType(obType: ObType): Component { + // console.log(obType.tag); + if (obType.tag === "Basic") { + return BasicObInput; + } else if (obType.tag === "ModeApp") { + switch (obType.content.modality) { + case "Discrete": + case "Codiscrete": + return obEditorForType(obType.content.obType); + case "List": + case "SymmetricList": + case "CocartesianList": + case "CartesianList": + case "AdditiveList": { + return ObListEditor; + } + } + } + throw new Error(`No editor for object of type: ${obType}`); +} /** Input a basic object in a diagram via its human-readable name. */ diff --git a/packages/frontend/src/diagram/object_list_editor.css b/packages/frontend/src/diagram/object_list_editor.css new file mode 100644 index 000000000..dc7a896ed --- /dev/null +++ b/packages/frontend/src/diagram/object_list_editor.css @@ -0,0 +1,10 @@ +.diagram-object-decl { + display: flex; + flex-direction: row; + gap: 1ex; + align-items: baseline; + + & .is-a:before { + content: ":"; + } +} diff --git a/packages/frontend/src/diagram/object_list_editor.tsx b/packages/frontend/src/diagram/object_list_editor.tsx new file mode 100644 index 000000000..e0e36144b --- /dev/null +++ b/packages/frontend/src/diagram/object_list_editor.tsx @@ -0,0 +1,200 @@ +import { + batch, + createEffect, + createSignal, + Index, + type JSX, + mergeProps, + Show, + untrack, + useContext, +} from "solid-js"; +import invariant from "tiny-invariant"; + +import type { TextInputOptions } from "catcolab-ui-components"; +import type { Ob, QualifiedName } from "catlog-wasm"; +import { ObIdInput } from "../components"; +import { removeProxyAndCopy } from "../util/remove_proxy_and_copy"; +import { LiveDiagramContext } from "./context"; +import type { ObInputProps } from "./object_input"; + +import "./object_list_editor.css"; + +type ObListEditorProps = ObInputProps & + TextInputOptions & { + insertKey?: string; + startDelimiter?: JSX.Element | string; + endDelimiter?: JSX.Element | string; + separator?: (index: number) => JSX.Element | string; + }; + +/** Edits a list of objects of given type. */ +export function ObListEditor(originalProps: ObListEditorProps) { + const props = mergeProps( + { + insertKey: ",", + startDelimiter:
{"["}
, + endDelimiter:
{"]"}
, + separator: () =>
{","}
, + }, + originalProps, + ); + + const liveDiagram = useContext(LiveDiagramContext); + invariant(liveDiagram, "Live model should be provided as context"); + + const [activeIndex, setActiveIndex] = createSignal(0); + + const setObList = (objects: Array) => { + props.setOb({ + tag: "List", + content: { + modality: modeAppType().content.modality, + objects, + }, + }); + }; + + const updateObList = (f: (objects: Array) => void) => { + const objects = removeProxyAndCopy(obList()); + f(objects); + setObList(objects); + }; + + const insertNewOb = (i: number) => { + batch(() => { + updateObList((objects) => { + objects.splice(i, 0, null); + }); + setActiveIndex(i); + }); + }; + + const modeAppType = () => { + if (props.obType.tag !== "ModeApp") { + throw new Error(`Object type should be a list modality, received: ${props.obType}`); + } + return props.obType; + }; + + const obList = (): Array => { + if (!props.ob) { + return []; + } + if (props.ob.tag !== "List") { + throw new Error(`Object should be a list, received: ${props.ob}`); + } + return props.ob.content.objects; + }; + + const completions = (): QualifiedName[] | undefined => + liveDiagram().elaboratedDiagram()?.obGeneratorsWithType(modeAppType().content.obType); + + // Make the default value the empty list, rather than null. + createEffect(() => { + if (!props.ob) { + setObList([]); + } + }); + + // Insert into new object into empty list when focus is gained. + createEffect(() => { + if (props.isActive && untrack(obList).length === 0) { + insertNewOb(0); + } + }); + + return ( +
    { + if (obList().length === 0) { + insertNewOb(0); + props.hasFocused?.(); + evt.preventDefault(); + } + }} + > + {props.startDelimiter} + }> + {(ob, i) => ( +
  • + 0 && props.separator}>{(sep) => sep()(i)} + { + updateObList((objects) => { + objects[i] = ob; + }); + }} + placeholder={props.placeholder} + idToLabel={(id) => + liveDiagram().elaboratedDiagram()?.obGeneratorLabel(id) + } + labelToId={(label) => + liveDiagram().elaboratedDiagram()?.obGeneratorWithLabel(label) + } + completions={completions()} + isActive={props.isActive && activeIndex() === i} + deleteBackward={() => + batch(() => { + updateObList((objects) => { + objects.splice(i, 1); + }); + if (i === 0) { + props.deleteBackward?.(); + } else { + setActiveIndex(i - 1); + } + }) + } + deleteForward={() => { + batch(() => { + updateObList((objects) => { + objects.splice(i, 1); + }); + if (i === 0) { + props.deleteForward?.(); + } + }); + }} + exitBackward={() => props.exitBackward?.()} + exitForward={() => props.exitForward?.()} + exitLeft={() => { + if (i === 0) { + props.exitLeft?.(); + } else { + setActiveIndex(i - 1); + } + }} + exitRight={() => { + if (i === obList().length - 1) { + props.exitRight?.(); + } else { + setActiveIndex(i + 1); + } + }} + interceptKeyDown={(evt) => { + if (evt.key === props.insertKey) { + insertNewOb(i + 1); + return true; + } else if (evt.key === "Home" && !evt.shiftKey) { + // TODO: Should move to beginning of input. + setActiveIndex(0); + } else if (evt.key === "End" && !evt.shiftKey) { + setActiveIndex(obList().length - 1); + } + return false; + }} + hasFocused={() => { + setActiveIndex(i); + props.hasFocused?.(); + }} + /> +
    • + )} +     + {props.endDelimiter} +
+ ); +} diff --git a/packages/frontend/src/stdlib/theories/petri-net.ts b/packages/frontend/src/stdlib/theories/petri-net.ts index e584783df..b5fddb941 100644 --- a/packages/frontend/src/stdlib/theories/petri-net.ts +++ b/packages/frontend/src/stdlib/theories/petri-net.ts @@ -98,5 +98,25 @@ export default function createPetriNetTheory(theoryMeta: TheoryMeta): Theory { }, }), ], + instanceOfName: "Diagrams in", + instanceTypes: [ + { + tag: "ObType", + obType: { tag: "Basic", content: "Object" }, + name: "Element", + description: "State of the system", + shortcut: ["O"], + }, + { + tag: "MorType", + morType: { + tag: "Hom", + content: { tag: "Basic", content: "Object" }, + }, + name: "Operation", + description: "Event causing change of state", + shortcut: ["M"], + }, + ], }); }