From 08169c5ac2c4b01f52e8904313aa5d0385a6bc7a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 31 Aug 2015 17:47:50 -1000 Subject: [PATCH] fix(library/unifier): fixes #809 Daniel is correct when he says the interaction between choice case-splits, delta case-splits, and coercions can be subtle. I believe the following condition https://github.com/leanprover/lean/blob/master/src/frontends/lean/elaborator.cpp#L111 reduces counter-intuitive behavior. Example, the coercion should not influence the resulting type. BTW, by removing this condition, many files in the library broke when I tried to compile from scratch make clean-olean make I used the following workaround. Given a delta-delta constraint f a =?= f b If the terms are types, and no case-split will be performed, then the delta-delta constraint is eagerly solved. In principle, we don't need the condition that the terms are types. However, many files break if we remove it. The problem is that many files in the standard library are abusing the higher-order unification procedure. The elaboration problems are quite tricky to solve. I use the extra condition "the terms are types" because usually if they are, "f" is morally injective, and we don't really want to unfold it. Note that the following two cases do not work check '{1, 2, 3} check insert 1 (insert 2 (insert 3 empty)) Well, they work if we the num namespace is open, and they are interpreted as having type (finset num) --- src/library/unifier.cpp | 34 +++++++++++++++++++++++++++++----- tests/lean/run/809.lean | 23 +++++++++++++++++++++++ tests/lean/run/809b.lean | 21 +++++++++++++++++++++ 3 files changed, 73 insertions(+), 5 deletions(-) create mode 100644 tests/lean/run/809.lean create mode 100644 tests/lean/run/809b.lean diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index e72282dd6..0c8c5f52b 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -817,6 +817,17 @@ struct unifier_fn { lean_unreachable(); // LCOV_EXCL_LINE } + /** \brief Return true if type of \c e is Type. + \remark constraints are discarded */ + bool is_type(expr const & e) { + constraint_seq cs; + optional t = infer(e, cs); + if (!t) + return false; + t = whnf(*t, cs); + return is_sort(*t); + } + optional is_delta(expr const & e) { return m_tc->is_delta(e); } @@ -1030,9 +1041,14 @@ struct unifier_fn { } if (is_eq_deltas(lhs, rhs)) { - // we need to create a backtracking point for this one - add_cnstr(c, cnstr_group::Basic); - return true; + if (!split_delta(lhs) && is_type(lhs)) { + // If lhs (and consequently rhs) is a type, and not case-split is generated, then process delta constraint eagerly. + return process_delta(c); + } else { + // we need to create a backtracking point for this one + add_cnstr(c, cnstr_group::Basic); + return true; + } } else if (is_meta(lhs) && is_meta(rhs)) { // flex-flex constraints are delayed the most. unsigned cidx = add_cnstr(c, cnstr_group::FlexFlex); @@ -1651,6 +1667,15 @@ struct unifier_fn { return true; } + // Return true if we should case-split on a delta constraint where \c lhs is the left-hand-side + bool split_delta(expr const & lhs) { + expr lhs_fn = get_app_fn(lhs); + lean_assert(is_constant(lhs_fn)); + declaration d = *m_env.find(const_name(lhs_fn)); + return (m_config.m_kind == unifier_kind::Liberal && + (m_config.m_computation || module::is_definition(m_env, d.get_name()) || is_at_least_quasireducible(m_env, d.get_name()))); + } + /** \brief Solve constraints of the form (f a_1 ... a_n) =?= (f b_1 ... b_n) where f can be expanded. We consider two possible solutions: @@ -1679,8 +1704,7 @@ struct unifier_fn { return unfold_delta(c, justification()); justification a; - if (m_config.m_kind == unifier_kind::Liberal && - (m_config.m_computation || module::is_definition(m_env, d.get_name()) || is_at_least_quasireducible(m_env, d.get_name()))) { + if (split_delta(lhs)) { // add case_split for t =?= s a = mk_assumption_justification(m_next_assumption_idx); add_case_split(std::unique_ptr(new delta_unfold_case_split(*this, j, c))); diff --git a/tests/lean/run/809.lean b/tests/lean/run/809.lean new file mode 100644 index 000000000..a99ddbf37 --- /dev/null +++ b/tests/lean/run/809.lean @@ -0,0 +1,23 @@ +import data.finset data.num data.nat data.int algebra.ring +open finset num nat int algebra + +check @finset.insert _ _ 1 (@finset.empty ℕ) + +check '{1, 2, 3} -- finset num +check ('{1, 2, 3} : finset ℕ) +check ('{1, 2, 3} : finset ℕ) -- finset ℕ +check ('{1, 2, 3} : finset ℤ) -- finset ℤ + +example : finset nat := +insert 1 (insert 2 (insert 3 empty)) + +check insert 1 (insert 2 (insert 3 empty)) -- finset num +check (insert 1 (insert 2 (insert 3 empty)) : finset nat) + +check (insert (1:nat) (insert (2:nat) (insert (3:nat) empty))) + +definition foo_nat (x : finset ℕ) : finset ℕ := x +definition foo_int (x : finset ℤ) : finset ℤ := x + +check foo_nat '{1, 2, 3} -- finset ℕ +check foo_int '{1, 2, 3} -- finset ℤ diff --git a/tests/lean/run/809b.lean b/tests/lean/run/809b.lean new file mode 100644 index 000000000..3b4197664 --- /dev/null +++ b/tests/lean/run/809b.lean @@ -0,0 +1,21 @@ +import algebra.ring data.finset +open finset nat algebra + +constant A : Type₁ +constants a b : A +axiom decA : decidable_eq A +attribute decA [instance] +notation 5 := a +notation 5 := b + +definition foo1 : finset nat := +'{ 1, 2, 5, 5 } + +definition foo2 : finset nat := +'{ 1, 2, 3 } + +definition foo3 : finset nat := +'{ 1 } + +noncomputable definition foo4 : finset A := +'{ 5, 5, b }