From 863355c6a06534a9cfd2e20d2a445dac51b6929b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Aug 2018 09:27:06 -0700 Subject: [PATCH] feat(kernel/inductive): continue new inductive datatype module Add more validation, and create new inductive_val and constant_val objects. --- library/init/lean/declaration.lean | 3 - src/kernel/declaration.cpp | 32 ++++-- src/kernel/declaration.h | 28 ++--- src/kernel/environment.cpp | 8 ++ src/kernel/environment.h | 3 + src/kernel/inductive.cpp | 169 ++++++++++++++++++++++------- 6 files changed, 179 insertions(+), 64 deletions(-) diff --git a/library/init/lean/declaration.lean b/library/init/lean/declaration.lean index 314d00fd1b..a8f809b9f8 100644 --- a/library/init/lean/declaration.lean +++ b/library/init/lean/declaration.lean @@ -79,9 +79,6 @@ structure inductive_val extends constant_val := (nindices : nat) -- Number of indices (all : list name) -- List of all (including this one) inductive datatypes in the mutual declaration containing this one (cnstrs : list name) -- List of all constructors for this inductive datatype -(recs : list name) -- List of all recursors generated when the mutual inductive declaration containing this declaration was accepted by the kernel - -- Remark: `recs.length` may be greater than `all.length` if declaration contains nested inductives - -- The first element in the list is the recursor of this inductive declaration (is_rec : bool) -- `tt` iff it is recursive (is_meta : bool) diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index 6c36a374c5..99d66e3eda 100644 --- a/src/kernel/declaration.cpp +++ b/src/kernel/declaration.cpp @@ -70,15 +70,19 @@ recursor_rule::recursor_rule(name const & cnstr, unsigned nfields, expr const & object_ref(mk_cnstr(0, cnstr, nat(nfields), rhs)) { } -static unsigned inductive_scalar_offset() { return sizeof(object*)*6; } -static unsigned constructor_scalar_offset() { return sizeof(object*)*3; } -static unsigned recursor_scalar_offset() { return sizeof(object*)*7; } +inductive_val::inductive_val(name const & n, level_param_names const & lparams, expr const & type, unsigned nparams, + unsigned nindices, names const & all, names const & cnstrs, bool rec, bool meta): + object_ref(mk_cnstr(0, constant_val(n, lparams, type), nat(nparams), nat(nindices), all, cnstrs, 2)) { + cnstr_set_scalar(raw(), sizeof(object*)*5, static_cast(rec)); + cnstr_set_scalar(raw(), sizeof(object*)*5 + 1, static_cast(meta)); + lean_assert(is_meta() == meta); + lean_assert(is_rec() == rec); +} -bool inductive_val::is_rec() const { return (cnstr_scalar(raw(), inductive_scalar_offset()) & 1) != 0; } -bool inductive_val::is_meta() const { return (cnstr_scalar(raw(), inductive_scalar_offset()) & 2) != 0; } -bool constructor_val::is_meta() const { return cnstr_scalar(raw(), constructor_scalar_offset()); } -bool recursor_val::is_k() const { return (cnstr_scalar(raw(), recursor_scalar_offset()) & 1) != 0; } -bool recursor_val::is_meta() const { return (cnstr_scalar(raw(), recursor_scalar_offset()) & 2) != 0; } +constructor_val::constructor_val(name const & n, level_param_names const & lparams, expr const & type, name const & induct, unsigned nparams, bool is_meta): + object_ref(mk_cnstr(0, constant_val(n, lparams, type), induct, nat(nparams), 1)) { + cnstr_set_scalar(raw(), sizeof(object*)*3, static_cast(is_meta)); +} bool declaration::is_meta() const { switch (kind()) { @@ -208,6 +212,14 @@ constant_info::constant_info(quot_val const & v): object_ref(mk_cnstr(static_cast(constant_info_kind::Quot), v)) { } +constant_info::constant_info(inductive_val const & v): + object_ref(mk_cnstr(static_cast(constant_info_kind::Inductive), v)) { +} + +constant_info::constant_info(constructor_val const & v): + object_ref(mk_cnstr(static_cast(constant_info_kind::Constructor), v)) { +} + static reducibility_hints * g_opaque = nullptr; reducibility_hints const & constant_info::get_hints() const { @@ -223,8 +235,8 @@ bool constant_info::is_meta() const { case constant_info_kind::Definition: return to_definition_val().is_meta(); case constant_info_kind::Theorem: return false; case constant_info_kind::Quot: return false; - case constant_info_kind::Inductive: return false; // TODO(Leo): to_inductive_val().is_meta(); - case constant_info_kind::Constructor: return false; // TODO(Leo): to_constructor_val().is_meta(); + case constant_info_kind::Inductive: return to_inductive_val().is_meta(); + case constant_info_kind::Constructor: return to_constructor_val().is_meta(); case constant_info_kind::Recursor: return false; // TODO(Leo): to_recursor_val().is_meta(); } lean_unreachable(); diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h index 50da11038f..c8360090bf 100644 --- a/src/kernel/declaration.h +++ b/src/kernel/declaration.h @@ -260,14 +260,13 @@ structure inductive_val extends constant_val := (nindices : nat) -- Number of indices (all : list name) -- List of all (including this one) inductive datatypes in the mutual declaration containing this one (cnstrs : list name) -- List of all constructors for this inductive datatype -(recs : list name) -- List of all recursors generated when the mutual inductive declaration containing this declaration was accepted by the kernel - -- Remark: `recs.length` may be greater than `all.length` if declaration contains nested inductives - -- The first element in the list is the recursor of this inductive declaration (is_rec : bool) -- `tt` iff it is recursive (is_meta : bool) */ class inductive_val : public object_ref { public: + inductive_val(name const & n, level_param_names const & lparams, expr const & type, unsigned nparams, + unsigned nindices, names const & all, names const & cnstrs, bool is_rec, bool is_meta); inductive_val(inductive_val const & other):object_ref(other) {} inductive_val(inductive_val && other):object_ref(other) {} inductive_val & operator=(inductive_val const & other) { object_ref::operator=(other); return *this; } @@ -277,9 +276,8 @@ public: nat const & get_nindices() const { return static_cast(cnstr_obj_ref(*this, 2)); } names const & get_all() const { return static_cast(cnstr_obj_ref(*this, 3)); } names const & get_cnstrs() const { return static_cast(cnstr_obj_ref(*this, 4)); } - names const & get_recs() const { return static_cast(cnstr_obj_ref(*this, 5)); } - bool is_rec() const; - bool is_meta() const; + bool is_rec() const { return cnstr_scalar(raw(), sizeof(object*)*5) != 0; } + bool is_meta() const { return cnstr_scalar(raw(), sizeof(object*)*5 + 1) != 0; } }; /* @@ -290,6 +288,7 @@ structure constructor_val extends constant_val := */ class constructor_val : public object_ref { public: + constructor_val(name const & n, level_param_names const & lparams, expr const & type, name const & induct, unsigned nparams, bool is_meta); constructor_val(constructor_val const & other):object_ref(other) {} constructor_val(constructor_val && other):object_ref(other) {} constructor_val & operator=(constructor_val const & other) { object_ref::operator=(other); return *this; } @@ -297,7 +296,7 @@ public: constant_val const & to_constant_val() const { return static_cast(cnstr_obj_ref(*this, 0)); } name const & get_induct() const { return static_cast(cnstr_obj_ref(*this, 1)); } nat const & get_nparams() const { return static_cast(cnstr_obj_ref(*this, 2)); } - bool is_meta() const; + bool is_meta() const { return cnstr_scalar(raw(), sizeof(object*)*3) != 0; } }; /* @@ -395,6 +394,8 @@ public: constant_info(declaration const & d); constant_info(definition_val const & v); constant_info(quot_val const & v); + constant_info(inductive_val const & v); + constant_info(constructor_val const & v); constant_info(constant_info const & other):object_ref(other) {} constant_info(constant_info && other):object_ref(other) {} @@ -410,6 +411,8 @@ public: bool is_definition() const { return kind() == constant_info_kind::Definition; } bool is_axiom() const { return kind() == constant_info_kind::Axiom; } bool is_theorem() const { return kind() == constant_info_kind::Theorem; } + bool is_inductive() const { return kind() == constant_info_kind::Inductive; } + bool is_constructor() const { return kind() == constant_info_kind::Constructor; } name const & get_name() const { return to_constant_val().get_name(); } level_param_names const & get_univ_params() const { return to_constant_val().get_lparams(); } @@ -419,12 +422,11 @@ public: expr const & get_value() const { lean_assert(has_value()); return static_cast(cnstr_obj_ref(to_val(), 1)); } reducibility_hints const & get_hints() const; - axiom_val const & to_axiom_val() const { lean_assert(is_axiom()); return static_cast(cnstr_obj_ref(raw(), 0)); } - definition_val const & to_definition_val() const { lean_assert(is_definition()); return static_cast(cnstr_obj_ref(raw(), 0)); } - theorem_val const & to_theorem_val() const { lean_assert(is_theorem()); return static_cast(cnstr_obj_ref(raw(), 0)); } - - // inductive_val const & to_inductive_val() const { lean_assert(is_inductive()); return static_cast(to_val()); } - // constructor_val const & to_constructor_val() const { lean_assert(is_constructor()); return static_cast(to_val()); } + axiom_val const & to_axiom_val() const { lean_assert(is_axiom()); return static_cast(to_val()); } + definition_val const & to_definition_val() const { lean_assert(is_definition()); return static_cast(to_val()); } + theorem_val const & to_theorem_val() const { lean_assert(is_theorem()); return static_cast(to_val()); } + inductive_val const & to_inductive_val() const { lean_assert(is_inductive()); return static_cast(to_val()); } + constructor_val const & to_constructor_val() const { lean_assert(is_constructor()); return static_cast(to_val()); } // recursor_val const & to_recursor_val() const { lean_assert(is_recursor()); return static_cast(to_val()); } }; diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index c1069d8214..b2d2d5f43c 100644 --- a/src/kernel/environment.cpp +++ b/src/kernel/environment.cpp @@ -71,6 +71,10 @@ static void check_name(environment const & env, name const & n) { throw already_declared_exception(env, n); } +void environment::check_name(name const & n) const { + ::lean::check_name(*this, n); +} + static void check_duplicated_univ_params(environment const & env, level_param_names ls) { while (!is_nil(ls)) { auto const & p = head(ls); @@ -83,6 +87,10 @@ static void check_duplicated_univ_params(environment const & env, level_param_na } } +void environment::check_duplicated_univ_params(level_param_names ls) const { + ::lean::check_duplicated_univ_params(*this, ls); +} + static void check_constant_val(environment const & env, constant_val const & v, type_checker & checker) { check_name(env, v.get_name()); check_duplicated_univ_params(env, v.get_lparams()); diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 33646e9af0..57e8971bbb 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -76,6 +76,9 @@ class environment { environment(environment const & env, extensions const & exts): m_header(env.m_header), m_quot_initialized(env.m_quot_initialized), m_constants(env.m_constants), m_extensions(exts) {} + void check_duplicated_univ_params(level_param_names ls) const; + void check_name(name const & n) const; + void add_core(constant_info const & info) { m_constants.insert(info.get_name(), info); } environment add(constant_info const & info) const { environment new_env(*this); diff --git a/src/kernel/inductive.cpp b/src/kernel/inductive.cpp index 7c5170312d..8d6f1f2b6b 100644 --- a/src/kernel/inductive.cpp +++ b/src/kernel/inductive.cpp @@ -4,10 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "runtime/sstream.h" #include "util/name_generator.h" #include "kernel/environment.h" #include "kernel/type_checker.h" #include "kernel/instantiate.h" +#include "kernel/find_fn.h" #include "kernel/kernel_exception.h" namespace lean { @@ -24,6 +26,7 @@ class add_inductive_fn { local_ctx m_lctx; level_param_names m_lparams; unsigned m_nparams; + bool m_is_meta; buffer m_ind_types; buffer m_nindices; level m_result_level; @@ -56,22 +59,14 @@ class add_inductive_fn { public: add_inductive_fn(environment const & env, inductive_decl const & decl): - m_env(env), m_ngen(*g_ind_fresh), m_lparams(decl.get_lparams()) { + m_env(env), m_ngen(*g_ind_fresh), m_lparams(decl.get_lparams()), m_is_meta(decl.is_meta()) { if (!decl.get_nparams().is_small()) throw kernel_exception(env, "invalid inductive datatype, number of parameters is too big"); m_nparams = decl.get_nparams().get_small_value(); to_buffer(decl.get_types(), m_ind_types); } - void dump() { - std::cout << "add_inductive_decl\n"; - for (inductive_type const & ind_type : m_ind_types) { - std::cout << "ind>> " << ind_type.get_name() << " : " << ind_type.get_type() << "\n"; - for (constructor const & c : ind_type.get_cnstrs()) { - std::cout << ">> " << constructor_name(c) << " : " << constructor_type(c) << "\n"; - } - } - } + type_checker tc(local_ctx const & lctx = local_ctx()) { return type_checker(m_env, lctx, true, !m_is_meta); } /** \brief Check whether the type of each datatype is well typed, and do not contain free variables or meta variables, @@ -91,8 +86,10 @@ public: bool first = true; for (inductive_type const & ind_type : m_ind_types) { expr type = ind_type.get_type(); + m_env.check_name(ind_type.get_name()); + m_env.check_name(mk_rec_name(ind_type.get_name())); check_no_metavar_no_fvar(m_env, ind_type.get_name(), type); - type_checker(m_env).check(type, m_lparams); + tc().check(type, m_lparams); m_nindices.push_back(0); unsigned i = 0; while (is_pi(type)) { @@ -109,7 +106,7 @@ public: if (i != m_nparams) throw kernel_exception(m_env, "number of parameters mismatch in inductive datatype declaration"); - type = type_checker(m_env, m_lctx).ensure_sort(type); + type = tc(m_lctx).ensure_sort(type); if (first) { m_result_level = sort_level(type); @@ -128,16 +125,125 @@ public: lean_assert(m_params.size() == m_nparams); } - /** \brief Add all datatype declarations to environment as axioms. + /** \brief Return true if declaration is recursive */ + bool is_rec() { + for (unsigned idx = 0; idx < m_ind_types.size(); idx++) { + inductive_type const & ind_type = m_ind_types[idx]; + for (constructor const & cnstr : ind_type.get_cnstrs()) { + expr t = constructor_type(cnstr); + while (is_pi(t)) { + if (find(binding_domain(t), [&](expr const & e, unsigned) { + if (is_constant(e)) { + for (expr const & I : m_ind_cnsts) + if (const_name(I) == const_name(e)) + return true; + } + return false; + })) { + return true; + } + t = binding_body(t); + } + } + } + return false; + } - We will update them later using `mk_inductive` when we know the exact number of - recursors. */ - void declare_inductive_types_as_constants() { + /** Return list with the names of all inductive datatypes in the mutual declaration. */ + names get_all_names() const { + buffer all_names; for (inductive_type const & ind_type : m_ind_types) { + all_names.push_back(ind_type.get_name()); + } + return names(all_names); + } + + /** \brief Add all datatype declarations to environment. */ + void declare_inductive_types() { + bool rec = is_rec(); + names all = get_all_names(); + for (unsigned idx = 0; idx < m_ind_types.size(); idx++) { + inductive_type const & ind_type = m_ind_types[idx]; name const & n = ind_type.get_name(); - if (m_env.m_constants.find(n)) - throw already_declared_exception(m_env, n); - m_env.m_constants.insert(n, constant_info(mk_axiom(n, m_lparams, ind_type.get_type()))); + buffer cnstr_names; + for (constructor const & cnstr : ind_type.get_cnstrs()) { + cnstr_names.push_back(constructor_name(cnstr)); + } + m_env.add_core(constant_info(inductive_val(n, m_lparams, ind_type.get_type(), m_nparams, m_nindices[idx], + all, names(cnstr_names), rec, m_is_meta))); + } + } + + /** Return type of the parameter at position `i` */ + expr get_param_type(unsigned i) const { + return m_lctx.get_local_decl(m_params[i]).get_type(); + } + + /** \brief Return true iff `t` is a term of the form `I As t` + where `I` is the inductive datatype at position `i` being declared and + `As` are the global parameters of this declaration. */ + bool is_valid_ind_app(expr const & t, unsigned i) { + buffer args; + expr I = get_app_args(t, args); + if (I != m_ind_cnsts[i] || args.size() != m_nparams + m_nindices[i]) + return false; + for (unsigned i = 0; i < m_nparams; i++) { + if (m_params[i] != args[i]) + return false; + } + return true; + } + + /** \brief Check whether the constructor declarations are type correct, parameters are in the expected positions, + constructor fields are in acceptable universe levels, and returns the expected result. + + \brief We do not check positivity and whether it contains valid nested occurrences of + the inductive datatypes being defined. */ + void check_constructor_types() { + for (unsigned idx = 0; idx < m_ind_types.size(); idx++) { + inductive_type const & ind_type = m_ind_types[idx]; + for (constructor const & cnstr : ind_type.get_cnstrs()) { + name const & n = constructor_name(cnstr); + expr t = constructor_type(cnstr); + m_env.check_name(n); + check_no_metavar_no_fvar(m_env, n, t); + tc().check(t, m_lparams); + unsigned i = 0; + local_ctx lctx = m_lctx; + while (is_pi(t)) { + if (i < m_nparams) { + if (!tc(lctx).is_def_eq(binding_domain(t), get_param_type(i))) + throw kernel_exception(m_env, sstream() << "arg #" << (i + 1) << " of '" << n << "' " + << "does not match inductive datatypes parameters'"); + t = instantiate(binding_body(t), m_params[i]); + } else { + expr s = tc(lctx).ensure_type(binding_domain(t)); + // the sort is ok IF + // 1- its level is <= inductive datatype level, OR + // 2- is an inductive predicate + if (!is_geq(m_result_level, sort_level(s)) || is_zero(m_result_level)) { + throw kernel_exception(m_env, sstream() << "universe level of type_of(arg #" << (i + 1) << ") " + << "of '" << n << "' is too big for the corresponding inductive datatype"); + } + expr local = m_lctx.mk_local_decl(m_ngen, binding_name(t), binding_domain(t), binding_info(t)); + t = instantiate(binding_body(t), local); + } + i++; + } + if (!is_valid_ind_app(t, idx)) + throw kernel_exception(m_env, sstream() << "invalid return type for '" << n << "'"); + } + } + } + + void declare_constructors() { + for (unsigned idx = 0; idx < m_ind_types.size(); idx++) { + inductive_type const & ind_type = m_ind_types[idx]; + for (constructor const & cnstr : ind_type.get_cnstrs()) { + name const & n = constructor_name(cnstr); + expr const & t = constructor_type(cnstr); + m_env.add_core(constant_info(constructor_val(n, m_lparams, t, ind_type.get_name(), m_nparams, m_is_meta))); + } } } @@ -180,7 +286,7 @@ public: while (is_pi(type)) { expr fvar = lctx.mk_local_decl(m_ngen, binding_name(type), binding_domain(type), binding_info(type)); if (i >= m_nparams) { - expr s = type_checker(m_env, lctx).ensure_type(binding_domain(type)); + expr s = tc(lctx).ensure_type(binding_domain(type)); if (!is_zero(sort_level(s))) { /* Current argument is not in Prop (i.e., condition 1 failed). We save it in to_check to be able to try condition 2 above. */ @@ -213,7 +319,7 @@ public: } m_elim_level = mk_univ_param(u); } - std::cout << ">> elim_level: " << m_elim_level << "\n"; + // std::cout << ">> elim_level: " << m_elim_level << "\n"; } void init_K_target() { @@ -240,27 +346,14 @@ public: } } - void check_constructor(constructor const & cnstr, unsigned /* idx */) { - check_no_metavar_no_fvar(m_env, constructor_name(cnstr), constructor_type(cnstr)); - type_checker(m_env).check(constructor_type(cnstr), m_lparams); - } - - void check_constructors() { - for (unsigned idx = 0; idx < m_ind_types.size(); idx++) { - inductive_type const & ind_type = m_ind_types[idx]; - for (constructor const & cnstr : ind_type.get_cnstrs()) { - check_constructor(cnstr, idx); - } - } - } - environment operator()() { - dump(); + m_env.check_duplicated_univ_params(m_lparams); check_inductive_types(); - declare_inductive_types_as_constants(); + declare_inductive_types(); + check_constructor_types(); + declare_constructors(); init_elim_level(); init_K_target(); - return m_env; } };