From b912ea267b59c254e4e7ab6bf85de159aca1b016 Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Tue, 12 Sep 2023 13:09:40 -0700
Subject: [PATCH] better test coverage

---
 src/syntax/GATs.jl        | 12 +-----------
 src/syntax/Scopes.jl      | 14 --------------
 src/syntax/TheoryMaps.jl  | 32 +++++++++++++-------------------
 test/syntax/GATs.jl       |  8 ++++++++
 test/syntax/Scopes.jl     |  7 +++++++
 test/syntax/TheoryMaps.jl | 19 +++++++++++++++++++
 6 files changed, 48 insertions(+), 44 deletions(-)

diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl
index 8784cd89..dc38ae93 100644
--- a/src/syntax/GATs.jl
+++ b/src/syntax/GATs.jl
@@ -110,7 +110,7 @@ headof(t::TrmTyp) = t.head
 argsof(t::TrmTyp) = t.args
 
 rename(tag::ScopeTag, reps::Dict{Symbol,Symbol}, t::T) where T<:TrmTyp =
-  T(rename(tag, reps, headof(t)), rename.(Ref(tag), Ref(reps), argsof(t)))
+  T(rename(tag, reps, headof(t)), AlgTerm[rename.(Ref(tag), Ref(reps), argsof(t))...])
 
 function Base.show(io::IO, type::T) where T<:TrmTyp
   print(io, "$(nameof(T))(")
@@ -257,11 +257,6 @@ sortsignature(tc::Union{AlgTypeConstructor, AlgTermConstructor}) =
 argcontext(t::Union{AlgTypeConstructor,AlgTermConstructor}) = 
   t.localcontext + t.args
 
-function retag_args(t::AlgTermConstructor) 
-  ac = gettag(argcontext(t))
-  Dict(gettag(t.localcontext)=>ac, gettag(t.args)=>ac)
-end
-
 """
 `AlgAxiom`
 
@@ -736,11 +731,6 @@ end
 ExprInterop.toexpr(c::Context, ts::TypeScope) =
   Expr(:vect,[Expr(:(::), nameof(b), toexpr(c, getvalue(b))) for b in ts]...)
 
-ExprInterop.fromexpr(c::Context, e, ::Type{TypeScope}) = @match e begin 
-  Expr(:vect, ps...) => parsetypescope(c, ps)
-  _ => error("Here $e $(dump(e))")
-end
-
 ExprInterop.toexpr(c::Context, at::Binding{AlgType, Nothing}) =
   Expr(:(::), nameof(at), ExprInterop.toexpr(c, getvalue(at)))
 
diff --git a/src/syntax/Scopes.jl b/src/syntax/Scopes.jl
index af52e75a..55e7891d 100644
--- a/src/syntax/Scopes.jl
+++ b/src/syntax/Scopes.jl
@@ -467,20 +467,6 @@ retag(replacements::Dict{ScopeTag,ScopeTag}, s::Scope{T,Sig}) where {T,Sig} =
                retag.(Ref(replacements), s.bindings), 
                s.names)
 
-function rename(tag::ScopeTag, 
-                replacements::Dict{Symbol, Symbol}, 
-                scope::Scope{T, Sig}) where {T, Sig}
-  if tag == gettag(scope)
-    Scope{T,Sig}(tag, map(scope.bindings) do b
-      Binding{T,Sig}(get(replacements,b.primary,b.primary), 
-              Set([get(replacements, a, a) for a in b.aliases]), 
-              rename(tag, replacements, b.value), b.sig, b.line)
-    end, Dict(get(replacements, k, k)=>v for (k,v) in collect(scope.names)))
-  else 
-    Scope{T,Sig}(tag, retag(Ref(replacements), ))
-  end
-end
-
 function Base.:(+)(x::Scope{T,Sig}, y::Scope{T,Sig}) where {T,Sig}
   newtag = x.tag+y.tag
   rep = Dict(gettag(x) => newtag, gettag(y)=>newtag)
diff --git a/src/syntax/TheoryMaps.jl b/src/syntax/TheoryMaps.jl
index 0aeccc72..131d5d70 100644
--- a/src/syntax/TheoryMaps.jl
+++ b/src/syntax/TheoryMaps.jl
@@ -22,29 +22,22 @@ thought of in many ways.
 3. X is a syntax for Y's semantics. 
 
 The main methods for an AbsTheoryMap to implement are: 
-  dom, codom, typemap, termmap
+  - dom, codom, 
+  - typemap: A dictionary of Ident (of AlgTypeConstructor in domain) to AlgSort
+             (This must be a AlgSort of the same arity.) 
+  - termmap: A dictionary of Ident (of AlgTermConstructor in domain) to 
+             TermInCtx. (The TypeScope of the TrmInCtx must be structurally 
+             identical to the localcontext + args of the term constructor 
+             associated with the key.)
+  
 """
 abstract type AbsTheoryMap end
 
-"""
-A dictionary of Ident (of AlgTypeConstructor in domain) to AlgSort
-
-This must be a AlgSort of the same arity.
-"""
-typemap(::AbsTheoryMap)::Dict{Ident, AlgSort} = error("Not implemented")
-
-"""
-A dictionary of Ident (of AlgTermConstructor in domain) to TermInCtx.
-The TypeScope of the TrmInCtx must be structurally identical to the 
-localcontext + args of the term constructor associated with the key.
-"""
-termmap(::AbsTheoryMap)::Dict{Ident, TermInCtx} = error("Not implemented")
-
 # Category of GATs
 #-----------------
-dom(f::AbsTheoryMap)::GAT = f.dom
+dom(f::AbsTheoryMap)::GAT = f.dom # assume this exists by default
 
-codom(f::AbsTheoryMap)::GAT = f.codom
+codom(f::AbsTheoryMap)::GAT = f.codom # assume this exists by default
 
 function compose(f::AbsTheoryMap, g::AbsTheoryMap)
   typmap = Dict(k => typemap(g)[only(v.ref)] for (k,v) in pairs(typemap(f)))
@@ -128,6 +121,8 @@ dom(f::IdTheoryMap)::GAT = f.gat
 
 codom(f::IdTheoryMap)::GAT = f.gat
 
+compose(f::IdTheoryMap, ::IdTheoryMap) = f
+
 compose(::IdTheoryMap, g::AbsTheoryMap) = g
 
 compose(f::AbsTheoryMap, ::IdTheoryMap) = f
@@ -240,7 +235,6 @@ end
 
 macro theorymap(head, body)
   (domname, codomname) = @match head begin
-    (name::Symbol) => (name, nothing)
     Expr(:call,:(=>), name, parent) => (name, parent)
     _ => error("could not parse head of @theory: $head")
   end
@@ -251,6 +245,6 @@ macro theorymap(head, body)
 end
 
 """Invert a theory iso"""
-Base.inv(::TheoryMap) = error("Not implemented")
+# Base.inv(::TheoryMap) = error("Not implemented")
 
 end # module
diff --git a/test/syntax/GATs.jl b/test/syntax/GATs.jl
index ef89f3e5..610c0126 100644
--- a/test/syntax/GATs.jl
+++ b/test/syntax/GATs.jl
@@ -59,6 +59,8 @@ O, H, i, cmp = idents(seg; lid=LID.(1:4))
 # Extend seg with a context of (A: Ob)
 sortscope = Scope([Binding{AlgType}(:A, Set([:A]), AlgType(O))])
 A = ident(sortscope; name=:A)
+ATerm = AlgTerm(A)
+
 
 ss = AppendScope(ScopeList([seg]), sortscope)
 @test sortcheck(ss, AlgTerm(A)) == AlgSort(O)
@@ -78,6 +80,12 @@ haia = AlgType(H,[AlgTerm(A),ida])
 @test sortcheck(ss, haa)
 @test_throws Exception sortcheck(ss, haia)
 
+# Renaming 
+BTerm = rename(gettag(sortscope), Dict(:A=>:B), ATerm)
+Bsortscope = Scope([Binding{AlgType}(:B, Set([:B]), AlgType(O))]; tag=gettag(sortscope))
+BTerm_expected = AlgTerm(ident(Bsortscope;name=:B))
+@test BTerm == BTerm_expected
+
 # Subset 
 #-------
 T = ThCategory.THEORY
diff --git a/test/syntax/Scopes.jl b/test/syntax/Scopes.jl
index dfe09150..3c61b04d 100644
--- a/test/syntax/Scopes.jl
+++ b/test/syntax/Scopes.jl
@@ -5,6 +5,8 @@ using Test, GATlab
 # ScopeTags
 ###########
 
+basicprinted(x; color=false) = sprint(show, x; context=(:color=>color))
+
 tag1 = newscopetag()
 tag2 = newscopetag()
 
@@ -16,6 +18,9 @@ err = ScopeTagError(nothing, nothing)
 
 @test sprint(showerror, err) isa String
 
+@test basicprinted(tag1) != basicprinted(tag2)
+@test basicprinted(tag1; color=true) != basicprinted(tag2)
+
 # Local IDs
 ###########
 
@@ -52,6 +57,8 @@ nameless = Ident(tag1, LID(1), nothing)
 
 # References
 ############
+@test_throws ArgumentError only(Reference())
+@test basicprinted(Reference()) == "_"
 
 y = Ident(tag2, LID(1), :y)
 xdoty = Reference(x, Reference(y))
diff --git a/test/syntax/TheoryMaps.jl b/test/syntax/TheoryMaps.jl
index e832bb03..045601c8 100644
--- a/test/syntax/TheoryMaps.jl
+++ b/test/syntax/TheoryMaps.jl
@@ -57,6 +57,8 @@ end
 @test PreorderCat(Cmp) isa TermInCtx
 @test PreorderCat(argcontext(getvalue(T[Cmp]))) isa TypeScope
 
+@test_throws KeyError PreorderCat(first(typecons(T2)))
+
 xterm = fromexpr(ThMonoid.THEORY, :(x ⊣ [x]), TermInCtx)
 res = NatPlusMonoid(xterm)
 toexpr(ThNat.THEORY, res)
@@ -70,7 +72,24 @@ expected = fromexpr(ThNatPlus.THEORY, :(Z+(Z+x) ⊣ [x::ℕ]), TermInCtx)
 #############
 TLC = ThLawlessCat.THEORY
 incl = TheoryIncl(TLC, T)
+@test TheoryMaps.dom(incl) == TLC
+@test TheoryMaps.codom(incl) == T
+incl2 = TheoryIncl(ThGraph.THEORY, TLC)
+incl3 = TheoryIncl(ThGraph.THEORY, T)
+
+@test TheoryMaps.compose(incl2, incl) == incl3
+
 toexpr(incl)
 @test_throws ErrorException TheoryIncl(T, TLC)
+@test_throws ErrorException inv(incl)
+
+# Identity 
+##########
+i = IdTheoryMap(T)
+@test TheoryMaps.dom(i) == T
+@test TheoryMaps.codom(i) == T
+@test TheoryMaps.compose(i,i) == i
+@test TheoryMaps.compose(incl,i) == incl
+
 
 end # module