From 42289d433489ed8ed882172b977708360e50e12b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 Feb 2015 16:10:16 -0800 Subject: [PATCH] feat(library/tactic/class_instance_synth): create class instance synthesis subproblems only for arguments marked with the `[]` binder annotation --- src/library/tactic/class_instance_synth.cpp | 12 +++++++++--- tests/lean/run/algebra1.lean | 6 +++--- tests/lean/run/class7.lean | 2 +- tests/lean/run/class8.lean | 4 ++-- tests/lean/run/elab_bug1.lean | 8 ++++---- tests/lean/run/univ_bug2.lean | 2 +- 6 files changed, 20 insertions(+), 14 deletions(-) diff --git a/src/library/tactic/class_instance_synth.cpp b/src/library/tactic/class_instance_synth.cpp index 8405968a1..fba4e3473 100644 --- a/src/library/tactic/class_instance_synth.cpp +++ b/src/library/tactic/class_instance_synth.cpp @@ -236,9 +236,15 @@ struct class_instance_elaborator : public choice_iterator { type = tc.whnf(type).first; if (!is_pi(type)) break; - pair ac = mk_class_instance_elaborator(m_C, m_ctx, some_expr(binding_domain(type)), g, m_depth+1); - expr arg = ac.first; - cs.push_back(ac.second); + expr arg; + if (binding_info(type).is_inst_implicit()) { + pair ac = mk_class_instance_elaborator(m_C, m_ctx, some_expr(binding_domain(type)), + g, m_depth+1); + arg = ac.first; + cs.push_back(ac.second); + } else { + arg = m_ctx.mk_meta(m_C->m_ngen, some_expr(binding_domain(type)), g); + } r = mk_app(r, arg, g); type = instantiate(binding_body(type), arg); } diff --git a/tests/lean/run/algebra1.lean b/tests/lean/run/algebra1.lean index 457abe94a..628e4209e 100644 --- a/tests/lean/run/algebra1.lean +++ b/tests/lean/run/algebra1.lean @@ -65,7 +65,7 @@ namespace semigroup definition assoc {A : Type} (s : semigroup_struct A) : is_assoc (mul s) := semigroup_struct.rec (fun f h, h) s - definition is_mul_struct [instance] (A : Type) (s : semigroup_struct A) : mul_struct A + definition is_mul_struct [instance] (A : Type) [s : semigroup_struct A] : mul_struct A := mul_struct.mk (mul s) inductive semigroup : Type := @@ -74,7 +74,7 @@ namespace semigroup definition carrier [coercion] (g : semigroup) := semigroup.rec (fun c s, c) g - definition is_semigroup [instance] (g : semigroup) : semigroup_struct (carrier g) + definition is_semigroup [instance] [g : semigroup] : semigroup_struct (carrier g) := semigroup.rec (fun c s, s) g end semigroup @@ -91,7 +91,7 @@ namespace monoid := monoid_struct.rec (fun mul id a i, a) s open semigroup - definition is_semigroup_struct [instance] (A : Type) (s : monoid_struct A) : semigroup_struct A + definition is_semigroup_struct [instance] (A : Type) [s : monoid_struct A] : semigroup_struct A := semigroup_struct.mk (mul s) (assoc s) inductive monoid : Type := diff --git a/tests/lean/run/class7.lean b/tests/lean/run/class7.lean index 4b6c248e7..ae001064f 100644 --- a/tests/lean/run/class7.lean +++ b/tests/lean/run/class7.lean @@ -9,7 +9,7 @@ theorem inh_bool [instance] : inh Prop set_option class.trace_instances true -theorem inh_fun [instance] {A B : Type} (H : inh B) : inh (A → B) +theorem inh_fun [instance] {A B : Type} [H : inh B] : inh (A → B) := inh.rec (λ b, inh.intro (λ a : A, b)) H theorem tst {A B : Type} (H : inh B) : inh (A → B → B) diff --git a/tests/lean/run/class8.lean b/tests/lean/run/class8.lean index 2982e5679..fb3e3fd02 100644 --- a/tests/lean/run/class8.lean +++ b/tests/lean/run/class8.lean @@ -15,10 +15,10 @@ theorem inh_exists {A : Type} {P : A → Prop} (H : ∃x, P x) : inh A theorem inh_bool [instance] : inh Prop := inh.intro true -theorem inh_fun [instance] {A B : Type} (H : inh B) : inh (A → B) +theorem inh_fun [instance] {A B : Type} [H : inh B] : inh (A → B) := inh.rec (λb, inh.intro (λa : A, b)) H -theorem pair_inh [instance] {A : Type} {B : Type} (H1 : inh A) (H2 : inh B) : inh (prod A B) +theorem pair_inh [instance] {A : Type} {B : Type} [H1 : inh A] [H2 : inh B] : inh (prod A B) := inh_elim H1 (λa, inh_elim H2 (λb, inh.intro (pair a b))) definition assump := eassumption diff --git a/tests/lean/run/elab_bug1.lean b/tests/lean/run/elab_bug1.lean index e1421fffa..9afb4341d 100644 --- a/tests/lean/run/elab_bug1.lean +++ b/tests/lean/run/elab_bug1.lean @@ -42,19 +42,19 @@ theorem congr_const_iff [instance] (T1 : Type) (R1 : T1 → T1 → Prop) (c : Pr congruence R1 iff (const T1 c) := congr_const iff iff.refl T1 R1 c theorem congr_or [instance] (T : Type) (R : T → T → Prop) (f1 f2 : T → Prop) - (H1 : congruence R iff f1) (H2 : congruence R iff f2) : + [H1 : congruence R iff f1] [H2 : congruence R iff f2] : congruence R iff (λx, f1 x ∨ f2 x) := sorry theorem congr_implies [instance] (T : Type) (R : T → T → Prop) (f1 f2 : T → Prop) - (H1 : congruence R iff f1) (H2 : congruence R iff f2) : + [H1 : congruence R iff f1] [H2 : congruence R iff f2] : congruence R iff (λx, f1 x → f2 x) := sorry theorem congr_iff [instance] (T : Type) (R : T → T → Prop) (f1 f2 : T → Prop) - (H1 : congruence R iff f1) (H2 : congruence R iff f2) : + [H1 : congruence R iff f1] [H2 : congruence R iff f2] : congruence R iff (λx, f1 x ↔ f2 x) := sorry theorem congr_not [instance] (T : Type) (R : T → T → Prop) (f : T → Prop) - (H : congruence R iff f) : + [H : congruence R iff f] : congruence R iff (λx, ¬ f x) := sorry theorem subst_iff {T : Type} {R : T → T → Prop} {P : T → Prop} [C : congruence R iff P] diff --git a/tests/lean/run/univ_bug2.lean b/tests/lean/run/univ_bug2.lean index d4ce5c812..8b3be7671 100644 --- a/tests/lean/run/univ_bug2.lean +++ b/tests/lean/run/univ_bug2.lean @@ -20,7 +20,7 @@ theorem infer_eq {T : Type} (t1 t2 : T) [C : simplifies_to t1 t2] : t1 = t2 := simplifies_to.rec (λx, x) C theorem simp_app [instance] (S : Type) (T : Type) (f1 f2 : S → T) (s1 s2 : S) - (C1 : simplifies_to f1 f2) (C2 : simplifies_to s1 s2) : simplifies_to (f1 s1) (f2 s2) := + [C1 : simplifies_to f1 f2] [C2 : simplifies_to s1 s2] : simplifies_to (f1 s1) (f2 s2) := mk (congr (get_eq C1) (get_eq C2)) theorem test1 (S : Type) (T : Type) (f1 f2 : S → T) (s1 s2 : S) (Hf : f1 = f2) (Hs : s1 = s2) :