Wrapper structs for models of a theory

src/models/SymbolicModels.jl

@@ -8,6 +8,7 @@ using ...Util
 using ...Syntax
 import ...Syntax: invoke_term
 using ..ModelInterface
+using ..ModelInterface: args_from_sorts, default_instance
 
 using Base.Meta: ParseError
 using MLStyle
@@ -262,6 +263,10 @@ macro symbolic_model(decl, theoryname, body)
 
   module_structs = symbolic_structs(theory, abstract_types, __module__)
 
+  # Part 1.5: Generate a model  
+  imp = Expr(:import, Expr(:(:), Expr(:., :., :., name), [
+    Expr(:., x) for x in [name, theoryname, name, nameof.(sorts(theory))...]]...))
+
   # Part 2: Generating internal methods
 
   module_methods = [internal_accessors(theory)..., 
@@ -271,15 +276,20 @@ macro symbolic_model(decl, theoryname, body)
     export $(nameof.(sorts(theory))...)
     using ..($(nameof(__module__)))
     import ..($(nameof(__module__))): $theoryname
+
+    $(module_structs...)
+
+    $(generate_function.(module_methods)...)
+
     module $(esc(:Meta))
-      import ..($(name)): $theoryname
+      $imp
       const $(esc(:theory_module)) = $(esc(theoryname))
       const $(esc(:theory)) = $(theory)
       const $(esc(:theory_type)) = $(esc(theoryname)).Meta.T
+      # Canonical symbolic model
+      $(esc(:M)) = Dispatch($(esc(:theory)), [$(esc.(nameof.(theory.sorts))...)])
     end
 
-    $(module_structs...)
-    $(generate_function.(module_methods)...)
   end)
 
   # Part 3: Generating instance of theory
@@ -731,4 +741,4 @@ function show_latex_script(io::IO, expr::GATExpr, head::String;
   print(io, "}")
 end
 
-end
+end # module

src/nonstdlib/models/Pushouts.jl

@@ -2,8 +2,6 @@ using DataStructures, StructEquality
 
 export PushoutInt
 
-using GATlab
-
 """Data required to specify a pushout. No fancy caching."""
 @struct_hash_equal struct PushoutInt
   ob::Int

src/stdlib/derivedmodels/DerivedModels.jl

@@ -6,7 +6,7 @@ using ...StdTheoryMaps
 using ...StdModels
 
 # Given a model of a category C, we can derive a model of Cᵒᵖ.
-OpFinSetC = migrate_model(OpCat, FinSetC())
+OpFinSetC = migrate_model(OpCat, FinSetC(), :OpFinSetCat)
 
 # Interpret `e` as `0` and `⋅` as `+`.
 IntMonoid = migrate_model(NatPlusMonoid, IntNatPlus())

src/stdlib/models/arithmetic.jl

@@ -3,22 +3,22 @@ export IntNat, IntNatPlus, IntPreorder, ZRing, BoolRing
 using ...Models
 using ..StdTheories
 
-struct IntNat <: Model{Tuple{Int}} end
+struct IntNat end
 
 @instance ThNat{Int} [model::IntNat] begin
   Z() = 0
   S(n::Int) = n + 1
 end
 
-struct IntNatPlus <: Model{Tuple{Int}} end
+struct IntNatPlus end
 
 @instance ThNatPlus{Int} [model::IntNatPlus] begin
   Z() = 0
   S(n::Int) = n + 1
   +(x::Int, y::Int) = x + y
 end
 
-struct IntPreorder <: Model{Tuple{Int, Tuple{Int,Int}}} end
+struct IntPreorder end
 
 @instance ThPreorder{Int, Tuple{Int,Int}} [model::IntPreorder] begin
   Leq(ab::Tuple{Int,Int}, a::Int, b::Int) = a ≤ b ? ab : @fail "$(ab[1]) ≰ $(ab[2])"
@@ -30,7 +30,7 @@ struct IntPreorder <: Model{Tuple{Int, Tuple{Int,Int}}} end
   end
 end
 
-struct ZRing <: Model{Tuple{Int}} end
+struct ZRing end
 
 @instance ThRing{Int} [model::ZRing] begin
   zero() = 0

src/stdlib/models/finmatrices.jl

@@ -3,8 +3,7 @@ export FinMatC
 using ...Models
 using ..StdTheories
 
-struct FinMatC{T<:Number} <: Model{Tuple{T}}
-end
+struct FinMatC{T <: Number} end
 
 @instance ThCategory{Int, Matrix{T}} [model::FinMatC{T}] where {T} begin
   Ob(n::Int) = n >= 0 ? n : @fail "expected nonnegative integer"

src/stdlib/models/finsets.jl

@@ -3,8 +3,7 @@ export FinSetC
 using ...Models
 using ..StdTheories
 
-struct FinSetC <: Model{Tuple{Int, Vector{Int}}}
-end
+struct FinSetC end
 
 @instance ThCategory{Int, Vector{Int}} [model::FinSetC] begin
   Ob(x::Int) = x >= 0 ? x : @fail "expected nonnegative integer"

src/stdlib/models/gats.jl

@@ -4,10 +4,7 @@ using ...Models
 using ...Syntax
 using ..StdTheories
 
-using GATlab, GATlab.Models
-
-struct GATC <: Model{Tuple{GAT, AbsTheoryMap}}
-end
+struct GATC end
 
 @instance ThCategory{GAT, AbsTheoryMap} [model::GATC] begin
   id(x::GAT) = IdTheoryMap(x)

src/stdlib/models/nothings.jl

@@ -2,8 +2,7 @@ export NothingC
 
 using ...Models, ..StdTheories
 
-struct NothingC <: Model{Tuple{Nothing, Nothing}}
-end
+struct NothingC end
 
 @instance ThCategory{Nothing, Nothing} [model::NothingC] begin
   Ob(::Nothing) = nothing

src/stdlib/models/op.jl

@@ -10,8 +10,17 @@ using ...Models
 using ..StdTheories
 using StructEquality
 
-@struct_hash_equal struct OpC{ObT, HomT, C<:Model{Tuple{ObT, HomT}}} <: Model{Tuple{ObT, HomT}}
-  cat::C
+# 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.
+
+@struct_hash_equal struct OpC{ObT, HomT, C}
+  cat::C 
+  function OpC(c::C) where C 
+    obtype = impl_type(c, ThCategory, :Ob)
+    homtype = impl_type(c, ThCategory, :Hom)
+    implements(c, ThCategory) ? new{obtype, homtype, C}(c) : error("bad")
+  end
 end
 
 op(c) = OpC(c)

src/stdlib/models/slicecategories.jl

@@ -9,13 +9,15 @@ using StructEquality
   hom::HomT
 end
 
-@struct_hash_equal struct SliceC{ObT, HomT, C<:Model{Tuple{ObT, HomT}}} <: Model{Tuple{SliceOb{ObT, HomT}, HomT}}
+@struct_hash_equal struct SliceC{ObT, HomT, C}
   cat::C
   over::ObT
-  # function SliceC(cat, over)
-  #   implements(cat, ThCategory)
-  #   new(cat, Ob[cat](over))
-  # end
+  function SliceC(cat::C, over) where C
+    implements(cat, ThCategory) || error("Bad cat $cat")
+    obtype = impl_type(cat, ThCategory, :Ob)
+    homtype = impl_type(cat, ThCategory, :Hom)
+    new{obtype, homtype, C}(cat, ThCategory.Ob[cat](over))
+  end
 end
 
 using .ThCategory

src/syntax/GATs.jl

@@ -14,7 +14,7 @@ export Constant, AlgTerm, AlgType, AlgAST,
 using ..Scopes
 import ..ExprInterop: fromexpr, toexpr
 
-import ..Scopes: retag, rename, reident
+import ..Scopes: retag, rename, reident, gettag
 
 import AlgebraicInterfaces: equations
 

src/syntax/TheoryInterface.jl

@@ -1,14 +1,11 @@
 module TheoryInterface
-export @theory, @signature, Model, invoke_term
+export @theory, @signature, invoke_term
 
 using ..Scopes, ..GATs, ..ExprInterop, GATlab.Util
-# using GATlab.Util
 
 using MLStyle, StructEquality, Markdown
 
-abstract type Model{Tup <: Tuple} end
-
-@struct_hash_equal struct WithModel{M <: Model}
+@struct_hash_equal struct WithModel{M}
   model::M
 end
 
@@ -153,11 +150,13 @@ function theory_impl(head, body, __module__)
   end
 
   doctarget = gensym()
+  mdp(::Nothing) = []
+  mdp(x::Markdown.MD) = x
+  mdp(x::Base.Docs.DocStr) = Markdown.parse(x.text...)
 
   push!(modulelines, Expr(:toplevel, :(module Meta
     struct T end
 
-    @doc ($(Markdown.MD)((@doc $(__module__).$doctarget), $docstr))
     const theory = $theory
 
     macro theory() $theory end
@@ -180,17 +179,33 @@ function theory_impl(head, body, __module__)
         $(structlines...)
         end
       ),
-      :(@doc ($(Markdown.MD)((@doc $doctarget), $docstr)) $name)
+      :(@doc ($(Markdown.MD)($mdp(@doc $doctarget), $docstr)) $name)
     )
   )
 end
 
+"""
+The Dispatch type is a model of every theory.
+"""
+@struct_hash_equal struct Dispatch 
+  t::GAT
+  types::Dict{AlgSort,Type}
+end
+
+Dispatch(t::GAT, v::AbstractVector{<:Type}) = 
+  Dispatch(t, Dict(zip(sorts(t), v)))
+
+# WARNING: if any other package play with indexing methodnames with their own 
+# structs, then this code could be broken because it assumes we are the only  
+# ones to use this trick.
 function juliadeclaration(name::Symbol)
   quote
     function $name end
+    # we expect just one method because of Dispatch type
+    if isempty(Base.methods(Base.getindex, [typeof($name), Any]))
+      Base.getindex(f::typeof($name), ::$(GlobalRef(TheoryInterface, :Dispatch))) = f
 
-    if Base.isempty(Base.methods(Base.getindex, [typeof($name), $(GlobalRef(TheoryInterface, :Model))]))
-      function Base.getindex(::typeof($name), m::$(GlobalRef(TheoryInterface, :Model)))
+      function Base.getindex(::typeof($name), m::Any) 
         (args...; context=nothing) -> $name($(GlobalRef(TheoryInterface, :WithModel))(m), args...; context)
       end
     end

src/syntax/TheoryMaps.jl

@@ -402,8 +402,6 @@ macro theorymap(head, body)
   codom = macroexpand(__module__, :($codomname.Meta.@theory))
   tmap = fromexpr(dom, codom, body, TheoryMap)
 
-  mig = migrator(tmap, dommod, codommod, dom, codom)
-
   esc(
     Expr(
       :toplevel,
@@ -413,8 +411,6 @@ macro theorymap(head, body)
           macro map() $tmap end
           macro dom() $dommod end
           macro codom() $codommod end
-
-          $mig
         end
       ),
       :(Core.@__doc__ $(name)),

src/syntax/gats/gat.jl

@@ -36,6 +36,8 @@ fancier.
   bysignature::Dict{AlgSorts, Ident}
 end
 
+Base.iterate(m::MethodResolver, i...) = iterate(m.bysignature, i...)
+
 function MethodResolver()
   MethodResolver(Dict{AlgSorts, Ident}())
 end
@@ -379,3 +381,5 @@ end
 
 """Get all structs in a theory"""
 structs(t::GAT) = AlgStruct[getvalue(t[methodof(s)]) for s in struct_sorts(t)]
+
+gettag(T::GAT) = gettag(T.segments.scopes[end])

test/models/ModelInterface.jl

@@ -1,11 +1,8 @@
 module TestModelInterface 
 
-using GATlab
-using Test
-using StructEquality
+using GATlab, Test, StructEquality
 
-@struct_hash_equal struct FinSetC <: Model{Tuple{Int, Vector{Int}}}
-end
+@struct_hash_equal struct FinSetC end
 
 @instance ThCategory{Int, Vector{Int}} [model::FinSetC] begin
   # check f is Hom: n -> m
@@ -56,9 +53,10 @@ end
 @test_throws ErrorException codom[FinSetC()]([1,2,3])
 
 @test implements(FinSetC(), ThCategory)
+@test !implements(FinSetC(), ThNatPlus)
 
 # Todo: get things working where Ob and Hom are the same type (i.e. binding dict not monic)
-struct TypedFinSetC <: Model{Tuple{Vector{Int}, Vector{Int}}}
+@struct_hash_equal struct TypedFinSetC
   ntypes::Int
 end
 
@@ -170,4 +168,65 @@ end
   munit() = 0
 end
 
+# Test scenario where we @import a method but then extend it
+############################################################
+@theory T1 begin 
+  X::TYPE; 
+  h(a::X)::X 
+end
+
+@theory T2<:T1 begin 
+  Y::TYPE; 
+  h(b::Y)::Y 
+end
+
+@instance T1{Int} begin 
+  h(a::Int) = 1 
+end
+
+@instance T2{Int,Bool} begin 
+  @import X, h
+  h(b::Bool) = false 
+end
+
+@test h(2) == 1
+
+@test h(false) == false
+
+# Test models with abstract types 
+#################################
+
+""" Assume this implements Base.iterate """
+abstract type MyAbsIter{V} end
+
+struct MyVect{V} <: MyAbsIter{V}
+  v::Vector{V}
+end
+
+Base.iterate(m::MyVect, i...) = iterate(m.v, i...)
+
+@instance ThSet{V} [model::MyAbsIter{V}] where V begin 
+  default(v::V) = v ∈ model ? v : @fail "Bad $v not in $model"
+end
+
+@test implements(MyVect([1,2,3]), ThSet)
+
+# this will fail unless WithModel accepts subtypes
+@test ThSet.default[MyVect([1,2,3])](1) == 1
+
+# Test default model + dispatch model
+#####################################
+@test_throws MethodError id(2)
+
+@default_model ThCategory{Int, Vector{Int}} [model::FinSetC]
+
+d = Dispatch(ThCategory.Meta.theory, [Int, Vector{Int}])
+@test implements(d, ThCategory)
+@test !implements(d, ThNatPlus)
+@test impl_type(d, ThCategory, :Ob) == Int 
+@test impl_type(d, ThCategory, :Hom) == Vector{Int} 
+
+@test id(2) == [1,2] == ThCategory.id[d](2)
+@test compose([1,2,3], [2,1,3]) == [2,1,3]
+
 end # module