Repository: AlgebraicJulia/Catlab.jl
Pull request #224 (2020-08-01 00:26:16)

ENH: trial implementation of DecidableSets
Nobody commented on #223, so I went ahead and implemented it.


Patch:
diff --git a/Project.toml b/Project.toml
index d1b3daf8f..4b4effb3f 100644
--- a/Project.toml
+++ b/Project.toml
@@ -9,6 +9,7 @@ AutoHashEquals = "15f4f7f2-30c1-5605-9d31-71845cf9641f"
 Compat = "34da2185-b29b-5c13-b0c7-acf172513d20"
 Compose = "a81c6b42-2e10-5240-aca2-a61377ecd94b"
 DataStructures = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8"
+FunctionWrappers = "069b7b12-0de2-55c6-9aab-29f3d0a68a2e"
 GeneralizedGenerated = "6b9d7cbe-bcb9-11e9-073f-15a7a543e2eb"
 JSON = "682c06a0-de6a-54ab-a142-c8b1cf79cde6"
 LabelledArrays = "2ee39098-c373-598a-b85f-a56591580800"
diff --git a/src/categorical_algebra/CategoricalAlgebra.jl b/src/categorical_algebra/CategoricalAlgebra.jl
index 153e80973..f891b69be 100644
--- a/src/categorical_algebra/CategoricalAlgebra.jl
+++ b/src/categorical_algebra/CategoricalAlgebra.jl
@@ -7,5 +7,6 @@ include("FinRelations.jl")
 include("Permutations.jl")
 include("CSets.jl")
 include("Graphs.jl")
+include("PredicatedSets.jl")
 
 end
diff --git a/src/categorical_algebra/PredicatedSets.jl b/src/categorical_algebra/PredicatedSets.jl
new file mode 100644
index 000000000..45022a107
--- /dev/null
+++ b/src/categorical_algebra/PredicatedSets.jl
@@ -0,0 +1,58 @@
+module PredicatedSets
+export PredicatedSet,PredicatedHom
+
+import FunctionWrappers
+import FunctionWrappers: FunctionWrapper
+using ...GAT
+using ...Theories
+import ...Theories: id, compose
+
+struct PredicatedSet{T}
+  predicate::FunctionWrapper{Bool,Tuple{T}}
+  PredicatedSet(T::DataType,f::Function) = new{T}(FunctionWrapper{Bool,Tuple{T}}(f))
+end
+
+function (t::PredicatedSet{T})(x::T)::Bool where {T}
+  t.predicate(x)
+end
+
+basetype(t::PredicatedSet{T}) where {T} = T
+
+struct PredicatedHom{T,S}
+  dom::PredicatedSet{T}
+  codom::PredicatedSet{S}
+  f::FunctionWrapper{S,Tuple{T}}
+  PredicatedHom(dom::PredicatedSet{T},codom::PredicatedSet{S},f) where {T,S} =
+    new{T,S}(dom,codom,FunctionWrapper{S,Tuple{T}}(f))
+end
+
+function (f::PredicatedHom{T,S})(x::T)::S where {T,S}
+  @assert f.dom(x)
+  y = f.f(x)
+  @assert f.codom(y)
+  y
+end
+
+function compose(f::PredicatedHom{T,S},g::PredicatedHom{S,U}) where {T,S,U}
+  function h(x)
+    y = f.f(x)
+    @assert f.codom(y)
+    @assert g.dom(y)
+    g.f(y)
+  end
+  PredicatedHom(f.dom,g.codom,h)
+end
+
+# This is really the category of decidable sets and partial functions...
+@instance Category(PredicatedSet, PredicatedHom) begin
+  dom(f::PredicatedHom) = f.dom
+  codom(f::PredicatedHom) = f.codom
+
+  id(t::PredicatedSet) = PredicatedHom(t,t,x->x)
+  compose(f::PredicatedHom,g::PredicatedHom) = begin
+    @assert basetype(f.codom) == basetype(g.dom)
+    compose(f,g)
+  end
+end
+
+end


Test patch:
diff --git a/test/categorical_algebra/CategoricalAlgebra.jl b/test/categorical_algebra/CategoricalAlgebra.jl
index f5d89ea97..bb4aadb21 100644
--- a/test/categorical_algebra/CategoricalAlgebra.jl
+++ b/test/categorical_algebra/CategoricalAlgebra.jl
@@ -27,4 +27,8 @@ end
   include("Graphs.jl")
 end
 
+@testset "PredicatedSets.jl" begin
+  include("PredicatedSets.jl")
+end
+
 end
diff --git a/test/categorical_algebra/PredicatedSets.jl b/test/categorical_algebra/PredicatedSets.jl
new file mode 100644
index 000000000..3b654b4f4
--- /dev/null
+++ b/test/categorical_algebra/PredicatedSets.jl
@@ -0,0 +1,22 @@
+module TestPredicatedSets
+using Test
+using Catlab.CategoricalAlgebra.PredicatedSets
+using Catlab.Theories
+
+odds = PredicatedSet(Int, x -> x % 2 == 1)
+evens = PredicatedSet(Int, x -> x % 2 == 0)
+
+plus_one_to_odd = PredicatedHom(odds,evens,x -> x+1)
+plus_one_to_even = PredicatedHom(evens,odds,x -> x+1)
+
+@test plus_one_to_odd(1) == 2
+@test_throws AssertionError plus_one_to_odd(2) == 3
+@test plus_one_to_even(2) == 3
+@test_throws AssertionError plus_one_to_even(3) == 4
+
+@test compose(plus_one_to_odd, plus_one_to_even)(3) == 5
+
+plus_two = PredicatedHom(odds,evens,x -> x+2)
+
+@test_throws AssertionError plus_two(3)
+end