refactor(kernel/type_checker): type checker should not unfold macros, but sign an error if a untrusted macro is used

Now, we unfold untrusted macros outside of the Lean kernel.

src/frontends/lean/builtin_cmds.cpp

@@ -431,7 +431,8 @@ static environment add_abbrev(parser & p, environment const & env, name const &
     name const & ns = get_namespace(env);
     name full_id    = ns + id;
     p.add_abbrev_index(full_id, d);
-    environment new_env = module::add(env, check(env, mk_definition(env, full_id, decl.get_univ_params(), decl.get_type(), value, opaque)));
+    environment new_env =
+        module::add(env, check(env, mk_definition(env, full_id, decl.get_univ_params(), decl.get_type(), value, opaque)));
     if (full_id != id)
         new_env = add_expr_alias_rec(new_env, id, full_id);
     return new_env;

src/frontends/lean/decl_cmds.cpp

@@ -20,6 +20,7 @@ Author: Leonardo de Moura
 #include "library/reducible.h"
 #include "library/coercion.h"
 #include "library/class.h"
+#include "library/unfold_macros.h"
 #include "library/definitional/equations.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/class.h"
@@ -129,12 +130,13 @@ static environment declare_var(parser & p, environment env,
         lean_assert(k == variable_kind::Constant || k == variable_kind::Axiom);
         name const & ns = get_namespace(env);
         name full_n  = ns + n;
+        expr new_type = unfold_untrusted_macros(env, type);
         if (k == variable_kind::Axiom) {
-            env = module::add(env, check(env, mk_axiom(full_n, ls, type)));
-            p.add_decl_index(full_n, pos, get_axiom_tk(), type);
+            env = module::add(env, check(env, mk_axiom(full_n, ls, new_type)));
+            p.add_decl_index(full_n, pos, get_axiom_tk(), new_type);
         } else {
-            env = module::add(env, check(env, mk_constant_assumption(full_n, ls, type)));
-            p.add_decl_index(full_n, pos, get_variable_tk(), type);
+            env = module::add(env, check(env, mk_constant_assumption(full_n, ls, new_type)));
+            p.add_decl_index(full_n, pos, get_variable_tk(), new_type);
         }
         if (!ns.is_anonymous())
             env = add_expr_alias(env, n, full_n);
@@ -671,6 +673,9 @@ class definition_cmd_fn {
                 try {
                     level_param_names c_ls; expr c_type, c_value;
                     std::tie(c_ls, c_type, c_value) = *it;
+                    // cache may have been created using a different trust level
+                    c_type  = unfold_untrusted_macros(m_env, c_type);
+                    c_value = unfold_untrusted_macros(m_env, c_value);
                     if (m_kind == Theorem) {
                         cd = check(m_env, mk_theorem(m_real_name, c_ls, c_type, c_value));
                         if (!m_p.keep_new_thms()) {
@@ -768,6 +773,12 @@ class definition_cmd_fn {
         lean_assert(aux_values.size() == m_aux_types.size());
         if (aux_values.size() != m_real_aux_names.size())
             throw exception("invalid declaration, failed to compile auxiliary declarations");
+        m_type  = unfold_untrusted_macros(m_env, m_type);
+        m_value = unfold_untrusted_macros(m_env, m_value);
+        for (unsigned i = 0; i < aux_values.size(); i++) {
+            m_aux_types[i] = unfold_untrusted_macros(m_env, m_aux_types[i]);
+            aux_values[i]  = unfold_untrusted_macros(m_env, aux_values[i]);
+        }
         if (is_definition()) {
             m_env = module::add(m_env, check(m_env, mk_definition(m_env, m_real_name, new_ls,
                                                                   m_type, m_value, m_is_opaque)));
@@ -798,6 +809,7 @@ class definition_cmd_fn {
                 std::tie(m_type, new_ls) = m_p.elaborate_type(m_type, list<expr>(), clear_pre_info);
                 check_no_metavar(m_env, m_real_name, m_type, true);
                 m_ls = append(m_ls, new_ls);
+                m_type = unfold_untrusted_macros(m_env, m_type);
                 expr type_as_is = m_p.save_pos(mk_as_is(m_type), type_pos);
                 if (!m_p.collecting_info() && m_kind == Theorem && m_p.num_threads() > 1) {
                     // Add as axiom, and create a task to prove the theorem.
@@ -806,6 +818,8 @@ class definition_cmd_fn {
                     m_env = module::add(m_env, check(m_env, mk_axiom(m_real_name, m_ls, m_type)));
                 } else {
                     std::tie(m_type, m_value, new_ls) = m_p.elaborate_definition(m_name, type_as_is, m_value, m_is_opaque);
+                    m_type  = unfold_untrusted_macros(m_env, m_type);
+                    m_value = unfold_untrusted_macros(m_env, m_value);
                     new_ls = append(m_ls, new_ls);
                     auto cd = check(m_env, mk_theorem(m_real_name, new_ls, m_type, m_value));
                     if (m_kind == Theorem) {
@@ -821,6 +835,8 @@ class definition_cmd_fn {
             } else {
                 std::tie(m_type, m_value, new_ls) = m_p.elaborate_definition(m_name, m_type, m_value, m_is_opaque);
                 new_ls = append(m_ls, new_ls);
+                m_type  = unfold_untrusted_macros(m_env, m_type);
+                m_value = unfold_untrusted_macros(m_env, m_value);
                 m_env = module::add(m_env, check(m_env, mk_definition(m_env, m_real_name, new_ls,
                                                                       m_type, m_value, m_is_opaque)));
                 m_p.cache_definition(m_real_name, pre_type, pre_value, new_ls, m_type, m_value);

src/frontends/lean/theorem_queue.cpp

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <vector>
+#include "library/unfold_macros.h"
 #include "kernel/type_checker.h"
 #include "frontends/lean/theorem_queue.h"
 #include "frontends/lean/parser.h"
@@ -19,6 +20,7 @@ void theorem_queue::add(environment const & env, name const & n, level_param_nam
             bool is_opaque = true; // theorems are always opaque
             std::tie(type, value, new_ls) = m_parser.elaborate_definition_at(env, lls, n, t, v, is_opaque);
             new_ls = append(ls, new_ls);
+            value  = unfold_untrusted_macros(env, value);
             auto r = check(env, mk_theorem(n, new_ls, type, value));
             m_parser.cache_definition(n, t, v, new_ls, type, value);
             return r;

src/kernel/type_checker.cpp

@@ -192,19 +192,10 @@ pair<expr, constraint_seq> type_checker::infer_macro(expr const & e, bool infer_
     expr t            = tcs.first;
     constraint_seq cs = tcs.second;
     if (!infer_only && def.trust_level() >= m_env.trust_lvl()) {
-        optional<expr> m = expand_macro(e);
-        if (!m)
-            throw_kernel_exception(m_env, "failed to expand macro", e);
-        pair<expr, constraint_seq> tmcs = infer_type_core(*m, infer_only);
-        cs = cs + tmcs.second;
-        simple_delayed_justification jst([=]() { return mk_macro_jst(e); });
-        pair<bool, constraint_seq> bcs  = is_def_eq(t, tmcs.first, jst);
-        if (!bcs.first)
-            throw_kernel_exception(m_env, g_macro_error_msg, e);
-        return mk_pair(t, bcs.second + cs);
-    } else {
-        return mk_pair(t, cs);
+        throw_kernel_exception(m_env, "declaration contains macro with trust-level higher than the one allowed "
+                               "(possible solution: unfold macro, or increase trust-level)", e);
     }
+    return mk_pair(t, cs);
 }
 
 pair<expr, constraint_seq> type_checker::infer_lambda(expr const & _e, bool infer_only) {

src/library/CMakeLists.txt

@@ -11,6 +11,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   typed_expr.cpp let.cpp type_util.cpp protected.cpp
   metavar_closure.cpp reducible.cpp init_module.cpp
   generic_exception.cpp fingerprint.cpp flycheck.cpp hott_kernel.cpp
-  local_context.cpp choice_iterator.cpp pp_options.cpp)
+  local_context.cpp choice_iterator.cpp pp_options.cpp unfold_macros.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/kernel_bindings.cpp

@@ -31,6 +31,7 @@ Author: Leonardo de Moura
 #include "library/module.h"
 #include "library/reducible.h"
 #include "library/print.h"
+#include "library/unfold_macros.h"
 
 // Lua Bindings for the Kernel classes. We do not include the Lua
 // bindings in the kernel because we do not want to inflate the Kernel.
@@ -1905,14 +1906,15 @@ static int type_check(lua_State * L) {
 static int add_declaration(lua_State * L) {
     int nargs = lua_gettop(L);
     optional<certified_declaration> d;
+    environment const & env = to_environment(L, 1);
     if (nargs == 2) {
-        d = check(to_environment(L, 1), to_declaration(L, 2));
+        d = check(env, unfold_untrusted_macros(env, to_declaration(L, 2)));
     } else if (nargs == 3) {
-        d = check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3));
+        d = check(env, unfold_untrusted_macros(env, to_declaration(L, 2)), to_name_generator(L, 3));
     } else {
         name_set extra_opaque = to_name_set(L, 4);
         extra_opaque_pred pred([=](name const & n) { return extra_opaque.contains(n); });
-        d = check(to_environment(L, 1), to_declaration(L, 2), to_name_generator(L, 3), pred);
+        d = check(env, unfold_untrusted_macros(env, to_declaration(L, 2)), to_name_generator(L, 3), pred);
     }
     return push_environment(L, module::add(to_environment(L, 1), *d));
 }

src/library/module.cpp

@@ -23,6 +23,7 @@ Author: Leonardo de Moura
 #include "library/module.h"
 #include "library/sorry.h"
 #include "library/kernel_serializer.h"
+#include "library/unfold_macros.h"
 #include "version.h"
 
 #ifndef LEAN_ASYNCH_IMPORT_THEOREM
@@ -357,6 +358,7 @@ struct import_modules_fn {
         declaration decl = read_declaration(d, midx);
         lean_assert(!decl.is_definition() || decl.get_module_idx() == midx);
         environment env  = m_senv.env();
+        decl = unfold_untrusted_macros(env, decl);
         if (decl.get_name() == get_sorry_name() && has_sorry(env))
             return;
         if (env.trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL) {

src/library/unfold_macros.cpp

@@ -0,0 +1,154 @@
+/*
+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/interrupt.h"
+#include "kernel/type_checker.h"
+#include "kernel/find_fn.h"
+#include "kernel/expr_maps.h"
+#include "kernel/instantiate.h"
+#include "kernel/abstract.h"
+#include "library/unfold_macros.h"
+#include "library/replace_visitor.h"
+#include "library/generic_exception.h"
+
+namespace lean {
+class unfold_untrusted_macros_fn {
+    typedef expr_bi_struct_map<expr> cache;
+
+    type_checker m_tc;
+    unsigned     m_trust_lvl;
+    cache        m_cache;
+
+    expr save_result(expr const & e, expr && r) {
+        m_cache.insert(std::make_pair(e, r));
+        return r;
+    }
+
+    expr visit_macro(expr const & e) {
+        buffer<expr> new_args;
+        for (unsigned i = 0; i < macro_num_args(e); i++)
+            new_args.push_back(visit(macro_arg(e, i)));
+        auto def = macro_def(e);
+        expr r = update_macro(e, new_args.size(), new_args.data());
+        if (def.trust_level() >= m_trust_lvl) {
+            if (optional<expr> new_r = m_tc.expand_macro(r)) {
+                return *new_r;
+            } else {
+                throw_generic_exception("failed to expand macro", e);
+            }
+        } else {
+            return r;
+        }
+    }
+
+    expr visit_app(expr const & e) {
+        expr new_f = visit(app_fn(e));
+        expr new_v = visit(app_arg(e));
+        return update_app(e, new_f, new_v);
+    }
+
+    expr visit_binding(expr e) {
+        expr_kind k = e.kind();
+        buffer<expr>  es;
+        buffer<expr>  ls;
+        while (e.kind() == k) {
+            expr d = visit(instantiate_rev(binding_domain(e), ls.size(), ls.data()));
+            expr l = mk_local(m_tc.mk_fresh_name(), binding_name(e), d, binding_info(e));
+            ls.push_back(l);
+            es.push_back(e);
+            e = binding_body(e);
+        }
+        e = visit(instantiate_rev(e, ls.size(), ls.data()));
+        expr r = abstract_locals(e, ls.size(), ls.data());
+        while (!ls.empty()) {
+            expr d = mlocal_type(ls.back());
+            ls.pop_back();
+            d = abstract_locals(d, ls.size(), ls.data());
+            r = update_binding(es.back(), d, r);
+            es.pop_back();
+        }
+        return r;
+    }
+
+    expr visit(expr const & e) {
+        switch (e.kind()) {
+        case expr_kind::Sort:  case expr_kind::Constant:
+        case expr_kind::Var:   case expr_kind::Meta:
+        case expr_kind::Local:
+            return e;
+        default:
+            break;
+        }
+
+        check_system("unfold macros");
+        auto it = m_cache.find(e);
+        if (it != m_cache.end())
+            return it->second;
+
+        switch (e.kind()) {
+        case expr_kind::Sort:  case expr_kind::Constant:
+        case expr_kind::Var:   case expr_kind::Meta:
+        case expr_kind::Local:
+            lean_unreachable();
+        case expr_kind::Macro:
+            return save_result(e, visit_macro(e));
+        case expr_kind::App:
+            return save_result(e, visit_app(e));
+        case expr_kind::Lambda: case expr_kind::Pi:
+            return save_result(e, visit_binding(e));
+        }
+        lean_unreachable();
+    }
+
+public:
+    unfold_untrusted_macros_fn(environment const & env):
+        m_tc(env), m_trust_lvl(env.trust_lvl()) {}
+
+    expr operator()(expr const & e) { return visit(e); }
+};
+
+bool contains_untrusted_macro(unsigned trust_lvl, expr const & e) {
+    return static_cast<bool>(find(e, [&](expr const & e, unsigned) {
+                return is_macro(e) && macro_def(e).trust_level() >= trust_lvl;
+            }));
+}
+
+expr unfold_untrusted_macros(environment const & env, expr const & e) {
+    if (contains_untrusted_macro(env.trust_lvl(), e)) {
+        return unfold_untrusted_macros_fn(env)(e);
+    } else {
+        return e;
+    }
+}
+
+bool contains_untrusted_macro(unsigned trust_lvl, declaration const & d) {
+    if (contains_untrusted_macro(trust_lvl, d.get_type()))
+        return true;
+    return (d.is_definition() || d.is_theorem()) && contains_untrusted_macro(trust_lvl, d.get_value());
+}
+
+declaration unfold_untrusted_macros(environment const & env, declaration const & d) {
+    if (contains_untrusted_macro(env.trust_lvl(), d)) {
+        expr new_t = unfold_untrusted_macros(env, d.get_type());
+        if (d.is_theorem()) {
+            expr new_v = unfold_untrusted_macros(env, d.get_value());
+            return mk_theorem(d.get_name(), d.get_univ_params(), new_t, new_v, d.get_module_idx());
+        } else if (d.is_definition()) {
+            expr new_v = unfold_untrusted_macros(env, d.get_value());
+            return mk_definition(d.get_name(), d.get_univ_params(), new_t, new_v,
+                                 d.is_opaque(), d.get_weight(), d.get_module_idx(), d.use_conv_opt());
+        } else if (d.is_axiom()) {
+            return mk_axiom(d.get_name(), d.get_univ_params(), new_t);
+        } else if (d.is_constant_assumption()) {
+            return mk_constant_assumption(d.get_name(), d.get_univ_params(), new_t);
+        } else {
+            lean_unreachable();
+        }
+    } else {
+        return d;
+    }
+}
+}

src/library/unfold_macros.h

@@ -0,0 +1,21 @@
+/*
+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 "kernel/environment.h"
+
+namespace lean {
+/** \brief Unfold any macro occurring in \c e that has trust level higher than the one
+    allowed in \c env.
+
+    \remark We use this function before sending declarations to the kernel.
+    The kernel refuses any expression containing "untrusted" macros, i.e.,
+    macros with trust level higher than the one allowed.
+*/
+expr unfold_untrusted_macros(environment const & env, expr const & e);
+
+declaration unfold_untrusted_macros(environment const & env, declaration const & d);
+}