feat(kernel/inductive): add normalizer extension for inductive datatypes, add procedure for creating an standard (empty) Lean environment

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/CMakeLists.txt

@@ -215,6 +215,8 @@ add_subdirectory(kernel)
 set(LEAN_LIBS ${LEAN_LIBS} kernel)
 add_subdirectory(kernel/inductive)
 set(LEAN_LIBS ${LEAN_LIBS} inductive)
+add_subdirectory(kernel/standard)
+set(LEAN_LIBS ${LEAN_LIBS} standard_kernel)
 add_subdirectory(library)
 set(LEAN_LIBS ${LEAN_LIBS} library)
 # add_subdirectory(library/rewriter)

src/kernel/inductive/inductive.cpp

@@ -98,22 +98,40 @@ static name g_tmp_prefix = name::mk_internal_unique_name();
 
 /** \brief Environment extension used to store the computational rules associated with inductive datatype declarations. */
 struct inductive_env_ext : public environment_extension {
-    struct comp_rule {
+    struct elim_info {
         level_param_names m_level_names; // level parameter names used in computational rule
         unsigned          m_num_params;  // number of global parameters A
         unsigned          m_num_ACe;     // sum of number of global parameters A, type formers C, and minor preimises e.
-        unsigned          m_num_bu;      // sum of number of arguments u and v in the corresponding introduction rule.
-        expr              m_comp_rhs;    // computational rule RHS
-        comp_rule(level_param_names const & ls, unsigned num_ps, unsigned num_ace, unsigned num_bu, expr const & rhs):
-            m_level_names(ls), m_num_params(num_ps), m_num_ACe(num_ace), m_num_bu(num_bu), m_comp_rhs(rhs) {}
+        unsigned          m_num_indices; // number of inductive datatype indices
+        elim_info() {}
+        elim_info(level_param_names const & ls, unsigned num_ps, unsigned num_ACe, unsigned num_indices):
+            m_level_names(ls), m_num_params(num_ps), m_num_ACe(num_ACe), m_num_indices(num_indices) {}
+    };
+
+    struct comp_rule {
+        name              m_elim_name;     // name of the corresponding eliminator
+        unsigned          m_num_bu;        // sum of number of arguments u and v in the corresponding introduction rule.
+        expr              m_comp_rhs;      // computational rule RHS: Fun (A, C, e, b, u), (e_k_i b u v)
+        expr              m_comp_rhs_body; // body of m_comp_rhs:  (e_k_i b u v)
+        comp_rule() {}
+        comp_rule(name const & e, unsigned num_bu, expr const & rhs):
+            m_elim_name(e), m_num_bu(num_bu), m_comp_rhs(rhs), m_comp_rhs_body(rhs) {
+            while (is_lambda(m_comp_rhs_body))
+                m_comp_rhs_body = binding_body(m_comp_rhs_body);
+        }
     };
     // mapping from introduction rule name to computation rule data
-    rb_map<name, comp_rule, name_quick_cmp> m_com_rules;
+    rb_map<name, elim_info, name_quick_cmp>  m_elim_info;
+    rb_map<name, comp_rule, name_quick_cmp>  m_com_rules;
 
     inductive_env_ext() {}
 
-    void add(name const & n, level_param_names const & ls, unsigned num_ps, unsigned num_ace, unsigned num_bu, expr const & rhs) {
-        m_com_rules.insert(n, comp_rule(ls, num_ps, num_ace, num_bu, rhs));
+    void add_elim(name const & n, level_param_names const & ls, unsigned num_ps, unsigned num_ace, unsigned num_indices) {
+        m_elim_info.insert(n, elim_info(ls, num_ps, num_ace, num_indices));
+    }
+
+    void add_comp_rhs(name const & n, name const & e, unsigned num_bu, expr const & rhs) {
+        m_com_rules.insert(n, comp_rule(e, num_bu, rhs));
     }
 };
 
@@ -599,6 +617,9 @@ struct add_inductive_fn {
             es.append(m_elim_info[i].m_minor_premises);
     }
 
+    /** \brief Return the number of indices of the i-th datatype. */
+    unsigned get_num_indices(unsigned i) { return m_elim_info[i].m_indices.size(); }
+
     /** \brief Create computional rules RHS. They are used by the normalizer extension. */
     void mk_comp_rules_rhs() {
         unsigned d_idx  = 0;
@@ -608,6 +629,7 @@ struct add_inductive_fn {
         levels ls = get_elim_level_params();
         inductive_env_ext ext(get_extension(m_env));
         for (auto d : m_decls) {
+            ext.add_elim(get_elim_name(d), get_elim_level_param_names(), m_num_params, m_num_params + C.size() + e.size(),  get_num_indices(d_idx));
             for (auto ir : inductive_decl_intros(d)) {
                 buffer<expr> b;
                 buffer<expr> u;
@@ -647,8 +669,7 @@ struct add_inductive_fn {
                 expr e_app = mk_app(mk_app(mk_app(e[minor_idx], b), u), v);
                 expr comp_rhs   = Fun(m_param_consts, Fun(C, Fun(e, Fun(b, Fun(u, e_app)))));
                 m_tc.check(comp_rhs, get_elim_level_param_names());
-                ext.add(intro_rule_name(ir), get_elim_level_param_names(),
-                        m_num_params, m_num_params + C.size() + e.size(), b.size() + u.size(), comp_rhs);
+                ext.add_comp_rhs(intro_rule_name(ir), get_elim_name(d_idx), b.size() + u.size(), comp_rhs);
                 minor_idx++;
             }
             d_idx++;
@@ -680,5 +701,67 @@ environment add_inductive(environment const & env, name const & ind_name, level_
                           unsigned num_params, expr const & type, list<intro_rule> const & intro_rules) {
     return add_inductive(env, level_params, num_params, list<inductive_decl>(inductive_decl(ind_name, type, intro_rules)));
 }
+
+
+/** \brief Normalizer extension for applying inductive datatype computational rules. */
+class inductive_normalizer_extension : public normalizer_extension {
+public:
+    virtual optional<expr> operator()(expr const & e, extension_context & ctx) const {
+        // Reduce terms \c e of the form
+        //    elim_k A C e p[A,b] (intro_k_i A b u)
+        inductive_env_ext const & ext = get_extension(ctx.env());
+        expr const & elim_fn   = get_app_fn(e);
+        if (!is_constant(elim_fn))
+            return none_expr();
+        auto it1 = ext.m_elim_info.find(const_name(elim_fn));
+        if (!it1)
+            return none_expr(); // it is not an eliminator
+        buffer<expr> elim_args;
+        get_app_args(e, elim_args);
+        if (elim_args.size() != it1->m_num_ACe + it1->m_num_indices + 1)
+            return none_expr(); // number of arguments does not match
+        expr intro_app = ctx.whnf(elim_args.back());
+        expr const & intro_fn  = get_app_fn(intro_app);
+        // Last argument must be a constant and an application of a constant.
+        if (!is_constant(intro_fn))
+            return none_expr();
+        // Check if intro_fn is an introduction rule matching elim_fn
+        auto it2 = ext.m_com_rules.find(const_name(intro_fn));
+        if (!it2 || it2->m_elim_name != const_name(elim_fn))
+            return none_expr();
+        buffer<expr> intro_args;
+        get_app_args(intro_app, intro_args);
+        // Check intro num_args
+        if (intro_args.size() != it1->m_num_params + it2->m_num_bu)
+            return none_expr();
+        // std::cout << "Candidate: " << e << "\n";
+        if (it1->m_num_params > 0) {
+            // Global parameters of elim and intro be definitionally equal
+            delayed_justification jst([=]() { return mk_justification("elim/intro global parameters must match", some_expr(e)); });
+            for (unsigned i = 0; i < it1->m_num_params; i++) {
+                if (!ctx.is_def_eq(elim_args[i], intro_args[i], jst))
+                    return none_expr();
+            }
+        }
+        // std::cout << "global params matched\n";
+        // Number of universe levels must match.
+        if (length(const_levels(elim_fn)) != length(it1->m_level_names))
+            return none_expr();
+        buffer<expr> ACebu;
+        for (unsigned i = 0; i < it1->m_num_ACe; i++)
+            ACebu.push_back(elim_args[i]);
+        for (unsigned i = 0; i < it2->m_num_bu; i++)
+            ACebu.push_back(intro_args[it1->m_num_params + i]);
+        std::reverse(ACebu.begin(), ACebu.end());
+        expr r = instantiate(it2->m_comp_rhs_body, ACebu.size(), ACebu.data());
+        r = instantiate_params(r, it1->m_level_names, const_levels(elim_fn));
+        // std::cout << "ELIM/INTRO: " << e << " ==> " << r << "\n";
+        return some_expr(r);
+    }
+};
+
+std::unique_ptr<normalizer_extension> mk_extension() {
+    return std::unique_ptr<normalizer_extension>(new inductive_normalizer_extension());
+}
 }
 }

src/kernel/standard/CMakeLists.txt

@@ -0,0 +1,2 @@
+add_library(standard_kernel standard.cpp)
+target_link_libraries(standard_kernel ${LEAN_LIBS})

src/kernel/standard/standard.cpp

@@ -0,0 +1,19 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/inductive/inductive.h"
+
+namespace lean {
+/** \brief Create standard Lean environment */
+environment mk_environment(unsigned trust_lvl) {
+    return environment(trust_lvl,
+                       true /* Type.{0} is proof irrelevant */,
+                       true /* Eta */,
+                       true /* Type.{0} is impredicative */,
+                       list<name>() /* No type class has proof irrelevance */,
+                       inductive::mk_extension() /* builtin support for inductive datatypes */);
+}
+}

src/kernel/standard/standard.h

@@ -0,0 +1,13 @@
+/*
+Copyright (c) 2014 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 Create standard Lean environment */
+environment mk_environment(unsigned trust_lvl = 0);
+}

src/library/kernel_bindings.cpp

@@ -20,6 +20,7 @@ Author: Leonardo de Moura
 #include "kernel/error_msgs.h"
 #include "kernel/type_checker.h"
 #include "kernel/inductive/inductive.h"
+#include "kernel/standard/standard.h"
 #include "library/occurs.h"
 #include "library/io_state_stream.h"
 #include "library/expr_lt.h"
@@ -1074,6 +1075,13 @@ static int mk_empty_environment(lua_State * L) {
     list<name> const & cls_proof_irrel = get_list_name_named_param(L, 1, "cls_proof_irrel", list<name>());
     return push_environment(L, environment(trust_lvl, prop_proof_irrel, eta, impredicative, cls_proof_irrel));
 }
+static int mk_environment(lua_State * L) {
+    unsigned trust_lvl = 0;
+    if (lua_gettop(L) > 0)
+        trust_lvl = lua_tonumber(L, 1);
+    return push_environment(L, mk_environment(trust_lvl));
+}
+
 static int environment_forget(lua_State * L) { return push_environment(L, to_environment(L, 1).forget()); }
 
 static const struct luaL_Reg environment_m[] = {
@@ -1140,6 +1148,7 @@ static void open_environment(lua_State * L) {
     setfuncs(L, environment_m, 0);
 
     SET_GLOBAL_FUN(mk_empty_environment,   "empty_environment");
+    SET_GLOBAL_FUN(mk_environment,         "environment");
     SET_GLOBAL_FUN(environment_pred,       "is_environment");
     SET_GLOBAL_FUN(get_environment,        "get_environment");
     SET_GLOBAL_FUN(get_environment,        "get_env");

tests/lua/ind1.lua

@@ -1,4 +1,4 @@
-local env      = empty_environment()
+local env      = environment()
 local l        = mk_param_univ("l")
 local A        = Const("A")
 local U_l      = mk_sort(l)
@@ -18,7 +18,7 @@ local u        = global_univ("u")
 local v        = global_univ("v")
 
 function display_type(env, t)
-   print(tostring(t) .. " : " .. tostring(type_checker(env):infer(t)))
+   print(tostring(t) .. " : " .. tostring(type_checker(env):check(t)))
 end
 
 env = add_inductive(env,
@@ -102,3 +102,30 @@ display_type(env, Const("Odd_rec"))
 display_type(env, Const("and_rec", {v}))
 display_type(env, Const("vec_rec", {v, u}))
 display_type(env, Const("flist_rec", {v, u}))
+
+local U_1      = mk_level_one()
+local n        = Const("n")
+local c        = Const("c")
+local nat_rec1 = Const("nat_rec", {U_1})
+local add      = Fun({{a, Nat}, {b, Nat}}, nat_rec1(mk_lambda("_", Nat, Nat), b, Fun({{n, Nat}, {c, Nat}}, succ(c)), a))
+display_type(env, add)
+local tc = type_checker(env)
+assert(tc:is_def_eq(add(succ(succ(zero)), succ(zero)),
+                    succ(succ(succ(zero)))))
+assert(tc:is_def_eq(add(succ(succ(succ(zero))), succ(succ(zero))),
+                    succ(succ(succ(succ(succ(zero)))))))
+
+local list_nat      = Const("list", {U_1})(Nat)
+local list_nat_rec1 = Const("list_rec", {U_1, U_1})(Nat)
+display_type(env, list_nat_rec1)
+local h        = Const("h")
+local t        = Const("t")
+local v        = Const("v")
+local l        = Const("l")
+local length   = Fun(l, list_nat, list_nat_rec1(mk_lambda("_", list_nat, Nat), zero, Fun({{h, Nat}, {t, list_nat}, {v, Nat}}, succ(v)), l))
+local nil_nat  = Const("nil", {U_1})(Nat)
+local cons_nat = Const("cons", {U_1})(Nat)
+print(tc:whnf(length(nil_nat)))
+assert(tc:is_def_eq(length(nil_nat), zero))
+assert(tc:is_def_eq(length(cons_nat(zero, nil_nat)), succ(zero)))
+assert(tc:is_def_eq(length(cons_nat(zero, cons_nat(zero, nil_nat))), succ(succ(zero))))