From 3dfbd98163677967e8b614c26617c28eea1128b4 Mon Sep 17 00:00:00 2001
From: Owen Lynch <root@owenlynch.org>
Date: Tue, 19 Sep 2023 16:38:26 -0700
Subject: [PATCH] references canceled

---
 src/models/SymbolicModels.jl     |   4 +-
 src/stdlib/models/ScopeTrees.jl  | 137 -------------------------------
 src/stdlib/models/module.jl      |   2 -
 src/syntax/ExprInterop.jl        |  64 ---------------
 src/syntax/GATs.jl               |  53 ++++++------
 src/syntax/Scopes.jl             |  71 ----------------
 src/syntax/TheoryMaps.jl         |  12 +--
 test/stdlib/models/ScopeTrees.jl |  45 ----------
 test/stdlib/models/tests.jl      |   1 -
 test/syntax/ExprInterop.jl       |   6 --
 test/syntax/GATs.jl              |   2 +-
 test/syntax/Presentations.jl     |   4 +-
 test/syntax/Scopes.jl            |  26 ------
 13 files changed, 35 insertions(+), 392 deletions(-)
 delete mode 100644 src/stdlib/models/ScopeTrees.jl
 delete mode 100644 test/stdlib/models/ScopeTrees.jl

diff --git a/src/models/SymbolicModels.jl b/src/models/SymbolicModels.jl
index 359e7390..50f5db93 100644
--- a/src/models/SymbolicModels.jl
+++ b/src/models/SymbolicModels.jl
@@ -353,8 +353,8 @@ function internal_constructors(theory::GAT)::Vector{JuliaFunction}
 
     check_or_error = Expr(:(||), :(!strict), check_expr, throw_expr)
     exprs = [idents(termcon.args)..., idents(termcon.localcontext)...]
-    expr_lookup = Dict{Reference, Any}(map(exprs) do x 
-      Reference(x) => build_infer_expr(first(eqs[x]))
+    expr_lookup = Dict{Ident, Any}(map(exprs) do x 
+      x => build_infer_expr(first(eqs[x]))
     end)
 
     build = Expr(
diff --git a/src/stdlib/models/ScopeTrees.jl b/src/stdlib/models/ScopeTrees.jl
deleted file mode 100644
index 5625e170..00000000
--- a/src/stdlib/models/ScopeTrees.jl
+++ /dev/null
@@ -1,137 +0,0 @@
-module ScopeTrees
-export ScopeTree, ScopeLeaf, ScopeNode, pure, wrap, unwrap, isleaf, isnode,
-  ScopeTreeHom, ScopeTreeC
-
-using ....Syntax, ....Models, ...StdTheories
-using MLStyle
-
-using StructEquality
-
-# Scope Tree
-############
-
-@data ScopeTree{T} <: HasContext begin
-  ScopeLeaf(T)
-  ScopeNode(Scope{ScopeTree{T}, Nothing})
-end
-
-Scopes.getcontext(t::ScopeTree) = @match t begin
-  ScopeLeaf(_) => EmptyContext()
-  ScopeNode(s) => s
-end
-
-pure(x::T) where {T} = ScopeLeaf{T}(x)
-
-wrap(s::Scope{ScopeTree{T}}) where {T} = ScopeNode{T}(s)
-
-wrap(p::Pair{Symbol,<:ScopeTree{T}}...) where {T} = wrap(Scope{ScopeTree{T}}(p...))
-
-unwrap(t::ScopeTree) = @match t begin
-  ScopeLeaf(x) => x
-  ScopeNode(s) => s
-end
-
-isleaf(t::ScopeTree) = @match t begin
-  ScopeLeaf(_) => true
-  ScopeNode(_) => false
-end
-
-isnode(t::ScopeTree) = @match t begin
-  ScopeLeaf(_) => false
-  ScopeNode(_) => true
-end
-
-Base.keys(t::ScopeTree) = @match t begin
-  ScopeLeaf(_) => [Reference()]
-  ScopeNode(s) => vcat([map(r -> Reference(x, r), keys(t)) for (x,t) in identvalues(s)]...)
-end
-
-Base.haskey(t::ScopeTree, k::Reference) = @match t begin
-  ScopeLeaf(_) && if isempty(k) end => true
-  ScopeNode(s) && if !isempty(k) && hasident(s, first(k)) end => haskey(getvalue(s, first(k)), rest(k))
-  _ => false
-end
-
-Base.getindex(t::ScopeTree, k::Reference) = @match t begin
-  ScopeLeaf(x) && if isempty(k) end => x
-  ScopeNode(s) && if !isempty(k) && hasident(s, first(k)) end => getvalue(s, first(k))[rest(k)]
-  _ => throw(KeyError(k))
-end
-
-@struct_hash_equal struct ScopeTreeHom{S}
-  map::Dict{Reference, Tuple{Reference, S}}
-end
-
-function ScopeTreeHom(pairs::Pair{Reference, Tuple{Reference, S}}...) where {S}
-  ScopeTreeHom{S}(Dict{Reference, Tuple{Reference, S}}(pairs...))
-end
-
-@struct_hash_equal struct ScopeTreeC{ObT, HomT, C<:Model{Tuple{ObT, HomT}}} <: Model{Tuple{ScopeTree{ObT}, ScopeTreeHom{HomT}}}
-  c::C
-end
-
-using .ThCategory
-
-function seteq(x, y)
-  (x ⊆ y) && (y ⊆ x)
-end
-
-@instance ThCategory{ScopeTree{ObT}, ScopeTreeHom{HomT}} (;model::ScopeTreeC{ObT, HomT, C}) where {ObT, HomT, C} begin
-  function Ob(t::ScopeTree{ObT})
-    @match t begin
-      ScopeLeaf(x) => try
-        Ob(x; model=model.c)
-      catch e
-        @fail ("leaf failed", e)
-      end
-      ScopeNode(s) => begin
-        for (x, t′) in identvalues(s)
-          try
-            Ob(t′; model)
-          catch e
-            @fail ("branch $x failed", e)
-          end
-        end
-      end
-    end
-    t
-  end
-
-  function Hom(f::ScopeTreeHom{HomT}, x::ScopeTree{ObT}, y::ScopeTree{ObT})
-    # TODO: report exactly which key was not in
-    seteq(keys(f.map), keys(x)) || @fail "keys of morphism not equal to keys of domain"
-    seteq(first.(values(f.map)), keys(y)) || @fail "values of morphism not equal to keys of codomain"
-    for (i, (j, f₀)) in f.map
-      try
-        Hom(f₀, x[i], y[j]; model=model.c)
-      catch e
-        @fail ("morphism at $i not valid", e)
-      end
-    end
-    f
-  end
-
-  id(x::ScopeTree{ObT}) = ScopeTreeHom{HomT}(Dict(k => (k, id(x[k]; model=model.c)) for k in keys(x)))
-
-  function compose(f::ScopeTreeHom{HomT}, g::ScopeTreeHom{HomT}; context)
-    if !isnothing(context)
-      [:a,:b,:c] ⊂ keys(context) || error("must provide full context or nothing")
-    end
-
-    ScopeTreeHom{HomT}(
-      Dict{Reference, Tuple{Reference, HomT}}(k => begin
-        (k′, f₀) = f.map[k]
-        (k″, g₀) = g.map[k′]
-        localcontext = if !isnothing(context)
-          (a=context.a[k], b=context.b[k′], c=context.c[k″])
-        else
-          nothing
-        end
-        (k″, compose(f₀, g₀; context=localcontext, model=model.c))
-      end
-      for k in keys(f.map))
-    )
-  end
-end
-
-end
diff --git a/src/stdlib/models/module.jl b/src/stdlib/models/module.jl
index 1a5f992f..b7613e4e 100644
--- a/src/stdlib/models/module.jl
+++ b/src/stdlib/models/module.jl
@@ -6,14 +6,12 @@ include("FinSets.jl")
 include("FinMatrices.jl")
 include("SliceCategories.jl")
 include("Nothings.jl")
-include("ScopeTrees.jl")
 include("GATs.jl")
 
 @reexport using .FinSets
 @reexport using .FinMatrices
 @reexport using .SliceCategories
 @reexport using .Nothings
-@reexport using .ScopeTrees
 @reexport using .GATs
 
 end
diff --git a/src/syntax/ExprInterop.jl b/src/syntax/ExprInterop.jl
index 15a4db6c..de6b0417 100644
--- a/src/syntax/ExprInterop.jl
+++ b/src/syntax/ExprInterop.jl
@@ -69,68 +69,4 @@ function fromexpr(c::Context, e, ::Type{Ident}; sig=nothing)
   end
 end
 
-function reftolist(c::Context, ref::Reference; kw...)
-  symbols = []
-  while !isempty(ref)
-    x = first(ref)
-    push!(symbols, toexpr(c, x; kw...))
-    ref = rest(ref)
-    if !isempty(ref)
-      c = getvalue(c, x)
-    end
-  end
-  symbols
-end
-
-function toexpr(c::Context, ref::Reference; kw...)
-  symbols = reftolist(c, ref; kw...)
-  if isempty(symbols)
-    :(_)
-  else
-    expr = symbols[1]
-    for x in symbols[2:end]
-      expr = Expr(:(.), expr, QuoteNode(x))
-    end
-    expr
-  end
-end
-
-function flattendotexpr(e)
-  syms = Symbol[]
-  while !(e isa Symbol)
-    @match e begin
-      Expr(:(.), e′, QuoteNode(y)) => begin
-        push!(syms, y)
-        e = e′
-      end
-      _ => error("unexpected syntax for reference: $e")
-    end
-  end
-  @match e begin
-    :(_) => nothing
-    x::Symbol => push!(syms, x)
-  end
-  reverse(syms)
-end
-
-function reffromlist(c::Context, syms::AbstractVector{Symbol}; sig=nothing)
-  if isempty(syms)
-    Reference()
-  else
-    x = fromexpr(c, syms[1], Ident; sig)
-    c′ = getvalue(c, x)
-    r = if c′ isa Context
-      reffromlist(c′, @view syms[2:end])
-    else
-      length(syms) == 1 || error("the value of $x is not a context: $(c′)")
-      Reference()
-    end
-    Reference(x, r)
-  end
-end
-
-function fromexpr(c::Context, e, ::Type{Reference}; sig=nothing)
-  reffromlist(c, flattendotexpr(e); sig)
-end
-
 end # module
diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl
index d56c4ccc..25450d59 100644
--- a/src/syntax/GATs.jl
+++ b/src/syntax/GATs.jl
@@ -33,17 +33,15 @@ One syntax tree to rule all the terms.
 Head can be a reference to an AlgTermConstructor, to a Binding{AlgType, Nothing}, or simply an AbstractConstant
 """
 @struct_hash_equal struct AlgTerm <: TrmTyp
-  head::Union{Reference, AbstractConstant}
+  head::Union{Ident, AbstractConstant}
   args::Vector{AlgTerm}
-  function AlgTerm(head::Union{Reference, AbstractConstant}, args::Vector{AlgTerm}=EMPTY_ARGS)
+  function AlgTerm(head::Union{Ident, AbstractConstant}, args::Vector{AlgTerm}=EMPTY_ARGS)
     new(head, args)
   end
 end
 
 const EMPTY_ARGS = AlgTerm[]
 
-AlgTerm(head::Ident, args::Vector{AlgTerm}=EMPTY_ARGS) = AlgTerm(Reference(head), args)
-
 """
 Some expr may have already been bound (e.g. by an explicit context) and thus 
 oughtn't be interpreted as `default` type.
@@ -54,22 +52,22 @@ function ExprInterop.fromexpr(c::Context, e, ::Type{AlgTerm}; bound=nothing)
     s::Symbol => begin
       scope = getscope(c, getlevel(c, s))
       ref = if sigtype(scope) == Union{Nothing, AlgSorts}
-        fromexpr(c, s, Reference; sig=AlgSort[])
+        fromexpr(c, s, Ident; sig=AlgSort[])
       else
-        fromexpr(c, s, Reference)
+        fromexpr(c, s, Ident)
       end
       AlgTerm(ref)
     end
     Expr(:call, head, argexprs...) => begin
       args = Vector{AlgTerm}(fromexpr.(Ref(c), argexprs, Ref(AlgTerm)))
       argsorts = AlgSorts(AlgSort.(Ref(c), args))
-      AlgTerm(fromexpr(c, head, Reference; sig=argsorts), args)
+      AlgTerm(fromexpr(c, head, Ident; sig=argsorts), args)
     end
     Expr(:(::), val, type) => 
       AlgTerm(Constant(val, get(bound, val, fromexpr(c, type, AlgType; bound=bound))))
     e::Expr => error("could not parse AlgTerm from $e")
     constant::Constant => AlgTerm(constant)
-    i::Ident => AlgTerm(Reference(i))
+    i::Ident => AlgTerm(i)
   end
 end
 
@@ -81,15 +79,13 @@ One syntax tree to rule all the types.
 `head` must be reference to a `AlgTypeConstructor`
 """
 @struct_hash_equal struct AlgType <: TrmTyp
-  head::Reference
+  head::Ident
   args::Vector{AlgTerm}
-  function AlgType(head::Reference, args::Vector{AlgTerm}=EMPTY_ARGS)
+  function AlgType(head::Ident, args::Vector{AlgTerm}=EMPTY_ARGS)
     new(head, args)
   end
 end
 
-AlgType(head::Ident, args::Vector{AlgTerm}=EMPTY_ARGS) = AlgType(Reference(head), args)
-
 """
 Some expr may have already been bound (e.g. by an explicit context) and thus 
 oughtn't be interpreted as `default` type.
@@ -97,9 +93,9 @@ oughtn't be interpreted as `default` type.
 function ExprInterop.fromexpr(c::Context, e, ::Type{AlgType}; bound=nothing)::AlgType
   bound = isnothing(bound) ? Dict{Symbol, AlgType}() : bound
   @match e begin
-    s::Symbol => AlgType(fromexpr(c, s, Reference))
+    s::Symbol => AlgType(fromexpr(c, s, Ident))
     Expr(:call, head, args...) =>
-      AlgType(fromexpr(c, head, Reference), fromexpr.(Ref(c), args, Ref(AlgTerm); bound=bound))
+      AlgType(fromexpr(c, head, Ident), fromexpr.(Ref(c), args, Ref(AlgTerm); bound=bound))
     _ => error("could not parse AlgType from $e")
   end
 end
@@ -139,17 +135,16 @@ A *sort*, which is essentially a type constructor without arguments
 `ref` must be reference to a `AlgTypeConstructor`
 """
 @struct_hash_equal struct AlgSort
-  ref::Reference
+  ref::Ident
 end
 
-AlgSort(i::Ident) = AlgSort(Reference(i))
 AlgSort(t::AlgType) = AlgSort(t.head)
 
 function AlgSort(c::Context, t::AlgTerm)
   if t.head isa AbstractConstant
     AlgSort(t.head.type.head)
   else
-    binding = c[only(t.head)]
+    binding = c[t.head]
     value = getvalue(binding)
     if value isa AlgType
       AlgSort(value.head)
@@ -197,7 +192,7 @@ Throw an error if a the head of an AlgTerm (which refers to a term constructor)
 has arguments of the wrong sort. Returns the sort of the term.
 """
 function sortcheck(ctx::Context, t::AlgTerm)::AlgSort
-  if t.head isa Reference
+  if t.head isa Ident
     judgment = ctx[t.head] |> getvalue
     if judgment isa AlgType
       isempty(t.args) || error("Cannot apply a variable to arguments: $t")
@@ -394,7 +389,7 @@ function allnames(theory::GAT; aliases=false)
 end
 
 function sortname(theory::GAT, type::AlgType)
-  canonicalize(theory, only(type.head))
+  canonicalize(theory, type.head)
 end
 
 Base.issubset(t1::GAT, t2::GAT) = 
@@ -467,12 +462,12 @@ function equations(args::TypeScope, localcontext::TypeScope, theory::GAT)
     for (i, arg) in enumerate(xtype.args)
       if arg.head isa Constant
         continue
-      elseif first(arg.head) ∈ theory
+      elseif arg.head ∈ theory
         continue
       else
-        @assert first(arg.head) ∈ context
+        @assert arg.head ∈ context
         a = ident(xtypecon.args; lid=LID(i))
-        y = first(arg.head)
+        y = arg.head
         expr′ = AccessorApplication(a, expr)
         push!(to_expand, y => expr′)
       end
@@ -486,14 +481,14 @@ equations(theory::GAT, x::Ident) = let x = getvalue(theory[x]);
   equations(x.args, x.localcontext, theory) 
 end
 
-function compile(expr_lookup::Dict{Reference}, term::AlgTerm; theorymodule=nothing)
+function compile(expr_lookup::Dict{Ident}, term::AlgTerm; theorymodule=nothing)
   if term.head isa Constant
     term.head.value
   else
     if haskey(expr_lookup, term.head)
       expr_lookup[term.head]
     else
-      name = nameof(only(term.head))
+      name = nameof(term.head)
       fun = if !isnothing(theorymodule)
         :($theorymodule.$name)
       else
@@ -509,7 +504,7 @@ function TermInCtx(g::GAT, k::Ident)
   tcon = getvalue(g[k])
   lc = argcontext(tcon)
   ids = reverse(reverse(idents(lc))[1:(length(tcon.args))])
-  TermInCtx(lc, AlgTerm(Reference(k), AlgTerm.(ids)))
+  TermInCtx(lc, AlgTerm(k, AlgTerm.(ids)))
 end
 
 """
@@ -534,7 +529,7 @@ we use `equations` which tell us, e.g., that `a = dom(f)`. So we can grab the
 first argument of the *type* of `f` (i.e. grab `x` from `Hom(x,x)`). 
 """
 function infer_type(theory::GAT, t::TermInCtx)
-  head = only(headof(t.trm))
+  head = headof(t.trm)
   if hasident(t.ctx, head) 
     getvalue(t.ctx[head]) # base case
   else
@@ -566,7 +561,7 @@ Take a term constructor and determine terms of its local context.
 This function is mutually recursive with `infer_type`. 
 """ 
 function bind_localctx(theory::GAT, t::TermInCtx)
-  head = only(headof(t.trm))
+  head = headof(t.trm)
 
   tc = getvalue(theory[head])
   eqs = equations(theory, head)
@@ -591,7 +586,7 @@ end
 
 """ Replace idents with AlgTerms. """
 function substitute_term(t::TrmTyp, dic::Dict{Ident,AlgTerm})
-  iden = only(headof(t))
+  iden = headof(t)
   if haskey(dic, iden)
     isempty(t.args) || error("Cannot substitute a term with arguments")
     dic[iden]
@@ -623,7 +618,7 @@ ExprInterop.toexpr(c::Context, term::AlgSort; kw...) =
   ExprInterop.toexpr(c, term.ref; kw...)
 
 ExprInterop.fromexpr(c::Context, e, ::Type{AlgSort}) = 
-  AlgSort(ExprInterop.fromexpr(c, e, Reference))
+  AlgSort(ExprInterop.fromexpr(c, e, Ident))
 
 
 function bindingexprs(c::Context, s::Scope)
diff --git a/src/syntax/Scopes.jl b/src/syntax/Scopes.jl
index 55e7891d..a4cb9fea 100644
--- a/src/syntax/Scopes.jl
+++ b/src/syntax/Scopes.jl
@@ -4,7 +4,6 @@ export
   ScopeTagError,
   LID,
   Ident, gettag, getlid, isnamed,
-  Reference, rest,
   Binding, getaliases, getvalue, getsignature, getline, setline,
   Context, getscope, nscopes, getlevel, hasname, hastag,
   HasContext, getcontext,
@@ -171,75 +170,6 @@ rename(tag::ScopeTag, replacements::Dict{Symbol, Symbol}, x::Ident) =
     x
   end
 
-# References
-############
-
-"""
-`Reference`
-
-A path of identifiers. We optimize for the (frequent) case where there is only
-one identifier by making this a linked list.
-"""
-@struct_hash_equal struct Reference
-  body::Union{Nothing, Tuple{Ident, Reference}}
-end
-
-function Reference(xs::Ident...)
-  if isempty(xs)
-    Reference(nothing)
-  else
-    Reference(xs[1], Reference(xs[2:end]...))
-  end
-end
-
-function Reference(first::Ident, rest::Reference)
-  Reference((first, rest))
-end
-
-Base.isempty(p::Reference) = isnothing(p.body)
-
-Base.first(p::Reference) = !isempty(p) ? p.body[1] : throw(BoundsError(p, 1))
-
-Base.rest(p::Reference) = !isempty(p) ? p.body[2] : p
-
-function Base.only(p::Reference)
-  if isempty(p)
-    throw(ArgumentError("Reference is empty, must contain exactly 1 element"))
-  end
-  (x, r) = p.body
-  if !isempty(r)
-    throw(ArgumentError("Reference has multiple elements, must contain exactly 1 element"))
-  end
-  x
-end
-
-function Base.show(io::IO, p::Reference)
-  if isempty(p)
-    print(io, "_")
-    return
-  end
-  cur = p
-  show(io, first(cur))
-  while !isempty(rest(cur))
-    cur = rest(cur)
-    id = first(cur)
-    if isnamed(id)
-      print(io, ".")
-      show(io, id)
-    else
-      print(io, "[")
-      print(io, getlid(id))
-      print(io, "]")
-    end
-  end
-end
-
-retag(replacements::Dict{ScopeTag, ScopeTag}, p::Reference) =
-  isempty(p) ? p : Reference(retag(replacements, first(p)), retag(replacements, rest(p)))
-
-rename(tag::ScopeTag, replacements::Dict{Symbol, Symbol}, p::Reference) =
-  isempty(p) ? p : Reference(rename(tag, replacements, first(p)), rename(tag, replacements, rest(p)))
-
 # Bindings
 ##########
 
@@ -758,7 +688,6 @@ function idents(
 end
 
 Base.getindex(c::Context, x::Ident) = getbinding(getscope(c, x), x)
-Base.getindex(c::Context, x::Reference) = c[only(x)]
 
 getvalue(c::Context, x::Ident) = getvalue(c[x])
 getvalue(c::Context, name::Symbol) = getvalue(c[ident(c; name)])
diff --git a/src/syntax/TheoryMaps.jl b/src/syntax/TheoryMaps.jl
index 131d5d70..544c1b84 100644
--- a/src/syntax/TheoryMaps.jl
+++ b/src/syntax/TheoryMaps.jl
@@ -40,7 +40,7 @@ dom(f::AbsTheoryMap)::GAT = f.dom # assume this exists by default
 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)))
+  typmap = Dict(k => typemap(g)[v.ref] for (k,v) in pairs(typemap(f)))
   trmmap = Dict(k => g(v) for (k, v) in pairs(termmap(f)))
   TheoryMap(dom(f), codom(g), typmap, trmmap)
 end
@@ -63,8 +63,8 @@ function (f::AbsTheoryMap)(ctx::TypeScope)
   scope = TypeScope()
   cache = Dict{Symbol, AlgTerm}()
   for b in ctx
-    argnames = nameof.(only.(headof.(b.value.args)))
-    val = AlgType(f(only(b.value.head)).ref, AlgTerm[cache[a] for a in argnames])
+    argnames = nameof.(headof.(b.value.args))
+    val = AlgType(f(b.value.head).ref, AlgTerm[cache[a] for a in argnames])
     new_binding = Binding{AlgType, Nothing}(b.primary, b.aliases, val, b.sig)
     cache[nameof(b)] = AlgTerm(Ident(gettag(scope), LID(length(scope)+1), 
                                nameof(new_binding)))
@@ -81,7 +81,7 @@ end
 """ Map a term `t` in context `c` along `f`. """
 function (f::AbsTheoryMap)(ctx::TypeScope, t::AlgTerm, fctx=nothing)::AlgTerm
   fctx = isnothing(fctx) ? f(ctx) : fctx
-  head = only(headof(t))
+  head = headof(t)
   if hasident(ctx, head)
     retag(Dict(gettag(ctx)=>gettag(fctx)), t) # term is already in the context
   else 
@@ -182,7 +182,7 @@ TODO: check that it is well-formed, axioms are preserved.
     # Check type constructors are coherent
     for (k, v) in pairs(typmap)
       f_args = f(argcontext(getvalue(dom[k])))
-      arg_fs = argcontext(getvalue(codom[only(v.ref)]))
+      arg_fs = argcontext(getvalue(codom[v.ref]))
       err = "Bad type map $k => $v ($f_args != $arg_fs)"
       Scopes.equiv(f_args, arg_fs) || error(err)
     end
@@ -223,7 +223,7 @@ function fromexpr(dom::GAT, codom::GAT, e, ::Type{TheoryMap})
       key = fromexpr(dom, e1, TermInCtx)
 
       # Check that dom ctx is the same (modulo retagging) with term argcontext
-      khead = only(key.trm.head)
+      khead = key.trm.head
       a_c = argcontext(getvalue(dom[khead]))
       Scopes.equiv(key.ctx, a_c) || error("CONTEXT ERROR\n$(key.ctx)\n$a_c")
 
diff --git a/test/stdlib/models/ScopeTrees.jl b/test/stdlib/models/ScopeTrees.jl
deleted file mode 100644
index 4e2c0b81..00000000
--- a/test/stdlib/models/ScopeTrees.jl
+++ /dev/null
@@ -1,45 +0,0 @@
-module TestScopeTrees
-
-using Test, GATlab
-
-t = wrap(
-  :a => pure(1),
-  :b => wrap(:x => pure(2), :y => pure(1)),
-  :c => wrap(:f => wrap(:g => pure(4)))
-)
-
-r = fromexpr(t, :(c.f.g), Reference)
-
-@test toexpr(t, r) == :(c.f.g)
-
-@test isnode(t)
-@test unwrap(t) isa Scope
-@test isleaf(getvalue(t, :a))
-@test unwrap(getvalue(t, :a)) == 1
-@test nameof.(first.(keys(t))) == [:a, :b, :b, :c]
-@test keys(t)[3] == fromexpr(t, :(b.y), Reference)
-@test haskey(t, r)
-@test t[r] == 4
-@test_throws KeyError t[fromexpr(t, :(c.f), Reference)]
-@test_throws KeyError t[fromexpr(t, :(_), Reference)]
-
-using .ThCategory
-
-t1 = wrap(:a => pure(1), :b => pure(1), :c => pure(2))
-t2 = wrap(:x => wrap(:p => pure(3), :q => pure(2)), :y => pure(7))
-a, b, c = fromexpr.(Ref(t1), [:a, :b, :c], Ref(Reference))
-xp, xq, y = fromexpr.(Ref(t2), [:(x.p), :(x.q), :y], Ref(Reference))
-f = ScopeTreeHom(a => (y, [6]), b => (xp, [2]), c => (xq, [2,2]))
-id_t1 = ScopeTreeHom(a => (a, [1]), b => (b, [1]), c => (c, [1,2]))
-
-@withmodel ScopeTreeC(FinSetC()) (Ob, Hom, compose, id) begin
-  @test Ob(t) == t
-  @test_throws TypeCheckFail Ob(wrap(:x => pure(-1)))
-  @test Hom(f, t1, t2) == f
-  @test_throws TypeCheckFail Hom(f, t1, t1)
-  @test_throws TypeCheckFail Hom(ScopeTreeHom(a => (a, [2]), b => (b, [1]), c => (c, [1,2])), t1, t2)
-  @test id(t1) == id_t1
-  @test compose(id(t1), f) == f
-end
-
-end
diff --git a/test/stdlib/models/tests.jl b/test/stdlib/models/tests.jl
index eff8aa21..6e7e807a 100644
--- a/test/stdlib/models/tests.jl
+++ b/test/stdlib/models/tests.jl
@@ -4,7 +4,6 @@ include("FinSets.jl")
 include("FinMatrices.jl")
 include("SliceCategories.jl")
 include("Nothings.jl")
-include("ScopeTrees.jl")
 include("GATs.jl")
 
 end
diff --git a/test/syntax/ExprInterop.jl b/test/syntax/ExprInterop.jl
index a71466ee..706ed4cf 100644
--- a/test/syntax/ExprInterop.jl
+++ b/test/syntax/ExprInterop.jl
@@ -27,10 +27,4 @@ c = ScopeList([scope, scope′])
 @test fromexpr(c, :(var"#1!1"), Ident) == x
 @test fromexpr(c, :(var"#1"), Ident) == x′
 
-@test toexpr(c, Reference(x)) == :x!1
-@test fromexpr(c, :x!1, Reference) == Reference(x)
-
-@test toexpr(c, Reference()) == :(_)
-@test fromexpr(c, :(_), Reference) == Reference()
-
 end
diff --git a/test/syntax/GATs.jl b/test/syntax/GATs.jl
index 610c0126..e374ecc8 100644
--- a/test/syntax/GATs.jl
+++ b/test/syntax/GATs.jl
@@ -11,7 +11,7 @@ end
 
 scope = Scope(:number, :(+), :(*))
 
-number, plus, times = Reference.(idents(scope; name=[:number, :(+), :(*)]))
+number, plus, times = idents(scope; name=[:number, :(+), :(*)])
 
 one = AlgTerm(Constant(1, AlgType(number)))
 
diff --git a/test/syntax/Presentations.jl b/test/syntax/Presentations.jl
index 12a6b9db..678adb9b 100644
--- a/test/syntax/Presentations.jl
+++ b/test/syntax/Presentations.jl
@@ -40,7 +40,7 @@ end
 src, tgt = idents(SchGraph; name=[:src, :tgt])
 Hom = ident(SchGraph; name=:Hom)
 
-@test getvalue(SchGraph[src]).head == Reference(Hom)
+@test getvalue(SchGraph[src]).head == Hom
 
 @present Z(ThGroup) begin
   (a,)
@@ -49,7 +49,7 @@ end
 t = fromexpr(Z, :(i(a) ⋅ (2::default)), AlgTerm)
 a = ident(Z; name=:a)
 
-@test compile(Dict(Reference(a) => :a), t; theorymodule=ThGroup) == :($(ThGroup).:(⋅)($(ThGroup).i(a), 2))
+@test compile(Dict(a => :a), t; theorymodule=ThGroup) == :($(ThGroup).:(⋅)($(ThGroup).i(a), 2))
 
 @present D₄(ThGroup) begin
   (r,f) :: default
diff --git a/test/syntax/Scopes.jl b/test/syntax/Scopes.jl
index 3c61b04d..6e751cc6 100644
--- a/test/syntax/Scopes.jl
+++ b/test/syntax/Scopes.jl
@@ -55,32 +55,6 @@ nameless = Ident(tag1, LID(1), nothing)
 @test gettag(retag(Dict(tag1 => tag2), x)) == tag2
 @test nameof(rename(tag1, Dict(:x => :y), x)) == :y
 
-# References
-############
-@test_throws ArgumentError only(Reference())
-@test basicprinted(Reference()) == "_"
-
-y = Ident(tag2, LID(1), :y)
-xdoty = Reference(x, Reference(y))
-@test xdoty == Reference(x,y)
-
-@test first(xdoty) == x
-@test rest(xdoty) == Reference(y)
-@test_throws ArgumentError only(xdoty)
-@test only(Reference(x)) == x
-
-@test basicprinted(xdoty) == "x.y"
-
-xsub1 = Reference(x, nameless)
-
-@test basicprinted(xsub1) == "x[1]"
-
-@test gettag(first(retag(Dict(tag1 => tag2), xdoty))) == tag2
-@test gettag(first(retag(Dict(tag2 => tag2), xdoty))) == tag1
-@test gettag(first(rest(retag(Dict(tag2 => tag1), xdoty)))) == tag1
-@test basicprinted(rename(tag1, Dict(:x => :y, :y => :z), xdoty)) == "y.y"
-@test basicprinted(rename(tag2, Dict(:x => :y, :y => :z), xdoty)) == "x.z"
-
 # Bindings
 ##########