From 8723f5b6133478654b59fcd20d99dd7b51854a9f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Nov 2014 22:54:46 -0800 Subject: [PATCH] fix(frontends/lean/inductive_cmd): inductive datatype elaborator was 'fixing' parameter mismatches. 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. --- src/frontends/lean/inductive_cmd.cpp | 17 ++++++++++++----- tests/lean/ind_parser_bug.lean | 15 +++++++++++++++ tests/lean/ind_parser_bug.lean.expected.out | 3 +++ 3 files changed, 30 insertions(+), 5 deletions(-) create mode 100644 tests/lean/ind_parser_bug.lean create mode 100644 tests/lean/ind_parser_bug.lean.expected.out diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index 8a56d486a..49813cf1c 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -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 const & ind_to_local) { - unsigned nparams = 0; // number of explicit parameters + buffer 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 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 { diff --git a/tests/lean/ind_parser_bug.lean b/tests/lean/ind_parser_bug.lean new file mode 100644 index 000000000..25d4634f5 --- /dev/null +++ b/tests/lean/ind_parser_bug.lean @@ -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" diff --git a/tests/lean/ind_parser_bug.lean.expected.out b/tests/lean/ind_parser_bug.lean.expected.out new file mode 100644 index 000000000..ce1a32766 --- /dev/null +++ b/tests/lean/ind_parser_bug.lean.expected.out @@ -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