From a3066e3eaa2ce8fdb4a59a0ed59a1326290f3c44 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 12 Nov 2014 13:10:19 -0800 Subject: [PATCH] fix(frontends/lean/inductive_cmd): bug in inductive datatype elaborator --- src/frontends/lean/inductive_cmd.cpp | 22 ++++++++++++++++++++++ tests/lean/run/confuse_ind.lean | 10 ++++++++++ 2 files changed, 32 insertions(+) create mode 100644 tests/lean/run/confuse_ind.lean diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index e12b4b4d0..1483fb583 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -547,6 +547,26 @@ struct inductive_cmd_fn { return infer_implicit_params(type, locals.size() + nparams, k); } + level replace_u(level const & l, level const & rlvl) { + return replace(l, [&](level const & l) { + if (l == m_u) return some_level(rlvl); + else return none_level(); + }); + } + + expr replace_u(expr const & type, level const & rlvl) { + return replace(type, [&](expr const & e) { + if (is_sort(e)) { + return some_expr(update_sort(e, replace_u(sort_level(e), rlvl))); + } else if (is_constant(e)) { + return some_expr(update_constant(e, map(const_levels(e), + [&](level const & l) { return replace_u(l, rlvl); }))); + } else { + return none_expr(); + } + }); + } + /** \brief Elaborate inductive datatypes and their introduction rules. */ void elaborate_decls(buffer & decls, buffer const & locals) { // We create an elaboration problem of the form @@ -603,6 +623,8 @@ struct inductive_cmd_fn { for (intro_rule const & ir : inductive_decl_intros(decl)) { expr type = mlocal_type(to_elab[i]); type = mk_intro_rule_type(intro_rule_name(ir), locals, nparams, to_elab.data(), local_to_ind, type); + if (m_infer_result_universe) + type = replace_u(type, resultant_level); new_irs.push_back(update_intro_rule(ir, type)); i++; } diff --git a/tests/lean/run/confuse_ind.lean b/tests/lean/run/confuse_ind.lean new file mode 100644 index 000000000..e2fd83b5c --- /dev/null +++ b/tests/lean/run/confuse_ind.lean @@ -0,0 +1,10 @@ +import logic data.prod data.unit + +definition mk_arrow (A : Type) (B : Type) := +A → A → B + +inductive confuse (A : Type) := +lean : confuse A, +node : mk_arrow A (confuse A) → confuse A + +check confuse.cases_on