Rewriting with Symmetric Monoidal Structure (#27)

Implement rewriting with symmetric monoidal structure

Bonchi, Filippo, et al. "String diagram rewrite theory II: Rewriting with symmetric monoidal structure." Mathematical Structures in Computer Science 32.4 (2022): 511-541.


# Details

- implement rewrite with SMT
- apply_smc_rewrite takes as arguments "witnesses" that inputs are legal, witnesses are implemented in previous PRs.
- We work on strict because some properties requires quotiented wires
- Some tests using circuits and compiler-like optimizations (dead code elimination, constant propagation)
- Refactoring for reuse existing checks without cloning.

Author: mstn

Cargo.toml

@@ -14,6 +14,7 @@ serde = { version = "1.0", features = ["derive"], optional = true }
 [features]
 default = []
 serde = ["dep:serde"]
+experimental = []
 
 [dev-dependencies]
 proptest = "1.6.0"

README.md

@@ -28,6 +28,23 @@ This code is an implementation of the paper
 - Functors, including optic transformation for ahead-of-time differentiation of
   syntax
 
+# Experimental APIs
+
+Some APIs are marked experimental and are disabled by default.
+
+Enable experimental APIs with Cargo features:
+
+```toml
+[dependencies]
+open-hypergraphs = { version = "0.2.10", features = ["experimental"] }
+```
+
+or on the command line:
+
+```bash
+cargo test --features experimental
+```
+
 # Examples
 
 An example for defining a simple expression language ([polynomial

src/array/traits.rs

@@ -78,6 +78,9 @@ pub trait Array<K: ArrayKind, T>: Clone {
     /// Concatenate two arrays
     fn concatenate(&self, other: &Self) -> Self;
 
+    /// Concatenate a slice of arrays into one array.
+    fn concatenate_many(arrays: &[&Self]) -> Self;
+
     /// `fill(x, n)` returns the array length n containing repeated element x.
     fn fill(x: T, n: K::I) -> Self;
 

src/array/vec/vec_array.rs

@@ -68,6 +68,23 @@ impl<T: Clone> Array<VecKind, T> for VecArray<T> {
         VecArray(result)
     }
 
+    fn concatenate_many(arrays: &[&Self]) -> Self {
+        if arrays.is_empty() {
+            return Self::empty();
+        }
+
+        let mut n = 0;
+        for arr in arrays {
+            n += arr.len();
+        }
+
+        let mut out = Vec::with_capacity(n);
+        for arr in arrays {
+            out.extend_from_slice(arr);
+        }
+        Self(out)
+    }
+
     fn fill(x: T, n: usize) -> Self {
         VecArray(vec![x; n])
     }