Visualize constraints

docs/Project.toml

@@ -10,3 +10,7 @@ Luxor = "ae8d54c2-7ccd-5906-9d76-62fc9837b5bc"
 PrettyTables = "08abe8d2-0d0c-5749-adfa-8a2ac140af0d"
 Revise = "295af30f-e4ad-537b-8983-00126c2a3abe"
 StructEquality = "6ec83bb0-ed9f-11e9-3b4c-2b04cb4e219c"
+
+[compat]
+ACSets = "0.2.6"
+Catlab = "0.15.5"

src/categorical_algebra/CSets.jl

@@ -376,27 +376,6 @@ function sub_vars(X::ACSet, subs::AbstractDict)
   return first(legs(pushout(ox, oc)))
 end 
 
-# """
-# For any ACSet, X, a canonical map A→X where A has distinct variables for all
-# subparts.
-# """
-# function abstract(X::StructACSet{S,Ts}; check::Bool=false) where {S,Ts} 
-#   A = deepcopy(X); 
-#   comps = Dict{Any,Any}(map(attrtypes(S)) do at
-#     rem_parts!(A, at, parts(A,at))
-#     comp = Union{AttrVar,attrtype_instantiation(S,Ts,at)}[]
-#     for (f, d, _) in attrs(S; to=at)
-#       append!(comp, A[f])
-#       A[f] = AttrVar.(add_parts!(A, at, nparts(A,d)))
-#     end 
-#     at => comp
-#   end)
-#   for o in ob(S) comps[o]=parts(X,o) end
-#   res = ACSetTransformation(A,X; comps...)
-#   !check || is_natural(res) || error("bad abstract $comps")
-#   return res
-# end 
-
 
 """
 Take an ACSet pullback combinatorially and freely add variables for all 

src/rewrite/Constraints.jl

@@ -2,9 +2,10 @@
 export apply_constraint, Constraint, CGraph, arity,
        ∀, ∃, ∃!, True, False, Commutes,
        AppCond, LiftCond, Trivial
-using Catlab, Catlab.CategoricalAlgebra, Catlab.Graphs
+using Catlab
 import Catlab.Theories: ⊗, ⊕
 import Catlab.CategoricalAlgebra: ¬
+import Catlab.Graphics: to_graphviz
 using StructEquality
 import ...CategoricalAlgebra.CSets: Migrate
 
@@ -43,7 +44,7 @@
 Ints are explicit arguments provided when apply_constraint is called
 """
 const CGraph = VELabeledGraph{Union{Nothing, ACSet},
-                              Union{Nothing,Int, ACSetTransformation}}
+                              Union{Nothing, Int, ACSetTransformation}}
 
 """Number of variables in a constraint graph"""
 arity(g::CGraph) = maximum(filter(v->v isa Int, g[:elabel]); init=0) 
@@ -113,13 +114,15 @@
 # Interpreter for boolean algebra
 #################################
 const Assgn = Vector{Union{Nothing, <:ACSetTransformation}} # partial assignment
+paren(x) = "($x)" 
 
 """Something that, in a context, can be evaluated to a bool"""
 abstract type BoolExpr end 
 check_expr(::CGraph, ::BoolExpr) = error("Method undefined")
 bound(::BoolExpr) = error("Method undefined")
 eval_boolexpr(::BoolExpr, ::CGraph, ::Assgn) = error("Method undefined")
 map_edges(f,c::BoolExpr) = error("Method undefined")
+subexprs(::BoolExpr) = error("Method undefined")
 
 """
 A commutative diagram with multiple parallel paths, asserted to either 
@@ -134,10 +137,17 @@
   end
 end
 
+subexprs(::Commutes) = BoolExpr[]
+Base.show(io::IO, c::Commutes) =
+  join(io, [join(p, "⋅") for p in c.pths], c.commutes ? " = " : " ≠ ")
+
 """Constant, independent of context"""
 @struct_hash_equal struct BoolConst <: BoolExpr 
   val::Bool
 end 
+Base.show(io::IO, c::BoolConst) = print(io, c.val ? "⊤" : "⊥")
+subexprs(::BoolConst) = BoolExpr[]
+
 const True = BoolConst(true)
 const False = BoolConst(false)
 
@@ -159,6 +169,27 @@
     k ∈ [:Exists,:Forall,:Exists!] ? new(e,k,x,st,monic) : error("$k not supported")
 end
 
+quantifier_symbol(c::Quantifier) = if     c.kind == :Exists  "∃"
+                                   elseif c.kind == :Forall  "∀"
+                                   elseif c.kind == :Exists! "∃!"
+                                   end
+
+function Base.show(io::IO, c::Quantifier)
+  q = quantifier_symbol(c)
+  m = if c.monic isa AbstractVector
+    "monic{$(join(c.monic, ","))}, "
+  elseif c.monic 
+    "monic, "
+  else
+    ""
+  end
+  st = c.st == True ? "" : paren(c.st)
+  mst = isempty(m*st) ? "" : " $(paren(m*st))"
+  x = c.expr == True && c.kind ∈ [:Exists, :Exists!] ? "" : ": $(paren(c.expr))"
+  print(io, join([q,c.e,mst,x]))
+end
+subexprs(q::Quantifier) = [q.expr, q.st]
+
 Exists!(e,x;st=True,monic=false) = Quantifier(e,:Exists,x;st=st,monic=monic)
 Forall(e,x;st=True,monic=false) = Quantifier(e,:Forall,x;st=st,monic=monic)
 Exists(e,x;st=True,monic=false) = Quantifier(e,:Exists,x;st=st,monic=monic)
@@ -169,23 +200,42 @@
 """Disjunction of multiple expressions"""
 @struct_hash_equal struct BoolOr <: BoolExpr 
   exprs::Vector{BoolExpr}
-  BoolOr(x...) = new(collect(x))
-end 
+  BoolOr(x...) = new(collect(filter(!=(False),x)))
+end
+
+Base.show(io::IO, b::BoolOr) = 
+  if isempty(b.exprs) 
+    print(io, False)
+  else 
+    join(io, paren.(b.exprs), " ∨ ")
+  end
+
+subexprs(b::BoolOr) = b.exprs
 
 ⊕(xs::BoolExpr...) = BoolOr(xs...)
 
 """Conjunction of multiple expressions"""
 @struct_hash_equal struct BoolAnd <: BoolExpr 
   exprs::Vector{BoolExpr}
-  BoolAnd(x...) = new(collect(x))
-end 
+  BoolAnd(x...) = new(collect(filter(!=(True),x)))
+end
+
+Base.show(io::IO, b::BoolAnd) = 
+  if isempty(b.exprs) 
+    show(io, True)
+  else 
+    join(io, paren.(b.exprs), " ∧ ")
+  end
+subexprs(b::BoolAnd) = b.exprs
 
 ⊗(xs::BoolExpr...) = BoolAnd(xs...) 
 
 """Negation of an expression"""
 @struct_hash_equal struct BoolNot <: BoolExpr 
   expr::BoolExpr
 end 
+subexprs(b::BoolNot) = [b.expr]
+Base.show(io::IO, b::BoolNot) = print(io, "¬$(b.expr isa Quantifier ? b.expr : paren(b.expr))") 
 
 ¬(x::BoolExpr) = BoolNot(x)
 
@@ -340,10 +390,11 @@
   end  
   new_g = merge_graphs(c1.g, c2.g)
   l1, l2 = legs(new_g)
-  Constraint(apex(new_g), map_edges(l1,c1.d) ⊕ map_edges(l2,c2.d))
+  new_d = map_edges(l1,c1.d) ⊕ map_edges(l2,c2.d)
+  Constraint(apex(new_g), new_d)
 end
 
-⊕(cs::Constraint...) = reduce(⊗, cs; init=Trivial′) 
+⊕(cs::Constraint...) = reduce(⊕, cs; init=Trivial′) 
 
 ¬(c::Constraint) = Constraint(c.g, ¬c.d)
 
@@ -421,4 +472,35 @@
   return Constraint(cg, expr)
 end
 
-end 
+# Visualize constraints
+#######################
+
+function to_graphviz(c::Constraint)
+  pg = to_graphviz_property_graph(c.g; node_labels=true,
+                                  graph_attrs=Dict(:label=>sprint(show, c.d)))
+
+  for v in vertices(c.g)
+    x = isnothing(c.g[v, :vlabel]) ? "λ" : ""
+    set_vprop!(pg, v, :label, "$x$v")
+  end
+
+  for e in edges(c.g)
+    x = if     c.g[e, :elabel] isa Int    "(λ$(c.g[e, :elabel]))"
+        elseif isnothing(c.g[e, :elabel]) getquantifier(c.d, e)
+        else                              ""
+    end 
+    set_eprop!(pg, e, :label, "$x$e")
+  end
+  to_graphviz(pg)
+end
+
+function getquantifier(d::BoolExpr, e::Int)
+  if d isa Quantifier && d.e == e
+    quantifier_symbol(d)
+  else 
+    qs = collect(filter(!isnothing, getquantifier.(subexprs(d), Ref(e))))
+    isempty(qs) ? nothing : only(qs)
+  end
+end
+
+end # module

test/Project.toml

@@ -8,3 +8,7 @@ Random = "9a3f8284-a2c9-5f02-9a11-845980a1fd5c"
 Revise = "295af30f-e4ad-537b-8983-00126c2a3abe"
 StructEquality = "6ec83bb0-ed9f-11e9-3b4c-2b04cb4e219c"
 Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"
+
+[compat]
+ACSets = "0.2.6"
+Catlab = "0.15.5"

test/rewrite/Constraints.jl

@@ -1,6 +1,6 @@
 module TestConstraints 
 using AlgebraicRewriting
-using Catlab, Catlab.CategoricalAlgebra, Catlab.Graphs
+using Catlab
 using Test 
 
 # Testing arity 2 constraints
@@ -12,6 +12,7 @@ c = Constraint(cg, ∃(3, Commutes([1],[2,3])))
 h1, hid, hnot, _ = homomorphisms(Graph.([2,2])...)
 @test !apply_constraint(c, hid, h1)
 @test apply_constraint(c, hid, hnot)
+@test arity(c) == 2
 
 # AppCond 
 #########
@@ -33,6 +34,7 @@ f = homomorphism(p2, G)
 
 @test apply_constraint(constr, f)
 @test !apply_constraint(constr, id(p2))
+to_graphviz(constr)
 
 # LiftCond
 ##########
@@ -78,6 +80,7 @@ h1,h2,h3,h4 = homomorphisms(G, loop_csp; initial=(V=Dict(1=>1),))
 @test !apply_constraint(constr,h2)
 @test !apply_constraint(constr,h3)
 @test apply_constraint(constr,h4)
+to_graphviz(constr)
 
 # Combining constraints
 #######################
@@ -89,5 +92,6 @@ three_loops = @acset Graph begin V=1; E=3; src=1; tgt=1 end
 c2 = AppCond(homomorphism(Graph(1), two_loops); monic=true)
 c3 = AppCond(homomorphism(Graph(1), three_loops); monic=true)
 constr = c2 ⊕ c3
+to_graphviz(constr)
 
 end # module