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

fix(library/choice): we should be able to store 'choice' operators in .olean files, this can happen because of notation decls

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-19 18:08:40 +01:00
parent d69db172a1
commit c1b7d7bf7e
1 changed files with 11 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/library/choice.cpp
View file

@ -7,10 +7,13 @@ Author: Leonardo de Moura
#include "util/sstream.h" #include "util/sstream.h"
#include "library/choice.h" #include "library/choice.h"
#include "library/kernel_bindings.h" #include "library/kernel_bindings.h"
#include "library/kernel_serializer.h"
namespace lean { namespace lean {
static name g_choice_name("choice"); static name g_choice_name("choice");
[[ noreturn ]] static void throw_ex() { throw exception("unexpected occurrence of 'choice' expression"); } static std::string g_choice_opcode("Choice");
[[ noreturn ]] static void throw_ex() { throw exception("unexpected occurrence of 'choice' expression");
}
// We encode a 'choice' expression using a macro. // We encode a 'choice' expression using a macro.
// This is a trick to avoid creating a new kind of expression. // This is a trick to avoid creating a new kind of expression.
@ -23,7 +26,10 @@ public:
// Choice expressions cannot be exported. They are transient/auxiliary objects. // Choice expressions cannot be exported. They are transient/auxiliary objects.
virtual expr get_type(expr const &, expr const *, extension_context &) const { throw_ex(); } 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 optional<expr> expand(expr const &, extension_context &) const { throw_ex(); }
virtual void write(serializer &) const { throw_ex(); } virtual void write(serializer & s) const {
// we should be able to write choice expressions because of notation declarations
s.write_string(g_choice_opcode);
}
}; };
static macro_definition g_choice(new choice_macro_cell()); static macro_definition g_choice(new choice_macro_cell());
@ -35,6 +41,9 @@ expr mk_choice(unsigned num_es, expr const * es) {
return mk_macro(g_choice, num_es, es); return mk_macro(g_choice, num_es, es);
} }
static register_macro_deserializer_fn
choice_macro_des_fn(g_choice_opcode, [](deserializer &, unsigned num, expr const * args) { return mk_choice(num, args); });
bool is_choice(expr const & e) { bool is_choice(expr const & e) {
return is_macro(e) && macro_def(e) == g_choice; return is_macro(e) && macro_def(e) == g_choice;
} }