Merge pull request #572 from kris-brown/dpo_expose_morphism

Expose DPO morphism relating input and output of rewriting

src/categorical_algebra/DPO.jl

@@ -1,5 +1,5 @@
 module DPO
-export rewrite, rewrite_match, pushout_complement, can_pushout_complement,
+export rewrite, rewrite_match, rewrite_match_maps, pushout_complement, can_pushout_complement,
   id_condition, dangling_condition
 
 using ...Theories
@@ -11,16 +11,35 @@ using ..CSets: dangling_condition
 Apply a rewrite rule (given as a span, L<-I->R) to a ACSet
 using a match morphism `m` which indicates where to apply
 the rewrite.
+              l   r
+           L <- I -> R
+         m ↓    ↓    ↓
+           G <- K -> H
+
+Returns:
+- The morphisms I->K, K->G (produced by pushout complement), followed by
+  R->H, and K->H (produced by pushout)
 """
-function rewrite_match(L::ACSetTransformation, R::ACSetTransformation,
-                       m::ACSetTransformation)::ACSet
+function rewrite_match_maps(
+    L::ACSetTransformation, R::ACSetTransformation, m::ACSetTransformation
+    )::Tuple{ACSetTransformation,ACSetTransformation,
+             ACSetTransformation,ACSetTransformation}
   dom(L) == dom(R) || error("Rewriting where L, R do not share domain")
   codom(L) == dom(m) || error("Rewriting where L does not compose with m")
-  (k, _) = pushout_complement(L, m)
-  l1, _ = pushout(R, k)
-  return codom(l1)
+  (ik, kg) = pushout_complement(L, m)
+  rh, kh = pushout(R, ik)
+  return ik, kg, rh, kh
 end
 
+"""
+Apply a rewrite rule (given as a span, L<-I->R) to a ACSet
+using a match morphism `m` which indicates where to apply
+the rewrite. Return the rewritten ACSet.
+"""
+rewrite_match(L::ACSetTransformation, R::ACSetTransformation,
+  m::ACSetTransformation)::ACSet = codom(rewrite_match_maps(L, R, m)[4])
+
+
 """
 Apply a rewrite rule (given as a span, L<-I->R) to a ACSet,
 where a match morphism is found automatically. If multiple