From 4adf813b51a341d212e196b7217c5e3d1135fc58 Mon Sep 17 00:00:00 2001 From: Evan Patterson Date: Tue, 12 Nov 2024 21:50:37 -0800 Subject: [PATCH] ENH: Add double theory for diagrammatic equations (unary ops only). --- package.json | 2 +- .../frontend/src/diagram/diagram_editor.tsx | 4 +- packages/frontend/src/stdlib/theories.tsx | 54 +++++++++++++++++++ 3 files changed, 57 insertions(+), 3 deletions(-) diff --git a/package.json b/package.json index 07ef1687..ddbe20e3 100644 --- a/package.json +++ b/package.json @@ -24,5 +24,5 @@ "tsx": "^4.16.5", "typedoc": "^0.26.5" }, - "packageManager": "pnpm@9.11.0" + "packageManager": "pnpm@9.12.3" } diff --git a/packages/frontend/src/diagram/diagram_editor.tsx b/packages/frontend/src/diagram/diagram_editor.tsx index a631d118..345289f2 100644 --- a/packages/frontend/src/diagram/diagram_editor.tsx +++ b/packages/frontend/src/diagram/diagram_editor.tsx @@ -41,8 +41,8 @@ export default function DiagramPage() { const { doc } = liveDoc; invariant(doc.type === "diagram", () => `Expected diagram, got type: ${doc.type}`); - const modelReactiveDoc = await getLiveDoc(rpc, repo, doc.modelRef.refId); - const liveModel = enlivenModelDocument(doc.modelRef.refId, modelReactiveDoc, theories); + const modelLiveDoc = await getLiveDoc(rpc, repo, doc.modelRef.refId); + const liveModel = enlivenModelDocument(doc.modelRef.refId, modelLiveDoc, theories); return enlivenDiagramDocument(refId, liveDoc, liveModel); }); diff --git a/packages/frontend/src/stdlib/theories.tsx b/packages/frontend/src/stdlib/theories.tsx index 4aa37c3c..7b9e81c1 100644 --- a/packages/frontend/src/stdlib/theories.tsx +++ b/packages/frontend/src/stdlib/theories.tsx @@ -436,3 +436,57 @@ stdTheories.add( }); }, ); + +stdTheories.add( + { + id: "diagrammatic-equations", + name: "Equational theory", + description: "Systems of equations specified diagrammatically", + group: "Applied Mathematics", + }, + (meta) => { + const thCategory = new catlog.ThCategory(); + return new Theory({ + ...meta, + theory: thCategory.theory(), + modelTypes: [ + { + tag: "ObType", + obType: { tag: "Basic", content: "Object" }, + name: "Type", + description: "Type of quantity", + shortcut: ["Q"], + }, + { + tag: "MorType", + morType: { + tag: "Hom", + content: { tag: "Basic", content: "Object" }, + }, + name: "Operation", + description: "Arithmetical operation or differential operator", + shortcut: ["A"], + }, + ], + instanceTypes: [ + { + tag: "ObType", + obType: { tag: "Basic", content: "Object" }, + name: "Quantity", + description: "Variables and other numerical quantities", + shortcut: ["Q"], + }, + { + tag: "MorType", + morType: { + tag: "Hom", + content: { tag: "Basic", content: "Object" }, + }, + name: "Application", + description: "Apply an operation to quantities", + shortcut: ["A"], + }, + ], + }); + }, +);