From 08ae17650be47a8d6796f3f691d670656bec35b9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 18 Aug 2014 18:24:08 -0700
Subject: [PATCH] feat(frontends/lean): try overloaded notation and
 declarations in the order they were defined

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/elaborator.cpp |  6 +++---
 tests/lean/run/alias1.lean        |  9 +++++----
 tests/lean/run/alias2.lean        |  2 +-
 tests/lean/run/nat_coe.lean       | 26 ++++++++++++++++++++++++++
 4 files changed, 35 insertions(+), 8 deletions(-)
 create mode 100644 tests/lean/run/nat_coe.lean

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index ddc86f38c..2cfaa23de 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -368,15 +368,15 @@ class elaborator {
                                list<expr> const & ctx, list<expr> const & full_ctx,
                                bool relax):
             m_elab(elab), m_mvar(mvar), m_choice(c), m_ctx(ctx), m_full_ctx(full_ctx),
-            m_idx(0), m_relax_main_opaque(relax) {
+            m_idx(get_num_choices(m_choice)), m_relax_main_opaque(relax) {
         }
 
         virtual optional<constraints> next() {
-            while (m_idx < get_num_choices(m_choice)) {
+            while (m_idx > 0) {
+                --m_idx;
                 expr const & c = get_choice(m_choice, m_idx);
                 expr const & f = get_app_fn(c);
                 m_elab.save_identifier_info(f);
-                m_idx++;
                 try {
                     new_scope s(m_elab, m_ctx, m_full_ctx);
                     expr r = m_elab.visit(c);
diff --git a/tests/lean/run/alias1.lean b/tests/lean/run/alias1.lean
index e7f9128a1..d2470d1b2 100644
--- a/tests/lean/run/alias1.lean
+++ b/tests/lean/run/alias1.lean
@@ -30,15 +30,16 @@ check foo a b
 theorem T1 : foo a b = N1.foo a b
 := refl _
 
-definition aux1 := foo a b  -- System elaborated it to N2.foo (f a) (f b)
-theorem T2 : aux1 = N2.foo (f a) (f b)
+definition aux1 := foo a b  -- System elaborated it to N1.foo a b
+#erase_cache T2
+theorem T2 : aux1 = N1.foo a b
 := refl _
 
 using N1
-definition aux2 := foo a b  -- Now N1 is in the beginning of the queue again, and this is elaborated to N1.foo a b
+definition aux2 := foo a b  -- Now N1 is in the end of the queue, this is elaborated to N2.foo (f a) (f b)
 check aux2
 
-theorem T3 : aux2 = N1.foo a b
+theorem T3 : aux2 = N2.foo (f a) (f b)
 := refl aux2
 
 
diff --git a/tests/lean/run/alias2.lean b/tests/lean/run/alias2.lean
index edb46f1d3..7ebca4252 100644
--- a/tests/lean/run/alias2.lean
+++ b/tests/lean/run/alias2.lean
@@ -10,8 +10,8 @@ namespace N2
   variable foo : val → val → val
 end N2
 
-using N2
 using N1
+using N2
 variables a b : num
 variable f : num → val
 coercion f
diff --git a/tests/lean/run/nat_coe.lean b/tests/lean/run/nat_coe.lean
new file mode 100644
index 000000000..bea135107
--- /dev/null
+++ b/tests/lean/run/nat_coe.lean
@@ -0,0 +1,26 @@
+import logic
+
+variable nat : Type.{1}
+variable int : Type.{1}
+
+variable nat_add : nat → nat → nat
+infixl `+`:65 := nat_add
+
+variable int_add : int → int → int
+infixl `+`:65 := int_add
+
+variable of_nat : nat → int
+coercion of_nat
+
+variables a b : nat
+variables i j : int
+
+abbreviation c1 := a + b
+
+theorem T1 : c1 = nat_add a b :=
+refl _
+
+abbreviation c2 := i + j
+
+theorem T2 : c2 = int_add i j :=
+refl _