diff --git a/src/stdlib/models/FinSets.jl b/src/stdlib/models/FinSets.jl index 8d9aa3ea..8bf8d303 100644 --- a/src/stdlib/models/FinSets.jl +++ b/src/stdlib/models/FinSets.jl @@ -27,6 +27,7 @@ end compose(f::Vector{Int}, g::Vector{Int}) = g[f] dom(f::Vector{Int}) = length(f) + codom(::Vector{Int}; context) = context[:codom] end end diff --git a/src/stdlib/models/Op.jl b/src/stdlib/models/Op.jl new file mode 100644 index 00000000..cbb6da38 --- /dev/null +++ b/src/stdlib/models/Op.jl @@ -0,0 +1,37 @@ +module Op + +export OpC, op + + +using ....Models +using ...StdTheories +using StructEquality + + +@struct_hash_equal struct OpC{ObT, HomT, C<:Model{Tuple{ObT, HomT}}} <: Model{Tuple{ObT, HomT}} + cat::C +end + +op(c) = OpC(c) + +using .ThCategory + +rename(::Nothing, ::Dict{Symbol,Symbol}) = nothing +rename(nt::NamedTuple, d::Dict{Symbol,Symbol}) = + NamedTuple(get(d, k, k) => v for (k, v) in pairs(nt)) + + +@instance ThCategory{ObT, HomT} [model::OpC{ObT, HomT, C}] where {ObT, HomT, C} begin + Ob(x::ObT) = Ob[model.cat](x) + Hom(x::HomT, d::ObT, cd::ObT) = Hom[model.cat](x, cd, d) + id(x::ObT) = id[model.cat](x) + dom(f::HomT; context) = + codom[model.cat](f; context=rename(context, Dict(:dom=>:codom, :codom=>:dom))) + codom(f::HomT; context) = + dom[model.cat](f; context=rename(context, Dict(:dom=>:codom, :codom=>:dom))) + compose(f::HomT, g::HomT; context=nothing) = + compose[model.cat](g, f; + context=rename(context, Dict(:a=>:c, :c=>:a, :b=>:b))) +end + +end # module diff --git a/src/stdlib/models/module.jl b/src/stdlib/models/module.jl index b7613e4e..328c7fe6 100644 --- a/src/stdlib/models/module.jl +++ b/src/stdlib/models/module.jl @@ -5,12 +5,14 @@ using Reexport include("FinSets.jl") include("FinMatrices.jl") include("SliceCategories.jl") +include("Op.jl") include("Nothings.jl") include("GATs.jl") @reexport using .FinSets @reexport using .FinMatrices @reexport using .SliceCategories +@reexport using .Op @reexport using .Nothings @reexport using .GATs diff --git a/test/stdlib/models/FinSets.jl b/test/stdlib/models/FinSets.jl index 04f67287..7887388e 100644 --- a/test/stdlib/models/FinSets.jl +++ b/test/stdlib/models/FinSets.jl @@ -4,7 +4,7 @@ using GATlab, Test using .ThCategory -@withmodel FinSetC() (Ob, Hom, id, compose, dom) begin +@withmodel FinSetC() (Ob, Hom, id, compose, dom, codom) begin @test Ob(0) == 0 @test_throws TypeCheckFail Ob(-1) @test_throws TypeCheckFail Hom([1,5,2], 3, 4) @@ -13,6 +13,7 @@ using .ThCategory @test id(2) == [1,2] @test compose([5], [1,1,1,3,2]) == [2] @test dom([5]) == 1 + @test codom([5]; context=(codom=10,)) == 10 end end diff --git a/test/stdlib/models/Op.jl b/test/stdlib/models/Op.jl new file mode 100644 index 00000000..06295f1f --- /dev/null +++ b/test/stdlib/models/Op.jl @@ -0,0 +1,21 @@ +"""Same as FinSetC tests but with all doms/codoms reversed""" +module TestOp + +using GATlab, Test + +using .ThCategory + +@withmodel op(FinSetC()) (Ob, Hom, id, compose, dom, codom) begin + @test Ob(0) == 0 + @test_throws TypeCheckFail Ob(-1) + @test_throws TypeCheckFail Hom([1,5,2], 4, 3) + @test Hom(Int[], 4, 0) == Int[] + + @test id(2) == [1,2] + @test compose([1,1,1,3,2], [5]) == [2] + @test compose([1,1,1,3,2], [5]; context=(;)) == [2] + @test codom([5]) == 1 + @test dom([5]; context=(dom=10,)) == 10 +end + +end # module diff --git a/test/stdlib/models/tests.jl b/test/stdlib/models/tests.jl index 6e7e807a..6555e913 100644 --- a/test/stdlib/models/tests.jl +++ b/test/stdlib/models/tests.jl @@ -3,6 +3,7 @@ module TestStdModels include("FinSets.jl") include("FinMatrices.jl") include("SliceCategories.jl") +include("Op.jl") include("Nothings.jl") include("GATs.jl")