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

fix(library/choice): avoid assertion violation when Lua API is misused

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-24 12:14:38 -07:00
parent 3169f8c126
commit 2c0f596665
2 changed files with 11 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/choice.cpp
View file

@ -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<expr> 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<expr> expand(expr const &, extension_context &) const { throw_ex(); }
virtual void write(serializer &) const { throw_ex(); }
};
static macro_definition g_choice(new choice_macro_cell());

6
tests/lua/choice2.lua Normal file
View file

@ -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)