UI for editing path equations in schemas and ologs

packages/catlog-wasm/src/model.rs

@@ -19,7 +19,9 @@ use catlog::dbl::{
     },
     theory::{self as dbl_theory, ModalObOp, NonUnital, Unital},
 };
-use catlog::one::{Category as _, FgCategory, Path, QualifiedPath};
+use catlog::one::{
+    Category as _, FgCategory, Path, QualifiedPath, graph_algorithms::bounded_simple_paths_all,
+};
 use catlog::tt::{
     self,
     notebook_elab::{Elaborator as ElaboratorNext, demote_modality, promote_modality},
@@ -584,6 +586,20 @@ impl DblModel {
         })
     }
 
+    /// Lists all simple paths in the model.
+    #[wasm_bindgen(js_name = "listSimplePaths")]
+    pub fn list_simple_paths(&self, max_length: Option<usize>) -> Result<Vec<Mor>, String> {
+        match &self.model {
+            DblModelBox::Discrete(model) => {
+                let graph = model.generating_graph();
+                let paths =
+                    bounded_simple_paths_all(graph, max_length).map(|p| Quoter.quote(&p)).collect();
+                Ok(paths)
+            }
+            _ => Err("listSimplePaths is only supported on discrete double models".into()),
+        }
+    }
+
     /// Gets the human-readable label, if any, for an object generator.
     #[wasm_bindgen(js_name = "obGeneratorLabel")]
     pub fn ob_generator_label(&self, id: &QualifiedName) -> Option<QualifiedLabel> {
@@ -918,4 +934,46 @@ pub(crate) mod tests {
         assert_eq!(model.mor_generators().len(), 2);
         assert_eq!(model.validate().0, JsResult::Ok(()));
     }
+
+    #[test]
+    fn list_simple_paths_basic() {
+        let th = ThSchema::new().theory();
+        let [a, entity, attr_type] = [Uuid::now_v7(), Uuid::now_v7(), Uuid::now_v7()];
+        let model = sch_walking_attr(&th, [a, entity, attr_type]);
+
+        let paths = model.list_simple_paths(None).expect("should succeed");
+
+        // Identity at entity + identity at attr_type + the single morphism `a`.
+        assert_eq!(paths.len(), 3);
+        // The basic morphism appears in the result.
+        assert!(paths.iter().any(|p| matches!(p, Mor::Basic(id) if id == &a.to_string())));
+        // Two identity paths appear in the result.
+        let id_count = paths
+            .iter()
+            .filter(|p| {
+                matches!(
+                    p,
+                    Mor::Composite(boxed) if matches!(boxed.as_ref(), notebook_path::Path::Id(_))
+                )
+            })
+            .count();
+        assert_eq!(id_count, 2);
+
+        // max_length = 0 yields only the two identity paths.
+        let paths_zero = model.list_simple_paths(Some(0)).expect("should succeed");
+        assert_eq!(paths_zero.len(), 2);
+    }
+
+    #[test]
+    fn list_simple_paths_non_discrete() {
+        // Modal theory ⇒ listSimplePaths should error.
+        let th = ThSymMonoidalCategory::new().theory();
+        let model = DblModel::new(&th);
+        let result = model.list_simple_paths(None);
+        let err = result.expect_err("expected error for non-discrete model");
+        assert!(
+            err.contains("only supported on discrete double models"),
+            "unexpected error: {err}"
+        );
+    }
 }

packages/catlog/src/one/graph_algorithms.rs

@@ -93,6 +93,24 @@ where
     maybe_empty_path.into_iter().chain(nonempty_paths)
 }
 
+/// Iterates over all simple paths of bounded length in a finite graph.
+pub fn bounded_simple_paths_all<'a, G>(
+    graph: &'a G,
+    max_length: Option<usize>,
+) -> impl Iterator<Item = Path<G::V, G::E>> + 'a
+where
+    G: FinGraph,
+    G::V: Hash,
+    G::E: Hash,
+{
+    let vertices: Vec<G::V> = graph.vertices().collect();
+    vertices.clone().into_iter().flat_map(move |from| {
+        vertices.clone().into_iter().flat_map(move |to| {
+            bounded_simple_paths(graph, &from.clone(), &to, max_length).collect::<Vec<_>>()
+        })
+    })
+}
+
 /// Arrange all the elements of a finite graph in specialization order.
 ///
 /// The [specialization
@@ -390,6 +408,80 @@ mod tests {
         assert_eq!(paths, target);
     }
 
+    #[test]
+    fn find_simple_paths_all() {
+        // Triangle: edge 0: 0->1, edge 1: 1->2, edge 2: 0->2.
+        let g = SkelGraph::triangle();
+        let paths: Vec<_> = bounded_simple_paths_all(&g, None).collect();
+        let paths_set: HashSet<_> = paths.iter().cloned().collect();
+        let expected: HashSet<_> = HashSet::from([
+            // Identity paths at each vertex.
+            Path::Id(0),
+            Path::Id(1),
+            Path::Id(2),
+            // Non-identity simple paths from 0.
+            Path::single(0),  // 0 -> 1
+            Path::single(2),  // 0 -> 2 (diagonal)
+            Path::pair(0, 1), // 0 -> 1 -> 2
+            // Non-identity simple paths from 1.
+            Path::single(1), /* 1 -> 2
+                              * No non-identity paths from 2 (no out-edges). */
+        ]);
+        assert_eq!(paths_set, expected);
+        // Vertices are visited in order, identity emitted first per vertex.
+        assert_eq!(
+            paths.iter().filter(|p| matches!(p, Path::Id(_))).cloned().collect::<Vec<_>>(),
+            vec![Path::Id(0), Path::Id(1), Path::Id(2)]
+        );
+
+        // max_length restricts edge count, but identity paths at every vertex
+        // are always emitted.
+        // 3 identities only.
+        assert_eq!(bounded_simple_paths_all(&g, Some(0)).count(), 3);
+        // 3 identities + 3 single-edge paths (0->1, 0->2, 1->2).
+        assert_eq!(bounded_simple_paths_all(&g, Some(1)).count(), 6);
+        // ...plus the 0 -> 1 -> 2 pair.
+        assert_eq!(bounded_simple_paths_all(&g, Some(2)).count(), 7);
+
+        // Cycle terminates due to simple-path semantics.
+        let g = SkelGraph::cycle(3);
+        let paths: HashSet<_> = bounded_simple_paths_all(&g, None).collect();
+        let expected: HashSet<_> = HashSet::from([
+            // Identity paths.
+            Path::Id(0),
+            Path::Id(1),
+            Path::Id(2),
+            // From 0: 0, 0;1, 0;1;2.
+            Path::single(0),
+            Path::pair(0, 1),
+            Path::Seq(nonempty![0, 1, 2]),
+            // From 1: 1, 1;2, 1;2;0.
+            Path::single(1),
+            Path::pair(1, 2),
+            Path::Seq(nonempty![1, 2, 0]),
+            // From 2: 2, 2;0, 2;0;1.
+            Path::single(2),
+            Path::pair(2, 0),
+            Path::Seq(nonempty![2, 0, 1]),
+        ]);
+        assert_eq!(paths, expected);
+
+        // Self-loops are simple paths of length 1.
+        let mut g: HashGraph<_, _> = Default::default();
+        assert!(g.add_vertex('x'));
+        assert!(g.add_edge('f', 'x', 'x'));
+        assert!(g.add_edge('g', 'x', 'x'));
+        let paths: HashSet<_> = bounded_simple_paths_all(&g, None).collect();
+        let expected: HashSet<_> = HashSet::from([
+            Path::Id('x'),
+            Path::Seq(nonempty!['f']),
+            Path::Seq(nonempty!['g']),
+            Path::Seq(nonempty!['f', 'g']),
+            Path::Seq(nonempty!['g', 'f']),
+        ]);
+        assert_eq!(paths, expected);
+    }
+
     #[test]
     fn toposorting() {
         let g = SkelGraph::path(5);

packages/document-methods/src/model.ts

@@ -38,6 +38,15 @@ export const newMorphismDecl = (morType: MorType): ModelJudgment & { tag: "morph
     cod: null,
 });
 
+/** Create a new equation declaration. */
+export const newEquationDecl = (): ModelJudgment & { tag: "equation" } => ({
+    tag: "equation",
+    id: v7(),
+    name: "",
+    lhs: null,
+    rhs: null,
+});
+
 /** Create a new instantiation of an existing model. */
 export const newInstantiatedModel = (
     model?: Link | null,

packages/document-types/src/v0/model.rs

@@ -33,7 +33,7 @@ pub enum Mor {
     Basic(String),
 
     /// Composite of morphisms.
-    Composite(Box<Path<Ob, Mor>>),
+    Composite(#[tsify(type = "Path<Ob, Mor>")] Box<Path<Ob, Mor>>),
 
     /// Morphism between tabulated morphisms, a commutative square.
     TabulatorSquare {

packages/frontend/src/model/editors.ts

@@ -1,7 +1,7 @@
 import type { Component } from "solid-js";
 
 import type { FocusHandle } from "catcolab-ui-components";
-import type { MorDecl, ObDecl } from "catlog-wasm";
+import type { EqnDecl, MorDecl, ObDecl } from "catlog-wasm";
 import type { CellActions } from "../notebook";
 import type { Theory } from "../theory";
 import type { MorTypeMap, ObTypeMap } from "../theory/types";
@@ -33,3 +33,12 @@ export type MorphismEditorProps = {
     actions: CellActions;
     theory: Theory;
 };
+
+/** Props for an equation cell editor component in a model. */
+export type EquationEditorProps = {
+    equation: EqnDecl;
+    modifyEquation: (f: (decl: EqnDecl) => void) => void;
+    focus: FocusHandle;
+    actions: CellActions;
+    theory: Theory;
+};