diff --git a/packages/catlog/src/dbl/mod.rs b/packages/catlog/src/dbl/mod.rs index 0439d3993..d861bcbf5 100644 --- a/packages/catlog/src/dbl/mod.rs +++ b/packages/catlog/src/dbl/mod.rs @@ -5,5 +5,6 @@ pub mod diagram; pub mod pasting; pub mod model; +pub mod model_diagram; pub mod model_morphism; pub mod theory; diff --git a/packages/catlog/src/dbl/model_diagram.rs b/packages/catlog/src/dbl/model_diagram.rs new file mode 100644 index 000000000..14d55abc4 --- /dev/null +++ b/packages/catlog/src/dbl/model_diagram.rs @@ -0,0 +1,165 @@ +/*! Diagrams in models of a double theory. + +A diagram in a [model](super::model) consists of a [morphism](super::model_morphism) +of models together with its domain, which is a free mode. + +Diagrams are currently used primarily to represent instances of models from +a fibered perspective. + +# References + +- TODO dev-docs + */ + +use std::hash::Hash; + +use nonempty::NonEmpty; +use thiserror::Error; + +use super::model::DiscreteDblModel; +use super::model_morphism::{DblModelMapping, DiscreteDblModelMapping}; +use crate::one::*; +use crate::validate::{self, Validate}; + +/** A diagram in a model of a double theory defined by a [mapping](DblModelMapping). + +This struct owns its data, namely, the domain model and the model +mapping. The domain is assumed to +be a valid model of a double theory. If that is in question, the +model should be validated *before* validating this object. +*/ +pub struct DblModelDiagram(pub Map, pub Dom); + +/// A diagram in a model of a discrete double theory. +pub type DiscreteDblModelDiagram = + DblModelDiagram, DiscreteDblModel>; + +impl DiscreteDblModelDiagram +where + DomId: Eq + Clone + Hash, + CodId: Eq + Clone + Hash, + Cat: FgCategory, + Cat::Ob: Hash, + Cat::Mor: Hash, +{ + /// The domain of the diagram. + pub fn domain(&self) -> &DiscreteDblModel { + &self.1 + } + + /// The mapping of the diagram. + pub fn mapping(&self) -> &DiscreteDblModelMapping { + &self.0 + } +} + +/** An invalid assignment in a double model diagram defined explicitly by data. + * + * Note that, by specifying a model morphism via its action on generators, we + * 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)] +pub enum InvalidDblModelDiagram { + /// Missing data + #[error("Object `{0}` is not mapped to anything in the codomain")] + MissingOb(Ob), + + /// Missing data + #[error("Morphism `{0}` is not mapped to anything in the codomain")] + MissingMor(Mor), +} + +impl Validate for DiscreteDblModelDiagram +where + DomId: Eq + Clone + Hash, + CodId: Eq + Clone + Hash, + Cat: FgCategory, + Cat::Ob: Hash, + Cat::Mor: Hash, +{ + type ValidationError = InvalidDblModelDiagram; + + fn validate(&self) -> Result<(), NonEmpty> { + validate::wrap_errors(self.iter_invalid()) + } +} + +impl DiscreteDblModelDiagram +where + DomId: Eq + Clone + Hash, + CodId: Eq + Clone + Hash, + Cat: FgCategory, + Cat::Ob: Hash, + Cat::Mor: Hash, +{ + /// An iterator over invalid objects and morphisms in the diagram. + pub fn iter_invalid(&self) -> impl Iterator> + '_ { + let DblModelDiagram(mapping, dom) = self; + + // Diagrams can always be indexed by free models. + assert!(dom.is_free(), "Domain model should be free"); + let ob_errors = dom.object_generators().filter_map(|v| { + if mapping.apply_ob(&v).is_some() { + None + } else { + Some(InvalidDblModelDiagram::MissingOb(v)) + } + }); + + let mor_errors = dom.morphism_generators().flat_map(|f| { + if mapping.apply_basic_mor(&f).is_some() { + vec![] // No errors + } else { + [InvalidDblModelDiagram::MissingMor(f)].to_vec() + } + }); + + ob_errors.chain(mor_errors) + } +} + +#[cfg(test)] +mod tests { + use super::*; + + use std::sync::Arc; + use ustr::ustr; + + use crate::one::fin_category::FinMor; + use crate::stdlib::*; + + #[test] + fn discrete_model_diagram() { + let th = Arc::new(th_schema()); + let mut model = DiscreteDblModel::new(th.clone()); + let entity = ustr("entity"); + model.add_ob(entity, ustr("Entity")); + model.add_ob(ustr("type"), ustr("AttrType")); + model.add_mor(ustr("a"), entity, ustr("type"), FinMor::Generator(ustr("Attr"))); + + let mut f: DiscreteDblModelMapping<_, _> = Default::default(); + f.assign_ob(entity, 'x'); + f.assign_ob(ustr("type"), 'y'); + f.assign_basic_mor(ustr("a"), Path::pair('p', 'q')); + + let diagram = DblModelDiagram(f.clone(), model.clone()); + assert_eq!(diagram.domain(), &model); + assert_eq!(diagram.mapping(), &f); + } + + #[test] + fn validate_model_diagram() { + let theory = Arc::new(th_signed_category()); + let negloop = negative_loop(theory.clone()); + + let mut f: DiscreteDblModelMapping<_, _> = Default::default(); + f.assign_ob(ustr("x"), ustr("x")); + f.assign_basic_mor(ustr(""), Path::Id(ustr("negative"))); + let dmd = DblModelDiagram(f, negloop); + assert!(dmd.validate().is_err()); + // A bad map from h to itself that is wrong for the ob (it is in the map + // but sent to something that doesn't exist) and for the hom generator + // (not in the map) + } +} diff --git a/packages/catlog/src/dbl/model_morphism.rs b/packages/catlog/src/dbl/model_morphism.rs index 745b0a49e..4850f60f8 100644 --- a/packages/catlog/src/dbl/model_morphism.rs +++ b/packages/catlog/src/dbl/model_morphism.rs @@ -349,7 +349,7 @@ where } } -impl<'a, DomId, CodId, Cat> Validate for DiscreteDblModelMorphism<'a, DomId, CodId, Cat> +impl Validate for DiscreteDblModelMorphism<'_, DomId, CodId, Cat> where DomId: Eq + Clone + Hash, CodId: Eq + Clone + Hash, diff --git a/packages/catlog/src/simulate/mathexpr/pprint.rs b/packages/catlog/src/simulate/mathexpr/pprint.rs index cce68c2e6..5c407e3ef 100644 --- a/packages/catlog/src/simulate/mathexpr/pprint.rs +++ b/packages/catlog/src/simulate/mathexpr/pprint.rs @@ -18,7 +18,7 @@ impl<'a, 'b, T: DisplayWithSource> WithSource<'a, 'b, T> { } } -impl<'a, 'b, T> fmt::Display for WithSource<'a, 'b, T> +impl fmt::Display for WithSource<'_, '_, T> where T: DisplayWithSource, {