feat(frontends/lean): add 'migrate' command

library/data/nat/order.lean

@@ -165,92 +165,38 @@ section
     mul_le_mul_of_nonneg_right := (take a b c H1 H2, mul_le_mul_right H1 c),
     mul_lt_mul_of_pos_left     := @mul_lt_mul_of_pos_left,
     mul_lt_mul_of_pos_right    := @mul_lt_mul_of_pos_right ⦄
+
+  migrate from algebra with nat
+    replacing has_le.ge → ge, has_lt.gt → gt
+    hiding pos_of_mul_pos_left, pos_of_mul_pos_right, lt_of_mul_lt_mul_left, lt_of_mul_lt_mul_right
 end
 
+calc_trans ge_of_eq_of_ge
+calc_trans ge_of_ge_of_eq
+calc_trans gt_of_eq_of_gt
+calc_trans gt_of_gt_of_eq
+
 section port_algebra
-  theorem ge_of_eq_of_ge : ∀{a b c : ℕ}, a = b → b ≥ c → a ≥ c := @algebra.ge_of_eq_of_ge _ _
-  theorem ge_of_ge_of_eq : ∀{a b c : ℕ}, a ≥ b → b = c → a ≥ c := @algebra.ge_of_ge_of_eq _ _
-  theorem gt_of_eq_of_gt : ∀{a b c : ℕ}, a = b → b > c → a > c := @algebra.gt_of_eq_of_gt _ _
-  theorem gt_of_gt_of_eq : ∀{a b c : ℕ}, a > b → b = c → a > c := @algebra.gt_of_gt_of_eq _ _
-  theorem ge.trans: ∀{a b c : ℕ}, a ≥ b → b ≥ c → a ≥ c := @algebra.ge.trans _ _
-  theorem gt.trans: ∀{a b c : ℕ}, a ≥ b → b ≥ c → a ≥ c := @algebra.ge.trans _ _
-  theorem gt_of_gt_of_ge : ∀{a b c : ℕ}, a > b → b ≥ c → a > c := @algebra.gt_of_gt_of_ge _ _
-  theorem gt_of_ge_of_gt : ∀{a b c : ℕ}, a ≥ b → b > c → a > c := @algebra.gt_of_ge_of_gt _ _
-  calc_trans ge_of_eq_of_ge
-  calc_trans ge_of_ge_of_eq
-  calc_trans gt_of_eq_of_gt
-  calc_trans gt_of_gt_of_eq
-
-  theorem ne_of_lt : ∀{a b : ℕ}, a < b → a ≠ b := @algebra.ne_of_lt _ _
-  theorem lt_of_le_of_ne : ∀{a b : ℕ}, a ≤ b → a ≠ b → a < b :=
-    @algebra.lt_of_le_of_ne _ _
-
-  theorem not_le_of_lt : ∀{a b : ℕ}, a < b → ¬ b ≤ a := @algebra.not_le_of_lt _ _
-  theorem not_lt_of_le : ∀{a b : ℕ}, a ≤ b → ¬ b < a := @algebra.not_lt_of_le _ _
-
-  theorem le_of_not_lt : ∀{a b : ℕ}, ¬ a < b → b ≤ a := @algebra.le_of_not_lt _ _
-  theorem lt_of_not_le : ∀{a b : ℕ}, ¬ a ≤ b → b < a := @algebra.lt_of_not_le _ _
-  theorem lt_or_ge : ∀a b : ℕ, a < b ∨ a ≥ b := @algebra.lt_or_ge _ _
-  theorem le_or_gt : ∀a b : ℕ, a ≤ b ∨ a > b := @algebra.le_or_gt _ _
-  theorem lt_or_gt_of_ne : ∀{a b : ℕ}, a ≠ b → a < b ∨ a > b := @algebra.lt_or_gt_of_ne _ _
-
-  theorem add_le_add : ∀{a b c d : ℕ}, a ≤ b → c ≤ d → a + c ≤ b + d := @algebra.add_le_add _ _
-  theorem add_lt_add : ∀{a b c d : ℕ}, a < b → c < d → a + c < b + d := @algebra.add_lt_add _ _
-  theorem add_lt_add_of_le_of_lt : ∀{a b c d : ℕ}, a ≤ b → c < d → a + c < b + d :=
-    @algebra.add_lt_add_of_le_of_lt _ _
-  theorem add_lt_add_of_lt_of_le : ∀{a b c d : ℕ}, a < b → c ≤ d → a + c < b + d :=
-    @algebra.add_lt_add_of_lt_of_le _ _
-  theorem lt_add_of_pos_left : ∀{a b : ℕ}, b > 0 → a < b + a := @algebra.lt_add_of_pos_left _ _
-
-  theorem le_of_add_le_add_right : ∀{a b c : ℕ}, a + b ≤ c + b → a ≤ c :=
-    @algebra.le_of_add_le_add_right _ _
-  theorem lt_of_add_lt_add_left : ∀{a b c : ℕ}, a + b < a + c → b < c :=
-    @algebra.lt_of_add_lt_add_left _ _
-  theorem lt_of_add_lt_add_right : ∀{a b c : ℕ}, a + b < c + b → a < c :=
-    @algebra.lt_of_add_lt_add_right _ _
-  theorem add_le_add_left_iff : ∀a b c : ℕ, a + b ≤ a + c ↔ b ≤ c := algebra.add_le_add_left_iff
-  theorem add_le_add_right_iff : ∀a b c : ℕ, a + b ≤ c + b ↔ a ≤ c := algebra.add_le_add_right_iff
-  theorem add_lt_add_left_iff : ∀a b c : ℕ, a + b < a + c ↔ b < c := algebra.add_lt_add_left_iff
-  theorem add_lt_add_right_iff : ∀a b c : ℕ, a + b < c + b ↔ a < c := algebra.add_lt_add_right_iff
-
   theorem add_pos_left : ∀{a : ℕ}, 0 < a → ∀b : ℕ, 0 < a + b :=
     take a H b, @algebra.add_pos_of_pos_of_nonneg _ _ a b H !zero_le
   theorem add_pos_right : ∀{a : ℕ}, 0 < a → ∀b : ℕ, 0 < b + a :=
     take a H b, !add.comm ▸ add_pos_left H b
-
   theorem add_eq_zero_iff_eq_zero_and_eq_zero : ∀{a b : ℕ},
     a + b = 0 ↔ a = 0 ∧ b = 0 :=
     take a b : ℕ,
       @algebra.add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg _ _ a b !zero_le !zero_le
-
   theorem le_add_of_le_left : ∀{a b c : ℕ}, b ≤ c → b ≤ a + c :=
     take a b c H, @algebra.le_add_of_nonneg_of_le _ _ a b c !zero_le H
   theorem le_add_of_le_right : ∀{a b c : ℕ}, b ≤ c → b ≤ c + a :=
     take a b c H, @algebra.le_add_of_le_of_nonneg _ _ a b c H !zero_le
-  theorem lt_add_of_pos_of_le : ∀{a b c : ℕ}, 0 < a → b ≤ c → b < a + c :=
-    @algebra.lt_add_of_pos_of_le _ _
-  theorem lt_add_of_le_of_pos : ∀{a b c : ℕ}, b ≤ c → 0 < a → b < c + a :=
-    @algebra.lt_add_of_le_of_pos _ _
-
   theorem lt_add_of_lt_left : ∀{b c : ℕ}, b < c → ∀a, b < a + c :=
     take b c H a, @algebra.lt_add_of_nonneg_of_lt _ _ a b c !zero_le H
   theorem lt_add_of_lt_right : ∀{b c : ℕ}, b < c → ∀a, b < c + a :=
     take b c H a, @algebra.lt_add_of_lt_of_nonneg _ _ a b c H !zero_le
-  theorem lt_add_of_pos_of_lt : ∀{a b c : ℕ}, 0 < a → b < c → b < a + c :=
-    @algebra.lt_add_of_pos_of_lt _ _
-  theorem lt_add_of_lt_of_pos : ∀{a b c : ℕ}, b < c → 0 < a → b < c + a :=
-    @algebra.lt_add_of_lt_of_pos _ _
-
-  theorem mul_pos : ∀{a b : ℕ}, 0 < a → 0 < b → 0 < a * b := @algebra.mul_pos _ _
-
   theorem lt_of_mul_lt_mul_left : ∀{a b c : ℕ}, c * a < c * b → a < b :=
     take a b c H, @algebra.lt_of_mul_lt_mul_left _ _ a b c H !zero_le
   theorem lt_of_mul_lt_mul_right : ∀{a b c : ℕ}, a * c < b * c → a < b :=
     take a b c H, @algebra.lt_of_mul_lt_mul_right _ _ a b c H !zero_le
-  theorem le_of_mul_le_mul_left : ∀{a b c : ℕ}, c * a ≤ c * b → c > 0 → a ≤ b :=
-    @algebra.le_of_mul_le_mul_left _ _
-  theorem le_of_mul_le_mul_right : ∀{a b c : ℕ}, a * c ≤ b * c → c > 0 → a ≤ b :=
-    @algebra.le_of_mul_le_mul_right _ _
   theorem pos_of_mul_pos_left : ∀{a b : ℕ}, 0 < a * b → 0 < b :=
     take a b H, @algebra.pos_of_mul_pos_left _ _ a b H !zero_le
   theorem pos_of_mul_pos_right : ∀{a b : ℕ}, 0 < a * b → 0 < a :=

src/emacs/lean-syntax.el

@@ -18,7 +18,7 @@
     "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"
     "using" "namespace" "section" "fields" "find_decl"
     "attribute" "local" "set_option" "add_rewrite" "extends" "include" "omit" "classes"
-    "instances" "coercions" "metaclasses" "raw")
+    "instances" "coercions" "metaclasses" "raw" "migrate" "replacing")
   "lean keywords")
 
 (defconst lean-syntax-table

src/frontends/lean/CMakeLists.txt

@@ -8,6 +8,6 @@ structure_cmd.cpp info_manager.cpp info_annotation.cpp find_cmd.cpp
 coercion_elaborator.cpp info_tactic.cpp
 init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp
 parse_tactic_location.cpp parse_rewrite_tactic.cpp
-type_util.cpp elaborator_exception.cpp)
+type_util.cpp elaborator_exception.cpp migrate_cmd.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/builtin_cmds.cpp

@@ -33,6 +33,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/notation_cmd.h"
 #include "frontends/lean/inductive_cmd.h"
 #include "frontends/lean/structure_cmd.h"
+#include "frontends/lean/migrate_cmd.h"
 #include "frontends/lean/find_cmd.h"
 #include "frontends/lean/begin_end_ext.h"
 #include "frontends/lean/decl_cmds.h"
@@ -701,6 +702,7 @@ void init_cmd_table(cmd_table & r) {
     register_decl_cmds(r);
     register_inductive_cmd(r);
     register_structure_cmd(r);
+    register_migrate_cmd(r);
     register_notation_cmds(r);
     register_calc_cmds(r);
     register_begin_end_cmds(r);

src/frontends/lean/init_module.cpp

@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/builtin_exprs.h"
 #include "frontends/lean/inductive_cmd.h"
 #include "frontends/lean/structure_cmd.h"
+#include "frontends/lean/migrate_cmd.h"
 #include "frontends/lean/info_manager.h"
 #include "frontends/lean/parse_table.h"
 #include "frontends/lean/token_table.h"
@@ -45,6 +46,7 @@ void initialize_frontend_lean_module() {
     initialize_begin_end_ext();
     initialize_inductive_cmd();
     initialize_structure_cmd();
+    initialize_migrate_cmd();
     initialize_info_manager();
     initialize_info_tactic();
     initialize_pp();
@@ -59,6 +61,7 @@ void finalize_frontend_lean_module() {
     finalize_pp();
     finalize_info_tactic();
     finalize_info_manager();
+    finalize_migrate_cmd();
     finalize_structure_cmd();
     finalize_inductive_cmd();
     finalize_begin_end_ext();

src/frontends/lean/migrate_cmd.cpp

@@ -0,0 +1,445 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/sexpr/option_declarations.h"
+#include "kernel/abstract.h"
+#include "kernel/instantiate.h"
+#include "library/reducible.h"
+#include "library/scoped_ext.h"
+#include "library/normalize.h"
+#include "library/explicit.h"
+#include "library/projection.h"
+#include "library/aliases.h"
+#include "library/coercion.h"
+#include "library/class.h"
+#include "library/locals.h"
+#include "library/placeholder.h"
+#include "library/util.h"
+#include "library/occurs.h"
+#include "library/module.h"
+#include "library/constants.h"
+#include "library/replace_visitor.h"
+#include "library/error_handling/error_handling.h"
+#include "frontends/lean/parser.h"
+#include "frontends/lean/util.h"
+#include "frontends/lean/decl_cmds.h"
+#include "frontends/lean/tokens.h"
+
+#ifndef LEAN_DEFAULT_MIGRATE_TRACE
+#define LEAN_DEFAULT_MIGRATE_TRACE false
+#endif
+
+namespace lean {
+static name * g_migrate_trace  = nullptr;
+
+bool get_migrate_trace(options const & o) { return o.get_bool(*g_migrate_trace, LEAN_DEFAULT_MIGRATE_TRACE); }
+
+/** \brief Converter used by the migrate command. It treat
+    definitions from a given set of namespaces as opaque.
+*/
+class migrate_converter : public unfold_semireducible_converter {
+    list<name> m_namespaces;
+public:
+    migrate_converter(environment const & env, list<name> const & ns):
+        unfold_semireducible_converter(env, true, true),
+        m_namespaces(ns) {
+    }
+
+    virtual bool is_opaque(declaration const & d) const {
+        name const & n = d.get_name();
+        if (!is_instance(m_env, n) &&
+            std::any_of(m_namespaces.begin(), m_namespaces.end(), [&](name const & ns) {
+                    return is_prefix_of(ns, n);
+                }))
+            return true;
+        return default_converter::is_opaque(d);
+    }
+};
+
+struct migrate_cmd_fn {
+    parser &                 m_p;
+    environment              m_env;
+    name_generator           m_ngen;
+    bool                     m_trace;
+
+    type_checker_ptr         m_tc;
+    type_checker_ptr         m_migrate_tc;
+
+    pos_info                 m_pos;
+    buffer<expr>             m_params;
+    level_param_names        m_ls;
+    name                     m_from;
+    buffer<pair<name, expr>> m_replacements;
+    buffer<pair<name, name>> m_renames;
+    buffer<name>             m_hiding;
+
+    list<expr>               m_ctx;
+    buffer<expr>             m_S_params;
+
+    migrate_cmd_fn(parser & p):
+        m_p(p), m_env(p.env()), m_ngen(p.mk_ngen()) {
+        m_trace = get_migrate_trace(p.get_options());
+    }
+
+    io_state_stream out() const { return regular(m_env, m_p.ios()); }
+    expr whnf(expr const & e) { return m_tc->whnf(e).first; }
+    expr infer_type(expr const & e) { return m_tc->infer(e).first; }
+
+    /** \brief Return true iff type has at least m_S_params.size() + 1 args, and argument m_S_params.size() is inst_implicit */
+    bool check_sufficient_args(expr type) {
+        for (unsigned i = 0; i < m_S_params.size(); i++) {
+            if (!is_pi(type))
+                return false;
+            type = binding_body(type);
+        }
+        return is_pi(type) && binding_info(type).is_inst_implicit();
+    }
+
+    /** \brief Return true iff \c e is of the form (p a_1 ... a_n s ...), where
+        \c p is a projection, n == m_S_params.size(), and s contains an instance */
+    bool is_projection_inst(expr const & e) {
+        if (!is_app(e))
+            return false;
+        expr const & f = get_app_fn(e);
+        if (!is_constant(f) || !is_projection(m_env, const_name(f)))
+            return false;
+        buffer<expr> args;
+        get_app_args(e, args);
+        if (args.size() < m_S_params.size() + 1)
+            return false;
+        return true; // TODO(Leo): check if instance occurs here refine
+    }
+
+    class normalize_fn : public replace_visitor {
+        migrate_cmd_fn & m_main;
+        unsigned         m_num_params; // number of parameters of the class
+
+        expr visit_app(expr const & e) {
+            buffer<expr> args;
+            expr f        = get_app_args(e, args);
+            expr new_f    = visit(f);
+            for (expr & arg : args)
+                arg = visit(arg);
+            expr r = mk_app(new_f, args);
+            if (is_constant(new_f) && args.size() >= m_num_params + 1) {
+                name const & fname = const_name(new_f);
+                if (is_projection(m_main.m_env, fname)) {
+                    return normalize(*m_main.m_migrate_tc, r, true);
+                } else {
+                    for (auto const & p : m_main.m_replacements) {
+                        if (p.first == fname) {
+                            expr new_r = p.second;
+                            for (unsigned i = m_num_params + 1; i < args.size(); i++)
+                                new_r = mk_app(new_r, args[i]);
+                            if (m_main.m_tc->is_def_eq(r, new_r).first)
+                                return new_r;
+                            break;
+                        }
+                    }
+                }
+            }
+            return r;
+        }
+
+        expr visit_binding(expr const & b) {
+            expr new_domain = visit(binding_domain(b));
+            expr l          = mk_local(m_main.m_tc->mk_fresh_name(), new_domain);
+            expr new_body   = abstract(visit(instantiate(binding_body(b), l)), l);
+            return update_binding(b, new_domain, new_body);
+        }
+
+    public:
+        normalize_fn(migrate_cmd_fn & m):
+            m_main(m), m_num_params(m_main.m_S_params.size()) {}
+    };
+
+    void migrate_decl(declaration const & d) {
+        if (!check_sufficient_args(d.get_type())) {
+            if (m_trace)
+                out() << "skipped '" << d.get_name() << "': does not have sufficient number of arguments\n";
+            return;
+        }
+        name d_name = d.get_name();
+        if (is_projection(m_env, d_name)) {
+            if (m_trace)
+                out() << "skipped '" << d.get_name() << "': projections are ignored\n";
+            return; // we don't migrate projections
+        }
+        if (is_coercion(m_env, d_name)) {
+            if (m_trace)
+                out() << "skipped '" << d.get_name() << "': coercions are ignored\n";
+            return; // we don't migrate coercions
+        }
+
+        bool renamed = false;
+        name short_name, full_name;
+        for (auto const & p : m_renames) {
+            if (p.first == d_name) {
+                renamed    = true;
+                full_name  = p.second;
+                short_name = full_name.replace_prefix(full_name, name());
+                break;
+            }
+        }
+        if (!renamed) {
+            short_name = d_name.replace_prefix(m_from, name());
+            full_name  = get_namespace(m_env) + short_name;
+        }
+
+        if (m_env.find(full_name)) {
+            if (m_trace)
+                out() << "skipped '" << d.get_name() << "': new name '" << full_name << "' has already been declared\n";
+            return; // already has this decl
+        }
+        try {
+            expr d_inst = mk_app(mk_app(mk_explicit(mk_constant(d_name)), m_S_params), mk_strict_expr_placeholder());
+            expr v; level_param_names ls;
+            std::tie(v, ls) = m_p.elaborate_relaxed(d_inst, m_ctx);
+            ls = append(m_ls, ls);
+            expr t = normalize_fn(*this)(infer_type(v));
+
+            expr new_type  = Pi(m_params, t);
+            expr new_value = Fun(m_params, v);
+            try {
+                if (d.is_theorem())
+                    m_env = module::add(m_env, check(m_env, mk_theorem(full_name, ls, new_type, new_value)));
+                else
+                    m_env = module::add(m_env, check(m_env, mk_definition(m_env, full_name, ls,
+                                                                          new_type, new_value, d.is_opaque())));
+                m_p.add_decl_index(full_name, m_pos, d.is_theorem() ? name("theorem") : name("definition"), new_type);
+                if (short_name != full_name)
+                    m_env = add_expr_alias_rec(m_env, short_name, full_name);
+                if (m_trace)
+                    out() << "migrated: " << full_name << " : " << new_type << "\n";
+            } catch (exception & ex) {
+                if (m_trace) {
+                    out() << "failed to migrate '" << d.get_name() << "', kernel rejected new declaration\n";
+                    ::lean::display_error(out(), nullptr, ex);
+                    out() << "\n";
+                }
+                return;
+            }
+        } catch (exception & ex) {
+            if (m_trace) {
+                out() << "skipped '" << d.get_name() << "': failed to be elaborated\n";
+                ::lean::display_error(out(), nullptr, ex);
+                out() << "\n";
+            }
+            return;
+        }
+    }
+
+
+    void parse_params() {
+        if (!m_p.curr_is_token(get_from_tk())) {
+            unsigned rbp = 0;
+            m_p.parse_binders(m_params, rbp);
+        }
+        for (expr const & l : m_params)
+            m_p.add_local(l);
+    }
+
+    void parse_S_params() {
+        m_p.check_token_next(get_with_tk(), "invalid 'migrate' command, 'with' expected");
+        while (true) {
+            m_S_params.push_back(m_p.parse_expr());
+            if (!m_p.curr_is_token(get_comma_tk()))
+                break;
+            m_p.next();
+        }
+    }
+
+    void parse_from_namespace() {
+        m_p.check_token_next(get_from_tk(), "invalid 'migrate' command, 'from' expected");
+        if (!m_p.curr_is_identifier())
+            throw parser_error("invalid 'migrate' command, identifier expected", m_p.pos());
+        auto n = to_valid_namespace_name(m_env, m_p.get_name_val());
+        if (!n)
+            throw parser_error(sstream() << "invalid 'migrate' command, '" << m_p.get_name_val() << "' is not a namespace", m_p.pos());
+        m_from = *n;
+        m_p.next();
+    }
+
+    name parse_source_id() {
+        if (!m_p.curr_is_identifier())
+            throw parser_error("invalid 'migrate' command, identifier expected", m_p.pos());
+        name n = m_p.get_name_val();
+        if (!m_env.find(n)) {
+            n = m_from + n;
+            if (!m_env.find(n))
+                throw parser_error(sstream() << "invalid 'migrate' command, '" << n << "' is not a declaration", m_p.pos());
+        } else {
+            if (is_prefix_of(m_from, n))
+                throw parser_error(sstream() << "invalid 'migrate' command, '" << n << "' is not in the source namespace", m_p.pos());
+        }
+        m_p.next();
+        return n;
+    }
+
+    name parse_to_id() {
+        if (!m_p.curr_is_identifier())
+            throw parser_error("invalid 'migrate' command, identifier expected", m_p.pos());
+        name n = m_p.get_name_val();
+        name ns = get_namespace(m_env);
+        if (!is_prefix_of(ns, n))
+            n = ns + n;
+        m_p.next();
+        return n;
+    }
+
+    void parse_modifiers() {
+        while (m_p.curr_is_token(get_replacing_tk()) ||
+               m_p.curr_is_token(get_hiding_tk()) ||
+               m_p.curr_is_token(get_renaming_tk())) {
+            if (m_p.curr_is_token(get_replacing_tk())) {
+                m_p.next();
+                while (true) {
+                    name from_id = parse_source_id();
+                    m_p.check_token_next(get_arrow_tk(), "invalid 'migrate' command, '->' expected");
+                    expr to   = m_p.parse_expr();
+                    m_replacements.emplace_back(from_id, to);
+                    if (!m_p.curr_is_token(get_comma_tk()))
+                        break;
+                    m_p.next();
+                }
+            } else if (m_p.curr_is_token(get_hiding_tk())) {
+                m_p.next();
+                while (true) {
+                    name id = parse_source_id();
+                    m_hiding.push_back(id);
+                    if (!m_p.curr_is_token(get_comma_tk()))
+                        break;
+                    m_p.next();
+                }
+            } else if (m_p.curr_is_token(get_renaming_tk())) {
+                m_p.next();
+                name from_id = parse_source_id();
+                m_p.check_token_next(get_arrow_tk(), "invalid 'migrate' command, '->' expected");
+                name to_id   = parse_to_id();
+                m_renames.emplace_back(from_id, to_id);
+                if (!m_p.curr_is_token(get_comma_tk()))
+                    break;
+                m_p.next();
+            } else {
+                lean_unreachable();
+            }
+        }
+    }
+
+    expr update_locals(expr new_tmp, buffer<expr> & locals) {
+        for (unsigned i = 0; i < locals.size(); i++) {
+            expr new_local = mk_local(mlocal_name(locals[i]), binding_name(new_tmp), binding_domain(new_tmp),
+                                      binding_info(new_tmp));
+            locals[i]      = new_local;
+            new_tmp        = instantiate(binding_body(new_tmp), new_local);
+        }
+        return new_tmp;
+    }
+
+    // hack to treat expressions as type
+    expr mk_as_type(expr const & e) {
+        return mk_app(mk_constant(get_eq_name()), e, e);
+    }
+
+    expr get_as_type_expr(expr const & e) {
+        lean_assert(is_eq(e));
+        return app_arg(e);
+    }
+
+    void elaborate() {
+        buffer<expr> include_vars;
+        m_p.get_include_variables(include_vars);
+        buffer<expr> tmp_locals;
+        tmp_locals.append(m_params);
+        for (auto const & p : m_S_params)
+            tmp_locals.push_back(mk_local(m_ngen.next(), mk_as_type(p)));
+        for (auto const & p : m_replacements)
+            tmp_locals.push_back(mk_local(m_ngen.next(), mk_as_type(p.second)));
+
+        expr_struct_set dep_set;
+        for (expr const & v : include_vars) {
+            ::lean::collect_locals(mlocal_type(v), dep_set);
+            dep_set.insert(v);
+        }
+        for (expr const & p : m_params)
+            ::lean::collect_locals(mlocal_type(p), dep_set);
+        buffer<expr> ctx;
+        sort_locals(dep_set, m_p, ctx);
+        expr dummy     = mk_Prop();
+        expr tmp       = Pi_as_is(ctx, Pi(tmp_locals, dummy, m_p), m_p);
+
+        level_param_names new_ls;
+        expr new_tmp;
+        std::tie(new_tmp, new_ls) = m_p.elaborate_type(tmp, list<expr>());
+        m_ls    = new_ls;
+        new_tmp = update_locals(new_tmp, ctx);
+        new_tmp = update_locals(new_tmp, m_params);
+        for (auto & p : m_S_params) {
+            p        = get_as_type_expr(binding_domain(new_tmp));
+            new_tmp  = binding_body(new_tmp);
+        }
+        for (auto & p : m_replacements) {
+            p.second = get_as_type_expr(binding_domain(new_tmp));
+            new_tmp  = binding_body(new_tmp);
+        }
+
+        buffer<expr> explicit_params;
+        explicit_params.append(m_params);
+        m_params.clear();
+        m_params.append(ctx);
+        m_params.append(explicit_params);
+    }
+
+    environment operator()() {
+        m_pos = m_p.pos();
+
+        m_migrate_tc = std::unique_ptr<type_checker>(new type_checker(m_env, m_ngen.mk_child(),
+                       std::unique_ptr<converter>(new migrate_converter(m_env, get_namespaces(m_env)))));
+        m_tc = std::unique_ptr<type_checker>(new type_checker(m_env, m_ngen.mk_child(),
+               std::unique_ptr<converter>(new unfold_semireducible_converter(m_env, true, true))));
+
+        parse_params();
+        parse_from_namespace();
+        parse_S_params();
+        parse_modifiers();
+        elaborate();
+
+        m_ctx = reverse_to_list(m_params.begin(), m_params.end());
+
+        for (expr & p : m_S_params)
+            p = mk_as_is(p);
+
+        environment env = m_env;
+        env.for_each_declaration([&](declaration const & d) {
+                if (!d.is_definition() && !d.is_theorem())
+                    return;
+                if (std::find(m_hiding.begin(), m_hiding.end(), d.get_name()) != m_hiding.end())
+                    return;
+                if (is_prefix_of(m_from, d.get_name()))
+                    migrate_decl(d);
+            });
+        return m_env;
+    }
+};
+
+static environment migrate_cmd(parser & p) {
+    return migrate_cmd_fn(p)();
+}
+
+void register_migrate_cmd(cmd_table & r) {
+    add_cmd(r, cmd_info("migrate",   "instantiate structure theorems", migrate_cmd));
+}
+
+void initialize_migrate_cmd() {
+    g_migrate_trace = new name{"migrate", "trace"};
+    register_bool_option(*g_migrate_trace, LEAN_DEFAULT_MIGRATE_TRACE,
+                         "(migrate) enable/disable trace messages describing which declarations have been migrated");
+}
+
+void finalize_migrate_cmd() {
+    delete g_migrate_trace;
+}
+}

src/frontends/lean/migrate_cmd.h

@@ -0,0 +1,14 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "frontends/lean/cmd_table.h"
+
+namespace lean {
+void register_migrate_cmd(cmd_table & r);
+void initialize_migrate_cmd();
+void finalize_migrate_cmd();
+}

src/frontends/lean/parser.cpp

@@ -670,6 +670,17 @@ std::tuple<expr, level_param_names> parser::elaborate_relaxed(expr const & e, li
     return r;
 }
 
+std::tuple<expr, level_param_names> parser::elaborate(expr const & e, list<expr> const & ctx) {
+    bool relax            = false;
+    bool check_unassigned = true;
+    bool ensure_type      = false;
+    parser_pos_provider pp = get_pos_provider();
+    elaborator_context env = mk_elaborator_context(pp, check_unassigned);
+    auto r = ::lean::elaborate(env, ctx, e, relax, ensure_type);
+    m_pre_info_manager.clear();
+    return r;
+}
+
 std::tuple<expr, level_param_names> parser::elaborate_type(expr const & e, list<expr> const & ctx, bool clear_pre_info) {
     bool relax            = false;
     bool check_unassigned = true;

src/frontends/lean/parser.h

@@ -438,6 +438,7 @@ public:
 
     /** \brief Elaborate \c e, and tolerate metavariables in the result. */
     std::tuple<expr, level_param_names> elaborate_relaxed(expr const & e, list<expr> const & ctx = list<expr>());
+    std::tuple<expr, level_param_names> elaborate(expr const & e, list<expr> const & ctx = list<expr>());
     /** \brief Elaborate \c e, and ensure it is a type. */
     std::tuple<expr, level_param_names> elaborate_type(expr const & e, list<expr> const & ctx = list<expr>(),
                                                        bool clear_pre_info = true);

src/frontends/lean/token_table.cpp

@@ -75,7 +75,7 @@ static char const * g_decreasing_unicode = "↓";
 void init_token_table(token_table & t) {
     pair<char const *, unsigned> builtin[] =
         {{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"at", 0}, {"have", 0}, {"assert", 0}, {"show", 0}, {"obtain", 0},
-         {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0},
+         {"if", 0}, {"then", 0}, {"else", 0}, {"by", 0}, {"hiding", 0}, {"replacing", 0}, {"renaming", 0},
          {"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec},
          {"{|", g_max_prec}, {"|}", 0}, {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
@@ -98,7 +98,7 @@ void init_token_table(token_table & t) {
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
          "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
          "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "multiple_instances", "find_decl", "attribute", "persistent",
-         "include", "omit", "#erase_cache", "#projections", "#telescope_eq", nullptr};
+         "include", "omit", "migrate", "#erase_cache", "#projections", "#telescope_eq", nullptr};
 
     pair<char const *, char const *> aliases[] =
         {{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},

src/frontends/lean/tokens.cpp

@@ -69,6 +69,7 @@ static name * g_decls        = nullptr;
 static name * g_hiding       = nullptr;
 static name * g_exposing     = nullptr;
 static name * g_renaming     = nullptr;
+static name * g_replacing    = nullptr;
 static name * g_extends      = nullptr;
 static name * g_as           = nullptr;
 static name * g_none         = nullptr;
@@ -193,6 +194,7 @@ void initialize_tokens() {
     g_hiding       = new name("hiding");
     g_exposing     = new name("exposing");
     g_renaming     = new name("renaming");
+    g_replacing    = new name("replacing");
     g_extends      = new name("extends");
     g_as           = new name("as");
     g_none         = new name("[none]");
@@ -324,6 +326,7 @@ void finalize_tokens() {
     delete g_hiding;
     delete g_exposing;
     delete g_renaming;
+    delete g_replacing;
     delete g_extends;
     delete g_as;
     delete g_none;
@@ -443,6 +446,7 @@ name const & get_decls_tk() { return *g_decls; }
 name const & get_hiding_tk() { return *g_hiding; }
 name const & get_exposing_tk() { return *g_exposing; }
 name const & get_renaming_tk() { return *g_renaming; }
+name const & get_replacing_tk() { return *g_replacing; }
 name const & get_extends_tk() { return *g_extends; }
 name const & get_as_tk() { return *g_as; }
 name const & get_none_tk() { return *g_none; }

src/frontends/lean/tokens.h

@@ -71,6 +71,7 @@ name const & get_decls_tk();
 name const & get_hiding_tk();
 name const & get_exposing_tk();
 name const & get_renaming_tk();
+name const & get_replacing_tk();
 name const & get_extends_tk();
 name const & get_as_tk();
 name const & get_none_tk();

src/frontends/lean/util.cpp

@@ -404,11 +404,14 @@ justification mk_type_mismatch_jst(expr const & v, expr const & v_type, expr con
         });
 }
 
-std::tuple<expr, level_param_names> parse_local_expr(parser & p) {
+std::tuple<expr, level_param_names> parse_local_expr(parser & p, bool relaxed) {
     expr e   = p.parse_expr();
     list<expr> ctx = p.locals_to_context();
     level_param_names new_ls;
-    std::tie(e, new_ls) = p.elaborate_relaxed(e, ctx);
+    if (relaxed)
+        std::tie(e, new_ls) = p.elaborate_relaxed(e, ctx);
+    else
+        std::tie(e, new_ls) = p.elaborate(e, ctx);
     level_param_names ls = to_level_param_names(collect_univ_params(e));
     return std::make_tuple(e, ls);
 }

src/frontends/lean/util.h

@@ -101,7 +101,7 @@ inline justification mk_type_mismatch_jst(expr const & v, expr const & v_type, e
 }
 
 /** \brief Auxiliary function for check/eval/find_decl */
-std::tuple<expr, level_param_names> parse_local_expr(parser & p);
+std::tuple<expr, level_param_names> parse_local_expr(parser & p, bool relaxed = true);
 
 optional<name> is_uniquely_aliased(environment const & env, name const & n);