From 4cd4b6236ddd67129ab665988203f7db3be7506c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 6 Dec 2015 15:17:10 -0800 Subject: [PATCH] fix(library/tactic/with_options_tactic): make sure we can load the standard library containing the auxiliary macro options_expr with trust level 0 --- src/library/tactic/with_options_tactic.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/library/tactic/with_options_tactic.cpp b/src/library/tactic/with_options_tactic.cpp index 04704eebf..4e128d3b0 100644 --- a/src/library/tactic/with_options_tactic.cpp +++ b/src/library/tactic/with_options_tactic.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include "kernel/type_checker.h" +#include "library/constants.h" #include "library/kernel_serializer.h" #include "library/tactic/tactic.h" #include "library/tactic/expr_to_tactic.h" @@ -14,8 +15,6 @@ namespace lean { static name * g_options_name = 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 class options_macro_cell : public macro_definition_cell { options m_info; @@ -25,8 +24,12 @@ public: virtual void write(serializer & s) const { s << *g_options_opcode << m_info; } - virtual pair check_type(expr const &, extension_context &, bool) const { throw_ex(); } - virtual optional expand(expr const &, extension_context &) const { throw_ex(); } + virtual pair check_type(expr const &, extension_context &, bool) const { + return mk_pair(mk_constant(get_tactic_expr_name()), constraint_seq()); + } + virtual optional 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 { if (auto o = dynamic_cast(&other)) return m_info == o->m_info;