diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 969216db0e..21aa98a05a 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -13,8 +13,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp attribute_manager.cpp unification_hint.cpp local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp delayed_abstraction.cpp fun_info.cpp congr_lemma.cpp defeq_canonizer.cpp - mpq_macro.cpp replace_visitor_with_tc.cpp - aux_definition.cpp inverse.cpp pattern_attribute.cpp choice.cpp + replace_visitor_with_tc.cpp aux_definition.cpp inverse.cpp pattern_attribute.cpp choice.cpp locals.cpp normalize.cpp discr_tree.cpp mt_task_queue.cpp st_task_queue.cpp library_task_builder.cpp diff --git a/src/library/arith_instance.h b/src/library/arith_instance.h index fc3855c2b0..1af2f2877e 100644 --- a/src/library/arith_instance.h +++ b/src/library/arith_instance.h @@ -26,14 +26,14 @@ namespace lean { `field`, `linerar_ordered_field`. Moreover, we want to use the unbundled approach for structures such as `monoid` and `group`. - - mpq_macro (which is used only by the SMT2 frontend) + - It was also used by mpq_macro (which is used only by the SMT2 frontend) Remark: the SMT2 frontend was originally built to test the performance of a blast tactic that Leo and Daniel were developing. This tactic does not exist anymore. Moreover, SMT2 benchmarks are far from ideal for testing - a system like Lean. AFAICT, nobody uses the SMT2 frontend + a system like Lean. AFAICT, nobody uses the SMT2 frontend. + So, we have deleted `mpq_macro` and the SMT2 frontend. Motivation: less stuff to maintain. Plan: - - Delete `mpq_macro` and the SMT2 frontend. Motivation: less stuff to maintain. - Reduce the number of structures used by `norm_num`. We just need to change the lemmas used by `norm_num` and adjust the C++ code. An additional motivation diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index e6759887c2..de012646a3 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -43,7 +43,6 @@ Author: Leonardo de Moura #include "library/delayed_abstraction.h" #include "library/app_builder.h" #include "library/fun_info.h" -#include "library/mpq_macro.h" #include "library/inverse.h" #include "library/pattern_attribute.h" #include "library/comp_val.h" @@ -108,7 +107,6 @@ void initialize_library_module() { initialize_unification_hint(); initialize_type_context(); initialize_delayed_abstraction(); - initialize_mpq_macro(); initialize_inverse(); initialize_pattern_attribute(); initialize_comp_val(); @@ -128,7 +126,6 @@ void finalize_library_module() { finalize_comp_val(); finalize_pattern_attribute(); finalize_inverse(); - finalize_mpq_macro(); finalize_delayed_abstraction(); finalize_type_context(); finalize_unification_hint(); diff --git a/src/library/mpq_macro.cpp b/src/library/mpq_macro.cpp deleted file mode 100644 index 8ec2edc9c3..0000000000 --- a/src/library/mpq_macro.cpp +++ /dev/null @@ -1,115 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Daniel Selsam -*/ -#include -#include "util/sstream.h" -#include "util/hash.h" -#include "library/num.h" -#include "library/util.h" -#include "library/mpq_macro.h" -#include "library/constants.h" -#include "library/kernel_serializer.h" -#include "library/type_context.h" -#include "library/arith_instance.h" - -namespace lean { -static name * g_mpq_macro_name = nullptr; -static std::string * g_mpq_opcode = nullptr; - -class mpq_macro_definition_cell : public macro_definition_cell { - mpq m_q; - - void check_macro(expr const & m) const { - if (!is_macro(m) || macro_num_args(m) != 1) - throw exception(sstream() << "invalid 'mpq' macro, incorrect number of arguments"); - expr const & type = macro_arg(m, 0); - bool ok_type = is_nat_type(type) || is_int_type(type) || type == mk_constant(get_real_name()); - if (!ok_type) - throw exception(sstream() << "invalid 'mpq' macro, only nat, int, and real accepted"); - } - -public: - mpq_macro_definition_cell(mpq const & q): m_q(q) {} - - mpq const & get_mpq() const { return m_q; } - virtual name get_name() const { return *g_mpq_macro_name; } - virtual expr check_type(expr const & m, abstract_type_context &, bool) const { - check_macro(m); - return macro_arg(m, 0); - } - - virtual optional expand(expr const & m, abstract_type_context & actx) const { - check_macro(m); - expr type = macro_arg(m, 0); - if (has_local(type) || has_metavar(type)) - throw exception(sstream() << "trying to expand invalid 'mpq' macro"); - type_context ctx(actx.env()); - arith_instance ainst(ctx, type); - return some_expr(ainst.mk_num(m_q)); - } - - virtual void write(serializer & s) const { - s.write_string(*g_mpq_opcode); - s << m_q; - } - - virtual bool operator==(macro_definition_cell const & other) const { - if (auto other_ptr = dynamic_cast(&other)) { - return get_mpq() == other_ptr->get_mpq(); - } else { - return false; - } - } - - virtual unsigned hash() const { - return ::lean::hash(get_name().hash(), m_q.hash()); - } -}; - -expr mk_mpq_macro(mpq const & q, expr const & type) { - macro_definition m(new mpq_macro_definition_cell(q)); - return mk_macro(m, 1, &type); -} - -bool is_mpq_macro(expr const & e) { - if (is_macro(e) && dynamic_cast(macro_def(e).raw())) - return true; - else - return false; -} - -bool is_mpq_macro(expr const & e, mpq & q) { - if (is_macro(e)) { - if (auto def = dynamic_cast(macro_def(e).raw())) { - q = def->get_mpq(); - return true; - } else { - return false; - } - } else { - return false; - } -} - -void initialize_mpq_macro() { - g_mpq_macro_name = new name("mpq"); - g_mpq_opcode = new std::string("MPQ"); - register_macro_deserializer(*g_mpq_opcode, - [](deserializer & d, unsigned num, expr const * args) { - if (num != 1) - throw corrupted_stream_exception(); - mpq q; - d >> q; - return mk_mpq_macro(q, args[0]); - }); -} - -void finalize_mpq_macro() { - delete g_mpq_macro_name; - delete g_mpq_opcode; -} - -} diff --git a/src/library/mpq_macro.h b/src/library/mpq_macro.h deleted file mode 100644 index 237c20e140..0000000000 --- a/src/library/mpq_macro.h +++ /dev/null @@ -1,20 +0,0 @@ -/* -Copyright (c) 2016 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Daniel Selsam -*/ -#pragma once -#include "kernel/expr.h" -#include "util/numerics/mpq.h" - -namespace lean { - -expr mk_mpq_macro(mpq const & q, expr const & type); - -bool is_mpq_macro(expr const & e); -bool is_mpq_macro(expr const & e, mpq & q); - -void initialize_mpq_macro(); -void finalize_mpq_macro(); -}