diff --git a/Cargo.lock b/Cargo.lock index 012bd7c34..f2f97ca4b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -307,6 +307,7 @@ dependencies = [ "all-the-same", "catlog", "console_error_panic_hook", + "derive_more", "getrandom", "js-sys", "nonempty", diff --git a/packages/catlog-wasm/Cargo.toml b/packages/catlog-wasm/Cargo.toml index 43d0fd5d8..da47ce042 100644 --- a/packages/catlog-wasm/Cargo.toml +++ b/packages/catlog-wasm/Cargo.toml @@ -14,6 +14,7 @@ default = ["console_error_panic_hook"] all-the-same = "1.1.0" catlog = { path = "../catlog", features = ["ode", "serde-wasm"] } console_error_panic_hook = { version = "0.1.7", optional = true } +derive_more = { version = "1", features = ["from", "try_into"] } getrandom = { version = "0.2", features = ["js"] } js-sys = "0.3.69" nonempty = { version = "0.10", features = ["serialize"] } diff --git a/packages/catlog-wasm/src/diagram.rs b/packages/catlog-wasm/src/diagram.rs deleted file mode 100644 index 2e9660681..000000000 --- a/packages/catlog-wasm/src/diagram.rs +++ /dev/null @@ -1,68 +0,0 @@ -//! Wasm bindings for diagrams in models of a double theory. - -use uuid::Uuid; - -use serde::{Deserialize, Serialize}; -use tsify_next::Tsify; -use wasm_bindgen::prelude::*; - -use super::model::{Mor, Ob}; -use super::theory::{MorType, ObType}; - -/// An object of a diagram in a model of a double theory. -#[derive(Debug, Serialize, Deserialize, Tsify)] -#[tsify(into_wasm_abi, from_wasm_abi)] -pub struct DiagramOb { - /// Indexing object. - pub ob: Ob, - - /// Object in the model that the indexing object is over. - pub over: Ob, -} - -/// A morphism of a diagram in a model of a double theory. -#[derive(Debug, Serialize, Deserialize, Tsify)] -#[tsify(into_wasm_abi, from_wasm_abi)] -pub struct DiagramMor { - /// Indexing morphism. - pub mor: Mor, - - /// Morphism that the indexing morphism is over (mapped to). - pub over: Mor, -} - -/// Declares an object of a diagram in a model. -#[derive(Serialize, Deserialize, Tsify)] -#[tsify(into_wasm_abi, from_wasm_abi, missing_as_null)] -pub struct DiagramObDecl { - /// Globally unique identifier of object. - pub id: Uuid, - - /// The object's type in the double theory. - #[serde(rename = "obType")] - pub ob_type: ObType, - - /// Object in the model that this object is over, if defined. - pub over: Option, -} - -/// Declares a morphism of a diagram in a model. -#[derive(Serialize, Deserialize, Tsify)] -#[tsify(into_wasm_abi, from_wasm_abi, missing_as_null)] -pub struct DiagramMorDecl { - /// Globally unique identifier of morphism. - pub id: Uuid, - - /// The morphism's type in the double theory. - #[serde(rename = "morType")] - pub mor_type: MorType, - - /// Morphism in the model that this morphism is over, if defined. - pub over: Option, - - /// Domain of this morphism, if defined. - pub dom: Option, - - /// Codomain of this morphism, if defined. - pub cod: Option, -} diff --git a/packages/catlog-wasm/src/lib.rs b/packages/catlog-wasm/src/lib.rs index 7ef691882..f39acc04f 100644 --- a/packages/catlog-wasm/src/lib.rs +++ b/packages/catlog-wasm/src/lib.rs @@ -1,7 +1,7 @@ pub mod result; -pub mod diagram; pub mod model; +pub mod model_diagram; pub mod model_morphism; pub mod theory; diff --git a/packages/catlog-wasm/src/model.rs b/packages/catlog-wasm/src/model.rs index fe4559943..7393986e6 100644 --- a/packages/catlog-wasm/src/model.rs +++ b/packages/catlog-wasm/src/model.rs @@ -1,21 +1,23 @@ //! Wasm bindings for models of double theories. use all_the_same::all_the_same; +use derive_more::{From, TryInto}; use uuid::Uuid; use serde::{Deserialize, Serialize}; use tsify_next::Tsify; use wasm_bindgen::prelude::*; -use super::theory::*; use catlog::dbl::model::{self as dbl_model, FgDblModel, InvalidDiscreteDblModel}; use catlog::one::fin_category::UstrFinCategory; -use catlog::one::Path; -use catlog::one::{Category as _, FgCategory}; -use catlog::validate::{self, Validate}; +use catlog::one::{Category as _, FgCategory, Path}; +use catlog::validate::Validate; + +use super::result::JsResult; +use super::theory::{DblTheory, DblTheoryBox, MorType, ObType}; /// An object in a model of a double theory. -#[derive(Debug, Serialize, Deserialize, Tsify)] +#[derive(Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)] #[serde(tag = "tag", content = "content")] #[tsify(into_wasm_abi, from_wasm_abi)] pub enum Ob { @@ -27,7 +29,7 @@ pub enum Ob { } /// A morphism in a model of a double theory. -#[derive(Debug, Serialize, Deserialize, Tsify)] +#[derive(Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)] #[serde(tag = "tag", content = "content")] #[tsify(into_wasm_abi, from_wasm_abi)] pub enum Mor { @@ -113,36 +115,19 @@ pub struct MorDecl { pub cod: Option, } -type UuidDiscreteDblModel = dbl_model::DiscreteDblModel; +pub(crate) type DiscreteDblModel = dbl_model::DiscreteDblModel; /** A box containing a model of a double theory of any kind. See [`DblTheoryBox`] for motivation. */ +#[derive(From, TryInto)] +#[try_into(ref)] pub enum DblModelBox { - Discrete(UuidDiscreteDblModel), + Discrete(DiscreteDblModel), // DiscreteTab(()), // TODO: Not yet implemented. } -/// Converts from a model of a discrete double theory. -impl From for DblModel { - fn from(model: UuidDiscreteDblModel) -> Self { - DblModel(DblModelBox::Discrete(model)) - } -} - -/// Converts into a model of a dicrete double theory. -impl<'a> TryFrom<&'a DblModel> for &'a UuidDiscreteDblModel { - type Error = String; - - fn try_from(model: &'a DblModel) -> Result { - match &model.0 { - DblModelBox::Discrete(model) => Ok(model), - //_ => Err("Cannot cast into a model of a discrete double theory".into()), - } - } -} - /// Wasm bindings for a model of a double theory. #[wasm_bindgen] pub struct DblModel(#[wasm_bindgen(skip)] pub DblModelBox); @@ -153,9 +138,7 @@ impl DblModel { #[wasm_bindgen(constructor)] pub fn new(theory: &DblTheory) -> Self { Self(match &theory.0 { - DblTheoryBox::Discrete(th) => { - DblModelBox::Discrete(UuidDiscreteDblModel::new(th.clone())) - } + DblTheoryBox::Discrete(th) => DiscreteDblModel::new(th.clone()).into(), DblTheoryBox::DiscreteTab(_) => panic!("Not implemented"), }) } @@ -178,10 +161,12 @@ impl DblModel { DblModelBox::[Discrete](model) => { let mor_type = decl.mor_type.try_into()?; let res = model.make_mor(decl.id, mor_type); - let dom = decl.dom.map(|ob| ob.try_into()).transpose()?; - let cod = decl.cod.map(|ob| ob.try_into()).transpose()?; - model.update_dom(decl.id, dom); - model.update_cod(decl.id, cod); + if let Some(dom) = decl.dom.map(|ob| ob.try_into()).transpose()? { + model.set_dom(decl.id, dom); + } + if let Some(cod) = decl.cod.map(|ob| ob.try_into()).transpose()? { + model.set_cod(decl.id, cod); + } Ok(res) } }) @@ -249,48 +234,68 @@ impl DblModel { /// Validates that the model is well defined. #[wasm_bindgen] - pub fn validate(&self) -> Vec> { + pub fn validate(&self) -> ModelValidationResult { all_the_same!(match &self.0 { - DblModelBox::[Discrete](model) => validate::unwrap_errors(model.validate()) + DblModelBox::[Discrete](model) => { + let res = model.validate(); + ModelValidationResult(res.map_err(|errs| errs.into()).into()) + } }) } } +/// Result of validating a model of a double theory. +#[derive(Serialize, Deserialize, Tsify)] +#[tsify(into_wasm_abi, from_wasm_abi)] +pub struct ModelValidationResult(pub JsResult<(), Vec>>); + #[cfg(test)] -mod tests { +pub(crate) mod tests { use super::*; use crate::theories::*; - #[test] - fn model_schema() { - let th = ThSchema::new().theory(); - let mut model = DblModel::new(&th); - let (x, y, a) = (Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()); + pub(crate) fn sch_walking_attr(th: &DblTheory, ids: [Uuid; 3]) -> DblModel { + let mut model = DblModel::new(th); + let [attr, entity, attr_type] = ids; assert!(model .add_ob(ObDecl { - id: x, + id: entity, ob_type: ObType::Basic("Entity".into()), }) .is_ok()); assert!(model .add_ob(ObDecl { - id: y, + id: attr_type, ob_type: ObType::Basic("AttrType".into()), }) .is_ok()); assert!(model .add_mor(MorDecl { - id: a, + id: attr, mor_type: MorType::Basic("Attr".into()), - dom: Some(Ob::Basic(x)), - cod: Some(Ob::Basic(y)), + dom: Some(Ob::Basic(entity)), + cod: Some(Ob::Basic(attr_type)), }) .is_ok()); + model + } + + #[test] + fn model_schema() { + let th = ThSchema::new().theory(); + let [a, x, y] = [Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()]; + let model = sch_walking_attr(&th, [a, x, y]); + assert_eq!(model.has_ob(Ob::Basic(x)), Ok(true)); assert_eq!(model.has_mor(Mor::Basic(a)), Ok(true)); assert_eq!(model.objects().len(), 2); assert_eq!(model.morphisms().len(), 1); - assert!(model.validate().is_empty()); + assert_eq!(model.objects_with_type(ObType::Basic("Entity".into())), Ok(vec![Ob::Basic(x)])); + assert_eq!( + model.morphisms_with_type(MorType::Basic("Attr".into())), + Ok(vec![Mor::Basic(a)]) + ); + assert_eq!(model.validate().0, JsResult::Ok(())); let mut model = DblModel::new(&th); assert!(model @@ -301,6 +306,9 @@ mod tests { cod: Some(Ob::Basic(y)), }) .is_ok()); - assert_eq!(model.validate().len(), 2); + let JsResult::Err(errs) = model.validate().0 else { + panic!("Model should not validate") + }; + assert_eq!(errs.len(), 2); } } diff --git a/packages/catlog-wasm/src/model_diagram.rs b/packages/catlog-wasm/src/model_diagram.rs new file mode 100644 index 000000000..31700326e --- /dev/null +++ b/packages/catlog-wasm/src/model_diagram.rs @@ -0,0 +1,227 @@ +//! Wasm bindings for diagrams in models of a double theory. + +use all_the_same::all_the_same; +use derive_more::From; +use uuid::Uuid; + +use serde::{Deserialize, Serialize}; +use tsify_next::Tsify; +use wasm_bindgen::prelude::*; + +use catlog::dbl::model::FgDblModel; +use catlog::dbl::model_diagram as diagram; +use catlog::one::FgCategory; + +use super::model::{DblModel, DblModelBox, DiscreteDblModel, Mor, Ob}; +use super::model_morphism::DiscreteDblModelMapping; +use super::result::JsResult; +use super::theory::{DblTheory, MorType, ObType}; + +/// Declares an object of a diagram in a model. +#[derive(Serialize, Deserialize, Tsify)] +#[tsify(into_wasm_abi, from_wasm_abi, missing_as_null)] +pub struct DiagramObDecl { + /// Globally unique identifier of object. + pub id: Uuid, + + /// The object's type in the double theory. + #[serde(rename = "obType")] + pub ob_type: ObType, + + /// Object in the model that this object is over, if defined. + pub over: Option, +} + +/// Declares a morphism of a diagram in a model. +#[derive(Serialize, Deserialize, Tsify)] +#[tsify(into_wasm_abi, from_wasm_abi, missing_as_null)] +pub struct DiagramMorDecl { + /// Globally unique identifier of morphism. + pub id: Uuid, + + /// The morphism's type in the double theory. + #[serde(rename = "morType")] + pub mor_type: MorType, + + /// Morphism in the model that this morphism is over, if defined. + pub over: Option, + + /// Domain of this morphism, if defined. + pub dom: Option, + + /// Codomain of this morphism, if defined. + pub cod: Option, +} + +/// A box containing a diagram in a model of a double theory. +#[derive(From)] +pub enum DblModelDiagramBox { + Discrete(diagram::DblModelDiagram), +} + +/// Wasm bindings for a diagram in a model of a double theory. +#[wasm_bindgen] +pub struct DblModelDiagram(#[wasm_bindgen(skip)] pub DblModelDiagramBox); + +#[wasm_bindgen] +impl DblModelDiagram { + /// Creates an empty diagram for the given theory. + #[wasm_bindgen(constructor)] + pub fn new(theory: &DblTheory) -> Self { + let model = DblModel::new(theory); + Self(all_the_same!(match model.0 { + DblModelBox::[Discrete](model) => { + let mapping = Default::default(); + diagram::DblModelDiagram(mapping, model).into() + } + })) + } + + /// Adds an object to the diagram. + #[wasm_bindgen(js_name = "addOb")] + pub fn add_ob(&mut self, decl: DiagramObDecl) -> Result { + all_the_same!(match &mut self.0 { + DblModelDiagramBox::[Discrete](diagram) => { + let (mapping, model) = diagram.into(); + let ob_type = decl.ob_type.try_into()?; + if let Some(over) = decl.over.map(|ob| ob.try_into()).transpose()? { + mapping.assign_ob(decl.id, over); + } + Ok(model.add_ob(decl.id, ob_type)) + } + }) + } + + /// Adds a morphism to the diagram. + #[wasm_bindgen(js_name = "addMor")] + pub fn add_mor(&mut self, decl: DiagramMorDecl) -> Result { + all_the_same!(match &mut self.0 { + DblModelDiagramBox::[Discrete](diagram) => { + let (mapping, model) = diagram.into(); + let mor_type = decl.mor_type.try_into()?; + let res = model.make_mor(decl.id, mor_type); + if let Some(dom) = decl.dom.map(|ob| ob.try_into()).transpose()? { + model.set_dom(decl.id, dom); + } + if let Some(cod) = decl.cod.map(|ob| ob.try_into()).transpose()? { + model.set_cod(decl.id, cod); + } + if let Some(over) = decl.over.map(|mor| mor.try_into()).transpose()? { + mapping.assign_basic_mor(decl.id, over); + } + Ok(res) + } + }) + } + + /// Returns array of all basic objects in the diagram. + #[wasm_bindgen] + pub fn objects(&self) -> Vec { + all_the_same!(match &self.0 { + DblModelDiagramBox::[Discrete](diagram) => { + let (_, model) = diagram.into(); + model.object_generators().map(|x| x.into()).collect() + } + }) + } + + /// Returns array of all basic morphisms in the diagram. + #[wasm_bindgen] + pub fn morphisms(&self) -> Vec { + all_the_same!(match &self.0 { + DblModelDiagramBox::[Discrete](diagram) => { + let (_, model) = diagram.into(); + model.morphism_generators().map(Mor::Basic).collect() + } + }) + } + + /// Returns array of basic objects with the given type. + #[wasm_bindgen(js_name = "objectsWithType")] + pub fn objects_with_type(&self, ob_type: ObType) -> Result, String> { + all_the_same!(match &self.0 { + DblModelDiagramBox::[Discrete](diagram) => { + let (_, model) = diagram.into(); + let ob_type = ob_type.try_into()?; + Ok(model.object_generators_with_type(&ob_type).map(Ob::Basic).collect()) + } + }) + } + + /// Returns array of basic morphisms with the given type. + #[wasm_bindgen(js_name = "morphismsWithType")] + pub fn morphisms_with_type(&self, mor_type: MorType) -> Result, String> { + all_the_same!(match &self.0 { + DblModelDiagramBox::[Discrete](diagram) => { + let (_, model) = diagram.into(); + let mor_type = mor_type.try_into()?; + Ok(model.morphism_generators_with_type(&mor_type).map(Mor::Basic).collect()) + } + }) + } + + /// Validates that the diagram is well defined in a model. + #[wasm_bindgen] + pub fn validate_in(&self, model: &DblModel) -> Result { + all_the_same!(match &self.0 { + DblModelDiagramBox::[Discrete](diagram) => { + let model = (&model.0).try_into().map_err( + |_| "Type of model should match type of diagram")?; + let res = diagram.validate_in(model); + Ok(ModelDiagramValidationResult(res.map_err(|errs| errs.into()).into())) + } + }) + } +} + +/// Result of validating a diagram in a model. +#[derive(Serialize, Deserialize, Tsify)] +#[tsify(into_wasm_abi, from_wasm_abi)] +pub struct ModelDiagramValidationResult( + pub JsResult<(), Vec>>, +); + +#[cfg(test)] +mod tests { + use super::*; + use crate::model::tests::sch_walking_attr; + use crate::theories::*; + + #[test] + fn diagram_schema() { + let th = ThSchema::new().theory(); + let [attr, entity, attr_type] = [Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()]; + let model = sch_walking_attr(&th, [attr, entity, attr_type]); + + let mut diagram = DblModelDiagram::new(&th); + let [x, y, var] = [Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()]; + assert!(diagram + .add_ob(DiagramObDecl { + id: var, + ob_type: ObType::Basic("AttrType".into()), + over: Some(Ob::Basic(attr_type)) + }) + .is_ok()); + for indiv in [x, y] { + assert!(diagram + .add_ob(DiagramObDecl { + id: indiv, + ob_type: ObType::Basic("Entity".into()), + over: Some(Ob::Basic(entity)) + }) + .is_ok()); + assert!(diagram + .add_mor(DiagramMorDecl { + id: Uuid::now_v7(), + mor_type: MorType::Basic("Attr".into()), + dom: Some(Ob::Basic(indiv)), + cod: Some(Ob::Basic(var)), + over: Some(Mor::Basic(attr)), + }) + .is_ok()); + } + assert_eq!(diagram.objects().len(), 3); + assert_eq!(diagram.morphisms().len(), 2); + assert_eq!(diagram.validate_in(&model).unwrap().0, JsResult::Ok(())); + } +} diff --git a/packages/catlog-wasm/src/model_morphism.rs b/packages/catlog-wasm/src/model_morphism.rs index e2fd2507a..f1626893a 100644 --- a/packages/catlog-wasm/src/model_morphism.rs +++ b/packages/catlog-wasm/src/model_morphism.rs @@ -1,10 +1,13 @@ use std::hash::Hash; +use uuid::Uuid; + +use catlog::dbl::{model, model_morphism}; +use catlog::one::{fin_category::UstrFinCategory, FgCategory}; + use super::model::DblModel; -use catlog::dbl::model; -use catlog::dbl::model_morphism::DiscreteDblModelMapping; -use catlog::one::fin_category::UstrFinCategory; -use catlog::one::FgCategory; + +pub(crate) type DiscreteDblModelMapping = model_morphism::DiscreteDblModelMapping; /// Find motifs in a model of a discrete double theory. pub fn motifs( @@ -14,8 +17,10 @@ pub fn motifs( where Id: Clone + Eq + Hash, { - let model: &model::DiscreteDblModel<_, _> = model.try_into()?; - let mut images: Vec<_> = DiscreteDblModelMapping::morphisms(motif, model) + let model: &model::DiscreteDblModel<_, _> = (&model.0) + .try_into() + .map_err(|_| "Motif finding expects a discrete double model")?; + let mut images: Vec<_> = model_morphism::DiscreteDblModelMapping::morphisms(motif, model) .monic() .find_all() .into_iter() @@ -28,7 +33,7 @@ where // Remove duplicates: different morphisms can have the same image. retain_unique(&mut images); - Ok(images.into_iter().map(|im| im.into()).collect()) + Ok(images.into_iter().map(|im| DblModel(im.into())).collect()) } /** Remove duplicate elements from a vector. diff --git a/packages/catlog-wasm/src/result.rs b/packages/catlog-wasm/src/result.rs index 4fc76cdb0..e21f334d5 100644 --- a/packages/catlog-wasm/src/result.rs +++ b/packages/catlog-wasm/src/result.rs @@ -13,7 +13,7 @@ the `Err` variant is given: When an error should be handled in the UI, it is often more convenient to return an error value than to raise an exception. That's what this enum does. */ -#[derive(Debug, Serialize, Deserialize, Tsify)] +#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize, Tsify)] #[serde(tag = "tag", content = "content")] #[tsify(into_wasm_abi, from_wasm_abi)] pub enum JsResult { diff --git a/packages/catlog-wasm/src/theories.rs b/packages/catlog-wasm/src/theories.rs index 489c69896..c9d680ddc 100644 --- a/packages/catlog-wasm/src/theories.rs +++ b/packages/catlog-wasm/src/theories.rs @@ -29,7 +29,7 @@ impl ThCategory { #[wasm_bindgen] pub fn theory(&self) -> DblTheory { - self.0.clone().into() + DblTheory(self.0.clone().into()) } } @@ -46,7 +46,7 @@ impl ThSchema { #[wasm_bindgen] pub fn theory(&self) -> DblTheory { - self.0.clone().into() + DblTheory(self.0.clone().into()) } } @@ -63,7 +63,7 @@ impl ThSignedCategory { #[wasm_bindgen] pub fn theory(&self) -> DblTheory { - self.0.clone().into() + DblTheory(self.0.clone().into()) } /// Find positive feedback loops in a model. @@ -87,7 +87,9 @@ impl ThSignedCategory { model: &DblModel, data: LotkaVolterraModelData, ) -> Result { - let model: &DiscreteDblModel<_, _> = model.try_into()?; + let model: &DiscreteDblModel<_, _> = (&model.0) + .try_into() + .map_err(|_| "Lotka-Volterra simulation expects a discrete double model")?; Ok(ODEResult( analyses::ode::LotkaVolterraAnalysis::new(ustr("Object")) .add_positive(FinMor::Id(ustr("Object"))) @@ -112,7 +114,7 @@ impl ThNullableSignedCategory { #[wasm_bindgen] pub fn theory(&self) -> DblTheory { - self.0.clone().into() + DblTheory(self.0.clone().into()) } } @@ -129,7 +131,7 @@ impl ThCategoryLinks { #[wasm_bindgen] pub fn theory(&self) -> DblTheory { - self.0.clone().into() + DblTheory(self.0.clone().into()) } } diff --git a/packages/catlog-wasm/src/theory.rs b/packages/catlog-wasm/src/theory.rs index f155bd0a3..4ddb5c91b 100644 --- a/packages/catlog-wasm/src/theory.rs +++ b/packages/catlog-wasm/src/theory.rs @@ -1,9 +1,11 @@ //! Wasm bindings for double theories. -use all_the_same::all_the_same; use std::collections::HashMap; use std::hash::Hash; use std::sync::Arc; + +use all_the_same::all_the_same; +use derive_more::From; use ustr::Ustr; use serde::{Deserialize, Serialize}; @@ -11,7 +13,7 @@ use tsify_next::Tsify; use wasm_bindgen::prelude::*; use catlog::dbl::theory; -use catlog::dbl::theory::{DblTheory as BaseDblTheory, TabMorType, TabObType}; +use catlog::dbl::theory::{DblTheory as _, TabMorType, TabObType}; use catlog::one::fin_category::*; /// Object type in a double theory. @@ -130,6 +132,7 @@ underlying double theory, but `wasm-bindgen` does not support [generics](https://github.com/rustwasm/wasm-bindgen/issues/3309). Instead, we explicitly enumerate the supported kinds of double theories in this enum. */ +#[derive(From)] pub enum DblTheoryBox { Discrete(Arc), DiscreteTab(Arc), @@ -140,20 +143,6 @@ pub enum DblTheoryBox { #[wasm_bindgen] pub struct DblTheory(#[wasm_bindgen(skip)] pub DblTheoryBox); -/// Converts from a discrete double theory. -impl From> for DblTheory { - fn from(theory: Arc) -> Self { - Self(DblTheoryBox::Discrete(theory)) - } -} - -/// Converts from a discrete tabulator theory. -impl From> for DblTheory { - fn from(theory: Arc) -> Self { - Self(DblTheoryBox::DiscreteTab(theory)) - } -} - #[wasm_bindgen] impl DblTheory { /// Kind of double theory ("double doctrine"). diff --git a/packages/catlog/src/dbl/model.rs b/packages/catlog/src/dbl/model.rs index a90cb1244..8c52d292e 100644 --- a/packages/catlog/src/dbl/model.rs +++ b/packages/catlog/src/dbl/model.rs @@ -222,14 +222,14 @@ where self.category.make_mor_generator(f) } - /// Updates the domain of a morphism, setting or unsetting it. - pub fn update_dom(&mut self, f: Id, x: Option) -> Option { - self.category.update_dom(f, x) + /// Sets the domain of a morphism. + pub fn set_dom(&mut self, f: Id, x: Id) -> Option { + self.category.set_dom(f, x) } /// Updates the codomain of a morphism, setting or unsetting it. - pub fn update_cod(&mut self, f: Id, x: Option) -> Option { - self.category.update_cod(f, x) + pub fn set_cod(&mut self, f: Id, x: Id) -> Option { + self.category.set_cod(f, x) } /// Iterates over failures to be well-defined model. @@ -413,7 +413,7 @@ where TODO: Missing case that equation has different composite morphism types on left and right hand sides. */ -#[derive(Debug)] +#[derive(Clone, Debug, PartialEq, Eq)] #[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] #[cfg_attr(feature = "serde", serde(tag = "tag", content = "content"))] #[cfg_attr(feature = "serde-wasm", derive(Tsify))] diff --git a/packages/catlog/src/dbl/model_diagram.rs b/packages/catlog/src/dbl/model_diagram.rs index 32a6c8f60..539e91f30 100644 --- a/packages/catlog/src/dbl/model_diagram.rs +++ b/packages/catlog/src/dbl/model_diagram.rs @@ -15,40 +15,28 @@ TODO: Document in devs docs and link here. use std::hash::Hash; +use derive_more::Into; +use either::Either; use nonempty::NonEmpty; +#[cfg(feature = "serde")] +use serde::{Deserialize, Serialize}; +#[cfg(feature = "serde-wasm")] +use tsify_next::{declare, Tsify}; + +use super::model::{DiscreteDblModel, InvalidDiscreteDblModel}; +use super::model_morphism::*; use crate::one::FgCategory; use crate::validate; -use super::model::DiscreteDblModel; -use super::model_morphism::DblModelMorphism; -use super::model_morphism::{DblModelMapping, DiscreteDblModelMapping, InvalidDblModelMorphism}; - /** A diagram in a model of a double theory. -This struct owns its data, namely, the domain model and the model -[mapping](DblModelMapping). The domain is assumed to be a valid model of a -double theory. If that is in question, then the model should be validated -*before* validating this object. +This struct owns its data, namely, the domain of the diagram (a model) and the +model [mapping](DblModelMapping) itself. */ -pub struct DblModelDiagram(Map, Dom); - -impl DblModelDiagram { - /// Constructs a new diagram from the given mapping and domain model. - pub fn new(map: Map, dom: Dom) -> Self { - Self(map, dom) - } - - /// The mapping underlying the diagram. - pub fn mapping(&self) -> &Map { - &self.0 - } - - /// The domain, or shape, of the diagram. - pub fn domain(&self) -> &Dom { - &self.1 - } -} +#[derive(Clone, Into)] +#[into(owned, ref, ref_mut)] +pub struct DblModelDiagram(pub Map, pub Dom); impl DblModelDiagram where @@ -65,10 +53,29 @@ where } } +/// A failure of a diagram in a model to be valid. +#[derive(Clone, Debug, PartialEq, Eq)] +#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr(feature = "serde", serde(tag = "tag", content = "err"))] +#[cfg_attr(feature = "serde-wasm", derive(Tsify))] +#[cfg_attr(feature = "serde-wasm", tsify(into_wasm_abi, from_wasm_abi))] +pub enum InvalidDblModelDiagram { + /// Domain of the diagram is invalid. + Dom(DomErr), + + /// Mapping underlying the diagram is invalid. + Map(MapErr), +} + /// A diagram in a model of a discrete double theory. pub type DiscreteDblModelDiagram = DblModelDiagram, DiscreteDblModel>; +/// A failure to be valid in a diagram in a model of a discrete double theory. +#[cfg_attr(feature = "serde-wasm", declare)] +pub type InvalidDiscreteDblModelDiagram = + InvalidDblModelDiagram, InvalidDblModelMorphism>; + impl DiscreteDblModelDiagram where DomId: Eq + Clone + Hash, @@ -77,11 +84,14 @@ where Cat::Ob: Hash, Cat::Mor: Hash, { - /// Validates that the diagram is well-defined in the given model. + /** 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: &DiscreteDblModel, - ) -> Result<(), NonEmpty>> { + ) -> Result<(), NonEmpty>> { validate::wrap_errors(self.iter_invalid_in(model)) } @@ -89,9 +99,14 @@ where pub fn iter_invalid_in<'a>( &'a self, model: &'a DiscreteDblModel, - ) -> impl Iterator> + '_ { - let morphism = DblModelMorphism::new(self.mapping(), self.domain(), model); - morphism.iter_invalid() + ) -> impl Iterator> + '_ { + 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)) + } } } @@ -119,7 +134,7 @@ mod tests { f.assign_ob(ustr("type"), 'y'); f.assign_basic_mor(ustr("attr"), Path::pair('p', 'q')); - let diagram = DblModelDiagram::new(f, model); + let diagram = DblModelDiagram(f, model); assert_eq!(diagram.ob(&entity), 'x'); assert_eq!(diagram.mor(&Path::single(ustr("attr"))), Path::pair('p', 'q')); } @@ -133,7 +148,7 @@ mod tests { let mut f: DiscreteDblModelMapping<_, _> = Default::default(); f.assign_ob(ustr("x"), ustr("x")); f.assign_basic_mor(ustr("positive"), Path::pair(ustr("negative"), ustr("negative"))); - let diagram = DblModelDiagram::new(f, pos_loop); + let diagram = DblModelDiagram(f, pos_loop); assert!(diagram.validate_in(&neg_loop).is_ok()); } } diff --git a/packages/catlog/src/dbl/model_morphism.rs b/packages/catlog/src/dbl/model_morphism.rs index 5c4e454f2..efe077c19 100644 --- a/packages/catlog/src/dbl/model_morphism.rs +++ b/packages/catlog/src/dbl/model_morphism.rs @@ -26,6 +26,11 @@ use derivative::Derivative; use nonempty::NonEmpty; use thiserror::Error; +#[cfg(feature = "serde")] +use serde::{Deserialize, Serialize}; +#[cfg(feature = "serde-wasm")] +use tsify_next::Tsify; + use crate::one::graph_algorithms::{simple_paths, spec_order}; use crate::one::*; use crate::validate::{self, Validate}; @@ -212,14 +217,7 @@ 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>(&'a Map, &'a Dom, &'a Cod); - -impl<'a, Map, Dom, Cod> DblModelMorphism<'a, Map, Dom, Cod> { - /// Constructs a new morphism between models. - pub fn new(map: &'a Map, dom: &'a Dom, cod: &'a Cod) -> Self { - Self(map, dom, cod) - } -} +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, DomId, CodId, Cat> = DblModelMorphism< @@ -376,7 +374,11 @@ where * obtain for free that identities are sent to identities and composites of * generators are sent to their composites in the codomain. */ -#[derive(Debug, Error, PartialEq, Clone)] +#[derive(Clone, Debug, Error, PartialEq)] +#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))] +#[cfg_attr(feature = "serde", serde(tag = "tag", content = "content"))] +#[cfg_attr(feature = "serde-wasm", derive(Tsify))] +#[cfg_attr(feature = "serde-wasm", tsify(into_wasm_abi, from_wasm_abi))] pub enum InvalidDblModelMorphism { /// Invalid data #[error("Object `{0}` is mapped to an object not in the codomain")] @@ -402,12 +404,12 @@ pub enum InvalidDblModelMorphism { #[error("Morphism `{0}` is not mapped to a morphism of the same type in the codomain")] MorType(Mor), - /// A morphism in the domain does not have dom preserved in codomain. - #[error("Morphism `{0}` domain not preserved in the codomain")] + /// Not functorial + #[error("Morphism `{0}` has domain not preserved by the mapping")] Dom(Mor), - /// A morphism in the domain does not have codom preserved in codomain - #[error("Morphism `{0}` codomain not preserved in the codomain")] + /// Not functorial + #[error("Morphism `{0}` has codomain not preserved by the mapping")] Cod(Mor), } diff --git a/packages/catlog/src/one/fin_category.rs b/packages/catlog/src/one/fin_category.rs index c4a48fb8b..01e949864 100644 --- a/packages/catlog/src/one/fin_category.rs +++ b/packages/catlog/src/one/fin_category.rs @@ -321,16 +321,6 @@ where self.generators.set_tgt(e, v) } - /// Updates the domain of a morphism generator, setting or unsetting it. - pub fn update_dom(&mut self, e: E, v: Option) -> Option { - self.generators.update_src(e, v) - } - - /// Updates the codomain of a morphism generator, setting or unsetting it. - pub fn update_cod(&mut self, e: E, v: Option) -> Option { - self.generators.update_tgt(e, v) - } - /// Adds a path equation to the presentation. pub fn add_equation(&mut self, key: EqKey, eq: PathEq) { self.equations.set(key, eq); diff --git a/packages/catlog/src/one/graph.rs b/packages/catlog/src/one/graph.rs index 7e238242a..585b1939b 100644 --- a/packages/catlog/src/one/graph.rs +++ b/packages/catlog/src/one/graph.rs @@ -169,16 +169,6 @@ pub trait ColumnarGraphMut: ColumnarGraph { fn set_tgt(&mut self, e: Self::E, v: Self::V) -> Option { self.tgt_map_mut().set(e, v) } - - /// Updates the source of an edge, setting or unsetting it. - fn update_src(&mut self, e: Self::E, v: Option) -> Option { - self.src_map_mut().update(e, v) - } - - /// Updates the source of an edge, setting or unsetting it. - fn update_tgt(&mut self, e: Self::E, v: Option) -> Option { - self.tgt_map_mut().update(e, v) - } } /** Derive implementation of a graph from a columnar graph. diff --git a/packages/frontend/package.json b/packages/frontend/package.json index 15550927c..e3480e086 100644 --- a/packages/frontend/package.json +++ b/packages/frontend/package.json @@ -31,6 +31,7 @@ "@modular-forms/solid": "^0.24.1", "@qubit-rs/client": "^0.4.4", "@solid-primitives/active-element": "^2.0.20", + "@solid-primitives/autofocus": "^0.0.111", "@solid-primitives/context": "^0.2.3", "@solid-primitives/destructure": "^0.1.17", "@solid-primitives/keyboard": "^1.2.8", diff --git a/packages/frontend/pnpm-lock.yaml b/packages/frontend/pnpm-lock.yaml index 675e47e35..11ca12560 100644 --- a/packages/frontend/pnpm-lock.yaml +++ b/packages/frontend/pnpm-lock.yaml @@ -53,6 +53,9 @@ importers: '@solid-primitives/active-element': specifier: ^2.0.20 version: 2.0.20(solid-js@1.9.2) + '@solid-primitives/autofocus': + specifier: ^0.0.111 + version: 0.0.111(solid-js@1.9.2) '@solid-primitives/context': specifier: ^0.2.3 version: 0.2.3(solid-js@1.9.2) @@ -1094,6 +1097,11 @@ packages: peerDependencies: solid-js: ^1.6.12 + '@solid-primitives/autofocus@0.0.111': + resolution: {integrity: sha512-WQUCcBzUmLdmHeyN0Z1lH75IN1IGIbvOMTcBEmuCY5DXeahRJm3riTGqVj+XOA4G+NHCMt7wPOJoYOAuwUov/Q==} + peerDependencies: + solid-js: ^1.6.12 + '@solid-primitives/context@0.2.3': resolution: {integrity: sha512-6/e8qu9qJf48FJ+sxc/B782NdgFw5TvI8+r6U0gHizumfZcWZg8FAJqvRZAiwlygkUNiTQOGTeO10LVbMm0kvg==} peerDependencies: @@ -3831,6 +3839,11 @@ snapshots: '@solid-primitives/utils': 6.2.3(solid-js@1.9.2) solid-js: 1.9.2 + '@solid-primitives/autofocus@0.0.111(solid-js@1.9.2)': + dependencies: + '@solid-primitives/utils': 6.2.3(solid-js@1.9.2) + solid-js: 1.9.2 + '@solid-primitives/context@0.2.3(solid-js@1.9.2)': dependencies: solid-js: 1.9.2 diff --git a/packages/frontend/src/components/inline_input.tsx b/packages/frontend/src/components/inline_input.tsx index 8d1dbc6a9..c6d016c29 100644 --- a/packages/frontend/src/components/inline_input.tsx +++ b/packages/frontend/src/components/inline_input.tsx @@ -1,6 +1,6 @@ import Popover from "@corvu/popover"; import { focus } from "@solid-primitives/active-element"; -import { type JSX, createSignal } from "solid-js"; +import { type JSX, type Setter, createSignal } from "solid-js"; focus; import { type Completion, Completions, type CompletionsRef } from "./completions"; @@ -10,7 +10,7 @@ import "./inline_input.css"; /** Optional props for `InlineInput` component. */ export type InlineInputOptions = { - ref?: HTMLInputElement; + ref?: HTMLInputElement | Setter; placeholder?: string; status?: InlineInputErrorStatus; completions?: Completion[]; diff --git a/packages/frontend/src/diagram/document.ts b/packages/frontend/src/diagram/document.ts index 0acdedbca..6c88441fa 100644 --- a/packages/frontend/src/diagram/document.ts +++ b/packages/frontend/src/diagram/document.ts @@ -1,11 +1,11 @@ import { type Accessor, createMemo } from "solid-js"; -import type { Uuid } from "catlog-wasm"; +import type { DblModelDiagram, ModelDiagramValidationResult, Uuid } from "catlog-wasm"; import type { ExternRef, LiveDoc } from "../api"; import type { LiveModelDocument } from "../model"; import { type Notebook, newNotebook } from "../notebook"; import { type IndexedMap, indexMap } from "../util/indexing"; -import type { DiagramJudgment } from "./types"; +import { type DiagramJudgment, catlogDiagram } from "./types"; /** A document defining a diagram in a model. */ export type DiagramDocument = { @@ -50,6 +50,15 @@ export type LiveDiagramDocument = { /** A memo of the indexed map from object ID to name. */ objectIndex: Accessor>; + + /** A memo of the diagram constructed and validated in the core. */ + validatedDiagram: Accessor; +}; + +/** A validated diagram as represented in `catlog`. */ +export type ValidatedDiagram = { + diagram: DblModelDiagram; + result: ModelDiagramValidationResult; }; export function enlivenDiagramDocument( @@ -75,5 +84,21 @@ export function enlivenDiagramDocument( return indexMap(map); }, indexMap(new Map())); - return { refId, liveDoc, liveModel, formalJudgments, objectIndex }; + const validatedDiagram = createMemo( + () => { + const th = liveModel.theory(); + const validatedModel = liveModel.validatedModel(); + if (!(th && validatedModel?.result.tag === "Ok")) { + // Abort immediately if the model itself is invalid. + return undefined; + } + const diagram = catlogDiagram(th.theory, formalJudgments()); + const result = diagram.validate_in(validatedModel.model); + return { diagram, result }; + }, + undefined, + { equals: false }, + ); + + return { refId, liveDoc, liveModel, formalJudgments, objectIndex, validatedDiagram }; } diff --git a/packages/frontend/src/diagram/morphism_cell_editor.tsx b/packages/frontend/src/diagram/morphism_cell_editor.tsx index 3c9085ef1..d594f317b 100644 --- a/packages/frontend/src/diagram/morphism_cell_editor.tsx +++ b/packages/frontend/src/diagram/morphism_cell_editor.tsx @@ -1,8 +1,9 @@ -import { useContext } from "solid-js"; +import { createSignal, useContext } from "solid-js"; import invariant from "tiny-invariant"; import { BasicMorInput } from "../model/morphism_input"; import type { CellActions } from "../notebook"; +import { focusInputWhen } from "../util/focus"; import { LiveDiagramContext } from "./context"; import { BasicObInput } from "./object_input"; import type { DiagramMorphismDecl } from "./types"; @@ -18,14 +19,31 @@ export function DiagramMorphismCellEditor(props: { isActive: boolean; actions: CellActions; }) { - let morRef!: HTMLInputElement; + const [morRef, setMorRef] = createSignal(); let domRef!: HTMLInputElement; let codRef!: HTMLInputElement; + focusInputWhen(morRef, () => props.isActive); const liveDiagram = useContext(LiveDiagramContext); invariant(liveDiagram, "Live diagram should be provided as context"); const theory = () => liveDiagram.liveModel.theory(); + const domType = () => theory()?.theory.src(props.decl.morType); + const codType = () => theory()?.theory.tgt(props.decl.morType); + + const errors = () => { + const validated = liveDiagram.validatedDiagram(); + if (validated?.result.tag !== "Err") { + return []; + } + return validated.result.content.filter((err) => err.err.content === props.decl.id); + }; + + const domInvalid = (): boolean => + errors().some((err) => err.err.tag === "Dom" || err.err.tag === "DomType"); + const codInvalid = (): boolean => + errors().some((err) => err.err.tag === "Cod" || err.err.tag === "CodType"); + return (
morRef()?.focus()} + exitBackward={() => morRef()?.focus()} + exitForward={() => codRef.focus()} + exitRight={() => morRef()?.focus()} + onFocus={props.actions.hasFocused} />
{ props.modifyDecl((decl) => { @@ -50,6 +75,15 @@ export function DiagramMorphismCellEditor(props: { }} morType={props.decl.morType} placeholder={theory()?.modelMorTypeMeta(props.decl.morType)?.name} + deleteBackward={props.actions.deleteBackward} + deleteForward={props.actions.deleteForward} + exitBackward={props.actions.activateAbove} + exitForward={() => domRef.focus()} + exitUp={props.actions.activateAbove} + exitDown={props.actions.activateBelow} + exitLeft={() => domRef.focus()} + exitRight={() => codRef.focus()} + onFocus={props.actions.hasFocused} />
@@ -65,6 +99,13 @@ export function DiagramMorphismCellEditor(props: { decl.cod = ob; }); }} + obType={codType()} + invalid={codInvalid()} + deleteBackward={() => morRef()?.focus()} + exitBackward={() => domRef.focus()} + exitForward={props.actions.activateBelow} + exitLeft={() => morRef()?.focus()} + onFocus={props.actions.hasFocused} />
); diff --git a/packages/frontend/src/diagram/object_cell_editor.tsx b/packages/frontend/src/diagram/object_cell_editor.tsx index d09b5cba2..ae44c96a3 100644 --- a/packages/frontend/src/diagram/object_cell_editor.tsx +++ b/packages/frontend/src/diagram/object_cell_editor.tsx @@ -1,9 +1,10 @@ -import { createEffect, useContext } from "solid-js"; +import { createSignal, useContext } from "solid-js"; import invariant from "tiny-invariant"; import { InlineInput } from "../components"; import { ObInput } from "../model/object_input"; import type { CellActions } from "../notebook"; +import { focusInputWhen } from "../util/focus"; import { LiveDiagramContext } from "./context"; import type { DiagramObjectDecl } from "./types"; @@ -17,15 +18,9 @@ export function DiagramObjectCellEditor(props: { isActive: boolean; actions: CellActions; }) { - let nameRef!: HTMLInputElement; + const [nameRef, setNameRef] = createSignal(); let obRef!: HTMLInputElement; - - createEffect(() => { - if (props.isActive) { - nameRef.focus(); - nameRef.selectionStart = nameRef.selectionEnd = nameRef.value.length; - } - }); + focusInputWhen(nameRef, () => props.isActive); const liveDiagram = useContext(LiveDiagramContext); invariant(liveDiagram, "Live diagram should be provided as context"); @@ -34,7 +29,7 @@ export function DiagramObjectCellEditor(props: { return (
{ props.modifyDecl((decl) => { @@ -62,7 +57,7 @@ export function DiagramObjectCellEditor(props: { placeholder={theory()?.modelObTypeMeta(props.decl.obType)?.name} exitUp={props.actions.activateAbove} exitDown={props.actions.activateBelow} - exitLeft={() => nameRef.focus()} + exitLeft={() => nameRef()?.focus()} onFocus={props.actions.hasFocused} />
diff --git a/packages/frontend/src/diagram/object_input.tsx b/packages/frontend/src/diagram/object_input.tsx index bf0301336..40e0a31e3 100644 --- a/packages/frontend/src/diagram/object_input.tsx +++ b/packages/frontend/src/diagram/object_input.tsx @@ -1,7 +1,7 @@ import { useContext } from "solid-js"; import invariant from "tiny-invariant"; -import type { Ob } from "catlog-wasm"; +import type { Ob, ObType } from "catlog-wasm"; import { type IdInputOptions, ObIdInput } from "../components"; import { LiveDiagramContext } from "./context"; @@ -11,10 +11,14 @@ export function BasicObInput( props: { ob: Ob | null; setOb: (ob: Ob | null) => void; + obType?: ObType; } & IdInputOptions, ) { const liveDiagram = useContext(LiveDiagramContext); invariant(liveDiagram, "Live diagram should be provided as context"); - return ; + const completions = (): Ob[] | undefined => + props.obType && liveDiagram.validatedDiagram()?.diagram.objectsWithType(props.obType); + + return ; } diff --git a/packages/frontend/src/diagram/types.ts b/packages/frontend/src/diagram/types.ts index c6c622912..5179e3381 100644 --- a/packages/frontend/src/diagram/types.ts +++ b/packages/frontend/src/diagram/types.ts @@ -1,6 +1,15 @@ import { uuidv7 } from "uuidv7"; -import type { DiagramMorDecl, DiagramObDecl, Mor, MorType, Ob, ObType } from "catlog-wasm"; +import { DblModelDiagram } from "catlog-wasm"; +import type { + DblTheory, + DiagramMorDecl, + DiagramObDecl, + Mor, + MorType, + Ob, + ObType, +} from "catlog-wasm"; /** A judgment in the definition of a diagram in a model. @@ -48,3 +57,16 @@ export const newDiagramMorphismDecl = (morType: MorType, over?: Mor): DiagramMor dom: null, cod: null, }); + +/** Construct a `catlog` diagram in a model from a sequence of judgments. */ +export function catlogDiagram(theory: DblTheory, judgments: Array) { + const diagram = new DblModelDiagram(theory); + for (const judgment of judgments) { + if (judgment.tag === "object") { + diagram.addOb(judgment); + } else if (judgment.tag === "morphism") { + diagram.addMor(judgment); + } + } + return diagram; +} diff --git a/packages/frontend/src/model/document.ts b/packages/frontend/src/model/document.ts index df2ed60e0..1839178ee 100644 --- a/packages/frontend/src/model/document.ts +++ b/packages/frontend/src/model/document.ts @@ -1,12 +1,12 @@ import { type Accessor, createMemo } from "solid-js"; -import type { Uuid } from "catlog-wasm"; +import type { DblModel, ModelValidationResult, Uuid } from "catlog-wasm"; import type { LiveDoc } from "../api"; import { type Notebook, newNotebook } from "../notebook"; import type { TheoryLibrary } from "../stdlib"; import type { Theory, TheoryId } from "../theory"; import { type IndexedMap, indexMap } from "../util/indexing"; -import { type ModelJudgment, type ModelValidationResult, validateModel } from "./types"; +import { type ModelJudgment, catlogModel } from "./types"; /** A document defining a model. */ export type ModelDocument = { @@ -52,8 +52,14 @@ export type LiveModelDocument = { /** A memo of the double theory that the model is of, if it is defined. */ theory: Accessor; - /** A memo of the result of validation.*/ - validationResult: Accessor; + /** A memo of the model constructed and validated in the core. */ + validatedModel: Accessor; +}; + +/** A validated model as represented in `catlog`. */ +export type ValidatedModel = { + model: DblModel; + result: ModelValidationResult; }; export function enlivenModelDocument( @@ -95,10 +101,20 @@ export function enlivenModelDocument( if (doc.theory !== undefined) return theories.get(doc.theory); }); - const validationResult = createMemo(() => { - const th = theory(); - return th ? validateModel(th.theory, formalJudgments()) : undefined; - }); + const validatedModel = createMemo( + () => { + const th = theory(); + if (th?.theory.kind !== "Discrete") { + // TODO: Currently only implemented for discrete theories. + return undefined; + } + const model = catlogModel(th.theory, formalJudgments()); + const result = model.validate(); + return { model, result }; + }, + undefined, + { equals: false }, + ); return { refId, @@ -107,6 +123,6 @@ export function enlivenModelDocument( objectIndex, morphismIndex, theory, - validationResult, + validatedModel, }; } diff --git a/packages/frontend/src/model/morphism_cell_editor.tsx b/packages/frontend/src/model/morphism_cell_editor.tsx index 65e90942b..c6419a9ec 100644 --- a/packages/frontend/src/model/morphism_cell_editor.tsx +++ b/packages/frontend/src/model/morphism_cell_editor.tsx @@ -1,8 +1,9 @@ -import { createEffect, useContext } from "solid-js"; +import { createSignal, useContext } from "solid-js"; import invariant from "tiny-invariant"; import { InlineInput } from "../components"; import type { CellActions } from "../notebook"; +import { focusInputWhen } from "../util/focus"; import { LiveModelContext } from "./context"; import { obClasses } from "./object_cell_editor"; import { ObInput } from "./object_input"; @@ -19,16 +20,10 @@ export function MorphismCellEditor(props: { isActive: boolean; actions: CellActions; }) { - let nameRef!: HTMLInputElement; + const [nameRef, setNameRef] = createSignal(); let domRef!: HTMLInputElement; let codRef!: HTMLInputElement; - - createEffect(() => { - if (props.isActive) { - nameRef.focus(); - nameRef.selectionStart = nameRef.selectionEnd = nameRef.value.length; - } - }); + focusInputWhen(nameRef, () => props.isActive); const liveModel = useContext(LiveModelContext); invariant(liveModel, "Live model should be provided as context"); @@ -47,12 +42,12 @@ export function MorphismCellEditor(props: { ]; const arrowClass = () => arrowStyles[morTypeMeta()?.arrowStyle ?? "default"]; - const morphismErrors = () => { - const result = liveModel.validationResult(); - if (result?.tag !== "errors") { + const errors = () => { + const validated = liveModel.validatedModel(); + if (validated?.result.tag !== "Err") { return []; } - return result.errors.get(props.morphism.id) ?? []; + return validated.result.content.filter((err) => err.content === props.morphism.id); }; return ( @@ -68,20 +63,18 @@ export function MorphismCellEditor(props: { }); }} obType={domType()} - invalid={morphismErrors().some( - (err) => err.tag === "Dom" || err.tag === "DomType", - )} - deleteForward={() => nameRef.focus()} - exitBackward={() => nameRef.focus()} + invalid={errors().some((err) => err.tag === "Dom" || err.tag === "DomType")} + deleteForward={() => nameRef()?.focus()} + exitBackward={() => nameRef()?.focus()} exitForward={() => codRef.focus()} - exitRight={() => nameRef.focus()} + exitRight={() => nameRef()?.focus()} onFocus={props.actions.hasFocused} />
{ @@ -115,13 +108,11 @@ export function MorphismCellEditor(props: { }); }} obType={codType()} - invalid={morphismErrors().some( - (err) => err.tag === "Cod" || err.tag === "CodType", - )} - deleteBackward={() => nameRef.focus()} + invalid={errors().some((err) => err.tag === "Cod" || err.tag === "CodType")} + deleteBackward={() => nameRef()?.focus()} exitBackward={() => domRef.focus()} exitForward={props.actions.activateBelow} - exitLeft={() => nameRef.focus()} + exitLeft={() => nameRef()?.focus()} onFocus={props.actions.hasFocused} />
diff --git a/packages/frontend/src/model/morphism_input.tsx b/packages/frontend/src/model/morphism_input.tsx index d38114ebe..332fede0c 100644 --- a/packages/frontend/src/model/morphism_input.tsx +++ b/packages/frontend/src/model/morphism_input.tsx @@ -19,10 +19,8 @@ export function BasicMorInput( const liveModel = useContext(LiveModelContext); invariant(liveModel, "Live model should be provided as context"); - const completions = (): Mor[] | undefined => { - const result = liveModel.validationResult(); - return props.morType && result && result.model.morphismsWithType(props.morType); - }; + const completions = (): Mor[] | undefined => + props.morType && liveModel.validatedModel()?.model.morphismsWithType(props.morType); return ( { - if (props.isActive) { - nameRef.focus(); - nameRef.selectionStart = nameRef.selectionEnd = nameRef.value.length; - } - }); + const [nameRef, setNameRef] = createSignal(); + focusInputWhen(nameRef, () => props.isActive); const liveModel = useContext(LiveModelContext); invariant(liveModel, "Live model should be provided as context"); @@ -39,7 +34,7 @@ export function ObjectCellEditor(props: { return (
{ diff --git a/packages/frontend/src/model/object_input.tsx b/packages/frontend/src/model/object_input.tsx index c186672b3..3696f3b16 100644 --- a/packages/frontend/src/model/object_input.tsx +++ b/packages/frontend/src/model/object_input.tsx @@ -35,10 +35,8 @@ function BasicObInput(allProps: ObInputProps & IdInputOptions) { const liveModel = useContext(LiveModelContext); invariant(liveModel, "Live model should be provided as context"); - const completions = (): Ob[] | undefined => { - const result = liveModel.validationResult(); - return props.obType && result && result.model.objectsWithType(props.obType); - }; + const completions = (): Ob[] | undefined => + props.obType && liveModel.validatedModel()?.model.objectsWithType(props.obType); return ( @@ -70,12 +68,12 @@ function TabulatedMorInput(allProps: ObInputProps & IdInputOptions) { const completions = (): Uuid[] | undefined => { const morType = tabulatedType(); - const result = liveModel.validationResult(); - if (!(morType && result)) { + if (!morType) { return undefined; } - return result.model - .morphismsWithType(morType) + return liveModel + .validatedModel() + ?.model.morphismsWithType(morType) .map((mor) => match(mor) .with( diff --git a/packages/frontend/src/model/types.ts b/packages/frontend/src/model/types.ts index 38338d932..6c09ec7b0 100644 --- a/packages/frontend/src/model/types.ts +++ b/packages/frontend/src/model/types.ts @@ -1,16 +1,7 @@ import { uuidv7 } from "uuidv7"; import { DblModel } from "catlog-wasm"; -import type { - DblTheory, - InvalidDiscreteDblModel, - MorDecl, - MorType, - ObDecl, - ObType, - Uuid, -} from "catlog-wasm"; -import { indexArray } from "../util/indexing"; +import type { DblTheory, MorDecl, MorType, ObDecl, ObType } from "catlog-wasm"; /** A judgment in the definition of a model. @@ -54,8 +45,7 @@ export const newMorphismDecl = (morType: MorType): MorphismDecl => ({ cod: null, }); -/** Construct a `catlog` model from a sequence of model judgments. - */ +/** Construct a `catlog` model from a sequence of model judgments. */ export function catlogModel(theory: DblTheory, judgments: Array): DblModel { const model = new DblModel(theory); for (const judgment of judgments) { @@ -67,40 +57,3 @@ export function catlogModel(theory: DblTheory, judgments: Array): } return model; } - -/** Result of validating a model in the categorical core. */ -export type ModelValidationResult = ValidatedModel | ModelValidationErrors; - -/** A valid model as represented in `catlog`. */ -export type ValidatedModel = { - tag: "validated"; - model: DblModel; -}; - -/** Errors in a model that did not validate. */ -export type ModelValidationErrors = { - tag: "errors"; - model: DblModel; - errors: Map[]>; -}; - -/** Validate a model in the categorical core. */ -export function validateModel( - theory: DblTheory, - judgments: Array, -): ModelValidationResult | undefined { - if (theory.kind !== "Discrete") { - // TODO: Validation should be implemented for all kinds of theories. - return undefined; - } - const model = catlogModel(theory, judgments); - const errs: InvalidDiscreteDblModel[] = model.validate(); - if (errs.length === 0) { - return { tag: "validated", model }; - } - return { - tag: "errors", - model, - errors: indexArray(errs, (err) => err.content), - }; -} diff --git a/packages/frontend/src/notebook/notebook_cell.tsx b/packages/frontend/src/notebook/notebook_cell.tsx index 28bac3762..5854fcc83 100644 --- a/packages/frontend/src/notebook/notebook_cell.tsx +++ b/packages/frontend/src/notebook/notebook_cell.tsx @@ -6,8 +6,9 @@ import { } from "@atlaskit/pragmatic-drag-and-drop/element/adapter"; import type { DocHandle, Prop } from "@automerge/automerge-repo"; import Popover from "@corvu/popover"; +import { createAutofocus } from "@solid-primitives/autofocus"; import type { EditorView } from "prosemirror-view"; -import { type JSX, Show, createEffect, createSignal, onCleanup, onMount } from "solid-js"; +import { type JSX, Show, createEffect, createSignal, onCleanup } from "solid-js"; import { type Completion, @@ -16,6 +17,7 @@ import { InlineInput, RichTextEditor, } from "../components"; +import { focusInputWhen } from "../util/focus"; import type { CellId } from "./types"; import ArrowDown from "lucide-solid/icons/arrow-down"; @@ -235,19 +237,13 @@ export function StemCellEditor(props: { }) { const [text, setText] = createSignal(""); - let ref!: HTMLInputElement; - - onMount(() => ref.focus()); - - createEffect(() => { - if (props.isActive) { - ref.focus(); - } - }); + const [ref, setRef] = createSignal(); + createAutofocus(ref); + focusInputWhen(ref, () => props.isActive); return ( (props: { const addAfterActiveCell = (cell: Cell) => { props.changeNotebook((nb) => { - nb.cells.splice(activeCell() + 1, 0, cell); - setActiveCell(activeCell() + 1); + const i = Math.min(activeCell() + 1, nb.cells.length); + nb.cells.splice(i, 0, cell); + setActiveCell(i); }); }; diff --git a/packages/frontend/src/stdlib/analyses/lotka_volterra.tsx b/packages/frontend/src/stdlib/analyses/lotka_volterra.tsx index 0343843d9..e1f4f338f 100644 --- a/packages/frontend/src/stdlib/analyses/lotka_volterra.tsx +++ b/packages/frontend/src/stdlib/analyses/lotka_volterra.tsx @@ -115,9 +115,9 @@ export function LotkaVolterra( const simulationResult = createMemo( () => { - const result = props.liveModel.validationResult(); - if (result?.tag === "validated") { - return props.simulate(result.model, props.content); + const validated = props.liveModel.validatedModel(); + if (validated?.result.tag === "Ok") { + return props.simulate(validated.model, props.content); } }, undefined, diff --git a/packages/frontend/src/stdlib/analyses/submodel_graphs.tsx b/packages/frontend/src/stdlib/analyses/submodel_graphs.tsx index 8158c5c2e..4bc6eda17 100644 --- a/packages/frontend/src/stdlib/analyses/submodel_graphs.tsx +++ b/packages/frontend/src/stdlib/analyses/submodel_graphs.tsx @@ -41,8 +41,8 @@ function SubmodelsAnalysis( } & ModelAnalysisProps, ) { const submodels = () => { - const res = props.liveModel.validationResult(); - return res?.tag === "validated" ? props.findSubmodels(res.model) : []; + const validated = props.liveModel.validatedModel(); + return validated?.result.tag === "Ok" ? props.findSubmodels(validated.model) : []; }; return ( diff --git a/packages/frontend/src/util/focus.ts b/packages/frontend/src/util/focus.ts new file mode 100644 index 000000000..64579b7d7 --- /dev/null +++ b/packages/frontend/src/util/focus.ts @@ -0,0 +1,16 @@ +import { type Accessor, createEffect } from "solid-js"; + +/** Focus an input component when a condition holds. */ +export function focusInputWhen( + ref: Accessor, + when: Accessor, +) { + createEffect(() => { + const el = ref(); + if (el && when()) { + el.focus(); + // Move cursor to end of input. + el.selectionStart = el.selectionEnd = el.value.length; + } + }); +}