From f950a5c9b3bd6f4b79131085ba535dc21de169b3 Mon Sep 17 00:00:00 2001 From: tslil-topos Date: Tue, 26 May 2026 12:35:11 -0700 Subject: [PATCH] feature: Petri net document type, delta lens Following the plan in https://github.com/ToposInstitute/CatColab-Roadmap/issues/59 , this change implements a bespoke document type for Petri nets which mirrors that used by Petrinaut internally, but constrained to those subset of features we will aim to support. Additionally it introduces a "delta lens" trait (for documents, is the intention). This is designed to support the use-case of keeping two different document types containing "compatible" content in-sync with one-another by providing a structured serialisation to, and updates based on changes in, "formal content". This lens trait is implemented for Notebooks and PetriNets. Future work: * integration of autosurgeon in the rust to allow automerge to learn from delta lens driven updates * teaching the backend about linked pairs of documents (Notebook + Petri net), and wiring them together with the delta lenses * much front-end work to support the embedded component and interacting with these linked pairs, along with some constraints on what the notebook editor will accept/allow in that mode --- packages/backend/src/user_state.rs | 2 + packages/document-types/src/v0/api.rs | 4 +- packages/document-types/src/v0/document.rs | 8 + .../document-types/src/v0/model_judgment.rs | 24 +- packages/document-types/src/v2/document.rs | 8 +- packages/document-types/src/v2/lens/mod.rs | 8 + .../document-types/src/v2/lens/notebook.rs | 35 +++ .../document-types/src/v2/lens/petri_test.rs | 230 ++++++++++++++++++ .../document-types/src/v2/lens/petrinet.rs | 181 ++++++++++++++ packages/document-types/src/v2/lens/types.rs | 79 ++++++ packages/document-types/src/v2/mod.rs | 3 + packages/document-types/src/v2/petrinet.rs | 47 ++++ packages/frontend/src/model/model_library.ts | 7 + 13 files changed, 627 insertions(+), 9 deletions(-) create mode 100644 packages/document-types/src/v2/lens/mod.rs create mode 100644 packages/document-types/src/v2/lens/notebook.rs create mode 100644 packages/document-types/src/v2/lens/petri_test.rs create mode 100644 packages/document-types/src/v2/lens/petrinet.rs create mode 100644 packages/document-types/src/v2/lens/types.rs create mode 100644 packages/document-types/src/v2/petrinet.rs diff --git a/packages/backend/src/user_state.rs b/packages/backend/src/user_state.rs index 7042ce56a..34748c736 100644 --- a/packages/backend/src/user_state.rs +++ b/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() } diff --git a/packages/document-types/src/v0/api.rs b/packages/document-types/src/v0/api.rs index 5ab7838eb..899aa7502 100644 --- a/packages/document-types/src/v0/api.rs +++ b/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)] diff --git a/packages/document-types/src/v0/document.rs b/packages/document-types/src/v0/document.rs index 2ae548483..b0cfa63c7 100644 --- a/packages/document-types/src/v0/document.rs +++ b/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}")), } } diff --git a/packages/document-types/src/v0/model_judgment.rs b/packages/document-types/src/v0/model_judgment.rs index e9d7dde16..d3e026495 100644 --- a/packages/document-types/src/v0/model_judgment.rs +++ b/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 { diff --git a/packages/document-types/src/v2/document.rs b/packages/document-types/src/v2/document.rs index 6f142093e..fe6c9476d 100644 --- a/packages/document-types/src/v2/document.rs +++ b/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 { diff --git a/packages/document-types/src/v2/lens/mod.rs b/packages/document-types/src/v2/lens/mod.rs new file mode 100644 index 000000000..7e6f30c18 --- /dev/null +++ b/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::*; diff --git a/packages/document-types/src/v2/lens/notebook.rs b/packages/document-types/src/v2/lens/notebook.rs new file mode 100644 index 000000000..b88bcb703 --- /dev/null +++ b/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 { + 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 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); + } + } + } + } +} diff --git a/packages/document-types/src/v2/lens/petri_test.rs b/packages/document-types/src/v2/lens/petri_test.rs new file mode 100644 index 000000000..3d28b2e50 --- /dev/null +++ b/packages/document-types/src/v2/lens/petri_test.rs @@ -0,0 +1,230 @@ +#[cfg(test)] +mod tests { + use std::collections::HashMap; + + use uuid::Uuid; + + use crate::v0::model::Ob; + use crate::v0::model_judgment::{ModelJudgment, MorDecl, ObDecl}; + use crate::v0::theory::{Modality, MorType, ObOp, ObType}; + use crate::v2::cell::NotebookCell; + use crate::v2::lens::types::{FormalContentDelta, FormalContentDeltaLens}; + use crate::v2::notebook::Notebook; + use crate::v2::petrinet::{ + PetriNetArc, PetriNetDocumentContent, PetriNetPlace, PetriNetTransition, + }; + + const S: Uuid = Uuid::from_u128(1); + const I: Uuid = Uuid::from_u128(2); + const INFECT: Uuid = Uuid::from_u128(3); + + fn empty_notebook() -> Notebook { + Notebook { + cell_contents: HashMap::new(), + cell_order: vec![], + } + } + + fn empty_petri_net() -> PetriNetDocumentContent { + PetriNetDocumentContent { + name: String::new(), + places: vec![], + transitions: vec![], + version: "2".to_string(), + } + } + + #[test] + fn petri_net_to_formal_content() { + let pn = PetriNetDocumentContent { + name: String::new(), + places: vec![ + PetriNetPlace { + id: S, + name: "S".to_string(), + x: 0.0, + y: 0.0, + }, + PetriNetPlace { + id: I, + name: "I".to_string(), + x: 0.0, + y: 0.0, + }, + ], + transitions: vec![PetriNetTransition { + id: INFECT, + name: "infect".to_string(), + input_arcs: vec![ + PetriNetArc { place_id: S, weight: 1 }, + PetriNetArc { place_id: I, weight: 1 }, + ], + output_arcs: vec![PetriNetArc { place_id: I, weight: 2 }], + x: 0.0, + y: 0.0, + }], + version: "2".to_string(), + }; + + assert_eq!( + pn.to_formal_content(), + vec![ + ModelJudgment::Object(ObDecl { + id: S, + name: "S".to_string(), + ob_type: ObType::Basic(ustr::ustr("Object")), + }), + ModelJudgment::Object(ObDecl { + id: I, + name: "I".to_string(), + ob_type: ObType::Basic(ustr::ustr("Object")), + }), + ModelJudgment::Morphism(MorDecl { + id: INFECT, + name: "infect".to_string(), + mor_type: MorType::Hom(Box::new(ObType::Basic(ustr::ustr("Object")))), + dom: Some(Ob::App { + op: ObOp::Basic(ustr::ustr("tensor")), + ob: Box::new(Ob::List { + modality: Modality::SymmetricList, + objects: vec![ + Some(Ob::Basic(S.to_string())), + Some(Ob::Basic(I.to_string())), + ], + }), + }), + cod: Some(Ob::App { + op: ObOp::Basic(ustr::ustr("tensor")), + ob: Box::new(Ob::List { + modality: Modality::SymmetricList, + objects: vec![ + Some(Ob::Basic(I.to_string())), + Some(Ob::Basic(I.to_string())), + ], + }), + }), + }), + ] + ); + } + + #[test] + fn notebook_round_trips_through_petri_net() { + // this is not really SI(R), but that would be too long to elaborate + // here. + let nb = Notebook { + cell_contents: HashMap::from([ + ( + S, + NotebookCell::Formal { + id: S, + content: ModelJudgment::Object(ObDecl { + id: S, + name: "S".to_string(), + ob_type: ObType::Basic(ustr::ustr("Object")), + }), + }, + ), + ( + INFECT, + NotebookCell::Formal { + id: INFECT, + content: ModelJudgment::Morphism(MorDecl { + id: INFECT, + name: "infect".to_string(), + mor_type: MorType::Hom(Box::new(ObType::Basic(ustr::ustr("Object")))), + dom: Some(Ob::App { + op: ObOp::Basic(ustr::ustr("tensor")), + ob: Box::new(Ob::List { + modality: Modality::SymmetricList, + objects: vec![Some(Ob::Basic(S.to_string()))], + }), + }), + cod: Some(Ob::App { + op: ObOp::Basic(ustr::ustr("tensor")), + ob: Box::new(Ob::List { + modality: Modality::SymmetricList, + objects: vec![Some(Ob::Basic(S.to_string()))], + }), + }), + }), + }, + ), + ]), + cell_order: vec![S, INFECT], + }; + + let mut pn = empty_petri_net(); + pn.apply_delta(&FormalContentDelta::diff(&[], &nb.to_formal_content())); + + let mut nb2 = empty_notebook(); + nb2.apply_delta(&FormalContentDelta::diff(&[], &pn.to_formal_content())); + + assert_eq!(nb2, nb); + } + + #[test] + fn insert_update_remove_on_both_sides() { + let mut pn = empty_petri_net(); + let mut nb = empty_notebook(); + + // Insert S on the petri net side, propagate to notebook. + pn.places.push(PetriNetPlace { + id: S, + name: "S".to_string(), + x: 0.0, + y: 0.0, + }); + nb.apply_delta(&FormalContentDelta::diff(&[], &pn.to_formal_content())); + let should_be = Notebook { + cell_contents: HashMap::from([( + Uuid::from_u128(1), + NotebookCell::Formal { + id: Uuid::from_u128(1), + content: ModelJudgment::Object(ObDecl { + name: "S".to_string(), + id: Uuid::from_u128(1), + ob_type: ObType::Basic(ustr::ustr("Object")), + }), + }, + )]), + cell_order: vec![Uuid::from_u128(1)], + }; + assert_eq!(nb, should_be); + + // Update S on the notebook side, propagate to petri net. + let cell_id = *nb.cell_order.first().unwrap(); + nb.cell_contents.insert( + cell_id, + NotebookCell::Formal { + id: cell_id, + content: ModelJudgment::Object(ObDecl { + id: S, + name: "S_renamed".to_string(), + ob_type: ObType::Basic(ustr::ustr("Object")), + }), + }, + ); + let pn_before = pn.to_formal_content(); + pn.apply_delta(&FormalContentDelta::diff(&pn_before, &nb.to_formal_content())); + let should_be = PetriNetDocumentContent { + name: String::new(), + places: vec![PetriNetPlace { + id: Uuid::from_u128(1), + name: "S_renamed".to_string(), + x: 0.0, + y: 0.0, + }], + transitions: Vec::new(), + version: "2".to_string(), + }; + assert_eq!(pn, should_be); + + // Remove S on the petri net side, propagate to notebook. + let pn_before = pn.to_formal_content(); + pn.places.clear(); + nb.apply_delta(&FormalContentDelta::diff(&pn_before, &pn.to_formal_content())); + let should_be = empty_notebook(); + assert_eq!(nb, should_be); + } +} diff --git a/packages/document-types/src/v2/lens/petrinet.rs b/packages/document-types/src/v2/lens/petrinet.rs new file mode 100644 index 000000000..c557e3b59 --- /dev/null +++ b/packages/document-types/src/v2/lens/petrinet.rs @@ -0,0 +1,181 @@ +use std::str::FromStr; + +use uuid::Uuid; + +use crate::v0::model::Ob; +use crate::v0::model_judgment::{ModelJudgment, MorDecl, ObDecl}; +use crate::v0::theory::{Modality, MorType, ObOp, ObType}; +use crate::v2::lens::types::{FormalContentChange, FormalContentDelta, FormalContentDeltaLens}; +use crate::v2::petrinet::{ + PetriNetArc, PetriNetDocumentContent, PetriNetPlace, PetriNetTransition, +}; + +// We have to bake in the particulars of the theory for Petri nets here so that +// our lens code functions correctly. +fn petri_ob_type() -> ObType { + ObType::Basic(ustr::ustr("Object")) +} + +fn petri_mor_type() -> MorType { + MorType::Hom(Box::new(petri_ob_type())) +} + +// Places <> Objects +fn place_from_ob_decl(ob_decl: &ObDecl) -> PetriNetPlace { + // WARNING! we completely ignore ob_decl.ob_type, the assumption here and + // elsewhere is that this delta lens for a Petri net will not be paired with + // deltas that are not interpretable into Petrin nets. + PetriNetPlace { + id: ob_decl.id, + name: ob_decl.name.clone(), + // In the future we may wish to do something more clever than defaulting + // to (0,0) for new data + x: 0.0, + y: 0.0, + } +} + +fn ob_decl_from_place(place: &PetriNetPlace) -> ObDecl { + ObDecl { + id: place.id, + name: place.name.clone(), + ob_type: petri_ob_type(), + } +} + +// Transitions <> Morphisms +fn transition_from_mor_decl(mor_decl: &MorDecl) -> PetriNetTransition { + // WARNING! we intentionally ignore mor_decl.mor_type, see the above comment + // on place_from_obj. + PetriNetTransition { + id: mor_decl.id, + name: mor_decl.name.clone(), + input_arcs: mor_decl.dom.as_ref().map(tensor_ob_to_arcs).unwrap_or_default(), + output_arcs: mor_decl.cod.as_ref().map(tensor_ob_to_arcs).unwrap_or_default(), + // Likewise here, future code changes could improve this with some kind + // of heuristic. + x: 0.0, + y: 0.0, + } +} + +fn mor_decl_from_transition(t: &PetriNetTransition) -> MorDecl { + MorDecl { + id: t.id, + name: t.name.clone(), + mor_type: petri_mor_type(), + dom: Some(arcs_to_tensor_ob(&t.input_arcs)), + cod: Some(arcs_to_tensor_ob(&t.output_arcs)), + } +} + +// Arcs <> Tensors +fn arcs_to_tensor_ob(arcs: &[PetriNetArc]) -> Ob { + Ob::App { + op: ObOp::Basic(ustr::ustr("tensor")), + ob: Box::new(Ob::List { + modality: Modality::SymmetricList, + objects: arcs_to_repeated_ob_list(arcs), + }), + } +} + +fn tensor_ob_to_arcs(ob: &Ob) -> Vec { + // WARNING! once more we make strong assumptions about the data, we are not + // checking that the modality is the one "it should be" for the theory of + // Petri nets and so forth. + match ob { + Ob::App { ob, .. } => match ob.as_ref() { + Ob::List { objects, .. } => repeated_ob_list_to_arcs(objects), + _ => vec![], + }, + _ => vec![], + } +} + +fn arcs_to_repeated_ob_list(arcs: &[PetriNetArc]) -> Vec> { + let mut objects = Vec::new(); + for arc in arcs { + let ob_str = arc.place_id.to_string(); + // we use weight as a repetition count + for _ in 0..arc.weight { + objects.push(Some(Ob::Basic(ob_str.clone()))); + } + } + objects +} + +fn repeated_ob_list_to_arcs(objects: &[Option]) -> Vec { + let mut arcs: Vec = Vec::new(); + // matching the above, here we assume that *adjacent* repetitions should + // resolve to weight + for ob in objects.iter().flatten() { + let Some(place_id) = place_id_from_ob(ob) else { + continue; + }; + if let Some(last) = arcs.last_mut() + && last.place_id == place_id + { + last.weight += 1; + } else { + arcs.push(PetriNetArc { place_id, weight: 1 }); + } + } + arcs +} + +fn place_id_from_ob(ob: &Ob) -> Option { + match ob { + Ob::Basic(s) => Uuid::from_str(s).ok(), + _ => None, + } +} + +impl FormalContentDeltaLens for PetriNetDocumentContent { + fn to_formal_content(&self) -> Vec { + let places = self.places.iter().map(|p| ModelJudgment::Object(ob_decl_from_place(p))); + let transitions = self + .transitions + .iter() + .map(|t| ModelJudgment::Morphism(mor_decl_from_transition(t))); + places.chain(transitions).collect() + } + + fn apply_delta(&mut self, delta: &FormalContentDelta) { + for change in delta { + match change { + FormalContentChange::Upsert(jgmt) => match jgmt { + ModelJudgment::Object(ob_decl) => { + if let Some(place) = self.places.iter_mut().find(|p| p.id == ob_decl.id) { + // the only data carried by a place that could be + // modified by a FormalContentDelta is the name. + place.name = ob_decl.name.clone(); + } else { + self.places.push(place_from_ob_decl(ob_decl)); + } + } + ModelJudgment::Morphism(mor_decl) => { + if let Some(t) = self.transitions.iter_mut().find(|t| t.id == mor_decl.id) { + t.name = mor_decl.name.clone(); + t.input_arcs = + mor_decl.dom.as_ref().map(tensor_ob_to_arcs).unwrap_or_default(); + t.output_arcs = + mor_decl.cod.as_ref().map(tensor_ob_to_arcs).unwrap_or_default(); + } else { + self.transitions.push(transition_from_mor_decl(mor_decl)); + } + } + // WARNING! we silently ignore everything that doesn't fit + // the Petri net world view. Again it is the responsibility + // of downstream code to ensure that we do not land up in + // this case. + _ => {} + }, + FormalContentChange::Remove(id) => { + self.places.retain(|p| &p.id != id); + self.transitions.retain(|t| &t.id != id); + } + } + } + } +} diff --git a/packages/document-types/src/v2/lens/types.rs b/packages/document-types/src/v2/lens/types.rs new file mode 100644 index 000000000..69c65bc78 --- /dev/null +++ b/packages/document-types/src/v2/lens/types.rs @@ -0,0 +1,79 @@ +use std::collections::HashSet; +use uuid::Uuid; + +use crate::v0::model_judgment::ModelJudgment; + +pub type FormalContent = Vec; + +pub enum FormalContentChange { + Upsert(ModelJudgment), + Remove(Uuid), +} + +pub struct FormalContentDelta(Vec); + +impl IntoIterator for FormalContentDelta { + type Item = FormalContentChange; + type IntoIter = std::vec::IntoIter; + + fn into_iter(self) -> Self::IntoIter { + self.0.into_iter() + } +} + +impl<'a> IntoIterator for &'a FormalContentDelta { + type Item = &'a FormalContentChange; + type IntoIter = std::slice::Iter<'a, FormalContentChange>; + + fn into_iter(self) -> Self::IntoIter { + self.0.iter() + } +} + +impl FormalContentDelta { + /// Compute a diff in FormalContent space. + pub fn diff(old: &[ModelJudgment], new: &[ModelJudgment]) -> Self { + let old_ids: HashSet = old.iter().map(|j| j.id()).collect(); + let new_ids: HashSet = new.iter().map(|j| j.id()).collect(); + + let mut changes = Vec::new(); + + for j in new { + if old_ids.contains(&j.id()) { + // this code could be made more efficient in the future to avoid + // this iteration cost, but for now we assume that the models + // are small and O(N) is acceptable. + if let Some(old_j) = old.iter().find(|o| o.id() == j.id()) { + // Because we are using structural equality, if for whatever + // reason we have non-trivial equalities in the model/theory + // and we see the same data under different presentations we + // will produce an upsert. + if old_j != j { + changes.push(FormalContentChange::Upsert(j.clone())); + } + } + } else { + changes.push(FormalContentChange::Upsert(j.clone())); + } + } + + for j in old { + if !new_ids.contains(&j.id()) { + changes.push(FormalContentChange::Remove(j.id())); + } + } + + FormalContentDelta(changes) + } +} + +/// An approximate model of a delta lens on FormalContent for a given Rust type. +/// In the words of Dana Scott, "just because you call something something, +/// doesn't make it that." We trust that the reader's generosity will exceed +/// their rigour. +pub trait FormalContentDeltaLens { + /// Extract the formal content from a container. + fn to_formal_content(&self) -> FormalContent; + /// Given a diff in formal content space, update the container. + fn apply_delta(&mut self, delta: &FormalContentDelta); +} diff --git a/packages/document-types/src/v2/mod.rs b/packages/document-types/src/v2/mod.rs index ce20e6a8a..01a67f878 100644 --- a/packages/document-types/src/v2/mod.rs +++ b/packages/document-types/src/v2/mod.rs @@ -4,7 +4,9 @@ pub use v1::{analysis, api, diagram_judgment, model, model_judgment, path, theor pub mod cell; pub mod document; +pub mod lens; pub mod notebook; +pub mod petrinet; pub use analysis::*; pub use api::*; @@ -14,6 +16,7 @@ pub use document::*; pub use model::*; pub use model_judgment::*; pub use notebook::*; +pub use petrinet::*; pub use theory::*; #[cfg(test)] diff --git a/packages/document-types/src/v2/petrinet.rs b/packages/document-types/src/v2/petrinet.rs new file mode 100644 index 000000000..551f90620 --- /dev/null +++ b/packages/document-types/src/v2/petrinet.rs @@ -0,0 +1,47 @@ +use serde::{Deserialize, Serialize}; +use tsify::Tsify; +use uuid::Uuid; + +/// A type hierarchy mirroring the fragment of SDCPN from [Petrinaut's core +/// library](github.com/hashintel/hash/blob/d3ac60c5509bd2d5a478f2e5a56433c59d353f7b/libs/%40hashintel/petrinaut-core/src/types/sdcpn.ts) +/// which is interpretable in CatColabs conception of Petri nets. + +#[derive(PartialEq, Debug, Serialize, Deserialize, Tsify)] +#[tsify(into_wasm_abi, from_wasm_abi)] +pub struct PetriNetDocumentContent { + pub name: String, + pub places: Vec, + pub transitions: Vec, + pub version: String, /* TODO: we may or may not wish to track this + * separately from the document version. */ +} + +#[derive(PartialEq, Debug, Serialize, Deserialize, Tsify)] +#[tsify(into_wasm_abi, from_wasm_abi)] +pub struct PetriNetPlace { + pub id: Uuid, + pub name: String, + pub x: f64, + pub y: f64, +} + +#[derive(PartialEq, Debug, Serialize, Deserialize, Tsify)] +#[tsify(into_wasm_abi, from_wasm_abi)] +pub struct PetriNetTransition { + pub id: Uuid, + pub name: String, + #[serde(rename = "inputArcs")] + pub input_arcs: Vec, + #[serde(rename = "outputArcs")] + pub output_arcs: Vec, + pub x: f64, + pub y: f64, +} + +#[derive(PartialEq, Eq, Debug, Serialize, Deserialize, Tsify)] +#[tsify(into_wasm_abi, from_wasm_abi)] +pub struct PetriNetArc { + #[serde(rename = "placeId")] + pub place_id: Uuid, + pub weight: u32, +} diff --git a/packages/frontend/src/model/model_library.ts b/packages/frontend/src/model/model_library.ts index cd3e068b1..1ae712be1 100644 --- a/packages/frontend/src/model/model_library.ts +++ b/packages/frontend/src/model/model_library.ts @@ -317,6 +317,13 @@ function isPatchToFormalContent(doc: Document, patch: Patch): boolean { return false; } if (path[0] === "notebook" && path[1] === "cellContents" && path[2]) { + // TODO: Clean this up. ModelLibrary.addModel installs this on a + // DocHandle, so this helper is called for non-ModelDocuments + // even though notebook cell checks are model-specific. Probably make + // the caller narrow to ModelDocument, or split from notebook handling. + if (!("notebook" in doc)) { + return false; + } // Ignores changes to cells without formal content. const cell = doc.notebook.cellContents[path[2]]; if (cell?.tag !== "formal") {