michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

test(lua): coercion module error messages

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-25 10:01:04 -07:00
parent ef14c3d67e
commit 71b555ab15
2 changed files with 26 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/coercion.cpp
View file

@ -298,9 +298,9 @@ environment add_coercion(environment const & env, name const & f, name const & C
expr fn = mk_constant(f, const_levels(C_fn)); expr fn = mk_constant(f, const_levels(C_fn));
optional<coercion_class> cls = type_to_coercion_class(binding_body(t)); optional<coercion_class> cls = type_to_coercion_class(binding_body(t));
if (!cls) if (!cls)
throw exception(sstream() << "invalid coercion, '" << f << "' does not have the expected type to be used as a coercion"); throw exception(sstream() << "invalid coercion, '" << f << "' cannot be used as a coercion from '" << C << "'");
else if (cls->kind() == coercion_class_kind::User && cls->get_name() == C) else if (cls->kind() == coercion_class_kind::User && cls->get_name() == C)
throw exception(sstream() << "invalid coercion, '" << f << "' is a coercion from '" << C << "' on itself"); throw exception(sstream() << "invalid coercion, '" << f << "' is a coercion from '" << C << "' to itself");
return add_coercion(env, C, fn, d.get_type(), d.get_params(), num, *cls, ios); return add_coercion(env, C, fn, d.get_type(), d.get_params(), num, *cls, ios);
} }
t = binding_body(t); t = binding_body(t);
@ -317,7 +317,7 @@ environment add_coercion(environment const & env, name const & f, io_state const
t = binding_body(t); t = binding_body(t);
expr C = get_app_fn(binding_domain(t)); expr C = get_app_fn(binding_domain(t));
if (!is_constant(C)) if (!is_constant(C))
throw exception(sstream() << "invalid coercion, '" << f << "' does not have the expected type to be used as a coercion"); throw exception(sstream() << "invalid coercion, '" << f << "' cannot be used as a coercion");
return add_coercion(env, f, const_name(C), ios); return add_coercion(env, f, const_name(C), ios);
} }

23
tests/lua/coe4.lua Normal file
View file

@ -0,0 +1,23 @@
local env = environment()
local l = param_univ("l")
local Ul = mk_sort(l)
local lst_l = Const("lst", {l})
local A = Local("A", Ul)
env = add_decl(env, mk_var_decl("lst", {l}, mk_arrow(Ul, Ul)))
env = add_decl(env, mk_var_decl("lst2lst", {l}, Pi(A, mk_arrow(lst_l(A), lst_l(A)))))
env = add_decl(env, mk_var_decl("head", {l}, Pi(A, mk_arrow(lst_l(A), A))))
env = add_decl(env, mk_var_decl("id", {l}, Pi(A, mk_arrow(A, A))))
function add_bad_coercion(env, c)
ok, msg = pcall(function() add_coercion(env, c) end)
assert(not ok)
print("Expected error: " .. tostring(msg:what()))
end
function add_bad_coercion2(env, c, cls)
ok, msg = pcall(function() add_coercion(env, c, cls) end)
assert(not ok)
print("Expected error: " .. tostring(msg:what()))
end
add_bad_coercion(env, "lst2lst")
add_bad_coercion(env, "head")
add_bad_coercion(env, "id")
add_bad_coercion2(env, "head", "lst")