clean up

src/syntax/GATs.jl

@@ -495,25 +495,11 @@ function equations(context::TypeCtx, args::AbstractVector{Ident}, theory::GAT; i
   ways_of_computing
 end
 
-function equations(theory::GAT, t::TypeInCtx)
-  error("FIXME")
-  tc = getvalue(theory[headof(t.trm)])
-  extended = ScopeList([t.ctx, Scope([Binding{AlgType, Nothing}(nothing, t.trm)])])
-  lastx = last(getidents(extended))
-  init = Dict{Ident, InferExpr}(map(zip(getidents(tc.args), t.trm.args)) do (accessor, arg)
-    hasident(t.ctx, headof(arg)) || error("Case not yet handled")
-    headof(arg) => AccessorApplication(accessor, lastx)
-  end)
-  equations(extended, Ident[], theory; init=init)
-end
-
 """Get equations for a term or type constructor"""
 equations(theory::GAT, x::Ident) = let x = getvalue(theory[x]);
   equations(x, idents(x; lid=x.args),theory) 
 end
 
-
-
 function compile(expr_lookup::Dict{Ident}, term::AlgTerm; theorymodule=nothing)
   if term.head isa Constant
     term.head.value
@@ -779,28 +765,6 @@ function parseaxiom(c::Context, localcontext, type_expr, e; name=nothing)
   end
 end
 
-"""Parse something that could either be a type or a term in context"""
-function fromexpr(c::Context, e, ::Type{InCtx}; kw...)
-  binding = @match normalize_decl(e) begin
-    Expr(:call, :(⊣), binding, _) => binding
-    otherwise => otherwise
-  end
-
-  # Determine if type or term 
-  head = @match binding begin
-    Expr(:call, f, args...) => f
-    e::Symbol => e 
-  end
-  istype = hasident(c; name=head) && getvalue(c[ident(c; name=head)]) isa AlgTypeConstructor
-
-  if istype 
-    fromexpr(c, e, TypeInCtx; kw...)
-  else 
-    fromexpr(c, e, TermInCtx; kw...)
-  end
-end
-
-
 """
 parse a term of the following forms:
   compose(f::Hom(a,b), g::Hom(b,c)) ⊣ [(a,b,c)::Ob]

test/syntax/tests.jl

@@ -23,9 +23,9 @@ end
   include("TheoryInterface.jl")
 end
 
-# @testset "TheoryMaps" begin
-#   include("TheoryMaps.jl")
-# end
+@testset "TheoryMaps" begin
+  include("TheoryMaps.jl")
+end
 
 
 end