Incorporating GATlab more deeply

Project.toml

@@ -2,7 +2,7 @@ name = "Catlab"
 uuid = "134e5e36-593f-5add-ad60-77f754baafbe"
 license = "MIT"
 authors = ["Evan Patterson <[email protected]>"]
-version = "0.16.18"
+version = "0.17.1"
 
 [deps]
 ACSets = "227ef7b5-1206-438b-ac65-934d6da304b8"
@@ -36,14 +36,6 @@ MetaGraphs = "626554b9-1ddb-594c-aa3c-2596fe9399a5"
 SCS = "c946c3f1-0d1f-5ce8-9dea-7daa1f7e2d13"
 TikzPictures = "37f6aa50-8035-52d0-81c2-5a1d08754b2d"
 
-[extensions]
-CatlabConvexExt = "Convex"
-CatlabDataFramesExt = "DataFrames"
-CatlabGraphsExt = "Graphs"
-CatlabGraphvizExt = "Graphviz_jll"
-CatlabMetaGraphsExt = "MetaGraphs"
-CatlabSCSExt = "SCS"
-CatlabTikzPicturesExt = "TikzPictures"
 
 [compat]
 ACSets = "0.2.20"

src/theories/Category.jl → src/01_theories/Category.jl

@@ -8,9 +8,10 @@ export ThCategory, FreeCategory, Ob, Hom, dom, codom, id, compose, ⋅,
 # Category
 ##########
 
-# Convenience constructors
-compose(fs::AbstractVector) = foldl(compose, fs)
-compose(f, g, h, fs...) = compose([f, g, h, fs...])
+# Convenience constructors TODO
+compose(f::GATExpr, g::GATExpr, h::GATExpr, fs...) =
+  compose(GATExpr[f, g, h, fs...])
+compose(fs::AbstractVector{<:GATExpr}) = foldl(compose, fs)
 
 @symbolic_model FreeCategory{ObExpr,HomExpr} ThCategory begin
   compose(f::Hom, g::Hom) = associate_unit(new(f,g; strict=true), id)

src/theories/HigherCategory.jl → src/01_theories/HigherCategory.jl

@@ -42,6 +42,10 @@ abstract type CellExpr{T} <: CategoryExpr{T} end
     [A::Ob, B::Ob, C::Ob, g::(B → C), h::(B → C)]
 end
 
+using GATlab.Syntax.TheoryInterface: GAT_MODULE_LOOKUP
+s = gettag(ThCategory2.Meta.theory)
+haskey(GAT_MODULE_LOOKUP, s) || error("BAD")
+
 # Convenience constructors
 composeH(αs::AbstractVector) = foldl(composeH, αs)
 composeH(α, β, γ, αs...) = composeH([α, β, γ, αs...])

src/theories/Monoidal.jl → src/01_theories/Monoidal.jl

@@ -53,9 +53,11 @@ might add a theory for weak monoidal categories later.
 end
 
 # Convenience constructors
-otimes(xs::AbstractVector{T}) where T =
+otimes(xs::AbstractVector{T})where {T<:GATExpr} =
   isempty(xs) ? munit(T) : foldl(otimes, xs)
-otimes(x, y, z, xs...) = otimes([x, y, z, xs...])
+
+otimes(x::GATExpr, y::GATExpr, z::GATExpr, xs...) = 
+  otimes(GATExpr[x, y, z, xs...])
 
 """ Collect generators of object in monoidal category as a vector.
 """

src/theories/MonoidalAdditive.jl → src/01_theories/MonoidalAdditive.jl

@@ -23,9 +23,9 @@ notation.
   mzero()::Ob
 end
 
-# Convenience constructors
-oplus(xs::AbstractVector{T}) where T = isempty(xs) ? mzero(T) : foldl(oplus, xs)
-oplus(x, y, z, xs...) = oplus([x, y, z, xs...])
+# Convenience constructors TODO FIX THIS
+oplus(xs::AbstractVector{T}) where {T<:GATExpr} = isempty(xs) ? mzero(T) : foldl(oplus, xs)
+oplus(x::GATExpr, y::GATExpr, z::GATExpr, xs...) = oplus(GATExpr[x, y, z, xs...])
 
 # Overload `collect` and `ndims` as for multiplicative monoidal categories.
 collect(expr::ObExpr{:oplus}) = vcat(map(collect, args(expr))...)

src/theories/Theories.jl → src/01_theories/module.jl

@@ -45,4 +45,5 @@ include("Preorders.jl")
 include("Relations.jl")
 include("Schema.jl")
 
+
 end

src/03_basic_sets/01_sets/EitherSets.jl

@@ -0,0 +1,55 @@
+module EitherSets 
+
+export EitherSet, Left, Right
+
+using StructEquality
+
+using GATlab
+import GATlab: getvalue
+
+using ..Sets: ThSet′, AbsSet
+import ..UnionSets: left, right
+
+
+""" Wrapper defined in GATlab """
+getvalue(l::Left) = l.val 
+
+""" Wrapper defined in GATlab"""
+getvalue(l::Right) = l.val 
+
+""" 
+Disjoint union type. In order to not conflate values, we need to wrap one 
+of the sets in `Left` and one in `Right`. 
+"""
+@struct_hash_equal struct EitherSet
+  left::AbsSet
+  right::AbsSet
+end
+
+# Accessors
+###########
+
+left(e::EitherSet) = e.left
+
+right(e::EitherSet) = e.right
+
+# ThSet implementation
+######################
+
+@instance ThSet′{Bool, Any} [model::EitherSet] begin
+
+  in′(i::Any)::Bool = if i isa Left 
+    getvalue(i) ∈ left(model) 
+  elseif i isa Right 
+    getvalue(i) ∈ right(model)
+  else 
+    false 
+  end
+
+  eltype()::Any = 
+    Union{Left{eltype(left(model))}, Right{eltype(right(model))}}
+
+end
+
+
+end # module

src/03_basic_sets/01_sets/PredSet.jl

@@ -0,0 +1,45 @@
+module PredSets 
+
+export PredicatedSet
+
+using StructEquality
+
+using GATlab
+
+using ..Sets: SetOb, ThSet′
+
+""" Set defined by a predicate (boolean-valued function) on a Julia data type.
+"""
+@struct_hash_equal struct PredicatedSet{T}
+  predicate::Any
+
+  PredicatedSet{T}(f) where T = new{T}(f)
+end
+
+PredicatedSet(T::Type, f) = PredicatedSet{T}(f)
+
+# Other methods
+###############
+
+
+""" Apply the predicate """
+function (s::PredicatedSet{T})(x::T)::Bool where {T}
+  s.predicate(x)
+end
+
+function Base.show(io::IO, s::PredicatedSet{T}) where T
+  print(io, "PredicatedSet($T, $(nameof(s.predicate)))")
+end
+
+# ThSet implementation 
+######################
+
+@instance ThSet′{Bool, Any} [model::PredicatedSet{T}] where T begin
+
+  in′(i::Any)::Bool = i isa T && model(i)
+
+  eltype()::Any = T
+
+end
+
+end # module

src/03_basic_sets/01_sets/ProdSets.jl

@@ -0,0 +1,43 @@
+module ProdSets 
+
+export ProdSet
+
+using StructEquality, MLStyle
+
+using GATlab
+
+using ..Sets: ThSet′, AbsSet
+
+
+""" 
+Unbiased Cartesian product.
+"""
+@struct_hash_equal struct ProdSet
+  sets::Vector{AbsSet}
+end
+
+GATlab.getvalue(s::ProdSet) = s.sets
+
+# Other methods
+###############
+
+Base.iterate(e::ProdSet, i...) = iterate(getvalue(e), i...)
+
+Base.getindex(e::ProdSet, i) = getvalue(e)[i]
+
+Base.length(e::ProdSet) = length(getvalue(e))
+
+# ThSet implementation
+######################
+
+@instance ThSet′{Bool, Any} [model::ProdSet] begin
+
+  in′(i::Any)::Bool = (i isa Tuple && length(i)==length(model) 
+    && all(e ∈ s for (s, e) in zip(model, i)))
+
+  eltype()::Any = Tuple{eltype.(model)...}
+
+end
+
+
+end # module

src/03_basic_sets/01_sets/Sets.jl

@@ -0,0 +1,38 @@
+export AbsSet, SetOb
+
+using StructEquality
+
+using GATlab
+
+import Base: eltype
+
+# Theory of Sets
+################
+
+"""
+One ought be able to ask of any Set whether something is in it. Also a Julia 
+type should be provided which includes all elements of the set.
+"""
+@theory ThSet′ begin
+  Bool′::TYPE
+  Any′::TYPE
+  in′(e::Any′)::Bool′ # the order of arguments is reversed, so give a diff name
+  eltype()::Any′
+end
+
+""" There are two kinds of Abstract Set. `SetOb` and `FinSet`."""
+abstract type AbsSet end
+
+""" Fix the order of in′ """
+Base.in(x, s::AbsSet) = ThSet′.in′[getvalue(s)](x)
+
+# Wrapper type for Models of ThSet′
+##################################
+"""
+Generic type for a set. It has some implementation of the theory of sets and 
+a model which provides the information for how it implements the theory.
+"""
+ThSet′.Meta.@wrapper SetOb <: AbsSet
+
+Base.show(io::IO, s::SetOb) = show(io, getvalue(s))
+

src/03_basic_sets/01_sets/SumSets.jl

@@ -0,0 +1,82 @@
+module SumSets 
+
+export SumSet, TaggedElem, Tagged, untag
+
+using StructEquality, MLStyle
+
+using GATlab
+
+using ..Sets: ThSet′, AbsSet
+
+
+@struct_hash_equal struct TaggedElem{I, T} 
+  val::T
+  TaggedElem(t::T, i::Int) where T = new{Val{i}, T}(t)
+end 
+
+GATlab.getvalue(l::TaggedElem) = l.val
+
+tag_I(::Type{TaggedElem{I,T}}) where {I,T} = I 
+tag_T(::Type{TaggedElem{I,T}}) where {I,T} = T
+
+""" Untag at the term level """
+untag(l::TaggedElem{I,T}, i::Int) where {I,T} =
+  Val{i} == I  ? l.val : error("Bad untag of $(l.val)::$T: $I ≠ $i")
+
+""" Untag at the type level """
+untag(::Type{TaggedElem{I,T}}, i::Int) where {I,T} = 
+  Val{i} == I ? T :  error("Bad untag of $T: $I ≠ $i")
+
+""" Untag at the type level """
+function untag(::Type{Union{Xs}}, i::Int) where Xs 
+  Xs.a <: TaggedElem || error("Can't untag a $(Xs.a)")
+  tag_I(Xs.a) == Val{i} && return tag_T(Xs.a)
+  return untag(Xs.b, i) # iterate through list of union types
+end
+
+
+getidx(::T) where {T<:TaggedElem} = only(T.parameters[1].parameters)
+
+""" 
+Unbiased disjoint union type. In order to not conflate values, we need to wrap 
+them in `TaggedElem` which adds an integer type parameter.
+"""
+@struct_hash_equal struct SumSet
+  sets::Vector{AbsSet}
+end
+
+GATlab.getvalue(s::SumSet) = s.sets
+
+# Other methods
+###############
+
+Base.iterate(e::SumSet, i...) = iterate(getvalue(e), i...)
+
+Base.getindex(e::SumSet, i) = getvalue(e)[i]
+
+Base.length(e::SumSet) = length(getvalue(e))
+
+# ThSet implementation
+######################
+
+@instance ThSet′{Bool, Any} [model::SumSet] begin
+
+  in′(i::Any)::Bool = @match i begin 
+    (t::TaggedElem) => let i = getidx(t); 
+      0 < i ≤ length(model) && getvalue(t) ∈ model[getidx(t)]
+    end
+    _ => false 
+  end
+
+  eltype()::Any = 
+    Union{[TaggedElem{Val{i}, eltype(s)} for (i, s) in enumerate(model)]...}
+
+end
+
+# Other helpers
+###############
+Tagged(vs::Vector{<:Union{Type,TypeVar}}) = 
+  Union{[TaggedElem{Val{i}, v} for (i,v) in zip(1:length(vs), vs)]...}
+
+
+end # module

src/03_basic_sets/01_sets/TypeSet.jl

@@ -0,0 +1,31 @@
+module TypeSets 
+
+export TypeSet
+
+using StructEquality
+
+using GATlab
+
+using ..Sets: ThSet′
+import ..Sets: SetOb
+
+""" Raw Julia type considered as a set"""
+@struct_hash_equal struct TypeSet{T} end
+
+TypeSet(T::Type) = TypeSet{T}()
+
+Base.show(io::IO, ::TypeSet{T}) where T = print(io, "TypeSet($T)")
+
+# ThSet implementation 
+
+@instance ThSet′{Bool, Any} [model::TypeSet{T}] where T begin
+  in′(i::Any)::Bool = i isa T
+  eltype()::Any = T
+end
+
+# Default model, for convenience
+
+""" Default model for a Set made out of a Julia `Type` """
+SetOb(T::Type) = SetOb(TypeSet{T}())
+
+end # module