Simple theory maps and simple pushouts

src/syntax/Scopes.jl

@@ -4,7 +4,7 @@ export
   ScopeTagError,
   LID,
   Ident, Alias, gettag, getlid, isnamed,
-  Binding, getvalue, setvalue, getline, setline,
+  Binding, getvalue, setname, setvalue, getline, setline,
   Context, getscope, nscopes, getlevel, hasname, hastag, alltags, allscopes,
   HasContext, getcontext,
   hasident, ident, getidents, idents, canonicalize,
@@ -155,14 +155,14 @@ function Base.show(io::IO, x::Ident)
 end
 
 retag(replacements::Dict{ScopeTag, ScopeTag}, x::Ident) =
-  if gettag(x) ∈ keys(replacements)
+  if haskey(replacements, gettag(x))
     Ident(replacements[gettag(x)], getlid(x), nameof(x))
   else
     x
   end
 
 rename(tag::ScopeTag, replacements::Dict{Symbol, Symbol}, x::Ident) =
-  if gettag(x) == tag && nameof(x) ∈ keys(replacements)
+  if haskey(replacements, nameof(x)) && gettag(x) == tag
     Ident(tag, getlid(x), replacements[nameof(x)])
   else
     x

src/syntax/TheoryMaps.jl

@@ -1,12 +1,13 @@
 module TheoryMaps
-export IdTheoryMap, TheoryIncl, AbsTheoryMap, TheoryMap, @theorymap,
+export IdTheoryMap, TheoryIncl, AbsTheoryMap, SimpleTheoryMap, TheoryMap, @theorymap,
        TypeMap, TermMap, typemap, termmap
 
-using ..GATs, ..Scopes, ..ExprInterop
+using ..GATs, ..Scopes, ..ExprInterop, ...Util.MetaUtils
 using ..Scopes: unsafe_pushbinding!
-using ..GATs: InCtx, bindingexprs, substitute_term
+using ..GATs: InCtx, TrmTypConstructor, bindingexprs, substitute_term, reident
 using ..TheoryInterface
 import ..ExprInterop: toexpr, fromexpr
+import ..Scopes: rename
 
 using StructEquality, MLStyle
 using DataStructures: OrderedDict
@@ -199,8 +200,64 @@
 
   Dict([k=>v[1] for (k,v) in pairs(typed_terms)])
 end
+# Simple
+#-------
+"""
+Simple theory maps just send idents to idents, not general terms
+This ought not be allowed to send two idents of the same name to idents of 
+different names in the codom.
+"""
+@struct_hash_equal struct SimpleTheoryMap <: AbsTheoryMap
+  dom::GAT 
+  codom::GAT
+  typmap::Dict{Ident,Ident}
+  trmmap::Dict{Ident,Ident}
+end
+
+"""
+Induce a SimpleTheoryMap via a mapping of names. 
+
+Any typecon / termcon constructors whose name is not in the dictionary must be 
+shared by the dom/codom
+"""
+function SimpleTheoryMap(d::GAT, c::GAT, names::Dict{Symbol,Symbol})
+  typs, trms, iddict = [Dict{Ident, Ident}() for _ in 1:3]
+  for xs in d.segments.scopes
+    for (x, v) in identvalues(xs)
+      if v isa AlgDeclaration 
+        iddict[x] = ident(c; name=get(names, nameof(x), nameof(x)))
+      elseif v isa TrmTypConstructor
+        v′ = reident(merge(typs, trms, iddict), v)
+        m = GATs.methodlookup(GATContext(c), iddict[v.declaration], sortsignature(v′))
+        (v isa AlgTermConstructor ? trms : typs)[x] = m
+      end
+    end
+  end
+  SimpleTheoryMap(d, c, typs, trms)
+end
+
+"""Go from Dict{Ident,Ident} to Dict{Symbol,Symbol}"""
+function namedict(m::SimpleTheoryMap)
+  Dict{Symbol,Symbol}(vcat(map([m.typmap, m.trmmap]) do d
+    map(collect(d)) do (k,v)
+      map([dom(m) => k, codom(m) => v]) do (theory, x)
+        nameof(getvalue(theory[x]).declaration)
+      end
+    end
+  end...))
+end
+
+typemap(m::SimpleTheoryMap) = 
+  OrderedDict(k => TypeInCtx(codom(m), m.typmap[k]) for k in last.(typecons(dom(m))))
+
+termmap(m::SimpleTheoryMap) = 
+  OrderedDict(k => TermInCtx(codom(m), m.trmmap[k]) for k in last.(termcons(dom(m))))
+
+function compose(f::SimpleTheoryMap, g::SimpleTheoryMap)
+  nf, ng = namedict(f), namedict(g)
+  SimpleTheoryMap(dom(f), codom(g), Dict(k=>get(ng,v,v) for (k,v) in nf))
+end
 
-# ID 
 #---
 @struct_hash_equal struct IdTheoryMap <: AbsTheoryMap
   gat::GAT
@@ -229,10 +286,12 @@
 @struct_hash_equal struct TheoryIncl <: AbsTheoryMap
   dom::GAT
   codom::GAT
-  function TheoryIncl(dom,codom) 
-    err = "Cannot construct TheoryInclusion"
-    dom ⊆ codom ? new(dom,codom) : error(err)
-  end
+  # `⊆` is a sufficient but not necessary condition of judgment-wise inclusion
+  # since the judgments may be split apart across different scopes in the codom 
+  #function TheoryIncl(dom,codom) 
+    #err = "Cannot construct TheoryInclusion"
+    #dom ⊆ codom ? new(dom,codom) : error(err)
+  #end
 end
 
 typemap(ι::Union{IdTheoryMap,TheoryIncl}) = 
@@ -243,8 +302,11 @@
 
 compose(f::TheoryIncl, g::TheoryIncl) = TheoryIncl(dom(f), codom(g))
 
-compose(f::AbsTheoryMap, g::TheoryIncl) = 
-  TheoryIncl(dom(f), codom(g), typemap(f), termmap(f))
+compose(f::TheoryIncl, g::SimpleTheoryMap) = 
+  SimpleTheoryMap(dom(f), codom(g), namedict(g))
+
+compose(f::SimpleTheoryMap, g::TheoryIncl) = 
+  SimpleTheoryMap(dom(f), codom(g), namedict(f))
 
 Base.inv(f::TheoryIncl) = 
   dom(f) == codom(f) ? f : error("Cannot invert a nontrivial theory inclusion")
@@ -283,6 +345,50 @@
 """Invert a theory iso"""
 # Base.inv(::TheoryMap) = error("Not implemented")
 
+# Renaming
+#---------
+
+"""
+Rename a GAT, T, yielding a GAT T' and a morphism T → T'
+"""
+function rename(theory::GAT, namedict::Dict{Symbol, Symbol}; name=nothing)
+  newtheory = GAT(isnothing(name) ? nameof(theory) : name)
+  iddict, typmap, trmmap = [Dict{Ident,Ident}() for _ in 1:3]
+
+  for xs in theory.segments.scopes
+    GATs.unsafe_newsegment!(newtheory)
+    for (x, v) in identvalues(xs)
+      if v isa AlgDeclaration 
+        b = MetaUtils.setname(theory[x], get(namedict, nameof(x), nameof(x)))
+        x′ = Scopes.unsafe_pushbinding!(newtheory, b)
+        iddict[x] = x′
+      elseif v isa TrmTypConstructor
+        x′ = Scopes.unsafe_pushbinding!(newtheory, reident(iddict, theory[x]))
+        (v isa AlgTermConstructor ? trmmap : typmap)[x] = x′
+        iddict[x] = x′
+      elseif v isa AlgAxiom
+        Scopes.unsafe_pushbinding!(newtheory, reident(iddict, theory[x]))
+      end
+    end
+  end
+
+  SimpleTheoryMap(theory, newtheory, typmap, trmmap)
+end
+
+"""
+Pushout of a multispan of theories. If necessary, names can be disambiguated
+via `names` - a vector of Dict{Symbol, Symbol} of the same length 
+"""
+function pushout(maps::Vector{<:AbsTheoryMap}; name=nothing, names=nothing)
+  any(m->m isa TheoryMap, maps) && error("Cannot pushout general theory maps")
+  names = isnothing(names) ? fill(Dict{Symbol,Symbol}(), length(maps)) : names
+  feet = rename.(codom.(maps), names)
+  apex = GAT(isnothing(name) ? Symbol(join(nameof.(feet), "_")) : name)
+  union!.(Ref(apex), codom.(feet))
+  [compose(f, TheoryIncl(codom(f), apex)) for f in feet]
+end
+
+pushout(maps::AbsTheoryMap...; name=nothing, names=nothing) = pushout(collect(maps); name, names)
 
 # Serialization
 #--------------

src/syntax/gats/gat.jl

@@ -119,19 +119,16 @@ function unsafe_updatecache!(theory::GAT, x::Ident, judgment::AlgStruct)
   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
 end
 
-function unsafe_updatecache!(theory::GAT, x::Ident, judgment::AlgAxiom)
+function unsafe_updatecache!(theory::GAT, x::Ident, ::AlgAxiom)
   push!(theory.axioms, x)
 end
 
-function unsafe_updatecache!(theory::GAT, x::Ident, judgment::Alias)
-  nothing
-end
+unsafe_updatecache!(::GAT, ::Ident, ::Alias) = nothing
 
 function Scopes.unsafe_pushbinding!(theory::GAT, binding::Binding{Judgment})
   x = Scopes.unsafe_pushbinding!(theory.segments, binding)
@@ -174,6 +171,57 @@ function Base.show(io::IO, theory::GAT)
   end
 end
 
+# Merging overlapping GATs
+
+"""
+There is no shadowing allowed in GATs, so if the new theory shares an 
+AlgDeclaration name with the base theory, the new theory Idents which refer 
+to that name should instead be retagged to refer to the AlgDeclaration in the 
+base theory.
+
+Returns a Dict mapping idents from the merged-in theory into the modified base 
+theory.
+"""
+function Base.union!(base::GAT, theory::GAT)
+  dict = Dict{Ident,Ident}()
+  for xs in theory.segments.scopes
+    unsafe_newsegment!(base)
+    for (x, v) in identvalues(xs)
+      if v isa AlgDeclaration 
+        if !hasident(base; name=nameof(x)) 
+          Scopes.unsafe_pushbinding!(base, theory[x])
+        end
+        dict[x] = ident(base; name=nameof(x))
+      else
+        x′ = nothing
+        v′ = reident(dict, v)
+        set = setvalue(theory[x], v′)
+        if v isa TrmTypConstructor
+          sig = sortsignature(v′)
+          res = base.resolvers[v′.declaration].bysignature
+          x′ = haskey(res, sig) ? res[sig] : Scopes.unsafe_pushbinding!(base, set)
+        elseif v isa AlgAxiom
+          for ax in base.axioms
+            axiom = getvalue(base[ax])
+            actx, vctx = getcontext.([axiom, v])
+            if values(actx) == [reident(dict, t) for t in values(vctx)]
+              dic = Dict([pairs(dict)..., zip(getidents.([vctx,actx])...)...])
+              if axiom.equands == [reident(dic, eq) for eq in v.equands]
+                x′ = ax
+              end
+            end
+          end
+          if isnothing(x′) 
+            x′ = Scopes.unsafe_pushbinding!(base, set)
+          end
+        end
+        dict[x] = x′
+      end
+    end
+  end
+  return dict
+end
+
 # Accessors
 
 Base.nameof(theory::GAT) = theory.name
@@ -218,7 +266,6 @@ function typecons(theory::GAT)
   xs
 end
 
-
 Base.issubset(t1::GAT, t2::GAT) =
   all(s->hastag(t2, s), gettag.(Scopes.getscopelist(t1).scopes))
 

src/syntax/gats/judgments.jl

@@ -7,7 +7,7 @@
 A scope where variables are assigned to `AlgType`s. We use a wrapper
 here so that it pretty prints as `[a::B]` instead of `{a => AlgType(B)}`
 """
-struct TypeScope <: HasScope{AlgType}
+@struct_hash_equal struct TypeScope <: HasScope{AlgType}
   scope::Scope{AlgType}
 end
 
@@ -18,9 +18,13 @@ TypeScope(bindings::Vector{Binding{AlgType}}; tag=newscopetag()) = TypeScope(Sco
 TypeScope(bindings::Pair{Symbol, AlgType}...) = TypeScope(Scope{AlgType}(bindings...))
 
 Scopes.getscope(ts::TypeScope) = ts.scope
+
 Scopes.unsafe_pushbinding!(ts::TypeScope, b) = 
   Scopes.unsafe_pushbinding!(ts.scope, b)
 
+reident(d::Dict{Ident, Ident}, ts::TypeScope) = 
+  TypeScope(reident(d, getscope(ts)))
+
 function Base.show(io::IO, ts::TypeScope)
   print(io, toexpr(EmptyContext{AlgType}(), ts))
 end
@@ -68,6 +72,13 @@ end
 
 Scopes.getcontext(tc::TrmTypConstructor) = tc.localcontext
 
+reident(d::Dict{Ident,Ident}, tc::AlgTypeConstructor) = AlgTypeConstructor(
+  get(d, tc.declaration, tc.declaration),
+  reident(d, Scopes.getcontext(tc)),
+  tc.args,
+)
+
+
 abstract type AccessorField <: Judgment end
 
 """
@@ -106,8 +117,35 @@ A declaration of a term constructor as a method of an `AlgFunction`.
 end
 
 
-sortsignature(tc::TrmTypConstructor) =
-  AlgSort.(getvalue.(argsof(tc)))
+sortsignature(tc::TrmTypConstructor) = AlgSort.(getvalue.(argsof(tc)))
+
+reident(d::Dict{Ident,Ident}, tc::AlgTermConstructor) = AlgTermConstructor(
+  get(d, tc.declaration, tc.declaration),
+  reident(d, Scopes.getcontext(tc)),
+  tc.args,
+  reident(d, tc.type)
+)
+
+function reident(d::Dict{Ident, Ident}, s::Scope{AlgType})
+  Scope(Binding{AlgType}[setvalue(b, reident(d, getvalue(b))) for b in s.bindings]; 
+        tag = gettag(s))
+end
+
+reident(d::Dict{Ident, Ident}, s::AlgSort) = 
+  AlgSort(reident(d, headof(s)), reident(d, methodof(s)))
+
+reident(d::Dict{Ident, Ident}, s::T) where T<:AlgAST = 
+  T(reident(d, bodyof(s)))
+
+reident(d::Dict{Ident, Ident}, x::Ident) = get(d, x, x)
+
+reident(d::Dict{Ident, Ident}, m::MethodApp{T}) where T = 
+  MethodApp{T}(reident(d, headof(m)), reident(d, methodof(m)), 
+               reident.(Ref(d), argsof(m)))
+
+reident(d::Dict{Ident,Ident}, b::Binding{Judgment}) =   
+  setvalue(b, reident(d, getvalue(b)))
+
 
 """
 `AlgAxiom`
@@ -120,6 +158,13 @@ A declaration of an axiom
   equands::Vector{AlgTerm}
 end
 
+Scopes.getcontext(ax::AlgAxiom) = ax.localcontext
+
+reident(d::Dict{Ident,Ident}, ax::AlgAxiom) = AlgAxiom(
+  reident(d, Scopes.getcontext(ax)),
+  reident(d, ax.sort),
+  reident.(Ref(d), ax.equands)
+)
 
 """
 `AlgSorts`

test/syntax/GATs.jl

@@ -143,6 +143,23 @@ end
   id_span(x) := Span(x, id(x),id(x)) ⊣ [x::Ob]
 end
 
+# Union
+#######
+
+@theory ThMonoid2 <: ThSemiGroup begin
+  e() :: default
+  e() ⋅ x == x ⊣ [x]
+  x ⋅ e() == x ⊣ [x]
+  e() ⋅ e() == e() ⊣ [x]
+end
+
+T, T′ = deepcopy.([ThMonoid.Meta.theory, ThMonoid2.Meta.theory]);
+@test length(T.axioms) == 3
+dic = union!(T, T′)
+@test dic isa Dict
+@test length(T.axioms) == 4
+@test length(termcons(T)) == 2
+@test length(typecons(T)) == 1
 
 
 end # module