diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index ade676e8f..d6c8340ea 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -1401,6 +1401,31 @@ struct unifier_fn { cs = append(aux, cs); } + /** \see ensure_sufficient_args */ + expr ensure_sufficient_args_core(expr mtype, unsigned nargs, unsigned i, constraint_seq & cs) { + if (i == nargs) + return mtype; + mtype = m_tc->ensure_pi(mtype, cs); + expr local = mk_local_for(mtype); + expr body = instantiate(binding_body(mtype), local); + return Pi(local, ensure_sufficient_args_core(body, nargs, i+1, cs)); + } + + /** \brief Make sure mtype is a Pi of size at least nargs. + If it is not, we use ensure_pi and (potentially) add new constaints to enforce it. + */ + expr ensure_sufficient_args(expr const & mtype, unsigned nargs, constraint_seq & cs) { + expr t = mtype; + unsigned num = 0; + while (is_pi(t)) { + num++; + t = binding_body(t); + } + if (num >= nargs) + return mtype; + return ensure_sufficient_args_core(mtype, nargs, 0, cs); + } + /** \brief Auxiliary functional object for implementing process_flex_rigid_core */ class flex_rigid_core_fn { unifier_fn & u; @@ -1470,29 +1495,9 @@ struct unifier_fn { return true; } - /** \see ensure_sufficient_args */ - expr ensure_sufficient_args_core(expr mtype, unsigned i, constraint_seq & cs) { - if (i == margs.size()) - return mtype; - mtype = tc().ensure_pi(mtype, cs); - expr local = u.mk_local_for(mtype); - expr body = instantiate(binding_body(mtype), local); - return Pi(local, ensure_sufficient_args_core(body, i+1, cs)); - } - - /** \brief Make sure mtype is a Pi of size at least margs.size(). - If it is not, we use ensure_pi and (potentially) add new constaints to enforce it. - */ + /** \brief Make sure mtype is a Pi of size at least margs.size(). */ expr ensure_sufficient_args(expr const & mtype, constraint_seq & cs) { - expr t = mtype; - unsigned num = 0; - while (is_pi(t)) { - num++; - t = binding_body(t); - } - if (num >= margs.size()) - return mtype; - return ensure_sufficient_args_core(mtype, 0, cs); + return u.ensure_sufficient_args(mtype, margs.size(), cs); } /** @@ -1970,6 +1975,63 @@ struct unifier_fn { postpone(c); } + // Auxiliary method used in process_flex_flex_approx + bool assign_flex_approx(expr const & m, expr const & v, justification const & j, constraint_seq & cs) { + lean_assert(m_config.m_discard); + buffer args; + expr const & fn = get_app_args(m, args); + lean_assert(is_metavar(fn)); + expr type = mlocal_type(fn); + type = ensure_sufficient_args(type, args.size(), cs); + buffer locals; + for (expr const & a : args) { + expr local = is_local(a) ? a : mk_local_for(type); + locals.push_back(local); + type = instantiate(binding_body(type), local); + } + return assign(m, fn, locals, v, j); + } + + bool process_flex_flex_approx(constraint const & c) { + lean_assert(m_config.m_discard); + // Try to solve constraint + // ?M_1 t_1 ... t_n =?= ?M_2 s_1 ... s_m + // by creating a fresh metavariable ?M using common local constants. + // If can't build approximate solution, then discard constraint. + expr const & lhs = cnstr_lhs_expr(c); + expr const & rhs = cnstr_rhs_expr(c); + buffer lhs_args, rhs_args; + get_app_args(lhs, lhs_args); + get_app_args(rhs, rhs_args); + buffer shared_locals; + unsigned sz = std::min(lhs_args.size(), rhs_args.size()); + unsigned i = 0; + for (; i < sz; i++) { + if (!is_local(lhs_args[i]) || !is_local(rhs_args[i]) || + mlocal_name(lhs_args[i]) != mlocal_name(rhs_args[i])) + break; + shared_locals.push_back(lhs_args[i]); + } + constraint_seq cs; + if (optional lhs_type = infer(lhs, cs)) { + expr new_type = Pi(shared_locals, *lhs_type); + if (!has_local(new_type)) { + expr new_mvar = mk_metavar(m_ngen.next(), new_type); + expr new_val = mk_app(new_mvar, shared_locals); + justification const & j = c.get_justification(); + return + assign_flex_approx(lhs, new_val, j, cs) && + assign_flex_approx(rhs, new_val, j, cs) && + process_constraints(cs, c.get_justification()); + } + } + // Failed to generate approximate solution. + // TODO(Leo): generate an error, or just ingore? + // we are currently just ignoring... + return true; + } + + bool process_flex_flex(constraint const & c) { expr const & lhs = cnstr_lhs_expr(c); expr const & rhs = cnstr_rhs_expr(c); @@ -1979,8 +2041,12 @@ struct unifier_fn { // ?M_1 l_1 ... l_k =?= ?M_2 l_1 ... l_k ... l_n // ?M_1 l_1 ... l_k ... l_n =?= ?M_2 l_1 ... l_k if (!is_simple_meta(lhs) || !is_simple_meta(rhs)) { - discard(c); - return true; + if (m_config.m_discard) { + return process_flex_flex_approx(c); + } else { + discard(c); + return true; + } } buffer lhs_args, rhs_args; expr ml = get_app_args(lhs, lhs_args); diff --git a/tests/lean/626a.lean.expected.out b/tests/lean/626a.lean.expected.out index c88a90c77..fc63afb35 100644 --- a/tests/lean/626a.lean.expected.out +++ b/tests/lean/626a.lean.expected.out @@ -1,6 +1,3 @@ -626a.lean:3:29: error: don't know how to synthesize placeholder -c : C¹ -⊢ nat → Type 626a.lean:3:42: error: don't know how to synthesize placeholder c : C¹ ⊢ ?M_1 @@ -12,9 +9,6 @@ c : C¹ remark: set 'formatter.hide_full_terms' to false to see the complete term λ (c : C¹), nat.rec_on c ?M_2 ?M_3 -626a.lean:8:29: error: don't know how to synthesize placeholder -c : C¹ -⊢ C¹ → Type 626a.lean:8:42: error: don't know how to synthesize placeholder c : C¹ ⊢ ?M_1 diff --git a/tests/lean/626c.lean.expected.out b/tests/lean/626c.lean.expected.out index e1c87b6ac..ce5c3cfa7 100644 --- a/tests/lean/626c.lean.expected.out +++ b/tests/lean/626c.lean.expected.out @@ -1,6 +1,3 @@ -626c.lean:2:27: error: don't know how to synthesize placeholder -c : C⁽ -⊢ C⁽ → Type 626c.lean:2:40: error: don't know how to synthesize placeholder c : C⁽ ⊢ ?M_1 @@ -12,9 +9,6 @@ c : C⁽ remark: set 'formatter.hide_full_terms' to false to see the complete term λ (c : C⁽), nat.rec_on c ?M_2 ?M_3 -626c.lean:5:27: error: don't know how to synthesize placeholder -c : α⁽ -⊢ α⁽ → Type 626c.lean:5:40: error: don't know how to synthesize placeholder c : α⁽ ⊢ ?M_1 @@ -26,9 +20,6 @@ c : α⁽ remark: set 'formatter.hide_full_terms' to false to see the complete term λ (c : α⁽), nat.rec_on c ?M_2 ?M_3 -626c.lean:8:27: error: don't know how to synthesize placeholder -c : _⁽ -⊢ _⁽ → Type 626c.lean:8:40: error: don't know how to synthesize placeholder c : _⁽ ⊢ ?M_1 @@ -40,9 +31,6 @@ c : _⁽ remark: set 'formatter.hide_full_terms' to false to see the complete term λ (c : _⁽), nat.rec_on c ?M_2 ?M_3 -626c.lean:11:28: error: don't know how to synthesize placeholder -c : C.⁽ -⊢ C.⁽ → Type 626c.lean:11:41: error: don't know how to synthesize placeholder c : C.⁽ ⊢ ?M_1 @@ -54,9 +42,6 @@ c : C.⁽ remark: set 'formatter.hide_full_terms' to false to see the complete term λ (c : C.⁽), nat.rec_on c ?M_2 ?M_3 -626c.lean:14:29: error: don't know how to synthesize placeholder -c : C⁽C⁽ -⊢ C⁽C⁽ → Type 626c.lean:14:42: error: don't know how to synthesize placeholder c : C⁽C⁽ ⊢ ?M_1 diff --git a/tests/lean/run/662.lean b/tests/lean/run/662.lean new file mode 100644 index 000000000..bd32c3bfb --- /dev/null +++ b/tests/lean/run/662.lean @@ -0,0 +1,46 @@ +open nat + +inductive type : Type := +| Nat : type +| Func : type → type → type + +open type + +section var +variable {var : type → Type} + +inductive term : type → Type := +| Var : ∀ {t}, var t → term t +| Const : nat → term Nat +| Plus : term Nat → term Nat → term Nat +| Abs : ∀ {dom ran}, (var dom → term ran) → term (Func dom ran) +| App : ∀ {dom ran}, term (Func dom ran) → term dom → term ran +| Let : ∀ {t1 t2}, term t1 → (var t1 → term t2) → term t2 +end var + +open term + +definition Term t := Π (var : type → Type), @term var t +open unit + +definition count_vars : Π {t : type}, @term (λ x, unit) t -> nat +| count_vars (Var _) := 1 +| count_vars (Const _) := 0 +| count_vars (Plus e1 e2) := count_vars e1 + count_vars e2 +| count_vars (Abs e1) := count_vars (e1 star) +| count_vars (App e1 e2) := count_vars e1 + count_vars e2 +| count_vars (Let e1 e2) := count_vars e1 + count_vars (e2 star) + +definition var (t : type) : @term (λ x, unit) t := +Var star + +example : count_vars (App (App (var (Func Nat (Func Nat Nat))) (var Nat)) (var Nat)) = 3 := +rfl + +definition count_vars2 : Π {t : type}, @term (λ x, unit) t -> nat +| _ (Var _) := 1 +| _ (Const _) := 0 +| _ (Plus e1 e2) := count_vars2 e1 + count_vars2 e2 +| _ (Abs e1) := count_vars2 (e1 star) +| _ (App e1 e2) := count_vars2 e1 + count_vars2 e2 +| _ (Let e1 e2) := count_vars2 e1 + count_vars2 (e2 star)