michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/inductive_cmd): inductive datatype elaborator was 'fixing' parameter mismatches.

Browse source 
Given a datatype C with parameters As, if the declaration contained
(C Bs), the elaborator would silently replace it with (C As).

This bug would confuse users and make them believe they define something
different.
This commit is contained in:
Leonardo de Moura 2014-11-05 22:54:46 -08:00
parent d306c42a1f
commit 8723f5b613
3 changed files with 30 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/frontends/lean/inductive_cmd.cpp
View file

@ -401,11 +401,12 @@ struct inductive_cmd_fn {
/** \brief Replace every occurrences of the inductive datatypes (in decls) in \c type with a local constant */
expr fix_intro_rule_type(expr const & type, name_map<expr> const & ind_to_local) {
unsigned nparams = 0; // number of explicit parameters
buffer<expr> explicit_params;
for (expr const & param : m_params) {
if (is_explicit(local_info(param)))
nparams++;
explicit_params.push_back(param);
}
unsigned neparams = explicit_params.size();
return replace(type, [&](expr const & e) {
expr const & fn = get_app_fn(e);
if (!is_constant(fn))
@ -413,13 +414,19 @@ struct inductive_cmd_fn {
if (auto it = ind_to_local.find(const_name(fn))) {
buffer<expr> args;
get_app_args(e, args);
if (args.size() < nparams)
throw parser_error(sstream() << "invalide datatype declaration, "
if (args.size() < neparams)
throw parser_error(sstream() << "invalid datatype declaration, "
<< "incorrect number of arguments to datatype '"
<< const_name(fn) << "'", m_p.pos_of(e));
for (unsigned i = 0; i < neparams; i++) {
if (args[i] != explicit_params[i])
throw parser_error(sstream() << "invalid datatype declaration, "
<< "mismatch in the #" << (i+1) << " explicit parameter",
m_p.pos_of(e));
}
pos_info pos = m_p.pos_of(e);
expr r = m_p.save_pos(copy(*it), pos);
for (unsigned i = nparams; i < args.size(); i++)
for (unsigned i = neparams; i < args.size(); i++)
r = m_p.mk_app(r, args[i], pos);
return some_expr(r);
} else {

15
tests/lean/ind_parser_bug.lean Normal file
View file

@ -0,0 +1,15 @@
import logic
inductive acc1 (A : Type) (R : A → A → Prop) (a : A) : Prop :=
intro : ∀ (x : A), (∀ (y : A), R y x → acc1 A R y) → acc1 A R x
section
variables (A : Type) (R : A → A → Prop)
inductive acc2 (a : A) : Prop :=
intro : ∀ (x : A), (∀ (y : A), R y x → acc2 y) → acc2 x
end
print "done"

3
tests/lean/ind_parser_bug.lean.expected.out Normal file
View file

@ -0,0 +1,3 @@
ind_parser_bug.lean:4:39: error: invalid datatype declaration, mismatch in the #3 explicit parameter
ind_parser_bug.lean:11:41: error: invalid datatype declaration, mismatch in the #1 explicit parameter
done