From 7f74fa4568d66f1898ed40d10397b8d48d046bd4 Mon Sep 17 00:00:00 2001
From: Matt Cuffaro <cuffaro.matt@gmail.com>
Date: Sat, 7 Mar 2026 20:26:25 -0500
Subject: [PATCH] WIP

---
 src/DynTrait.jl        | 90 ++++++++++++++++++++++++++++++++++++++++++
 src/TraitInterfaces.jl |  1 +
 test/Renaming.jl       | 12 ++----
 3 files changed, 94 insertions(+), 9 deletions(-)
 create mode 100644 src/DynTrait.jl

diff --git a/src/DynTrait.jl b/src/DynTrait.jl
new file mode 100644
index 0000000..7dbcc76
--- /dev/null
+++ b/src/DynTrait.jl
@@ -0,0 +1,90 @@
+using MLStyle: @λ
+using DataStructures: OrderedDict
+
+const LNN = LineNumberNode
+
+function makefunc(name::Symbol, fieldtoparam::OrderedDict, fieldtotheory::OrderedDict, fieldtogensym::OrderedDict, fieldtotype::OrderedDict)
+    implementcalls = [Expr(:macrocall, Symbol("@assert"), LNN, Expr(:call, :implements, field, type)) for (field, type) in fieldtotheory]
+    bindings = [Expr(:(::), field, type) for (field, type) in fieldtotype]
+    params = unique(values(fieldtoparam)) 
+    # TODO ^ we need to make sure they are in the same order as the typeparams...
+    # TODO ^ why unique?
+    Expr(:function,
+        Expr(:where, Expr(:call, name, bindings...), params...),
+        Expr(:block, implementcalls...,
+             # for every field whose type implements an interface,
+             Expr(:call, Expr(:curly, :new, params...), keys(fieldtotype)...)))
+end
+
+""" @impl
+
+This macro interprets `⊢` (\vdash) bindings in a struct as bindings to fields which implement a certain interface specified by @instance.
+```julia
+@impl Graph
+    V⊢ThRing
+    E⊢ThRing
+end
+```
+Here is an example of a struct with trait-type, a concrete type, and a type parameter.
+```julia
+@impl _J{S}
+    a⊢ThMonoid
+    b::Int
+    c::S
+end
+```
+
+"""
+macro impl(body)
+    funcname = nothing 
+    # XXX recall that a dictionary is not ordered
+    fieldtotype = OrderedDict{Symbol, Symbol}() # e.g., :a => Symbol("##ThRing#999"), :b => :Int, :c => T
+    fieldtogensym = OrderedDict{Symbol, Symbol}() # e.g., :a => Symbol("##ThRing#999")
+    fieldtoparam = OrderedDict{Symbol, Symbol}() # fieldtotype, but restricted to parameters
+    fieldtotheory = OrderedDict{Symbol, Symbol}() # e.g., :a => :ThRing
+    ordinaryparams = nothing
+    expr = @λ begin
+        # struct A{T}; ... end
+        Expr(:struct, ismutable, Expr(:curly, name, typeparams...), e) => begin
+            funcname = name
+            ordinaryparams = typeparams
+            block = expr(e)
+            theoryparams = values(fieldtoparam)
+            Expr(:struct, ismutable, Expr(:curly, name, theoryparams...), block)
+        end
+        # struct A; ... end
+        Expr(:struct, ismutable, name, e) => begin
+            funcname = name
+            block = expr(e) 
+            theoryparams = values(fieldtoparam)
+            Expr(:struct, ismutable, Expr(:curly, name, theoryparams...), block)
+        end
+        # a ⊢ ThRing
+        Expr(:call, :⊢, field, theory) => begin
+            type=gensym(theory) # e.g., Symbol("##ThRing#999")
+            push!(fieldtotype, field => type)
+            push!(fieldtoparam, field => type)
+            push!(fieldtogensym, field => type)
+            push!(fieldtotheory, field => theory)
+            Expr(:(::), field, type)
+        end
+        # a::Int
+        Expr(:(::), field, type) => begin
+            push!(fieldtotype, field => type)
+            if !isnothing(ordinaryparams) && type ∈ ordinaryparams
+                push!(fieldtoparam, field => type)
+            end
+            Expr(:(::), field, type)
+        end
+        #
+        Expr(:block, args...) => begin
+            args = expr.(args)
+            newfun = makefunc(funcname, fieldtoparam, fieldtotheory, fieldtogensym, fieldtotype)
+            Expr(:block, args..., newfun)
+        end
+        #
+        s => s
+    end
+    newbody = expr(body)
+    newbody
+end
diff --git a/src/TraitInterfaces.jl b/src/TraitInterfaces.jl
index d14dda2..3eccd18 100644
--- a/src/TraitInterfaces.jl
+++ b/src/TraitInterfaces.jl
@@ -2,6 +2,7 @@ module TraitInterfaces
 
 using Reexport 
 
+include("DynTrait.jl")
 include("MetaUtils.jl")
 
 include("Interfaces/module.jl")
diff --git a/test/Renaming.jl b/test/Renaming.jl
index be93e63..acd04e1 100644
--- a/test/Renaming.jl
+++ b/test/Renaming.jl
@@ -4,22 +4,18 @@ using TraitInterfaces, Test
 
 @interface ThMonoid begin
   X::TYPE
-
   unit()::X
   @op (e) := unit
-
   mul(x::X,y::X)::X
   @op (⋅) := mul
-
   assoc := (x ⋅ y) ⋅ z == x ⋅ (y⋅ z) ⊣ [(x,y,z)::X]
   unitality := ((e() ⋅ x) == x == (x ⋅ e())) ⊣ [x::X]
 end
 
 
 @interface ThGroup <: ThMonoid begin
-  inv(x::X)::X
-  @op (⁻¹) := inv
-
+  inverse(x::X)::X
+  @op (⁻¹) := inverse
   ⁻¹(x) ⋅ x == x == x ⋅ ⁻¹(x) ⊣ [x::X]
 end
 
@@ -31,12 +27,10 @@ module RingModule
   export ThRing
   using TraitInterfaces
   using ..ThAbGroup, ..ThMonoid
-
   @interface ThRing begin
     using ThAbGroup: unit => zero, mul => plus,  :⋅ => :+, e => Z, 
-                     inv => minus, ⁻¹ => :-
+                     inverse => minus, ⁻¹ => :-
     using ThMonoid:  unit => one,  mul => times, :⋅ => :×, e => I
-
     left_distrib  := a × (b + c) == (a × b) + (a × c) ⊣ [(a, b, c)::X]
     right_distrib := (b + c) × a == (b × a) + (c × a) ⊣ [(a, b, c)::X]
   end