diff --git a/packages/catlog-wasm/src/model.rs b/packages/catlog-wasm/src/model.rs index 7dae0666c..d8a914848 100644 --- a/packages/catlog-wasm/src/model.rs +++ b/packages/catlog-wasm/src/model.rs @@ -918,4 +918,98 @@ pub(crate) mod tests { assert_eq!(model.mor_generators().len(), 2); assert_eq!(model.validate().0, JsResult::Ok(())); } + + pub(crate) fn dec_heat_eq(th: &DblTheory, ids: [Uuid; 3]) -> DblModel { + let mut model = DblModel::new(th); + let [form0, op1dot, op1laplace] = ids; + let ob_type = ObType::Basic("Object".into()); + assert!( + model + .add_ob(&ObDecl { + name: "Form0".into(), + id: form0, + ob_type: ob_type.clone() + }) + .is_ok() + ); + assert!( + model + .add_mor(&MorDecl { + name: "Dot".into(), + id: op1dot, + mor_type: MorType::Basic("Form0".into()), + dom: Some(Ob::Basic(form0.to_string())), + cod: Some(Ob::Basic(form0.to_string())) + }) + .is_ok() + ); + assert!( + model + .add_mor(&MorDecl { + name: "Laplace".into(), + id: op1laplace, + mor_type: MorType::Basic("Form0".into()), + dom: Some(Ob::Basic(form0.to_string())), + cod: Some(Ob::Basic(form0.to_string())) + }) + .is_ok() + ); + model + } + + pub(crate) fn dec_wedge(th: &DblTheory, ids: [Uuid; 4]) -> DblModel { + let mut model = DblModel::new(th); + let [form0, form1, op1d, op2wedge] = ids; + let ob_type = ObType::Basic("Object".into()); + assert!( + model + .add_ob(&ObDecl { + name: "Form0".into(), + id: form0, + ob_type: ob_type.clone() + }) + .is_ok() + ); + assert!( + model + .add_ob(&ObDecl { + name: "Form1".into(), + id: form1, + ob_type: ob_type.clone() + }) + .is_ok() + ); + assert!( + model + .add_mor(&MorDecl { + name: "d".into(), + id: op1d, + mor_type: MorType::Basic("Multihom".into()), + dom: Some(Ob::List { + modality: Modality::List, + objects: vec![Some(Ob::Basic(form0.to_string()))] + }), + cod: Some(Ob::Basic(form1.to_string())) + }) + .is_ok() + ); + assert!( + model + .add_mor(&MorDecl { + name: "wedge".into(), + id: op2wedge, + mor_type: MorType::Basic("Multihom".into()), + dom: Some(Ob::List { + modality: Modality::List, + objects: vec![ + Some(Ob::Basic(form0.to_string())), + Some(Ob::Basic(form1.to_string())) + ] + }), + cod: Some(Ob::Basic(form1.to_string())) + }) + .is_ok() + ); + model + } } diff --git a/packages/catlog-wasm/src/model_diagram.rs b/packages/catlog-wasm/src/model_diagram.rs index d0b0b7b97..0699d1e71 100644 --- a/packages/catlog-wasm/src/model_diagram.rs +++ b/packages/catlog-wasm/src/model_diagram.rs @@ -9,10 +9,12 @@ use tsify::Tsify; use wasm_bindgen::prelude::*; use catcolab_document_types::current::*; -use catlog::dbl::model::{DblModel as _, DiscreteDblModel, FpDblModel, MutDblModel}; +use catlog::dbl::modal::ModalDblModelMapping; +use catlog::dbl::model::{DblModel as _, DiscreteDblModel, FpDblModel, ModalDblModel, MutDblModel}; use catlog::dbl::model_diagram as diagram; -use catlog::dbl::model_morphism::DiscreteDblModelMapping; -use catlog::one::FgCategory; +use catlog::dbl::model_morphism::{DiscreteDblModelMapping, MutDblModelMapping}; +use catlog::dbl::theory::{DblTheory as DblT, Unital}; +use catlog::one::{Category, FgCategory}; use catlog::zero::{MutMapping, NameLookup, NameSegment, Namespace, QualifiedLabel, QualifiedName}; use super::model::DblModel; @@ -22,11 +24,14 @@ use super::result::JsResult; use super::theory::{DblTheory, DblTheoryBox}; /// A box containing a diagram in a model of a double theory. +#[allow(clippy::large_enum_variant)] #[derive(From)] pub enum DblModelDiagramBox { /// A diagram in a model of a discrete double theory. Discrete(diagram::DblModelDiagram), - // Modal(), # TODO: Not implemented. + /// A diagram in a model of a modal double theory. + // TODO moar kind fixing + Modal(diagram::DblModelDiagram>), } /// Wasm binding for a diagram in a model of a double theory. @@ -47,6 +52,11 @@ impl DblModelDiagram { let model = DiscreteDblModel::new(theory.clone()); diagram::DblModelDiagram(mapping, model).into() } + DblTheoryBox::ModalUnital(theory) => { + let mapping = Default::default(); + let model = ModalDblModel::new(theory.clone()); + diagram::DblModelDiagram(mapping, model).into() + } _ => panic!("Diagrams only implemented for discrete double theories"), }; Self { @@ -57,8 +67,8 @@ impl DblModelDiagram { /// Adds an object to the diagram. pub fn add_ob(&mut self, decl: &DiagramObDecl) -> Result<(), String> { - all_the_same!(match &mut self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { + match &mut self.diagram { + DblModelDiagramBox::Discrete(diagram) => { let (mapping, model) = diagram.into(); let ob_type: QualifiedName = Elaborator.elab(&decl.ob_type)?; if let Some(over) = decl.over.as_ref().map(|ob| Elaborator.elab(ob)).transpose()? { @@ -66,7 +76,16 @@ impl DblModelDiagram { } model.add_ob(decl.id.into(), ob_type); } - }); + DblModelDiagramBox::Modal(diagram) => { + let (mapping, model) = diagram.into(); + let ob_type: catlog::dbl::modal::ModeApp = + Elaborator.elab(&decl.ob_type)?; + if let Some(over) = decl.over.as_ref().map(|ob| Elaborator.elab(ob)).transpose()? { + mapping.assign_ob(decl.id.into(), over); + } + model.add_ob(decl.id.into(), ob_type); + } + }; if !decl.name.is_empty() { self.ob_namespace.set_label(decl.id, decl.name.as_str().into()); } @@ -75,10 +94,10 @@ impl DblModelDiagram { /// Adds a morphism to the diagram. pub fn add_mor(&mut self, decl: &DiagramMorDecl) -> Result<(), String> { - all_the_same!(match &mut self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { + match &mut self.diagram { + DblModelDiagramBox::Discrete(diagram) => { let (mapping, model) = diagram.into(); - let mor_type = Elaborator.elab(&decl.mor_type)?; + let mor_type: catlog::one::QualifiedPath = Elaborator.elab(&decl.mor_type)?; model.make_mor(decl.id.into(), mor_type); if let Some(dom) = decl.dom.as_ref().map(|ob| Elaborator.elab(ob)).transpose()? { model.set_dom(decl.id.into(), dom); @@ -86,11 +105,38 @@ impl DblModelDiagram { if let Some(cod) = decl.cod.as_ref().map(|ob| Elaborator.elab(ob)).transpose()? { model.set_cod(decl.id.into(), cod); } - if let Some(over) = decl.over.as_ref().map(|mor| Elaborator.elab(mor)).transpose()? { + if let Some(over) = + decl.over.as_ref().map(|mor| Elaborator.elab(mor)).transpose()? + { mapping.assign_mor(decl.id.into(), over); } } - }); + DblModelDiagramBox::Modal(diagram) => { + let (mapping, model) = diagram.into(); + let mor_type: catlog::one::ShortPath< + catlog::dbl::modal::ModeApp, + _, + > = Elaborator.elab(&decl.mor_type)?; + model.make_mor(decl.id.into(), mor_type.clone()); + if let Some(dom) = decl.dom.as_ref().map(|ob| Elaborator.elab(ob)).transpose()? { + model.set_dom(decl.id.into(), dom); + } + if let Some(cod) = decl.cod.as_ref().map(|ob| Elaborator.elab(ob)).transpose()? { + if !model.has_ob(&cod) { + let ob_type = model.theory().tgt_type(&mor_type); + if let Some(name) = cod.clone().generator() { + model.add_ob(name, ob_type); + } + } + model.set_cod(decl.id.into(), cod); + } + if let Some(over) = + decl.over.as_ref().map(|mor| Elaborator.elab(mor)).transpose()? + { + mapping.assign_mor(decl.id.into(), over); + } + } + }; if decl.name.is_empty() { Ok(()) } else { @@ -106,7 +152,7 @@ impl DblModelDiagram { #[wasm_bindgen(js_name = "obType")] pub fn ob_type(&self, ob: Ob) -> Result { all_the_same!(match &self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { + DblModelDiagramBox::[Discrete, Modal](diagram) => { let (_, model) = diagram.into(); Ok(Quoter.quote(&model.ob_type(&Elaborator.elab(&ob)?))) } @@ -117,7 +163,7 @@ impl DblModelDiagram { #[wasm_bindgen(js_name = "morType")] pub fn mor_type(&self, mor: Mor) -> Result { all_the_same!(match &self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { + DblModelDiagramBox::[Discrete, Modal](diagram) => { let (_, model) = diagram.into(); Ok(Quoter.quote(&model.mor_type(&Elaborator.elab(&mor)?))) } @@ -128,7 +174,7 @@ impl DblModelDiagram { #[wasm_bindgen(js_name = "obGenerators")] pub fn ob_generators(&self) -> Vec { all_the_same!(match &self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { + DblModelDiagramBox::[Discrete, Modal](diagram) => { let (_, model) = diagram.into(); model.ob_generators().collect() } @@ -139,7 +185,7 @@ impl DblModelDiagram { #[wasm_bindgen(js_name = "morGenerators")] pub fn mor_generators(&self) -> Vec { all_the_same!(match &self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { + DblModelDiagramBox::[Discrete, Modal](diagram) => { let (_, model) = diagram.into(); model.mor_generators().collect() } @@ -150,7 +196,7 @@ impl DblModelDiagram { #[wasm_bindgen(js_name = "obGeneratorsWithType")] pub fn ob_generators_with_type(&self, ob_type: ObType) -> Result, String> { all_the_same!(match &self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { + DblModelDiagramBox::[Discrete, Modal](diagram) => { let (_, model) = diagram.into(); let ob_type = Elaborator.elab(&ob_type)?; Ok(model.ob_generators_with_type(&ob_type).collect()) @@ -165,7 +211,7 @@ impl DblModelDiagram { mor_type: MorType, ) -> Result, String> { all_the_same!(match &self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { + DblModelDiagramBox::[Discrete, Modal](diagram) => { let (_, model) = diagram.into(); let mor_type = Elaborator.elab(&mor_type)?; Ok(model.mor_generators_with_type(&mor_type).collect()) @@ -190,10 +236,10 @@ impl DblModelDiagram { pub fn ob_presentation(&self, id: QualifiedName) -> Option { let label = self.ob_generator_label(&id); let (ob_type, over) = all_the_same!(match &self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { + DblModelDiagramBox::[Discrete, Modal](diagram) => { let (mapping, model) = diagram.into(); (Quoter.quote(&model.ob_generator_type(&id)), - Quoter.quote(mapping.0.ob_generator_map.get(&id)?)) + Quoter.quote(mapping.ob_generator_map().get(&id)?)) } }); Some(DiagramObGenerator { id, label, ob_type, over }) @@ -203,10 +249,10 @@ impl DblModelDiagram { #[wasm_bindgen(js_name = "morPresentation")] pub fn mor_presentation(&self, id: QualifiedName) -> Option { let (mor_type, over, dom, cod) = all_the_same!(match &self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { + DblModelDiagramBox::[Discrete, Modal](diagram) => { let (mapping, model) = diagram.into(); (Quoter.quote(&model.mor_generator_type(&id)), - Quoter.quote(mapping.0.mor_generator_map.get(&id)?), + Quoter.quote(mapping.mor_generator_map().get(&id)?), Quoter.quote(model.get_dom(&id)?), Quoter.quote(model.get_cod(&id)?)) } @@ -218,7 +264,7 @@ impl DblModelDiagram { #[wasm_bindgen] pub fn presentation(&self) -> ModelDiagramPresentation { all_the_same!(match &self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { + DblModelDiagramBox::[Discrete, Modal](diagram) => { let (_, model) = diagram.into(); ModelDiagramPresentation { ob_generators: { @@ -236,7 +282,7 @@ impl DblModelDiagram { #[wasm_bindgen(js_name = "inferMissingFrom")] pub fn infer_missing_from(&mut self, model: &DblModel) -> Result<(), String> { all_the_same!(match &mut self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { + DblModelDiagramBox::[Discrete, Modal](diagram) => { let model: &Rc<_> = (&model.model).try_into().map_err( |_| "Type of model should match type of diagram")?; diagram.infer_missing_from(model); @@ -262,7 +308,7 @@ impl DblModelDiagram { #[wasm_bindgen(js_name = "validateIn")] pub fn validate_in(&self, model: &DblModel) -> Result { let result = all_the_same!(match &self.diagram { - DblModelDiagramBox::[Discrete](diagram) => { + DblModelDiagramBox::[Discrete, Modal](diagram) => { let model: &Rc<_> = (&model.model).try_into().map_err( |_| "Type of model should match type of diagram")?; diagram.validate_in(model) @@ -303,7 +349,7 @@ mod tests { use uuid::Uuid; use super::*; - use crate::model::tests::sch_walking_attr; + use crate::model::tests::{dec_heat_eq, dec_wedge, sch_walking_attr}; use crate::theories::*; #[test] @@ -359,4 +405,186 @@ mod tests { assert_eq!(presentation.ob_generators.len(), 3); assert_eq!(presentation.mor_generators.len(), 2); } + + #[test] + fn diagram_dec_heat_eq() { + let th = ThDEC::new().theory(); + let [form0, op1dot, op1laplace] = [Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()]; + let _model = dec_heat_eq(&th, [form0, op1dot, op1laplace]); + + let mut diagram = DblModelDiagram::new(&th); + let [u, udot, dot, lapl] = [Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()]; + + assert!( + diagram + .add_ob(&DiagramObDecl { + name: "u".into(), + id: u, + ob_type: ObType::Basic("Form0".into()), + over: Some(Ob::Basic(form0.to_string())) + }) + .is_ok() + ); + + assert!( + diagram + .add_ob(&DiagramObDecl { + name: "udot".into(), + id: udot, + ob_type: ObType::Basic("Form0".into()), + over: Some(Ob::Basic(form0.to_string())) + }) + .is_ok() + ); + + assert!( + diagram + .add_mor(&DiagramMorDecl { + name: "".into(), + id: dot, + mor_type: MorType::Basic("Form0".into()), + dom: Some(Ob::List { + modality: Modality::List, + objects: vec![Some(Ob::Basic(u.to_string()))] + }), + cod: Some(Ob::Basic(udot.to_string())), + over: Some(Mor::Basic(op1dot.to_string())), + }) + .is_ok() + ); + + assert!( + diagram + .add_mor(&DiagramMorDecl { + name: "".into(), + id: lapl, + mor_type: MorType::Basic("Form0".into()), + dom: Some(Ob::List { + modality: Modality::List, + objects: vec![Some(Ob::Basic(u.to_string()))] + }), + cod: Some(Ob::Basic(udot.to_string())), + over: Some(Mor::Basic(op1laplace.to_string())), + }) + .is_ok() + ); + } + + #[test] + fn diagram_dec() { + let th = ThDEC::new().theory(); + let [form0, form1, op1d, op2wedge] = + [Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()]; + let _model = dec_wedge(&th, [form0, form1, op1d, op2wedge]); + + let mut diagram = DblModelDiagram::new(&th); + let [u0, v0, v1, _d, wedge01, wedge00, wedge00result, result] = [ + Uuid::now_v7(), + Uuid::now_v7(), + Uuid::now_v7(), + Uuid::now_v7(), + Uuid::now_v7(), + Uuid::now_v7(), + Uuid::now_v7(), + Uuid::now_v7(), + ]; + + assert!( + diagram + .add_ob(&DiagramObDecl { + name: "u".into(), + id: u0, + ob_type: ObType::Basic("Form0".into()), + over: Some(Ob::Basic(form0.to_string())), + }) + .is_ok() + ); + + assert!( + diagram + .add_ob(&DiagramObDecl { + name: "v0".into(), + id: v0, + ob_type: ObType::Basic("Form0".into()), + over: Some(Ob::Basic(form0.to_string())), + }) + .is_ok() + ); + + assert!( + diagram + .add_ob(&DiagramObDecl { + name: "v1".into(), + id: v0, + ob_type: ObType::Basic("Form1".into()), + over: Some(Ob::Basic(form1.to_string())), + }) + .is_ok() + ); + + assert!( + diagram + .add_ob(&DiagramObDecl { + name: "result".into(), + id: result, + ob_type: ObType::Basic("Form1".into()), + over: Some(Ob::Basic(form1.to_string())), + }) + .is_ok() + ); + + assert!( + diagram + .add_mor(&DiagramMorDecl { + name: "".into(), + id: op1d, + mor_type: MorType::Basic("Multihom".into()), + dom: Some(Ob::List { + modality: Modality::List, + objects: vec![Some(Ob::Basic(form0.to_string()))] + }), + cod: Some(Ob::Basic(result.to_string())), + over: Some(Mor::Basic(op1d.to_string())), + }) + .is_ok() + ); + + assert!( + diagram + .add_mor(&DiagramMorDecl { + name: "".into(), + id: wedge00, + mor_type: MorType::Basic("Multihom".into()), + dom: Some(Ob::List { + modality: Modality::List, + objects: vec![ + Some(Ob::Basic(u0.to_string())), + Some(Ob::Basic(u0.to_string())) + ] + }), + cod: Some(Ob::Basic(wedge00result.to_string())), + over: Some(Mor::Basic(op2wedge.to_string())), + }) + .is_ok() + ); + + assert!( + diagram + .add_mor(&DiagramMorDecl { + name: "".into(), + id: wedge01, + mor_type: MorType::Basic("Multihom".into()), + dom: Some(Ob::List { + modality: Modality::List, + objects: vec![ + Some(Ob::Basic(wedge00result.to_string())), + Some(Ob::Basic(v1.to_string())) + ] + }), + cod: Some(Ob::Basic(result.to_string())), + over: Some(Mor::Basic(op2wedge.to_string())), + }) + .is_ok() + ); + } } diff --git a/packages/catlog-wasm/src/theories.rs b/packages/catlog-wasm/src/theories.rs index f01b6c7a1..72386e4f7 100644 --- a/packages/catlog-wasm/src/theories.rs +++ b/packages/catlog-wasm/src/theories.rs @@ -534,6 +534,23 @@ impl ThPowerSystem { } } +/// A theory of the DEC +#[wasm_bindgen] +pub struct ThDEC(Rc>); + +#[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::*; diff --git a/packages/catlog/src/dbl/discrete/model_morphism.rs b/packages/catlog/src/dbl/discrete/model_morphism.rs index eabd0e906..d064358fd 100644 --- a/packages/catlog/src/dbl/discrete/model_morphism.rs +++ b/packages/catlog/src/dbl/discrete/model_morphism.rs @@ -24,8 +24,23 @@ type DiscreteDblModelMappingData = FpFunctorData< >; impl DiscreteDblModelMapping { + /// Returns object generators. + pub fn ob_generator_map(&self) -> HashColumn { + self.0.ob_generator_map.clone() + } + + /// Returns morphism generators. + pub fn mor_generator_map(&self) -> HashColumn { + self.0.mor_generator_map.clone() + } +} + +impl MutDblModelMapping for DiscreteDblModelMapping { + type ObGen = QualifiedName; + type MorGen = QualifiedPath; + /// Constructs a model mapping from a pair of hash maps. - pub fn new( + fn new( ob_pairs: impl IntoIterator, mor_pairs: impl IntoIterator, ) -> Self { @@ -36,25 +51,27 @@ impl DiscreteDblModelMapping { } /// Assigns an object generator, returning the previous assignment. - pub fn assign_ob(&mut self, x: QualifiedName, y: QualifiedName) -> Option { + fn assign_ob(&mut self, x: QualifiedName, y: QualifiedName) -> Option { self.0.ob_generator_map.set(x, y) } /// Assigns a morphism generator, returning the previous assignment. - pub fn assign_mor(&mut self, e: QualifiedName, n: QualifiedPath) -> Option { + fn assign_mor(&mut self, e: QualifiedName, n: QualifiedPath) -> Option { self.0.mor_generator_map.set(e, n) } /// Unassigns an object generator, returning the previous assignment. - pub fn unassign_ob(&mut self, x: &QualifiedName) -> Option { + fn unassign_ob(&mut self, x: &QualifiedName) -> Option { self.0.ob_generator_map.unset(x) } /// Unassigns a morphism generator, returning the previous assignment. - pub fn unassign_mor(&mut self, e: &QualifiedName) -> Option { + fn unassign_mor(&mut self, e: &QualifiedName) -> Option { self.0.mor_generator_map.unset(e) } +} +impl DiscreteDblModelMapping { /// Interprets the data as a functor into the given model. pub fn functor_into<'a>( &'a self, @@ -72,13 +89,6 @@ impl DiscreteDblModelMapping { } } -/// A functor between models of a double theory. -/// -/// This struct borrows its data to perform validation. The domain and codomain are -/// assumed to be valid models of double theories. If that is in question, the -/// models should be validated *before* validating this object. -pub struct DblModelMorphism<'a, Map, Dom, Cod>(pub &'a Map, pub &'a Dom, pub &'a Cod); - /// A morphism between models of a discrete double theory. pub type DiscreteDblModelMorphism<'a> = DblModelMorphism<'a, DiscreteDblModelMapping, DiscreteDblModel, DiscreteDblModel>; diff --git a/packages/catlog/src/dbl/modal/mod.rs b/packages/catlog/src/dbl/modal/mod.rs index fe527ba76..a45ae3fac 100644 --- a/packages/catlog/src/dbl/modal/mod.rs +++ b/packages/catlog/src/dbl/modal/mod.rs @@ -1,7 +1,11 @@ //! Doctrine of modal double theories. pub mod model; +pub mod model_diagram; +pub mod model_morphism; pub mod theory; pub use model::*; +pub use model_diagram::*; +pub use model_morphism::*; pub use theory::*; diff --git a/packages/catlog/src/dbl/modal/model.rs b/packages/catlog/src/dbl/modal/model.rs index 11f3c9363..acc4dbab7 100644 --- a/packages/catlog/src/dbl/modal/model.rs +++ b/packages/catlog/src/dbl/modal/model.rs @@ -11,7 +11,7 @@ use ref_cast::RefCast; use super::theory::*; use crate::dbl::theory::DblTheoryKind; -use crate::dbl::{graph::VDblGraph, model::*, theory::DblTheory}; +use crate::dbl::{category::VDblCategory, graph::VDblGraph, model::*, theory::DblTheory}; use crate::tt::util::pretty::*; use crate::validate::{self, Validate}; use crate::{one::computad::*, one::*, zero::*}; @@ -100,6 +100,30 @@ impl ModalDblModel { fn computad(&self) -> Computad<'_, ModalOb, ModalDblModelObs, QualifiedName> { Computad::new(ModalDblModelObs::ref_cast(self), &self.mor_generators) } + + /// Infers missing data in the model, where possible. + /// + /// Objects used in the domain or codomain of morphisms, but not contained as + /// objects of the model, are added and their types are inferred. It is not + /// always possible to do this consistently, so it is important to `validate` + /// the model even after calling this method. + pub fn infer_missing(&mut self) { + let edges: Vec<_> = self.mor_generators().collect(); + for e in edges { + if let Some(x) = self.get_dom(&e).filter(|x| !self.has_ob(x)) { + let ob_type = self.theory.src(&self.mor_generator_type(&e)); + if let Some(id) = x.clone().generator() { + self.add_ob(id.clone(), ob_type) + }; + } + if let Some(x) = self.get_cod(&e).filter(|x| !self.has_ob(x)) { + let ob_type = self.theory.tgt(&self.mor_generator_type(&e)); + if let Some(id) = x.clone().generator() { + self.add_ob(id.clone(), ob_type) + }; + } + } + } } #[derive(RefCast)] @@ -410,6 +434,13 @@ impl ModalDblModel { _ => false, } } + + // TODO + /// Iterates over failures of model to be well defined. + pub fn iter_invalid(&self) -> impl Iterator + '_ { + // type Invalid = InvalidDblModel; + vec![].into_iter() + } } impl ModalObOp { diff --git a/packages/catlog/src/dbl/modal/model_diagram.rs b/packages/catlog/src/dbl/modal/model_diagram.rs new file mode 100644 index 000000000..8e5ddb7c7 --- /dev/null +++ b/packages/catlog/src/dbl/modal/model_diagram.rs @@ -0,0 +1,181 @@ +//! Diagrams in models of a modal double theory. + +#[cfg(feature = "serde-wasm")] +use tsify::declare; + +use crate::dbl::{ + modal::ModalDblModelMapping, + model::{InvalidDblModel, ModalDblModel, MutDblModel}, + model_diagram::*, + model_morphism::{DblModelMorphism, InvalidDblModelMorphism}, + theory::DblTheoryKind, +}; +use crate::one::{ + category::{Category, FgCategory}, + graph::GraphMapping, +}; +use crate::validate; +use crate::zero::{QualifiedName, column::Mapping}; + +use itertools::Either; +use nonempty::NonEmpty; + +/// A diagram is a model of a modal double theoruy. +pub type ModalDblModelDiagram = DblModelDiagram>; + +/// A failure to be valid in a diagram in a model of a discrete double theory. +#[cfg_attr(feature = "serde-wasm", declare)] +pub type InvalidModalDblModelDiagram = + InvalidDblModelDiagram>; + +impl ModalDblModelDiagram { + /// Validates that the diagram is well-defined in the given model. + /// + /// Assumes that the model is valid. If it is not, this function may panic. + pub fn validate_in( + &self, + model: &ModalDblModel, + ) -> Result<(), NonEmpty> { + validate::wrap_errors(self.iter_invalid_in(model)) + } + + /// Iterates over failures of the diagram to be valid in the given model. + pub fn iter_invalid_in<'a>( + &'a self, + model: &'a ModalDblModel, + ) -> impl Iterator + 'a { + let mut dom_errs = self.1.iter_invalid().peekable(); + if dom_errs.peek().is_some() { + Either::Left(dom_errs.map(InvalidDblModelDiagram::Dom)) + } else { + let morphism = DblModelMorphism(&self.0, &self.1, model); + Either::Right(morphism.iter_invalid().map(InvalidDblModelDiagram::Map)) + } + } + + /// Infer missing data in the diagram from the model, where possible. + /// + /// Assumes that the model is valid. + pub fn infer_missing_from(&mut self, model: &ModalDblModel) { + let (mapping, domain) = self.into(); + domain.infer_missing(); + for e in domain.mor_generators() { + let Some(g) = mapping.edge_map().apply_to_ref(&e) else { + continue; + }; + if !model.has_mor(&g) { + continue; + } + + mapping.infer_missing(domain.clone().get_dom(&e), model.dom(&g)); + mapping.infer_missing(domain.clone().get_cod(&e), model.cod(&g)); + } + } +} + +#[cfg(test)] +mod tests { + use super::*; + use crate::dbl::model_diagram::DblModelDiagram; + use crate::dbl::model_morphism::MutDblModelMapping; + use crate::stdlib::dec; + use crate::stdlib::th_multicategory; + use crate::tt::modelgen::Model; + use crate::validate; + use crate::zero::name; + use std::rc::Rc; + + #[test] + fn validate_modal_model_diagram() { + let th = Rc::new(th_multicategory()); + let dec = dec(th.clone()); + // TODO does not like numbers + let heat_eq = Model::from_text( + &th.into(), + "[ + u : Object, + dot_u : Object, + k : Object, + anon : Object, + partial_t : Multihom[[u], dot_u], + laplacian : Multihom[[u], anon], + multiplication : Multihom[[k, anon], dot_u] + ]", + ); + let heat_eq = heat_eq.unwrap().as_modal().unwrap(); + + let mut f: ModalDblModelMapping = Default::default(); + f.assign_ob(name("u"), name("Form0").into()); + f.assign_ob(name("dot_u"), name("Form0").into()); + f.assign_ob(name("k"), name("Form0").into()); + f.assign_ob(name("anon"), name("Form0").into()); + f.assign_mor(name("laplacian"), name("laplacian").into()); + f.assign_mor(name("partial_t"), name("partial_t0").into()); + f.assign_mor(name("multiplication"), name("multiplication").into()); + + let diagram = DblModelDiagram(f, heat_eq); + assert!(diagram.validate_in(&dec).is_ok()); + } + + #[test] + fn validate_bad_modal_model_diagram() { + let th = Rc::new(th_multicategory()); + let dec = dec(th.clone()); + // TODO does not like numbers + let heat_eq = Model::from_text( + &th.into(), + "[ + u : Object, + dot_u : Object, + k : Object, + anon : Object, + partial_t : Multihom[[u], dot_u], + laplacian : Multihom[[u], anon], + multiplication : Multihom[[k, anon], dot_u] + ]", + ); + let heat_eq = heat_eq.unwrap().as_modal().unwrap(); + + let mut f: ModalDblModelMapping = Default::default(); + f.assign_ob(name("u"), name("Form0").into()); + f.assign_ob(name("dot_u"), name("Form0").into()); + f.assign_ob(name("k"), name("Form1").into()); // this is intentionally wrong. + f.assign_ob(name("anon"), name("Form0").into()); + f.assign_mor(name("laplacian"), name("laplacian").into()); + f.assign_mor(name("partial_t"), name("partial_t0").into()); + f.assign_mor(name("multiplication"), name("multiplication").into()); + + let diagram = DblModelDiagram(f, heat_eq); + let err = validate::wrap_errors( + vec![InvalidDblModelDiagram::Map(InvalidDblModelMorphism::Dom(name( + "multiplication", + )))] + .into_iter(), + ); + assert_eq!(diagram.validate_in(&dec), err); + } + + #[test] + fn infer_modal_model_diagram() { + let th = Rc::new(th_multicategory()); + let domain = Model::from_text( + &th.clone().into(), + "[ + u : Object, + dot_u : Object, + partial_t : Multihom[[u], dot_u] + ]", + ) + .unwrap() + .as_modal() + .unwrap(); + + let mut f: ModalDblModelMapping = Default::default(); + f.assign_mor(name("partial_t"), name("partial_t0").into()); + let mut diagram = DblModelDiagram(f, domain.clone()); + + let dec = dec(th.clone()); + diagram.infer_missing_from(&dec); + assert!(diagram.validate_in(&dec).is_ok()); + } +} diff --git a/packages/catlog/src/dbl/modal/model_morphism.rs b/packages/catlog/src/dbl/modal/model_morphism.rs new file mode 100644 index 000000000..6f08b74ae --- /dev/null +++ b/packages/catlog/src/dbl/modal/model_morphism.rs @@ -0,0 +1,232 @@ +//! Morphism between models of a modal double theory. + +use crate::dbl::modal::{ModalDblModel, ModalMor, ModalOb}; +use crate::dbl::model::MutDblModel; +use crate::dbl::model_morphism::{DblModelMorphism, InvalidDblModelMorphism, MutDblModelMapping}; +use crate::dbl::theory::DblTheoryKind; +use crate::one::{ + category::{Category, FgCategory}, + graph::GraphMapping, +}; +use crate::validate::{self, Validate}; +use crate::zero::{HashColumn, Mapping, MutMapping, QualifiedName}; + +use nonempty::NonEmpty; + +/// A mapping between models of a modal double theory. +#[derive(Clone, Debug, Default, PartialEq, Eq)] +pub struct ModalDblModelMapping( + pub HashColumn, + pub HashColumn, +); + +impl ModalDblModelMapping { + /// Returns object generators. + pub fn ob_generator_map(&self) -> HashColumn { + self.0.clone() + } + + /// Returns morphism generators. + pub fn mor_generator_map(&self) -> HashColumn { + self.1.clone() + } +} + +impl MutDblModelMapping for ModalDblModelMapping { + type ObGen = ModalOb; + type MorGen = ModalMor; + /// Constructs a new model mapping from a pair of hash maps. + fn new( + ob_pairs: impl IntoIterator, + mor_pairs: impl IntoIterator, + ) -> Self { + Self(ob_pairs.into_iter().collect(), mor_pairs.into_iter().collect()) + } + + /// Assigns an object generator, returning the previous assignment. + fn assign_ob(&mut self, x: QualifiedName, y: ModalOb) -> Option { + self.0.set(x, y) + } + + /// Assigns a morphism generator, returning the previous assignment. + fn assign_mor(&mut self, e: QualifiedName, n: ModalMor) -> Option { + self.1.set(e, n) + } + + /// Unassigns an object generator, returning the previous assignment. + fn unassign_ob(&mut self, x: &QualifiedName) -> Option { + self.0.unset(x) + } + + /// Unassigns a morphism generator, returning the previous assignment. + fn unassign_mor(&mut self, e: &QualifiedName) -> Option { + self.1.unset(e) + } +} + +impl GraphMapping for ModalDblModelMapping +where + HashColumn: Mapping, + HashColumn: Mapping, +{ + type DomV = QualifiedName; + type DomE = QualifiedName; + type CodV = ModalOb; + type CodE = ModalMor; + type VertexMap = HashColumn; + type EdgeMap = HashColumn; + + fn vertex_map(&self) -> &Self::VertexMap { + &self.0 + } + fn edge_map(&self) -> &Self::EdgeMap { + &self.1 + } +} + +impl ModalDblModelMapping { + /// This checks if an object in the domain also exists in the model. + pub fn infer_missing(&mut self, domain_ob: Option<&ModalOb>, model_ob: ModalOb) { + if let Some(ob) = domain_ob { + let names: Vec = match ob { + ModalOb::Generator(name) => vec![name.clone()], + ModalOb::App(_, name) => vec![name.clone()], + ModalOb::List(_, args) => { + args.iter().filter_map(|ob| ob.clone().generator()).collect() + } + }; + + for name in names { + if !self.is_vertex_assigned(&name) { + match model_ob { + ref ob @ ModalOb::Generator(_) => self.assign_ob(name, ob.clone()), + ref ob @ ModalOb::App(_, _) => self.assign_ob(name, ob.clone()), + ModalOb::List(_, ref args) => match args.as_slice() { + [only] => self.assign_ob(name, only.clone()), + _ => todo!("What happens when we receive more than one arg?"), + }, + }; + }; + } + }; + } + + /// This applies a mapping onto a given object in the domain, returning the corresponding + /// object in the codomain. + fn apply_ob(&self, ob: ModalOb) -> Result { + match ob { + ModalOb::Generator(name) => { + self.apply_vertex(name.clone()).ok_or("Vertex {name} not found".to_string()) + } + ModalOb::App(_, name) => { + self.apply_vertex(name.clone()).ok_or("Vertex {name} not found".to_string()) + } + ModalOb::List(list, args) => args + .into_iter() + .map(|name| self.apply_ob(name.clone())) + .collect::, String>>() + .map(|args| ModalOb::List(list, args)), + } + } +} + +/// A morphism between models of a modal double theory. +pub type ModalDblModelMorphism<'a, Kind> = + DblModelMorphism<'a, ModalDblModelMapping, ModalDblModel, ModalDblModel>; + +impl<'a, Kind: DblTheoryKind> ModalDblModelMorphism<'a, Kind> { + /// Iterates over failures of the mapping to be a model morphism. + pub fn iter_invalid( + &self, + ) -> impl Iterator> + 'a + use<'a, Kind> + { + let DblModelMorphism(mapping, dom, cod) = *self; + + let ob_errors = dom.ob_generators().filter_map(|v| { + if mapping.vertex_map().apply_to_ref(&v).is_some_and(|w| cod.has_ob(&w)) { + None + } else { + Some(InvalidDblModelMorphism::::Ob(v)) + } + }); + + let mor_errors = dom.mor_generators().filter_map(|e| { + // Check if the morphism is correct. + let f = match mapping.edge_map().apply_to_ref(&e) { + Some(ModalMor::Generator(f)) if cod.has_mor(&ModalMor::Generator(f.clone())) => f, + Some(ModalMor::Generator(f)) => return Some(InvalidDblModelMorphism::Mor(f)), + _ => return None, + }; + + let dom_check = dom.get_dom(&e).zip(cod.get_dom(&f)).and_then(|(left, right)| { + (mapping.apply_ob(left.clone()) != Ok(right.clone())) + .then_some(InvalidDblModelMorphism::Dom(e.clone())) + }); + + let cod_check = dom.get_cod(&e).zip(cod.get_cod(&f)).and_then(|(left, right)| { + (mapping.apply_ob(left.clone()) != Ok(right.clone())) + .then_some(InvalidDblModelMorphism::Cod(e)) + }); + + // we're short-circuiting errors here. i'd like to collect them into one error message + // in the future + dom_check.or(cod_check) + }); + + ob_errors.chain(mor_errors) + } +} + +impl Validate for ModalDblModelMorphism<'_, Kind> { + type ValidationError = InvalidDblModelMorphism; + + fn validate(&self) -> Result<(), NonEmpty> { + validate::wrap_errors(self.iter_invalid()) + } +} + +#[cfg(test)] +mod tests { + use std::rc::Rc; + + use super::*; + use crate::stdlib::*; + use crate::tt::modelgen::Model; + use crate::zero::name; + + #[test] + fn validate_bad_modal_model_mapping() { + let th = Rc::new(th_multicategory()); + let dec = dec(th.clone()); + // TODO does not like numbers + let heat_eq = Model::from_text( + &th.into(), + "[ + u : Object, + dot_u : Object, + k : Object, + anon : Object, + partial_t : Multihom[[u], dot_u], + laplacian : Multihom[[u], anon], + multiplication : Multihom[[k, anon], dot_u] + ]", + ); + let heat_eq = heat_eq.unwrap().as_modal().unwrap(); + + let mut f: ModalDblModelMapping = Default::default(); + f.assign_ob(name("u"), name("Form0").into()); + f.assign_ob(name("dot_u"), name("Form0").into()); + f.assign_ob(name("k"), name("Form1").into()); // this is intentionally wrong. + f.assign_ob(name("anon"), name("Form0").into()); + f.assign_mor(name("laplacian"), name("laplacian").into()); + f.assign_mor(name("partial_t"), name("partial_t0").into()); + f.assign_mor(name("multiplication"), name("multiplication").into()); + + let d = DblModelMorphism(&f, &heat_eq, &dec); + + let err = validate::wrap_errors( + vec![(InvalidDblModelMorphism::Dom(name("multiplication")))].into_iter(), + ); + assert_eq!(d.validate(), err); + } +} diff --git a/packages/catlog/src/dbl/model_morphism.rs b/packages/catlog/src/dbl/model_morphism.rs index 3102bf82f..d10789fe5 100644 --- a/packages/catlog/src/dbl/model_morphism.rs +++ b/packages/catlog/src/dbl/model_morphism.rs @@ -21,6 +21,8 @@ use thiserror::Error; +use crate::zero::QualifiedName; + #[cfg(feature = "serde")] use serde::{Deserialize, Serialize}; #[cfg(feature = "serde-wasm")] @@ -28,6 +30,39 @@ use tsify::Tsify; pub use super::discrete::model_morphism::*; +/// A functor between models of a double theory. +/// +/// This struct borrows its data to perform validation. The domain and codomain are +/// assumed to be valid models of double theories. If that is in question, the +/// models should be validated *before* validating this object. +pub struct DblModelMorphism<'a, Map, Dom, Cod>(pub &'a Map, pub &'a Dom, pub &'a Cod); + +/// Trait for mutating morphisms between double models. +pub trait MutDblModelMapping { + /// Object generators for the DblModelMapping. + type ObGen; + /// Morphism generators for the DblModelMapping. + type MorGen; + + /// Constructs a model mapping from a pair of hash maps. + fn new( + ob_pairs: impl IntoIterator, + mor_pairs: impl IntoIterator, + ) -> Self; + + /// Assigns an object generator, returning the previous assignment. + fn assign_ob(&mut self, x: QualifiedName, y: Self::ObGen) -> Option; + + /// Assigns a morphism generator, returning the previous assignment. + fn assign_mor(&mut self, e: QualifiedName, n: Self::MorGen) -> Option; + + /// Unassigns an object generator, returning the previous assignment. + fn unassign_ob(&mut self, x: &QualifiedName) -> Option; + + /// Unassigns a morphism generator, returning the previous assignment. + fn unassign_mor(&mut self, e: &QualifiedName) -> Option; +} + /// An invalid assignment in a morphism between models of a double theory. #[derive(Clone, Debug, Error, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] diff --git a/packages/catlog/src/stdlib/models.rs b/packages/catlog/src/stdlib/models.rs index 6965d47f9..26f3c20dc 100644 --- a/packages/catlog/src/stdlib/models.rs +++ b/packages/catlog/src/stdlib/models.rs @@ -235,6 +235,80 @@ pub fn lotka_volterra_dynamics(th: Rc>) -> ModalDblMod model } +/// The forms and operations of the two-dimensional Discrete Exterior Calculus viewed as a model of +/// a modal double theory. +pub fn dec(th: Rc>) -> ModalDblModel { + let ob_type = ModalObType::new(name("Object")); + let mut model = ModalDblModel::new(th); + let forms = vec![name("Form0"), name("Form1"), name("Form2")]; + for form in forms.clone() { + model.add_ob(form, ob_type.clone()); + } + + model.add_mor( + name("laplacian"), + ModalOb::List(List::Plain, vec![ModalOb::Generator(forms[0].clone())]), + ModalOb::Generator(forms[0].clone()), + ModalMorType::Zero(ob_type.clone()), + ); + + let dualforms = vec![name("DualForm0"), name("DualForm1"), name("DualForm2")]; + for form in dualforms.clone() { + model.add_ob(form, ob_type.clone()); + } + + for (dim, form) in forms.clone().into_iter().enumerate() { + model.add_mor( + name(format!("partial_t{dim}").as_str()), + ModalOb::List(List::Plain, vec![ModalOb::Generator(form.clone())]), + ModalOb::Generator(form.clone()), + ModalMorType::Zero(ob_type.clone()), + ); + model.add_mor( + name(format!("hodge_{dim}").as_str()), + ModalOb::List(List::Plain, vec![ModalOb::Generator(form.clone())]), + ModalOb::Generator(dualforms[3 - dim - 1].clone()), + ModalMorType::Zero(ob_type.clone()), + ); + + if dim >= 2 { + continue; + } + + model.add_mor( + name(format!("d_{dim}").as_str()), + ModalOb::List(List::Plain, vec![ModalOb::Generator(form.clone())]), + ModalOb::Generator(forms[dim + 1].clone()), + ModalMorType::Zero(ob_type.clone()), + ); + } + + let mor_type: ModalMorType = ModeApp::new(name("Multihom")).into(); + + model.add_mor( + name("multiplication"), + ModalOb::List(List::Plain, vec![forms[0].clone().into(), forms[0].clone().into()]), + ModalOb::Generator(forms[0].clone()), + mor_type.clone(), + ); + + for (i, form1) in forms.iter().enumerate() { + for (j, form2) in forms.iter().enumerate() { + if (i >= j) || (i + j > 2) { + continue; + } + model.add_mor( + name(format!("wedge_{}", i + j).as_str()), + ModalOb::List(List::Plain, vec![form1.clone().into(), form2.clone().into()]), + forms[i + j].clone().into(), + mor_type.clone(), + ); + } + } + + model +} + #[cfg(test)] mod tests { use super::super::theories::*; diff --git a/packages/frontend/src/components/id_input.tsx b/packages/frontend/src/components/id_input.tsx index 5ffb66c0d..dfa597e16 100644 --- a/packages/frontend/src/components/id_input.tsx +++ b/packages/frontend/src/components/id_input.tsx @@ -126,7 +126,13 @@ 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 setNewId = () => props.generateId && props.setId(props.generateId()); const labelType = (id: Uuid | null): "named" | "anonymous" | "undefined" => { if (id == null) { diff --git a/packages/frontend/src/diagram/morphism_cell_editor.tsx b/packages/frontend/src/diagram/morphism_cell_editor.tsx index bd698c0d3..1ec34efad 100644 --- a/packages/frontend/src/diagram/morphism_cell_editor.tsx +++ b/packages/frontend/src/diagram/morphism_cell_editor.tsx @@ -1,6 +1,5 @@ import { useContext } from "solid-js"; import invariant from "tiny-invariant"; -import { v7 } from "uuid"; import { type FocusHandle, useChildFocus } from "catcolab-ui-components"; import type { DiagramMorDecl } from "catlog-wasm"; @@ -8,7 +7,7 @@ import { BasicMorInput } from "../model/morphism_input"; import type { CellActions } from "../notebook"; import type { Theory } from "../theory"; import { LiveDiagramContext } from "./context"; -import { BasicObInput } from "./object_input"; +import { ObInput } from "./object_input"; import arrowStyles from "../stdlib/arrow_styles.module.css"; import "./morphism_cell_editor.css"; @@ -45,7 +44,7 @@ export function DiagramMorphismCellEditor(props: { return (
- { @@ -54,7 +53,6 @@ export function DiagramMorphismCellEditor(props: { }); }} obType={domType()} - generateId={v7} isInvalid={domInvalid()} focus={focus.childFocus("dom")} deleteForward={() => focus.setActiveChild("mor")} @@ -88,7 +86,7 @@ export function DiagramMorphismCellEditor(props: {
- { @@ -97,7 +95,6 @@ export function DiagramMorphismCellEditor(props: { }); }} obType={codType()} - generateId={v7} isInvalid={codInvalid()} focus={focus.childFocus("cod")} deleteBackward={() => focus.setActiveChild("mor")} diff --git a/packages/frontend/src/diagram/object_input.tsx b/packages/frontend/src/diagram/object_input.tsx index aaf9da5d8..9501b476d 100644 --- a/packages/frontend/src/diagram/object_input.tsx +++ b/packages/frontend/src/diagram/object_input.tsx @@ -1,9 +1,99 @@ -import { useContext } from "solid-js"; +import { deepEqual } from "fast-equals"; +import { type Component, splitProps, useContext } from "solid-js"; +import { Dynamic } from "solid-js/web"; import invariant from "tiny-invariant"; -import type { Ob, ObType, QualifiedName } from "catlog-wasm"; +import type { TextInputOptions } from "catcolab-ui-components"; +import type { Ob, ObOp, ObType, QualifiedName } from "catlog-wasm"; import { type IdInputOptions, ObIdInput } from "../components"; import { LiveDiagramContext } from "./context"; +import { ObListEditor } from "./object_list_editor"; + +/** Props passed to any object input component. */ +export type ObInputProps = { + /** Current value of object, if any. */ + ob: Ob | null; + + /** Handler to set a new value of the object. */ + setOb: (ob: Ob | null) => void; + + /** Type of object being edited. */ + obType: ObType; + + /** Placeholder text to show when no object has been chosen. */ + placeholder?: string; + + /** Whether the choice of object is invalid, say by having wrong type. + + This is a stub; we should propagate error messages from the core. + */ + isInvalid?: boolean; +}; + +/** Input an object that already exists in a model. */ +export function ObInput( + allProps: ObInputProps & + TextInputOptions & { + /** Operation to apply to the object afterwards, if any. */ + applyOp?: ObOp; + }, +) { + const [props, otherProps] = splitProps(allProps, ["ob", "setOb", "obType", "applyOp"]); + + const ob = () => { + if (props.applyOp) { + return props.ob?.tag === "App" && deepEqual(props.ob.content.op, props.applyOp) + ? props.ob.content.ob + : null; + } else { + return props.ob; + } + }; + + const setOb = (ob: Ob | null) => { + if (ob && props.applyOp) { + props.setOb({ + tag: "App", + content: { + op: props.applyOp, + ob, + }, + }); + } else { + props.setOb(ob); + } + }; + + return ( + + ); +} + +function obEditorForType(obType: ObType): Component { + if (obType.tag === "Basic") { + return BasicObInput; + } else if (obType.tag === "ModeApp") { + switch (obType.content.modality) { + case "Discrete": + case "Codiscrete": + return obEditorForType(obType.content.obType); + case "List": + case "SymmetricList": + case "CocartesianList": + case "CartesianList": + case "AdditiveList": { + return ObListEditor; + } + } + } + throw new Error(`No editor for object of type: ${obType}`); +} /** Input a basic object in a diagram via its human-readable name. */ diff --git a/packages/frontend/src/diagram/object_list_editor.css b/packages/frontend/src/diagram/object_list_editor.css new file mode 100644 index 000000000..dc7a896ed --- /dev/null +++ b/packages/frontend/src/diagram/object_list_editor.css @@ -0,0 +1,10 @@ +.diagram-object-decl { + display: flex; + flex-direction: row; + gap: 1ex; + align-items: baseline; + + & .is-a:before { + content: ":"; + } +} diff --git a/packages/frontend/src/diagram/object_list_editor.tsx b/packages/frontend/src/diagram/object_list_editor.tsx new file mode 100644 index 000000000..e0e36144b --- /dev/null +++ b/packages/frontend/src/diagram/object_list_editor.tsx @@ -0,0 +1,200 @@ +import { + batch, + createEffect, + createSignal, + Index, + type JSX, + mergeProps, + Show, + untrack, + useContext, +} from "solid-js"; +import invariant from "tiny-invariant"; + +import type { TextInputOptions } from "catcolab-ui-components"; +import type { Ob, QualifiedName } from "catlog-wasm"; +import { ObIdInput } from "../components"; +import { removeProxyAndCopy } from "../util/remove_proxy_and_copy"; +import { LiveDiagramContext } from "./context"; +import type { ObInputProps } from "./object_input"; + +import "./object_list_editor.css"; + +type ObListEditorProps = ObInputProps & + TextInputOptions & { + insertKey?: string; + startDelimiter?: JSX.Element | string; + endDelimiter?: JSX.Element | string; + separator?: (index: number) => JSX.Element | string; + }; + +/** Edits a list of objects of given type. */ +export function ObListEditor(originalProps: ObListEditorProps) { + const props = mergeProps( + { + insertKey: ",", + startDelimiter:
{"["}
, + endDelimiter:
{"]"}
, + separator: () =>
{","}
, + }, + originalProps, + ); + + const liveDiagram = useContext(LiveDiagramContext); + invariant(liveDiagram, "Live model should be provided as context"); + + const [activeIndex, setActiveIndex] = createSignal(0); + + const setObList = (objects: Array) => { + props.setOb({ + tag: "List", + content: { + modality: modeAppType().content.modality, + objects, + }, + }); + }; + + const updateObList = (f: (objects: Array) => void) => { + const objects = removeProxyAndCopy(obList()); + f(objects); + setObList(objects); + }; + + const insertNewOb = (i: number) => { + batch(() => { + updateObList((objects) => { + objects.splice(i, 0, null); + }); + setActiveIndex(i); + }); + }; + + const modeAppType = () => { + if (props.obType.tag !== "ModeApp") { + throw new Error(`Object type should be a list modality, received: ${props.obType}`); + } + return props.obType; + }; + + const obList = (): Array => { + if (!props.ob) { + return []; + } + if (props.ob.tag !== "List") { + throw new Error(`Object should be a list, received: ${props.ob}`); + } + return props.ob.content.objects; + }; + + const completions = (): QualifiedName[] | undefined => + liveDiagram().elaboratedDiagram()?.obGeneratorsWithType(modeAppType().content.obType); + + // Make the default value the empty list, rather than null. + createEffect(() => { + if (!props.ob) { + setObList([]); + } + }); + + // Insert into new object into empty list when focus is gained. + createEffect(() => { + if (props.isActive && untrack(obList).length === 0) { + insertNewOb(0); + } + }); + + return ( +
    { + if (obList().length === 0) { + insertNewOb(0); + props.hasFocused?.(); + evt.preventDefault(); + } + }} + > + {props.startDelimiter} + }> + {(ob, i) => ( +
  • + 0 && props.separator}>{(sep) => sep()(i)} + { + updateObList((objects) => { + objects[i] = ob; + }); + }} + placeholder={props.placeholder} + idToLabel={(id) => + liveDiagram().elaboratedDiagram()?.obGeneratorLabel(id) + } + labelToId={(label) => + liveDiagram().elaboratedDiagram()?.obGeneratorWithLabel(label) + } + completions={completions()} + isActive={props.isActive && activeIndex() === i} + deleteBackward={() => + batch(() => { + updateObList((objects) => { + objects.splice(i, 1); + }); + if (i === 0) { + props.deleteBackward?.(); + } else { + setActiveIndex(i - 1); + } + }) + } + deleteForward={() => { + batch(() => { + updateObList((objects) => { + objects.splice(i, 1); + }); + if (i === 0) { + props.deleteForward?.(); + } + }); + }} + exitBackward={() => props.exitBackward?.()} + exitForward={() => props.exitForward?.()} + exitLeft={() => { + if (i === 0) { + props.exitLeft?.(); + } else { + setActiveIndex(i - 1); + } + }} + exitRight={() => { + if (i === obList().length - 1) { + props.exitRight?.(); + } else { + setActiveIndex(i + 1); + } + }} + interceptKeyDown={(evt) => { + if (evt.key === props.insertKey) { + insertNewOb(i + 1); + return true; + } else if (evt.key === "Home" && !evt.shiftKey) { + // TODO: Should move to beginning of input. + setActiveIndex(0); + } else if (evt.key === "End" && !evt.shiftKey) { + setActiveIndex(obList().length - 1); + } + return false; + }} + hasFocused={() => { + setActiveIndex(i); + props.hasFocused?.(); + }} + /> +
    • + )} +     + {props.endDelimiter} +
+ ); +} diff --git a/packages/frontend/src/stdlib/analyses.tsx b/packages/frontend/src/stdlib/analyses.tsx index 2bb74794c..55a7fcd5a 100644 --- a/packages/frontend/src/stdlib/analyses.tsx +++ b/packages/frontend/src/stdlib/analyses.tsx @@ -49,6 +49,16 @@ export const diagramGraph = ( const DiagramGraph = lazy(() => import("./analyses/diagram_graph")); +export const modalDiagramGraph = ( + options: AnalysisOptions, +): DiagramAnalysisMeta => ({ + ...options, + component: (props) => , + initialContent: GraphLayoutConfig.defaultConfig, +}); + +const ModalDiagramGraph = lazy(() => import("./analyses/modal_diagram_graph")); + export const tabularView = ( options: AnalysisOptions, ): DiagramAnalysisMeta> => ({ @@ -358,7 +368,7 @@ export function renderSQL( help, component: (props) => , initialContent: () => ({ - backend: SQLBackend.PostgresSQL, + backend: SQLBackend.MySQL, filename: "schema.sql", }), }; diff --git a/packages/frontend/src/stdlib/analyses/modal_diagram_graph.tsx b/packages/frontend/src/stdlib/analyses/modal_diagram_graph.tsx new file mode 100644 index 000000000..9b0fcb475 --- /dev/null +++ b/packages/frontend/src/stdlib/analyses/modal_diagram_graph.tsx @@ -0,0 +1,122 @@ +import type { DblModel, DblModelDiagram } from "catlog-wasm"; +import type { DiagramAnalysisProps } from "../../analysis"; +import type { Theory } from "../../theory"; +import type { GraphLayoutConfig, GraphSpec } from "../../visualization"; +import * as graphStyles from "../graph_styles"; +import { GraphVisualizationAnalysis } from "./graph_visualization"; + +/** Visualize a diagram in a model as a graph. + +Such a visualization makes sense for any discrete double theory and is in +general restricted to basic objects. See `ModelGraph` for more. + */ +export default function ModalDiagramGraph( + props: DiagramAnalysisProps & { + title?: string; + }, +) { + const graph = () => { + const theory = props.liveDiagram.liveModel.theory(); + const model = props.liveDiagram.liveModel.elaboratedModel(); + const diagram = props.liveDiagram.elaboratedDiagram(); + if (theory && model && diagram) { + return modalDiagramToGraph(diagram, model, theory); + } + }; + + return ( + + ); +} + +/** Convert a diagram in a model into a graph. */ +export function modalDiagramToGraph( + diagram: DblModelDiagram, + model: DblModel, + theory: Theory, +): GraphSpec.Graph { + // Add nodes for places. + const nodes: GraphSpec.Node[] = []; + for (const id of diagram.obGenerators()) { + const ob = diagram.obPresentation(id); + if (!(ob && ob.over.tag === "Basic")) { + continue; + } + const meta = theory.instanceObTypeMeta(ob.obType); + const label = ob.label?.join("."); + const overLabel = model.obGeneratorLabel(ob.over.content)?.join("."); + nodes.push({ + id, + label: [label, overLabel].filter((s) => s).join(" : "), + cssClass: graphStyles.svgNodeCssClasses(meta).join(" "), + isMonospaced: graphStyles.isMonospaced(meta), + }); + } + + /// Add nodes for transitions and edges for arcs. + const edges: GraphSpec.Edge[] = []; + for (const id of diagram.morGenerators()) { + const mor = diagram.morPresentation(id); + if (!(mor && mor.over.tag === "Basic")) { + continue; + } + const overLabel = model.morGeneratorLabel(mor.over.content)?.join("."); + nodes.push({ + id, + label: overLabel, + cssClass: "", + isMonospaced: false, + }); + /// XXX have cases for each modality + // incoming edges + if (mor.dom.tag === "List") { + for (const ob of mor.dom.content.objects) { + if (!(ob && ob.tag === "Basic")) { + continue; + } + edges.push({ + id: `${id}:dom:${ob.content}`, + source: ob.content, + target: id, + label: "", + cssClass: "", + isMonospaced: false, + }); + } + } + if (mor.cod.tag === "List") { + for (const ob of mor.cod.content.objects) { + if (!(ob && ob.tag === "Basic")) { + continue; + } + edges.push({ + id: `${ob.content}:cod:${id}`, + source: id, + target: ob.content, + label: "", + cssClass: "", + isMonospaced: false, + }); + } + } else { + if (!(mor.cod.tag === "Basic")) { + continue; + } + edges.push({ + id, + source: id, + target: mor.cod.content, + label: "", + cssClass: "", + isMonospaced: false, + }); + } + } + + return { nodes, edges }; +} diff --git a/packages/frontend/src/stdlib/analyses/sql.tsx b/packages/frontend/src/stdlib/analyses/sql.tsx index c8c8e1c18..e01ca25b0 100644 --- a/packages/frontend/src/stdlib/analyses/sql.tsx +++ b/packages/frontend/src/stdlib/analyses/sql.tsx @@ -8,8 +8,6 @@ import { CodeView, BlockTitle, ErrorAlert, IconButton } from "catcolab-ui-compon import type { ModelAnalysisProps } from "../../analysis"; import * as SQL from "./sql_types.ts"; -import styles from "./sql.module.css"; - const copyToClipboard = (text: string) => navigator.clipboard.writeText(text); const tooltip = () => ( @@ -33,7 +31,14 @@ const tooltip = () => ( export function SQLHeader(sql: string) { return ( -
+
copyToClipboard(sql)} disabled={false} @@ -107,13 +112,10 @@ export default function SQLSchemaAnalysis( )} -
- - -

{"The model failed to compile into a SQL script."}

-

{"Check for cycles in foreign key constraints."}

- -
+ +

{"The model failed to compile into a SQL script."}

+

{"Check for cycles in foreign key constraints."}

+ )} diff --git a/packages/frontend/src/stdlib/theories.ts b/packages/frontend/src/stdlib/theories.ts index 507e13a2d..d516d2d83 100644 --- a/packages/frontend/src/stdlib/theories.ts +++ b/packages/frontend/src/stdlib/theories.ts @@ -143,13 +143,13 @@ stdTheories.add( stdTheories.add( { - id: "unary-dec", + id: "dec", name: "Discrete exterior calculus (DEC)", description: "DEC operators on a geometrical space", iconLetters: ["D", "c"], group: "Experimental", }, - async () => (await import("./theories/unary-dec")).default, + async () => (await import("./theories/dec")).default, ); stdTheories.add( diff --git a/packages/frontend/src/stdlib/theories/dec.ts b/packages/frontend/src/stdlib/theories/dec.ts new file mode 100644 index 000000000..c4ecb3369 --- /dev/null +++ b/packages/frontend/src/stdlib/theories/dec.ts @@ -0,0 +1,67 @@ +import { lazy } from "solid-js"; + +import { ThDEC } from "catlog-wasm"; +import { type DiagramAnalysisMeta, Theory, type TheoryMeta } from "../../theory"; +import * as analyses from "../analyses"; + +const ObjectCellEditor = lazy(() => import("../../model/object_cell_editor")); +const MorphismCellEditor = lazy(() => import("../../model/morphism_cell_editor")); + +export default function createThDECTheory(theoryMeta: TheoryMeta): Theory { + const thDEC = new ThDEC(); + const diagramAnalyses: DiagramAnalysisMeta[] = [ + analyses.modalDiagramGraph({ + id: "graph", + name: "Visualization", + description: "Visualize the instance as a graph", + help: "visualization", + }), + ]; + + return new Theory({ + ...theoryMeta, + theory: thDEC.theory(), + modelTypes: [ + { + tag: "ObType", + obType: { tag: "Basic", content: "Object" }, + editor: ObjectCellEditor, + name: "Form", + description: "State of the system", + shortcut: ["O"], + }, + { + tag: "MorType", + morType: { + tag: "Basic", + content: "Multihom", + }, + editor: MorphismCellEditor, + name: "Operation", + description: "Event causing change of state", + shortcut: ["M"], + }, + ], + instanceOfName: "Diagrams in", + instanceTypes: [ + { + tag: "ObType", + obType: { tag: "Basic", content: "Object" }, + name: "Element", + description: "State of the system", + shortcut: ["O"], + }, + { + tag: "MorType", + morType: { + tag: "Basic", + content: "Multihom", + }, + name: "Operation", + description: "Event causing change of state", + shortcut: ["M"], + }, + ], + diagramAnalyses: diagramAnalyses, + }); +} diff --git a/packages/frontend/src/stdlib/theories/petri-net.ts b/packages/frontend/src/stdlib/theories/petri-net.ts index e584783df..14422caab 100644 --- a/packages/frontend/src/stdlib/theories/petri-net.ts +++ b/packages/frontend/src/stdlib/theories/petri-net.ts @@ -11,6 +11,26 @@ const MorphismCellEditor = lazy(() => import("../../model/morphism_cell_editor") export default function createPetriNetTheory(theoryMeta: TheoryMeta): Theory { const thSymMonoidalCategory = new ThSymMonoidalCategory(); + // const _diagramAnalyses: DiagramAnalysisMeta[] = [ + // analyses.diagramGraph({ + // id: "graph", + // name: "Visualization", + // description: "Visualize the instance as a graph", + // help: "visualization", + // }), + // ]; + + // if (import.meta.env.DEV) { + // diagramAnalyses.push( + // analyses.tabularView({ + // id: "tabularview", + // name: "Tabular Visualization", + // description: "Visualize the instance as a table", + // help: "tabularview", + // }), + // ); + // } + return new Theory({ ...theoryMeta, theory: thSymMonoidalCategory.theory(),