diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 71afce44b2..7a9a950112 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/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(); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 42cd625035..77fafadc3b 100644 --- a/src/frontends/lean/parser.cpp +++ b/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 m_ctx; - legacy_type_context & ctx() { + std::unique_ptr 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: diff --git a/src/frontends/lean/print_cmd.cpp b/src/frontends/lean/print_cmd.cpp index cc1299d85d..ffc4fa222c 100644 --- a/src/frontends/lean/print_cmd.cpp +++ b/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 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 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 tt(get_token_table(p.env())); t.for_each([&](unsigned num, notation::transition const * ts, list 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) diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index af83288d68..87b20e93ce 100644 --- a/src/library/CMakeLists.txt +++ b/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 ) diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index ead761a740..328ea8cbd1 100644 --- a/src/library/init_module.cpp +++ b/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(); diff --git a/src/library/legacy_type_context.cpp b/src/library/legacy_type_context.cpp deleted file mode 100644 index 1805d9cc58..0000000000 --- a/src/library/legacy_type_context.cpp +++ /dev/null @@ -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 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 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 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 legacy_type_context::mk_subsingleton_instance(expr const & type) { - flet 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; -} -} diff --git a/src/library/legacy_type_context.h b/src/library/legacy_type_context.h deleted file mode 100644 index b4376c58bd..0000000000 --- a/src/library/legacy_type_context.h +++ /dev/null @@ -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 -#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 uassignment; - typedef rb_map eassignment; - name_predicate m_not_reducible_pred; - - struct assignment { - uassignment m_uassignment; - eassignment m_eassignment; - }; - assignment m_assignment; - std::vector 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 const & insts = list(), 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 get_assignment(level const & u) const; - virtual optional 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 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(); -} diff --git a/src/shell/emscripten.cpp b/src/shell/emscripten.cpp index 086ae2ddad..9bb03b622c 100644 --- a/src/shell/emscripten.cpp +++ b/src/shell/emscripten.cpp @@ -7,7 +7,7 @@ Author: Leonardo de Moura #include #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); } diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index c27af0960f..de51a966a7 100644 --- a/src/shell/lean.cpp +++ b/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) {