Skip to content

Commit

Permalink
pass model via Base.getindex instead of keyword argument
Browse files Browse the repository at this point in the history
  • Loading branch information
olynch committed Sep 20, 2023
1 parent 7f93f97 commit 6d791a3
Show file tree
Hide file tree
Showing 8 changed files with 42 additions and 42 deletions.
6 changes: 3 additions & 3 deletions src/models/ModelInterface.jl
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
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
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
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
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
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
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
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

0 comments on commit 6d791a3

Please sign in to comment.