From bc47341e698541e39d2501ca686e7094589e3820 Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Mon, 16 Oct 2023 11:49:13 -0700
Subject: [PATCH 01/13] Migrate models differently

---
 src/models/ModelInterface.jl              | 160 +++++++++++-----------
 src/stdlib/derivedmodels/DerivedModels.jl |   6 +-
 src/syntax/TheoryMaps.jl                  |   7 +
 src/util/MetaUtils.jl                     |  27 +++-
 test/stdlib/models/Arithmetic.jl          |  10 +-
 test/stdlib/models/Op.jl                  |   3 +-
 6 files changed, 116 insertions(+), 97 deletions(-)

diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl
index a16c256d..2cbeeeaa 100644
--- a/src/models/ModelInterface.jl
+++ b/src/models/ModelInterface.jl
@@ -1,13 +1,16 @@
 module ModelInterface
 
 export Model, implements, TypeCheckFail, SignatureMismatchError, 
-       @model, @instance, @withmodel, @fail, @migrate
+       @model, @instance, @withmodel, @fail, migrate
 
 using ...Syntax
 using ...Util.MetaUtils
+using ...Util.MetaUtils: JuliaFunctionSigNoWhere
+
+import ...Syntax.TheoryMaps: migrator 
 
 using MLStyle
-using DataStructures: DefaultDict
+using DataStructures: DefaultDict, OrderedDict
 
 """
 `Model{Tup <: Tuple}`
@@ -16,7 +19,7 @@ A Julia value with type `Model{Tuple{Ts...}}` represents a model of some
 part of the theory hierarchy, which uses the types in `Ts...` to implement
 the sorts.
 
-A model `m::Model{Tup}` is marked as implementing a `seg::GATSegmant` iff
+A model `m::Model{Tup}` is marked as implementing a `seg::GATSegment` iff
 
 `implements(m, ::Type{Val{gettag(seg)}}) == true`
 
@@ -332,6 +335,8 @@ end
 function ExprInterop.toexpr(sig::JuliaFunctionSig)
   Expr(:call, sig.name, [Expr(:(::), type) for type in sig.types]...)
 end
+ExprInterop.toexpr(sig::JuliaFunctionSigNoWhere) = 
+  ExprInterop.toexpr(sig |> JuliaFunctionSig)
 
 struct SignatureMismatchError <: Exception
   name::Symbol
@@ -363,7 +368,7 @@ function typecheck_instance(
   typechecked = JuliaFunction[]
 
   # The overloads that we have to provide
-  undefined_signatures = Dict{JuliaFunctionSig, Tuple{Ident, Ident}}()
+  undefined_signatures = Dict{JuliaFunctionSigNoWhere, Tuple{Ident, Ident}}()
 
   overload_errormsg =
    "the types for this model declaration do not permit Julia overloading to distinguish between GAT overloads"
@@ -373,7 +378,7 @@ function typecheck_instance(
       continue
     end
     for (_, x) in allmethods(resolver)
-      sig = julia_signature(getvalue(theory[x]), jltype_by_sort; oldinstance, X=x)
+      sig = julia_signature(getvalue(theory[x]), jltype_by_sort; oldinstance, X=x) |> JuliaFunctionSigNoWhere
       if haskey(undefined_signatures, sig)
         error(overload_errormsg)
       end
@@ -388,15 +393,14 @@ function typecheck_instance(
   end
 
   for f in functions
-    sig = parse_function_sig(f)
-
+    sig = parse_function_sig(f) |> JuliaFunctionSigNoWhere
     if haskey(undefined_signatures, sig)
       (decl, method) = undefined_signatures[sig]
 
       judgment = getvalue(theory, method)
 
       if judgment isa AlgTypeConstructor
-        f = expand_fail(theory, decl, f)
+        f = expand_fail(theory, decl, f) 
       end
 
       delete!(undefined_signatures, sig)
@@ -601,104 +605,101 @@ end
 Future work: There is some subtlety in how accessor functions should be handled.
 TODO: The new instance methods do not yet handle the `context` keyword argument.
 """
-macro migrate(head)
-  # Parse
-  (name, mapname, modelname) = @match head begin
-    Expr(:(=), name, Expr(:call, mapname, modelname)) =>
-      (name, mapname, modelname)
-    _ => error("could not parse head of @theory: $head")
-  end
-  codom_types = :(only(supertype($modelname).parameters).types)
-  # Unpack
-  tmap = macroexpand(__module__, :($mapname.@map))
-  dom_module = macroexpand(__module__, :($mapname.@dom))
-  codom_module = macroexpand(__module__, :($mapname.@codom))
-  dom_theory, codom_theory = TheoryMaps.dom(tmap), TheoryMaps.codom(tmap)
-
-  codom_jltype_by_sort = Dict{Ident,Expr0}(map(enumerate(sorts(codom_theory))) do (i,v)
-    v.method => Expr(:ref, codom_types, i)
-  end)
+function migrator(tmap, dom_module, codom_module, dom_theory, codom_theory)
+
+  # Map CODOM sorts to whereparam symbols
+  whereparamdict = OrderedDict(s=>gensym(s.head.name) for s in sorts(codom_theory))
+  whereparams = collect(values(whereparamdict))
+  name = :Migrator #gensym("migrator")
   _x = gensym("val")
-  dom_types = map(methodof.(sorts(dom_theory))) do s
-    codom_jltype_by_sort[typemap(tmap)[s].val.body.method]
-  end
-  jltype_by_sort = Dict(zip(sorts(dom_theory), dom_types))
+
+  jltype_by_sort = Dict(map(sorts(dom_theory)) do v
+    v => whereparamdict[AlgSort(tmap(v.method).val)]
+  end)
+
+  accessor_funs = [] # accessors
 
   # TypeCons for @instance macro
-  funs = map(collect(typemap(tmap))) do (x, fx)
-    tcon = getvalue(dom_theory[x])
-    fxbody = bodyof(fx.val)
-    fxdecl, fxmethod = headof(fxbody), methodof(fxbody)
-    fxname = nameof(fxdecl)
-    xdecl = tcon.declaration
-    xname = nameof(xdecl)
-    jltype_by_sort[AlgSort(fxdecl, fxmethod)] = jltype_by_sort[AlgSort(xdecl, x)]
+  typecon_funs = map(collect(typemap(tmap))) do (x, fx)
+    typecon = getvalue(dom_theory[x])
+    # Accessors
+    eq = equations(codom_theory, fx)
+    args = [:($_x::$(jltype_by_sort[AlgSort(typecon.declaration, x)]))]
+    scopedict = Dict{ScopeTag,ScopeTag}(gettag(typecon.localcontext)=>gettag(fx.ctx))
+    for accessor in idents(typecon.localcontext; lid=typecon.args)
+      accessor = retag(scopedict, accessor)
+      a = nameof(accessor)
+      # If we have a default means of computing the accessor...
+      if !isempty(eq[accessor])
+        rtype = typecon.localcontext[ident(typecon.localcontext; name=a)]
+        ret_type = jltype_by_sort[AlgSort(getvalue(rtype))]
+        impl = to_call_accessor(first(eq[accessor]), _x, codom_module)
+        jf = JuliaFunction(;name=a, args=args, return_type=ret_type, impl=impl)
+        push!(accessor_funs, jf)
+      end
+    end
+
+    # Typecon function
+    codom_body = bodyof(fx.val)
+    fxname = nameof(headof(codom_body))
+    xname = nameof(typecon.declaration)
     sig = julia_signature(dom_theory, x, jltype_by_sort)
-    argnames = [_x, nameof.(argsof(tcon))...]
-    args = [:($k::$v) for (k, v) in zip(argnames, sig.types)]
-    impls = to_call_impl.(fxbody.args, Ref(termcons(codom_theory)), Ref(codom_module))
+    argnames = [_x, nameof.(argsof(typecon))...]
+    args = [:($k::$(v)) for (k, v) in zip(argnames, sig.types)]
+    impls = to_call_impl.(codom_body.args, Ref(termcons(codom_theory)), Ref(codom_module))
     impl = Expr(:call, Expr(:ref, :($codom_module.$fxname), :(model.model)), _x, impls...)
     JuliaFunction(;name=xname, args=args, return_type=sig.types[1], impl=impl)
   end
 
   # TermCons for @instance macro
-  funs2 = map(collect(termmap(tmap))) do (x, fx)
-    tcon = getvalue(dom_theory[x])
-    xname = nameof(tcon.declaration)
+  termcon_funs = map(collect(termmap(tmap))) do (x, fx)
+    termcon = getvalue(dom_theory[x])
+    func_name = nameof(termcon.declaration)
     sig = julia_signature(dom_theory, x, jltype_by_sort)
-    argnames = nameof.(argsof(tcon))
-    ftype = typemap(tmap)[tcon.type.body.method].val.body
-    ret_type = jltype_by_sort[AlgSort(headof(ftype), methodof(ftype))]
+    argnames = nameof.(argsof(termcon))
+    ret_type = jltype_by_sort[AlgSort(termcon.type)]
 
     args = [:($k::$v) for (k, v) in zip(argnames, sig.types)]
 
     impl = to_call_impl(fx.val, first.(termcons(codom_theory)), codom_module)
 
-    JuliaFunction(;name=xname, args=args, return_type=ret_type, impl=impl)
-  end
-
-  funs3 = [] # accessors
-  for (x, fx) in pairs(typemap(tmap))
-    tc = getvalue(dom_theory[x])
-    eq = equations(codom_theory, fx)
-    args = [:($_x::$(jltype_by_sort[AlgSort(fx.val)]))]
-    scopedict = Dict{ScopeTag,ScopeTag}(gettag(tc.localcontext)=>gettag(fx.ctx))
-    for accessor in idents(tc.localcontext; lid=tc.args)
-      accessor = retag(scopedict, accessor)
-      a = nameof(accessor)
-      # If we have a default means of computing the accessor...
-      if !isempty(eq[accessor])
-        rtype = tc.localcontext[ident(tc.localcontext; name=a)]
-        ret_type = jltype_by_sort[AlgSort(getvalue(rtype))]
-        impl = to_call_accessor(first(eq[accessor]), _x, codom_module)
-        jf = JuliaFunction(;name=a, args=args, return_type=ret_type, impl=impl)
-        push!(funs3, jf)
-      end
-    end
+    JuliaFunction(;name=func_name, args=args, return_type=ret_type, impl=impl)
   end
 
-  model_expr = Expr(
-    :curly,
-    GlobalRef(Syntax.TheoryInterface, :Model),
-    Expr(:curly, :Tuple, esc.(dom_types)...)
-  )
 
+  # Generate instance code 
   instance_code = generate_instance(
     dom_theory,
     dom_module,
     jltype_by_sort,
-    name,
-    [],
-    Expr(:block, generate_function.([funs...,funs2..., funs3...])...);
-    typecheck=false
+    Expr(:curly, name, whereparams...),
+    whereparams,
+    Expr(:block, generate_function.([typecon_funs...,
+                                     termcon_funs..., 
+                                     accessor_funs...
+                                     ])...);
+    typecheck=true, escape=false
   )
 
+  tup_params = Expr(:curly, :Tuple, whereparams...)
+
+  model_expr = Expr(
+    :curly,
+    GlobalRef(Syntax.TheoryInterface, :Model),
+    tup_params
+  )
+
+  # The second whereparams needs to be reordered by the sorts of the DOM theory
   quote
-    struct $(esc(name)) <: $model_expr
-      model :: $(esc(modelname))
+    struct Migrator{$(whereparams...)} <: $model_expr
+      model ::  $(GlobalRef(ModelInterface, :Model)){$tup_params}
+      function Migrator(model:: $(GlobalRef(ModelInterface, :Model)){$tup_params}) where {$(whereparams...)}
+        $(GlobalRef(ModelInterface, :implements))(model, $codom_module) || error("Cannot migrate model $model")
+        new{$(whereparams...)}(model)
+      end
     end
 
-    $instance_code
+    $(instance_code.args...)
   end
 end
 
@@ -725,5 +726,6 @@ function to_call_accessor(t::AlgTerm, x::Symbol, mod::Module)
   Expr(:call, Expr(:ref, :($mod.$(nameof(headof(b)))), :(model.model)), rest)
 end
 
+migrate(theorymap::Module, m::Model) = theorymap.Migrator(m)
 
 end # module
diff --git a/src/stdlib/derivedmodels/DerivedModels.jl b/src/stdlib/derivedmodels/DerivedModels.jl
index 7f8685ba..6723655a 100644
--- a/src/stdlib/derivedmodels/DerivedModels.jl
+++ b/src/stdlib/derivedmodels/DerivedModels.jl
@@ -6,12 +6,12 @@ using ...StdTheoryMaps
 using ...StdModels
 
 # Given a model of a category C, we can derive a model of Cᵒᵖ.
-@migrate OpFinSetC = OpCat(FinSetC)
+OpFinSetC = migrate(OpCat, FinSetC())
 
 # Interpret `e` as `0` and `⋅` as `+`.
-@migrate IntMonoid = NatPlusMonoid(IntNatPlus)
+IntMonoid = migrate(NatPlusMonoid, IntNatPlus())
 
 # Interpret `id` as reflexivity and `compose` as transitivity.
-@migrate IntPreorderCat = PreorderCat(IntPreorder)
+IntPreorderCat = migrate(PreorderCat, IntPreorder())
 
 end
diff --git a/src/syntax/TheoryMaps.jl b/src/syntax/TheoryMaps.jl
index c679b3e0..fae0f915 100644
--- a/src/syntax/TheoryMaps.jl
+++ b/src/syntax/TheoryMaps.jl
@@ -402,6 +402,8 @@ 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,
@@ -411,6 +413,8 @@ macro theorymap(head, body)
           macro map() $tmap end
           macro dom() $dommod end
           macro codom() $codommod end
+
+          $mig
         end
       ),
       :(Core.@__doc__ $(name)),
@@ -418,4 +422,7 @@ macro theorymap(head, body)
   )
 end
 
+function migrator end
+
+
 end # module
diff --git a/src/util/MetaUtils.jl b/src/util/MetaUtils.jl
index 470866b1..a3793808 100644
--- a/src/util/MetaUtils.jl
+++ b/src/util/MetaUtils.jl
@@ -51,6 +51,16 @@ setname(f::JuliaFunction, name) =
   end
 end
 
+"""For comparing JuliaFunctionSigs modulo the where parameters"""
+@struct_hash_equal struct JuliaFunctionSigNoWhere 
+  name::Expr0
+  types::Vector{Expr0}
+end
+JuliaFunctionSigNoWhere(f::JuliaFunctionSig) =
+  JuliaFunctionSigNoWhere(f.name, f.types)
+
+JuliaFunctionSig(f::JuliaFunctionSigNoWhere) = JuliaFunctionSig(f.name, f.types)
+
 # Parsing Julia functions
 #########################
 
@@ -81,12 +91,12 @@ function parse_function(expr::Expr)::JuliaFunction
     Expr(:where, fun_head, whereparams...) => (fun_head, whereparams)
     _ => (fun_expr, Expr0[])
   end
-  (call_expr, return_type, impl, doc) = @match fun_expr begin
+  (call_expr, return_type, impl, doc) = @match fun_head begin
     Expr(:(::), Expr(:call, args...), return_type) =>
       (Expr(:call, args...), return_type, impl, doc)
     Expr(:call, args...) =>
       (Expr(:call, args...), nothing, impl, doc)
-    _ => throw(ParseError("Ill-formed function header $fun_expr"))
+    _ => throw(ParseError("Ill-formed function header $fun_head"))
   end
   (name, args, kwargs) = @match call_expr begin
     Expr(:call, name, Expr(:parameters, kwargs...), args...) => (name, args, kwargs)
@@ -137,14 +147,17 @@ function generate_function(fun::JuliaFunction; rename=n->n)::Expr
     []
   end
   call_expr = Expr(:call, rename(fun.name), kwargsblock..., fun.args...)
-  if !isempty(fun.whereparams)
-    call_expr = Expr(:where, call_expr, fun.whereparams...)
+
+  if !isnothing(fun.return_type)
+    call_expr = Expr(:(::), call_expr, fun.return_type)
   end
-  head = if isnothing(fun.return_type)
+
+  head = if isempty(fun.whereparams)
     call_expr
-  else 
-    Expr(:(::), call_expr, fun.return_type)
+  else
+    Expr(:where, call_expr, fun.whereparams...)
   end
+
   body = if isnothing(fun.impl)
     Expr(:block)
   else
diff --git a/test/stdlib/models/Arithmetic.jl b/test/stdlib/models/Arithmetic.jl
index 07bb6a39..85e3fedd 100644
--- a/test/stdlib/models/Arithmetic.jl
+++ b/test/stdlib/models/Arithmetic.jl
@@ -15,10 +15,9 @@ end
 #--------------------------------------
 using .ThMonoid
 
-IM = IntMonoid(IntNatPlus())
-@withmodel IM (e) begin
+@withmodel IntMonoid (e) begin
   @test e() == 0
-  @test (ThMonoid.:(⋅)[IM])(3, 4) == 7
+  @test (ThMonoid.:(⋅)[IntMonoid])(3, 4) == 7
 end
 
 # Integers as preorder
@@ -26,7 +25,7 @@ end
 using .ThPreorder
 
 @withmodel IntPreorder() (Leq, refl, trans) begin
-  @test trans((1,3), (3,5)) == (1,5)
+  @test trans((1,3), (3,5)) == (1,5)  
   @test_throws TypeCheckFail Leq((5,3), 5, 3)
   @test refl(2) == (2,2)
 end
@@ -34,9 +33,8 @@ end
 # Now using category interface
 
 using .ThCategory
-M = IntPreorderCat(IntPreorder())
 
-@withmodel M (Hom, id, compose) begin
+@withmodel IntPreorderCat (Hom, id, compose) begin
   @test compose((1,3), (3,5)) == (1,5)
   @test_throws TypeCheckFail Hom((5,3), 5, 3)
   @test_throws ErrorException compose((1,2), (3,5))
diff --git a/test/stdlib/models/Op.jl b/test/stdlib/models/Op.jl
index 01882147..b0e698f2 100644
--- a/test/stdlib/models/Op.jl
+++ b/test/stdlib/models/Op.jl
@@ -24,8 +24,7 @@ end
 # Theory-morphism Op
 #-------------------
 
-M = OpFinSetC(FinSetC())
-@withmodel M (Ob, Hom, id, compose, dom, codom) begin
+@withmodel OpFinSetC (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)

From ed4ecef5c55204023b090ba9b6b35d94a30fb6f2 Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Mon, 16 Oct 2023 13:32:02 -0700
Subject: [PATCH 02/13] fix docstring

---
 src/models/ModelInterface.jl | 101 +++++++++++++++++------------------
 1 file changed, 49 insertions(+), 52 deletions(-)

diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl
index 2cbeeeaa..3e5cd477 100644
--- a/src/models/ModelInterface.jl
+++ b/src/models/ModelInterface.jl
@@ -582,88 +582,86 @@ end
 
 
 """
-Given a Theory Morphism T->U and a type Mᵤ (whose values are models of U),
-obtain a type Mₜ which has one parameter (of type Mᵤ) and is a model of T.
-
-E.g. given NatIsMonoid: ThMonoid->ThNatPlus and IntPlus <: Model{Tuple{Int}}
-and IntPlus implements ThNatPlus:
-
-```
-@migrate IntPlusMonoid = NatIsMonoid(IntPlus){Int}
-```
-
-Yields:
-
-```
-struct IntPlusMonoid <: Model{Tuple{Int}}
-  model::IntPlus
-end
-
-@instance ThMonoid{Int} [model::IntPlusMonoid] begin ... end
-```
+Given a Theory Morphism T->U and a model Mᵤ which implements U,
+obtain a model Mₜ which wraps Mᵤ and is a model of T.
 
 Future work: There is some subtlety in how accessor functions should be handled.
 TODO: The new instance methods do not yet handle the `context` keyword argument.
 """
 function migrator(tmap, dom_module, codom_module, dom_theory, codom_theory)
 
+  # Symbols
+  migrator_name = :Migrator # TODO do we need to gensym?
+  _x = gensym("val")
+
   # Map CODOM sorts to whereparam symbols
   whereparamdict = OrderedDict(s=>gensym(s.head.name) for s in sorts(codom_theory))
+  # New model is parameterized by these types
   whereparams = collect(values(whereparamdict))
-  name = :Migrator #gensym("migrator")
-  _x = gensym("val")
-
+  # Julia types of domain sorts determined by theorymap 
   jltype_by_sort = Dict(map(sorts(dom_theory)) do v
     v => whereparamdict[AlgSort(tmap(v.method).val)]
   end)
 
-  accessor_funs = [] # accessors
+  # Create input for instance_code
+  ################################
+  accessor_funs = JuliaFunction[] # added to during typecon_funs loop
 
-  # TypeCons for @instance macro
   typecon_funs = map(collect(typemap(tmap))) do (x, fx)
     typecon = getvalue(dom_theory[x])
+
     # Accessors
-    eq = equations(codom_theory, fx)
+    #----------
+    # accessor arg is a value of the type constructor's result type
     args = [:($_x::$(jltype_by_sort[AlgSort(typecon.declaration, x)]))]
-    scopedict = Dict{ScopeTag,ScopeTag}(gettag(typecon.localcontext)=>gettag(fx.ctx))
-    for accessor in idents(typecon.localcontext; lid=typecon.args)
-      accessor = retag(scopedict, accessor)
-      a = nameof(accessor)
-      # If we have a default means of computing the accessor...
+    # Equations are how the value of the accessor is related to the type 
+    eq = equations(codom_theory, fx)
+    scopedict = Dict(gettag(typecon.localcontext) => gettag(fx.ctx))
+    accessors = idents(typecon.localcontext; lid=typecon.args)
+    for accessor in retag.(Ref(scopedict), accessors)
+      name = nameof(accessor)
+      # If we have a means of computing the accessor...
       if !isempty(eq[accessor])
-        rtype = typecon.localcontext[ident(typecon.localcontext; name=a)]
-        ret_type = jltype_by_sort[AlgSort(getvalue(rtype))]
+        rtype = typecon.localcontext[ident(typecon.localcontext; name)]
+        return_type = jltype_by_sort[AlgSort(getvalue(rtype))]
+        # Convert accessor expression into Julia expression
         impl = to_call_accessor(first(eq[accessor]), _x, codom_module)
-        jf = JuliaFunction(;name=a, args=args, return_type=ret_type, impl=impl)
-        push!(accessor_funs, jf)
+        push!(accessor_funs, JuliaFunction(;name, args, return_type, impl))
       end
     end
 
-    # Typecon function
-    codom_body = bodyof(fx.val)
+    # Type constructor function
+    #--------------------------
+    codom_body = bodyof(fx.val) 
     fxname = nameof(headof(codom_body))
-    xname = nameof(typecon.declaration)
     sig = julia_signature(dom_theory, x, jltype_by_sort)
+    
+    name = nameof(typecon.declaration)
+
     argnames = [_x, nameof.(argsof(typecon))...]
     args = [:($k::$(v)) for (k, v) in zip(argnames, sig.types)]
-    impls = to_call_impl.(codom_body.args, Ref(termcons(codom_theory)), Ref(codom_module))
-    impl = Expr(:call, Expr(:ref, :($codom_module.$fxname), :(model.model)), _x, impls...)
-    JuliaFunction(;name=xname, args=args, return_type=sig.types[1], impl=impl)
+    
+    return_type = first(sig.types)
+
+    impls = to_call_impl.(codom_body.args, Ref(codom_module))
+    impl = Expr(:call, Expr(:ref, :($codom_module.$fxname), 
+                            :(model.model)), _x, impls...)
+
+    JuliaFunction(;name, args, return_type, impl)
   end
 
-  # TermCons for @instance macro
+  # Term constructors
+  #------------------
   termcon_funs = map(collect(termmap(tmap))) do (x, fx)
     termcon = getvalue(dom_theory[x])
-    func_name = nameof(termcon.declaration)
     sig = julia_signature(dom_theory, x, jltype_by_sort)
-    argnames = nameof.(argsof(termcon))
-    ret_type = jltype_by_sort[AlgSort(termcon.type)]
-
-    args = [:($k::$v) for (k, v) in zip(argnames, sig.types)]
 
-    impl = to_call_impl(fx.val, first.(termcons(codom_theory)), codom_module)
+    name = nameof(termcon.declaration)
+    return_type = jltype_by_sort[AlgSort(termcon.type)]
+    args = [:($k::$v) for (k, v) in zip(nameof.(argsof(termcon)), sig.types)]
+    impl = to_call_impl(fx.val, codom_module)
 
-    JuliaFunction(;name=func_name, args=args, return_type=ret_type, impl=impl)
+    JuliaFunction(;name, args, return_type, impl)
   end
 
 
@@ -672,7 +670,7 @@ function migrator(tmap, dom_module, codom_module, dom_theory, codom_theory)
     dom_theory,
     dom_module,
     jltype_by_sort,
-    Expr(:curly, name, whereparams...),
+    Expr(:curly, migrator_name, whereparams...),
     whereparams,
     Expr(:block, generate_function.([typecon_funs...,
                                      termcon_funs..., 
@@ -707,14 +705,13 @@ end
 Compile an AlgTerm into a Julia call Expr where termcons (e.g. `f`) are
 interpreted as `mod.f[model.model](...)`.
 """
-function to_call_impl(t::AlgTerm, termcons, mod::Module)
+function to_call_impl(t::AlgTerm, mod::Module)
   b = bodyof(t)
   if GATs.isvariable(t)
     nameof(b)
   else 
-    args = to_call_impl.(argsof(b), Ref(termcons), Ref(mod))
+    args = to_call_impl.(argsof(b), Ref(mod))
     name = nameof(headof(b))
-    b.head in termcons || error("t $t termcons $termcons")
     Expr(:call, Expr(:ref, :($mod.$name), :(model.model)), args...)
   end
 end

From 62422a536fe90fdfd8e1e28d2d1813ae235017ab Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Fri, 20 Oct 2023 02:28:04 -0700
Subject: [PATCH 03/13] working pushouts

---
 src/GATlab.jl                               |   1 +
 src/models/ModelInterface.jl                | 104 ++++++++++++---
 src/nonstdlib/models/Pushouts.jl            |  41 ++++++
 src/nonstdlib/models/module.jl              |  10 ++
 src/nonstdlib/module.jl                     |  15 +++
 src/nonstdlib/theories/Pushouts.jl          |  52 ++++++++
 src/nonstdlib/theories/module.jl            |  10 ++
 src/stdlib/derivedmodels/DerivedModels.jl   |   2 +-
 src/syntax/GATs.jl                          |  13 +-
 src/syntax/TheoryInterface.jl               |  30 ++++-
 src/syntax/gats/algorithms.jl               |  36 +++++
 src/syntax/gats/ast.jl                      |  77 ++++++++---
 src/syntax/gats/exprinterop.jl              | 140 ++++++++++++++++----
 src/syntax/gats/gat.jl                      |  41 +++++-
 src/syntax/gats/judgments.jl                | 100 ++++++++++++--
 test/Project.toml                           |   1 +
 test/nonstdlib/Pushouts.jl                  |  28 ++++
 test/nonstdlib/tests.jl                     |   5 +
 test/runtests.jl                            |   5 +
 test/stdlib/{models => }/Arithmetic.jl      |   0
 test/stdlib/{models => }/FinMatrices.jl     |   0
 test/stdlib/{models => }/FinSets.jl         |   0
 test/stdlib/{models => }/GATs.jl            |   0
 test/stdlib/{models => }/Nothings.jl        |   0
 test/stdlib/{models => }/Op.jl              |   0
 test/stdlib/{models => }/SliceCategories.jl |   0
 test/stdlib/models/tests.jl                 |  11 --
 test/stdlib/tests.jl                        |  12 +-
 test/syntax/GATs.jl                         |  21 ++-
 29 files changed, 643 insertions(+), 112 deletions(-)
 create mode 100644 src/nonstdlib/models/Pushouts.jl
 create mode 100644 src/nonstdlib/models/module.jl
 create mode 100644 src/nonstdlib/module.jl
 create mode 100644 src/nonstdlib/theories/Pushouts.jl
 create mode 100644 src/nonstdlib/theories/module.jl
 create mode 100644 test/nonstdlib/Pushouts.jl
 create mode 100644 test/nonstdlib/tests.jl
 rename test/stdlib/{models => }/Arithmetic.jl (100%)
 rename test/stdlib/{models => }/FinMatrices.jl (100%)
 rename test/stdlib/{models => }/FinSets.jl (100%)
 rename test/stdlib/{models => }/GATs.jl (100%)
 rename test/stdlib/{models => }/Nothings.jl (100%)
 rename test/stdlib/{models => }/Op.jl (100%)
 rename test/stdlib/{models => }/SliceCategories.jl (100%)
 delete mode 100644 test/stdlib/models/tests.jl

diff --git a/src/GATlab.jl b/src/GATlab.jl
index 39bdf22a..bc3b0dc5 100644
--- a/src/GATlab.jl
+++ b/src/GATlab.jl
@@ -7,6 +7,7 @@ include("util/module.jl")
 include("syntax/module.jl")
 include("models/module.jl")
 include("stdlib/module.jl")
+include("nonstdlib/module.jl") # don't reexport this
 
 @reexport using .Util
 @reexport using .Syntax
diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl
index 3e5cd477..088921dd 100644
--- a/src/models/ModelInterface.jl
+++ b/src/models/ModelInterface.jl
@@ -145,7 +145,18 @@ macro instance(head, model, body)
   theory = macroexpand(__module__, :($theory_module.Meta.@theory))
 
   # A dictionary to look up the Julia type of a type constructor from its name (an ident)
-  jltype_by_sort = Dict(zip(sorts(theory), instance_types)) # for type checking
+  i = 0
+  jltype_by_sort = Dict(map(sorts(theory)) do s 
+    sorttype = getvalue(theory[methodof(s)])
+    s => if sorttype isa AlgTypeConstructor 
+      i += 1
+      instance_types[i]
+    elseif sorttype isa AlgStruct
+      nameof(sorttype.declaration)
+    end
+  end)
+  i == length(instance_types) || error("Did not use all types ($i): $instance_types")
+
 
   # Get the model type that we are overloading for, or nothing if this is the
   # default instance for `instance_types`
@@ -176,7 +187,7 @@ function generate_instance(
   # methods for type constructors and type argument accessors if these methods
   # are missing
   typechecked_functions = if typecheck
-    typecheck_instance(theory, functions, ext_functions, jltype_by_sort; oldinstance)
+    typecheck_instance(theory, functions, ext_functions, jltype_by_sort; oldinstance, theory_module)
   else
     [functions..., ext_functions...] # skip typechecking and expand_fail
   end
@@ -187,15 +198,16 @@ function generate_instance(
   # to
   # `ThCategory.Ob(m::WithModel{M}, x; context=nothing) = let model = m.model in blah end`
   qualified_functions =
-    map(fun -> qualify_function(fun, theory_module, model_type, whereparams), typechecked_functions)
+    map(fun -> qualify_function(fun, theory_module, model_type, whereparams, 
+                                Set(nameof.(structs(theory)))), 
+        typechecked_functions)
 
   append!(
     qualified_functions,
-    make_alias_definitions(theory, theory_module, jltype_by_sort, model_type, whereparams, ext_functions)
+    make_alias_definitions(theory, theory_module, jltype_by_sort, model_type, 
+                           whereparams, ext_functions)
   )
 
-  # Add overloads for the alias methods
-
   # Declare that this model implements the theory
 
   implements_declarations = if !isnothing(model_type)
@@ -302,7 +314,7 @@ function julia_signature(
   args = if oldinstance && isempty(sortsig)
     Expr0[Expr(:curly, :Type, jltype_by_sort[AlgSort(termcon.type)])]
   else
-    Expr0[jltype_by_sort[sort] for sort in sortsignature(termcon)]
+    Expr0[jltype_by_sort[sort] for sort in sortsig if !sort.eq]
   end
   JuliaFunctionSig(
     nameof(getdecl(termcon)),
@@ -332,6 +344,16 @@ function julia_signature(
   JuliaFunctionSig(nameof(getdecl(acc)), [jlargtype])
 end
 
+
+function julia_signature(str::AlgFunction, jltype_by_sort::Dict{AlgSort}; kw...)
+  sortsig = sortsignature(str)
+  args = Expr0[jltype_by_sort[sort] for sort in sortsig]
+  JuliaFunctionSig(
+    nameof(getdecl(str)),
+    args
+  )
+end
+
 function ExprInterop.toexpr(sig::JuliaFunctionSig)
   Expr(:call, sig.name, [Expr(:(::), type) for type in sig.types]...)
 end
@@ -364,6 +386,7 @@ function typecheck_instance(
   ext_functions::Vector{Symbol},
   jltype_by_sort::Dict{AlgSort};
   oldinstance=false,
+  theory_module=nothing,
 )::Vector{JuliaFunction}
   typechecked = JuliaFunction[]
 
@@ -378,14 +401,24 @@ function typecheck_instance(
       continue
     end
     for (_, x) in allmethods(resolver)
+      if getvalue(theory[x]) isa AlgStruct 
+        continue 
+      end
       sig = julia_signature(getvalue(theory[x]), jltype_by_sort; oldinstance, X=x) |> JuliaFunctionSigNoWhere
       if haskey(undefined_signatures, sig)
-        error(overload_errormsg)
+        error(overload_errormsg * ": $x vs $(undefined_signatures[sig])")
       end
       undefined_signatures[sig] = (decl, x)
     end
   end
 
+  for x in getidents(theory)
+    v = getvalue(theory[x])
+    if v isa AlgFunction 
+      push!(typechecked, mk_fun(v, theory, theory_module, jltype_by_sort))
+    end 
+  end
+
   expected_signatures = DefaultDict{Ident, Set{Expr0}}(()->Set{Expr0}())
 
   for (sig, (decl, _)) in undefined_signatures
@@ -432,7 +465,7 @@ function typecheck_instance(
   for (sig, (decl, method)) in undefined_signatures
     judgment = getvalue(theory[method])
     if judgment isa AlgTermConstructor
-      error("Failed to implement $(toexpr(sig))")
+      error("Failed to implement $decl: $(toexpr(sig))")
     elseif judgment isa AlgTypeConstructor
       push!(typechecked, default_typecon_impl(method, theory, jltype_by_sort))
     elseif judgment isa AlgAccessor
@@ -464,6 +497,15 @@ function expand_fail(theory::GAT, x::Ident, f::JuliaFunction)
   )
 end
 
+function mk_fun(f::AlgFunction, theory, mod, jltype_by_sort)
+  name = nameof(f.declaration)
+  args = map(zip(f.args, sortsignature(f))) do (i,s)
+    Expr(:(::),nameof(f[i]),jltype_by_sort[s])
+  end
+  impl = to_call_impl(f.value,theory, mod, false)
+  JuliaFunction(;name=name, args, impl)
+end
+
 function make_alias_definitions(theory, theory_module, jltype_by_sort, model_type, whereparams, ext_functions)
   lines = []
   oldinstance = isnothing(model_type)
@@ -471,7 +513,7 @@ function make_alias_definitions(theory, theory_module, jltype_by_sort, model_typ
     for binding in segment
       alias = getvalue(binding)
       name = nameof(binding)
-      if alias isa Alias && name ∉ ext_functions
+      if alias isa Alias && nameof(alias.ref) ∉ ext_functions
         for (argsorts, method) in allmethods(theory.resolvers[alias.ref])
           args = [(gensym(), jltype_by_sort[sort]) for sort in argsorts]
           args = if oldinstance
@@ -504,9 +546,10 @@ end
 """
 Add `WithModel` param first, if this is not an old instance (it shouldn't have it already)
 Qualify method name to be in theory module
+Qualify args to struct types
 Add `context` kwargs if not already present
 """
-function qualify_function(fun::JuliaFunction, theory_module, model_type::Union{Expr0, Nothing}, whereparams)
+function qualify_function(fun::JuliaFunction, theory_module, model_type::Union{Expr0, Nothing}, whereparams, structnames)
   kwargs = filter(fun.kwargs) do kwarg
     @match kwarg begin
       Expr(:kw, :context, _) => false
@@ -517,11 +560,18 @@ function qualify_function(fun::JuliaFunction, theory_module, model_type::Union{E
     end
   end
   kwargs = Expr0[Expr(:kw, :context, nothing); kwargs]
-
   (args, impl) = if !isnothing(model_type)
+    args = map(fun.args) do arg
+      @match arg begin
+        Expr(:(::), argname, ty) => Expr(:(::), argname,
+          ty ∈ structnames ? Expr(:., theory_module, QuoteNode(ty)) : ty )
+        _ => arg
+      end
+    end
+
     m = gensym(:m)
     (
-      [Expr(:(::), m, Expr(:curly, TheoryInterface.WithModel, model_type)), fun.args...],
+      [Expr(:(::), m, Expr(:curly, TheoryInterface.WithModel, model_type)), args...],
       Expr(:let, Expr(:(=), :model, :($m.model)), fun.impl)
     )
   else
@@ -542,9 +592,12 @@ end
 function implements_declaration(model_type, scope, whereparams)
   notes = ImplementationNotes(nothing)
   quote
-    $(GlobalRef(ModelInterface, :implements))(
-      ::$(model_type), ::Type{Val{$(gettag(scope))}}
-    ) where {$(whereparams...)} = $notes
+    if !hasmethod($(GlobalRef(ModelInterface, :implements)), 
+        ($(model_type) where {$(whereparams...)}, Type{Val{$(gettag(scope))}}))
+      $(GlobalRef(ModelInterface, :implements))(
+        ::$(model_type), ::Type{Val{$(gettag(scope))}}
+      ) where {$(whereparams...)} = $notes
+    end
   end
 end
 
@@ -643,7 +696,7 @@ function migrator(tmap, dom_module, codom_module, dom_theory, codom_theory)
     
     return_type = first(sig.types)
 
-    impls = to_call_impl.(codom_body.args, Ref(codom_module))
+    impls = to_call_impl.(codom_body.args, Ref(codom_theory), Ref(codom_module), true)
     impl = Expr(:call, Expr(:ref, :($codom_module.$fxname), 
                             :(model.model)), _x, impls...)
 
@@ -659,7 +712,7 @@ function migrator(tmap, dom_module, codom_module, dom_theory, codom_theory)
     name = nameof(termcon.declaration)
     return_type = jltype_by_sort[AlgSort(termcon.type)]
     args = [:($k::$v) for (k, v) in zip(nameof.(argsof(termcon)), sig.types)]
-    impl = to_call_impl(fx.val, codom_module)
+    impl = to_call_impl(fx.val, codom_theory, codom_module, true)
 
     JuliaFunction(;name, args, return_type, impl)
   end
@@ -705,14 +758,21 @@ end
 Compile an AlgTerm into a Julia call Expr where termcons (e.g. `f`) are
 interpreted as `mod.f[model.model](...)`.
 """
-function to_call_impl(t::AlgTerm, mod::Module)
+function to_call_impl(t::AlgTerm, theory::GAT, mod::Union{Symbol,Module}, migrate::Bool)
   b = bodyof(t)
   if GATs.isvariable(t)
     nameof(b)
-  else 
-    args = to_call_impl.(argsof(b), Ref(mod))
+  elseif  GATs.isdot(t)
+    Expr(:., to_call_impl(b.body, theory, mod, migrate), QuoteNode(b.head))
+  else
+    args = to_call_impl.(argsof(b), Ref(theory), Ref(mod), migrate)
     name = nameof(headof(b))
-    Expr(:call, Expr(:ref, :($mod.$name), :(model.model)), args...)
+    newhead = if name ∈ nameof.(structs(theory))
+      Expr(:., :($mod), QuoteNode(name))
+    else 
+      Expr(:ref, :($mod.$name), migrate ? :(model.model) : :model)
+    end
+    Expr(:call, newhead, args...)
   end
 end
 
diff --git a/src/nonstdlib/models/Pushouts.jl b/src/nonstdlib/models/Pushouts.jl
new file mode 100644
index 00000000..06f93765
--- /dev/null
+++ b/src/nonstdlib/models/Pushouts.jl
@@ -0,0 +1,41 @@
+using DataStructures, StructEquality
+
+export PushoutInt
+
+using GATlab
+
+"""Data required to specify a pushout. No fancy caching."""
+@struct_hash_equal struct PushoutInt
+  ob::Int
+  i1::Vector{Int}
+  i2::Vector{Int}
+end
+
+using .ThPushout 
+
+@instance ThPushout{Int, Vector{Int}, PushoutInt} [model::FinSetC] begin
+  @import Ob, Hom, id, compose, dom, codom
+  function pushout(sp::Span; context)
+    B, C = context[:d], context[:c]
+    d = DataStructures.IntDisjointSets(B+C)
+    [union!(d, sp.left[a], sp.right[a]+B) for a in 1:sp.apex]
+    roots = DataStructures.find_root!.(Ref(d), 1:length(d))
+    rootindex = sort(collect(Set(values(roots))))
+    toindex = [findfirst(==(r),rootindex) for r in roots]
+    PushoutInt(DataStructures.num_groups(d), 
+     [toindex[roots[b]] for b in 1:B], 
+     [toindex[roots[c+B]] for c in 1:C]
+    )
+  end
+  cospan(p::PushoutInt) = Cospan(p.ob, p.i1, p.i2)
+  function universal(p::PushoutInt, csp::Cospan; context)
+    map(1:p.ob) do i
+      for (proj, csp_map) in [(p.i1, csp.left), (p.i2, csp.right)]
+        for (j, i′) in enumerate(proj)
+          if i′ == i return csp_map[j] end
+        end
+      end
+      error("Pushout is jointly surjective")
+    end
+  end
+end
diff --git a/src/nonstdlib/models/module.jl b/src/nonstdlib/models/module.jl
new file mode 100644
index 00000000..8279b837
--- /dev/null
+++ b/src/nonstdlib/models/module.jl
@@ -0,0 +1,10 @@
+module NonStdModels
+
+using ...Syntax
+using ...Models
+using ...Stdlib
+using ..NonStdTheories
+
+include("Pushouts.jl")
+
+end
diff --git a/src/nonstdlib/module.jl b/src/nonstdlib/module.jl
new file mode 100644
index 00000000..be91a91f
--- /dev/null
+++ b/src/nonstdlib/module.jl
@@ -0,0 +1,15 @@
+module NonStdlib
+
+using Reexport
+
+include("theories/module.jl")
+include("models/module.jl")
+# include("theorymaps/module.jl")
+# include("derivedmodels/module.jl")
+
+@reexport using .NonStdTheories
+@reexport using .NonStdModels
+# @reexport using .StdTheoryMaps
+# @reexport using .StdDerivedModels
+
+end
diff --git a/src/nonstdlib/theories/Pushouts.jl b/src/nonstdlib/theories/Pushouts.jl
new file mode 100644
index 00000000..0173e9ae
--- /dev/null
+++ b/src/nonstdlib/theories/Pushouts.jl
@@ -0,0 +1,52 @@
+"""
+A theory of a category with pushouts highlights two features of 
+GATs which require syntactic sugar. The first is an operation 
+with a (dependent) record type as its output.
+
+The second is the type of equality witnesses for any given 
+AlgSort. This allows us to define functions which are only 
+valid when certain *derived terms* from the arguments are 
+equal. (E.g. when to apply universal property of a pushout).
+"""
+
+export ThPushout
+
+@theory ThSpanCospan <: ThCategory begin
+  struct Span(dom::Ob, codom::Ob)
+    apex::Ob
+    left::(apex→dom)
+    right::(apex→codom)
+  end
+
+  struct Cospan(dom::Ob, codom::Ob)
+    apex::Ob
+    left::(dom→apex)
+    right::(codom→apex)
+  end
+end
+
+"""A category with pushouts"""
+@theory ThPushout <: ThSpanCospan begin
+  Pushout(s)::TYPE                       ⊣ [(d,c)::Ob, s::Span(d,c)]
+  pushout(s)::Pushout(s)                 ⊣ [(d,c)::Ob, s::Span(d,c)] # compute representative
+  cospan(p::Pushout(s))::Cospan(d,c)     ⊣ [(d,c)::Ob, s::Span(d,c)] # extract result
+  apex(p::Pushout(s)) := cospan(p).apex  ⊣ [(d,c)::Ob, s::Span(d,c)]
+  ι₁(p::Pushout(s))   := cospan(p).left  ⊣ [(d,c)::Ob, s::Span(d,c)]
+  ι₂(p::Pushout(s))   := cospan(p).right ⊣ [(d,c)::Ob, s::Span(d,c)]
+  
+  (pushout_commutes :=  (s.left)⋅ι₁(p) == (s.right)⋅ι₂(p)
+    ⊣ [(d,c)::Ob, s::Span(d,c), p::Pushout(s)])
+
+  (universal(p, csp, eq) :: (apex(p) → csp.apex)
+    ⊣ [(d,c)::Ob, sp::Span(d,c), csp::Cospan(d,c), p::Pushout(sp),
+        eq::(sp.left⋅csp.left == sp.right⋅csp.right)])
+
+  ((ι₁(p) ⋅ universal(p, csp, eq) == csp.left)
+    ⊣ [(d,c)::Ob, sp::Span(d,c), csp::Cospan(d,c), p::Pushout(sp),
+        eq::(sp.left⋅csp.left == sp.right⋅csp.right)])
+
+  ((ι₂(p) ⋅ universal(p, csp, eq) == csp.right)
+    ⊣ [(d,c)::Ob, sp::Span(d,c), csp::Cospan(d,c), p::Pushout(sp),
+        eq::(sp.left⋅csp.left == sp.right⋅csp.right)])
+end
+
diff --git a/src/nonstdlib/theories/module.jl b/src/nonstdlib/theories/module.jl
new file mode 100644
index 00000000..ac482603
--- /dev/null
+++ b/src/nonstdlib/theories/module.jl
@@ -0,0 +1,10 @@
+module NonStdTheories
+
+using ...Syntax
+using ...Stdlib
+
+using Reexport
+
+include("Pushouts.jl")
+
+end
diff --git a/src/stdlib/derivedmodels/DerivedModels.jl b/src/stdlib/derivedmodels/DerivedModels.jl
index 6723655a..a2b80cb1 100644
--- a/src/stdlib/derivedmodels/DerivedModels.jl
+++ b/src/stdlib/derivedmodels/DerivedModels.jl
@@ -14,4 +14,4 @@ IntMonoid = migrate(NatPlusMonoid, IntNatPlus())
 # Interpret `id` as reflexivity and `compose` as transitivity.
 IntPreorderCat = migrate(PreorderCat, IntPreorder())
 
-end
+end # module
diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl
index 964b6c8f..629192c0 100644
--- a/src/syntax/GATs.jl
+++ b/src/syntax/GATs.jl
@@ -1,12 +1,15 @@
 module GATs
 export Constant, AlgTerm, AlgType, AlgAST,
   TypeScope, TypeCtx, AlgSort, AlgSorts,
-  AlgDeclaration, AlgTermConstructor, AlgTypeConstructor, AlgAccessor, AlgAxiom,
-  sortsignature, getdecl,
-  GATSegment, GAT, GATContext, gettheory, gettypecontext, allmethods, resolvemethod,
-  termcons,typecons, accessors,
+  AlgDeclaration, AlgTermConstructor, 
+  AlgTypeConstructor, AlgAccessor, AlgAxiom, AlgStruct, AlgDot, AlgFunction,
+  typesortsignature, sortsignature, getdecl,
+  GATSegment, GAT, GATContext, gettheory, gettypecontext, allmethods, 
+  resolvemethod, resolvefield,
+  termcons,typecons, accessors, structs,
   equations, build_infer_expr, compile, sortcheck, allnames, sorts, sortname,
-  InCtx, TermInCtx, TypeInCtx, headof, argsof, methodof, bodyof, argcontext
+  InCtx, TermInCtx, TypeInCtx, headof, argsof, methodof, bodyof, argcontext,
+  infer_type
 
 using ..Scopes
 import ..ExprInterop: fromexpr, toexpr
diff --git a/src/syntax/TheoryInterface.jl b/src/syntax/TheoryInterface.jl
index 543dee0c..48d24685 100644
--- a/src/syntax/TheoryInterface.jl
+++ b/src/syntax/TheoryInterface.jl
@@ -3,11 +3,11 @@ export @theory, @signature, Model, invoke_term
 
 using ..Scopes, ..GATs, ..ExprInterop
 
-using MLStyle
+using MLStyle, StructEquality
 
 abstract type Model{Tup <: Tuple} end
 
-struct WithModel{M <: Model}
+@struct_hash_equal struct WithModel{M <: Model}
   model::M
 end
 
@@ -78,13 +78,16 @@ function theory_impl(head, body, __module__)
 
   lines = Any[]
   newnames = Symbol[]
-
+  structlines = Expr[]
+  structnames = Set([nameof(s.declaration) for s in structs(theory)])
   for binding in newsegment
     judgment = getvalue(binding)
     bname = nameof(binding)
-    if judgment isa Union{AlgDeclaration, Alias}
+    if judgment isa Union{AlgDeclaration, Alias} && bname ∉ structnames
       push!(lines, juliadeclaration(bname))
       push!(newnames, bname)
+    elseif judgment isa AlgStruct 
+      push!(structlines, mk_struct(judgment, fqmn(__module__)))
     end
   end
 
@@ -123,6 +126,7 @@ function theory_impl(head, body, __module__)
       :(
         module $name
         $(modulelines...)
+        $(structlines...)
         end
       ),
       :(Core.@__doc__ $(name)),
@@ -161,4 +165,22 @@ function invoke_term(theory_module, types, name, args; model=nothing)
   end
 end
 
+
+"""
+
+"""
+function mk_struct(s::AlgStruct, mod)
+  fields = map(s.args) do i
+    Expr(:(::), nameof(s[i]), nameof(AlgSort(getvalue(s[i]))))
+  end 
+  sorts = unique([f.args[2] for f in fields])
+  she = Expr(:macrocall, GlobalRef(StructEquality, Symbol("@struct_hash_equal")), mod, nameof(s))
+  quote
+    struct $(nameof(s)){$(sorts...)}
+      $(fields...)
+    end
+
+    $she
+  end
+end
 end
diff --git a/src/syntax/gats/algorithms.jl b/src/syntax/gats/algorithms.jl
index 2076c702..51a1f378 100644
--- a/src/syntax/gats/algorithms.jl
+++ b/src/syntax/gats/algorithms.jl
@@ -5,16 +5,24 @@ Throw an error if a the head of an AlgTerm (which refers to a term constructor)
 has arguments of the wrong sort. Returns the sort of the term.
 """
 function sortcheck(ctx::Context, t::AlgTerm)::AlgSort
+  t_sub = substitute_funs(ctx, t)
+  if t_sub != t 
+    return sortcheck(ctx, t_sub)
+  end 
   if isapp(t)
     judgment = ctx[t.body.method] |> getvalue
     if judgment isa AlgTermConstructor
       argsorts = sortcheck.(Ref(ctx), t.body.args)
       argsorts == sortsignature(judgment) || error("Sorts don't match")
       AlgSort(judgment.type)
+    else
+      error("Unexpected app $t") 
     end
   elseif isvariable(t)
     type = ctx[t.body] |> getvalue
     AlgSort(type)
+  elseif isdot(t)
+    AlgSort(ctx, t)
   else
     AlgSort(t.body.type)
   end
@@ -173,3 +181,31 @@ end
 function substitute_term(ma::MethodApp{AlgTerm}, subst::Dict{Ident, AlgTerm})
   MethodApp{AlgTerm}(ma.head, ma.method, substitute_term.(ma.args, Ref(subst)))
 end
+
+function substitute_term(ad::AlgDot, subst::Dict{Ident, AlgTerm})
+  AlgDot(ad.head, substitute_term(ad.body, subst), ad.sort)
+end
+
+
+"""Replace all functions with their desugared expressions"""
+function substitute_funs(ctx::Context, t::AlgTerm)
+  b = bodyof(t)
+  if isapp(t)
+    m = getvalue(ctx[methodof(b)])
+    if m isa AlgTermConstructor
+      args = substitute_funs.(Ref(ctx), argsof(b))
+      AlgTerm(MethodApp{AlgTerm}(headof(b), methodof(b), args))
+    elseif m isa AlgFunction 
+      subst = Dict(zip(idents(m.localcontext; lid=m.args), argsof(b)))
+      substitute_term(m.value, subst)
+    else 
+      error("Bad app $m")
+    end
+  elseif isvariable(t) || isconstant(t)
+    t 
+  elseif isdot(t)
+    AlgTerm(AlgDot(headof(b), substitute_funs(ctx, bodyof(b)), b.sort))
+  else 
+    error("Bad term $t")
+  end
+end
\ No newline at end of file
diff --git a/src/syntax/gats/ast.jl b/src/syntax/gats/ast.jl
index 94796d15..18c91662 100644
--- a/src/syntax/gats/ast.jl
+++ b/src/syntax/gats/ast.jl
@@ -6,6 +6,11 @@ We need this to resolve a mutual reference loop; the only subtype is Constant
 """
 abstract type AbstractConstant end
 
+"""
+We need this to resolve a mutual reference loop; the only subtype is Dot
+"""
+abstract type AbstractDot end
+
 """
 `MethodApp`
 
@@ -44,16 +49,14 @@ abstract type AlgAST end
 
 bodyof(t::AlgAST) = t.body
 
+
 """
 `AlgTerm`
 
 One syntax tree to rule all the terms.
 """
 @struct_hash_equal struct AlgTerm <: AlgAST
-  body::Union{Ident, MethodApp{AlgTerm}, AbstractConstant}
-  function AlgTerm(body::Union{Ident, MethodApp{AlgTerm}, AbstractConstant})
-    new(body)
-  end
+  body::Union{Ident, MethodApp{AlgTerm}, AbstractConstant, AbstractDot}
 end
 
 
@@ -71,6 +74,8 @@ isvariable(t::AlgTerm) = t.body isa Ident
 
 isapp(t::AlgTerm) = t.body isa MethodApp
 
+isdot(t::AlgAST) = t.body isa AlgDot
+
 isconstant(t::AlgTerm) = t.body isa AbstractConstant
 
 rename(tag::ScopeTag, reps::Dict{Symbol,Symbol}, t::AlgTerm) =
@@ -78,19 +83,8 @@ rename(tag::ScopeTag, reps::Dict{Symbol,Symbol}, t::AlgTerm) =
 
 retag(reps::Dict{ScopeTag, ScopeTag}, t::AlgTerm) = AlgTerm(retag(reps, t.body))
 
-"""
-`Eq`
-
-The type of equality judgments.
-"""
-@struct_hash_equal struct Eq
-  equands::Tuple{AlgTerm, AlgTerm}
-end
-
-retag(reps::Dict{ScopeTag, ScopeTag}, eq::Eq) = Eq(retag.(Ref(reps), eq.equands))
-
-rename(tag::ScopeTag, reps::Dict{Symbol, Symbol}, eq::Eq) =
-  Eq(retag.(Ref(tag), Ref(reps), eq.equands))
+abstract type AbstractEq end # needs to be defined after AlgSort
+abstract type AbstractAlgTup end # needs to be defined after TypeScope
 
 """
 `AlgType`
@@ -98,7 +92,7 @@ rename(tag::ScopeTag, reps::Dict{Symbol, Symbol}, eq::Eq) =
 One syntax tree to rule all the types.
 """
 @struct_hash_equal struct AlgType <: AlgAST
-  body::Union{MethodApp{AlgTerm}, Eq}
+  body::Union{MethodApp{AlgTerm}, AbstractEq, AbstractAlgTup}
 end
 
 function AlgType(fun::Ident, method::Ident)
@@ -118,8 +112,8 @@ isconstant(t::AlgType) = false
 AlgType(head::Ident, method::Ident, args::Vector{AlgTerm}) =
   AlgType(MethodApp{AlgTerm}(head, method, args))
 
-AlgType(lhs::AlgTerm, rhs::AlgTerm) =
-  AlgType(Eq((lhs, rhs)))
+AlgType(c::Context, lhs::AlgTerm, rhs::AlgTerm) =
+  AlgType(Eq((lhs, rhs), AlgSort(c, lhs)))
 
 retag(reps::Dict{ScopeTag,ScopeTag}, t::AlgType) =
   AlgType(retag(reps, t.body))
@@ -146,6 +140,7 @@ A Julia value in an algebraic context. Type checked elsewhere.
   type::AlgType
 end
 
+
 # AlgSorts
 ##########
 
@@ -157,20 +152,33 @@ A *sort*, which is essentially a type constructor without arguments
 @struct_hash_equal struct AlgSort
   head::Ident
   method::Ident
+  eq::Bool
+  AlgSort(h::Ident,m::Ident,eq::Bool=false) = new(h,m,eq)
 end
 
-AlgSort(t::AlgType) = AlgSort(t.body.head, t.body.method)
+AlgSort(t::AlgType) = if iseq(t)
+  AlgSort(t.body.sort.head, t.body.sort.method, true)
+else 
+  AlgSort(t.body.head, t.body.method)
+end
 
+iseq(s::AlgSort) = s.eq
 headof(a::AlgSort) = a.head
 methodof(a::AlgSort) = a.method
 
 function AlgSort(c::Context, t::AlgTerm)
+  t_sub = substitute_funs(c, t)
+  if t_sub != t 
+    return AlgSort(c, t_sub)
+  end
   if isconstant(t)
     AlgSort(t.body.type)
   elseif isapp(t)
     binding = c[t.body.method]
     value = getvalue(binding)
     AlgSort(value.type)
+  elseif isdot(t)
+    AlgSort(resolvefield(c, t.body.sort.method, t.body.head))
   else # variable
     binding = c[t.body]
     AlgSort(getvalue(binding))
@@ -181,6 +189,33 @@ Base.nameof(sort::AlgSort) = nameof(sort.head)
 
 getdecl(s::AlgSort) = s.head
 
+
+"""
+`Eq`
+
+The type of equality judgments.
+"""
+@struct_hash_equal struct Eq <: AbstractEq
+  equands::Tuple{AlgTerm, AlgTerm}
+  sort::AlgSort
+end
+
+retag(reps::Dict{ScopeTag, ScopeTag}, eq::Eq) = Eq(retag.(Ref(reps), eq.equands))
+
+rename(tag::ScopeTag, reps::Dict{Symbol, Symbol}, eq::Eq) =
+  Eq(retag.(Ref(tag), Ref(reps), eq.equands))
+
+
+"""
+Accessing a name from a term of tuple type
+"""
+@struct_hash_equal struct AlgDot <: AbstractDot
+  head::Symbol
+  body::AlgTerm
+  sort::AlgSort
+end
+headof(a::AlgDot) = a.head 
+bodyof(a::AlgDot) = a.body
 # Type Contexts
 ###############
 
diff --git a/src/syntax/gats/exprinterop.jl b/src/syntax/gats/exprinterop.jl
index 363b6f25..f0cc4291 100644
--- a/src/syntax/gats/exprinterop.jl
+++ b/src/syntax/gats/exprinterop.jl
@@ -26,6 +26,15 @@ function toexpr(c::Context, m::MethodApp)
   Expr(:call, toexpr(c, m.head), toexpr.(Ref(c), m.args)...)
 end
 
+function toexpr(c::Context, m::AlgDot)
+  Expr(:.,  toexpr(c, m.body), QuoteNode(m.head))
+end
+
+function toexpr(c::Context, m::Eq)
+  Expr(:(==),  toexpr.(Ref(c), m.args)...)
+end
+
+
 function fromexpr(c::GATContext, e, ::Type{AlgTerm})
   @match e begin
     s::Symbol => begin
@@ -37,6 +46,11 @@ function fromexpr(c::GATContext, e, ::Type{AlgTerm})
         error("nullary constructors must be explicitly called: $e")
       end
     end
+    Expr(:., body, QuoteNode(head)) => begin 
+      t = fromexpr(c, body, AlgTerm)
+      str = AlgSort(c, t)
+      AlgTerm(AlgDot(head, t, str))
+  end
     Expr(:call, head::Symbol, argexprs...) => AlgTerm(parse_methodapp(c, head, argexprs))
     Expr(:(::), val, type) => AlgTerm(Constant(val, fromexpr(c, type, AlgType)))
     e::Expr => error("could not parse AlgTerm from $e")
@@ -54,7 +68,12 @@ function fromexpr(p::GATContext, e, ::Type{AlgType})::AlgType
     Expr(:call, head, args...) && if head != :(==) end =>
       AlgType(parse_methodapp(p, head, args))
     Expr(:call, :(==), lhs, rhs) =>
-      AlgType(fromexpr(p, lhs, AlgTerm), fromexpr(p, rhs, AlgTerm))
+      AlgType(p, fromexpr(p, lhs, AlgTerm), fromexpr(p, rhs, AlgTerm))
+    Expr(:ref, f, args...) => begin 
+      fterm = fromexpr(p, f, AlgTerm).body
+      ts = fromexpr(p, Expr(:vec, args...), TypeScope)
+      AlgType(AlgTup(headof(fterm), methodof(fterm), ts))
+    end
     _ => error("could not parse AlgType from $e")
   end
 end
@@ -156,12 +175,40 @@ function judgmenthead(theory::GAT, name, judgment::AlgAxiom)
   end
 end
 
+function judgmenthead(theory::GAT, name′, judgment::AlgFunction)
+  isnothing(name′) || error("AlgFunction received name argument $name′")
+  name = nameof(getdecl(judgment))
+  call = Expr(:call, name, nameof.(argsof(judgment))...)
+  val = toexpr(GATContext(theory, judgment.localcontext), judgment.value)
+  Expr(:(:=), call, val)
+end
+
+function toexpr(theory::GAT, judgment::AlgStruct)
+  name = nameof(getdecl(judgment))
+  ctx = GATContext(theory, judgment.localcontext)
+  callargs = [toexpr(ctx, a) for a in typeargsof(judgment)]
+  body = [toexpr(ctx, a) for a in argsof(judgment)]
+  call = Expr(:call, name, callargs...)
+  lc = [b for (i,b) in enumerate(getbindings(judgment.localcontext)) 
+        if LID(i) ∉ judgment.typeargs ∪ judgment.args] |> TypeScope
+  stexpr = Expr(:struct, false, call, Expr(:block, body...))
+  if isempty(lc) 
+    return stexpr 
+  else 
+    return Expr(:call, :⊣, stexpr, toexpr(theory, lc))
+  end
+end
+
+
+
 function toexpr(c::GAT, binding::Binding{Judgment})
   judgment = getvalue(binding)
   name = nameof(binding)
   # FIXME
   if judgment isa Alias
     return nothing
+  elseif judgment isa AlgStruct 
+    return toexpr(c, judgment)
   end
   head = judgmenthead(c, name, judgment)
   if isnothing(head)
@@ -206,7 +253,7 @@ function parse_binding_expr!(c::GATContext, pushbinding!, e)
     Expr(:(::), name, T) => p!(name, T)
     Expr(:call, :(==), lhs, rhs) =>
       pushbinding!(Binding{AlgType}(
-        nothing, AlgType(fromexpr(c, lhs, AlgTerm), fromexpr(c, rhs, AlgTerm))
+        nothing, AlgType(c, fromexpr(c, lhs, AlgTerm), fromexpr(c, rhs, AlgTerm))
       ))
     _ => error("invalid binding expression $e")
   end
@@ -223,17 +270,19 @@ end
 
 function parseargs!(theory::GAT, exprs::AbstractVector, scope::TypeScope)
   c = GATContext(theory, scope)
-  map(exprs) do expr
+  linenumber = nothing
+  Vector{LID}(filter(x->x isa LID, map(exprs) do expr
     binding_expr = @match expr begin
       a::Symbol => getlid(ident(scope; name=a))
+      l::LineNumberNode => begin linenumber = l end
       :($a :: $T) => begin
         binding = fromexpr(c, expr, Binding{AlgType})
-        Scopes.unsafe_pushbinding!(scope.scope, binding)
+        Scopes.unsafe_pushbinding!(scope.scope, setline(binding, linenumber))
         LID(length(scope))
       end
       _ => error("invalid argument expression $expr")
     end
-  end
+  end))
 end
 
 function parseaxiom!(theory::GAT, localcontext, sort_expr, e; name=nothing)
@@ -264,33 +313,24 @@ function parseconstructor!(theory::GAT, localcontext, type_expr, e)
   args = parseargs!(theory, arglist, localcontext)
   @match type_expr begin
     :TYPE => begin
-      decl = if hasname(theory, name)
-        ident(theory; name)
-      else
-        Scopes.unsafe_pushbinding!(theory, Binding{Judgment}(name, AlgDeclaration()))
-      end
+      decl = hasname!(theory, name)
       typecon = AlgTypeConstructor(decl, localcontext, args)
       X = Scopes.unsafe_pushbinding!(theory, Binding{Judgment}(nothing, typecon))
       for (i, arg) in enumerate(argsof(typecon))
         argname = nameof(arg)
-        argdecl = if hasname(theory, argname)
-          ident(theory; name=argname)
-        else
-          Scopes.unsafe_pushbinding!(theory, Binding{Judgment}(argname, AlgDeclaration()))
-        end
+        argdecl = hasname!(theory, argname)
         Scopes.unsafe_pushbinding!(theory, Binding{Judgment}(nothing, AlgAccessor(argdecl, decl, X, i)))
       end
     end
     _ => begin
       c = GATContext(theory, localcontext)
-      type = fromexpr(c, type_expr, AlgType)
-      decl = if hasname(theory, name)
-        ident(theory; name)
-      else
-        Scopes.unsafe_pushbinding!(theory, Binding{Judgment}(name, AlgDeclaration()))
-      end
+      type = @match type_expr begin 
+        Expr(:vect, _...) => fromexpr(c, type_expr, TypeScope)
+        _ => fromexpr(c, type_expr, AlgType)
+      end      
+      decl = hasname!(theory, name)
       termcon = AlgTermConstructor(decl, localcontext, args, type)
-      Scopes.unsafe_pushbinding!(theory, Binding{Judgment}(nothing, termcon))
+      m = Scopes.unsafe_pushbinding!(theory, Binding{Judgment}(nothing, termcon))
     end
   end
 end
@@ -308,6 +348,7 @@ function normalize_judgment(e)
     :(($lhs == $rhs :: $typ) ⊣ $ctx) => :((($lhs == $rhs) :: $typ) ⊣ $ctx)
     :($trmcon :: $typ ⊣ $ctx) => :(($trmcon :: $typ) ⊣ $ctx)
     :($name := $lhs == $rhs ⊣ $ctx) => :((($name := ($lhs == $rhs))) ⊣ $ctx)
+    :($name := $fun ⊣ $ctx) => :(($name := $fun) ⊣ $ctx)
     :($lhs == $rhs ⊣ $ctx) => :(($lhs == $rhs) ⊣ $ctx)
     :($(trmcon::Symbol) ⊣ $ctx) => :(($trmcon :: default) ⊣ $ctx)
     :($f($(args...)) ⊣ $ctx) && if f ∉ [:(==), :(⊣)] end => :(($f($(args...)) :: default) ⊣ $ctx)
@@ -334,12 +375,57 @@ function parse_binding_line!(theory::GAT, e, linenumber)
   end
 
   @match head begin
-    Expr(:(:=), name, equation) => parseaxiom!(theory, localcontext, type_expr, equation; name)
+    Expr(:(:=), name, equation) => @match equation begin 
+      Expr(:call, :(==), _, _) => parseaxiom!(theory, localcontext, type_expr, equation; name)
+      _ => parsefunction!(theory, localcontext, type_expr, name, equation)
+    end
     Expr(:call, :(==), _, _) => parseaxiom!(theory, localcontext, type_expr, head)
     _ => parseconstructor!(theory, localcontext, type_expr, head)
   end
 end
 
+function  parsefunction!(theory::GAT, localcontext, sort_expr, call, e)
+  isnothing(sort_expr) || error("No explicit sort for functions $call :: $sort_expr")
+  name, args′ = @match call begin
+    Expr(:call, name, args...) => (name, args)
+  end
+  args = parseargs!(theory, args′, localcontext)
+  c = GATContext(theory, localcontext)
+  decl = hasname!(theory, name)
+  trm = fromexpr(c, e, AlgTerm)
+  fun = AlgFunction(decl, localcontext, args, trm)
+  Scopes.unsafe_pushbinding!(theory, Binding{Judgment}(nothing, fun))
+end
+
+function parse_struct!(theory::GAT, e, linenumber, ctx=nothing)
+  localcontext = isnothing(ctx) ? TypeScope() : fromexpr(theory, ctx, TypeScope)
+  (name, args...) = @match e begin 
+    Expr(:struct, false, Expr(:call, name, lc...), Expr(:block, body...)) => begin
+      typeargs = parseargs!(theory, lc, localcontext)
+      args = parseargs!(theory, body, localcontext)
+      (name, localcontext, typeargs, args)
+    end
+  end
+  decl = hasname!(theory, name)
+  str = AlgStruct(decl, args...)
+  X = Scopes.unsafe_pushbinding!(theory, Binding{Judgment}(nothing, str))
+
+  for arg in typeargsof(str)
+    argname = nameof(arg)
+    i = ident(localcontext; name=argname).lid.val
+    argdecl = hasname!(theory, argname)
+    b = Binding{Judgment}(nothing, AlgAccessor(argdecl, decl, X, i))
+    Scopes.unsafe_pushbinding!(theory, b)
+  end
+  # theory.fields[X] = Dict{Symbol, LID}()
+  # for lid in str.args
+  #   n = nameof(ident(localcontext;lid))
+  #   theory.fields[X][n] = lid
+  # end
+end
+
+
+
 # GATs
 ######
 
@@ -363,6 +449,8 @@ end
 function parse_gat_line!(theory::GAT, e::Expr, linenumber; current_module)
   try
     @match e begin
+      Expr(:struct, _...) => parse_struct!(theory, e, linenumber)
+      Expr(:call, :⊣, Expr(:struct, _...), ctx) => parse_struct!(theory, e.args[2], linenumber, ctx)
       Expr(:macrocall, var"@op", _, aliasexpr) => begin
         lines = @match aliasexpr begin
           Expr(:block, lines...) => lines
@@ -374,11 +462,7 @@ function parse_gat_line!(theory::GAT, e::Expr, linenumber; current_module)
               nothing
             @case :($alias := $name)
               # check if there is already a declaration for name, if not, create declaration
-              decl = if hasname(theory, name)
-                ident(theory; name)
-              else
-                Scopes.unsafe_pushbinding!(theory, Binding{Judgment}(name, AlgDeclaration()))
-              end
+              decl = hasname!(theory, name)
               binding = Binding{Judgment}(alias, Alias(decl), linenumber)
               Scopes.unsafe_pushbinding!(theory, binding)
             @case _
diff --git a/src/syntax/gats/gat.jl b/src/syntax/gats/gat.jl
index d29c2e1a..7733ca8d 100644
--- a/src/syntax/gats/gat.jl
+++ b/src/syntax/gats/gat.jl
@@ -70,7 +70,7 @@ function Base.copy(theory::GAT; name=theory.name)
     deepcopy(theory.resolvers),
     copy(theory.sorts),
     deepcopy(theory.accessors),
-    copy(theory.axioms)
+    copy(theory.axioms),
   )
 end
 
@@ -81,7 +81,7 @@ function GAT(name::Symbol)
     Dict{Ident, MethodResolver}(),
     AlgSort[],
     Dict{Ident, Dict{Int, Ident}}(),
-    Ident[]
+    Ident[],
   )
 end
 
@@ -106,6 +106,18 @@ function unsafe_updatecache!(theory::GAT, x::Ident, judgment::AlgTypeConstructor
   theory.accessors[x] = Dict{Int, Ident}()
 end
 
+function unsafe_updatecache!(theory::GAT, x::Ident, judgment::AlgFunction)
+  addmethod!(theory.resolvers[getdecl(judgment)], sortsignature(judgment), x)
+end
+
+function unsafe_updatecache!(theory::GAT, x::Ident, judgment::AlgStruct)
+  addmethod!(theory.resolvers[getdecl(judgment)], sortsignature(judgment), x)
+  addmethod!(theory.resolvers[getdecl(judgment)], typesortsignature(judgment), x) # Collision?
+  push!(theory.sorts, AlgSort(getdecl(judgment), x))
+  theory.accessors[x] = Dict{Int, Ident}()
+end
+
+
 function unsafe_updatecache!(theory::GAT, x::Ident, judgment::AlgAccessor)
   addmethod!(theory.resolvers[getdecl(judgment)], sortsignature(judgment), x)
   theory.accessors[judgment.typecon][judgment.arg] = x
@@ -125,6 +137,7 @@ function Scopes.unsafe_pushbinding!(theory::GAT, binding::Binding{Judgment})
   x
 end
 
+
 # Pretty-printing
 
 function Base.show(io::IO, theory::GAT)
@@ -211,3 +224,27 @@ function methodlookup(c::GATContext, x::Ident, sig::AlgSorts)
     error("no method of $x found with signature $(getdecl.(sig))")
   end
 end
+
+hasname!(theory::GAT, name::Symbol) = if hasname(theory, name)
+  ident(theory; name)
+else
+  Scopes.unsafe_pushbinding!(theory, Binding{Judgment}(name, AlgDeclaration()))
+end
+
+"""Get type associated with a field of a struct"""
+function resolvefield(t::Context, method::Ident, field::Symbol)
+  str = getvalue(t[method])
+  str[ident(str; name=field)] |> getvalue
+end
+
+"""Get all structs in a theory"""
+function structs(t::GAT)
+  res = AlgStruct[]
+  for s in sorts(t)
+    v = getvalue(t[methodof(s)])
+    if v isa AlgStruct 
+      push!(res, v)
+    end
+  end
+  res
+end
diff --git a/src/syntax/gats/judgments.jl b/src/syntax/gats/judgments.jl
index 4a008cb0..3be6a766 100644
--- a/src/syntax/gats/judgments.jl
+++ b/src/syntax/gats/judgments.jl
@@ -25,6 +25,28 @@ function Base.show(io::IO, ts::TypeScope)
   print(io, toexpr(EmptyContext{AlgType}(), ts))
 end
 
+
+"""
+A type that comes from applying a term constructor (which has a tuple output)
+
+We don't always know what the inputs to that function were. E.g. 
+
+universal(p::pushout[apex::Ob, i1::b->apex, i2::c->apex], ...) 
+  ⊣ [(a,b,c):Ob, ...]
+
+However, because of the possibility of overloading, we need to know what the 
+argument sorts are in order to identify the method.
+"""
+@struct_hash_equal struct AlgTup <: AbstractAlgTup
+  head::Ident
+  method::Ident
+  body::TypeScope
+end
+  
+bodyof(t::AlgTup) = t.body
+methodof(t::AlgTup) = t.method
+headof(t::AlgTup) = t.head
+
 """
 A GAT is conceptually a bunch of `Judgment`s strung together.
 """
@@ -40,6 +62,8 @@ Base.getindex(tc::TrmTypConstructor, lid::LID) = getindex(tc.localcontext, lid)
 
 Base.getindex(tc::TrmTypConstructor, lids::AbstractVector{LID}) = getindex(tc.localcontext, lids)
 
+getdecl(tc::TrmTypConstructor) = tc.declaration
+
 """
 `AlgDeclaration`
 
@@ -65,7 +89,7 @@ end
 
 Scopes.getcontext(tc::AlgTypeConstructor) = tc.localcontext
 
-getdecl(tc::AlgTypeConstructor) = tc.declaration
+abstract type AccessorField <: Judgment end
 
 """
 `AlgAccessor`
@@ -77,18 +101,19 @@ I.e., declaring `Hom(dom::Ob, codom::Ob)::TYPE` implicitly overloads a previous
 declaration for `dom` and `codom`, or creates declarations if none previously
 exist.
 """
-@struct_hash_equal struct AlgAccessor <: Judgment
+@struct_hash_equal struct AlgAccessor <: AccessorField
   declaration::Ident
   typecondecl::Ident
   typecon::Ident
   arg::Int
 end
 
-Scopes.getcontext(acc::AlgAccessor) = EmptyContext{AlgType}()
+Scopes.getcontext(::AccessorField) = EmptyContext{AlgType}()
+
+getdecl(acc::AccessorField) = acc.declaration
 
-getdecl(acc::AlgAccessor) = acc.declaration
+sortsignature(acc::AccessorField) = [AlgSort(acc.typecondecl, acc.typecon)]
 
-sortsignature(acc::AlgAccessor) = [AlgSort(acc.typecondecl, acc.typecon)]
 
 """
 `AlgTermConstructor`
@@ -99,14 +124,12 @@ A declaration of a term constructor as a method of an `AlgFunction`.
   declaration::Ident
   localcontext::TypeScope
   args::Vector{LID}
-  type::AlgType
+  type::Union{TypeScope,AlgType}
 end
 
 Scopes.getcontext(tc::AlgTermConstructor) = tc.localcontext
 
-getdecl(tc::AlgTermConstructor) = tc.declaration
-
-sortsignature(tc::Union{AlgTypeConstructor, AlgTermConstructor}) =
+sortsignature(tc::TrmTypConstructor) =
   AlgSort.(getvalue.(argsof(tc)))
 
 """
@@ -129,3 +152,62 @@ A description of the argument sorts for a term constructor, used to disambiguate
 multiple term constructors of the same name.
 """
 const AlgSorts = Vector{AlgSort}
+
+"""
+`AlgStruct`
+
+A declaration which is sugar for an AlgTypeConstructor, an AlgTermConstructor 
+which constructs an element of that type, and projection term constructors. E.g.
+
+    struct Cospan(dom, codom) ⊣ [dom:Ob, codom::Ob]
+      apex::Ob
+      i1::dom->apex
+      i2::codom->apex
+    end
+
+Is sugar for:
+
+    Cospan(dom, codom, apex, i1, i2)::TYPE 
+      ⊣ [(dom, codom, apex)::Ob, i1::dom->apex, i2::codom->apex]
+
+    Cospan(apex, i1, i2)::Cospan(dom, codom, apex, i1, i2) 
+      ⊣ [(dom, codom, apex)::Ob, i1::dom->apex, i2::codom->apex]
+
+    apex(csp::Cospan(d, c, a, i_1, i_2))::Ob             ⊣ [(d,c,a)::Ob, ...]
+    i1(csp  ::Cospan(d, c, a, i_1, i_2))::(d->apex(csp)) ⊣ [(d,c,a)::Ob, ...]
+    i2(csp  ::Cospan(d, c, a, i_1, i_2))::(c->apex(csp)) ⊣ [(d,c,a)::Ob, ...]
+
+    apex(Cospan(a,i_1,i_2)) == a ⊣ [a::Ob,...]
+    i1(Cospan(a,i_1,i_2)) == i_1 ⊣ [a::Ob,...]
+    i2(Cospan(a,i_1,i_2)) == i_2 ⊣ [a::Ob,...]
+
+    c == Cospan(apex(c), i1(c), i2(c)) ⊣ [..., c::Cospan(...)]
+
+"""
+@struct_hash_equal struct AlgStruct <: TrmTypConstructor
+  declaration::Ident
+  localcontext::TypeScope
+  typeargs::Vector{LID}
+  args::Vector{LID}
+end
+
+Base.nameof(t::AlgStruct) = nameof(t.declaration)
+typeargsof(t::AlgStruct) = t[t.typeargs]
+typesortsignature(tc::AlgStruct) =
+  AlgSort.(getvalue.(typeargsof(tc)))
+
+Scopes.getcontext(tc::AlgStruct) = tc.localcontext
+
+"""
+A shorthand for a function, such as "square(x) := x * x".  It is relevant for 
+models but can be ignored by theory maps, as it is fully determined by other 
+judgments in the theory.
+"""
+@struct_hash_equal struct AlgFunction <: TrmTypConstructor
+  declaration::Ident
+  localcontext::TypeScope
+  args::Vector{LID}
+  value::AlgTerm
+end
+
+Scopes.getcontext(tc::AlgFunction) = tc.localcontext
diff --git a/test/Project.toml b/test/Project.toml
index abf3794d..b7561128 100644
--- a/test/Project.toml
+++ b/test/Project.toml
@@ -1,4 +1,5 @@
 [deps]
+DataStructures = "864edb3b-99cc-5e75-8d2d-829cb0a9cfe8"
 GATlab = "f0ffcf3b-d13a-433e-917c-cc44ccf5ead2"
 StructEquality = "6ec83bb0-ed9f-11e9-3b4c-2b04cb4e219c"
 Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"
diff --git a/test/nonstdlib/Pushouts.jl b/test/nonstdlib/Pushouts.jl
new file mode 100644
index 00000000..a9566c72
--- /dev/null
+++ b/test/nonstdlib/Pushouts.jl
@@ -0,0 +1,28 @@
+
+using Test
+using GATlab
+using GATlab.NonStdlib
+
+using .ThPushout
+
+"""
+Pushout Input                       Output
+   1  <--- a ---> x                   12x
+   2  <--- b ---↗                     3y
+   3  <--- c ---> y                   4
+   4              z                   z
+
+Universal input:                    Output
+  1 --↘ d                          12x -> c 
+  2 --> c <-- x                     3y -> b
+  3 --> b <-- y                      4 -> b
+  4 --↗ a <-- z                      z -> a
+"""
+
+@withmodel FinSetC() (pushout, universal, cospan, ι₁) begin
+  res = pushout(Span(3, [1,2,3], [1,1,2]); context=(d=4, c=3))
+  @test res == PushoutInt(4, [1,1,2,3],[1,2,4])
+  @test cospan(res) == Cospan(4, [1,1,2,3], [1,2,4])
+  @test ι₁(res) == [1,1,2,3]
+  @test universal(res, Cospan(4, [3,3,2,2],[3,2,1])) == [3,2,2,1]
+end
diff --git a/test/nonstdlib/tests.jl b/test/nonstdlib/tests.jl
new file mode 100644
index 00000000..73f34d72
--- /dev/null
+++ b/test/nonstdlib/tests.jl
@@ -0,0 +1,5 @@
+module TestNonStdModels
+
+include("Pushouts.jl")
+
+end
diff --git a/test/runtests.jl b/test/runtests.jl
index f8db642b..da2cd870 100644
--- a/test/runtests.jl
+++ b/test/runtests.jl
@@ -15,3 +15,8 @@ end
 @testset "stdlib" begin
   include("stdlib/tests.jl")
 end
+
+@testset "nonstdlib" begin
+  include("nonstdlib/tests.jl")
+end
+
diff --git a/test/stdlib/models/Arithmetic.jl b/test/stdlib/Arithmetic.jl
similarity index 100%
rename from test/stdlib/models/Arithmetic.jl
rename to test/stdlib/Arithmetic.jl
diff --git a/test/stdlib/models/FinMatrices.jl b/test/stdlib/FinMatrices.jl
similarity index 100%
rename from test/stdlib/models/FinMatrices.jl
rename to test/stdlib/FinMatrices.jl
diff --git a/test/stdlib/models/FinSets.jl b/test/stdlib/FinSets.jl
similarity index 100%
rename from test/stdlib/models/FinSets.jl
rename to test/stdlib/FinSets.jl
diff --git a/test/stdlib/models/GATs.jl b/test/stdlib/GATs.jl
similarity index 100%
rename from test/stdlib/models/GATs.jl
rename to test/stdlib/GATs.jl
diff --git a/test/stdlib/models/Nothings.jl b/test/stdlib/Nothings.jl
similarity index 100%
rename from test/stdlib/models/Nothings.jl
rename to test/stdlib/Nothings.jl
diff --git a/test/stdlib/models/Op.jl b/test/stdlib/Op.jl
similarity index 100%
rename from test/stdlib/models/Op.jl
rename to test/stdlib/Op.jl
diff --git a/test/stdlib/models/SliceCategories.jl b/test/stdlib/SliceCategories.jl
similarity index 100%
rename from test/stdlib/models/SliceCategories.jl
rename to test/stdlib/SliceCategories.jl
diff --git a/test/stdlib/models/tests.jl b/test/stdlib/models/tests.jl
deleted file mode 100644
index 7893f362..00000000
--- a/test/stdlib/models/tests.jl
+++ /dev/null
@@ -1,11 +0,0 @@
-module TestStdModels
-
-include("FinSets.jl")
-include("Arithmetic.jl")
-include("FinMatrices.jl")
-include("SliceCategories.jl")
-include("Op.jl")
-include("Nothings.jl")
-include("GATs.jl")
-
-end
diff --git a/test/stdlib/tests.jl b/test/stdlib/tests.jl
index 367c527a..7893f362 100644
--- a/test/stdlib/tests.jl
+++ b/test/stdlib/tests.jl
@@ -1,5 +1,11 @@
-module TestTheories 
+module TestStdModels
 
-include("models/tests.jl")
+include("FinSets.jl")
+include("Arithmetic.jl")
+include("FinMatrices.jl")
+include("SliceCategories.jl")
+include("Op.jl")
+include("Nothings.jl")
+include("GATs.jl")
 
-end # module
+end
diff --git a/test/syntax/GATs.jl b/test/syntax/GATs.jl
index 8a37dfc9..3ab8bcc1 100644
--- a/test/syntax/GATs.jl
+++ b/test/syntax/GATs.jl
@@ -2,6 +2,7 @@ module TestGATs
 
 using GATlab, Test
 
+
 # GAT ASTs
 ##########
 
@@ -113,13 +114,21 @@ TG = ThGraph.Meta.theory
 #-------
 toexpr.(Ref(T), T.segments)
 
-# InCtx
-#----------
-# tic = fromexpr(T, :(compose(f,compose(id(b),id(b))) ⊣ [a::Ob, b::Ob, f::Hom(a,b)]), TermInCtx);
-# tic2 = fromexpr(T,toexpr(T, tic), TermInCtx) # same modulo scope tags
+# @theory
+#########
+@theory ThI2 <: ThCategory begin
+  square(x) := f⋅f ⊣ [x::Ob, f::Hom(x,x)]
+end
+
+@theory ThSpan <: ThCategory begin
+  struct Span(dom::Ob, codom::Ob)
+    apex::Ob
+    left::Hom(apex, dom)
+    right::Hom(apex, codom)
+  end
+  id_span(x) := Span(x, id(x),id(x)) ⊣ [x::Ob]
+end
 
 
-# typic = fromexpr(T, :(Hom(a,b) ⊣ [a::Ob, b::Ob, f::Hom(a,b)]), TypeInCtx)
-# typic2 = fromexpr(T,toexpr(T, typic), TypeInCtx) # same modulo scope tags
 
 end # module

From d8a525fce77c8263e71a96e014a1b0c284ce8cfe Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Fri, 20 Oct 2023 10:48:34 -0700
Subject: [PATCH 04/13] remove residual algtup code

---
 src/syntax/gats/ast.jl         |  3 +--
 src/syntax/gats/exprinterop.jl |  5 -----
 src/syntax/gats/judgments.jl   | 21 ---------------------
 3 files changed, 1 insertion(+), 28 deletions(-)

diff --git a/src/syntax/gats/ast.jl b/src/syntax/gats/ast.jl
index 18c91662..8ffe6311 100644
--- a/src/syntax/gats/ast.jl
+++ b/src/syntax/gats/ast.jl
@@ -84,7 +84,6 @@ rename(tag::ScopeTag, reps::Dict{Symbol,Symbol}, t::AlgTerm) =
 retag(reps::Dict{ScopeTag, ScopeTag}, t::AlgTerm) = AlgTerm(retag(reps, t.body))
 
 abstract type AbstractEq end # needs to be defined after AlgSort
-abstract type AbstractAlgTup end # needs to be defined after TypeScope
 
 """
 `AlgType`
@@ -92,7 +91,7 @@ abstract type AbstractAlgTup end # needs to be defined after TypeScope
 One syntax tree to rule all the types.
 """
 @struct_hash_equal struct AlgType <: AlgAST
-  body::Union{MethodApp{AlgTerm}, AbstractEq, AbstractAlgTup}
+  body::Union{MethodApp{AlgTerm}, AbstractEq}
 end
 
 function AlgType(fun::Ident, method::Ident)
diff --git a/src/syntax/gats/exprinterop.jl b/src/syntax/gats/exprinterop.jl
index f0cc4291..682c5da6 100644
--- a/src/syntax/gats/exprinterop.jl
+++ b/src/syntax/gats/exprinterop.jl
@@ -69,11 +69,6 @@ function fromexpr(p::GATContext, e, ::Type{AlgType})::AlgType
       AlgType(parse_methodapp(p, head, args))
     Expr(:call, :(==), lhs, rhs) =>
       AlgType(p, fromexpr(p, lhs, AlgTerm), fromexpr(p, rhs, AlgTerm))
-    Expr(:ref, f, args...) => begin 
-      fterm = fromexpr(p, f, AlgTerm).body
-      ts = fromexpr(p, Expr(:vec, args...), TypeScope)
-      AlgType(AlgTup(headof(fterm), methodof(fterm), ts))
-    end
     _ => error("could not parse AlgType from $e")
   end
 end
diff --git a/src/syntax/gats/judgments.jl b/src/syntax/gats/judgments.jl
index 3be6a766..bfce7f2d 100644
--- a/src/syntax/gats/judgments.jl
+++ b/src/syntax/gats/judgments.jl
@@ -26,27 +26,6 @@ function Base.show(io::IO, ts::TypeScope)
 end
 
 
-"""
-A type that comes from applying a term constructor (which has a tuple output)
-
-We don't always know what the inputs to that function were. E.g. 
-
-universal(p::pushout[apex::Ob, i1::b->apex, i2::c->apex], ...) 
-  ⊣ [(a,b,c):Ob, ...]
-
-However, because of the possibility of overloading, we need to know what the 
-argument sorts are in order to identify the method.
-"""
-@struct_hash_equal struct AlgTup <: AbstractAlgTup
-  head::Ident
-  method::Ident
-  body::TypeScope
-end
-  
-bodyof(t::AlgTup) = t.body
-methodof(t::AlgTup) = t.method
-headof(t::AlgTup) = t.head
-
 """
 A GAT is conceptually a bunch of `Judgment`s strung together.
 """

From 9a7b7419baf44f0c352758a9babc637e35c1f6b6 Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Thu, 26 Oct 2023 13:09:53 -0700
Subject: [PATCH 05/13] better coverage

---
 src/syntax/gats/algorithms.jl  |  8 ++++++--
 src/syntax/gats/exprinterop.jl |  2 --
 test/nonstdlib/Pushouts.jl     |  4 ++++
 test/syntax/GATs.jl            | 13 ++++++++++++-
 4 files changed, 22 insertions(+), 5 deletions(-)

diff --git a/src/syntax/gats/algorithms.jl b/src/syntax/gats/algorithms.jl
index 51a1f378..640ddb37 100644
--- a/src/syntax/gats/algorithms.jl
+++ b/src/syntax/gats/algorithms.jl
@@ -15,6 +15,8 @@ function sortcheck(ctx::Context, t::AlgTerm)::AlgSort
       argsorts = sortcheck.(Ref(ctx), t.body.args)
       argsorts == sortsignature(judgment) || error("Sorts don't match")
       AlgSort(judgment.type)
+    elseif judgment isa AlgStruct
+      AlgSort(headof(bodyof(t)), methodof(bodyof(t)))
     else
       error("Unexpected app $t") 
     end
@@ -23,8 +25,10 @@ function sortcheck(ctx::Context, t::AlgTerm)::AlgSort
     AlgSort(type)
   elseif isdot(t)
     AlgSort(ctx, t)
-  else
+  elseif isconstant(t)
     AlgSort(t.body.type)
+  else
+    error("Make this branch explicit if it's ever used $t")
   end
 end
 
@@ -192,7 +196,7 @@ function substitute_funs(ctx::Context, t::AlgTerm)
   b = bodyof(t)
   if isapp(t)
     m = getvalue(ctx[methodof(b)])
-    if m isa AlgTermConstructor
+    if m isa AlgTermConstructor || m isa AlgStruct
       args = substitute_funs.(Ref(ctx), argsof(b))
       AlgTerm(MethodApp{AlgTerm}(headof(b), methodof(b), args))
     elseif m isa AlgFunction 
diff --git a/src/syntax/gats/exprinterop.jl b/src/syntax/gats/exprinterop.jl
index 682c5da6..196abc75 100644
--- a/src/syntax/gats/exprinterop.jl
+++ b/src/syntax/gats/exprinterop.jl
@@ -125,8 +125,6 @@ function toexpr(p::Context, b::Binding{AlgType})
     Expr(:(::), nameof(b), toexpr(p, val))
   elseif iseq(val)
     Expr(:call, :(==), toexpr.(Ref(p), val.body.equands)...)
-  elseif val isa Alias
-    Expr(:(=), nameof(b), toexpr(Ref(p), name.ref))
   end
 end
 
diff --git a/test/nonstdlib/Pushouts.jl b/test/nonstdlib/Pushouts.jl
index a9566c72..17f0bf5b 100644
--- a/test/nonstdlib/Pushouts.jl
+++ b/test/nonstdlib/Pushouts.jl
@@ -5,6 +5,10 @@ using GATlab.NonStdlib
 
 using .ThPushout
 
+T = ThPushout.Meta.theory
+@test all(e -> e isa Expr, toexpr.(Ref(T), T.segments))
+
+
 """
 Pushout Input                       Output
    1  <--- a ---> x                   12x
diff --git a/test/syntax/GATs.jl b/test/syntax/GATs.jl
index 3ab8bcc1..60dda27a 100644
--- a/test/syntax/GATs.jl
+++ b/test/syntax/GATs.jl
@@ -45,11 +45,18 @@ seg_expr = quote
     a::Ob, b::Ob, c::Ob, d::Ob,
     f::Hom(a, b), g::Hom(b, c), h::Hom(c, d)
   ]
+  struct Span(dom::Ob, codom::Ob)
+    apex::Ob
+    left::Hom(apex, dom)
+    right::Hom(apex, codom)
+  end
+  id_span(x) := Span(x, id(x),id(x)) ⊣ [x::Ob]
 end
 
+
 thcat = fromexpr(GAT(:ThCat), seg_expr, GAT; current_module=[:Foo, :Bar])
 
-O, H, i, cmp = idents(thcat; name=[:Ob, :Hom, :id, :compose])
+O, H, i = idents(thcat; name=[:Ob, :Hom, :id])
 
 ob_decl = getvalue(thcat[O])
 
@@ -57,6 +64,7 @@ ObT = fromexpr(thcat, :Ob, AlgType)
 ObS = AlgSort(ObT)
 @test toexpr(GATContext(thcat), ObS) == :Ob
 
+
 # Extend seg with a context of (A: Ob)
 sortscope = TypeScope(:A => ObT)
 
@@ -79,6 +87,9 @@ HomS = AlgSort(HomT)
 
 @test sortcheck(c, AlgTerm(A)) == ObS
 
+x = fromexpr(c, :(id_span(A)), AlgTerm)
+@test sortcheck(c, x) isa AlgSort
+
 # # Good term and bad term
 ida = fromexpr(c, :(id(A)), AlgTerm)
 

From db5c7b6d5df89f480413005a65f4d92a0b5e09ba Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Thu, 26 Oct 2023 13:41:32 -0700
Subject: [PATCH 06/13] remove else branches

---
 src/syntax/gats/algorithms.jl | 8 --------
 test/syntax/GATs.jl           | 2 ++
 2 files changed, 2 insertions(+), 8 deletions(-)

diff --git a/src/syntax/gats/algorithms.jl b/src/syntax/gats/algorithms.jl
index 640ddb37..fbd626a6 100644
--- a/src/syntax/gats/algorithms.jl
+++ b/src/syntax/gats/algorithms.jl
@@ -17,8 +17,6 @@ function sortcheck(ctx::Context, t::AlgTerm)::AlgSort
       AlgSort(judgment.type)
     elseif judgment isa AlgStruct
       AlgSort(headof(bodyof(t)), methodof(bodyof(t)))
-    else
-      error("Unexpected app $t") 
     end
   elseif isvariable(t)
     type = ctx[t.body] |> getvalue
@@ -27,8 +25,6 @@ function sortcheck(ctx::Context, t::AlgTerm)::AlgSort
     AlgSort(ctx, t)
   elseif isconstant(t)
     AlgSort(t.body.type)
-  else
-    error("Make this branch explicit if it's ever used $t")
   end
 end
 
@@ -202,14 +198,10 @@ function substitute_funs(ctx::Context, t::AlgTerm)
     elseif m isa AlgFunction 
       subst = Dict(zip(idents(m.localcontext; lid=m.args), argsof(b)))
       substitute_term(m.value, subst)
-    else 
-      error("Bad app $m")
     end
   elseif isvariable(t) || isconstant(t)
     t 
   elseif isdot(t)
     AlgTerm(AlgDot(headof(b), substitute_funs(ctx, bodyof(b)), b.sort))
-  else 
-    error("Bad term $t")
   end
 end
\ No newline at end of file
diff --git a/test/syntax/GATs.jl b/test/syntax/GATs.jl
index 60dda27a..fe34251d 100644
--- a/test/syntax/GATs.jl
+++ b/test/syntax/GATs.jl
@@ -24,6 +24,8 @@ three = AlgTerm(plus, plusmethod, [one, two])
 
 @test fromexpr(GAT(:Empty), two.body, AlgTerm) == two
 
+@test GATs.substitute_funs(scope, one) == one
+
 @test basicprinted(two) == "AlgTerm(2::number)"
 
 @test_throws Exception AlgSort(scope, three)

From b7c90ae4a4ef4f6e215a03b8cad508f78070dff8 Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Thu, 26 Oct 2023 14:01:04 -0700
Subject: [PATCH 07/13] remove vestigal code

---
 src/syntax/gats/exprinterop.jl | 21 ++-------------------
 test/nonstdlib/Pushouts.jl     |  1 -
 2 files changed, 2 insertions(+), 20 deletions(-)

diff --git a/src/syntax/gats/exprinterop.jl b/src/syntax/gats/exprinterop.jl
index 196abc75..e59932ac 100644
--- a/src/syntax/gats/exprinterop.jl
+++ b/src/syntax/gats/exprinterop.jl
@@ -15,13 +15,6 @@ function parse_methodapp(c::GATContext, head::Symbol, argexprs)
   MethodApp{AlgTerm}(fun, method, args)
 end
 
-function fromexpr(c::GATContext, e, ::Type{MethodApp{AlgTerm}})
-  @match e begin
-    Expr(:call, head::Symbol, argexprs...) => parse_methodapp(c, head, argexprs)
-    _ => error("expected a call expression")
-  end
-end
-
 function toexpr(c::Context, m::MethodApp)
   Expr(:call, toexpr(c, m.head), toexpr.(Ref(c), m.args)...)
 end
@@ -30,11 +23,6 @@ function toexpr(c::Context, m::AlgDot)
   Expr(:.,  toexpr(c, m.body), QuoteNode(m.head))
 end
 
-function toexpr(c::Context, m::Eq)
-  Expr(:(==),  toexpr.(Ref(c), m.args)...)
-end
-
-
 function fromexpr(c::GATContext, e, ::Type{AlgTerm})
   @match e begin
     s::Symbol => begin
@@ -80,7 +68,7 @@ function toexpr(c::Context, type::AlgType)
     else
       Expr(:call, toexpr(c, type.body.head), toexpr.(Ref(c), type.body.args)...)
     end
-  else
+  elseif iseq(type)
     Expr(:call, :(==), toexpr.(Ref(c), type.body.equands)...)
   end
 end
@@ -120,12 +108,7 @@ end
 ###########
 
 function toexpr(p::Context, b::Binding{AlgType})
-  val = getvalue(b)
-  if isapp(val)
-    Expr(:(::), nameof(b), toexpr(p, val))
-  elseif iseq(val)
-    Expr(:call, :(==), toexpr.(Ref(p), val.body.equands)...)
-  end
+  Expr(:(::), nameof(b), toexpr(p, getvalue(b)))
 end
 
 function bindingexprs(c::Context, s::HasScope)
diff --git a/test/nonstdlib/Pushouts.jl b/test/nonstdlib/Pushouts.jl
index 17f0bf5b..76597ef5 100644
--- a/test/nonstdlib/Pushouts.jl
+++ b/test/nonstdlib/Pushouts.jl
@@ -8,7 +8,6 @@ using .ThPushout
 T = ThPushout.Meta.theory
 @test all(e -> e isa Expr, toexpr.(Ref(T), T.segments))
 
-
 """
 Pushout Input                       Output
    1  <--- a ---> x                   12x

From 0679e900519cc8a9ada07d3ec657cdd57896fa29 Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Wed, 1 Nov 2023 16:12:49 -0700
Subject: [PATCH 08/13] two kinds of AlgSort

---
 src/models/ModelInterface.jl  |   4 +-
 src/syntax/GATs.jl            |   2 +-
 src/syntax/gats/algorithms.jl |   2 +-
 src/syntax/gats/ast.jl        | 137 +++++++++++++++++-----------------
 src/syntax/gats/judgments.jl  |  27 ++++---
 5 files changed, 87 insertions(+), 85 deletions(-)

diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl
index 088921dd..c9455621 100644
--- a/src/models/ModelInterface.jl
+++ b/src/models/ModelInterface.jl
@@ -273,7 +273,7 @@ function parse_instance_body(expr::Expr, theory::GAT)
   return (funs, ext_funs)
 end
 
-function args_from_sorts(sorts::Vector{AlgSort}, jltype_by_sort::Dict{AlgSort})
+function args_from_sorts(sorts::AlgSorts, jltype_by_sort::Dict{AlgSort})
   Expr0[Expr(:(::), gensym(), jltype_by_sort[s]) for s in sorts]
 end
 
@@ -314,7 +314,7 @@ function julia_signature(
   args = if oldinstance && isempty(sortsig)
     Expr0[Expr(:curly, :Type, jltype_by_sort[AlgSort(termcon.type)])]
   else
-    Expr0[jltype_by_sort[sort] for sort in sortsig if !sort.eq]
+    Expr0[jltype_by_sort[sort] for sort in sortsig if !GATs.iseq(sort)]
   end
   JuliaFunctionSig(
     nameof(getdecl(termcon)),
diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl
index 629192c0..c7db9c82 100644
--- a/src/syntax/GATs.jl
+++ b/src/syntax/GATs.jl
@@ -1,7 +1,7 @@
 module GATs
 export Constant, AlgTerm, AlgType, AlgAST,
   TypeScope, TypeCtx, AlgSort, AlgSorts,
-  AlgDeclaration, AlgTermConstructor, 
+  AlgDeclaration, AlgTermConstructor, AbstractAlgSort,
   AlgTypeConstructor, AlgAccessor, AlgAxiom, AlgStruct, AlgDot, AlgFunction,
   typesortsignature, sortsignature, getdecl,
   GATSegment, GAT, GATContext, gettheory, gettypecontext, allmethods, 
diff --git a/src/syntax/gats/algorithms.jl b/src/syntax/gats/algorithms.jl
index fbd626a6..839d8e25 100644
--- a/src/syntax/gats/algorithms.jl
+++ b/src/syntax/gats/algorithms.jl
@@ -4,7 +4,7 @@
 Throw an error if a the head of an AlgTerm (which refers to a term constructor)
 has arguments of the wrong sort. Returns the sort of the term.
 """
-function sortcheck(ctx::Context, t::AlgTerm)::AlgSort
+function sortcheck(ctx::Context, t::AlgTerm)::AbstractAlgSort
   t_sub = substitute_funs(ctx, t)
   if t_sub != t 
     return sortcheck(ctx, t_sub)
diff --git a/src/syntax/gats/ast.jl b/src/syntax/gats/ast.jl
index 8ffe6311..bba011a2 100644
--- a/src/syntax/gats/ast.jl
+++ b/src/syntax/gats/ast.jl
@@ -1,6 +1,35 @@
 # GAT ASTs
 ##########
 
+
+# AlgSorts
+#---------
+abstract type AbstractAlgSort end
+
+"""
+`AlgSort`
+
+A *sort*, which is essentially a type constructor without arguments
+"""
+@struct_hash_equal struct AlgSort <: AbstractAlgSort
+  head::Ident
+  method::Ident
+end
+
+@struct_hash_equal struct AlgEqSort <: AbstractAlgSort
+  head::Ident
+  method::Ident
+end
+
+iseq(::AlgEqSort) = true
+iseq(::AlgSort) = false
+headof(a::AbstractAlgSort) = a.head
+methodof(a::AbstractAlgSort) = a.method
+
+Base.nameof(sort::AbstractAlgSort) = nameof(sort.head)
+
+getdecl(s::AbstractAlgSort) = s.head
+
 """
 We need this to resolve a mutual reference loop; the only subtype is Constant
 """
@@ -83,7 +112,39 @@ rename(tag::ScopeTag, reps::Dict{Symbol,Symbol}, t::AlgTerm) =
 
 retag(reps::Dict{ScopeTag, ScopeTag}, t::AlgTerm) = AlgTerm(retag(reps, t.body))
 
-abstract type AbstractEq end # needs to be defined after AlgSort
+function AlgSort(c::Context, t::AlgTerm)
+  t_sub = substitute_funs(c, t)
+  if t_sub != t 
+    return AlgSort(c, t_sub)
+  end
+  if isconstant(t)
+    AlgSort(t.body.type)
+  elseif isapp(t)
+    binding = c[t.body.method]
+    value = getvalue(binding)
+    AlgSort(value.type)
+  elseif isdot(t)
+    AlgSort(resolvefield(c, t.body.sort.method, t.body.head))
+  else # variable
+    binding = c[t.body]
+    AlgSort(getvalue(binding))
+  end
+end
+
+"""
+`Eq`
+
+The type of equality judgments.
+"""
+@struct_hash_equal struct Eq
+  equands::Tuple{AlgTerm, AlgTerm}
+  sort::AlgSort
+end
+
+retag(reps::Dict{ScopeTag, ScopeTag}, eq::Eq) = Eq(retag.(Ref(reps), eq.equands))
+
+rename(tag::ScopeTag, reps::Dict{Symbol, Symbol}, eq::Eq) =
+  Eq(retag.(Ref(tag), Ref(reps), eq.equands))
 
 """
 `AlgType`
@@ -91,7 +152,7 @@ abstract type AbstractEq end # needs to be defined after AlgSort
 One syntax tree to rule all the types.
 """
 @struct_hash_equal struct AlgType <: AlgAST
-  body::Union{MethodApp{AlgTerm}, AbstractEq}
+  body::Union{MethodApp{AlgTerm}, Eq}
 end
 
 function AlgType(fun::Ident, method::Ident)
@@ -120,6 +181,13 @@ retag(reps::Dict{ScopeTag,ScopeTag}, t::AlgType) =
 rename(tag::ScopeTag, reps::Dict{Symbol, Symbol}, t::AlgType) =
   AlgType(rename(tag, reps, t.body))
 
+AlgSort(t::AlgType) = if iseq(t)
+  AlgEqSort(t.body.sort.head, t.body.sort.method)
+else 
+  AlgSort(t.body.head, t.body.method)
+end
+  
+
 """
 Common methods for AlgType and AlgTerm
 """
@@ -140,71 +208,6 @@ A Julia value in an algebraic context. Type checked elsewhere.
 end
 
 
-# AlgSorts
-##########
-
-"""
-`AlgSort`
-
-A *sort*, which is essentially a type constructor without arguments
-"""
-@struct_hash_equal struct AlgSort
-  head::Ident
-  method::Ident
-  eq::Bool
-  AlgSort(h::Ident,m::Ident,eq::Bool=false) = new(h,m,eq)
-end
-
-AlgSort(t::AlgType) = if iseq(t)
-  AlgSort(t.body.sort.head, t.body.sort.method, true)
-else 
-  AlgSort(t.body.head, t.body.method)
-end
-
-iseq(s::AlgSort) = s.eq
-headof(a::AlgSort) = a.head
-methodof(a::AlgSort) = a.method
-
-function AlgSort(c::Context, t::AlgTerm)
-  t_sub = substitute_funs(c, t)
-  if t_sub != t 
-    return AlgSort(c, t_sub)
-  end
-  if isconstant(t)
-    AlgSort(t.body.type)
-  elseif isapp(t)
-    binding = c[t.body.method]
-    value = getvalue(binding)
-    AlgSort(value.type)
-  elseif isdot(t)
-    AlgSort(resolvefield(c, t.body.sort.method, t.body.head))
-  else # variable
-    binding = c[t.body]
-    AlgSort(getvalue(binding))
-  end
-end
-
-Base.nameof(sort::AlgSort) = nameof(sort.head)
-
-getdecl(s::AlgSort) = s.head
-
-
-"""
-`Eq`
-
-The type of equality judgments.
-"""
-@struct_hash_equal struct Eq <: AbstractEq
-  equands::Tuple{AlgTerm, AlgTerm}
-  sort::AlgSort
-end
-
-retag(reps::Dict{ScopeTag, ScopeTag}, eq::Eq) = Eq(retag.(Ref(reps), eq.equands))
-
-rename(tag::ScopeTag, reps::Dict{Symbol, Symbol}, eq::Eq) =
-  Eq(retag.(Ref(tag), Ref(reps), eq.equands))
-
-
 """
 Accessing a name from a term of tuple type
 """
diff --git a/src/syntax/gats/judgments.jl b/src/syntax/gats/judgments.jl
index bfce7f2d..b583e015 100644
--- a/src/syntax/gats/judgments.jl
+++ b/src/syntax/gats/judgments.jl
@@ -130,7 +130,7 @@ Scopes.getcontext(t::AlgAxiom) = t.localcontext
 A description of the argument sorts for a term constructor, used to disambiguate
 multiple term constructors of the same name.
 """
-const AlgSorts = Vector{AlgSort}
+const AlgSorts = Vector{<:AbstractAlgSort}
 
 """
 `AlgStruct`
@@ -144,24 +144,23 @@ which constructs an element of that type, and projection term constructors. E.g.
       i2::codom->apex
     end
 
-Is sugar for:
+Is tantamount to (in a vanilla GAT):
 
-    Cospan(dom, codom, apex, i1, i2)::TYPE 
-      ⊣ [(dom, codom, apex)::Ob, i1::dom->apex, i2::codom->apex]
+    Cospan(dom::Ob, codom::Ob)::TYPE 
 
-    Cospan(apex, i1, i2)::Cospan(dom, codom, apex, i1, i2) 
+    cospan(apex, i1, i2)::Cospan(dom, codom) 
       ⊣ [(dom, codom, apex)::Ob, i1::dom->apex, i2::codom->apex]
 
-    apex(csp::Cospan(d, c, a, i_1, i_2))::Ob             ⊣ [(d,c,a)::Ob, ...]
-    i1(csp  ::Cospan(d, c, a, i_1, i_2))::(d->apex(csp)) ⊣ [(d,c,a)::Ob, ...]
-    i2(csp  ::Cospan(d, c, a, i_1, i_2))::(c->apex(csp)) ⊣ [(d,c,a)::Ob, ...]
-
-    apex(Cospan(a,i_1,i_2)) == a ⊣ [a::Ob,...]
-    i1(Cospan(a,i_1,i_2)) == i_1 ⊣ [a::Ob,...]
-    i2(Cospan(a,i_1,i_2)) == i_2 ⊣ [a::Ob,...]
-
-    c == Cospan(apex(c), i1(c), i2(c)) ⊣ [..., c::Cospan(...)]
+    apex(csp::Cospan(d::Ob, c::Ob))::Ob            
+    i1(csp::Cospan(d::Ob, c::Ob))::(d->apex(csp))
+    i2(csp::Cospan(d::Ob, c::Ob))::(c->apex(csp))
 
+    apex(cospan(a, i_1, i_2)) == a  
+      ⊣ [(dom, codom, apex)::Ob, i_1::dom->apex, i_2::codom->apex]
+    i1(cospan(a, i_1, i_2)) == i_1 
+      ⊣ [(dom, codom, apex)::Ob, i_1::dom->apex, i_2::codom->apex]
+    i2(cospan(a, i_1, i_2)) == i_2
+      ⊣ [(dom, codom, apex)::Ob, i_1::dom->apex, i_2::codom->apex]
 """
 @struct_hash_equal struct AlgStruct <: TrmTypConstructor
   declaration::Ident

From 75f9e18a43e1692a705f32eb1db35112b3ac7bc3 Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Wed, 1 Nov 2023 16:58:56 -0700
Subject: [PATCH 09/13] struct.args -> struct.fields

---
 src/syntax/TheoryInterface.jl  | 4 ++--
 src/syntax/gats/exprinterop.jl | 9 ++-------
 src/syntax/gats/gat.jl         | 2 +-
 src/syntax/gats/judgments.jl   | 3 ++-
 4 files changed, 7 insertions(+), 11 deletions(-)

diff --git a/src/syntax/TheoryInterface.jl b/src/syntax/TheoryInterface.jl
index 48d24685..628abe3d 100644
--- a/src/syntax/TheoryInterface.jl
+++ b/src/syntax/TheoryInterface.jl
@@ -170,8 +170,8 @@ end
 
 """
 function mk_struct(s::AlgStruct, mod)
-  fields = map(s.args) do i
-    Expr(:(::), nameof(s[i]), nameof(AlgSort(getvalue(s[i]))))
+  fields = map(argsof(s)) do b
+    Expr(:(::), nameof(b), nameof(AlgSort(getvalue(b))))
   end 
   sorts = unique([f.args[2] for f in fields])
   she = Expr(:macrocall, GlobalRef(StructEquality, Symbol("@struct_hash_equal")), mod, nameof(s))
diff --git a/src/syntax/gats/exprinterop.jl b/src/syntax/gats/exprinterop.jl
index e59932ac..5ec2bc0d 100644
--- a/src/syntax/gats/exprinterop.jl
+++ b/src/syntax/gats/exprinterop.jl
@@ -166,7 +166,7 @@ function toexpr(theory::GAT, judgment::AlgStruct)
   body = [toexpr(ctx, a) for a in argsof(judgment)]
   call = Expr(:call, name, callargs...)
   lc = [b for (i,b) in enumerate(getbindings(judgment.localcontext)) 
-        if LID(i) ∉ judgment.typeargs ∪ judgment.args] |> TypeScope
+        if LID(i) ∉ judgment.typeargs ∪ judgment.fields] |> TypeScope
   stexpr = Expr(:struct, false, call, Expr(:block, body...))
   if isempty(lc) 
     return stexpr 
@@ -378,7 +378,7 @@ function parse_struct!(theory::GAT, e, linenumber, ctx=nothing)
   (name, args...) = @match e begin 
     Expr(:struct, false, Expr(:call, name, lc...), Expr(:block, body...)) => begin
       typeargs = parseargs!(theory, lc, localcontext)
-      args = parseargs!(theory, body, localcontext)
+      args = fromexpr(GATContext(theory, localcontext),Expr(:vect,body...),TypeScope)  
       (name, localcontext, typeargs, args)
     end
   end
@@ -393,11 +393,6 @@ function parse_struct!(theory::GAT, e, linenumber, ctx=nothing)
     b = Binding{Judgment}(nothing, AlgAccessor(argdecl, decl, X, i))
     Scopes.unsafe_pushbinding!(theory, b)
   end
-  # theory.fields[X] = Dict{Symbol, LID}()
-  # for lid in str.args
-  #   n = nameof(ident(localcontext;lid))
-  #   theory.fields[X][n] = lid
-  # end
 end
 
 
diff --git a/src/syntax/gats/gat.jl b/src/syntax/gats/gat.jl
index 7733ca8d..e62a0181 100644
--- a/src/syntax/gats/gat.jl
+++ b/src/syntax/gats/gat.jl
@@ -234,7 +234,7 @@ end
 """Get type associated with a field of a struct"""
 function resolvefield(t::Context, method::Ident, field::Symbol)
   str = getvalue(t[method])
-  str[ident(str; name=field)] |> getvalue
+  str.fields[ident(str.fields; name=field)] |> getvalue
 end
 
 """Get all structs in a theory"""
diff --git a/src/syntax/gats/judgments.jl b/src/syntax/gats/judgments.jl
index b583e015..a3ad371c 100644
--- a/src/syntax/gats/judgments.jl
+++ b/src/syntax/gats/judgments.jl
@@ -166,13 +166,14 @@ Is tantamount to (in a vanilla GAT):
   declaration::Ident
   localcontext::TypeScope
   typeargs::Vector{LID}
-  args::Vector{LID}
+  fields::TypeScope
 end
 
 Base.nameof(t::AlgStruct) = nameof(t.declaration)
 typeargsof(t::AlgStruct) = t[t.typeargs]
 typesortsignature(tc::AlgStruct) =
   AlgSort.(getvalue.(typeargsof(tc)))
+argsof(t::AlgStruct) = getbindings(t.fields)
 
 Scopes.getcontext(tc::AlgStruct) = tc.localcontext
 

From 03b8e35f4c156171dbbaa3e23228c2bb31428d69 Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Wed, 1 Nov 2023 17:33:33 -0700
Subject: [PATCH 10/13] AlgDot has ident, no AlgSort needed

---
 src/models/ModelInterface.jl   | 7 ++++++-
 src/syntax/gats/algorithms.jl  | 4 ++--
 src/syntax/gats/ast.jl         | 7 ++++---
 src/syntax/gats/exprinterop.jl | 4 ++--
 4 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl
index c9455621..f532d2b0 100644
--- a/src/models/ModelInterface.jl
+++ b/src/models/ModelInterface.jl
@@ -763,7 +763,12 @@ function to_call_impl(t::AlgTerm, theory::GAT, mod::Union{Symbol,Module}, migrat
   if GATs.isvariable(t)
     nameof(b)
   elseif  GATs.isdot(t)
-    Expr(:., to_call_impl(b.body, theory, mod, migrate), QuoteNode(b.head))
+    impl = to_call_impl(b.body, theory, mod, migrate)
+    if isnamed(b.head)
+      Expr(:., impl, QuoteNode(nameof(b.head)))
+    else 
+      Expr(:ref, impl, getlid(b.head).val)
+    end
   else
     args = to_call_impl.(argsof(b), Ref(theory), Ref(mod), migrate)
     name = nameof(headof(b))
diff --git a/src/syntax/gats/algorithms.jl b/src/syntax/gats/algorithms.jl
index 839d8e25..b19ee1ac 100644
--- a/src/syntax/gats/algorithms.jl
+++ b/src/syntax/gats/algorithms.jl
@@ -183,7 +183,7 @@ function substitute_term(ma::MethodApp{AlgTerm}, subst::Dict{Ident, AlgTerm})
 end
 
 function substitute_term(ad::AlgDot, subst::Dict{Ident, AlgTerm})
-  AlgDot(ad.head, substitute_term(ad.body, subst), ad.sort)
+  AlgDot(ad.head, substitute_term(ad.body, subst))
 end
 
 
@@ -202,6 +202,6 @@ function substitute_funs(ctx::Context, t::AlgTerm)
   elseif isvariable(t) || isconstant(t)
     t 
   elseif isdot(t)
-    AlgTerm(AlgDot(headof(b), substitute_funs(ctx, bodyof(b)), b.sort))
+    AlgTerm(AlgDot(headof(b), substitute_funs(ctx, bodyof(b))))
   end
 end
\ No newline at end of file
diff --git a/src/syntax/gats/ast.jl b/src/syntax/gats/ast.jl
index bba011a2..72f07d0a 100644
--- a/src/syntax/gats/ast.jl
+++ b/src/syntax/gats/ast.jl
@@ -124,7 +124,8 @@ function AlgSort(c::Context, t::AlgTerm)
     value = getvalue(binding)
     AlgSort(value.type)
   elseif isdot(t)
-    AlgSort(resolvefield(c, t.body.sort.method, t.body.head))
+    algstruct = c[AlgSort(c, bodyof(bodyof(t))).method] |> getvalue
+    AlgSort(getvalue(algstruct.fields[headof(bodyof(t))]))
   else # variable
     binding = c[t.body]
     AlgSort(getvalue(binding))
@@ -212,9 +213,9 @@ end
 Accessing a name from a term of tuple type
 """
 @struct_hash_equal struct AlgDot <: AbstractDot
-  head::Symbol
+  head::Ident #Symbol
   body::AlgTerm
-  sort::AlgSort
+  # sort::AlgSort
 end
 headof(a::AlgDot) = a.head 
 bodyof(a::AlgDot) = a.body
diff --git a/src/syntax/gats/exprinterop.jl b/src/syntax/gats/exprinterop.jl
index 5ec2bc0d..612e6b6f 100644
--- a/src/syntax/gats/exprinterop.jl
+++ b/src/syntax/gats/exprinterop.jl
@@ -36,8 +36,8 @@ function fromexpr(c::GATContext, e, ::Type{AlgTerm})
     end
     Expr(:., body, QuoteNode(head)) => begin 
       t = fromexpr(c, body, AlgTerm)
-      str = AlgSort(c, t)
-      AlgTerm(AlgDot(head, t, str))
+      algstruct = c[AlgSort(c, t).method] |> getvalue
+      AlgTerm(AlgDot(ident(algstruct.fields; name=head), t))# , str))
   end
     Expr(:call, head::Symbol, argexprs...) => AlgTerm(parse_methodapp(c, head, argexprs))
     Expr(:(::), val, type) => AlgTerm(Constant(val, fromexpr(c, type, AlgType)))

From c53cd4b9715ae1b9aedfdabfeea923ce8a84b7d2 Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Thu, 2 Nov 2023 09:46:44 -0700
Subject: [PATCH 11/13] primitive vs struct sorts, more coverage

---
 src/models/ModelInterface.jl | 16 ++++------------
 src/syntax/GATs.jl           |  4 ++--
 src/syntax/gats/gat.jl       | 23 +++++++----------------
 src/syntax/gats/judgments.jl |  9 +--------
 test/nonstdlib/Pushouts.jl   |  1 +
 test/syntax/GATs.jl          |  1 +
 6 files changed, 16 insertions(+), 38 deletions(-)

diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl
index f532d2b0..b4f25eff 100644
--- a/src/models/ModelInterface.jl
+++ b/src/models/ModelInterface.jl
@@ -145,18 +145,10 @@ macro instance(head, model, body)
   theory = macroexpand(__module__, :($theory_module.Meta.@theory))
 
   # A dictionary to look up the Julia type of a type constructor from its name (an ident)
-  i = 0
-  jltype_by_sort = Dict(map(sorts(theory)) do s 
-    sorttype = getvalue(theory[methodof(s)])
-    s => if sorttype isa AlgTypeConstructor 
-      i += 1
-      instance_types[i]
-    elseif sorttype isa AlgStruct
-      nameof(sorttype.declaration)
-    end
-  end)
-  i == length(instance_types) || error("Did not use all types ($i): $instance_types")
-
+  jltype_by_sort = Dict{AlgSort,Expr0}([
+    zip(primitive_sorts(theory), instance_types)..., 
+    [s => nameof(headof(s)) for s in struct_sorts(theory)]...
+  ]) 
 
   # Get the model type that we are overloading for, or nothing if this is the
   # default instance for `instance_types`
diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl
index c7db9c82..3d451eb2 100644
--- a/src/syntax/GATs.jl
+++ b/src/syntax/GATs.jl
@@ -5,8 +5,8 @@ export Constant, AlgTerm, AlgType, AlgAST,
   AlgTypeConstructor, AlgAccessor, AlgAxiom, AlgStruct, AlgDot, AlgFunction,
   typesortsignature, sortsignature, getdecl,
   GATSegment, GAT, GATContext, gettheory, gettypecontext, allmethods, 
-  resolvemethod, resolvefield,
-  termcons,typecons, accessors, structs,
+  resolvemethod,
+  termcons,typecons, accessors, structs, primitive_sorts, struct_sorts,
   equations, build_infer_expr, compile, sortcheck, allnames, sorts, sortname,
   InCtx, TermInCtx, TypeInCtx, headof, argsof, methodof, bodyof, argcontext,
   infer_type
diff --git a/src/syntax/gats/gat.jl b/src/syntax/gats/gat.jl
index e62a0181..eba4b2cd 100644
--- a/src/syntax/gats/gat.jl
+++ b/src/syntax/gats/gat.jl
@@ -163,6 +163,12 @@ function allnames(theory::GAT; aliases=false)
 end
 
 sorts(theory::GAT) = theory.sorts
+primitive_sorts(theory::GAT) = 
+  filter(s->getvalue(theory[methodof(s)]) isa AlgTypeConstructor, sorts(theory))
+
+# NOTE: AlgStruct is the only derived sort this returns.
+struct_sorts(theory::GAT) = 
+  filter(s->getvalue(theory[methodof(s)]) isa AlgStruct, sorts(theory))
 
 function termcons(theory::GAT)
   xs = Tuple{Ident, Ident}[]
@@ -231,20 +237,5 @@ else
   Scopes.unsafe_pushbinding!(theory, Binding{Judgment}(name, AlgDeclaration()))
 end
 
-"""Get type associated with a field of a struct"""
-function resolvefield(t::Context, method::Ident, field::Symbol)
-  str = getvalue(t[method])
-  str.fields[ident(str.fields; name=field)] |> getvalue
-end
-
 """Get all structs in a theory"""
-function structs(t::GAT)
-  res = AlgStruct[]
-  for s in sorts(t)
-    v = getvalue(t[methodof(s)])
-    if v isa AlgStruct 
-      push!(res, v)
-    end
-  end
-  res
-end
+structs(t::GAT) = AlgStruct[getvalue(t[methodof(s)]) for s in struct_sorts(t)]
\ No newline at end of file
diff --git a/src/syntax/gats/judgments.jl b/src/syntax/gats/judgments.jl
index a3ad371c..6bc28b36 100644
--- a/src/syntax/gats/judgments.jl
+++ b/src/syntax/gats/judgments.jl
@@ -66,7 +66,7 @@ A declaration of a type constructor.
   args::Vector{LID}
 end
 
-Scopes.getcontext(tc::AlgTypeConstructor) = tc.localcontext
+Scopes.getcontext(tc::TrmTypConstructor) = tc.localcontext
 
 abstract type AccessorField <: Judgment end
 
@@ -87,7 +87,6 @@ exist.
   arg::Int
 end
 
-Scopes.getcontext(::AccessorField) = EmptyContext{AlgType}()
 
 getdecl(acc::AccessorField) = acc.declaration
 
@@ -106,7 +105,6 @@ A declaration of a term constructor as a method of an `AlgFunction`.
   type::Union{TypeScope,AlgType}
 end
 
-Scopes.getcontext(tc::AlgTermConstructor) = tc.localcontext
 
 sortsignature(tc::TrmTypConstructor) =
   AlgSort.(getvalue.(argsof(tc)))
@@ -122,7 +120,6 @@ A declaration of an axiom
   equands::Vector{AlgTerm}
 end
 
-Scopes.getcontext(t::AlgAxiom) = t.localcontext
 
 """
 `AlgSorts`
@@ -175,8 +172,6 @@ typesortsignature(tc::AlgStruct) =
   AlgSort.(getvalue.(typeargsof(tc)))
 argsof(t::AlgStruct) = getbindings(t.fields)
 
-Scopes.getcontext(tc::AlgStruct) = tc.localcontext
-
 """
 A shorthand for a function, such as "square(x) := x * x".  It is relevant for 
 models but can be ignored by theory maps, as it is fully determined by other 
@@ -188,5 +183,3 @@ judgments in the theory.
   args::Vector{LID}
   value::AlgTerm
 end
-
-Scopes.getcontext(tc::AlgFunction) = tc.localcontext
diff --git a/test/nonstdlib/Pushouts.jl b/test/nonstdlib/Pushouts.jl
index 76597ef5..7b2b2a98 100644
--- a/test/nonstdlib/Pushouts.jl
+++ b/test/nonstdlib/Pushouts.jl
@@ -28,4 +28,5 @@ Universal input:                    Output
   @test cospan(res) == Cospan(4, [1,1,2,3], [1,2,4])
   @test ι₁(res) == [1,1,2,3]
   @test universal(res, Cospan(4, [3,3,2,2],[3,2,1])) == [3,2,2,1]
+  @test_throws ErrorException universal(PushoutInt(4, [1,1,2,3],[1,2,3]), Cospan(4, [3,3,2,2],[3,2,1]))
 end
diff --git a/test/syntax/GATs.jl b/test/syntax/GATs.jl
index fe34251d..7640d69f 100644
--- a/test/syntax/GATs.jl
+++ b/test/syntax/GATs.jl
@@ -64,6 +64,7 @@ ob_decl = getvalue(thcat[O])
 
 ObT = fromexpr(thcat, :Ob, AlgType)
 ObS = AlgSort(ObT)
+@test headof(ObS) == O
 @test toexpr(GATContext(thcat), ObS) == :Ob
 
 

From d91b2aa5b51035ec44b2ff8d77595f4f2b96b963 Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Fri, 10 Nov 2023 19:35:34 +0530
Subject: [PATCH 12/13] cleanup

---
 src/nonstdlib/models/Pushouts.jl | 6 +++---
 src/syntax/gats/ast.jl           | 8 ++++++--
 src/syntax/gats/judgments.jl     | 4 ++++
 3 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/src/nonstdlib/models/Pushouts.jl b/src/nonstdlib/models/Pushouts.jl
index 06f93765..c91376c6 100644
--- a/src/nonstdlib/models/Pushouts.jl
+++ b/src/nonstdlib/models/Pushouts.jl
@@ -23,19 +23,19 @@ using .ThPushout
     rootindex = sort(collect(Set(values(roots))))
     toindex = [findfirst(==(r),rootindex) for r in roots]
     PushoutInt(DataStructures.num_groups(d), 
-     [toindex[roots[b]] for b in 1:B], 
+     [toindex[roots[b]] for b in 1:B],
      [toindex[roots[c+B]] for c in 1:C]
     )
   end
   cospan(p::PushoutInt) = Cospan(p.ob, p.i1, p.i2)
-  function universal(p::PushoutInt, csp::Cospan; context)
+  function universal(p::PushoutInt, csp::Cospan)
     map(1:p.ob) do i
       for (proj, csp_map) in [(p.i1, csp.left), (p.i2, csp.right)]
         for (j, i′) in enumerate(proj)
           if i′ == i return csp_map[j] end
         end
       end
-      error("Pushout is jointly surjective")
+      error("Pushout $p is not jointly surjective")
     end
   end
 end
diff --git a/src/syntax/gats/ast.jl b/src/syntax/gats/ast.jl
index 72f07d0a..6cfc7120 100644
--- a/src/syntax/gats/ast.jl
+++ b/src/syntax/gats/ast.jl
@@ -16,6 +16,11 @@ A *sort*, which is essentially a type constructor without arguments
   method::Ident
 end
 
+"""
+`AlgSort`
+
+A sort for equality judgments of terms for a particular sort
+"""
 @struct_hash_equal struct AlgEqSort <: AbstractAlgSort
   head::Ident
   method::Ident
@@ -213,9 +218,8 @@ end
 Accessing a name from a term of tuple type
 """
 @struct_hash_equal struct AlgDot <: AbstractDot
-  head::Ident #Symbol
+  head::Ident
   body::AlgTerm
-  # sort::AlgSort
 end
 headof(a::AlgDot) = a.head 
 bodyof(a::AlgDot) = a.body
diff --git a/src/syntax/gats/judgments.jl b/src/syntax/gats/judgments.jl
index 6bc28b36..096de5eb 100644
--- a/src/syntax/gats/judgments.jl
+++ b/src/syntax/gats/judgments.jl
@@ -158,6 +158,10 @@ Is tantamount to (in a vanilla GAT):
       ⊣ [(dom, codom, apex)::Ob, i_1::dom->apex, i_2::codom->apex]
     i2(cospan(a, i_1, i_2)) == i_2
       ⊣ [(dom, codom, apex)::Ob, i_1::dom->apex, i_2::codom->apex]
+
+    cospan(apex(csp), i1(csp), i2(csp)) == csp
+      ⊣ [(dom, codom)::Ob, csp::Cospan(dom, codom)]
+
 """
 @struct_hash_equal struct AlgStruct <: TrmTypConstructor
   declaration::Ident

From bfc173b0e1fc48ec8674990e8c98dcd044d26051 Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Sat, 11 Nov 2023 07:29:25 +0530
Subject: [PATCH 13/13] migrate -> migrate_theory

---
 src/models/ModelInterface.jl              | 4 ++--
 src/stdlib/derivedmodels/DerivedModels.jl | 6 +++---
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/models/ModelInterface.jl b/src/models/ModelInterface.jl
index b4f25eff..dd104b00 100644
--- a/src/models/ModelInterface.jl
+++ b/src/models/ModelInterface.jl
@@ -1,7 +1,7 @@
 module ModelInterface
 
 export Model, implements, TypeCheckFail, SignatureMismatchError, 
-       @model, @instance, @withmodel, @fail, migrate
+       @model, @instance, @withmodel, @fail, migrate_theory
 
 using ...Syntax
 using ...Util.MetaUtils
@@ -780,6 +780,6 @@ function to_call_accessor(t::AlgTerm, x::Symbol, mod::Module)
   Expr(:call, Expr(:ref, :($mod.$(nameof(headof(b)))), :(model.model)), rest)
 end
 
-migrate(theorymap::Module, m::Model) = theorymap.Migrator(m)
+migrate_theory(theorymap::Module, m::Model) = theorymap.Migrator(m)
 
 end # module
diff --git a/src/stdlib/derivedmodels/DerivedModels.jl b/src/stdlib/derivedmodels/DerivedModels.jl
index a2b80cb1..dff93ee2 100644
--- a/src/stdlib/derivedmodels/DerivedModels.jl
+++ b/src/stdlib/derivedmodels/DerivedModels.jl
@@ -6,12 +6,12 @@ using ...StdTheoryMaps
 using ...StdModels
 
 # Given a model of a category C, we can derive a model of Cᵒᵖ.
-OpFinSetC = migrate(OpCat, FinSetC())
+OpFinSetC = migrate_theory(OpCat, FinSetC())
 
 # Interpret `e` as `0` and `⋅` as `+`.
-IntMonoid = migrate(NatPlusMonoid, IntNatPlus())
+IntMonoid = migrate_theory(NatPlusMonoid, IntNatPlus())
 
 # Interpret `id` as reflexivity and `compose` as transitivity.
-IntPreorderCat = migrate(PreorderCat, IntPreorder())
+IntPreorderCat = migrate_theory(PreorderCat, IntPreorder())
 
 end # module