Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
186 changes: 169 additions & 17 deletions packages/catlog-wasm/src/model.rs
Original file line number Diff line number Diff line change
@@ -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;
Expand All @@ -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),
}

Expand All @@ -38,16 +41,24 @@ pub enum Mor {

/// Composite of morphisms.
Composite(Box<Path<Ob, Mor>>),

/// Morphism between tabulated morphisms, a commutative square.
TabulatorSquare {
dom: Box<Mor>,
cod: Box<Mor>,
pre: Box<Mor>,
post: Box<Mor>,
},
}

/// Convert from object in a model of discrete double theory.
/// Convert from an object in a model of discrete double theory.
impl From<Uuid> 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<Path<Uuid, Uuid>> for Mor {
fn from(path: Path<Uuid, Uuid>) -> Self {
if path.len() == 1 {
Expand All @@ -58,7 +69,7 @@ impl From<Path<Uuid, Uuid>> 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<Ob> for Uuid {
type Error = String;

Expand All @@ -70,7 +81,7 @@ impl TryFrom<Ob> 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<Mor> for Path<Uuid, Uuid> {
type Error = String;

Expand All @@ -81,6 +92,107 @@ impl TryFrom<Mor> for Path<Uuid, Uuid> {
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<Ob> for dbl_model::TabOb<Uuid, Uuid> {
type Error = String;

fn try_from(ob: Ob) -> Result<Self, Self::Error> {
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<Mor> for dbl_model::TabMor<Uuid, Uuid> {
type Error = String;

fn try_from(mor: Mor) -> Result<Self, Self::Error> {
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<Mor> for dbl_model::TabEdge<Uuid, Uuid> {
type Error = String;

fn try_from(mor: Mor) -> Result<Self, Self::Error> {
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<dbl_model::TabOb<Uuid, Uuid>> for Ob {
fn from(value: dbl_model::TabOb<Uuid, Uuid>) -> 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<dbl_model::TabMor<Uuid, Uuid>> for Mor {
fn from(path: dbl_model::TabMor<Uuid, Uuid>) -> Self {
if path.len() == 1 {
path.only().unwrap().into()
} else {
Mor::Composite(Box::new(path.map(|ob| ob.into(), |mor| mor.into())))
}
}
}

impl From<dbl_model::TabEdge<Uuid, Uuid>> for Mor {
fn from(value: dbl_model::TabEdge<Uuid, Uuid>) -> 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()),
},
}
}
}
Expand Down Expand Up @@ -116,6 +228,8 @@ pub struct MorDecl {
}

pub(crate) type DiscreteDblModel = dbl_model::DiscreteDblModel<Uuid, UstrFinCategory>;
pub(crate) type DiscreteTabModel =
dbl_model::DiscreteTabModel<Uuid, Ustr, BuildHasherDefault<IdentityHasher>>;

/** A box containing a model of a double theory of any kind.

Expand All @@ -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.
Expand All @@ -139,15 +253,15 @@ 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(),
})
}

/// Adds an object to the model.
#[wasm_bindgen(js_name = "addOb")]
pub fn add_ob(&mut self, decl: ObDecl) -> Result<bool, String> {
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))
}
Expand All @@ -158,7 +272,7 @@ impl DblModel {
#[wasm_bindgen(js_name = "addMor")]
pub fn add_mor(&mut self, decl: MorDecl) -> Result<bool, String> {
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()? {
Expand All @@ -176,7 +290,7 @@ impl DblModel {
#[wasm_bindgen(js_name = "hasOb")]
pub fn has_ob(&self, ob: Ob) -> Result<bool, String> {
all_the_same!(match &self.0 {
DblModelBox::[Discrete](model) => {
DblModelBox::[Discrete, DiscreteTab](model) => {
let ob = ob.try_into()?;
Ok(model.has_ob(&ob))
}
Expand All @@ -187,7 +301,7 @@ impl DblModel {
#[wasm_bindgen(js_name = "hasMor")]
pub fn has_mor(&self, mor: Mor) -> Result<bool, String> {
all_the_same!(match &self.0 {
DblModelBox::[Discrete](model) => {
DblModelBox::[Discrete, DiscreteTab](model) => {
let mor = mor.try_into()?;
Ok(model.has_mor(&mor))
}
Expand All @@ -198,23 +312,23 @@ impl DblModel {
#[wasm_bindgen]
pub fn objects(&self) -> Vec<Ob> {
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()
})
}

/// Returns array of all basic morphisms in the model.
#[wasm_bindgen]
pub fn morphisms(&self) -> Vec<Mor> {
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()
})
}

/// Returns array of basic objects with the given type.
#[wasm_bindgen(js_name = "objectsWithType")]
pub fn objects_with_type(&self, ob_type: ObType) -> Result<Vec<Ob>, 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())
}
Expand All @@ -225,7 +339,7 @@ impl DblModel {
#[wasm_bindgen(js_name = "morphismsWithType")]
pub fn morphisms_with_type(&self, mor_type: MorType) -> Result<Vec<Mor>, 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())
}
Expand All @@ -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())
}
Expand Down Expand Up @@ -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(()));
}
}
12 changes: 8 additions & 4 deletions packages/catlog-wasm/src/model_diagram.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -58,6 +58,7 @@ pub struct DiagramMorDecl {
#[derive(From)]
pub enum DblModelDiagramBox {
Discrete(diagram::DblModelDiagram<DiscreteDblModelMapping, DiscreteDblModel>),
// DiscreteTab(), # TODO: Not implemented.
}

/// Wasm bindings for a diagram in a model of a double theory.
Expand All @@ -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.
Expand Down
Loading
Loading