chore(library/mpq_macro): delete mpq_macro

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

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

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();

src/library/mpq_macro.cpp

@@ -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 <string>
-#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<expr> 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<mpq_macro_definition_cell const *>(&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<mpq_macro_definition_cell const *>(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<mpq_macro_definition_cell const *>(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;
-}
-
-}

src/library/mpq_macro.h

@@ -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();
-}