From a15fa6f022474cb8ab9a640f8196beb945799b9f Mon Sep 17 00:00:00 2001
From: Kris Brown <kris@topos.institute>
Date: Fri, 22 Sep 2023 11:12:05 -0700
Subject: [PATCH] more tests

---
 src/syntax/GATs.jl    |  7 -------
 src/syntax/Scopes.jl  |  5 +----
 test/syntax/Scopes.jl | 13 +++++++++++--
 3 files changed, 12 insertions(+), 13 deletions(-)

diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl
index 955ae0dd..328c9467 100644
--- a/src/syntax/GATs.jl
+++ b/src/syntax/GATs.jl
@@ -640,10 +640,6 @@ toexpr(c::Context, constant::Constant; kw...) =
   Expr(:(::), constant.value, toexpr(c, constant.type; kw...))
 
 
-toexpr(c::Context, term::AlgSort; kw...) = toexpr(c, term.ref; kw...)
-
-fromexpr(c::Context, e, ::Type{AlgSort}) = AlgSort(fromexpr(c, e, Ident))
-
 function bindingexprs(c::Context, s::Scope)
   c′ = AppendScope(c, s)
   [Expr(:(::), nameof(b), toexpr(c′, getvalue(b))) for b in s]
@@ -785,9 +781,6 @@ end
 toexpr(c::Context, ts::TypeScope; kw...) =
   Expr(:vect,[Expr(:(::), nameof(b), toexpr(c, getvalue(b); kw...)) for b in ts]...)
 
-toexpr(c::Context, at::Binding{AlgType, Nothing}) =
-  Expr(:(::), nameof(at), toexpr(c, getvalue(at)))
-
 function fromexpr(c::Context, e, ::Type{JudgmentBinding})
   (binding, localcontext) = @match normalize_decl(e; axiom=true) begin
     Expr(:call, :(⊣), binding, Expr(:vect, args...)) => (binding, parsetypescope(c, args))
diff --git a/src/syntax/Scopes.jl b/src/syntax/Scopes.jl
index f4348183..20a276c2 100644
--- a/src/syntax/Scopes.jl
+++ b/src/syntax/Scopes.jl
@@ -397,9 +397,6 @@ Base.:(==)(s1::Scope, s2::Scope) = s1.tag == s2.tag
 
 Base.hash(s::Scope, h::UInt64) = hash(s.tag, h)
 
-"""Compare two scopes, ignoring the difference in the top-level scope tag."""
-equiv(s1::Scope, s2::Scope) = s1.bindings == retag(Dict(s2.tag => s1.tag), s2).bindings
-
 Scope{T, Sig}() where {T, Sig} = 
   Scope{T, Sig}(newscopetag(), Binding{T, Sig}[], Dict{Symbol, Dict{Sig, LID}}())
 
@@ -855,7 +852,7 @@ hastag(hsl::HasScopeList, t::ScopeTag) =
 hasname(hsl::HasScopeList, name::Symbol) =
   haskey(getscopelist(hsl).namelookup, name)
 
-getidents(hsl::HasScopeList; kw...) = Iterators.flatten(getidents.(getscopelist(hsl)))
+getidents(hsl::HasScopeList; kw...) = vcat(getidents.(getscopelist(hsl))...)
 
 """
 Flatten a scopelist if possible. This will fail if any of the bindings shadow 
diff --git a/test/syntax/Scopes.jl b/test/syntax/Scopes.jl
index 4bf43c80..5d513c33 100644
--- a/test/syntax/Scopes.jl
+++ b/test/syntax/Scopes.jl
@@ -62,6 +62,7 @@ nameless = Ident(tag1, LID(1), nothing)
 bind_x = Binding{String}(:x, "ex")
 bind_y = Binding{String}(:y, "why")
 
+@test nameof(setname(bind_x, :z)) == :z
 @test retag(Dict(tag1 => tag2), bind_x) == bind_x
 
 @test nameof(bind_x) == :x
@@ -156,7 +157,7 @@ Scopes.unsafe_addalias!(s, :x, :X)
 @test_throws KeyError getlevel(s, tag1)
 @test getlevel(s, :x) == 1
 @test_throws KeyError getlevel(s, :elephant)
-
+@test Scopes.check_names(s)
 # Context Utilities
 ###################
 
@@ -167,6 +168,11 @@ Scopes.unsafe_addalias!(s, :x, :X)
 
 # ScopeList
 ###########
+e = ScopeList(Scope{Nothing,Nothing}[])
+@test nscopes(e) == 0 
+flat = Scopes.flatten(e)
+@test flat == Scope(Binding{Nothing,Nothing}[],tag=gettag(flat))
+@test sprint(show, e) == "[]"
 
 @test_throws Exception ScopeList([xy_scope, xy_scope])
 
@@ -184,6 +190,7 @@ xz_scope = Scope([bind_x, bind_z])
 @test valtype(xz_scope) == String
 
 c = ScopeList([xy_scope, xz_scope])
+@test_throws ErrorException Scopes.flatten(c)
 
 @test getscope(c, 1) == xy_scope
 @test getscope(c, 2) == xz_scope
@@ -206,7 +213,7 @@ c = ScopeList([xy_scope, xz_scope])
 @test_throws Exception AppendScope(ScopeList([xy_scope]), xy_scope)
 
 c = AppendScope(ScopeList([xy_scope]), xz_scope)
-
+@test length(getidents(c)) == 4
 @test getscope(c, 1) == xy_scope
 @test getscope(c, 2) == xz_scope
 @test nscopes(c) == 2
@@ -223,6 +230,8 @@ c = AppendScope(ScopeList([xy_scope]), xz_scope)
 
 # EmptyContext 
 e = EmptyContext{Nothing, Nothing}()
+@test nscopes(e) == 0
+@test !hastag(e, newscopetag())
 @test_throws BoundsError getscope(e, 1)
 @test_throws KeyError getlevel(e, :x) 
 @test_throws KeyError getlevel(e, gettag(x))