diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index fe16760c6e..c34f270edb 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -498,44 +498,73 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer< expr fn_type = try_to_pi(infer_type(fn)); buffer new_args; - // In the first pass we only process the arguments at info.m_explicit_idxs + /* In the first pass we only process the arguments at info.m_explicit_idxs */ expr type = fn_type; unsigned i = 0; unsigned j = 0; - list const & main_idxs = info.m_explicit_idxs; - while (is_pi(type)) { - expr const & d = binding_domain(type); - binder_info const & bi = binding_info(type); - expr new_arg; - if (std::find(main_idxs.begin(), main_idxs.end(), i) != main_idxs.end()) { - new_arg = visit(args[j], some_expr(d)); - j++; - if (has_expr_metavar(new_arg)) { - throw elaborator_exception(ref, format("invalid '") + format(const_name(fn)) + format ("' application, ") + - format("elaborator has special support for this kind of application ") + - format("(it is handled as an \"eliminator\"), ") + - format("but term") + pp_indent(new_arg) + - line() + format("must not contain metavariables because") + - format("it is used to compute the motive")); + list main_idxs = info.m_explicit_idxs; + buffer> postponed_args; // mark arguments that must be elaborated in the second pass. + { + checkpoint C(*this); + while (is_pi(type)) { + expr const & d = binding_domain(type); + binder_info const & bi = binding_info(type); + expr new_arg; + optional postponed; + if (std::find(main_idxs.begin(), main_idxs.end(), i) != main_idxs.end()) { + new_arg = visit(args[j], some_expr(d)); + j++; + if (has_expr_metavar(new_arg)) { + throw elaborator_exception(ref, format("invalid '") + format(const_name(fn)) + + format ("' application, ") + + format("elaborator has special support for this kind of application ") + + format("(it is handled as an \"eliminator\"), ") + + format("but term") + pp_indent(new_arg) + + line() + format("must not contain metavariables because") + + format("it is used to compute the motive")); + } + expr new_arg_type = infer_type(new_arg); + if (!is_def_eq(new_arg_type, d)) { + throw elaborator_exception(ref, mk_app_type_mismatch_error(mk_app(fn, i+1, new_args.data()), + new_arg, new_arg_type, d)); + } + } else if (is_explicit(bi)) { + new_arg = mk_metavar(d); + postponed = args[j]; + j++; + } else if (bi.is_inst_implicit()) { + new_arg = mk_instance(d); + } else { + new_arg = mk_metavar(d); } - expr new_arg_type = infer_type(new_arg); - if (!is_def_eq(new_arg_type, d)) { - throw elaborator_exception(ref, mk_app_type_mismatch_error(mk_app(fn, i+1, new_args.data()), - new_arg, new_arg_type, d)); - } - } else if (is_explicit(bi)) { - new_arg = mk_metavar(d); - j++; - } else if (bi.is_inst_implicit()) { - new_arg = mk_instance(d); - } else { - new_arg = mk_metavar(d); + new_args.push_back(new_arg); + postponed_args.push_back(postponed); + type = try_to_pi(instantiate(binding_body(type), new_arg)); + i++; } - new_args.push_back(new_arg); - type = try_to_pi(instantiate(binding_body(type), new_arg)); - i++; + + lean_assert(new_args.size() == info.m_arity); + + /* Process extra arguments */ + for (; j < args.size(); j++) { + new_args.push_back(visit(args[j], none_expr())); + } + process_checkpoint(C); } + /* Compute expected_type for the recursor application without extra arguments */ + buffer extra_args; + i = new_args.size(); + while (i > info.m_arity) { + --i; + expr new_arg = instantiate_mvars(new_args[i]); + expr new_arg_type = instantiate_mvars(infer_type(new_arg)); + expected_type = mk_pi("_a", new_arg_type, kabstract(m_ctx, expected_type, new_arg)); + extra_args.push_back(new_arg); + } + new_args.shrink(i); + std::reverse(extra_args.begin(), extra_args.end()); + // Compute motive */ trace_elab_debug(tout() << "compute motive by using keyed-abstraction:\n " << instantiate_mvars(type) << "\nwith\n " << @@ -557,8 +586,21 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer< throw elaborator_exception(ref, format("\"eliminator\" elaborator failed to compute the motive")); } - // TODO(Leo) - lean_unreachable(); + /* Elaborate postponed arguments */ + for (unsigned i = 0; i < new_args.size(); i++) { + if (optional arg = postponed_args[i]) { + lean_assert(is_metavar(new_args[i])); + expr new_arg_type = instantiate_mvars(infer_type(new_args[i])); + expr new_arg = visit(*arg, some_expr(new_arg_type)); + if (!is_def_eq(new_args[i], new_arg)) { + throw elaborator_exception(ref, format("\"eliminator\" elaborator failed to assign explicit argument")); + } + } + } + + expr r = instantiate_mvars(mk_app(mk_app(fn, new_args), extra_args)); + trace_elab_debug(tout() << "elaborated recursor:\n " << r << "\n";); + return r; } expr elaborator::visit_default_app_core(expr const & fn, arg_mask amask, buffer const & args, diff --git a/tests/lean/run/elab5.lean b/tests/lean/run/elab5.lean new file mode 100644 index 0000000000..d2c6aab8a2 --- /dev/null +++ b/tests/lean/run/elab5.lean @@ -0,0 +1,19 @@ +set_option pp.implicit true + +check (λ a b : nat, (nat.rec_on a (λ b, b) (λ a' ih b, ih b + 1) b : nat)) + +#elab (λ a b : nat, (nat.rec_on a (λ b, b) (λ a' ih b, ih b + 1) b : nat)) + +constants a b c : nat +constant p : nat → nat → Prop +constant f : nat → nat +axiom H1 : p (f a) (f a) +axiom H2 : a = b +axiom H3 : a = c + +#elab (eq.subst H2 H1 : p (f a) (f b)) +#elab (eq.subst H2 (eq.subst H3 H1) : p (f c) (f b)) + +axiom H4 : a + 1 = b +axiom H5 : p (a + nat.succ nat.zero) a +#elab (eq.subst H4 H5 : p b a)