From f335623530e6bbfd1197c31734a215230fa4cebc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Sep 2018 13:59:21 -0700 Subject: [PATCH] feat(library/constructions/brec_on): add `below` and `ibelow` for new inductive datatype module --- src/frontends/lean/inductive_cmds.cpp | 12 +- src/library/constructions/brec_on.cpp | 158 ++++++++++++++++++++--- src/library/constructions/brec_on.h | 8 +- src/library/inductive_compiler/basic.cpp | 8 +- src/library/util.cpp | 2 +- src/library/util.h | 4 +- tests/lean/run/new_inductive.lean | 2 +- tests/lean/run/new_inductive2.lean | 2 + 8 files changed, 166 insertions(+), 30 deletions(-) diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp index bc0e6ba9db..823196d4ab 100644 --- a/src/frontends/lean/inductive_cmds.cpp +++ b/src/frontends/lean/inductive_cmds.cpp @@ -33,6 +33,7 @@ Authors: Daniel Selsam, Leonardo de Moura #include "library/tactic/tactic_evaluator.h" #include "library/constructions/cases_on.h" #include "library/constructions/rec_on.h" +#include "library/constructions/brec_on.h" #include "library/constructions/no_confusion.h" #include "frontends/lean/decl_cmds.h" #include "frontends/lean/decl_util.h" @@ -741,14 +742,17 @@ public: bool has_eq = has_eq_decls(m_env); bool has_heq = has_heq_decls(m_env); bool has_unit = has_punit_decls(m_env); - // bool has_prod = has_pprod_decls(m_env); + bool has_prod = has_pprod_decls(m_env); for (inductive_type const & ind_type : ind_types) { m_env = mk_rec_on(m_env, ind_type.get_name()); - if (has_unit) { + if (has_unit) m_env = mk_cases_on(m_env, ind_type.get_name()); - if (has_eq && has_heq) - m_env = mk_no_confusion(m_env, ind_type.get_name()); + if (has_unit && has_eq && has_heq) + m_env = mk_no_confusion(m_env, ind_type.get_name()); + if (has_unit && has_prod) { + m_env = mk_below(m_env, ind_type.get_name()); + m_env = mk_ibelow(m_env, ind_type.get_name()); } } } diff --git a/src/library/constructions/brec_on.cpp b/src/library/constructions/brec_on.cpp index 935aad401c..4757ce2944 100644 --- a/src/library/constructions/brec_on.cpp +++ b/src/library/constructions/brec_on.cpp @@ -9,8 +9,8 @@ Author: Leonardo de Moura #include "kernel/environment.h" #include "kernel/instantiate.h" #include "kernel/abstract.h" -#include "kernel/old_type_checker.h" -#include "kernel/inductive/inductive.h" +#include "kernel/type_checker.h" +#include "kernel/inductive.h" #include "library/protected.h" #include "library/reducible.h" #include "library/module.h" @@ -19,6 +19,10 @@ Author: Leonardo de Moura #include "library/aux_recursors.h" #include "library/constructions/util.h" +// TODO(Leo): delete following includes +#include "kernel/inductive/inductive.h" +#include "kernel/old_type_checker.h" + namespace lean { static void throw_corrupted(name const & n) { throw exception(sstream() << "error in 'brec_on' generation, '" << n << "' inductive datatype declaration is corrupted"); @@ -37,7 +41,7 @@ static optional is_typeformer_app(buffer const & typeformer_name return optional(); } -static environment mk_below(environment const & env, name const & n, bool ibelow) { +static environment old_mk_below(environment const & env, name const & n, bool ibelow) { if (!is_recursive_datatype(env, n)) return env; if (is_inductive_predicate(env, n) || !can_elim_to_type(env, n)) @@ -64,7 +68,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow // we are eliminating to Prop blvls = tail(lps); rlvl = mk_level_zero(); - ref_type = instantiate_univ_param(rec_info.get_type(), param_id(lvl), mk_level_zero()); + ref_type = instantiate_lparam(rec_info.get_type(), param_id(lvl), mk_level_zero()); } else if (is_reflexive) { blvls = lps; rlvl = get_datatype_level(ind_info.get_type()); @@ -72,7 +76,7 @@ static environment mk_below(environment const & env, name const & n, bool ibelow if (is_max(rlvl) && is_one(max_lhs(rlvl))) rlvl = max_rhs(rlvl); rlvl = mk_max(mk_succ(lvl), rlvl); - ref_type = instantiate_univ_param(rec_info.get_type(), param_id(lvl), mk_succ(lvl)); + ref_type = instantiate_lparam(rec_info.get_type(), param_id(lvl), mk_succ(lvl)); } else { // we can simplify the universe levels for non-reflexive datatypes blvls = lps; @@ -151,15 +155,15 @@ static environment mk_below(environment const & env, name const & n, bool ibelow return add_protected(new_env, below_name); } -environment mk_below(environment const & env, name const & n) { - return mk_below(env, n, false); +environment old_mk_below(environment const & env, name const & n) { + return old_mk_below(env, n, false); } -environment mk_ibelow(environment const & env, name const & n) { - return mk_below(env, n, true); +environment old_mk_ibelow(environment const & env, name const & n) { + return old_mk_below(env, n, true); } -static environment mk_brec_on(environment const & env, name const & n, bool ind) { +static environment old_mk_brec_on(environment const & env, name const & n, bool ind) { if (!is_recursive_datatype(env, n)) return env; if (is_inductive_predicate(env, n) || !can_elim_to_type(env, n)) @@ -191,7 +195,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) blps = tail(lps); blvls = lvls; rlvl = mk_level_zero(); - ref_type = instantiate_univ_param(rec_info.get_type(), param_id(lvl), mk_level_zero()); + ref_type = instantiate_lparam(rec_info.get_type(), param_id(lvl), mk_level_zero()); } else if (is_reflexive) { blps = lps; blvls = cons(lvl, lvls); @@ -202,7 +206,7 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) rlvl = mk_max(mk_succ(lvl), rlvl); // inner_prod, inner_prod_intro, pr1, pr2 do not use the same universe levels for // reflective datatypes. - ref_type = instantiate_univ_param(rec_info.get_type(), param_id(lvl), mk_succ(lvl)); + ref_type = instantiate_lparam(rec_info.get_type(), param_id(lvl), mk_succ(lvl)); } else { // we can simplify the universe levels for non-reflexive datatypes blps = lps; @@ -331,11 +335,133 @@ static environment mk_brec_on(environment const & env, name const & n, bool ind) return add_protected(new_env, brec_on_name); } -environment mk_brec_on(environment const & env, name const & n) { - return mk_brec_on(env, n, false); +environment old_mk_brec_on(environment const & env, name const & n) { + return old_mk_brec_on(env, n, false); } -environment mk_binduction_on(environment const & env, name const & n) { - return mk_brec_on(env, n, true); +environment old_mk_binduction_on(environment const & env, name const & n) { + return old_mk_brec_on(env, n, true); +} + +static environment mk_below(environment const & env, name const & n, bool ibelow) { + if (!is_recursive_datatype(env, n)) + return env; + if (is_inductive_predicate(env, n)) + return env; + local_ctx lctx; + constant_info ind_info = env.get(n); + inductive_val ind_val = ind_info.to_inductive_val(); + name_generator ngen = mk_constructions_name_generator(); + unsigned nparams = ind_val.get_nparams(); + constant_info rec_info = env.get(mk_rec_name(n)); + recursor_val rec_val = rec_info.to_recursor_val(); + unsigned nminors = rec_val.get_nminors(); + unsigned ntypeformers = rec_val.get_nmotives(); + names lps = rec_info.get_lparams(); + bool is_reflexive = ind_val.is_reflexive(); + level lvl = mk_univ_param(head(lps)); + levels lvls = lparams_to_levels(tail(lps)); + names blvls; // universe parameter names of ibelow/below + level rlvl; // universe level of the resultant type + // The arguments of below (ibelow) are the ones in the recursor - minor premises. + // The universe we map to is also different (l+1 for below of reflexive types) and (0 fo ibelow). + expr ref_type; + expr Type_result; + if (ibelow) { + // we are eliminating to Prop + blvls = tail(lps); + rlvl = mk_level_zero(); + ref_type = instantiate_lparam(rec_info.get_type(), param_id(lvl), mk_level_zero()); + } else if (is_reflexive) { + blvls = lps; + rlvl = get_datatype_level(ind_info.get_type()); + // if rlvl is of the form (max 1 l), then rlvl <- l + if (is_max(rlvl) && is_one(max_lhs(rlvl))) + rlvl = max_rhs(rlvl); + rlvl = mk_max(mk_succ(lvl), rlvl); + ref_type = instantiate_lparam(rec_info.get_type(), param_id(lvl), mk_succ(lvl)); + } else { + // we can simplify the universe levels for non-reflexive datatypes + blvls = lps; + rlvl = mk_max(mk_level_one(), lvl); + ref_type = rec_info.get_type(); + } + Type_result = mk_sort(rlvl); + buffer ref_args; + to_telescope(lctx, ngen, ref_type, ref_args); + lean_assert(ref_args.size() != nparams + ntypeformers + nminors + ind_val.get_nindices() + 1); + + // args contains the below/ibelow arguments + buffer args; + buffer typeformer_names; + // add parameters and typeformers + for (unsigned i = 0; i < nparams; i++) + args.push_back(ref_args[i]); + for (unsigned i = nparams; i < nparams + ntypeformers; i++) { + args.push_back(ref_args[i]); + typeformer_names.push_back(fvar_name(ref_args[i])); + } + // we ignore minor premises in below/ibelow + for (unsigned i = nparams + ntypeformers + nminors; i < ref_args.size(); i++) + args.push_back(ref_args[i]); + + // We define below/ibelow using the recursor for this type + levels rec_lvls = cons(mk_succ(rlvl), lvls); + expr rec = mk_constant(rec_info.get_name(), rec_lvls); + for (unsigned i = 0; i < nparams; i++) + rec = mk_app(rec, args[i]); + // add type formers + for (unsigned i = nparams; i < nparams + ntypeformers; i++) { + buffer targs; + to_telescope(lctx, ngen, lctx.get_type(args[i]), targs); + rec = mk_app(rec, lctx.mk_lambda(targs, Type_result)); + } + // add minor premises + for (unsigned i = nparams + ntypeformers; i < nparams + ntypeformers + nminors; i++) { + expr minor = ref_args[i]; + expr minor_type = lctx.get_type(minor); + buffer minor_args; + minor_type = to_telescope(lctx, ngen, minor_type, minor_args); + buffer prod_pairs; + for (expr & minor_arg : minor_args) { + buffer minor_arg_args; + expr minor_arg_type = to_telescope(env, lctx, ngen, lctx.get_type(minor_arg), minor_arg_args); + if (is_typeformer_app(typeformer_names, minor_arg_type)) { + expr fst = lctx.get_type(minor_arg); + minor_arg = lctx.mk_local_decl(ngen, lctx.get_local_decl(minor_arg).get_user_name(), lctx.mk_pi(minor_arg_args, Type_result)); + expr snd = lctx.mk_pi(minor_arg_args, mk_app(minor_arg, minor_arg_args)); + type_checker tc(env, lctx); + prod_pairs.push_back(mk_pprod(tc, fst, snd, ibelow)); + } + } + type_checker tc(env, lctx); + expr new_arg = foldr([&](expr const & a, expr const & b) { return mk_pprod(tc, a, b, ibelow); }, + [&]() { return mk_unit(rlvl, ibelow); }, + prod_pairs.size(), prod_pairs.data()); + rec = mk_app(rec, lctx.mk_lambda(minor_args, new_arg)); + } + + // add indices and major premise + for (unsigned i = nparams + ntypeformers; i < args.size(); i++) { + rec = mk_app(rec, args[i]); + } + + name below_name = ibelow ? name{n, "ibelow"} : name{n, "below"}; + expr below_type = lctx.mk_pi(args, Type_result); + expr below_value = lctx.mk_lambda(args, rec); + + declaration new_d = mk_definition_inferring_meta(env, below_name, blvls, below_type, below_value, + reducibility_hints::mk_abbreviation()); + environment new_env = module::add(env, new_d); + new_env = set_reducible(new_env, below_name, reducible_status::Reducible, true); + return add_protected(new_env, below_name); +} + +environment mk_below(environment const & env, name const & n) { + return mk_below(env, n, false); +} + +environment mk_ibelow(environment const & env, name const & n) { + return mk_below(env, n, true); } } diff --git a/src/library/constructions/brec_on.h b/src/library/constructions/brec_on.h index 8103be656c..bf24facbf6 100644 --- a/src/library/constructions/brec_on.h +++ b/src/library/constructions/brec_on.h @@ -12,9 +12,13 @@ namespace lean { n.below auxiliary construction for n.brec_on (aka below recursion on) to the environment. */ +environment old_mk_below(environment const & env, name const & n); +environment old_mk_ibelow(environment const & env, name const & n); + +environment old_mk_brec_on(environment const & env, name const & n); +environment old_mk_binduction_on(environment const & env, name const & n); + environment mk_below(environment const & env, name const & n); environment mk_ibelow(environment const & env, name const & n); -environment mk_brec_on(environment const & env, name const & n); -environment mk_binduction_on(environment const & env, name const & n); } diff --git a/src/library/inductive_compiler/basic.cpp b/src/library/inductive_compiler/basic.cpp index c010ee69a9..f92ccd0746 100644 --- a/src/library/inductive_compiler/basic.cpp +++ b/src/library/inductive_compiler/basic.cpp @@ -96,17 +96,17 @@ class add_basic_inductive_decl_fn { if (gen_brec_on && has_prod) { lean_trace(name({"inductive_compiler"}), tout() << ">> generate below\n";); - m_env = mk_below(m_env, ind_name); + m_env = old_mk_below(m_env, ind_name); lean_trace(name({"inductive_compiler"}), tout() << ">> generate ibelow\n";); - m_env = mk_ibelow(m_env, ind_name); + m_env = old_mk_ibelow(m_env, ind_name); } } if (gen_brec_on && has_unit && has_prod) { lean_trace(name({"inductive_compiler"}), tout() << ">> generate brec_on\n";); - m_env = mk_brec_on(m_env, ind_name); + m_env = old_mk_brec_on(m_env, ind_name); lean_trace(name({"inductive_compiler"}), tout() << ">> generate binduction_on\n";); - m_env = mk_binduction_on(m_env, ind_name); + m_env = old_mk_binduction_on(m_env, ind_name); } } diff --git a/src/library/util.cpp b/src/library/util.cpp index 97afc641e2..a7fed7698e 100644 --- a/src/library/util.cpp +++ b/src/library/util.cpp @@ -388,7 +388,7 @@ void get_constructor_rec_arg_mask(environment const & env, name const & n, buffe get_num_inductive_hypotheses_for(env, n, rec_mask); } -expr instantiate_univ_param (expr const & e, name const & p, level const & l) { +expr instantiate_lparam (expr const & e, name const & p, level const & l) { return instantiate_lparams(e, names(p), levels(l)); } diff --git a/src/library/util.h b/src/library/util.h index d0ac17d769..3f5f319a01 100644 --- a/src/library/util.h +++ b/src/library/util.h @@ -171,7 +171,7 @@ level get_datatype_level(expr const & ind_type); and store them in telescope and updates . If `binfo` is provided, then the free variables are annotated with the given `binder_info`, otherwise the procedure uses the one attached in the domain. The procedure returns the "body" of type. */ -expr to_telescope(local_ctx & lctx, name_generator & ngen, expr const & type, buffer & telescope, optional const & binfo); +expr to_telescope(local_ctx & lctx, name_generator & ngen, expr const & type, buffer & telescope, optional const & binfo = optional()); /** \brief Similar to previous procedure, but uses whnf to check whether `type` reduces to `Pi` or not. */ expr to_telescope(environment const & env, local_ctx & lctx, name_generator & ngen, expr type, buffer & telescope, optional const & binfo = optional()); @@ -179,7 +179,7 @@ expr to_telescope(environment const & env, local_ctx & lctx, name_generator & ng /** \brief Update the result sort of the given type */ expr update_result_sort(expr t, level const & l); -expr instantiate_univ_param (expr const & e, name const & p, level const & l); +expr instantiate_lparam (expr const & e, name const & p, level const & l); expr mk_true(); bool is_true(expr const & e); diff --git a/tests/lean/run/new_inductive.lean b/tests/lean/run/new_inductive.lean index 8fe173bc08..bf3b15521e 100644 --- a/tests/lean/run/new_inductive.lean +++ b/tests/lean/run/new_inductive.lean @@ -22,7 +22,7 @@ inductive term (α : Type) (β : Type) | foo (p : nat → my_pair term (my_list term)) (n : β) : my_list (my_list term) → term #print term - +#print term.below #check @term.cases_on #print term.no_confusion_type #print term.no_confusion diff --git a/tests/lean/run/new_inductive2.lean b/tests/lean/run/new_inductive2.lean index de4f8d7e9c..1422ea7018 100644 --- a/tests/lean/run/new_inductive2.lean +++ b/tests/lean/run/new_inductive2.lean @@ -9,3 +9,5 @@ inductive foo #print foo #print foo.rec +set_option pp.all true +#print foo.below