diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 223a7738ba..05e9ead128 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -677,7 +677,6 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer< list main_idxs = info.m_explicit_idxs; buffer> postponed_args; // mark arguments that must be elaborated in the second pass. { - checkpoint C1(*this); while (is_pi(type)) { expr const & d = binding_domain(type); binder_info const & bi = binding_info(type); @@ -685,9 +684,9 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer< optional postponed; if (std::find(main_idxs.begin(), main_idxs.end(), i) != main_idxs.end()) { { - checkpoint C2(*this); + checkpoint C(*this); new_arg = visit(args[j], some_expr(d)); - process_checkpoint(C2); + process_checkpoint(C); new_arg = instantiate_mvars(new_arg); } j++; @@ -723,11 +722,14 @@ expr elaborator::visit_elim_app(expr const & fn, elim_info const & info, buffer< 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 extra arguments */ + checkpoint C(*this); + for (; j < args.size(); j++) { + new_args.push_back(visit(args[j], none_expr())); + } + process_checkpoint(C); } - process_checkpoint(C1); } /* Compute expected_type for the recursor application without extra arguments */ @@ -1258,8 +1260,6 @@ expr elaborator::visit_convoy(expr const & e, optional const & expected_ty lean_assert(is_app(e)); lean_assert(is_equations(get_app_fn(e))); expr const & ref = e; - if (!expected_type) - throw elaborator_exception(ref, "invalid match/convoy expression, expected type is not known"); buffer args, new_args; expr const & eqns = get_app_args(e, args); lean_assert(equations_num_fns(eqns) == 1); @@ -1269,6 +1269,8 @@ expr elaborator::visit_convoy(expr const & e, optional const & expected_ty if (is_placeholder(fn_type)) { /* User did not provide the type for the match, we try to infer one using expected_type and the type of the arguments */ + if (!expected_type) + throw elaborator_exception(ref, "invalid match/convoy expression, expected type is not known"); checkpoint C(*this); for (unsigned i = 0; i < args.size(); i++) new_args.push_back(visit(args[i], none_expr())); @@ -1299,24 +1301,23 @@ expr elaborator::visit_convoy(expr const & e, optional const & expected_ty it = binding_body(it); new_args.push_back(new_arg); } - expr b = instantiate_rev(it, locals); - expr new_b = visit(b, none_expr()); - expr inst_b = replace_locals(new_b, locals.as_buffer(), new_args); - if (!is_def_eq(inst_b, *expected_type)) { - auto pp_fn = mk_pp_ctx(); - throw elaborator_exception(ref, format("type mismatch at match expected type") + - pp_indent(pp_fn, inst_b) + - line() + format("but is expected") + - pp_indent(pp_fn, *expected_type)); - } - process_checkpoint(C); - new_fn_type = instantiate_mvars(inst_b); - unsigned i = args.size(); - while (i > 0) { - --i; - expr new_arg = instantiate_mvars(new_args[i]); - expr new_arg_type = instantiate_mvars(infer_type(new_arg)); - new_fn_type = m_ctx.mk_pi(locals.as_buffer()[i], kabstract(m_ctx, new_fn_type, new_arg)); + if (is_placeholder(it)) { + process_checkpoint(C); + if (!expected_type) + throw elaborator_exception(ref, "invalid match/convoy expression, expected type is not known"); + new_fn_type = *expected_type; + unsigned i = args.size(); + while (i > 0) { + --i; + new_args[i] = instantiate_mvars(new_args[i]); + new_fn_type = instantiate(kabstract(m_ctx, new_fn_type, new_args[i]), locals.as_buffer()[i]); + } + new_fn_type = instantiate_mvars(locals.mk_pi(new_fn_type)); + } else { + expr b = instantiate_rev(it, locals); + expr new_b = visit(b, none_expr()); + process_checkpoint(C); + new_fn_type = instantiate_mvars(locals.mk_pi(instantiate_mvars(new_b))); } } if (has_expr_metavar(new_fn_type)) { diff --git a/tests/lean/run/match_convoy3.lean b/tests/lean/run/match_convoy3.lean new file mode 100644 index 0000000000..bcde026029 --- /dev/null +++ b/tests/lean/run/match_convoy3.lean @@ -0,0 +1,25 @@ +set_option new_elaborator true + +constant bag_setoid : ∀ A, setoid (list A) +attribute [instance] bag_setoid + +noncomputable definition bag (A : Type) : Type := +quot (bag_setoid A) + +constant subcount : ∀ {A}, list A → list A → bool +constant list.count : ∀ {A}, A → list A → nat +constant all_of_subcount_eq_tt : ∀ {A} {l₁ l₂ : list A}, subcount l₁ l₂ = tt → ∀ a, list.count a l₁ ≤ list.count a l₂ +constant ex_of_subcount_eq_ff : ∀ {A} {l₁ l₂ : list A}, subcount l₁ l₂ = ff → ∃ a, ¬ list.count a l₁ ≤ list.count a l₂ +noncomputable definition count {A} (a : A) (b : bag A) : nat := +quot.lift_on b (λ l, list.count a l) + (λ l₁ l₂ h, sorry) +noncomputable definition subbag {A} (b₁ b₂ : bag A) := ∀ a, count a b₁ ≤ count a b₂ +infix ⊆ := subbag + +attribute [instance] +noncomputable definition decidable_subbag {A} (b₁ b₂ : bag A) : decidable (b₁ ⊆ b₂) := +quot.rec_on_subsingleton₂ b₁ b₂ (λ l₁ l₂, + match subcount l₁ l₂, rfl : ∀ (b : _), subcount l₁ l₂ = b → _ with + | tt, H := decidable.tt (all_of_subcount_eq_tt H) + | ff, H := decidable.ff (λ h, exists.elim (ex_of_subcount_eq_ff H) (λ w hw, hw (h w))) + end)