From ee5aa8fe5c31cb855eedf1fbf84527a62a817c8a Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Wed, 16 Aug 2023 09:33:58 -0700
Subject: [PATCH 1/4] minor fixes

---
 docs/src/full_demo.jl            |  2 --
 src/categorical_algebra/CSets.jl |  1 +
 test/rewrite/DPO.jl              | 11 +++--------
 3 files changed, 4 insertions(+), 10 deletions(-)

diff --git a/docs/src/full_demo.jl b/docs/src/full_demo.jl
index 754c595..06c66c4 100644
--- a/docs/src/full_demo.jl
+++ b/docs/src/full_demo.jl
@@ -11,8 +11,6 @@ This is a regular julia file that can be run interactively.
 Importantly: 
  - use Julia 1.9 (not yet official released)
  - ]activate the environment in AlgebraicRewriting.jl/docs 
- - check (via ]status) that Catlab branch "varacsets4" is used
- - check that AlgebraicRewriting.jl branch "compat_varacsets" is used
  - check that graphviz is installed locally (test via "which dot" in terminal)
 
 Table of contents:
diff --git a/src/categorical_algebra/CSets.jl b/src/categorical_algebra/CSets.jl
index 8a7ec7e..0292e73 100644
--- a/src/categorical_algebra/CSets.jl
+++ b/src/categorical_algebra/CSets.jl
@@ -217,6 +217,7 @@ end
 function can_pushout_complement(pair::ComposablePair{<:ACSet})
   S = acset_schema(dom(pair))
   Ts = datatypes(dom(pair))
+  all(is_natural, pair) || error("Unnatural inputs")
 
   all(can_pushout_complement, unpack_diagram(pair; S=S, Ts=Ts)) &&
     isempty(dangling_condition(pair))
diff --git a/test/rewrite/DPO.jl b/test/rewrite/DPO.jl
index 9d189a0..e847012 100644
--- a/test/rewrite/DPO.jl
+++ b/test/rewrite/DPO.jl
@@ -117,21 +117,16 @@ end
 # Graphs with attributes
 ########################
 
-@present TheoryDecGraph(FreeSchema) begin
-  E::Ob
-  V::Ob
-  src::Hom(E,V)
-  tgt::Hom(E,V)
-
+@present SchDecGraph <: SchGraph begin
   X::AttrType
   dec::Attr(E,X)
 end
 
-@present TheoryLabeledDecGraph <: TheoryDecGraph begin
+@present SchLabeledDecGraph <: SchDecGraph begin
   label::Attr(V,X)
 end
 
-@acset_type LabeledDecGraph(TheoryLabeledDecGraph, index=[:src,:tgt])
+@acset_type LabeledDecGraph(SchLabeledDecGraph, index=[:src,:tgt])
 
 aI2 = @acset LabeledDecGraph{String} begin
   V = 2;  label = ["a","b"]

From 193dbe6d917d5b55431517935155bb042085d376 Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Fri, 13 Oct 2023 15:32:40 -0700
Subject: [PATCH 2/4] Conegation rewriting

---
 src/rewrite/CoNeg.jl   | 48 ++++++++++++++++++++++++++++++++++++++++++
 src/rewrite/Rewrite.jl |  2 ++
 src/rewrite/Utils.jl   |  7 +++---
 test/rewrite/CoNeg.jl  | 18 ++++++++++++++++
 test/runtests.jl       |  4 ++++
 5 files changed, 76 insertions(+), 3 deletions(-)
 create mode 100644 src/rewrite/CoNeg.jl
 create mode 100644 test/rewrite/CoNeg.jl

diff --git a/src/rewrite/CoNeg.jl b/src/rewrite/CoNeg.jl
new file mode 100644
index 0000000..869a890
--- /dev/null
+++ b/src/rewrite/CoNeg.jl
@@ -0,0 +1,48 @@
+module CoNeg 
+using Catlab.CategoricalAlgebra
+
+using ...CategoricalAlgebra.CSets
+using ..Utils
+import ..Utils: rewrite_match_maps
+import Catlab.CategoricalAlgebra: Subobject
+
+Subobject(X::ACSet, f::ACSetTransformation) = 
+  Subobject(X; Dict([k=>collect(vs) for (k,vs) in pairs(components(f))])...)
+
+"""    rewrite_match_maps(r::Rule{:CoNeg}, m)
+Apply a CoNegation rewrite rule (given as a span, L↩I->R) to a ACSet
+using a monic match morphism `m` which indicates where to apply the rewrite.
+              l   r
+           L <- I -> R
+         m ↓    ↓    ↓
+           G <- K -> H   where  K = ~L ∨ I
+
+This works for any type that implements bi-Heyting logic operators ~ and ∨.
+
+This is described [here](https://topos.site/blog/2023/04/conegation-rewriting).
+Essentially, it is partway between DPO and SPO. Suppose the rule tries to delete
+two things, one of which satisfies the dangling condition, the other violates it.
+While DPO would fail to apply at all, and SPO would delete both things (cascading 
+the deletion for the latter), co-negation rewriting would simply delete the item 
+which can be deleted without cascading and ignore the other element.
+
+It includes a quote which indicates that this method should work even when the 
+match morphism isn't monic, if it satisfies the identification condition. 
+Supporting this is not yet implemented.
+
+Match morphisms which bind attribute variables are not monic, hence we this 
+form of rewriting doesn't support VarACSets. Intuitively it feels like this 
+restriction could be relaxed.
+"""
+function rewrite_match_maps(r::Rule{:CoNeg}, m; check::Bool=false)
+  !check || is_monic(m) || error("Can only use CoNeg rewriting with monic matches: $m")
+  L = codom(m)
+  L′ = Subobject(L, m)
+  I′ = Subobject(L, compose(left(r), m))
+  K′ = ~L′ ∨ I′
+  ik = hom(Subobject(dom(hom(K′)), hom(I′)))
+  rh, kh = pushout(right(r), ik)
+  Dict(:ik => ik, :kg => hom(K′), :rh => rh, :kh => kh)
+end
+
+end # module
\ No newline at end of file
diff --git a/src/rewrite/Rewrite.jl b/src/rewrite/Rewrite.jl
index 81fc2e4..7d83ef8 100644
--- a/src/rewrite/Rewrite.jl
+++ b/src/rewrite/Rewrite.jl
@@ -5,6 +5,7 @@ using Reexport
 include("Constraints.jl")
 include("Utils.jl")
 include("DPO.jl")
+include("CoNeg.jl")
 include("SPO.jl")
 include("SqPO.jl")
 include("PBPO.jl")
@@ -14,6 +15,7 @@ include("Representable.jl")
 @reexport using .Utils
 @reexport using .Representable
 @reexport using .DPO
+@reexport using .CoNeg
 @reexport using .SPO
 @reexport using .SqPO
 @reexport using .PBPO
diff --git a/src/rewrite/Utils.jl b/src/rewrite/Utils.jl
index b88d1b4..c9e64d4 100644
--- a/src/rewrite/Utils.jl
+++ b/src/rewrite/Utils.jl
@@ -26,7 +26,7 @@ The L structure encodes a pattern to be matched.
 The R morphism encodes a replacement pattern to be substituted in.
 They are related to each other by an interface I with maps: L ⟵ I ⟶ R 
 
-A semantics (DPO, SPO, or SqPO) must be chosen.
+A semantics (DPO, SPO, CoNeg, or SqPO) must be chosen.
 
 Control the match-finding process by specifying whether the match is
 intended to be monic or not, as well as an optional application
@@ -94,11 +94,12 @@ right(r::Rule{T}) where T = r.R
 
 # Extracting specific maps from rewriting output data 
 #####################################################
+DPO′ = [:DPO, :CoNeg] # these have identical diagrams
 
 """Extract the map from the R to the result from the full output data"""
 function get_rmap(sem::Symbol, maps)
   if isnothing(maps)  nothing
-  elseif sem == :DPO  maps[:rh]
+  elseif sem ∈ DPO′  maps[:rh]
   elseif sem == :SPO  invert_hom(maps[:rmono], epic=false) ⋅ maps[:rmap]
   elseif sem == :SqPO maps[:r]
   elseif sem == :PBPO maps[:w]
@@ -111,7 +112,7 @@ get_result(sem::Symbol, maps) = codom(get_rmap(sem, maps))
 """Extract the partial map (derived rule) from full output data"""
 function get_pmap(sem::Symbol, maps)
   if isnothing(maps)  nothing
-  elseif sem == :DPO  Span(maps[:kg], maps[:kh])
+  elseif sem ∈ DPO′  Span(maps[:kg], maps[:kh])
   elseif sem == :SPO  Span(maps[:gmono], maps[:gmap])
   elseif sem == :SqPO Span(maps[:i], maps[:o])
   elseif sem == :PBPO Span(maps[:gl], maps[:gr])
diff --git a/test/rewrite/CoNeg.jl b/test/rewrite/CoNeg.jl
new file mode 100644
index 0000000..cdc5f3b
--- /dev/null
+++ b/test/rewrite/CoNeg.jl
@@ -0,0 +1,18 @@
+module TestCoNeg 
+
+using Test
+using AlgebraicRewriting, Catlab
+
+# Graphs
+########
+L = Graph(2)
+R = ob(terminal(Graph))
+r = Rule{:CoNeg}(create.([L,R])...)
+
+G = path_graph(Graph, 2) ⊕ Graph(1)
+m = ACSetTransformation(L, G; V=[1,3]);
+
+expected = path_graph(Graph, 2) ⊕ R
+@test is_isomorphic(expected, rewrite_match(r, m))
+
+end # module
\ No newline at end of file
diff --git a/test/runtests.jl b/test/runtests.jl
index ac0e795..5f12096 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -47,6 +47,10 @@ end
   include("rewrite/DPO.jl")
 end
 
+@testset "CoNeg" begin
+  include("rewrite/CoNeg.jl")
+end
+
 @testset "SPO" begin
   include("rewrite/SPO.jl")
 end

From ebfaa98cc35f396b24265582c75aec86ff055f39 Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Fri, 13 Oct 2023 17:06:27 -0700
Subject: [PATCH 3/4] bump acsets version

---
 Project.toml         | 2 +-
 src/rewrite/CoNeg.jl | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Project.toml b/Project.toml
index f430b70..2db855c 100644
--- a/Project.toml
+++ b/Project.toml
@@ -20,7 +20,7 @@ Luxor = "ae8d54c2-7ccd-5906-9d76-62fc9837b5bc"
 AlgebraicRewritingLuxorExt = "Luxor"
 
 [compat]
-ACSets = "0.2.3"
+ACSets = "0.2.9"
 Catlab = "0.15.4"
 DataStructures = "0.17, 0.18"
 Reexport = "^1"
diff --git a/src/rewrite/CoNeg.jl b/src/rewrite/CoNeg.jl
index 869a890..9afb449 100644
--- a/src/rewrite/CoNeg.jl
+++ b/src/rewrite/CoNeg.jl
@@ -31,7 +31,7 @@ match morphism isn't monic, if it satisfies the identification condition.
 Supporting this is not yet implemented.
 
 Match morphisms which bind attribute variables are not monic, hence we this 
-form of rewriting doesn't support VarACSets. Intuitively it feels like this 
+form of rewriting doesn't support VarACSets. Intuitively, it feels like this 
 restriction could be relaxed.
 """
 function rewrite_match_maps(r::Rule{:CoNeg}, m; check::Bool=false)

From 0d707da8f57228d7e68524322ed3692eaaefd962 Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Fri, 13 Oct 2023 18:26:12 -0700
Subject: [PATCH 4/4] docs warnonly

---
 docs/make.jl | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/docs/make.jl b/docs/make.jl
index 990c2da..9ff2e6c 100644
--- a/docs/make.jl
+++ b/docs/make.jl
@@ -11,7 +11,8 @@ end
 makedocs(
     sitename = "AlgebraicRewriting",
     format = Documenter.HTML(),
-    modules = [AlgebraicRewriting]
+    modules = [AlgebraicRewriting],
+    warnonly = true
 )