Skip to content

Commit f950a5c

Browse files
author
tslil-topos
committed
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
1 parent c190c08 commit f950a5c

13 files changed

Lines changed: 627 additions & 9 deletions

File tree

packages/backend/src/user_state.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -505,6 +505,8 @@ pub mod arbitrary {
505505
DocumentType::Model,
506506
DocumentType::Diagram,
507507
DocumentType::Analysis,
508+
// TODO: Re-enable once DocumentType::PetriNet is restored in document-types.
509+
// DocumentType::PetriNet,
508510
])
509511
.boxed()
510512
}

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ use tsify::Tsify;
88
/// `id`, to avoid conflicts with other keys and unambiguously signal that the
99
/// data occur at the *database* level, rather than merely the *document* level.
1010
/// The same convention is used in document databases like CouchDB and MongoDB.
11-
#[derive(PartialEq, Eq, Debug, Serialize, Deserialize, Tsify)]
11+
#[derive(Clone, PartialEq, Eq, Debug, Serialize, Deserialize, Tsify)]
1212
#[tsify(into_wasm_abi, from_wasm_abi)]
1313
#[tsify(missing_as_null)]
1414
pub struct StableRef {
@@ -38,7 +38,7 @@ pub struct StableRef {
3838
///
3939
/// The source of the link is the document containing this data and the target
4040
/// of link is given by the data itself.
41-
#[derive(PartialEq, Eq, Debug, Serialize, Deserialize, Tsify)]
41+
#[derive(Clone, PartialEq, Eq, Debug, Serialize, Deserialize, Tsify)]
4242
#[tsify(into_wasm_abi, from_wasm_abi)]
4343
pub struct Link {
4444
#[serde(flatten)]

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -64,6 +64,12 @@ pub enum DocumentType {
6464
Diagram,
6565
#[cfg_attr(feature = "backend", autosurgeon(rename = "analysis"))]
6666
Analysis,
67+
// TODO: Re-enable this only after the frontend supports Petri net documents
68+
// throughout its document routing, menus ... other exhaustive checks over
69+
// document types.
70+
71+
// #[cfg_attr(feature = "backend", autosurgeon(rename = "petrinet"))]
72+
// PetriNet,
6773
}
6874

6975
impl FromStr for DocumentType {
@@ -74,6 +80,8 @@ impl FromStr for DocumentType {
7480
"model" => Ok(DocumentType::Model),
7581
"diagram" => Ok(DocumentType::Diagram),
7682
"analysis" => Ok(DocumentType::Analysis),
83+
// TODO: Re-enable with the PetriNet DocumentType variant above.
84+
// "petrinet" => Ok(DocumentType::PetriNet),
7785
other => Err(format!("unknown document type: {other}")),
7886
}
7987
}

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

Lines changed: 18 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ use super::model::{Mor, Ob};
77
use super::theory::{MorType, ObType};
88

99
/// Declares an object in a model of a double theory.
10-
#[derive(Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
10+
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
1111
#[tsify(into_wasm_abi, from_wasm_abi, missing_as_null)]
1212
pub struct ObDecl {
1313
/// Human-readable label for object.
@@ -22,7 +22,7 @@ pub struct ObDecl {
2222
}
2323

2424
/// Declares a morphism in a model of a double theory.
25-
#[derive(Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
25+
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
2626
#[tsify(into_wasm_abi, from_wasm_abi, missing_as_null)]
2727
pub struct MorDecl {
2828
/// Human-readable label for morphism.
@@ -43,7 +43,7 @@ pub struct MorDecl {
4343
}
4444

4545
/// Instantiates an existing model into the current model.
46-
#[derive(Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
46+
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
4747
#[tsify(into_wasm_abi, from_wasm_abi, missing_as_null)]
4848
pub struct InstantiatedModel {
4949
/// Human-readable label for the instantiation.
@@ -60,7 +60,7 @@ pub struct InstantiatedModel {
6060
}
6161

6262
/// A specialization of a generating object in an instantiated model.
63-
#[derive(Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
63+
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
6464
#[tsify(into_wasm_abi, from_wasm_abi, missing_as_null)]
6565
pub struct SpecializeModel {
6666
/// ID (qualified name) of generating object to specialize.
@@ -71,7 +71,7 @@ pub struct SpecializeModel {
7171
}
7272

7373
/// Declares an equation in a model of a double theory.
74-
#[derive(Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
74+
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
7575
#[tsify(into_wasm_abi, from_wasm_abi, missing_as_null)]
7676
pub struct EqnDecl {
7777
/// Human-readable label for equation.
@@ -88,7 +88,7 @@ pub struct EqnDecl {
8888
}
8989

9090
/// A judgment defining part of a model of a double theory.
91-
#[derive(Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
91+
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)]
9292
#[serde(tag = "tag")]
9393
#[tsify(into_wasm_abi, from_wasm_abi)]
9494
pub enum ModelJudgment {
@@ -109,6 +109,18 @@ pub enum ModelJudgment {
109109
Instantiation(InstantiatedModel),
110110
}
111111

112+
impl ModelJudgment {
113+
/// UUIDs are unique among all components, so we may extract them uniformly.
114+
pub fn id(&self) -> Uuid {
115+
match self {
116+
ModelJudgment::Object(d) => d.id,
117+
ModelJudgment::Morphism(d) => d.id,
118+
ModelJudgment::Equation(d) => d.id,
119+
ModelJudgment::Instantiation(d) => d.id,
120+
}
121+
}
122+
}
123+
112124
/// Arbitrary instances for property-based testing.
113125
#[cfg(feature = "property-tests")]
114126
pub(crate) mod arbitrary {

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

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ pub struct AnalysisDocumentContent {
4848
pub version: String,
4949
}
5050

51-
#[derive(PartialEq, Eq, Debug, Serialize, Deserialize, Tsify)]
51+
#[derive(PartialEq, Debug, Serialize, Deserialize, Tsify)]
5252
#[serde(tag = "type")]
5353
#[tsify(into_wasm_abi, from_wasm_abi)]
5454
pub enum Document {
@@ -58,6 +58,12 @@ pub enum Document {
5858
Diagram(DiagramDocumentContent),
5959
#[serde(rename = "analysis")]
6060
Analysis(AnalysisDocumentContent),
61+
// TODO: Re-enable this only after the frontend supports Petri net documents
62+
// throughout its document routing, menus ... other exhaustive checks over
63+
// document types.
64+
65+
// #[serde(rename = "petrinet")]
66+
// PetriNet(PetriNetDocumentContent),
6167
}
6268

6369
impl Document {
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
pub mod notebook;
2+
pub mod petrinet;
3+
pub mod types;
4+
5+
#[cfg(test)]
6+
mod petri_test;
7+
8+
pub use types::*;
Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,35 @@
1+
use crate::v0::model_judgment::ModelJudgment;
2+
use crate::v2::cell::NotebookCell;
3+
use crate::v2::lens::{
4+
FormalContent, FormalContentChange, FormalContentDelta, FormalContentDeltaLens,
5+
};
6+
use crate::v2::notebook::Notebook;
7+
8+
impl FormalContentDeltaLens for Notebook<ModelJudgment> {
9+
fn to_formal_content(&self) -> FormalContent {
10+
// We perform no filtering here, as this is intended to be a generic
11+
// delta lens implementation.
12+
self.formal_content().cloned().collect()
13+
}
14+
15+
fn apply_delta(&mut self, delta: &FormalContentDelta) {
16+
// Notebook<ModelJudgement> is very close to FormalContent already,
17+
// there's little to do.
18+
for change in delta {
19+
match change {
20+
FormalContentChange::Upsert(jgmt) => {
21+
let id = jgmt.id();
22+
let cell = NotebookCell::Formal { id, content: jgmt.clone() };
23+
if !self.cell_contents.contains_key(&id) {
24+
self.cell_order.push(id);
25+
}
26+
self.cell_contents.insert(id, cell);
27+
}
28+
FormalContentChange::Remove(id) => {
29+
self.cell_contents.remove(id);
30+
self.cell_order.retain(|i| i != id);
31+
}
32+
}
33+
}
34+
}
35+
}

0 commit comments

Comments
 (0)