From 30ae8a29b6e5bb6664e6308133e7e1e4b5976fb2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 Nov 2016 13:05:52 -0700 Subject: [PATCH] fix(library/compiler/elim_recursors): some recursor applications were not being eliminated --- src/library/compiler/elim_recursors.cpp | 7 ++++--- tests/lean/run/compiler_bug1.lean | 7 +++++++ 2 files changed, 11 insertions(+), 3 deletions(-) create mode 100644 tests/lean/run/compiler_bug1.lean diff --git a/src/library/compiler/elim_recursors.cpp b/src/library/compiler/elim_recursors.cpp index 3b4fb70186..6bac389246 100644 --- a/src/library/compiler/elim_recursors.cpp +++ b/src/library/compiler/elim_recursors.cpp @@ -226,9 +226,10 @@ protected: expr cases_on = mk_app(mk_app(cases_on_fn, cases_on_args), extra_args); expr aux_decl_value = locals.mk_lambda(cases_on); expr aux_decl_cnst = declare_aux_def(aux_decl_name, aux_decl_value); - unsigned num_rest_args = args.size() - nparams - 1 - nminors; - expr const * rest_args = args.data() + nparams + 1 + nminors; - expr r = mk_app(mk_rev_app(aux_decl_cnst, abst_locals), num_rest_args, rest_args); + buffer rest_args; + for (unsigned i = nparams + 1 + nminors; i < args.size(); i++) + rest_args.push_back(visit(args[i])); + expr r = mk_app(mk_rev_app(aux_decl_cnst, abst_locals), rest_args); return r; } diff --git a/tests/lean/run/compiler_bug1.lean b/tests/lean/run/compiler_bug1.lean new file mode 100644 index 0000000000..98b36c979d --- /dev/null +++ b/tests/lean/run/compiler_bug1.lean @@ -0,0 +1,7 @@ +inductive stmt : Type +| switch : list (nat × stmt) → stmt → stmt +| nop : stmt + +meta def compile_cases_on_to_ir_expr : option stmt := do +do cs' ← return ([] : list (nat × stmt)), + return (stmt.switch cs' stmt.nop)