From 2c0f596665454d2c9035731b9ab9174001eef216 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 Jun 2014 12:14:38 -0700 Subject: [PATCH] fix(library/choice): avoid assertion violation when Lua API is misused Signed-off-by: Leonardo de Moura --- src/library/choice.cpp | 8 +++++--- tests/lua/choice2.lua | 6 ++++++ 2 files changed, 11 insertions(+), 3 deletions(-) create mode 100644 tests/lua/choice2.lua diff --git a/src/library/choice.cpp b/src/library/choice.cpp index 9128ad600..7c15af453 100644 --- a/src/library/choice.cpp +++ b/src/library/choice.cpp @@ -10,6 +10,8 @@ Author: Leonardo de Moura namespace lean { static name g_choice_name("choice"); +[[ noreturn ]] static void throw_ex() { throw exception("unexpected occurrence of 'choice' expression"); } + // We encode a 'choice' expression using a macro. // This is a trick to avoid creating a new kind of expression. // 'Choice' expressions are temporary objects used by the elaborator, @@ -19,9 +21,9 @@ public: virtual name get_name() const { return g_choice_name; } // Choice expressions must be replaced with metavariables before invoking the type checker. // Choice expressions cannot be exported. They are transient/auxiliary objects. - virtual expr get_type(expr const &, expr const *, extension_context &) const { lean_unreachable(); } - virtual optional expand(expr const &, extension_context &) const { lean_unreachable(); } - virtual void write(serializer &) const { lean_unreachable(); } + virtual expr get_type(expr const &, expr const *, extension_context &) const { throw_ex(); } + virtual optional expand(expr const &, extension_context &) const { throw_ex(); } + virtual void write(serializer &) const { throw_ex(); } }; static macro_definition g_choice(new choice_macro_cell()); diff --git a/tests/lua/choice2.lua b/tests/lua/choice2.lua new file mode 100644 index 000000000..332e4ced9 --- /dev/null +++ b/tests/lua/choice2.lua @@ -0,0 +1,6 @@ +local a = Local("a", Bool) +local b = Local("b", Bool) +local c = mk_choice(a, b) +print(c) +local env = environment() +check_error(function() env:infer_type(c) end)