chore(library): remove legacy_type_context

src/frontends/lean/builtin_cmds.cpp

@@ -27,7 +27,6 @@ Author: Leonardo de Moura
 #include "library/aux_recursors.h"
 #include "library/private.h"
 #include "library/type_context.h"
-#include "library/legacy_type_context.h"
 #include "library/reducible.h"
 #include "library/typed_expr.h"
 #include "library/vm/vm.h"
@@ -205,7 +204,7 @@ environment eval_cmd(parser & p) {
         p.display_information_pos(p.cmd_pos());
         p.ios().get_regular_stream() << "eval result:\n";
     }
-    legacy_type_context tc(p.env(), p.get_options());
+    type_context tc(p.env(), p.get_options());
     auto out = regular(p.env(), p.ios(), tc);
     out << r << endl;
     return p.env();

src/frontends/lean/parser.cpp

@@ -45,7 +45,7 @@ Author: Leonardo de Moura
 #include "library/noncomputable.h"
 #include "library/error_handling.h"
 #include "library/scope_pos_info_provider.h"
-#include "library/legacy_type_context.h"
+#include "library/type_context.h"
 #include "library/equations_compiler/equations.h"
 #include "library/pattern_attribute.h"
 #include "frontends/lean/tokens.h"
@@ -336,7 +336,7 @@ void parser::updt_options() {
 }
 
 void parser::display_warning_pos(unsigned line, unsigned pos) {
-    legacy_type_context tc(env(), get_options());
+    type_context tc(env(), get_options());
     auto out = regular(env(), ios(), tc);
     ::lean::display_warning_pos(out, get_stream_name().c_str(), line, pos);
 }
@@ -362,7 +362,7 @@ void parser::display_error(char const * msg, unsigned line, unsigned pos) {
 void parser::display_error(char const * msg, pos_info p) { display_error(msg, p.first, p.second); }
 
 void parser::display_error(throwable const & ex) {
-    legacy_type_context tc(env(), get_options());
+    type_context tc(env(), get_options());
     auto out = regular(env(), ios(), tc);
     ::lean::display_error(out, this, ex);
 }
@@ -2081,10 +2081,10 @@ expr parser::parse_tactic(unsigned) {
 class lazy_type_context : public abstract_type_context {
     environment const & m_env;
     options const & m_opts;
-    std::unique_ptr<legacy_type_context> m_ctx;
-    legacy_type_context & ctx() {
+    std::unique_ptr<type_context> m_ctx;
+    type_context & ctx() {
         if (!m_ctx)
-            m_ctx.reset(new legacy_type_context(m_env, m_opts));
+            m_ctx.reset(new type_context(m_env, m_opts));
         return *m_ctx;
     }
 public:

src/frontends/lean/print_cmd.cpp

@@ -22,7 +22,7 @@ Author: Leonardo de Moura
 #include "library/attribute_manager.h"
 #include "library/user_recursors.h"
 #include "library/noncomputable.h"
-#include "library/legacy_type_context.h"
+#include "library/type_context.h"
 #include "library/unification_hint.h"
 #include "library/reducible.h"
 #include "library/rfl_lemmas.h"
@@ -76,14 +76,14 @@ static environment print_axioms(parser & p) {
     if (p.curr_is_identifier()) {
         name c = p.check_constant_next("invalid 'print axioms', constant expected");
         environment new_env = p.reveal_all_theorems();
-        legacy_type_context tc(new_env, p.get_options());
+        type_context tc(new_env, p.get_options());
         auto out = regular(new_env, p.ios(), tc);
         print_axioms_deps(p.env(), out)(c);
         return new_env;
     } else {
         bool has_axioms = false;
         environment const & env = p.env();
-        legacy_type_context tc(env, p.get_options());
+        type_context tc(env, p.get_options());
         auto out = regular(env, p.ios(), tc);
         env.for_each_declaration([&](declaration const & d) {
                 name const & n = d.get_name();
@@ -102,7 +102,7 @@ static void print_prefix(parser & p) {
     name prefix = p.check_id_next("invalid 'print prefix' command, identifier expected");
     environment const & env = p.env();
     buffer<declaration> to_print;
-    legacy_type_context tc(env, p.get_options());
+    type_context tc(env, p.get_options());
     auto out = regular(env, p.ios(), tc);
     env.for_each_declaration([&](declaration const & d) {
             if (is_prefix_of(prefix, d.get_name())) {
@@ -123,7 +123,7 @@ static void print_fields(parser const & p, name const & S, pos_info const & pos)
         throw parser_error(sstream() << "invalid 'print fields' command, '" << S << "' is not a structure", pos);
     buffer<name> field_names;
     get_structure_fields(env, S, field_names);
-    legacy_type_context tc(env, p.get_options());
+    type_context tc(env, p.get_options());
     auto out = regular(env, p.ios(), tc);
     for (name const & field_name : field_names) {
         declaration d = env.get(field_name);
@@ -153,7 +153,7 @@ static bool print_parse_table(parser const & p, parse_table const & t, bool nud,
     os = os.update(get_pp_notation_name(), false);
     os = os.update(get_pp_preterm_name(), true);
     ios.set_options(os);
-    legacy_type_context tc(p.env(), p.get_options());
+    type_context tc(p.env(), p.get_options());
     io_state_stream out = regular(p.env(), ios, tc);
     optional<token_table> tt(get_token_table(p.env()));
     t.for_each([&](unsigned num, notation::transition const * ts, list<notation::accepting> const & overloads) {
@@ -193,7 +193,7 @@ static void print_patterns(parser & p, name const & n) {
                 options opts         = p.get_options();
                 opts                 = opts.update_if_undef(get_pp_metavar_args_name(), true);
                 io_state new_ios(p.ios(), opts);
-                legacy_type_context tc(p.env(), opts);
+                type_context tc(p.env(), opts);
                 io_state_stream out = regular(p.env(), new_ios, tc);
                 out << "(multi-)patterns:\n";
                 if (!is_nil(hi.m_mvars)) {
@@ -234,7 +234,7 @@ static void print_definition(parser const & p, name const & n, pos_info const &
     options opts        = p.get_options();
     opts                = opts.update_if_undef(get_pp_beta_name(), false);
     io_state ios(p.ios(), opts);
-    legacy_type_context tc(env, opts);
+    type_context tc(env, opts);
     io_state_stream out = regular(env, ios, tc);
     if (d.is_axiom())
         throw parser_error(sstream() << "invalid 'print definition', theorem '" << to_user_name(env, n)

src/library/CMakeLists.txt

@@ -19,6 +19,6 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
 
   # Legacy -- The following files will be eventually deleted
   normalize.cpp justification.cpp constraint.cpp metavar.cpp
-  old_type_context.cpp legacy_type_context.cpp old_type_checker.cpp old_converter.cpp old_default_converter.cpp
+  old_type_context.cpp old_type_checker.cpp old_converter.cpp old_default_converter.cpp
   old_util.cpp
   )

src/library/init_module.cpp

@@ -57,7 +57,6 @@ Author: Leonardo de Moura
 #include "library/old_default_converter.h"
 #include "library/old_type_checker.h"
 #include "library/old_type_context.h"
-#include "library/legacy_type_context.h"
 
 
 namespace lean {
@@ -114,7 +113,6 @@ void initialize_library_module() {
     initialize_noncomputable();
     initialize_aux_recursors();
     initialize_old_type_context();
-    initialize_legacy_type_context();
     initialize_app_builder();
     // initialize_light_rule_set();
     // initialize_congr_lemma_manager();
@@ -142,7 +140,6 @@ void finalize_library_module() {
     // finalize_congr_lemma_manager();
     // finalize_light_rule_set();
     finalize_app_builder();
-    finalize_legacy_type_context();
     finalize_old_type_context();
     finalize_aux_recursors();
     finalize_noncomputable();

src/library/legacy_type_context.cpp

@@ -1,116 +0,0 @@
-/*
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "library/legacy_type_context.h"
-#include "library/reducible.h"
-
-namespace lean {
-static name * g_tmp_prefix                   = nullptr;
-legacy_type_context::legacy_type_context(environment const & env, options const & o,
-                                         list<expr> const & insts, bool multiple_instances):
-    old_type_context(env, o, multiple_instances),
-    m_not_reducible_pred(mk_not_reducible_pred(env)) {
-    m_ignore_if_zero = false;
-    m_next_uvar_idx  = 0;
-    m_next_mvar_idx  = 0;
-    set_local_instances(insts);
-}
-
-legacy_type_context::~legacy_type_context() {}
-
-bool legacy_type_context::is_uvar(level const & l) const {
-    if (!is_meta(l))
-        return false;
-    name const & n = meta_id(l);
-    return !n.is_atomic() && n.get_prefix() == *g_tmp_prefix;
-}
-
-bool legacy_type_context::is_mvar(expr const & e) const {
-    if (!is_metavar(e))
-        return false;
-    name const & n = mlocal_name(e);
-    return !n.is_atomic() && n.get_prefix() == *g_tmp_prefix;
-}
-
-unsigned legacy_type_context::uvar_idx(level const & l) const {
-    lean_assert(is_uvar(l));
-    return meta_id(l).get_numeral();
-}
-
-unsigned legacy_type_context::mvar_idx(expr const & m) const {
-    lean_assert(is_mvar(m));
-    return mlocal_name(m).get_numeral();
-}
-
-optional<level> legacy_type_context::get_assignment(level const & u) const {
-    if (auto v = m_assignment.m_uassignment.find(uvar_idx(u)))
-        return some_level(*v);
-    else
-        return none_level();
-}
-
-optional<expr> legacy_type_context::get_assignment(expr const & m) const {
-    if (auto v = m_assignment.m_eassignment.find(mvar_idx(m)))
-        return some_expr(*v);
-    else
-        return none_expr();
-}
-
-void legacy_type_context::update_assignment(level const & u, level const & v) {
-    m_assignment.m_uassignment.insert(uvar_idx(u), v);
-}
-
-void legacy_type_context::update_assignment(expr const & m, expr const & v) {
-    m_assignment.m_eassignment.insert(mvar_idx(m), v);
-}
-
-level legacy_type_context::mk_uvar() {
-    unsigned idx = m_next_uvar_idx;
-    m_next_uvar_idx++;
-    return mk_meta_univ(name(*g_tmp_prefix, idx));
-}
-
-expr legacy_type_context::mk_mvar(expr const & type) {
-    unsigned idx = m_next_mvar_idx;
-    m_next_mvar_idx++;
-    return mk_metavar(name(*g_tmp_prefix, idx), type);
-}
-
-optional<expr> legacy_type_context::mk_subsingleton_instance(expr const & type) {
-    flet<bool> set(m_ignore_if_zero, true);
-    return old_type_context::mk_subsingleton_instance(type);
-}
-
-bool legacy_type_context::ignore_universe_def_eq(level const & l1, level const & l2) const {
-    if (is_meta(l1) || is_meta(l2)) {
-        // The unifier may invoke this module before universe metavariables in the class
-        // have been instantiated. So, we just ignore and assume they will be solved by
-        // the unifier.
-
-        // See comment at m_ignore_if_zero declaration.
-        if (m_ignore_if_zero && (is_zero(l1) || is_zero(l2)))
-            return false;
-        return true; // we ignore
-    } else {
-        return false;
-    }
-}
-
-bool legacy_type_context::validate_assignment_types(expr const &, expr const &) {
-    // We disable this check because the interface between type_context and the elaborator unifier
-    // is currently quite brittle.
-    // Recall that this class is used to implement the type class inference in the Lean frontend.
-    return true;
-}
-
-void initialize_legacy_type_context() {
-    g_tmp_prefix      = new name(name::mk_internal_unique_name());
-}
-
-void finalize_legacy_type_context() {
-    delete g_tmp_prefix;
-}
-}

src/library/legacy_type_context.h

@@ -1,81 +0,0 @@
-/*
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include <vector>
-#include "library/old_type_context.h"
-
-namespace lean {
-
-/** \brief (Legacy) implementation for the generic type_context class.
-    It implements a simple meta-variable assignment.
-
-    We use this class to implement the interface with the (old) elaborator. */
-class legacy_type_context : public old_type_context {
-    typedef rb_map<unsigned, level, unsigned_cmp> uassignment;
-    typedef rb_map<unsigned, expr,  unsigned_cmp> eassignment;
-    name_predicate            m_not_reducible_pred;
-
-    struct assignment {
-        uassignment m_uassignment;
-        eassignment m_eassignment;
-    };
-    assignment                m_assignment;
-    std::vector<assignment>   m_trail;
-    unsigned                  m_next_uvar_idx;
-    unsigned                  m_next_mvar_idx;
-
-   /** \brief When m_ignore_if_zero is true, the following type-class resolution problem fails
-       Given (A : Type{?u}), where ?u is a universe meta-variable created by an external module,
-
-       ?Inst : subsingleton.{?u} A := subsingleton_prop ?M
-
-       This case generates the unification problem
-
-       subsingleton.{?u} A =?= subsingleton.{0} ?M
-
-       which can be solved by assigning (?u := 0) and (?M := A)
-       when the hack is enabled, the is_def_eq method in the type class module fails at the subproblem:
-
-           ?u =?= 0
-
-       That is, when the hack is on, type-class resolution cannot succeed by instantiating an external universe
-       meta-variable with 0.
-   */
-    bool                      m_ignore_if_zero;
-
-    unsigned uvar_idx(level const & l) const;
-    unsigned mvar_idx(expr const & m) const;
-
-public:
-    legacy_type_context(environment const & env, options const & o,
-                           list<expr> const & insts = list<expr>(), bool multiple_instances = false);
-    virtual ~legacy_type_context();
-    virtual bool is_extra_opaque(name const & n) const { return m_not_reducible_pred(n); }
-    virtual bool ignore_universe_def_eq(level const & l1, level const & l2) const;
-    virtual bool is_uvar(level const & l) const;
-    virtual bool is_mvar(expr const & e) const;
-    virtual optional<level> get_assignment(level const & u) const;
-    virtual optional<expr> get_assignment(expr const & m) const;
-    virtual void update_assignment(level const & u, level const & v);
-    virtual void update_assignment(expr const & m, expr const & v);
-    virtual level mk_uvar();
-    virtual expr mk_mvar(expr const &);
-    virtual expr infer_local(expr const & e) const { return mlocal_type(e); }
-    virtual expr infer_metavar(expr const & e) const { return mlocal_type(e); }
-    virtual void push_core() { m_trail.push_back(m_assignment); }
-    virtual void pop_core() { lean_assert(!m_trail.empty()); m_assignment = m_trail.back(); m_trail.pop_back(); }
-    virtual unsigned get_num_check_points() const { return m_trail.size(); }
-    virtual void commit() { lean_assert(!m_trail.empty()); m_trail.pop_back(); }
-    virtual optional<expr> mk_subsingleton_instance(expr const & type);
-    virtual bool validate_assignment_types(expr const & m, expr const & v);
-    // TODO(REMOVE)
-    bool & get_ignore_if_zero() { return m_ignore_if_zero; }
-};
-
-void initialize_legacy_type_context();
-void finalize_legacy_type_context();
-}

src/shell/emscripten.cpp

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #include <string>
 #include "library/module.h"
 #include "library/standard_kernel.h"
-#include "library/legacy_type_context.h"
+#include "library/type_context.h"
 #include "library/error_handling.h"
 #include "frontends/lean/pp.h"
 #include "frontends/lean/parser.h"
@@ -37,7 +37,7 @@ public:
             env = import_modules(env, base, 1, &mod, num_threads, keep_proofs, ios);
         } catch (lean::exception & ex) {
             simple_pos_info_provider pp("import_module");
-            legacy_type_context tc(env, ios.get_options());
+            type_context tc(env, ios.get_options());
             auto out = diagnostic(env, ios, tc);
             lean::display_error(out, &pp, ex);
             return 1;
@@ -56,7 +56,7 @@ public:
         } catch (lean::exception & ex) {
             simple_pos_info_provider pp(input_filename.c_str());
             ok = false;
-            legacy_type_context tc(env, ios.get_options());
+            type_context tc(env, ios.get_options());
             auto out = diagnostic(env, ios, tc);
             lean::display_error(out, &pp, ex);
         }

src/shell/lean.cpp

@@ -29,7 +29,7 @@ Author: Leonardo de Moura
 #include "library/hott_kernel.h"
 #include "library/module.h"
 #include "library/flycheck.h"
-#include "library/legacy_type_context.h"
+#include "library/type_context.h"
 #include "library/io_state_stream.h"
 #include "library/definition_cache.h"
 #include "library/declaration_index.h"
@@ -65,7 +65,7 @@ using lean::module_name;
 using lean::simple_pos_info_provider;
 using lean::shared_file_lock;
 using lean::exclusive_file_lock;
-using lean::legacy_type_context;
+using lean::type_context;
 using lean::type_checker;
 
 enum class input_kind { Unspecified, Lean, HLean, Trace };
@@ -418,7 +418,7 @@ int main(int argc, char ** argv) {
                 ok = ::lean::smt2::parse_commands(env, ios, argv[i]);
             } catch (lean::exception & ex) {
                 ok = false;
-                legacy_type_context tc(env, ios.get_options());
+                type_context tc(env, ios.get_options());
                 auto out = diagnostic(env, ios, tc);
                 simple_pos_info_provider pp(argv[i]);
                 lean::display_error(out, &pp, ex);
@@ -516,7 +516,7 @@ int main(int argc, char ** argv) {
             } catch (lean::exception & ex) {
                 simple_pos_info_provider pp(argv[i]);
                 ok = false;
-                legacy_type_context tc(env, ios.get_options());
+                type_context tc(env, ios.get_options());
                 auto out = diagnostic(env, ios, tc);
                 lean::display_error(out, &pp, ex);
             }
@@ -551,7 +551,7 @@ int main(int argc, char ** argv) {
         }
         return ok ? 0 : 1;
     } catch (lean::throwable & ex) {
-        legacy_type_context tc(env, ios.get_options());
+        type_context tc(env, ios.get_options());
         auto out = diagnostic(env, ios, tc);
         lean::display_error(out, nullptr, ex);
     } catch (std::bad_alloc & ex) {