max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/constructions/brec_on): add below and ibelow for new inductive datatype module

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-05 13:59:21 -07:00
parent afb9584a63
commit f335623530
8 changed files with 166 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/frontends/lean/inductive_cmds.cpp
View file

@ -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());
}
}
}

158
src/library/constructions/brec_on.cpp
View file

@ -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<unsigned> is_typeformer_app(buffer<name> const & typeformer_name
return optional<unsigned>();
}
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<expr> 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<expr> args;
buffer<name> 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<expr> 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<expr> minor_args;
minor_type = to_telescope(lctx, ngen, minor_type, minor_args);
buffer<expr> prod_pairs;
for (expr & minor_arg : minor_args) {
buffer<expr> 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);
}
}

8
src/library/constructions/brec_on.h
View file

@ -12,9 +12,13 @@ namespace lean {
<tt>n.below</tt> auxiliary construction for <tt>n.brec_on</t>
(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);
}

8
src/library/inductive_compiler/basic.cpp
View file

@ -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);
}
}

2
src/library/util.cpp
View file

@ -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));
}

4
src/library/util.h
View file

@ -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<expr> & telescope, optional<binder_info> const & binfo);
expr to_telescope(local_ctx & lctx, name_generator & ngen, expr const & type, buffer<expr> & telescope, optional<binder_info> const & binfo = optional<binder_info>());
/** \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<expr> & telescope, optional<binder_info> const & binfo = optional<binder_info>());
@ -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);

2
tests/lean/run/new_inductive.lean
View file

@ -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

2
tests/lean/run/new_inductive2.lean
View file

@ -9,3 +9,5 @@ inductive foo
#print foo
#print foo.rec
set_option pp.all true
#print foo.below