Modular instantiation component

packages/catlog-wasm/src/model_diagram.rs

@@ -1,11 +1,15 @@
 //! Wasm bindings for diagrams in models of a double theory.
 
+use std::collections::HashMap;
 use std::rc::Rc;
 
 use all_the_same::all_the_same;
+use catlog::tt;
+use catlog::tt::toplevel::Toplevel;
 use derive_more::From;
 use serde::{Deserialize, Serialize};
 use tsify::Tsify;
+use ustr::ustr;
 use wasm_bindgen::prelude::*;
 
 use catcolab_document_types::current::*;
@@ -22,14 +26,15 @@
 use super::theory::{DblTheory, DblTheoryBox};
 
 /// A box containing a diagram in a model of a double theory.
-#[derive(From)]
+#[derive(From, Clone)]
 pub enum DblModelDiagramBox {
     /// A diagram in a model of a discrete double theory.
     Discrete(diagram::DblModelDiagram<DiscreteDblModelMapping, DiscreteDblModel>),
     // Modal(), # TODO: Not implemented.
 }
 
 /// Wasm binding for a diagram in a model of a double theory.
+#[derive(Clone)]
 #[wasm_bindgen]
 pub struct DblModelDiagram {
     /// The boxed underlying diagram.
@@ -279,6 +284,63 @@
     pub JsResult<(), Vec<diagram::InvalidDiscreteDblModelDiagram>>,
 );
 
+/// A named collection of diagrams of double models.
+#[wasm_bindgen]
+pub struct DblDiagramMap {
+    #[wasm_bindgen(skip)]
+    diagrams: HashMap<String, DblModelDiagram>,
+    #[wasm_bindgen(skip)]
+    toplevel: Toplevel,
+}
+
+impl Default for DblDiagramMap {
+    fn default() -> Self {
+        Self::new()
+    }
+}
+
+#[wasm_bindgen]
+impl DblDiagramMap {
+    /// Constructs an empty collection of models.
+    #[wasm_bindgen(constructor)]
+    pub fn new() -> Self {
+        DblDiagramMap {
+            diagrams: HashMap::new(),
+            toplevel: Toplevel::new(tt::theory::std_theories()),
+        }
+    }
+
+    /// Returns whether the collection contains a model with the given name.
+    #[wasm_bindgen(js_name = "has")]
+    pub fn contains_key(&self, id: &str) -> bool {
+        self.diagrams.contains_key(id)
+    }
+
+    /// Inserts a model with the given name.
+    #[wasm_bindgen(js_name = "set")]
+    pub fn insert(&mut self, id: String, diagram: &DblModelDiagram) {
+        // let id_ustr = ustr(&id);
+        self.diagrams.insert(id, diagram.clone());
+        // let DblModelDiagramBox::Discrete(diagram::DblModelDiagram(_, model)) = diagram.diagram
+        // else {
+        //     panic!()
+        // };
+        // if let Some((ty_s, ty_v)) = &model.ty {
+        //     let Some(theory) = model.theory().try_into_tt() else {
+        //         return;
+        //     };
+        //     self.toplevel.declarations.insert(
+        //         NameSegment::Text(id_ustr),
+        //         TopDecl::Type(Type::new(
+        //             tt::theory::Theory::new(ustr("_").into(), theory),
+        //             ty_s.clone(),
+        //             ty_v.clone(),
+        //         )),
+        //     );
+        // }
+    }
+}
+
 /// Elaborates a diagram defined by a notebook into a catlog diagram.
 #[wasm_bindgen(js_name = "elaborateDiagram")]
 pub fn elaborate_diagram(
@@ -290,6 +352,7 @@
         match judgment {
             DiagramJudgment::Object(decl) => diagram.add_ob(&decl)?,
             DiagramJudgment::Morphism(decl) => diagram.add_mor(&decl)?,
+            DiagramJudgment::Instantiation(_) => return Err("Instantiation not supported".into()),
             DiagramJudgment::Equation(_) => {
                 return Err("Elaboration of equations in diagrams is not yet supported".into());
             }

packages/catlog-wasm/src/theories.rs

@@ -534,6 +534,23 @@ impl ThPowerSystem {
     }
 }
 
+/// A theory of the DEC
+#[wasm_bindgen]
+pub struct ThDEC(Rc<theory::ModalDblTheory<Unital>>);
+
+#[wasm_bindgen]
+impl ThDEC {
+    #[wasm_bindgen(constructor)]
+    pub fn new() -> Self {
+        Self(Rc::new(theories::th_multicategory())) // TODO symmetric?
+    }
+
+    #[wasm_bindgen]
+    pub fn theory(&self) -> DblTheory {
+        DblTheory(self.0.clone().into())
+    }
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;

packages/catlog-wasm/src/theory.rs

@@ -324,6 +324,14 @@ impl DblTheory {
             }
         })
     }
+
+    /// Does the theory support elaboriating diagrams?
+    ///
+    /// Eventually diagrams will be replaced by instances.
+    #[wasm_bindgen(js_name = "canElaborateDiagrams")]
+    pub fn can_elaborate_diagrams(&self) -> bool {
+        matches!(&self.0, DblTheoryBox::Discrete(_))
+    }
 }
 
 /// Mapping from object types to numerical indices.

packages/document-methods/src/diagram.ts

@@ -53,6 +53,18 @@ export const newDiagramMorphismDecl = (
     cod: null,
 });
 
+/** Create a new instantiation of an existing model. */
+export const newInstantiatedDiagram = (
+    diagram?: Link | null,
+): DiagramJudgment & { tag: "instantiation" } => ({
+    tag: "instantiation",
+    id: v7(),
+    name: "",
+    diagram: diagram ?? null,
+    specializations: [],
+});
+
+
 /** Duplicate a diagram judgment, creating a fresh UUID. */
 export const duplicateDiagramJudgment = (jgmt: DiagramJudgment): DiagramJudgment => ({
     ...structuredClone(jgmt),

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

@@ -2,6 +2,8 @@
 use tsify::Tsify;
 use uuid::Uuid;
 
+use crate::v1::Link;
+
 use super::model::{Mor, Ob};
 use super::theory::{MorType, ObType};
 
@@ -80,4 +82,36 @@
     /// Declares an equation between morphisms in the diagram.
     #[serde(rename = "equation")]
     Equation(DiagramEqnDecl),
+
+    /// Declares an instantiated diagram
+    #[serde(rename = "instantiation")]
+    Instantiation(InstantiatedDiagram),
+}
+
+/// Instantiates an existing diagram into the current diagram
+#[derive(Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
+#[tsify(into_wasm_abi, from_wasm_abi, missing_as_null)]
+pub struct InstantiatedDiagram {
+    /// Human-readable label for the instantiation.
+    pub name: String,
+
+    /// Globally unique identifier of the instantiation.
+    pub id: Uuid,
+
+    /// Link to the diagram to instantiate.
+    pub diagram: Option<Link>,
+
+    /// List of specializations to perform on the instantiated diagram.
+    pub specializations: Vec<SpecializeDiagram>,
+}
+
+/// A specialization of a generating object in an instantiated diagram.
+#[derive(Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
+#[tsify(into_wasm_abi, from_wasm_abi, missing_as_null)]
+pub struct SpecializeDiagram {
+    /// ID (qualified name) of generating object to specialize.
+    pub id: Option<String>,
+
+    /// Object to insert as the specialization.
+    pub ob: Option<Ob>,
 }

packages/frontend/src/App.tsx

@@ -11,6 +11,7 @@ import * as uuid from "uuid";
 
 import { Button } from "catcolab-ui-components";
 import { Api, ApiContext, useApi } from "./api";
+import { createDiagramLibraryWithApi, DiagramLibraryContext } from "./diagram";
 import { helpRoutes } from "./help/routes";
 import { createModelLibraryWithApi, ModelLibraryContext } from "./model";
 import { createModel } from "./model/document";
@@ -43,6 +44,7 @@ const Root = (props: RouteSectionProps) => {
 
     const theories = stdTheories;
     const models = createModelLibraryWithApi(api, theories);
+    const diagrams = createDiagramLibraryWithApi(api, theories);
 
     return (
         <FirebaseProvider app={firebaseApp}>
@@ -51,6 +53,7 @@ const Root = (props: RouteSectionProps) => {
                     [ApiContext, api],
                     [TheoryLibraryContext, theories],
                     [ModelLibraryContext, models],
+                    [DiagramLibraryContext, diagrams],
                     UserStateProvider,
                 ]}
             >

packages/frontend/src/components/id_input.tsx

@@ -113,7 +113,7 @@ export function IdInput(
 
     const isComplete = () => {
         const name = props.id ? idToText(props.id) : "";
-        return text() === name;
+        return name === "" || text() === name;
     };
 
     const status = (): InlineInputErrorStatus => {
@@ -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) {

packages/frontend/src/components/index.ts

@@ -3,3 +3,4 @@ export * from "./document_picker";
 export * from "./id_input";
 export * from "./json_import";
 export * from "./rich_text_editor";
+export * from "./instantiation_cell_editor.tsx";