From cc1591ebbe1e4fbb7e37e5931f86ce66e7999aae Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Fri, 19 Jul 2024 14:10:13 -0700
Subject: [PATCH 1/2] remove support for Attr change via DPO

---
 Project.toml                       |   2 +-
 docs/literate/full_demo.jl         |  13 +---
 docs/literate/lotka_volterra.jl    | 121 ++++++++++++++++-------------
 src/categorical_algebra/CSets.jl   |  49 +++---------
 src/categorical_algebra/FinSets.jl |  11 +++
 src/rewrite/DPO.jl                 |  37 ---------
 src/rewrite/Inplace.jl             |   5 ++
 src/rewrite/Utils.jl               |  97 ++++++++++++-----------
 test/Project.toml                  |   1 +
 test/categorical_algebra/CSets.jl  |   9 +--
 test/incremental/IncrementalCC.jl  |  15 ++--
 test/rewrite/DPO.jl                |  87 ++++++---------------
 test/rewrite/Inplace.jl            |   4 +-
 test/runtests.jl                   |   8 +-
 test/schedules/Eval.jl             |  93 +---------------------
 15 files changed, 187 insertions(+), 365 deletions(-)

diff --git a/Project.toml b/Project.toml
index dc31d84..0602cde 100644
--- a/Project.toml
+++ b/Project.toml
@@ -2,7 +2,7 @@ name = "AlgebraicRewriting"
 uuid = "725a01d3-f174-5bbd-84e1-b9417bad95d9"
 license = "MIT"
 authors = ["Kris Brown <kris@topos.institute>"]
-version = "0.3.6"
+version = "0.3.7"
 
 [deps]
 ACSets = "227ef7b5-1206-438b-ac65-934d6da304b8"
diff --git a/docs/literate/full_demo.jl b/docs/literate/full_demo.jl
index ff172d6..cda0b5a 100644
--- a/docs/literate/full_demo.jl
+++ b/docs/literate/full_demo.jl
@@ -354,20 +354,15 @@ end
 
 l = homomorphism(I, L; initial=(V=1:2,))
 r = homomorphism(I, R; initial=(V=1:2,))
-rule = Rule(l, r; monic=[:E], expr=Dict(:Weight => [xs -> xs[1] + xs[2]]))
+rule = Rule(l, r; monic=[:E], expr=Dict(:Weight => [((w₁,w₂),) -> w₁ + w₂]))
 
 G = @acset WeightedGraph{Int} begin
-  V = 1
-  E = 3
-  src = 1
-  tgt = 1
-  weight = [10, 20, 100]
+  V = 1; E = 3; src = 1; tgt = 1; weight = [10, 20, 100]
 end
 
-m = get_matches(rule,G)[1]
+m = homomorphism(L, G; initial=(E=1:2,))
 @test rewrite_match(rule, m) == @acset WeightedGraph{Int} begin
-  V = 1; E = 2
-  src = [1]; tgt = [1]; weight = [30, 100]
+  V = 1; E = 2; src = [1]; tgt = [1]; weight = [30, 100]
 end
 
 # # 8. Graph processes
diff --git a/docs/literate/lotka_volterra.jl b/docs/literate/lotka_volterra.jl
index 7ad1596..86506d2 100644
--- a/docs/literate/lotka_volterra.jl
+++ b/docs/literate/lotka_volterra.jl
@@ -48,8 +48,10 @@ be oriented in a particular direction at any point in time.
   (Sheep, Wolf)::Ob
   sheep_loc::Hom(Sheep, V); wolf_loc::Hom(Wolf, V)
 
-  (Time, Eng)::AttrType
-  countdown::Attr(V, Time); 
+  Time::Ob 
+  countdown::Hom(Time, V); 
+
+  Eng::AttrType
   sheep_eng::Attr(Sheep, Eng); wolf_eng::Attr(Wolf, Eng)
   
   Dir::AttrType
@@ -59,7 +61,7 @@ end
 ## efficient ABM rewriting uses BitSetParts rather than DenseParts to allow 
 ## in-place pushout rewriting, rather than pure/non-mutating pushouts.)
 @acset_type LV_Generic(SchLV, part_type=BitSetParts) <: HasGraph
-const LV = LV_Generic{Int, Int, Symbol}
+const LV = LV_Generic{Int, Symbol}
 
 to_graphviz(SchLV; prog="dot")
 
@@ -77,7 +79,7 @@ unnecessary when doing the actual agent-based modeling. So what we will do is
 end
 
 @acset_type LV′_Generic(SchLV′, part_type=BitSetParts) <: HasGraph
-const LV′ = LV′_Generic{Int, Int, Symbol, Tuple{Int,Int}};
+const LV′ = LV′_Generic{Int, Symbol, Tuple{Int,Int}};
 
 #=
 We will be representing directions as `Symbol`s and encode the geometry via 
@@ -123,7 +125,7 @@ obtain the analogous actions for wolves.
 =#
 
 F = Migrate(
-  Dict(:Sheep => :Wolf, :Wolf => :Sheep),
+  Dict(:Sheep => :Wolf, :Wolf => :Sheep, :Time=>:Time),
   Dict([:sheep_loc => :wolf_loc, :wolf_loc => :sheep_loc,
     :sheep_eng => :wolf_eng, :wolf_eng => :sheep_eng, :countdown => :countdown,
     :sheep_dir => :wolf_dir, :wolf_dir => :sheep_dir,]), SchLV, LV);
@@ -148,7 +150,8 @@ function create_grid(n::Int)
   coords = Dict()
   for i in 0:n-1  # Initialize grass 50% green, 50% uniformly between 0-30
     for j in 0:n-1
-      coords[i=>j] = add_part!(lv, :V; countdown=max(0, rand(-30:30)), coord=(i, j))
+      coords[i=>j] = add_part!(lv, :V; coord=(i, j))
+      add_parts!(lv, :Time, max(0, rand(-30:30)); countdown=coords[i=>j])
     end
   end
   for i in 0:n-1
@@ -210,7 +213,7 @@ function view_LV(p::LV′, pth=tempname(); name="G", title="", star=nothing)
   stmts = Statement[]
   for s in 1:nv(p)
     st = (star == (:V => s)) ? "*" : ""
-    gv = p[s, :countdown]
+    gv = length(incident(p, s, :countdown))
     col = gv == 0 ? "lightgreen" : "tan"
     push!(stmts, Node("v$s", Attributes(
       :label => gv == 0 ? "" : string(gv) * st,
@@ -266,8 +269,8 @@ obtain a generic LV′ sheep. We use this as the domain of a hom that
 assigns the sheep to Sheep #2 of the world state `init` from above.
 =#
 
-S = @acset LV begin V=1; Sheep=1; Dir=1; Eng=1; Time=1;
-  sheep_loc=1; sheep_dir=[AttrVar(1)]; sheep_eng=[AttrVar(1)]; countdown=[AttrVar(1)]
+S = @acset LV begin V=1; Sheep=1; Dir=1; Eng=1;
+  sheep_loc=1; sheep_dir=[AttrVar(1)]; sheep_eng=[AttrVar(1)];
 end
 
 view_LV(hom(F2(S), init; initial=(Sheep=[2],)))
@@ -285,6 +288,9 @@ yLV = yoneda_cache(LV; clear=false); # cache=false means reuse cached results
 I = LV() # Empty agent type
 S = @acset_colim yLV begin s::Sheep end # Generic sheep agent
 W = F(S) # Generic wolf agent, obtained via the swapping `F` data migration
+E = @acset_colim yLV begin e::Eng end
+D = @acset_colim yLV begin d::Dir end
+T = @acset_colim yLV begin t::Time end
 G = @acset_colim yLV begin v::V end # Generic grass agent
 N = Names(Dict("W" => W, "S" => S, "G" => G, "" => I)); # give these ACSets names
 
@@ -319,11 +325,12 @@ single ACSet along with an `expr` dictionary which states how attributes
 change.
 =#
 
-rl = Rule(S; expr=(Dir=[xs -> left(only(xs))],));
-rr = Rule(S; expr=(Dir=[xs -> right(only(xs))],));
+GS_Eng = hom(G⊕E, S; monic=true)
+rl = Rule(GS_Eng,GS_Eng; expr=(Dir=[((s,),) -> left(s)],));
+rr = Rule(GS_Eng,GS_Eng; expr=(Dir=[((s,),) -> right(s)],));
 
-sheep_rotate_l = tryrule(RuleApp(:turn_left, rl, S));
-sheep_rotate_r = tryrule(RuleApp(:turn_right, rr, S));
+sheep_rotate_l = tryrule(RuleApp(:turn_left, rl, id(S), id(S)));
+sheep_rotate_r = tryrule(RuleApp(:turn_right, rr, id(S), id(S)));
 
 # We can imagine executing these rules in sequence 
 seq_sched = (sheep_rotate_l ⋅ sheep_rotate_r);
@@ -336,8 +343,8 @@ view_sched(par_sched; names=N)
 # #### Test rotation
 begin
   ex = @acset LV begin 
-    E=1; Sheep=1; V=2
-    src=1; tgt=2; dir=:W; countdown = [0, 0]
+    E=1; Sheep=1; V=2; Time=2
+    src=1; tgt=2; dir=:W; countdown = [1, 2]
     sheep_loc=1; sheep_eng=100; sheep_dir=:N
   end;
 
@@ -382,8 +389,8 @@ sheep_fwd = tryrule(RuleApp(:move_fwd, sheep_fwd_rule,
 
 begin
   ex = @acset LV begin
-    V=3; E=2; Sheep=1; 
-    countdown=[0,0,0]
+    V=3; E=2; Sheep=1; Time=4 
+    countdown=[1,2,2,3]
     src=[1,2]; tgt=[2,3]; dir=[:N,:W]
     sheep_loc=1; sheep_dir=:N; sheep_eng = 10
   end
@@ -397,24 +404,38 @@ end;
 
 # ### Sheep eat grass
 
-s_eat_pac = @acset_colim yLV begin s::Sheep; countdown(sheep_loc(s)) == 0 end;
+function add_time(lv::LV, n::Int) 
+  res = deepcopy(lv)
+  add_parts!(res, :Time, n; countdown=1)
+  res
+end
+
+s_eat_nac = @acset_colim yLV begin 
+  s::Sheep; t::Time; countdown(t) == sheep_loc(s) 
+end;
 
-se_rule = Rule(S; expr=(Eng=[vs -> only(vs) + 4], Time=[vs -> 30],),
-  ac=[AppCond(hom(S, s_eat_pac))]);
+GS_Dir = hom(G⊕D, S; monic=true)
+GS_Dir30 = hom(G⊕D, add_time(S, 30); monic=true)
 
-sheep_eat = tryrule(RuleApp(:Sheep_eat, se_rule, S));
+se_rule = Rule(GS_Dir,GS_Dir30; expr=(Eng=[vs -> only(vs) + 4],),
+  ac=[AppCond(hom(S, s_eat_nac), false)]);
+
+S_to_S30 = hom(S, add_time(S, 30))
+sheep_eat = tryrule(RuleApp(:Sheep_eat, se_rule, id(S), S_to_S30));
 
 # #### Sheep eating test
 begin
   ex = @acset LV begin
-    E=1; V=2; Sheep=1; 
-    src=1; tgt=2; dir=:S; countdown=[10, 0]
+    E=1; V=2; Sheep=1; Time=2 
+    src=1; tgt=2; dir=:S; countdown=[1,1]
     sheep_loc = 2; sheep_eng = 3; sheep_dir=:W
   end
 
-  expected = copy(ex)
-  expected[2,:countdown] = 30
-  expected[1,:sheep_eng] = 7
+  expected = @acset LV begin
+    E=1; V=2; Sheep=1; Time=32 
+    src=1; tgt=2; dir=:S; countdown=[1,1, fill(2, 30)...]
+    sheep_loc = 2; sheep_eng = 7; sheep_dir=:W
+  end
 
   @test is_isomorphic(expected, rewrite(se_rule, ex))
   rewrite!(se_rule, ex)
@@ -428,15 +449,17 @@ w_eat_l = @acset_colim yLV begin
   sheep_loc(s) == wolf_loc(w)
 end;
 
-we_rule = Rule(hom(W, w_eat_l), id(W); expr=(Eng=[vs -> vs[2] + 20],));
+GWS_Dir = hom(G⊕D, w_eat_l; initial=(Dir=[AttrVar(2)],))
+GW_Dir = hom(G⊕D, W; monic=true,)
+we_rule = Rule(GWS_Dir, GW_Dir, expr=(Eng=[vs -> vs[2] + 20],));
 
-wolf_eat = tryrule(RuleApp(:Wolf_eat, we_rule, W));
+wolf_eat = tryrule(RuleApp(:Wolf_eat, we_rule, hom(W, w_eat_l), id(W)));
 
 # #### Wolf eating test
 begin
   ex = @acset LV begin 
-    Sheep=1; Wolf=1; V=3; E=2; 
-    src=[1,2]; tgt=[2,3]; countdown=[9,10,11]; dir=[:N,:N]; 
+    Sheep=1; Wolf=1; V=3; E=2; Time=3;
+    src=[1,2]; tgt=[2,3]; countdown=[1,2,3]; dir=[:N,:N]; 
     sheep_loc=2; sheep_eng=[3]; sheep_dir=[:N]
     wolf_loc=[2];  wolf_eng=[16];  wolf_dir=[:S]
   end
@@ -463,8 +486,8 @@ sheep_starve = (RuleApp(:starve, sheep_die_rule,
 
 begin
   ex = @acset LV begin 
-    V=1; Sheep=1; Wolf=1
-    countdown=20;
+    V=1; Sheep=1; Wolf=1; Time=1
+    countdown=[1];
     sheep_loc=1; sheep_eng=0; sheep_dir=:W
     wolf_loc=1; wolf_eng=10; wolf_dir=:S
   end
@@ -486,8 +509,8 @@ end;
 sheep_reprod_rule = Rule(
   hom(G, S),
   hom(G, s_reprod_r);
-  expr=(Dir=fill(vs->only(vs) ,2), 
-        Eng=fill(vs -> round(Int, vs[1] / 2, RoundUp), 2),)
+  expr=(Dir=fill(((dₛ,),)->dₛ ,2), 
+        Eng=fill(((eₛ,),) -> round(Int, eₛ / 2, RoundUp), 2),)
 );
 
 sheep_reprod = RuleApp(:reproduce, sheep_reprod_rule,
@@ -497,8 +520,8 @@ sheep_reprod = RuleApp(:reproduce, sheep_reprod_rule,
 
 begin # test
   ex = @acset LV begin 
-    Sheep=1; Wolf=1; V=2; 
-    countdown=[20,30]
+    Sheep=1; Wolf=1; V=2; Time=2
+    countdown=[1,2]
     sheep_loc=1; sheep_eng=10; sheep_dir=:W 
     wolf_loc=2; wolf_eng=5; wolf_dir=:N
   end
@@ -509,6 +532,7 @@ begin # test
   expected[:sheep_loc] = [1, 1]
   expected[:sheep_dir] = [:W, :W]
 
+  rewrite(sheep_reprod_rule,ex)
   @test is_isomorphic(rewrite(sheep_reprod_rule,ex),expected)
   rewrite!(sheep_reprod_rule,ex)
   @test is_isomorphic(ex, expected)
@@ -516,13 +540,7 @@ end;
   
 # ### Grass increments
 
-g_inc_n = deepcopy(G)
-set_subpart!(g_inc_n, 1, :countdown, 0)
-rem_part!(g_inc_n, :Time, 1);
-
-g_inc_rule = Rule(id(G), id(G);
-  ac=[AppCond(hom(G, g_inc_n), false)],
-  expr=(Time=[vs -> only(vs) - 1],));
+g_inc_rule = Rule(hom(G, T), id(G));
 
 g_inc = RuleApp(:GrassIncrements, g_inc_rule, G) |> tryrule;
 
@@ -530,20 +548,15 @@ g_inc = RuleApp(:GrassIncrements, g_inc_rule, G) |> tryrule;
 
 begin
   ex = @acset LV begin
-    Sheep = 1; V = 3; E = 2
-    src = [1, 2]; tgt = [2, 3]
-    sheep_loc = 2; sheep_eng = [3]; sheep_dir = [:N]
-    countdown = [1, 10, 2]; dir = fill(:N, 2)  
-  end
-  expected = @acset LV begin
-    Sheep = 1; V = 3; E = 2
+    Sheep = 1; V = 3; E = 2; Time=3
     src = [1, 2]; tgt = [2, 3]
     sheep_loc = 2; sheep_eng = [3]; sheep_dir = [:N]
-    countdown = [0, 10, 2]; dir = fill(:N, 2)
+    countdown = [2,2,2]; dir = fill(:N, 2)  
   end
-  m = get_matches(g_inc_rule, ex)[1]
-  @test is_isomorphic(rewrite_match(g_inc_rule, m), expected)
-  rewrite_match!(g_inc_rule, m)
+  expected = deepcopy(ex);
+  rem_part!(expected, :Time, 1)
+  @test is_isomorphic(rewrite(g_inc_rule, ex), expected)
+  rewrite!(g_inc_rule, ex)
   @test is_isomorphic(ex, expected)
 end;
 
diff --git a/src/categorical_algebra/CSets.jl b/src/categorical_algebra/CSets.jl
index 6689dd8..f95ce42 100644
--- a/src/categorical_algebra/CSets.jl
+++ b/src/categorical_algebra/CSets.jl
@@ -151,11 +151,6 @@ finite sets. If any of the pointwise identification conditions fail (in FinSet),
 this method will raise an error. If the dangling condition fails, the resulting
 C-set will be only partially defined. To check all these conditions in advance,
 use the function [`can_pushout_complement`](@ref).
-
-In the absence of AttrVars, K is a subobject of G. But we want to be able to 
-change the value of attributes. So any variables in I are not concretized by 
-the I->K map. However, AttrVars may be merged together if `m: L -> G` merges 
-parts together.
 """
 function pushout_complement(pair::ComposablePair{<:ACSet, <:TightACSetTransformation})
   l, m = pair 
@@ -163,46 +158,20 @@ function pushout_complement(pair::ComposablePair{<:ACSet, <:TightACSetTransforma
   S = acset_schema(I)
   all(at->nparts(G, at)==0, attrtypes(S)) || error("Cannot rewrite with AttrVars in G")
   # Compute pushout complements pointwise in FinSet.
-  comps = NamedTuple(Dict(map(ob(S)) do o 
+  comps = NamedTuple(Dict(map(types(S)) do o 
       o => pushout_complement(ComposablePair(l[o], m[o]))
   end))
-  k_components = Dict{Symbol,Any}(pairs(map(first, comps)))
-  g_components = Dict{Symbol,Any}(pairs(map(last, comps)))
-
-  # Reassemble components into natural transformations.
-  g = hom(Subobject(G, NamedTuple(Dict(o => g_components[o] for o in ob(S)))))
-  K = dom(g)
 
-  var_eq = var_eqs(l, m) # equivalence class of attrvars
-  for at in attrtypes(S)
-    eq = var_eq[at]
-    roots = unique(find_root!.(Ref(eq), 1:length(eq)))
-    add_parts!(K, at, length(roots))
-    k_components[at] = map(parts(I, at)) do pᵢ
-      attrvar = AttrVar(findfirst(==(find_root!(eq, pᵢ)), roots))
-      for (a, d, _) in attrs(S; to=at)
-        for p in incident(I, AttrVar(pᵢ), a)
-          K[k_components[d](p), a] = attrvar
-        end
-      end
-      attrvar
-    end
-    T = Union{AttrVar, attrtype_type(G, at)}
-    g_components[at] = Vector{T}(map(parts(K, at)) do v
-      try 
-        f, o, val = var_reference(K, at, v)
-        G[g_components[o](val), f]
-      catch e 
-        vᵢ = findfirst(==(AttrVar(v)), k_components[at])
-        m[at](l[at](AttrVar(vᵢ)))
-      end 
-    end)
-  end
+  k_components = Dict{Symbol,Any}(pairs(map(first, comps)))
+  g_components = Dict{Symbol,Any}(k => k ∈ ob(S) ? v : FinFunction(v) 
+                                  for (k,v) in pairs(map(last, comps)))
 
-  k = ACSetTransformation(I, K; k_components...)
-  g = ACSetTransformation(K, G; g_components...)
+  # # Reassemble components into natural transformations.
+  g = hom(Subobject(G, NamedTuple(g_components)))
+  k = ACSetTransformation(I, dom(g); k_components...)
   kg, lm = force.(compose.([k,l], [g, m]))
-  kg == lm || error("Square doesn't commute: \n\t$(components(kg)) \n!= \n\t$(components(lm))")
+  kg == lm || error(
+    "Square doesn't commute: \n\t$(components(kg)) \n!= \n\t$(components(lm))")
   is_natural(k) || error("k unnatural $k")
   is_natural(g) || error("g unnatural")
   return ComposablePair(k, g)
diff --git a/src/categorical_algebra/FinSets.jl b/src/categorical_algebra/FinSets.jl
index 8fb5f55..f9dbfef 100644
--- a/src/categorical_algebra/FinSets.jl
+++ b/src/categorical_algebra/FinSets.jl
@@ -75,4 +75,15 @@ function id_condition(pair::ComposablePair{<:FinSet{Int}})
            if m(l_imageᶜ[i]) == m(l_imageᶜ[j])))
 end
 
+
+"""
+Given a monic VarFunction (which only sends AttrVars to AttrVars) and a 
+VarFunction which only sends AttrVars to concrete values, we have a unique 
+means of first sending vars to concrete 
+
+"""
+function pushout_complement(pair::ComposablePair{<:VarSet{T}}) where T 
+  f, g = pair 
+  return ComposablePair(f ⋅ g, id(codom(g)))
+end 
 end # module
diff --git a/src/rewrite/DPO.jl b/src/rewrite/DPO.jl
index d34c858..e68b4e6 100644
--- a/src/rewrite/DPO.jl
+++ b/src/rewrite/DPO.jl
@@ -28,41 +28,4 @@ function rewrite_match_maps(r::Rule{:DPO}, m; check::Bool=false)
   Dict(:ik=>ik, :kg=>kg, :rh=>rh, :kh=>kh)
 end
 
-"""Further induced equations between AttrVars, given a specific match morphism"""
-var_eqs(r::Rule{:DPO}, m::ACSetTransformation) = var_eqs(left(r), m)
-
-"""
-A match may be invalid because two variables (which are to be assigned different
-values via the I -> R map) are identified (due to merging via the I->L map, 
-which morally ought be monic but is not for AttrVars). We can check this before
-computing the pushout to make sure that we will not get an inconsistent result 
-when trying to compute it. This requires executing the custom exprs of the 
-rewrite rule, so we may wish to build in the ability to skip this step if that 
-is computationally intensive.
-"""
-function check_match_var_eqs(r::Rule{:DPO}, m::ACSetTransformation)
-  eqs = var_eqs(r, m)
-  I = dom(left(r))
-  S = acset_schema(I)
-  errs = []
-  for at in attrtypes(S)
-    roots = find_root!.(Ref(eqs[at]), 1:length(eqs[at]))
-    for root in unique(roots)
-      elems = findall(==(root), roots)
-      if length(elems) > 1 # potential for conflict
-        res = map(AttrVar.(elems)) do elem
-          rval = right(r)[at](elem)
-          rval isa AttrVar || return rval
-          r.exprs[at][rval.val](collect(m[at]))
-        end
-        length(unique(res)) == 1 || push!(errs, "$at: inconsistent $elems↦$res")
-      end
-    end
-  end
-  return errs
-end
-
-"""Ignore for other categories"""
-check_match_var_eqs(::Rule{:DPO}, m) = []
-
 end # module 
diff --git a/src/rewrite/Inplace.jl b/src/rewrite/Inplace.jl
index 8296610..3fb090f 100644
--- a/src/rewrite/Inplace.jl
+++ b/src/rewrite/Inplace.jl
@@ -170,8 +170,13 @@ function add(::Rule, c::Compiler, ob::Symbol, part::Int)
 end
 
 function init(r::Rule, c::Compiler, attrtype::Symbol, var::Int)
+  preim = preimage(right(r)[attrtype], AttrVar(var))
+
   initializer = if var ∈ keys(r.exprs[attrtype])
+    isempty(preim) || error("Cannot give expr to preserved variable")
      Compute(r.exprs[attrtype][var])
+  elseif !isempty(preim)
+    Compute(vs -> vs[left(r)[attrtype](AttrVar(only(preim))).val])
   else
     # Fresh()
     error(
diff --git a/src/rewrite/Utils.jl b/src/rewrite/Utils.jl
index 5a36a4f..33befff 100644
--- a/src/rewrite/Utils.jl
+++ b/src/rewrite/Utils.jl
@@ -16,6 +16,9 @@ using ..Constraints
 using ...CategoricalAlgebra
 using ...CategoricalAlgebra.CSets: invert_hom
 
+import Catlab.CategoricalAlgebra.FinSets: is_monic
+is_monic(f::SliceHom) = is_monic(f.f) # UPSTREAM
+
 
 # RULES 
 #######
@@ -40,54 +43,59 @@ condition(s)
   monic::Vector{Symbol} # further constraint on match morphism
   exprs::Dict{Symbol, Dict{Int,Union{Nothing,Function}}}
 
-  function Rule{T}(L, R; ac=nothing, monic=false, expr=nothing, freevar=false) where {T}
-    S = acset_schema(dom(L))
+  function Rule{T}(l, r; ac=nothing, monic=false, expr=nothing, freevar=false) where {T}
+    L, R, I, I′ = codom(l), codom(r), dom(l), dom(r)
+    S = acset_schema(L)
     monic = monic isa Bool ? (monic ? ob(S) : []) : monic
-    dom(L) == dom(R) || error("L<->R not a span")
+    expr = isnothing(expr) ? Dict() : expr
+    T==:SqPO || is_monic(l) || error("Left leg must be monic $(components(l))")
+    I == I′ || error("L<->R not a span")
     ACs = isnothing(ac) ? [] : deepcopy.(ac)
     exprs = isnothing(expr) ? Dict() : Dict(pairs(expr))
-    map(enumerate([L,R,])) do (i, f)
-      if !is_natural(f)
-        error("unnatural map #$i: $f")
-      end
+    for (lbl, f) in ["left"=>l, "right"=>r]
+      is_natural(f) || error("unnatural $lbl map: $f")
     end
+
+    # Check the application conditions are maps out of L
     for (i,cond) in enumerate(ACs)
       λ = findfirst(==(1), cond.g[:elabel])
       λv = cond.g[λ, :src]
       λs = cond.g[λv,:vlabel]
-      err = "Condition $i: source $λs \n != match L $(codom(L))\nE#$λ V#$λv"
-      λs == codom(L) || error(err)
+      err = "Condition $i: source $λs \n != match L $(L)\nE#$λ V#$λv"
+      λs == L || error(err)
     end 
-    # For the case of ACSet rewriting, address variable substitution in R
-    if !(dom(L) isa ACSet)
-      exprs = Dict()
-    else 
-      exprs = Dict(map(attrtypes(S)) do o
-        binding = Dict()
-        for r_var in parts(codom(R), o)
-          # User explicitly provides a function to evaluate for this variable
-          if !isnothing(expr) && haskey(expr, o) && r_var ∈ keys(expr[o])
-            binding[r_var] = expr[o][r_var]
-          else # try to see if the value is determined by the partial map
-            preim = preimage(R[o],AttrVar(r_var))
-            pr = unique(L[o].(AttrVar.(preimage(R[o],AttrVar(r_var)))))
-            if length(pr) == 1 
-              binding[r_var] = vs -> vs[only(pr).val] 
-            elseif freevar # We are ok with introducing free variables
-              continue 
-            else 
-              error("Unbound variable in R $o#$r_var")
-            end 
+
+    # For the case of ACSet rewriting, address variable assignment in R
+    exprs = !(L isa ACSet) ? Dict() : Dict(map(attrtypes(S)) do o
+      binding = Dict()
+      is_monic(r[o]) || error("I→R AttrType component must be monic $(r[o])")
+      for r_var in parts(R, o)
+        preim = preimage(r[o], AttrVar(r_var))
+        x = get′(expr, o, r_var)
+        if !isempty(preim) # the value of this attrvar is preserved
+          isnothing(x) || error(
+            "Cannot manually set AttrVar value for a preserved attribute")
+        else # value of this attr is set explicitly (or a freevar is introduced)
+          if !isnothing(x)
+            binding[r_var] = x
+          elseif freevar continue 
+          else 
+            error(
+            "Must set AttrVar value for newly introduced attribute via `exprs`")
           end
         end
-        o => binding
-      end)
-    end
-    new{T}(deepcopy(L), deepcopy(R), ACs, monic, exprs)
+      end
+      o => binding
+    end)
+    new{T}(deepcopy(l), deepcopy(r), ACs, monic, exprs)
   end
 end
 
-Rule(X::ACSet; kw...) = Rule(id(X), id(X); kw...) # only changing attributes
+get′(d::Union{NamedTuple,AbstractDict}, o::Symbol, i::Int) =  
+  haskey(d, o) && haskey′(d[o], i) ? d[o][i] : nothing 
+haskey′(d::AbstractDict{Int}, k::Int) = haskey(d, k) 
+haskey′(d::AbstractVector, k::Int) = length(d) ≥ k 
+
 Rule(l, r; kw...) = Rule{:DPO}(l, r; kw...) # Assume DPO by default
 ruletype(::Rule{T}) where T = T
 left(r::Rule{T}) where T = r.L
@@ -171,10 +179,10 @@ function can_match(r::Rule{T}, m; homsearch=false, initial=Dict()) where T
       return ("Gluing conditions failed", gc)
     end
 
-    meq = check_match_var_eqs(r, m)
-    if !isempty(meq)
-      return ("Induced attrvar equation failed", meq)
-    end
+    # meq = check_match_var_eqs(r, m)
+    # if !isempty(meq)
+    #   return ("Induced attrvar equation failed", meq)
+    # end
   end
 
   for (nᵢ, N) in enumerate(r.conditions)
@@ -237,17 +245,8 @@ function get_expr_binding_map(r::Rule{T}, m::ACSetTransformation, res) where T
   X = codom(rmap)
   comps = Dict(map(attrtypes(acset_schema(X))) do at 
       bound_vars = Vector{Any}(collect(m[at]))
-      binding = Dict()
-      for prt in parts(X, at)
-        exprs = filter(!isnothing, map(preimage(rmap[at], AttrVar(prt))) do rprt 
-          get(r.exprs[at], rprt, nothing)
-        end)
-        if !isempty(exprs)
-          
-          binding[prt] = only(unique([expr(bound_vars) for expr in exprs]))
-        end 
-      end
-      return at => binding
+      at => Dict(rmap[at](AttrVar(i)).val => xpr(bound_vars) 
+                 for (i, xpr) in r.exprs[at])
   end)
   sub_vars(X, comps)
 end
diff --git a/test/Project.toml b/test/Project.toml
index 3c3089d..63cae83 100644
--- a/test/Project.toml
+++ b/test/Project.toml
@@ -1,4 +1,5 @@
 [deps]
+AlgebraicPetri = "4f99eebe-17bf-4e98-b6a1-2c4f205a959b"
 AlgebraicRewriting = "725a01d3-f174-5bbd-84e1-b9417bad95d9"
 Catlab = "134e5e36-593f-5add-ad60-77f754baafbe"
 DataMigrations = "0c4ad18d-0c49-4bc2-90d5-5bca8f00d6ae"
diff --git a/test/categorical_algebra/CSets.jl b/test/categorical_algebra/CSets.jl
index 0a8f8fc..9b41116 100644
--- a/test/categorical_algebra/CSets.jl
+++ b/test/categorical_algebra/CSets.jl
@@ -1,8 +1,5 @@
 module TestCSets
-using Test
-using Catlab, Catlab.Graphs, Catlab.CategoricalAlgebra
-using AlgebraicRewriting
-
+using Test, Catlab, AlgebraicRewriting
 
 # Pushout complement 
 ####################
@@ -34,8 +31,8 @@ G = @acset LSet begin X=2; f=[:x,:y] end
 f = homomorphism(I,G; initial=(X=[1],))
 
 kg = last(pushout_complement(id(I),f))
-@test dom(kg) == @acset LSet begin X=2; D=1; f=[AttrVar(1),:y] end
-@test collect(kg[:D]) == [:x]
+@test dom(kg) == @acset LSet begin X=2; f=[:x,:y] end
+@test nparts(kg|> dom, :D) == 0
 
 # Slices 
 ########
diff --git a/test/incremental/IncrementalCC.jl b/test/incremental/IncrementalCC.jl
index c27649a..c2d6c57 100644
--- a/test/incremental/IncrementalCC.jl
+++ b/test/incremental/IncrementalCC.jl
@@ -220,17 +220,16 @@ rewrite!(hset, Rule(id(I), r), m)
 @present SchLSet(FreeSchema) begin X::Ob; D::AttrType; f::Attr(X,D) end
 @acset_type LSet(SchLSet){Symbol}
 rep = @acset LSet begin X=1; D=1; f=[AttrVar(1)] end # representable X
-X = @acset LSet begin X=1; f=[:X] end
-Y = @acset LSet begin X=1; f=[:Y] end
-to_X, to_Y = homomorphism.(Ref(rep),[X,Y]);
+rep2 = @acset LSet begin X=2;D=1;f=[AttrVar(1),AttrVar(1)] end
+start = @acset LSet begin X=1; f=[:X] end
 
-hset = IncHomSet(X, [to_X, to_Y], X);
-@test isempty(hset.static.overlaps[to_Y]) # Y cannot generate new matches
-@test length(hset.static.overlaps[to_X])==1
+f = homomorphism(rep, rep2; any=true)
+hset = IncHomSet(start, [f], start);
+@test length(hset.static.overlaps[f])==1
 @test length(keys(hset)) == 1;
-rewrite!(hset, Rule(to_X,to_Y))
+rewrite!(hset, Rule(id(rep), f))
 validate(hset)
-rewrite!(hset, Rule(to_Y,to_X))
+rewrite!(hset, Rule(id(rep), f))
 validate(hset)
 
 end # module
diff --git a/test/rewrite/DPO.jl b/test/rewrite/DPO.jl
index b436a5b..24b81ab 100644
--- a/test/rewrite/DPO.jl
+++ b/test/rewrite/DPO.jl
@@ -172,29 +172,23 @@ z_ = @acset UndirectedBipartiteGraph begin
   V₁=2; V₂=2; E=3; src= [1,2,2]; tgt= [1,1,2]
 end
 
-line = UndirectedBipartiteGraph()
-add_vertices₁!(line, 1)
-add_vertices₂!(line, 2)
-add_edges!(line, [1], [1])
-
-parallel = UndirectedBipartiteGraph()
-add_vertices₁!(parallel, 2)
-add_vertices₂!(parallel, 2)
-add_edges!(parallel, [1,2], [1,2])
-
-merge = UndirectedBipartiteGraph()
-add_vertices₁!(merge, 2)
-add_vertices₂!(merge, 2)
-add_edges!(merge, [1,2], [1,1])
-
-Lspan = UndirectedBipartiteGraph()
-add_vertices₁!(Lspan, 1)
-add_vertices₂!(Lspan, 2)
-add_edges!(Lspan, [1,1],[1,2])
-
-I = UndirectedBipartiteGraph()
-add_vertices₁!(I, 1)
-add_vertices₂!(I, 2)
+line = @acset UndirectedBipartiteGraph begin 
+  V₁=1; V₂=2; E=1; src=[1]; tgt=[1] 
+end
+
+parallel =  @acset UndirectedBipartiteGraph begin 
+  V₁=2; V₂=2; E=2; src=[1,2]; tgt=[1,2] 
+end
+
+merge = @acset UndirectedBipartiteGraph begin 
+  V₁=2; V₂=2; E=2; src=[1,2]; tgt=[1,1] 
+end
+
+Lspan =  @acset UndirectedBipartiteGraph begin 
+  V₁=1; V₂=2; E=2; src=[1,1]; tgt=[1,2] 
+end
+
+I =  @acset UndirectedBipartiteGraph begin V₁=1; V₂=2; end
 
 L = ACSetTransformation(I, Lspan, V₁=[1], V₂=[1,2])
 R = ACSetTransformation(I, line, V₁=[1], V₂=[1,2])
@@ -219,11 +213,8 @@ end
 
 quadrangle = @acset SSet begin
     T=2; E=5; V=4
-    d1=[1,1]
-    d2=[2,3]
-    d3=[4,5]
-    src=[1,1,1,2,3]
-    tgt=[4,2,3,4,4]
+    d1=[1,1]; d2=[2,3]; d3=[4,5]
+    src=[1,1,1,2,3];  tgt=[4,2,3,4,4]
 end
 
 L = quadrangle  # We defined quadrilateral above.
@@ -234,11 +225,8 @@ I = @acset SSet begin
 end
 R = @acset SSet begin
   T=2; E=5; V=4
-  d1=[2,3]
-  d2=[1,5]
-  d3=[5,4]
-  src=[1,1,2,3,2]
-  tgt=[2,3,4,4,3]
+  d1=[2,3]; d2=[1,5]; d3=[5,4]
+  src=[1,1,2,3,2]; tgt=[2,3,4,4,3]
 end
 edge = @acset SSet begin E=1; V=2; src=[1]; tgt=[2] end
 edge_left = only(homomorphisms(edge, L; initial=Dict([:V=>[1,3]])))
@@ -279,7 +267,7 @@ X = @acset WeightedGraph{Int} begin
 end
 rule = Rule(id(WeightedGraph{Int}()), create(X); freevar=true)
 G = @acset WeightedGraph{Int} begin V=1; E=3; src=1; tgt=1; weight=[10,20,100] end
-G2 = rewrite(rule,G)
+G2 = rewrite(rule, G)
 
 L = @acset WeightedGraph{Int} begin V=2; E=2; Weight=2; src=1; tgt=2; 
                                     weight=AttrVar.(1:2) end
@@ -303,36 +291,5 @@ m = get_matches(rule, G)[1]
 @test rewrite_match(rule, m) == @acset WeightedGraph{Int} begin 
   V=1; E=2; Weight=1; src=1; tgt=1; weight=[AttrVar(1), 100] end
 
-# Rewriting with induced equations between AttrVars in the rule
-#--------------------------------------------------------------
-
-@present SchFoo(FreeSchema) begin X::Ob; D::AttrType; f::Attr(X,D) end
-@acset_type AbsFoo(SchFoo)
-const Foo = AbsFoo{Bool}
-
-L = @acset Foo begin X=2; f=[false, false] end 
-I = @acset Foo begin X=2;D=2; f=AttrVar.(1:2) end 
-R = @acset Foo begin X=2; f=[false, true]end 
-rule = Rule(homomorphism(I, L; initial=(X=1:2,)), 
-            homomorphism(I, R; initial=(X=1:2,)))
-
-# we cannot match both X of L to the same part in G because this would yield 
-# an inconsistent result
-@test length(get_matches(rule, L)) == 2
-m = get_matches(rule, L)[1]
-res = rewrite_match(rule, m)
-@test is_isomorphic(res, R)
-
-# Now with arbitrary functions
-
-rule = Rule(I; expr=(D=[((x₁, x₂),) -> x₁ && x₂, ((x₁, x₂),) -> x₁ ≤ x₂],))
-
-# We can match (1,2) and (2,1) no matter what because those impose no constraints
-# (1,1) and (2,2) do unify the variables of the rule, so it is only a valid 
-# match if the two expressions evaluate to the same value. Because ⊥∧⊥ ≠ ⊥⟹⊥
-# (whereas ⊤∧⊤ = ⊤⟹⊤), the only match where both X's are mapped to a single 
-# value is the case where they are mapped to the one with the attribute ⊤.
-@test collect.(getindex.(components.(get_matches(rule, R)), :X)) == [[1,2],[2,1],[2,2]]
-
 
 end # module 
diff --git a/test/rewrite/Inplace.jl b/test/rewrite/Inplace.jl
index fefba9b..3855ef6 100644
--- a/test/rewrite/Inplace.jl
+++ b/test/rewrite/Inplace.jl
@@ -29,7 +29,7 @@ Pat = mk_switch()
 # toggle rule 
 flip(xs) = !only(xs)
 
-toggle = Rule(id(Pat), id(Pat); expr=(State=[flip],))
+toggle = Rule(create(Pat), create(Pat); expr=(State=[flip],))
 
 # Apply rewrite
 prog = compile_rewrite(toggle)
@@ -38,7 +38,7 @@ prog = compile_rewrite(toggle)
 
 m= homomorphism(Pat, T)
 rewrite_match!(toggle, m; prog);
-@test T == F
+@test is_isomorphic(T, F)
 
 
 # Sum parallel edges of Weighted Graph 
diff --git a/test/runtests.jl b/test/runtests.jl
index aa60e64..4bcdb81 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -3,15 +3,19 @@ using Test
 # Test package extension loading
 using AlgebraicRewriting
 @test length(methods(view_traj)) == 1
-@test length(methods(Rule)) == 2
+@test length(methods(Rule)) == 1
 using Luxor
 @test length(methods(view_traj)) > 1
 using DataMigrations
-@test length(methods(Rule)) > 2
+@test length(methods(Rule)) > 1
 
 # Demos
 #######
 
+@testset "Full Demo" begin
+  include("../docs/literate/full_demo.jl")
+end
+
 @testset "Lotka Volterra" begin
   include("../docs/literate/lotka_volterra.jl")
 end
diff --git a/test/schedules/Eval.jl b/test/schedules/Eval.jl
index e398600..0530172 100644
--- a/test/schedules/Eval.jl
+++ b/test/schedules/Eval.jl
@@ -125,97 +125,6 @@ sched = for_schedule(maybe_add_loop ⋅ merge_wires(g1), 3);
 view_sched(sched)
 interpret!(sched, id(g1)) |> codom
 
-
-# Simple game of life 
-#####################
-@present SchLifeGraph <: SchGraph begin # inherit Graph schema
-  Cell::Ob
-  (Life, Eng)::AttrType
-  (cell_W,cell_E,cell_S,cell_N)::Hom(Cell, E)
-  live::Attr(Cell, Life)
-  eng::Attr(Cell, Eng)
-end
-@acset_type AbsLifeGraph(SchLifeGraph, part_type=BitSetParts)
-const LG = AbsLifeGraph{Bool,Int}
-
-"""
-ASCII example
-"""
-function view_life(X::LG, path=tempname())
-  coords, n, m = get_coords(X)
-  mat = pretty_table(String, reduce(hcat,map(1:n) do i 
-    map(1:m) do j 
-      l = X[coords[(i,j)],:live] ? "O" : "X"
-      return "$(l)$(X[coords[(i,j)],:eng])"
-    end
-  end); show_header=false, tf=tf_markdown)
-  open(path, "w") do io write(io, mat) end
-  return mat
-end
-
-"""Assume it's rectangular"""
-function get_coords(X::LG)
-  res = Union{Nothing,Tuple{Int,Int}}[nothing for _ in parts(X,:Cell)]
-  function get_coord!(c)
-    if !isnothing(res[c]) return res[c] end 
-    n_e, w_e = [X[c, Symbol("cell_$s")] for s in "NW"]
-    neighbor_n = incident(X, n_e, :cell_S)
-    if !isempty(neighbor_n)
-      i, j = get_coord!(only(neighbor_n))
-      res[c] = (i+1,j)
-      return res[c]
-    else
-      neighbor_w = incident(X, w_e, :cell_E)
-      if !isempty(neighbor_w)
-        i, j = get_coord!(only(neighbor_w))
-        res[c] = (i,j+1)
-        return res[c]
-      else
-        res[c] = (1,1)
-        return res[c]
-      end
-    end 
-  end
-  get_coord!.(parts(X, :Cell))
-  n, m = [maximum(f.(res)) for f in [first,last]]
-  return Dict(v=>i for (i,v) in enumerate(res)), n, m
-end
-
-# A generic cell
-Cell = @acset LG begin Cell=1; V=4; E=4; Life=1; Eng=1
-  src=[1,1,2,3]; tgt=[2,3,4,4]; live=[AttrVar(1)]; eng=[AttrVar(1)] 
-  cell_S=1; cell_W=2; cell_E=3; cell_N=4
-end 
-
-# Rule which updates eastern neighbor of a live cell to have +1 eng
-inc_E_ = @acset LG begin Cell=2; V=6; E=7; Life=1; Eng=2
-  src=[1,1,2,2,3,4,5]; tgt=[2,4,3,5,6,5,6]; 
-  cell_W=[2,4]; cell_E=[4,5]; cell_S=[1,3]; cell_N=[6,7]
-  live=[true,AttrVar(1)]; eng=AttrVar.(1:2)
-end
-inc_E = Rule(id(inc_E_), id(inc_E_); expr=(Eng=[es->es[1],es->es[2]+1],))
-inc_E_rule = RuleApp(
-  :incE, inc_E, homomorphism(Cell, inc_E_; initial=(V=[1,2,4,5],))) |> tryrule
-
-# Assemble a schedule 
-sched = agent(inc_E_rule, Cell, ret=Cell)
-
-
-# Demonstrate on a 2 x 2 grid:  L D
-#                               L D
-G = @acset LG begin Cell=4; V=9; E=12
-  src=[1,1,2,2,3,4,4,5,5,6,7,8]; tgt=[2,4,3,5,6,5,7,6,8,9,8,9]; 
-  cell_W=[2,4,7,9]; cell_E=[4,5,9,10]; cell_S=[1,3,6,8]; cell_N=[6,8,11,12]
-  live=[true,false,true,false]; eng=[1,10,100,1000]
-end
-
-traj = interpret(sched, G)
-view_traj(sched, traj, view_life; agent=false)
-
-res = codom(last(traj)[1])
-expected = deepcopy(G)
-expected[:eng] = [1,11,100,1001] # the dead cells get +1
-
-@test is_isomorphic(res, expected)
+# TODO add an attributed example
 
 end # module

From 56dddeae340b661735d019fe49b802306b98b33c Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Fri, 19 Jul 2024 14:25:34 -0700
Subject: [PATCH 2/2] change L name

---
 docs/literate/game_of_life.jl | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/docs/literate/game_of_life.jl b/docs/literate/game_of_life.jl
index 309f53b..380a37d 100644
--- a/docs/literate/game_of_life.jl
+++ b/docs/literate/game_of_life.jl
@@ -315,9 +315,9 @@ view_sched(next_step)
 
 life(n::Int) = for_schedule(update_next ⋅ next_step, n) |> F
 
-const L = life(1) # Game of life simulation that runs just one (global) timestep
+const L1 = life(1) # Game of life simulation that runs just one (global) timestep
 
-view_sched(L)
+view_sched(L1)
 
 # ## Running the simulation
 
@@ -331,11 +331,11 @@ view_life_graph(G)
 view_life(G) |> println
 
 # Run the simulation
-res = interpret(L, G; maxstep=1000);
+res = interpret(L1, G; maxstep=1000);
 
 # Look at the end state
 
 res[end][1] |> codom |> view_life |> println
 
 # Visualize the results in the `traj` folder
-view_traj(L, res[1:10], view_life; agent=true)
+view_traj(L1, res[1:10], view_life; agent=true)