diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl index 2f3dd28b..99af1747 100644 --- a/src/syntax/GATs.jl +++ b/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] diff --git a/test/syntax/tests.jl b/test/syntax/tests.jl index 6918ba32..47033529 100644 --- a/test/syntax/tests.jl +++ b/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