Merge pull request #71 from AlgebraicJulia/schema_eqs

Updates for equations in schema

Project.toml

@@ -2,7 +2,7 @@ name = "AlgebraicRewriting"
 uuid = "725a01d3-f174-5bbd-84e1-b9417bad95d9"
 license = "MIT"
 authors = ["Kris Brown <[email protected]>"]
-version = "0.3.4"
+version = "0.3.5"
 
 [deps]
 ACSets = "227ef7b5-1206-438b-ac65-934d6da304b8"
@@ -24,8 +24,8 @@ AlgebraicRewritingLuxorExt = "Luxor"
 AlgebraicRewritingDataMigrationsExt = "DataMigrations"
 
 [compat]
-ACSets = "0.2.9"
-Catlab = "0.16.7"
+ACSets = "0.2.20"
+Catlab = "0.16.11"
 DataMigrations = "0.0.3"
 DataStructures = "0.17, 0.18"
 Reexport = "^1"

src/categorical_algebra/CSets.jl

@@ -163,18 +163,17 @@ 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.
-  components = NamedTuple(Dict(map(ob(S)) do o 
+  comps = NamedTuple(Dict(map(ob(S)) do o 
       o => pushout_complement(ComposablePair(l[o], m[o]))
   end))
-  k_components = Dict{Symbol,Any}(pairs(map(first, components)))
-  g_components = Dict{Symbol,Any}(pairs(map(last, components)))
+  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)))
@@ -190,14 +189,20 @@ function pushout_complement(pair::ComposablePair{<:ACSet, <:TightACSetTransforma
     end
     T = Union{AttrVar, attrtype_type(G, at)}
     g_components[at] = Vector{T}(map(parts(K, at)) do v
-      f, o, val = var_reference(K, at, v)
-      G[g_components[o](val), f]
+      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](AttrVar(l[at](vᵢ)))
+      end 
     end)
   end
 
   k = ACSetTransformation(I, K; k_components...)
   g = ACSetTransformation(K, G; g_components...)
-  force(compose(k,g)) == force(compose(l, m)) || error("Square doesn't commute")
+  kg, lm = force.(compose.([k,l], [g, m]))
+  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)

src/incremental/Algorithms.jl

@@ -55,9 +55,9 @@ Find all partial maps from the pattern to the addition, with some restrictions:
    mapped to newly added material
 """
 function compute_overlaps(L::ACSet, I_R::ACSetTransformation; monic=[],   
-                          S=nothing)::Vector{Span}
+                         )::Vector{Span}
   overlaps = Span[]
-  for subobj in all_subobjects(L, S)
+  for subobj in all_subobjects(L)
     abs_subobj = abstract_attributes(dom(subobj))  
     for h in homomorphisms(dom(abs_subobj), codom(I_R); monic)
       lft = abs_subobj ⋅ subobj
@@ -227,8 +227,8 @@ Compute and cache the subobject classifier; reuse if already computed.
 Some schemas have no finitely presentable subobject classifier. Return `nothing` 
 in that case.
 """
-function subobject_cache(T::Type, S=nothing; cache="cache")
-  S = deattr(isnothing(S) ? Presentation(T) : S)
+function subobject_cache(T::Type; cache="cache")
+  S = deattr(Presentation(T))
   T = AnonACSetType(Schema(S))
   name = joinpath(cache,"Ω_$(nameof(T))_$(pres_hash(S)).json")
   mkpath(cache)
@@ -238,7 +238,7 @@ function subobject_cache(T::Type, S=nothing; cache="cache")
     return read_json_acset(T, name)
   else 
     try 
-      Ω = first(subobject_classifier(T, S))
+      Ω = first(subobject_classifier(T))
       write_json_acset(Ω, name)
       return Ω  
     catch e 
@@ -262,10 +262,10 @@ function to_subobj(f::ACSetTransformation)
 end
 
 """Get all subobjects as monos into X"""
-function all_subobjects(X::ACSet, S=nothing; cache="cache")
-  Ω = subobject_cache(typeof(X), S; cache) 
+function all_subobjects(X::ACSet; cache="cache")
+  Ω = subobject_cache(typeof(X); cache) 
   isnothing(Ω) && return hom.(subobject_graph(X)[2]) # compute the slow way
-  S = isnothing(S) ? acset_schema(X) : Schema(S)
+  S = acset_schema(X)
   X′ = typeof(Ω)()
   copy_parts!(X′, X)
   return map(homomorphisms(X′, Ω; alg=VMSearch())) do h

src/incremental/Cast.jl

@@ -53,8 +53,7 @@ Automatically determine whether one creates an IncCC or an IncHom.
 not one. Having any constraints will also force it to be treated as a single CC.
 """
 function IncHomSet(pattern::ACSet, additions::Vector{<:ACSetTransformation}, 
-                   state::ACSet; single=false, monic=false, pac=[], nac=[], 
-                   S=nothing)
+                   state::ACSet; single=false, monic=false, pac=[], nac=[])
   obs = ob(acset_schema(pattern))
   monic = monic isa Bool ? (monic ? obs : []) : monic
   pac, nac = PAC.(pac), NAC.(nac)
@@ -65,12 +64,12 @@ function IncHomSet(pattern::ACSet, additions::Vector{<:ACSetTransformation},
   coprod, iso = connected_acset_components(pattern)
   single = single || !isempty(constr)
   if single || length(coprod) == 1
-    stat = IncCCStatic(pattern, constr, additions, S)
+    stat = IncCCStatic(pattern, constr, additions)
     runt = IncCCRuntime(pattern, state, constr)
     return IncCCHomSet(stat, runt, constr)
   else 
     pats = dom.(coprod.cocone)
-    ccs = IncCCHomSet.(IncCCStatic.(pats, Ref(constr), Ref(additions), Ref(S)), 
+    ccs = IncCCHomSet.(IncCCStatic.(pats, Ref(constr), Ref(additions)), 
                        IncCCRuntime.(pats, Ref(state), Ref(constr)), 
                        Ref(constr))
     stat = IncSumStatic(pattern, coprod, iso, static.(ccs))
@@ -86,16 +85,16 @@ Initialize an Incremental hom set from a rule, using it's pattern `L` as the
 domain of the hom set. Any additions other than the map `I->R` can be passed in
 by `additions`, and the schema Presentation can be passed as `S`.
 """
-function IncHomSet(rule::Rule{T}, state::ACSet, additions=ACSetTransformation[], 
-                   S=nothing) where T
+function IncHomSet(rule::Rule{T}, state::ACSet, additions=ACSetTransformation[]
+                  ) where T
   pac, nac = [], []
   dpo = (T == :DPO) ? [left(rule)] : ACSetTransformation[]
   right(rule) ∈ additions || push!(additions, right(rule))
-  for c in AC.(rule.conditions, Ref(additions), Ref(dpo), Ref(S))
+  for c in AC.(rule.conditions, Ref(additions), Ref(dpo))
     c isa PAC && push!(pac, c)
     c isa NAC && push!(nac, c)
   end
-  IncHomSet(codom(left(rule)), additions, state; monic=rule.monic, pac, nac, S)
+  IncHomSet(codom(left(rule)), additions, state; monic=rule.monic, pac, nac)
 end
 
 

src/incremental/IncrementalCC.jl

@@ -24,9 +24,8 @@ have constraints forcing it to be treated all at once instead of componentwise.
 @struct_hash_equal struct IncCCStatic <: IncStatic
   pattern::ACSet
   overlaps::Dict{ACSetTransformation, Vector{Span}}
-  S::Union{Nothing, Presentation}
-  function IncCCStatic(pattern::ACSet, constr::IncConstraints, adds=[], S=nothing)
-    hs = new(pattern, Dict(), S)
+  function IncCCStatic(pattern::ACSet, constr::IncConstraints, adds=[])
+    hs = new(pattern, Dict())
     push!.(Ref(hs), Ref(constr,), adds)
     return hs 
   end
@@ -38,8 +37,7 @@ additions(h::IncCCStatic) = collect(keys(h.overlaps))
 function Base.push!(hs::IncCCStatic, constr::IncConstraints, 
                     addition::ACSetTransformation)
   haskey(hs.overlaps, addition) && return nothing
-  hs.overlaps[addition]=compute_overlaps(pattern(hs), addition; constr.monic, 
-                                         S=hs.S)
+  hs.overlaps[addition]=compute_overlaps(pattern(hs), addition; constr.monic)
 end
 
 """

src/incremental/IncrementalConstraints.jl

@@ -26,11 +26,11 @@ abstract type AC end
 Coerce a general `Constraint` into a simple application condition, if possible. 
 This works if the `Constraint` was created by `AppCond`.
 """
-function AC(c::Constraint, addns=[], dpo=[], S=nothing)
+function AC(c::Constraint, addns=[], dpo=[])
   m, expr = c.g[1,:elabel], c.d
   monic = expr isa BoolNot ? expr.expr.monic : expr.monic
-  AppCond(m; monic) == c && return PAC(m, addns, monic, S)
-  AppCond(m, false; monic) == c && return NAC(m, monic, dpo, S)
+  AppCond(m; monic) == c && return PAC(m, addns, monic)
+  AppCond(m, false; monic) == c && return NAC(m, monic, dpo)
   return nothing
 end
 
@@ -57,10 +57,10 @@ sent to something that is deleted (part of L/I).
   m_complement::ACSetTransformation
   subobj::Vector{ACSetTransformation}
   overlaps::Dict{ACSetTransformation, Vector{Span}}
-  function NAC(m, monic, dpos, S=nothing)
+  function NAC(m, monic, dpos)
     m_comp = hom(~Subobject(m))
-    subobjs = all_subobjects(dom(m_comp), S)
-    subobjs_L = all_subobjects(dom(m), S)
+    subobjs = all_subobjects(dom(m_comp))
+    subobjs_L = all_subobjects(dom(m))
     Ob = ob(acset_schema(dom(m)))
     part_N = partition_image(m)
     overlaps = Dict(map(dpos) do dpo
@@ -84,8 +84,8 @@ end
 
 NAC(n::NAC) = n
 
-NAC(m::ACSetTransformation, b::Bool=false, dpo=[], S=nothing) = 
-  NAC(m, b ? ob(acset_schema(dom(m))) : [], dpo, S)
+NAC(m::ACSetTransformation, b::Bool=false, dpo=[]) = 
+  NAC(m, b ? ob(acset_schema(dom(m))) : [], dpo)
 
 """
 A positive application condition L -> P means a match L -> X is valid only if 
@@ -102,17 +102,17 @@ addition could intersect with P.
   m_complement::ACSetTransformation
   overlaps::Dict{ACSetTransformation, Vector{Span}}
   function PAC(m::ACSetTransformation, additions::Vector{<:ACSetTransformation}, 
-               monic::Vector{Symbol}, S=nothing)
+               monic::Vector{Symbol})
     newP = hom(~Subobject(m))
     new(m, monic, newP, 
-        Dict(a => compute_overlaps(dom(newP), a; monic, S) for a in additions))
+        Dict(a => compute_overlaps(dom(newP), a; monic) for a in additions))
   end
 end
 
 PAC(p::PAC) = p
 
-PAC(m::ACSetTransformation, additions=ACSetTransformation[], b::Bool=false, S=nothing) = 
-  PAC(m, additions, b ? ob(acset_schema(dom(m))) : Symbol[], S)
+PAC(m::ACSetTransformation, additions=ACSetTransformation[], b::Bool=false) = 
+  PAC(m, additions, b ? ob(acset_schema(dom(m))) : Symbol[])
 
 
 

src/rewrite/Migration.jl

@@ -40,8 +40,8 @@ schema changes. This minimizes the need to clear the cache.
 """
 pres_hash(p::Presentation) = "$(hash(p.generators))_$(hash(p.equations))"
 
-function repr_dict(T::Type,S=nothing; clear=false, cache="cache")
-  S = isnothing(S) ? Presentation(T) : S
+function repr_dict(T::Type; clear=false, cache="cache")
+  S = Presentation(T)
   tname = "$(nameof(T))_$(pres_hash(S))"
   Dict{Symbol,Tuple{T,Int}}(map(generators(S, :Ob)) do ob
     name = nameof(ob)
@@ -51,15 +51,15 @@ function repr_dict(T::Type,S=nothing; clear=false, cache="cache")
       (read_json_acset(T, path), parse(Int,open(io->read(io, String), ipath)))
     else 
       @debug "Computing representable $name"
-      rep, i = representable(T, S, name; return_unit_id=true)
+      rep, i = representable(T, name; return_unit_id=true)
       write_json_acset(rep, path)
       write(ipath, string(i))
       (rep, i)
     end
   end)
 end
 
-yoneda_cache(T::Type,S=nothing; clear=false, cache="cache") = 
-  yoneda(T; cache=repr_dict(T, S; clear, cache))
+yoneda_cache(T::Type; clear=false, cache="cache") = 
+  yoneda(T; cache=repr_dict(T; clear, cache))
 
 end # module 

test/incremental/Algorithms.jl

@@ -29,7 +29,7 @@ so_wg = all_subobjects(wg)
 
 # Mini benchmark
 G = SymmetricGraph(3) ⊕ cycle_graph(SymmetricGraph, 3)
-@time x1 = all_subobjects(G, SchSymmetricGraph);
+@time x1 = all_subobjects(G);
 @time x2 = subobject_graph(G)[2]; # should be much longer than all_subobjects
 @test length(x1) == length(x2) # yet give same result