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

fix(library/tactic/with_options_tactic): make sure we can load the standard library containing the auxiliary macro options_expr with trust level 0

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-06 15:17:10 -08:00
parent b044f9e8c1
commit 4cd4b6236d
1 changed files with 7 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/library/tactic/with_options_tactic.cpp
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/ */
#include <string> #include <string>
#include "kernel/type_checker.h" #include "kernel/type_checker.h"
#include "library/constants.h"
#include "library/kernel_serializer.h" #include "library/kernel_serializer.h"
#include "library/tactic/tactic.h" #include "library/tactic/tactic.h"
#include "library/tactic/expr_to_tactic.h" #include "library/tactic/expr_to_tactic.h"
@ -14,8 +15,6 @@ namespace lean {
static name * g_options_name = nullptr; static name * g_options_name = nullptr;
static std::string * g_options_opcode = nullptr; static std::string * g_options_opcode = nullptr;
[[ noreturn ]] static void throw_ex() { throw exception("unexpected occurrence of 'options' expression"); }
// Auxiliary macro for wrapping a options object as an expression // Auxiliary macro for wrapping a options object as an expression
class options_macro_cell : public macro_definition_cell { class options_macro_cell : public macro_definition_cell {
options m_info; options m_info;
@ -25,8 +24,12 @@ public:
virtual void write(serializer & s) const { virtual void write(serializer & s) const {
s << *g_options_opcode << m_info; s << *g_options_opcode << m_info;
} }
virtual pair<expr, constraint_seq> check_type(expr const &, extension_context &, bool) const { throw_ex(); } virtual pair<expr, constraint_seq> check_type(expr const &, extension_context &, bool) const {
virtual optional<expr> expand(expr const &, extension_context &) const { throw_ex(); } return mk_pair(mk_constant(get_tactic_expr_name()), constraint_seq());
}
virtual optional<expr> expand(expr const &, extension_context &) const {
return some_expr(mk_constant(get_tactic_expr_builtin_name()));
}
virtual bool operator==(macro_definition_cell const & other) const { virtual bool operator==(macro_definition_cell const & other) const {
if (auto o = dynamic_cast<options_macro_cell const *>(&other)) if (auto o = dynamic_cast<options_macro_cell const *>(&other))
return m_info == o->m_info; return m_info == o->m_info;