more tests

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))

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 

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))