diff --git a/src/syntax/GATs.jl b/src/syntax/GATs.jl index c05bb34..25447be 100644 --- a/src/syntax/GATs.jl +++ b/src/syntax/GATs.jl @@ -9,7 +9,8 @@ export Constant, AlgTerm, AlgType, AlgAST, termcons,typecons, accessors, structs, primitive_sorts, struct_sorts, equations, build_infer_expr, compile, sortcheck, allnames, sorts, sortname, InCtx, TermInCtx, TypeInCtx, headof, argsof, methodof, bodyof, argcontext, - infer_type + infer_type, + tcompose using ..Scopes import ..ExprInterop: fromexpr, toexpr diff --git a/src/syntax/gats/closures.jl b/src/syntax/gats/closures.jl index 366cc40..bf30076 100644 --- a/src/syntax/gats/closures.jl +++ b/src/syntax/gats/closures.jl @@ -115,8 +115,10 @@ function tcompose(fs::Dtry{AlgClosure}, argnames::Vector{Symbol}) end function (f::AlgClosure)(argvals::Any...) - if length(f.methods) > 1 && any(!(x isa AlgTerm) for x in argvals) - error("cannot infer type of non-AlgTerm value $x") + for x in argvals + if !(x isa AlgTerm) + error("cannot infer type of non-AlgTerm value $x") + end end sorts = AlgSort[sortcheck.(Ref(f.theory), argvals)...] if !haskey(f.methods, sorts) diff --git a/test/syntax/GATs.jl b/test/syntax/GATs.jl index 00b930b..c2479f7 100644 --- a/test/syntax/GATs.jl +++ b/test/syntax/GATs.jl @@ -157,6 +157,8 @@ end id_span(x) := Span(x, id(x),id(x)) ⊣ [x::Ob] end +@test Base.isempty(GAT(:_EMPTY)) + # Dtrys tuplescope = fromexpr(ThMonoid.Meta.theory, :([x::(a::(s,t),b)]), TypeScope) @@ -165,6 +167,13 @@ tuplescope = fromexpr(ThMonoid.Meta.theory, :([x::(a::(s,t),b)]), TypeScope) x * y + x * x end -@test Base.isempty(GAT(:_EMPTY)) +@test only(f.methods)[2](1, 2) isa AlgTerm +@test_throws ErrorException f(1, 2) +@test_throws ErrorException f() + +@test sprint(show, f) isa String + +@test tcompose(Dtrys.node(:a => Dtrys.leaf(f), :b => Dtrys.leaf(f)), [:x, :y]) + isa AlgClosure end # module