Use a wrapper type for ThCategory in Opposite cat models

src/stdlib/models/op.jl

@@ -3,26 +3,21 @@ Explicit Op model. Alternatively, see DerivedModels.jl (`OpFinSetC`) for
 theory-morphism-derived Op models.
 """
 
-export OpC, op
+export OpC, op, CatWrapper
 
 
 using ...Models
 using ..StdTheories
 using StructEquality
 
-# TODO when we implement custom structs for models of a particular theory, we 
-# can use that rather than a generic "C" for which we then have to check 
-# whether it implements the theory.
+ThCategory.Meta.@wrapper CatWrapper 
 
-@struct_hash_equal struct OpC{ObT, HomT, C}
-  cat::C 
-  function OpC(c::C) where C 
-    types = impl_types(c, ThCategory)
-    implements(c, ThCategory, types) ? new{types..., C}(c) : error("bad")
-  end
+@struct_hash_equal struct OpC{ObT, HomT}
+  cat::CatWrapper
+  OpC(c::CatWrapper) = new{impl_type.(Ref(c),[:Ob,:Hom])...}(c)
 end
 
-op(c) = OpC(c)
+op(c::CatWrapper) = OpC(c)
 
 using .ThCategory
 
@@ -31,15 +26,15 @@ 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)
+@instance ThCategory{ObT, HomT} [model::OpC{ObT, HomT}] where {ObT, HomT} 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(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)))
+    dom(model.cat, f; context=rename(context, Dict(:dom=>:codom, :codom=>:dom)))
   compose(f::HomT, g::HomT; context=nothing) =
-    compose[model.cat](g, f; 
+    compose(model.cat, g, f; 
             context=rename(context, Dict(:a=>:c, :c=>:a, :b=>:b)))
 end

src/syntax/TheoryInterface.jl

@@ -321,6 +321,9 @@ function wrapper(name::Symbol, t::GAT, mod)
         :($(GlobalRef($(TheoryInterface), :impl_type))(x, $s))
       end
 
+      gv = :($(GlobalRef($(Scopes), :getvalue)))
+      it = :($(GlobalRef($(TheoryInterface), :impl_type)))
+
       esc(quote 
         # Catch any potential docs above the macro call
         const $(doctarget) = nothing
@@ -341,9 +344,8 @@ function wrapper(name::Symbol, t::GAT, mod)
         # Define == and hash
         $(Expr(:macrocall, $(GlobalRef(StructEquality, Symbol("@struct_hash_equal"))), $(mod), $(:n)))
 
-        # GlobalRef doesn't work: "invalid function name".
-        GATlab.getvalue(x::$n) = x.val 
-        GATlab.impl_type(x::$n, o::Symbol) = GATlab.impl_type(x.val, $($name), o)
+        $gv(x::$n) = x.val 
+        $it(x::$n, o::Symbol) = $it(x.val, $($name), o)
 
         # Dispatch on model value for all declarations in theory
         $(map(filter(x->x[2] isa $AlgDeclaration, $(identvalues(t)))) do (x,j)
@@ -366,6 +368,10 @@ function wrapper(name::Symbol, t::GAT, mod)
       XTs = map(zip(Ts,Xs)) do (T,X)
         :($X <: $T || error("Mismatch $($($(Meta.quot)(T))): $($X) ⊄ $($T)"))
       end
+
+      gv = :($(GlobalRef($(Scopes), :getvalue)))
+      it = :($(GlobalRef($(TheoryInterface), :impl_type)))
+
       esc(quote 
         # Catch any potential docs above the macro call
         const $(doctarget) = nothing
@@ -392,9 +398,8 @@ function wrapper(name::Symbol, t::GAT, mod)
         # Define == and hash
         $(Expr(:macrocall, $(GlobalRef(StructEquality, Symbol("@struct_hash_equal"))), $(mod), $(:n)))
 
-        # GlobalRef doesn't work: "invalid function name".
-        GATlab.getvalue(x::$n) = x.val 
-        GATlab.impl_type(x::$n, o::Symbol) = GATlab.impl_type(x.val, $($name), o)
+        $gv(x::$n) = x.val 
+        $it(x::$n, o::Symbol) = $it(x.val, $($name), o)
 
         # Dispatch on model value for all declarations in theory
         $(map(filter(x->x[2] isa $AlgDeclaration, $(identvalues(t)))) do (x,j)

test/stdlib/Op.jl

@@ -8,7 +8,7 @@ using .ThCategory
 # Explicit Op model
 #------------------
 
-@withmodel op(FinSetC()) (Ob, Hom, id, compose, dom, codom) begin
+@withmodel op(CatWrapper(FinSetC())) (Ob, Hom, id, compose, dom, codom) begin
   @test Ob(0) == 0
   @test_throws ErrorException Ob(-1)
   @test_throws ErrorException Hom([1,5,2], 4, 3)