From de67288305f64e15da9430b1e4413f2d3452f779 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 17 Nov 2015 15:51:12 -0800 Subject: [PATCH] fix(library/app_builder): mk_rel supports relations where the lhs and rhs are not necessarily the last two arguments (e.g., heq) --- src/library/app_builder.cpp | 18 +++++++++++++----- tests/lean/congr_rel.lean | 1 + tests/lean/congr_rel.lean.expected.out | 24 ++++++++++++++++++++++++ 3 files changed, 38 insertions(+), 5 deletions(-) create mode 100644 tests/lean/congr_rel.lean.expected.out diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index fac05f569..7af31a63f 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -104,13 +104,15 @@ struct app_builder::imp { typedef std::unordered_map map; map m_map; - refl_info_getter m_refl_getter; - symm_info_getter m_symm_getter; - trans_info_getter m_trans_getter; + relation_info_getter m_rel_getter; + refl_info_getter m_refl_getter; + symm_info_getter m_symm_getter; + trans_info_getter m_trans_getter; imp(tmp_type_context & ctx, bool owner): m_ctx(&ctx), m_ctx_owner(owner), + m_rel_getter(mk_relation_info_getter(m_ctx->env())), m_refl_getter(mk_refl_info_getter(m_ctx->env())), m_symm_getter(mk_symm_info_getter(m_ctx->env())), m_trans_getter(mk_trans_info_getter(m_ctx->env())) { @@ -371,9 +373,15 @@ struct app_builder::imp { return mk_eq(lhs, rhs); } else if (n == get_iff_name()) { return mk_iff(lhs, rhs); + } else if (auto info = m_rel_getter(n)) { + buffer mask; + for (unsigned i = 0; i < info->get_arity(); i++) { + mask.push_back(i == info->get_lhs_pos() || i == info->get_rhs_pos()); + } + expr args[2] = {lhs, rhs}; + return mk_app(n, info->get_arity(), mask.data(), args); } else { - // TODO(Leo): for some relations (e.g., heq), the lhs and rhs are not necessarily - // the last two arguments. + // for unregistered relations assume lhs and rhs are the last two arguments. expr args[2] = {lhs, rhs}; return mk_app(n, 2, args); } diff --git a/tests/lean/congr_rel.lean b/tests/lean/congr_rel.lean index 57ce18cc3..1162a4c69 100644 --- a/tests/lean/congr_rel.lean +++ b/tests/lean/congr_rel.lean @@ -4,3 +4,4 @@ open perm #congr_rel @eq #congr_rel @iff #congr_rel @perm +#congr_rel @heq diff --git a/tests/lean/congr_rel.lean.expected.out b/tests/lean/congr_rel.lean.expected.out new file mode 100644 index 000000000..a3823d811 --- /dev/null +++ b/tests/lean/congr_rel.lean.expected.out @@ -0,0 +1,24 @@ +[fixed, eq, eq] +λ (A : Type) (a a_1 : A) (H1 : a = a_1) (a_2 a_3 : A) (H2 : a_2 = a_3), + iff.intro (λ (x : a = a_2), eq.trans (eq.symm H1) (eq.trans x H2)) + (λ (x : a_1 = a_3), eq.trans H1 (eq.trans x (eq.symm H2))) +: +∀ (A : Type) (a a_1 : A), a = a_1 → (∀ (a_2 a_3 : A), a_2 = a_3 → (a = a_2 ↔ a_1 = a_3)) +[eq, eq] +λ (a a_1 : Prop) (H1 : a ↔ a_1) (b b_1 : Prop) (H2 : b ↔ b_1), + iff.intro (λ (x : a ↔ b), iff.trans (iff.symm H1) (iff.trans x H2)) + (λ (x : a_1 ↔ b_1), iff.trans H1 (iff.trans x (iff.symm H2))) +: +∀ (a a_1 : Prop), (a ↔ a_1) → (∀ (b b_1 : Prop), (b ↔ b_1) → (a ↔ b ↔ (a_1 ↔ b_1))) +[fixed, eq, eq] +λ (A : Type) (a a_1 : list A) (H1 : a ~ a_1) (a_2 a_3 : list A) (H2 : a_2 ~ a_3), + iff.intro (λ (x : a ~ a_2), trans (perm.symm H1) (trans x H2)) + (λ (x : a_1 ~ a_3), trans H1 (trans x (perm.symm H2))) +: +∀ (A : Type) (a a_1 : list A), a ~ a_1 → (∀ (a_2 a_3 : list A), a_2 ~ a_3 → (a ~ a_2 ↔ a_1 ~ a_3)) +[fixed, eq, fixed, eq] +λ (A : Type) (a a_1 : A) (H1 : a == a_1) (B : Type) (a_2 a_3 : B) (H2 : a_2 == a_3), + iff.intro (λ (x : a == a_2), heq.trans (heq.symm H1) (heq.trans x H2)) + (λ (x : a_1 == a_3), heq.trans H1 (heq.trans x (heq.symm H2))) +: +∀ (A : Type) (a a_1 : A), a == a_1 → (∀ (B : Type) (a_2 a_3 : B), a_2 == a_3 → (a == a_2 ↔ a_1 == a_3))