feat(library/user_recursors): generalize acceptable use-defined recursors
see issue #492
This commit is contained in:
Leonardo de Moura
parent
62082c72a8
commit
c61c049152
15 changed files with 230 additions and 128 deletions
|
|
@ -123,11 +123,12 @@
|
|||
"\[irreducible\]" "\[semireducible\]" "\[quasireducible\]" "\[wf\]"
|
||||
"\[whnf\]" "\[multiple-instances\]" "\[none\]"
|
||||
"\[decls\]" "\[declarations\]" "\[coercions\]" "\[classes\]"
|
||||
"\[symm\]" "\[subst\]" "\[refl\]" "\[trans\]" "\[recursor\]"
|
||||
"\[symm\]" "\[subst\]" "\[refl\]" "\[trans\]"
|
||||
"\[notations\]" "\[abbreviations\]" "\[begin-end-hints\]" "\[tactic-hints\]"
|
||||
"\[reduce-hints\]" "\[unfold-hints\]" "\[aliases\]" "\[eqv\]" "\[localrefinfo\]"))
|
||||
. 'font-lock-doc-face)
|
||||
(,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
|
||||
(,(rx "\[recursor" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
|
||||
(,(rx "\[unfold-c" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
|
||||
;; tactics
|
||||
("cases[ \t\n]+[^ \t\n]+[ \t\n]+\\(with\\)" (1 'font-lock-constant-face))
|
||||
|
|
|
|||
|
|
@ -230,17 +230,30 @@ static void print_inductive(parser & p, name const & n, pos_info const & pos) {
|
|||
|
||||
static void print_recursor_info(parser & p) {
|
||||
name c = p.check_constant_next("invalid 'print [recursor]', constant expected");
|
||||
auto out = p.regular_stream();
|
||||
recursor_info info = get_recursor_info(p.env(), c);
|
||||
p.regular_stream() << "recursor information\n"
|
||||
<< " num. parameters: " << info.get_num_params() << "\n"
|
||||
<< " num. indices: " << info.get_num_indices() << "\n";
|
||||
out << "recursor information\n"
|
||||
<< " num. parameters: " << info.get_num_params() << "\n"
|
||||
<< " num. indices: " << info.get_num_indices() << "\n";
|
||||
if (auto r = info.get_motive_univ_pos())
|
||||
p.regular_stream() << " motive univ. pos. : " << *r << "\n";
|
||||
out << " motive univ. pos.: " << *r << "\n";
|
||||
else
|
||||
p.regular_stream() << " recursor eliminate only to Prop\n";
|
||||
p.regular_stream() << " motive pos.: " << info.get_motive_pos() << "\n"
|
||||
<< " major premise pos.: " << info.get_major_pos() << "\n"
|
||||
<< " dep. elimination: " << info.has_dep_elim() << "\n";
|
||||
out << " recursor eliminate only to Prop\n";
|
||||
out << " motive pos.: " << info.get_motive_pos() + 1 << "\n"
|
||||
<< " major premise pos.: " << info.get_major_pos() + 1 << "\n"
|
||||
<< " dep. elimination: " << info.has_dep_elim() << "\n";
|
||||
if (info.get_num_params() > 0) {
|
||||
out << " parameters pos. at major:";
|
||||
for (unsigned p : info.get_params_pos())
|
||||
out << " " << p+1;
|
||||
out << "\n";
|
||||
}
|
||||
if (info.get_num_indices() > 0) {
|
||||
out << " indices pos. at major: ";
|
||||
for (unsigned p : info.get_indices_pos())
|
||||
out << " " << p+1;
|
||||
out << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
bool print_constant(parser & p, char const * kind, declaration const & d) {
|
||||
|
|
@ -406,6 +419,7 @@ environment print_cmd(parser & p) {
|
|||
print_inductive(p, c, pos);
|
||||
} else if (p.curr_is_token(get_recursor_tk())) {
|
||||
p.next();
|
||||
p.check_token_next(get_rbracket_tk(), "invalid 'print [recursor]', ']' expected");
|
||||
print_recursor_info(p);
|
||||
} else if (print_polymorphic(p)) {
|
||||
} else {
|
||||
|
|
|
|||
|
|
@ -361,6 +361,7 @@ struct decl_attributes {
|
|||
bool m_refl;
|
||||
bool m_subst;
|
||||
bool m_recursor;
|
||||
optional<unsigned> m_recursor_major_pos;
|
||||
optional<unsigned> m_priority;
|
||||
optional<unsigned> m_unfold_c_hint;
|
||||
|
||||
|
|
@ -513,6 +514,13 @@ struct decl_attributes {
|
|||
m_subst = true;
|
||||
} else if (p.curr_is_token(get_recursor_tk())) {
|
||||
p.next();
|
||||
if (!p.curr_is_token(get_rbracket_tk())) {
|
||||
unsigned r = p.parse_small_nat();
|
||||
if (r == 0)
|
||||
throw parser_error("invalid '[recursor]' attribute, value must be greater than 0", pos);
|
||||
m_recursor_major_pos = r - 1;
|
||||
}
|
||||
p.check_token_next(get_rbracket_tk(), "invalid 'recursor', ']' expected");
|
||||
m_recursor = true;
|
||||
} else {
|
||||
break;
|
||||
|
|
@ -570,7 +578,7 @@ struct decl_attributes {
|
|||
if (m_subst)
|
||||
env = add_subst(env, d, m_persistent);
|
||||
if (m_recursor)
|
||||
env = add_user_recursor(env, d, m_persistent);
|
||||
env = add_user_recursor(env, d, m_recursor_major_pos, m_persistent);
|
||||
if (m_is_class)
|
||||
env = add_class(env, d, m_persistent);
|
||||
if (m_has_multiple_instances)
|
||||
|
|
|
|||
|
|
@ -107,7 +107,7 @@ void init_token_table(token_table & t) {
|
|||
"definition", "example", "coercion", "abbreviation",
|
||||
"variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
|
||||
"[none]", "[class]", "[coercion]", "[reducible]", "[irreducible]", "[semireducible]", "[quasireducible]",
|
||||
"[parsing-only]", "[multiple-instances]", "[symm]", "[trans]", "[refl]", "[subst]", "[recursor]",
|
||||
"[parsing-only]", "[multiple-instances]", "[symm]", "[trans]", "[refl]", "[subst]", "[recursor",
|
||||
"evaluate", "check", "eval", "[wf]", "[whnf]", "[priority", "[unfold-f]",
|
||||
"[constructor]", "[unfold-c", "print",
|
||||
"end", "namespace", "section", "prelude", "help",
|
||||
|
|
@ -117,7 +117,8 @@ void init_token_table(token_table & t) {
|
|||
"exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
|
||||
"add_begin_end_tactic", "set_begin_end_tactic", "instance", "class",
|
||||
"multiple_instances", "find_decl", "attribute", "persistent",
|
||||
"include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq", nullptr};
|
||||
"include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq",
|
||||
nullptr};
|
||||
|
||||
pair<char const *, char const *> aliases[] =
|
||||
{{g_lambda_unicode, "fun"}, {"forall", "Pi"}, {g_forall_unicode, "Pi"}, {g_pi_unicode, "Pi"},
|
||||
|
|
|
|||
|
|
@ -244,7 +244,7 @@ void initialize_tokens() {
|
|||
g_trans_tk = new name{"[trans]"};
|
||||
g_refl_tk = new name{"[refl]"};
|
||||
g_subst_tk = new name{"[subst]"};
|
||||
g_recursor_tk = new name{"[recursor]"};
|
||||
g_recursor_tk = new name{"[recursor"};
|
||||
g_attribute_tk = new name{"attribute"};
|
||||
g_with_tk = new name{"with"};
|
||||
g_class_tk = new name{"[class]"};
|
||||
|
|
|
|||
|
|
@ -106,7 +106,7 @@ symm [symm]
|
|||
trans [trans]
|
||||
refl [refl]
|
||||
subst [subst]
|
||||
recursor [recursor]
|
||||
recursor [recursor
|
||||
attribute attribute
|
||||
with with
|
||||
class [class]
|
||||
|
|
|
|||
|
|
@ -22,20 +22,25 @@ bool recursor_info::is_minor(unsigned pos) const {
|
|||
return true;
|
||||
}
|
||||
|
||||
recursor_info::recursor_info(name const & r, name const & I, unsigned num_params, unsigned num_indices, unsigned major,
|
||||
optional<unsigned> const & motive_univ_pos, bool dep_elim):
|
||||
m_recursor(r), m_type_name(I), m_num_params(num_params), m_num_indices(num_indices), m_major_pos(major),
|
||||
m_motive_univ_pos(motive_univ_pos), m_dep_elim(dep_elim) {}
|
||||
recursor_info::recursor_info(name const & r, name const & I, optional<unsigned> const & motive_univ_pos,
|
||||
bool dep_elim, unsigned major_pos, list<unsigned> const & params_pos,
|
||||
list<unsigned> const & indices_pos):
|
||||
m_recursor(r), m_type_name(I), m_motive_univ_pos(motive_univ_pos), m_dep_elim(dep_elim),
|
||||
m_major_pos(major_pos), m_params_pos(params_pos), m_indices_pos(indices_pos) {}
|
||||
recursor_info::recursor_info() {}
|
||||
|
||||
void recursor_info::write(serializer & s) const {
|
||||
s << m_recursor << m_type_name << m_num_params << m_num_indices << m_major_pos << m_motive_univ_pos << m_dep_elim;
|
||||
s << m_recursor << m_type_name << m_motive_univ_pos << m_dep_elim << m_major_pos;
|
||||
write_list(s, m_params_pos);
|
||||
write_list(s, m_indices_pos);
|
||||
}
|
||||
|
||||
recursor_info recursor_info::read(deserializer & d) {
|
||||
recursor_info info;
|
||||
d >> info.m_recursor >> info.m_type_name >> info.m_num_params >> info.m_num_indices >> info.m_major_pos
|
||||
>> info.m_motive_univ_pos >> info.m_dep_elim;
|
||||
d >> info.m_recursor >> info.m_type_name >> info.m_motive_univ_pos >> info.m_dep_elim
|
||||
>> info.m_major_pos;
|
||||
info.m_params_pos = read_list<unsigned>(d);
|
||||
info.m_indices_pos = read_list<unsigned>(d);
|
||||
return info;
|
||||
}
|
||||
|
||||
|
|
@ -47,30 +52,19 @@ static void throw_invalid_motive(expr const & C) {
|
|||
"and I is a constant");
|
||||
}
|
||||
|
||||
static void throw_invalid_major(buffer<expr> const & tele, expr const & I, unsigned num_params,
|
||||
unsigned num_indices, unsigned major_pos) {
|
||||
sstream msg;
|
||||
msg << "invalid user defined recursor, major premise '" << tele[major_pos] << "' is expected to have type " << I;
|
||||
for (unsigned i = 0; i < num_params; i++)
|
||||
msg << " " << tele[i];
|
||||
for (unsigned i = major_pos - num_indices; i < major_pos; i++)
|
||||
msg << " " << tele[i];
|
||||
throw exception(msg);
|
||||
}
|
||||
|
||||
recursor_info mk_recursor_info(environment const & env, name const & r) {
|
||||
recursor_info mk_recursor_info(environment const & env, name const & r, optional<unsigned> const & given_major_pos) {
|
||||
if (auto I = inductive::is_elim_rule(env, r)) {
|
||||
if (*inductive::get_num_type_formers(env, *I) > 1)
|
||||
throw exception(sstream() << "unsupported recursor '" << r << "', it has multiple motives");
|
||||
optional<unsigned> motive_univ_pos;
|
||||
if (env.get(name(*I, "rec")).get_num_univ_params() != env.get(name(*I)).get_num_univ_params())
|
||||
motive_univ_pos = 0;
|
||||
return recursor_info(r, *I,
|
||||
*inductive::get_num_params(env, *I),
|
||||
*inductive::get_num_indices(env, *I),
|
||||
*inductive::get_elim_major_idx(env, r),
|
||||
motive_univ_pos,
|
||||
inductive::has_dep_elim(env, *I));
|
||||
unsigned major_pos = *inductive::get_elim_major_idx(env, r);
|
||||
unsigned num_indices = *inductive::get_num_indices(env, *I);
|
||||
list<unsigned> params_pos = mk_list_range(0, *inductive::get_num_params(env, *I));
|
||||
list<unsigned> indices_pos = mk_list_range(major_pos - num_indices, major_pos);
|
||||
return recursor_info(r, *I, motive_univ_pos, inductive::has_dep_elim(env, *I),
|
||||
major_pos, params_pos, indices_pos);
|
||||
}
|
||||
declaration d = env.get(r);
|
||||
type_checker tc(env);
|
||||
|
|
@ -78,22 +72,99 @@ recursor_info mk_recursor_info(environment const & env, name const & r) {
|
|||
expr rtype = to_telescope(tc, d.get_type(), tele);
|
||||
buffer<expr> C_args;
|
||||
expr C = get_app_args(rtype, C_args);
|
||||
if (!is_local(C) || !std::all_of(C_args.begin(), C_args.end(), is_local) || C_args.empty()) {
|
||||
throw exception("invalid user defined recursor, result type must be of the form (C i t), "
|
||||
"where C and t are bound variables, and i is a (possibly empty) sequence of bound variables");
|
||||
if (!is_local(C) || !std::all_of(C_args.begin(), C_args.end(), is_local)) {
|
||||
throw exception("invalid user defined recursor, result type must be of the form (C t), "
|
||||
"where C is a bound variable, and t is a (possibly empty) sequence of bound variables");
|
||||
}
|
||||
unsigned num_indices = C_args.size() - 1;
|
||||
|
||||
// Compute number of parameters.
|
||||
// We assume a parameter is anything that occurs before the motive.
|
||||
unsigned num_params = 0;
|
||||
for (expr const & x : tele) {
|
||||
if (mlocal_name(x) == mlocal_name(C))
|
||||
break;
|
||||
num_params++;
|
||||
}
|
||||
|
||||
// Locate major premise, and check whether the recursor supports dependent elimination or not.
|
||||
expr major;
|
||||
unsigned major_pos = 0;
|
||||
bool dep_elim;
|
||||
if (given_major_pos) {
|
||||
if (*given_major_pos >= tele.size())
|
||||
throw exception(sstream() << "invalid user defined recursor, invalid major premise position, "
|
||||
"recursor has only " << tele.size() << "arguments");
|
||||
major = tele[*given_major_pos];
|
||||
major_pos = *given_major_pos;
|
||||
if (!C_args.empty() && tc.is_def_eq(C_args.back(), major).first)
|
||||
dep_elim = true;
|
||||
else
|
||||
dep_elim = false;
|
||||
} else {
|
||||
major = C_args.back();
|
||||
dep_elim = true;
|
||||
for (expr const & x : tele) {
|
||||
if (tc.is_def_eq(x, major).first)
|
||||
break;
|
||||
major_pos++;
|
||||
}
|
||||
}
|
||||
|
||||
// Number of indices
|
||||
unsigned num_indices = C_args.size();
|
||||
if (dep_elim)
|
||||
num_indices--; // when we have dependent elimination, the last element is the major premise.
|
||||
if (major_pos < num_indices)
|
||||
throw exception(sstream() << "invalid user defined recursor, indices must occur before major premise '"
|
||||
<< major << "'");
|
||||
|
||||
buffer<expr> I_args;
|
||||
expr I = get_app_args(mlocal_type(major), I_args);
|
||||
if (!is_constant(I)) {
|
||||
throw exception(sstream() << "invalid user defined recursor, type of the major premise '" << major
|
||||
<< "' must be for the form (I ...), where I is a constant");
|
||||
}
|
||||
|
||||
// Store position of the recursor parameters in the major premise.
|
||||
buffer<unsigned> params_pos;
|
||||
for (unsigned i = 0; i < num_params; i++) {
|
||||
expr const & A = tele[i];
|
||||
unsigned j = 0;
|
||||
for (; j < I_args.size(); j++) {
|
||||
if (tc.is_def_eq(I_args[j], A).first)
|
||||
break;
|
||||
}
|
||||
if (j == I_args.size()) {
|
||||
throw exception(sstream() << "invalid user defined recursor, type of the major premise '" << major
|
||||
<< "' does not contain the recursor parameter '" << A << "'");
|
||||
}
|
||||
params_pos.push_back(j);
|
||||
}
|
||||
|
||||
// Store position of the recursor indices in the major premise
|
||||
buffer<unsigned> indices_pos;
|
||||
for (unsigned i = major_pos - num_indices; i < major_pos; i++) {
|
||||
expr const & idx = tele[i];
|
||||
unsigned j = 0;
|
||||
for (; j < I_args.size(); j++) {
|
||||
if (tc.is_def_eq(I_args[j], idx).first)
|
||||
break;
|
||||
}
|
||||
if (j == I_args.size()) {
|
||||
throw exception(sstream() << "invalid user defined recursor, type of the major premise '" << major
|
||||
<< "' does not contain the recursor index '" << idx << "'");
|
||||
}
|
||||
indices_pos.push_back(j);
|
||||
}
|
||||
|
||||
|
||||
buffer<expr> C_tele;
|
||||
expr C_rtype = to_telescope(tc, mlocal_type(C), C_tele);
|
||||
if (!is_sort(C_rtype) || C_tele.size() != C_args.size()) {
|
||||
throw_invalid_motive(C);
|
||||
}
|
||||
// Calculate position of the motive's universe.
|
||||
// Remark: if we are in the standard environment, then the motive may be a proposition, and be fixed at 0.
|
||||
// The following pragma is for avoiding gcc bogus warning
|
||||
#if defined(__GNUC__) && !defined(__CLANG__)
|
||||
#pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
|
||||
|
|
@ -120,52 +191,8 @@ recursor_info mk_recursor_info(environment const & env, name const & r) {
|
|||
lean_assert(*C_univ_pos < length(d.get_univ_params()));
|
||||
}
|
||||
|
||||
buffer<expr> I_args;
|
||||
expr I = get_app_args(mlocal_type(C_tele.back()), I_args);
|
||||
if (!is_constant(I) || I_args.size() != num_params + num_indices) {
|
||||
throw_invalid_motive(C);
|
||||
}
|
||||
for (unsigned i = 0; i < num_params; i++) {
|
||||
if (!tc.is_def_eq(I_args[i], tele[i]).first)
|
||||
throw_invalid_motive(C);
|
||||
}
|
||||
for (unsigned i = 0; i < num_indices; i++) {
|
||||
if (!tc.is_def_eq(I_args[num_params + i], C_tele[i]).first) {
|
||||
throw_invalid_motive(C);
|
||||
}
|
||||
}
|
||||
expr const & major = C_args.back();
|
||||
unsigned major_pos = 0;
|
||||
for (expr const & x : tele) {
|
||||
if (mlocal_name(x) == mlocal_name(major))
|
||||
break;
|
||||
major_pos++;
|
||||
}
|
||||
lean_assert(major_pos < tele.size());
|
||||
if (major_pos < num_indices)
|
||||
throw exception(sstream() << "invalid user defined recursor, indices must occur before major premise '"
|
||||
<< major << "'");
|
||||
recursor_info info(r, const_name(I), num_params, num_indices, major_pos, C_univ_pos, true);
|
||||
unsigned first_index_pos = info.get_first_index_pos();
|
||||
for (unsigned i = 0; i < num_indices; i++) {
|
||||
if (!tc.is_def_eq(tele[first_index_pos+i], C_args[i]).first) {
|
||||
throw exception(sstream() << "invalid user defined recursor, index '" << C_args[i]
|
||||
<< "' expected, but got '" << tele[i] << "'");
|
||||
}
|
||||
}
|
||||
buffer<expr> I_args_major;
|
||||
expr I_major = get_app_args(mlocal_type(tele[major_pos]), I_args_major);
|
||||
if (I != I_major)
|
||||
throw_invalid_major(tele, I, num_params, num_indices, major_pos);
|
||||
for (unsigned i = 0; i < num_params; i++) {
|
||||
if (!tc.is_def_eq(I_args_major[i], tele[i]).first)
|
||||
throw_invalid_major(tele, I, num_params, num_indices, major_pos);
|
||||
}
|
||||
for (unsigned i = 0; i < num_indices; i++) {
|
||||
if (!tc.is_def_eq(I_args_major[num_params + i], tele[first_index_pos + i]).first)
|
||||
throw_invalid_major(tele, I, num_params, num_indices, major_pos);
|
||||
}
|
||||
return info;
|
||||
return recursor_info(r, const_name(I), C_univ_pos, dep_elim, major_pos,
|
||||
to_list(params_pos), to_list(indices_pos));
|
||||
}
|
||||
|
||||
struct recursor_state {
|
||||
|
|
@ -214,17 +241,18 @@ struct recursor_config {
|
|||
template class scoped_ext<recursor_config>;
|
||||
typedef scoped_ext<recursor_config> recursor_ext;
|
||||
|
||||
environment add_user_recursor(environment const & env, name const & r, bool persistent) {
|
||||
environment add_user_recursor(environment const & env, name const & r, optional<unsigned> const & major_pos,
|
||||
bool persistent) {
|
||||
if (inductive::is_elim_rule(env, r))
|
||||
throw exception(sstream() << "invalid user defined recursor, '" << r << "' is a builtin recursor");
|
||||
recursor_info info = mk_recursor_info(env, r);
|
||||
recursor_info info = mk_recursor_info(env, r, major_pos);
|
||||
return recursor_ext::add_entry(env, get_dummy_ios(), info, persistent);
|
||||
}
|
||||
|
||||
recursor_info get_recursor_info(environment const & env, name const & r) {
|
||||
if (auto info = recursor_ext::get_state(env).m_recursors.find(r))
|
||||
return *info;
|
||||
return mk_recursor_info(env, r);
|
||||
return mk_recursor_info(env, r, optional<unsigned>());
|
||||
}
|
||||
|
||||
list<name> get_recursors_for(environment const & env, name const & I) {
|
||||
|
|
|
|||
|
|
@ -11,25 +11,33 @@ namespace lean {
|
|||
class recursor_info {
|
||||
name m_recursor;
|
||||
name m_type_name;
|
||||
unsigned m_num_params;
|
||||
unsigned m_num_indices;
|
||||
unsigned m_major_pos;
|
||||
optional<unsigned> m_motive_univ_pos; // if none, then recursor can only eliminate to Prop
|
||||
bool m_dep_elim;
|
||||
unsigned m_major_pos;
|
||||
list<unsigned> m_params_pos; // position of the recursor parameters in the major premise
|
||||
list<unsigned> m_indices_pos; // position of the recursor indices in the major premise
|
||||
|
||||
public:
|
||||
recursor_info(name const & r, name const & I, unsigned num_params, unsigned num_indices, unsigned major,
|
||||
optional<unsigned> const & motive_univ_pos, bool dep_elim);
|
||||
recursor_info(name const & r, name const & I,
|
||||
optional<unsigned> const & motive_univ_pos,
|
||||
bool dep_elim,
|
||||
unsigned major_pos,
|
||||
list<unsigned> const & params_pos,
|
||||
list<unsigned> const & indices_pos);
|
||||
recursor_info();
|
||||
|
||||
name const & get_name() const { return m_recursor; }
|
||||
name const & get_type_name() const { return m_type_name; }
|
||||
unsigned get_num_params() const { return m_num_params; }
|
||||
unsigned get_num_indices() const { return m_num_indices; }
|
||||
unsigned get_motive_pos() const { return m_num_params; }
|
||||
unsigned get_first_index_pos() const { return m_major_pos - m_num_indices; }
|
||||
unsigned get_num_params() const { return length(m_params_pos); }
|
||||
unsigned get_num_indices() const { return length(m_indices_pos); }
|
||||
unsigned get_motive_pos() const { return get_num_params(); }
|
||||
unsigned get_first_index_pos() const { return m_major_pos - get_num_indices(); }
|
||||
unsigned get_major_pos() const { return m_major_pos; }
|
||||
optional<unsigned> get_motive_univ_pos() const { return m_motive_univ_pos; }
|
||||
optional<unsigned> const & get_motive_univ_pos() const { return m_motive_univ_pos; }
|
||||
/** \brief Return position of the recursor parameters in the major premise. */
|
||||
list<unsigned> const & get_params_pos() const { return m_params_pos; }
|
||||
/** \brief Return position of the recursor indices in the major premise. */
|
||||
list<unsigned> const & get_indices_pos() const { return m_indices_pos; }
|
||||
bool has_dep_elim() const { return m_dep_elim; }
|
||||
bool is_minor(unsigned pos) const;
|
||||
|
||||
|
|
@ -37,7 +45,7 @@ public:
|
|||
static recursor_info read(deserializer & d);
|
||||
};
|
||||
|
||||
environment add_user_recursor(environment const & env, name const & r, bool persistent);
|
||||
environment add_user_recursor(environment const & env, name const & r, optional<unsigned> const & major_pos, bool persistent);
|
||||
recursor_info get_recursor_info(environment const & env, name const & r);
|
||||
list<name> get_recursors_for(environment const & env, name const & I);
|
||||
|
||||
|
|
|
|||
|
|
@ -4,6 +4,6 @@ add_library(util trace.cpp debug.cpp name.cpp name_set.cpp
|
|||
realpath.cpp script_state.cpp script_exception.cpp rb_map.cpp
|
||||
lua.cpp luaref.cpp lua_named_param.cpp stackinfo.cpp lean_path.cpp
|
||||
serializer.cpp lbool.cpp thread_script_state.cpp bitap_fuzzy_search.cpp
|
||||
init_module.cpp thread.cpp memory_pool.cpp utf8.cpp name_map.cpp)
|
||||
init_module.cpp thread.cpp memory_pool.cpp utf8.cpp name_map.cpp list_fn.cpp)
|
||||
|
||||
target_link_libraries(util ${LEAN_LIBS})
|
||||
|
|
|
|||
|
|
@ -302,4 +302,6 @@ template<typename T>
|
|||
T const & get_ith(list<T> const & l, unsigned idx) {
|
||||
return idx == 0 ? head(l) : get_ith(tail(l), idx - 1);
|
||||
}
|
||||
|
||||
list<unsigned> mk_list_range(unsigned from, unsigned to);
|
||||
}
|
||||
|
|
|
|||
14
tests/lean/hott/id_tac5.hlean
Normal file
14
tests/lean/hott/id_tac5.hlean
Normal file
|
|
@ -0,0 +1,14 @@
|
|||
open equiv
|
||||
|
||||
constant rec_on_ua {A B : Type} {P : A ≃ B → Type}
|
||||
(f : A ≃ B) (H : Π(q : A = B), P (equiv_of_eq q)) : P f
|
||||
|
||||
set_option pp.universes true
|
||||
set_option pp.implicit true
|
||||
set_option pp.notation false
|
||||
|
||||
check @rec_on_ua
|
||||
|
||||
attribute rec_on_ua [recursor]
|
||||
|
||||
print [recursor] rec_on_ua
|
||||
12
tests/lean/hott/ind_tac3.hlean
Normal file
12
tests/lean/hott/ind_tac3.hlean
Normal file
|
|
@ -0,0 +1,12 @@
|
|||
import cubical.pathover
|
||||
open cubical
|
||||
|
||||
set_option pp.implicit true
|
||||
set_option pp.universes true
|
||||
set_option pp.notation false
|
||||
|
||||
check @idp_rec_on
|
||||
|
||||
attribute idp_rec_on [recursor]
|
||||
|
||||
print [recursor] idp_rec_on
|
||||
6
tests/lean/hott/ind_tac4.hlean
Normal file
6
tests/lean/hott/ind_tac4.hlean
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
import hit.circle
|
||||
open circle
|
||||
|
||||
attribute circle.elim_on [recursor 2]
|
||||
|
||||
print [recursor] circle.elim_on
|
||||
5
tests/lean/run/ind_tac1.lean
Normal file
5
tests/lean/run/ind_tac1.lean
Normal file
|
|
@ -0,0 +1,5 @@
|
|||
check @heq.rec_on
|
||||
|
||||
attribute heq.rec_on [recursor 6]
|
||||
|
||||
print [recursor] heq.rec_on
|
||||
|
|
@ -1,43 +1,46 @@
|
|||
urec.lean:3:0: error: invalid user defined recursor, result type must be of the form (C i t), where C and t are bound variables, and i is a (possibly empty) sequence of bound variables
|
||||
urec.lean:3:0: error: invalid user defined recursor, result type must be of the form (C t), where C is a bound variable, and t is a (possibly empty) sequence of bound variables
|
||||
urec.lean:5:0: error: invalid user defined recursor, 'nat.rec' is a builtin recursor
|
||||
urec.lean:19:0: error: invalid user defined recursor, motive 'C' must have a type of the form (C : Pi (i : B A), I A i -> Type), where A is (possibly empty) sequence of bound variables (aka parameters), (i : B A) is a (possibly empty) telescope (aka indices), and I is a constant
|
||||
urec.lean:23:0: error: invalid user defined recursor, resultant type of minor premise 'a' must be of the form (M ...)
|
||||
urec.lean:19:0: error: invalid user defined recursor, type of the major premise 'a' must be for the form (I ...), where I is a constant
|
||||
myrec.{l_1 l_2} :
|
||||
Π (A : Type.{l_1}) (M : list.{l_1} A → Type.{l_2}) (l : list.{l_1} A),
|
||||
M (@nil.{l_1} A) → (Π (a : A), M [a]) → (Π (a₁ a₂ : A), M [a₁, a₂]) → M l
|
||||
recursor information
|
||||
num. parameters: 1
|
||||
num. indices: 0
|
||||
motive univ. pos. : 1
|
||||
motive pos.: 1
|
||||
major premise pos.: 2
|
||||
dep. elimination: 1
|
||||
num. parameters: 1
|
||||
num. indices: 0
|
||||
motive univ. pos.: 1
|
||||
motive pos.: 2
|
||||
major premise pos.: 3
|
||||
dep. elimination: 1
|
||||
parameters pos. at major: 1
|
||||
recursor information
|
||||
num. parameters: 0
|
||||
num. indices: 0
|
||||
num. parameters: 0
|
||||
num. indices: 0
|
||||
recursor eliminate only to Prop
|
||||
motive pos.: 0
|
||||
major premise pos.: 1
|
||||
dep. elimination: 1
|
||||
motive pos.: 1
|
||||
major premise pos.: 2
|
||||
dep. elimination: 1
|
||||
vector.induction_on.{l_1} :
|
||||
∀ {A : Type.{l_1}} {C : Π (a : nat), vector.{l_1} A a → Prop} {a : nat} (n : vector.{l_1} A a),
|
||||
C nat.zero (@vector.nil.{l_1} A) →
|
||||
(∀ {n : nat} (a : A) (a_1 : vector.{l_1} A n), C n a_1 → C (nat.succ n) (@vector.cons.{l_1} A n a a_1)) →
|
||||
C a n
|
||||
recursor information
|
||||
num. parameters: 1
|
||||
num. indices: 1
|
||||
num. parameters: 1
|
||||
num. indices: 1
|
||||
recursor eliminate only to Prop
|
||||
motive pos.: 1
|
||||
major premise pos.: 3
|
||||
dep. elimination: 1
|
||||
motive pos.: 2
|
||||
major premise pos.: 4
|
||||
dep. elimination: 1
|
||||
parameters pos. at major: 1
|
||||
indices pos. at major: 2
|
||||
Exists.rec.{l_1} :
|
||||
∀ {A : Type.{l_1}} {P : A → Prop} {C : Prop},
|
||||
(∀ (a : A), P a → C) → @Exists.{l_1} A P → C
|
||||
recursor information
|
||||
num. parameters: 2
|
||||
num. indices: 0
|
||||
num. parameters: 2
|
||||
num. indices: 0
|
||||
recursor eliminate only to Prop
|
||||
motive pos.: 2
|
||||
major premise pos.: 4
|
||||
dep. elimination: 0
|
||||
motive pos.: 3
|
||||
major premise pos.: 5
|
||||
dep. elimination: 0
|
||||
parameters pos. at major: 1 2
|
||||
|
|
|
|||
Loading…
Reference in a new issue