diff --git a/packages/catlog-wasm/src/model.rs b/packages/catlog-wasm/src/model.rs index 4979822ed..4725b1f62 100644 --- a/packages/catlog-wasm/src/model.rs +++ b/packages/catlog-wasm/src/model.rs @@ -1,14 +1,17 @@ //! Wasm bindings for models of double theories. +use std::hash::BuildHasherDefault; + use all_the_same::all_the_same; use derive_more::{From, TryInto}; +use ustr::{IdentityHasher, Ustr}; use uuid::Uuid; use serde::{Deserialize, Serialize}; use tsify_next::Tsify; use wasm_bindgen::prelude::*; -use catlog::dbl::model::{self as dbl_model, FgDblModel, InvalidDblModel}; +use catlog::dbl::model::{self as dbl_model, FgDblModel, InvalidDblModel, MutDblModel}; use catlog::one::fin_category::UstrFinCategory; use catlog::one::{Category as _, FgCategory, Path}; use catlog::validate::Validate; @@ -24,7 +27,7 @@ pub enum Ob { /// Basic or generating object. Basic(Uuid), - /// A morphism viewed as an object of a tabulator. + /// Morphism viewed as an object of a tabulator. Tabulated(Mor), } @@ -38,16 +41,24 @@ pub enum Mor { /// Composite of morphisms. Composite(Box>), + + /// Morphism between tabulated morphisms, a commutative square. + TabulatorSquare { + dom: Box, + cod: Box, + pre: Box, + post: Box, + }, } -/// Convert from object in a model of discrete double theory. +/// Convert from an object in a model of discrete double theory. impl From for Ob { fn from(value: Uuid) -> Self { Ob::Basic(value) } } -/// Convert from morphism in a model of a discrete double theory. +/// Convert from a morphism in a model of a discrete double theory. impl From> for Mor { fn from(path: Path) -> Self { if path.len() == 1 { @@ -58,7 +69,7 @@ impl From> for Mor { } } -/// Convert into object in a model of a discrete double theory. +/// Convert into an object in a model of a discrete double theory. impl TryFrom for Uuid { type Error = String; @@ -70,7 +81,7 @@ impl TryFrom for Uuid { } } -/// Convert into morphism in a model of a discrete double theory. +/// Convert into a morphism in a model of a discrete double theory. impl TryFrom for Path { type Error = String; @@ -81,6 +92,107 @@ impl TryFrom for Path { let result_path = (*path).try_map(|ob| ob.try_into(), |mor| mor.try_into()); result_path.map(|path| path.flatten()) } + _ => Err(format!("Cannot cast morphism for discrete double theory: {:#?}", mor)), + } + } +} + +/// Convert into an object in a model of a discrete tabulator theory. +impl TryFrom for dbl_model::TabOb { + type Error = String; + + fn try_from(ob: Ob) -> Result { + match ob { + Ob::Basic(id) => Ok(dbl_model::TabOb::Basic(id)), + Ob::Tabulated(f) => Ok(dbl_model::TabOb::Tabulated(Box::new(f.try_into()?))), + } + } +} + +/// Convert into a morphism in a model of a discrete tabulator theory. +impl TryFrom for dbl_model::TabMor { + type Error = String; + + fn try_from(mor: Mor) -> Result { + match mor { + Mor::Basic(id) => Ok(Path::single(dbl_model::TabEdge::Basic(id))), + Mor::Composite(path) => { + let result_path = (*path).try_map(|ob| ob.try_into(), |mor| mor.try_into()); + result_path.map(|path| path.flatten()) + } + Mor::TabulatorSquare { + dom, + cod, + pre, + post, + } => Ok(Path::single(dbl_model::TabEdge::Square { + dom: Box::new((*dom).try_into()?), + cod: Box::new((*cod).try_into()?), + pre: Box::new((*pre).try_into()?), + post: Box::new((*post).try_into()?), + })), + } + } +} + +impl TryFrom for dbl_model::TabEdge { + type Error = String; + + fn try_from(mor: Mor) -> Result { + match mor { + Mor::Basic(id) => Ok(dbl_model::TabEdge::Basic(id)), + Mor::TabulatorSquare { + dom, + cod, + pre, + post, + } => Ok(dbl_model::TabEdge::Square { + dom: Box::new((*dom).try_into()?), + cod: Box::new((*cod).try_into()?), + pre: Box::new((*pre).try_into()?), + post: Box::new((*post).try_into()?), + }), + _ => Err(format!("Cannot cast morphism for discrete tabulator theory: {:#?}", mor)), + } + } +} + +/// Convert from an object in a model of a discrete tabulator theory. +impl From> for Ob { + fn from(value: dbl_model::TabOb) -> Self { + match value { + dbl_model::TabOb::Basic(x) => Ob::Basic(x), + dbl_model::TabOb::Tabulated(f) => Ob::Tabulated((*f).into()), + } + } +} + +/// Convert from a morphism in a model of a discrete tabulator theory. +impl From> for Mor { + fn from(path: dbl_model::TabMor) -> Self { + if path.len() == 1 { + path.only().unwrap().into() + } else { + Mor::Composite(Box::new(path.map(|ob| ob.into(), |mor| mor.into()))) + } + } +} + +impl From> for Mor { + fn from(value: dbl_model::TabEdge) -> Self { + match value { + dbl_model::TabEdge::Basic(f) => Mor::Basic(f), + dbl_model::TabEdge::Square { + dom, + cod, + pre, + post, + } => Mor::TabulatorSquare { + dom: Box::new((*dom).into()), + cod: Box::new((*cod).into()), + pre: Box::new((*pre).into()), + post: Box::new((*post).into()), + }, } } } @@ -116,6 +228,8 @@ pub struct MorDecl { } pub(crate) type DiscreteDblModel = dbl_model::DiscreteDblModel; +pub(crate) type DiscreteTabModel = + dbl_model::DiscreteTabModel>; /** A box containing a model of a double theory of any kind. @@ -125,7 +239,7 @@ See [`DblTheoryBox`] for motivation. #[try_into(ref)] pub enum DblModelBox { Discrete(DiscreteDblModel), - // DiscreteTab(()), // TODO: Not yet implemented. + DiscreteTab(DiscreteTabModel), } /// Wasm bindings for a model of a double theory. @@ -139,7 +253,7 @@ impl DblModel { pub fn new(theory: &DblTheory) -> Self { Self(match &theory.0 { DblTheoryBox::Discrete(th) => DiscreteDblModel::new(th.clone()).into(), - DblTheoryBox::DiscreteTab(_) => panic!("Not implemented"), + DblTheoryBox::DiscreteTab(th) => DiscreteTabModel::new(th.clone()).into(), }) } @@ -147,7 +261,7 @@ impl DblModel { #[wasm_bindgen(js_name = "addOb")] pub fn add_ob(&mut self, decl: ObDecl) -> Result { all_the_same!(match &mut self.0 { - DblModelBox::[Discrete](model) => { + DblModelBox::[Discrete, DiscreteTab](model) => { let ob_type = decl.ob_type.try_into()?; Ok(model.add_ob(decl.id, ob_type)) } @@ -158,7 +272,7 @@ impl DblModel { #[wasm_bindgen(js_name = "addMor")] pub fn add_mor(&mut self, decl: MorDecl) -> Result { all_the_same!(match &mut self.0 { - DblModelBox::[Discrete](model) => { + DblModelBox::[Discrete, DiscreteTab](model) => { 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()? { @@ -176,7 +290,7 @@ impl DblModel { #[wasm_bindgen(js_name = "hasOb")] pub fn has_ob(&self, ob: Ob) -> Result { all_the_same!(match &self.0 { - DblModelBox::[Discrete](model) => { + DblModelBox::[Discrete, DiscreteTab](model) => { let ob = ob.try_into()?; Ok(model.has_ob(&ob)) } @@ -187,7 +301,7 @@ impl DblModel { #[wasm_bindgen(js_name = "hasMor")] pub fn has_mor(&self, mor: Mor) -> Result { all_the_same!(match &self.0 { - DblModelBox::[Discrete](model) => { + DblModelBox::[Discrete, DiscreteTab](model) => { let mor = mor.try_into()?; Ok(model.has_mor(&mor)) } @@ -198,7 +312,7 @@ impl DblModel { #[wasm_bindgen] pub fn objects(&self) -> Vec { all_the_same!(match &self.0 { - DblModelBox::[Discrete](model) => model.objects().map(|x| x.into()).collect() + DblModelBox::[Discrete, DiscreteTab](model) => model.objects().map(|x| x.into()).collect() }) } @@ -206,7 +320,7 @@ impl DblModel { #[wasm_bindgen] pub fn morphisms(&self) -> Vec { all_the_same!(match &self.0 { - DblModelBox::[Discrete](model) => model.morphisms().map(|f| f.into()).collect() + DblModelBox::[Discrete, DiscreteTab](model) => model.morphisms().map(|f| f.into()).collect() }) } @@ -214,7 +328,7 @@ impl DblModel { #[wasm_bindgen(js_name = "objectsWithType")] pub fn objects_with_type(&self, ob_type: ObType) -> Result, String> { all_the_same!(match &self.0 { - DblModelBox::[Discrete](model) => { + DblModelBox::[Discrete, DiscreteTab](model) => { let ob_type = ob_type.try_into()?; Ok(model.objects_with_type(&ob_type).map(|ob| ob.into()).collect()) } @@ -225,7 +339,7 @@ impl DblModel { #[wasm_bindgen(js_name = "morphismsWithType")] pub fn morphisms_with_type(&self, mor_type: MorType) -> Result, String> { all_the_same!(match &self.0 { - DblModelBox::[Discrete](model) => { + DblModelBox::[Discrete, DiscreteTab](model) => { let mor_type = mor_type.try_into()?; Ok(model.morphisms_with_type(&mor_type).map(|mor| mor.into()).collect()) } @@ -236,7 +350,7 @@ impl DblModel { #[wasm_bindgen] pub fn validate(&self) -> ModelValidationResult { all_the_same!(match &self.0 { - DblModelBox::[Discrete](model) => { + DblModelBox::[Discrete, DiscreteTab](model) => { let res = model.validate(); ModelValidationResult(res.map_err(|errs| errs.into()).into()) } @@ -311,4 +425,42 @@ pub(crate) mod tests { }; assert_eq!(errs.len(), 2); } + + #[test] + fn model_category_links() { + let th = ThCategoryLinks::new().theory(); + let mut model = DblModel::new(&th); + let [f, x, y, link] = [Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()]; + assert!(model + .add_ob(ObDecl { + id: x, + ob_type: ObType::Basic("Object".into()), + }) + .is_ok()); + assert!(model + .add_ob(ObDecl { + id: y, + ob_type: ObType::Basic("Object".into()), + }) + .is_ok()); + assert!(model + .add_mor(MorDecl { + id: f, + mor_type: MorType::Hom(Box::new(ObType::Basic("Object".into()))), + dom: Some(Ob::Basic(x)), + cod: Some(Ob::Basic(y)), + }) + .is_ok()); + assert!(model + .add_mor(MorDecl { + id: link, + mor_type: MorType::Basic("Link".into()), + dom: Some(Ob::Basic(x)), + cod: Some(Ob::Tabulated(Mor::Basic(f))), + }) + .is_ok()); + assert_eq!(model.objects().len(), 2); + assert_eq!(model.morphisms().len(), 2); + assert_eq!(model.validate().0, JsResult::Ok(())); + } } diff --git a/packages/catlog-wasm/src/model_diagram.rs b/packages/catlog-wasm/src/model_diagram.rs index 33a8f160b..7ae47bbd8 100644 --- a/packages/catlog-wasm/src/model_diagram.rs +++ b/packages/catlog-wasm/src/model_diagram.rs @@ -8,7 +8,7 @@ use serde::{Deserialize, Serialize}; use tsify_next::Tsify; use wasm_bindgen::prelude::*; -use catlog::dbl::model::FgDblModel; +use catlog::dbl::model::{FgDblModel, MutDblModel}; use catlog::dbl::model_diagram as diagram; use catlog::dbl::model_morphism::DblModelMapping; use catlog::one::FgCategory; @@ -58,6 +58,7 @@ pub struct DiagramMorDecl { #[derive(From)] pub enum DblModelDiagramBox { Discrete(diagram::DblModelDiagram), + // DiscreteTab(), # TODO: Not implemented. } /// Wasm bindings for a diagram in a model of a double theory. @@ -70,12 +71,15 @@ impl DblModelDiagram { #[wasm_bindgen(constructor)] pub fn new(theory: &DblTheory) -> Self { let model = DblModel::new(theory); - Self(all_the_same!(match model.0 { - DblModelBox::[Discrete](model) => { + Self(match model.0 { + DblModelBox::Discrete(model) => { let mapping = Default::default(); diagram::DblModelDiagram(mapping, model).into() } - })) + DblModelBox::DiscreteTab(_) => { + panic!("Diagrams not implemented for tabulator theories") + } + }) } /// Adds an object to the diagram. diff --git a/packages/catlog/src/dbl/model.rs b/packages/catlog/src/dbl/model.rs index b864d22ed..72150eb8c 100644 --- a/packages/catlog/src/dbl/model.rs +++ b/packages/catlog/src/dbl/model.rs @@ -119,7 +119,7 @@ pub trait DblModel: Category { fn mor_act(&self, m: Self::Mor, α: &Self::MorOp) -> Self::Mor; } -/// A finitely-generated model of a double theory. +/// A finitely generated model of a double theory. pub trait FgDblModel: DblModel + FgCategory { /// Type of an object generator. fn ob_generator_type(&self, ob: &Self::ObGen) -> Self::ObType; @@ -151,6 +151,41 @@ pub trait FgDblModel: DblModel + FgCategory { } } +/// A mutable, finitely generated model of a double theory. +pub trait MutDblModel: FgDblModel { + /// Adds a basic object to the model. + fn add_ob(&mut self, x: Self::ObGen, ob_type: Self::ObType) -> bool; + + /// Adds a basic morphism to the model. + fn add_mor( + &mut self, + f: Self::MorGen, + dom: Self::Ob, + cod: Self::Ob, + mor_type: Self::MorType, + ) -> bool { + let is_new = self.make_mor(f.clone(), mor_type); + self.set_dom(f.clone(), dom); + self.set_cod(f, cod); + is_new + } + + /// Adds a basic morphism to the model without setting its (co)domain. + fn make_mor(&mut self, f: Self::MorGen, mor_type: Self::MorType) -> bool; + + /// Gets the domain of a basic morphism, if it is set. + fn get_dom(&self, f: &Self::MorGen) -> Option<&Self::Ob>; + + /// Gets the codomain of a basic morphism, if it is set. + fn get_cod(&self, f: &Self::MorGen) -> Option<&Self::Ob>; + + /// Sets the domain of a basic morphism. + fn set_dom(&mut self, f: Self::MorGen, x: Self::Ob) -> Option; + + /// Sets the codomain of a basic morphism. + fn set_cod(&mut self, f: Self::MorGen, x: Self::Ob) -> Option; +} + /** A finitely presented model of a discrete double theory. Since discrete double theory has only identity operations, such a model is a @@ -208,49 +243,11 @@ where self.category.is_free() } - /// Adds a basic object to the model. - pub fn add_ob(&mut self, x: Id, typ: Cat::Ob) -> bool { - self.ob_types.set(x.clone(), typ); - self.category.add_ob_generator(x) - } - - /// Adds a basic morphism to the model. - pub fn add_mor(&mut self, f: Id, dom: Id, cod: Id, typ: Cat::Mor) -> bool { - self.mor_types.set(f.clone(), typ); - self.category.add_mor_generator(f, dom, cod) - } - /// Adds an equation to the model, making it not free. pub fn add_equation(&mut self, key: Id, eq: PathEq) { self.category.add_equation(key, eq); } - /// Adds a basic morphism to the model without setting its (co)domain. - pub fn make_mor(&mut self, f: Id, typ: Cat::Mor) -> bool { - self.mor_types.set(f.clone(), typ); - self.category.make_mor_generator(f) - } - - /// Gets the domain of a basic morphism, if it is set. - pub fn get_dom(&self, f: &Id) -> Option<&Id> { - self.category.get_dom(f) - } - - /// Gets the codomain of a basic morphism, if it is set. - pub fn get_cod(&self, f: &Id) -> Option<&Id> { - self.category.get_cod(f) - } - - /// Sets the domain of a basic morphism. - pub fn set_dom(&mut self, f: Id, x: Id) -> Option { - self.category.set_dom(f, x) - } - - /// Sets the codomain of a basic morphism. - pub fn set_cod(&mut self, f: Id, x: Id) -> Option { - self.category.set_cod(f, x) - } - /// Iterates over failures of model to be well defined. pub fn iter_invalid(&self) -> impl Iterator> + '_ { type Invalid = InvalidDblModel; @@ -423,6 +420,42 @@ where } } +impl MutDblModel for DiscreteDblModel +where + Id: Eq + Clone + Hash, + Cat: FgCategory, + Cat::Ob: Hash, + Cat::Mor: Hash, +{ + fn add_ob(&mut self, x: Id, typ: Cat::Ob) -> bool { + self.ob_types.set(x.clone(), typ); + self.category.add_ob_generator(x) + } + + fn add_mor(&mut self, f: Id, dom: Id, cod: Id, typ: Cat::Mor) -> bool { + self.mor_types.set(f.clone(), typ); + self.category.add_mor_generator(f, dom, cod) + } + + fn make_mor(&mut self, f: Id, typ: Cat::Mor) -> bool { + self.mor_types.set(f.clone(), typ); + self.category.make_mor_generator(f) + } + + fn get_dom(&self, f: &Id) -> Option<&Id> { + self.category.get_dom(f) + } + fn get_cod(&self, f: &Id) -> Option<&Id> { + self.category.get_cod(f) + } + fn set_dom(&mut self, f: Id, x: Id) -> Option { + self.category.set_dom(f, x) + } + fn set_cod(&mut self, f: Id, x: Id) -> Option { + self.category.set_cod(f, x) + } +} + impl Validate for DiscreteDblModel where Id: Eq + Clone + Hash, @@ -507,7 +540,7 @@ pub enum TabEdge { /// Basic morphism between any two objects. Basic(E), - /// Generating morphism between tabulated morphisms, a commuting square. + /// Generating morphism between tabulated morphisms, a commutative square. Square { /// The domain, a tabulated morphism. dom: Box>, @@ -567,9 +600,7 @@ where fn has_edge(&self, edge: &Self::E) -> bool { match edge { TabEdge::Basic(e) => { - self.morphisms.contains(e) - && self.dom.apply(e).map_or(false, |x| self.has_vertex(x)) - && self.cod.apply(e).map_or(false, |x| self.has_vertex(x)) + self.morphisms.contains(e) && self.dom.is_set(e) && self.cod.is_set(e) } TabEdge::Square { dom, @@ -655,26 +686,6 @@ where self.tabulated(Path::single(TabEdge::Basic(f))) } - /// Adds a basic object to the model. - pub fn add_ob(&mut self, x: Id, typ: TabObType) -> bool { - self.ob_types.set(x.clone(), typ); - self.generators.objects.insert(x) - } - - /// Adds a basic morphism to the model. - pub fn add_mor( - &mut self, - f: Id, - dom: TabOb, - cod: TabOb, - typ: TabMorType, - ) -> bool { - self.mor_types.set(f.clone(), typ); - self.generators.dom.set(f.clone(), dom); - self.generators.cod.set(f.clone(), cod); - self.generators.morphisms.insert(f) - } - /// Iterates over failures of model to be well defined. pub fn iter_invalid(&self) -> impl Iterator> + '_ { type Invalid = InvalidDblModel; @@ -839,6 +850,36 @@ where } } +impl MutDblModel for DiscreteTabModel +where + Id: Eq + Clone + Hash, + ThId: Eq + Clone + Hash, + S: BuildHasher, +{ + fn add_ob(&mut self, x: Self::ObGen, ob_type: Self::ObType) -> bool { + self.ob_types.set(x.clone(), ob_type); + self.generators.objects.insert(x) + } + + fn make_mor(&mut self, f: Self::MorGen, mor_type: Self::MorType) -> bool { + self.mor_types.set(f.clone(), mor_type); + self.generators.morphisms.insert(f) + } + + fn get_dom(&self, f: &Self::MorGen) -> Option<&Self::Ob> { + self.generators.dom.apply(f) + } + fn get_cod(&self, f: &Self::MorGen) -> Option<&Self::Ob> { + self.generators.cod.apply(f) + } + fn set_dom(&mut self, f: Self::MorGen, x: Self::Ob) -> Option { + self.generators.dom.set(f, x) + } + fn set_cod(&mut self, f: Self::MorGen, x: Self::Ob) -> Option { + self.generators.cod.set(f, x) + } +} + impl Validate for DiscreteTabModel where Id: Eq + Clone + Hash, diff --git a/packages/catlog/src/dbl/model_diagram.rs b/packages/catlog/src/dbl/model_diagram.rs index ace643d58..758cd2b7f 100644 --- a/packages/catlog/src/dbl/model_diagram.rs +++ b/packages/catlog/src/dbl/model_diagram.rs @@ -24,8 +24,7 @@ use serde::{Deserialize, Serialize}; #[cfg(feature = "serde-wasm")] use tsify_next::{declare, Tsify}; -use super::model::{DiscreteDblModel, InvalidDblModel}; -use super::model_morphism::*; +use super::{model::*, model_morphism::*}; use crate::one::{Category, FgCategory}; use crate::validate; diff --git a/packages/catlog/src/dbl/model_morphism.rs b/packages/catlog/src/dbl/model_morphism.rs index 3a87ccc41..ad4a8f3d7 100644 --- a/packages/catlog/src/dbl/model_morphism.rs +++ b/packages/catlog/src/dbl/model_morphism.rs @@ -36,7 +36,7 @@ use crate::one::*; use crate::validate::{self, Validate}; use crate::zero::{Column, HashColumn, Mapping}; -use super::model::{DblModel, DiscreteDblModel, FgDblModel}; +use super::model::*; /** A mapping between models of a double theory. diff --git a/packages/catlog/src/dbl/theory.rs b/packages/catlog/src/dbl/theory.rs index 366372579..ca315f3b7 100644 --- a/packages/catlog/src/dbl/theory.rs +++ b/packages/catlog/src/dbl/theory.rs @@ -278,7 +278,7 @@ impl Validate for DiscreteDblTheory { } /// Object type in a discrete tabulator theory. -#[derive(Clone, PartialEq, Eq, Hash)] +#[derive(Clone, Debug, PartialEq, Eq, Hash)] pub enum TabObType { /// Basic or generating object type. Basic(V), @@ -288,7 +288,7 @@ pub enum TabObType { } /// Morphism type in a discrete tabulator theory. -#[derive(Clone, PartialEq, Eq, Hash)] +#[derive(Clone, Debug, PartialEq, Eq, Hash)] pub enum TabMorType { /// Basic or generating morphism type. Basic(E), @@ -298,7 +298,7 @@ pub enum TabMorType { } /// Object operation in a discrete tabulator theory. -#[derive(Clone, PartialEq, Eq)] +#[derive(Clone, Debug, PartialEq, Eq)] pub enum TabObOp { /// Identity operation on an object type. Id(TabObType), @@ -311,7 +311,7 @@ pub enum TabObOp { } /// Morphism operation in a discrete tabulator theory. -#[derive(Clone, PartialEq, Eq)] +#[derive(Clone, Debug, PartialEq, Eq)] pub enum TabMorOp { /// Identity operation on a morphism type. Id(TabMorType), @@ -415,32 +415,32 @@ where fn has_ob_type(&self, ob_type: &Self::ObType) -> bool { match ob_type { TabObType::Basic(x) => self.ob_types.contains(x), - TabObType::Tabulator(f) => self.has_mor_type(f.as_ref()), + TabObType::Tabulator(f) => self.has_mor_type(f), } } fn has_mor_type(&self, mor_type: &Self::MorType) -> bool { match mor_type { TabMorType::Basic(e) => self.mor_types.contains(e), - TabMorType::Hom(x) => self.has_ob_type(x.as_ref()), + TabMorType::Hom(x) => self.has_ob_type(x), } } fn src(&self, mor_type: &Self::MorType) -> Self::ObType { match mor_type { TabMorType::Basic(e) => { - self.src.apply(e).expect("Source of morphism type should be defined").clone() + self.src.apply(e).cloned().expect("Source of morphism type should be defined") } - TabMorType::Hom(x) => x.as_ref().clone(), + TabMorType::Hom(x) => (**x).clone(), } } fn tgt(&self, mor_type: &Self::MorType) -> Self::ObType { match mor_type { TabMorType::Basic(e) => { - self.tgt.apply(e).expect("Target of morphism type should be defined").clone() + self.tgt.apply(e).cloned().expect("Target of morphism type should be defined") } - TabMorType::Hom(x) => x.as_ref().clone(), + TabMorType::Hom(x) => (**x).clone(), } } @@ -546,8 +546,12 @@ mod tests { th.add_ob_type('*'); let x = TabObType::Basic('*'); assert!(th.has_ob_type(&x)); - let tab = th.tabulator(th.hom_type(x)); + let tab = th.tabulator(th.hom_type(x.clone())); assert!(th.has_ob_type(&tab)); - assert!(th.has_mor_type(&th.hom_type(tab))); + assert!(th.has_mor_type(&th.hom_type(tab.clone()))); + + th.add_mor_type('m', x, tab); + let m = TabMorType::Basic('m'); + assert!(th.has_mor_type(&m)); } } diff --git a/packages/frontend/src/model/document.ts b/packages/frontend/src/model/document.ts index f3d8765e5..ee42a4e80 100644 --- a/packages/frontend/src/model/document.ts +++ b/packages/frontend/src/model/document.ts @@ -106,13 +106,11 @@ function enlivenModelDocument( const validatedModel = createMemo( () => { const th = theory(); - if (th?.theory.kind !== "Discrete") { - // TODO: Currently only implemented for discrete theories. - return undefined; + if (th) { + const model = toCatlogModel(th.theory, formalJudgments()); + const result = model.validate(); + return { model, result }; } - const model = toCatlogModel(th.theory, formalJudgments()); - const result = model.validate(); - return { model, result }; }, undefined, { equals: false },