Petri net document type and delta lens

packages/backend/src/user_state.rs

@@ -505,6 +505,8 @@ pub mod arbitrary {
             DocumentType::Model,
             DocumentType::Diagram,
             DocumentType::Analysis,
+            // TODO: Re-enable once DocumentType::PetriNet is restored in document-types.
+            // DocumentType::PetriNet,
         ])
         .boxed()
     }

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

@@ -8,7 +8,7 @@ use tsify::Tsify;
 /// `id`, to avoid conflicts with other keys and unambiguously signal that the
 /// data occur at the *database* level, rather than merely the *document* level.
 /// The same convention is used in document databases like CouchDB and MongoDB.
-#[derive(PartialEq, Eq, Debug, Serialize, Deserialize, Tsify)]
+#[derive(Clone, PartialEq, Eq, Debug, Serialize, Deserialize, Tsify)]
 #[tsify(into_wasm_abi, from_wasm_abi)]
 #[tsify(missing_as_null)]
 pub struct StableRef {
@@ -38,7 +38,7 @@ pub struct StableRef {
 ///
 /// The source of the link is the document containing this data and the target
 /// of link is given by the data itself.
-#[derive(PartialEq, Eq, Debug, Serialize, Deserialize, Tsify)]
+#[derive(Clone, PartialEq, Eq, Debug, Serialize, Deserialize, Tsify)]
 #[tsify(into_wasm_abi, from_wasm_abi)]
 pub struct Link {
     #[serde(flatten)]

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

@@ -64,6 +64,12 @@ pub enum DocumentType {
     Diagram,
     #[cfg_attr(feature = "backend", autosurgeon(rename = "analysis"))]
     Analysis,
+    // TODO: Re-enable this only after the frontend supports Petri net documents
+    // throughout its document routing, menus ... other exhaustive checks over
+    // document types.
+
+    // #[cfg_attr(feature = "backend", autosurgeon(rename = "petrinet"))]
+    // PetriNet,
 }
 
 impl FromStr for DocumentType {
@@ -74,6 +80,8 @@ impl FromStr for DocumentType {
             "model" => Ok(DocumentType::Model),
             "diagram" => Ok(DocumentType::Diagram),
             "analysis" => Ok(DocumentType::Analysis),
+            // TODO: Re-enable with the PetriNet DocumentType variant above.
+            // "petrinet" => Ok(DocumentType::PetriNet),
             other => Err(format!("unknown document type: {other}")),
         }
     }

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

@@ -7,7 +7,7 @@ use super::model::{Mor, Ob};
 use super::theory::{MorType, ObType};
 
 /// Declares an object in a model of a double theory.
-#[derive(Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
+#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
 #[tsify(into_wasm_abi, from_wasm_abi, missing_as_null)]
 pub struct ObDecl {
     /// Human-readable label for object.
@@ -22,7 +22,7 @@ pub struct ObDecl {
 }
 
 /// Declares a morphism in a model of a double theory.
-#[derive(Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
+#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
 #[tsify(into_wasm_abi, from_wasm_abi, missing_as_null)]
 pub struct MorDecl {
     /// Human-readable label for morphism.
@@ -43,7 +43,7 @@ pub struct MorDecl {
 }
 
 /// Instantiates an existing model into the current model.
-#[derive(Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
+#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
 #[tsify(into_wasm_abi, from_wasm_abi, missing_as_null)]
 pub struct InstantiatedModel {
     /// Human-readable label for the instantiation.
@@ -60,7 +60,7 @@ pub struct InstantiatedModel {
 }
 
 /// A specialization of a generating object in an instantiated model.
-#[derive(Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
+#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
 #[tsify(into_wasm_abi, from_wasm_abi, missing_as_null)]
 pub struct SpecializeModel {
     /// ID (qualified name) of generating object to specialize.
@@ -71,7 +71,7 @@ pub struct SpecializeModel {
 }
 
 /// Declares an equation in a model of a double theory.
-#[derive(Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
+#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
 #[tsify(into_wasm_abi, from_wasm_abi, missing_as_null)]
 pub struct EqnDecl {
     /// Human-readable label for equation.
@@ -88,7 +88,7 @@ pub struct EqnDecl {
 }
 
 /// A judgment defining part of a model of a double theory.
-#[derive(Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
+#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
 #[serde(tag = "tag")]
 #[tsify(into_wasm_abi, from_wasm_abi)]
 pub enum ModelJudgment {
@@ -109,6 +109,18 @@ pub enum ModelJudgment {
     Instantiation(InstantiatedModel),
 }
 
+impl ModelJudgment {
+    /// UUIDs are unique among all components, so we may extract them uniformly.
+    pub fn id(&self) -> Uuid {
+        match self {
+            ModelJudgment::Object(d) => d.id,
+            ModelJudgment::Morphism(d) => d.id,
+            ModelJudgment::Equation(d) => d.id,
+            ModelJudgment::Instantiation(d) => d.id,
+        }
+    }
+}
+
 /// Arbitrary instances for property-based testing.
 #[cfg(feature = "property-tests")]
 pub(crate) mod arbitrary {

packages/document-types/src/v2/document.rs

@@ -48,7 +48,7 @@ pub struct AnalysisDocumentContent {
     pub version: String,
 }
 
-#[derive(PartialEq, Eq, Debug, Serialize, Deserialize, Tsify)]
+#[derive(PartialEq, Debug, Serialize, Deserialize, Tsify)]
 #[serde(tag = "type")]
 #[tsify(into_wasm_abi, from_wasm_abi)]
 pub enum Document {
@@ -58,6 +58,12 @@ pub enum Document {
     Diagram(DiagramDocumentContent),
     #[serde(rename = "analysis")]
     Analysis(AnalysisDocumentContent),
+    // TODO: Re-enable this only after the frontend supports Petri net documents
+    // throughout its document routing, menus ... other exhaustive checks over
+    // document types.
+
+    // #[serde(rename = "petrinet")]
+    // PetriNet(PetriNetDocumentContent),
 }
 
 impl Document {

packages/document-types/src/v2/lens/mod.rs

@@ -0,0 +1,8 @@
+pub mod notebook;
+pub mod petrinet;
+pub mod types;
+
+#[cfg(test)]
+mod petri_test;
+
+pub use types::*;

packages/document-types/src/v2/lens/notebook.rs

@@ -0,0 +1,35 @@
+use crate::v0::model_judgment::ModelJudgment;
+use crate::v2::cell::NotebookCell;
+use crate::v2::lens::{
+    FormalContent, FormalContentChange, FormalContentDelta, FormalContentDeltaLens,
+};
+use crate::v2::notebook::Notebook;
+
+impl FormalContentDeltaLens for Notebook<ModelJudgment> {
+    fn to_formal_content(&self) -> FormalContent {
+        // We perform no filtering here, as this is intended to be a generic
+        // delta lens implementation.
+        self.formal_content().cloned().collect()
+    }
+
+    fn apply_delta(&mut self, delta: &FormalContentDelta) {
+        // Notebook<ModelJudgement> is very close to FormalContent already,
+        // there's little to do.
+        for change in delta {
+            match change {
+                FormalContentChange::Upsert(jgmt) => {
+                    let id = jgmt.id();
+                    let cell = NotebookCell::Formal { id, content: jgmt.clone() };
+                    if !self.cell_contents.contains_key(&id) {
+                        self.cell_order.push(id);
+                    }
+                    self.cell_contents.insert(id, cell);
+                }
+                FormalContentChange::Remove(id) => {
+                    self.cell_contents.remove(id);
+                    self.cell_order.retain(|i| i != id);
+                }
+            }
+        }
+    }
+}