ENH: added theory and model

Author: quffaro

packages/catlog/src/stdlib/models.rs

@@ -1,7 +1,7 @@
 //! Standard library of models of double theories.
 
 use std::rc::Rc;
-use ustr::{Ustr, ustr};
+use ustr::{ustr, Ustr};
 
 use crate::dbl::{model::*, theory::*};
 use crate::one::Path;
@@ -141,6 +141,41 @@ pub fn catalyzed_reaction(th: Rc<UstrModalDblTheory>) -> UstrModalDblModel {
     model
 }
 
+/**
+ */
+pub fn water(th: Rc<UstrModalDblTheory>) -> UstrModalDblModel {
+    let (state_type, aux_type) =
+        (ModalObType::new(ustr("State")), ModalObType::new(ustr("Auxiliary")));
+    let mut model = UstrModalDblModel::new(th);
+    let (water, container) = (ustr("water"), ustr("container"));
+    model.add_ob(water, state_type.clone());
+    model.add_ob(container, state_type.clone());
+    let (bwater, bcontainer) = (ustr("&water"), ustr("&container"));
+    model.add_ob(bwater, aux_type.clone());
+    model.add_ob(bcontainer, aux_type);
+    let borrow = ModalMorType::One(ModeApp::new(ustr("borrow")));
+    model.add_mor(
+        ustr("borrow1"),
+        ModalOb::Generator(water),
+        ModalOb::Generator(bwater),
+        borrow.clone(),
+    );
+    model.add_mor(
+        ustr("borrow2"),
+        ModalOb::Generator(container),
+        ModalOb::Generator(bcontainer),
+        borrow,
+    );
+    let (comparator, comparator_out) = (ustr("comparator"), ustr("comparator_out"));
+    model.add_mor(
+        comparator,
+        ModalOb::List(List::Plain, vec![bwater.into(), bcontainer.into()]).into(),
+        ModalOb::Generator(comparator_out),
+        ModalMorType::One(ModeApp::new(ustr("function"))),
+    );
+    model
+}
+
 #[cfg(test)]
 mod tests {
     use super::super::theories::*;

packages/catlog/src/stdlib/theories.rs

@@ -3,7 +3,7 @@
 use ustr::ustr;
 
 use crate::dbl::theory::*;
-use crate::one::{Path, fp_category::UstrFpCategory};
+use crate::one::{fp_category::UstrFpCategory, Path};
 
 /** The empty theory, which has a single model, the empty model.
 
@@ -151,6 +151,11 @@ pub fn th_sym_monoidal_category() -> UstrModalDblTheory {
     th_list_algebra(List::Symmetric)
 }
 
+///
+pub fn th_modal_state_aux() -> UstrModalDblTheory {
+    th_modal_sf(List::Plain)
+}
+
 /** The theory of a strict algebra of a list monad.
 
 This is a modal double theory, parametric over which variant of the double list
@@ -194,6 +199,22 @@ fn th_list_lax_algebra(list: List) -> UstrModalDblTheory {
     th
 }
 
+///
+fn th_modal_sf(list: List) -> UstrModalDblTheory {
+    let m = Modality::List(list);
+    let mut th: UstrModalDblTheory = Default::default();
+    let (state, aux) = (ustr("State"), ustr("Auxiliary"));
+    th.add_ob_type(state);
+    th.add_ob_type(aux);
+    let function = ustr("function");
+    th.add_mor_type(function, ModeApp::new(aux).apply(m), ModeApp::new(aux));
+    let (borrow, outpos, outneg) = (ustr("borrow"), ustr("out-pos"), ustr("out-neg"));
+    th.add_mor_type(borrow, ModeApp::new(state), ModeApp::new(aux));
+    th.add_mor_type(outpos, ModeApp::new(aux), ModeApp::new(state));
+    th.add_mor_type(outneg, ModeApp::new(aux), ModeApp::new(state));
+    th
+}
+
 #[cfg(test)]
 mod tests {
     use super::*;
@@ -221,6 +242,7 @@ mod tests {
     fn validate_modal_theories() {
         assert!(th_monoidal_category().validate().is_ok());
         assert!(th_lax_monoidal_category().validate().is_ok());
+        assert!(th_modal_state_aux().validate().is_ok());
     }
 
     #[test]