Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Pass model via Base.getindex #106

Merged
merged 1 commit into from
Sep 20, 2023
Merged

Pass model via Base.getindex #106

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions src/models/ModelInterface.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -109,7 +109,7 @@ struct TypedFinSetC <: Model{Tuple{Vector{Int}, Vector{Int}}}
ntypes::Int
end

@instance ThCategory{Vector{Int}, Vector{Int}} (;model::TypedFinSetC) begin
@instance ThCategory{Vector{Int}, Vector{Int}} [model::TypedFinSetC] begin
Ob(v::Vector{Int}) = all(1 <= j <= model.ntypes for j in v)
Hom(f::Vector{Int}, v::Vector{Int}, w::Vector{Int}) =
length(f) == length(v) && all(1 <= y <= length(w) for y in f)
Expand All @@ -125,7 +125,7 @@ struct SliceCat{Ob, Hom, C <: Model{Tuple{Ob, Hom}}} <: Model{Tuple{Tuple{Ob, Ho
c::C
end

@instance ThCategory{Tuple{Ob, Hom}, Hom} (;model::SliceCat{Ob, Hom, C}) where {Ob, Hom, C<:Model{Tuple{Ob, Hom}}} begin
@instance ThCategory{Tuple{Ob, Hom}, Hom} [model::SliceCat{Ob, Hom, C}] where {Ob, Hom, C<:Model{Tuple{Ob, Hom}}} begin
end
```

Expand Down Expand Up @@ -191,7 +191,7 @@ function parse_model_param(e)
end

model_type = @match paramdecl begin
Expr(:tuple, Expr(:parameters, Expr(:(::), :model, model_type))) => model_type
Expr(:vect, Expr(:(::), :model, model_type)) => model_type
nothing => nothing
_ => error("invalid syntax for declaring model type: $model")
end
Expand Down
2 changes: 1 addition & 1 deletion src/stdlib/models/FinMatrices.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ using ...StdTheories
struct FinMatC{T<:Number} <: Model{Tuple{T}}
end

@instance ThCategory{Int, Matrix{T}} (;model::FinMatC{T}) where {T} begin
@instance ThCategory{Int, Matrix{T}} [model::FinMatC{T}] where {T} begin
Ob(n::Int) = n >= 0 ? n : @fail "expected nonnegative integer"
Hom(A::Matrix{T}, n::Int, m::Int) =
size(A) == (n,m) ? A : @fail "expected dimensions to be $((n,m))"
Expand Down
2 changes: 1 addition & 1 deletion src/stdlib/models/FinSets.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ using ...StdTheories
struct FinSetC <: Model{Tuple{Int, Vector{Int}}}
end

@instance ThCategory{Int, Vector{Int}} (;model::FinSetC) begin
@instance ThCategory{Int, Vector{Int}} [model::FinSetC] begin
Ob(x::Int) = x >= 0 ? x : @fail "expected nonnegative integer"

function Hom(f::Vector{Int}, n::Int, m::Int)
Expand Down
2 changes: 1 addition & 1 deletion src/stdlib/models/GATs.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ using GATlab, GATlab.Models
struct GATC <: Model{Tuple{GAT, AbsTheoryMap}}
end

@instance ThCategory{GAT, AbsTheoryMap} (;model::GATC) begin
@instance ThCategory{GAT, AbsTheoryMap} [model::GATC] begin
id(x::GAT) = IdTheoryMap(x)
compose(f::AbsTheoryMap, g::AbsTheoryMap) = TheoryMaps.compose(f,g)
dom(f::AbsTheoryMap) = TheoryMaps.dom(f)
Expand Down
2 changes: 1 addition & 1 deletion src/stdlib/models/Nothings.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ using ....Models, ...StdTheories
struct NothingC <: Model{Tuple{Nothing, Nothing}}
end

@instance ThCategory{Nothing, Nothing} (;model::NothingC) begin
@instance ThCategory{Nothing, Nothing} [model::NothingC] begin
Ob(::Nothing) = nothing
Hom(::Nothing, ::Nothing, ::Nothing) = nothing

Expand Down
14 changes: 7 additions & 7 deletions src/stdlib/models/SliceCategories.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,15 +17,15 @@ end

using .ThCategory

@instance ThCategory{SliceOb{ObT, HomT}, HomT} (;model::SliceC{ObT, HomT, C}) where {ObT, HomT, C} begin
@instance ThCategory{SliceOb{ObT, HomT}, HomT} [model::SliceC{ObT, HomT, C}] where {ObT, HomT, C} begin
function Ob(x::SliceOb{ObT, HomT})
try
Ob(x.ob; model=model.cat)
Ob[model.cat](x.ob)
catch e
@fail ("ob is not valid", e)
end
try
Hom(x.hom, x.ob, model.over; model=model.cat)
Hom[model.cat](x.hom, x.ob, model.over)
catch e
@fail ("hom is not valid", e)
end
Expand All @@ -36,19 +36,19 @@ using .ThCategory

function Hom(f::HomT, x::SliceOb{ObT, HomT}, y::SliceOb{ObT, HomT})
try
Hom(f, x.ob, y.ob; model=model.cat)
Hom[model.cat](f, x.ob, y.ob)
catch e
@fail ("morphism is not valid in base category", e)
end
compose(f, y.hom; model=model.cat, context=(a=x.ob, b=y.ob, c=model.over)) == x.hom ||
compose[model.cat](f, y.hom; context=(a=x.ob, b=y.ob, c=model.over)) == x.hom ||
@fail "commutativity of triangle does not hold"
f
end

id(x::SliceOb{ObT, HomT}) = id(x.ob; model=model.cat)
id(x::SliceOb{ObT, HomT}) = id[model.cat](x.ob)

compose(f::HomT, g::HomT; context=nothing) =
compose(f, g; model=model.cat, context=isnothing(context) ? nothing : map(x -> x.ob, context))
compose[model.cat](f, g; context=isnothing(context) ? nothing : map(x -> x.ob, context))
end

end
14 changes: 7 additions & 7 deletions src/syntax/TheoryInterface.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,13 +72,13 @@ macro theory(head, body)
# TODO: also push an automatically generated docstring
push!(
modulelines,
:(function $name(args...; model=nothing, context=nothing)
if !isnothing(model)
$name($(WithModel)(model), args...; context)
else
throw(MethodError($name, args))
end
end)
quote
function $name end

function Base.getindex(::typeof($name), m::$(GlobalRef(TheoryInterface, :Model)))
(args...; context=nothing) -> $name($(GlobalRef(TheoryInterface, :WithModel))(m), args...; context)
end
end
)
end

Expand Down
42 changes: 21 additions & 21 deletions test/models/ModelInterface.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ using StructEquality
@struct_hash_equal struct FinSetC <: Model{Tuple{Int, Vector{Int}}}
end

@instance ThCategory{Int, Vector{Int}} (;model::FinSetC) begin
@instance ThCategory{Int, Vector{Int}} [model::FinSetC] begin
# check f is Hom: n -> m
function Hom(f::Vector{Int}, n::Int, m::Int)
if length(f) == n
Expand All @@ -30,12 +30,12 @@ end

using .ThCategory

@test Ob(-1; model=FinSetC()) == -1
@test Hom([1,2,3], 3, 3; model=FinSetC()) == [1,2,3]
@test_throws TypeCheckFail Hom([1,2,3], 3, 2; model=FinSetC())
@test Ob[FinSetC()](-1) == -1
@test Hom[FinSetC()]([1,2,3], 3, 3) == [1,2,3]
@test_throws TypeCheckFail Hom[FinSetC()]([1,2,3], 3, 2)

try
ThCategory.Hom([1,2,3], 3, 2; model=FinSetC())
ThCategory.Hom[FinSetC()]([1,2,3], 3, 2)
catch e
@test e.model == FinSetC()
@test e.theory == ThCategory.THEORY
Expand All @@ -46,14 +46,14 @@ catch e
@test sprint(showerror, e) isa String
end

@test_throws TypeCheckFail Hom([1,2,3], 3, 2; model=FinSetC())
@test_throws TypeCheckFail Hom([1,2,3], 2, 3; model=FinSetC())
@test compose([1,3,2], [1,3,2]; model=FinSetC()) == [1,2,3]
@test_throws TypeCheckFail Hom[FinSetC()]([1,2,3], 3, 2)
@test_throws TypeCheckFail Hom[FinSetC()]([1,2,3], 2, 3)
@test compose[FinSetC()]([1,3,2], [1,3,2]) == [1,2,3]

@test id(2; model=FinSetC()) == [1,2]
@test id[FinSetC()](2) == [1,2]

@test dom([1,2,3]; model=FinSetC()) == 3
@test_throws ErrorException codom([1,2,3]; model=FinSetC())
@test dom[FinSetC()]([1,2,3]) == 3
@test_throws ErrorException codom[FinSetC()]([1,2,3])

@test implements(FinSetC(), ThCategory)

Expand All @@ -62,7 +62,7 @@ struct TypedFinSetC <: Model{Tuple{Vector{Int}, Vector{Int}}}
ntypes::Int
end

@instance ThStrictMonCat{Int, Vector{Int}} (;model::FinSetC) begin
@instance ThStrictMonCat{Int, Vector{Int}} [model::FinSetC] begin
@import Ob, Hom, id, compose, dom, codom

mcompose(a::Int, b::Int) = a + b
Expand All @@ -75,8 +75,8 @@ end

using .ThStrictMonCat

@test mcompose(id(2; model=FinSetC()), id(2; model=FinSetC()); context=(;B₁=2), model=FinSetC()) ==
id(4; model=FinSetC())
@test mcompose[FinSetC()](id[FinSetC()](2), id[FinSetC()](2); context=(;B₁=2)) ==
id[FinSetC()](4)

@struct_hash_equal struct FinSet
n::Int
Expand All @@ -87,7 +87,7 @@ end
dom::FinSet
codom::FinSet
function FinFunction(values::AbstractVector, dom::FinSet, codom::FinSet)
new(ThCategory.Hom(Vector{Int}(values), dom.n, codom.n; model=FinSetC()), dom, codom)
new(ThCategory.Hom[FinSetC()](Vector{Int}(values), dom.n, codom.n), dom, codom)
end
end

Expand Down Expand Up @@ -127,22 +127,22 @@ end

@test_throws MethodError id(2)

@test_throws LoadError @eval @instance ThCategory{Int, Vector{Int}} (;model::FinSetC) begin
@test_throws LoadError @eval @instance ThCategory{Int, Vector{Int}} [model::FinSetC] begin
end

@test_throws LoadError @eval @instance ThCategory{Int, Vector{Int}} (;model::FinSetC) begin
@test_throws LoadError @eval @instance ThCategory{Int, Vector{Int}} [model::FinSetC] begin
compose(f::Vector{Int}, g::Vector{Int}) = g[f]
dom(f::Vector{Int}) = length(f)
end

@test_throws LoadError @eval @instance ThCategory{Int, Vector{Int}} (;model::FinSetC) begin
@test_throws LoadError @eval @instance ThCategory{Int, Vector{Int}} [model::FinSetC] begin
id(f::Vector{Int}) = f
compose(f::Vector{Int}, g::Vector{Int}) = g[f]
dom(f::Vector{Int}) = length(f)
end

try
@eval @instance ThCategory{Int, Vector{Int}} (;model::FinSetC) begin
@eval @instance ThCategory{Int, Vector{Int}} [model::FinSetC] begin
id(f::Vector{Int}) = f
compose(f::Vector{Int}, g::Vector{Int}) = g[f]
dom(f::Vector{Int}) = length(f)
Expand All @@ -152,15 +152,15 @@ catch e
@test sprint(showerror, e.error) isa String
end

@test_throws LoadError @eval @instance ThStrictMonCat{Int, Vector{Int}} (;model::FinSetC) begin
@test_throws LoadError @eval @instance ThStrictMonCat{Int, Vector{Int}} [model::FinSetC] begin
@import Ob, Hom, id, compose, dom, codom

mcompose(f::Vector{Int}, g::Vector{Int}; context) = [f; g .+ context.B₁]

munit() = 0
end

@test_throws LoadError @eval @instance ThStrictMonCat{Int, Int} (;model::FinSetC) begin
@test_throws LoadError @eval @instance ThStrictMonCat{Int, Int} [model::FinSetC] begin
@import Ob, Hom, id, compose, dom, codom

mcompose(a::Int, b::Int) = a + b
Expand Down