Skip to content

Commit

Permalink
more coverage for algclosure
Browse files Browse the repository at this point in the history
  • Loading branch information
olynch committed Jul 3, 2024
1 parent e4d5c4d commit 7e81a46
Show file tree
Hide file tree
Showing 3 changed files with 17 additions and 4 deletions.
3 changes: 2 additions & 1 deletion src/syntax/GATs.jl
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
6 changes: 4 additions & 2 deletions src/syntax/gats/closures.jl
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
12 changes: 11 additions & 1 deletion test/syntax/GATs.jl
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -165,6 +167,14 @@ 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

0 comments on commit 7e81a46

Please sign in to comment.