Fix bug involving simulataneous shadowing (#90)

The bug would cause shadowed symbols to be spuriously unbound due to the
order in which we were processing them when the shadowing context was
popped.

This would only occur if we parsed a binder that simultaneously shadowed
2 symbols at once.

A regression is added that demonstrates the issue.

src/state.cpp

@@ -206,8 +206,10 @@ void State::popScope()
   }
   size_t lastSize = d_declsSizeCtx.back();
   d_declsSizeCtx.pop_back();
-  for (size_t i=lastSize, currSize = d_decls.size(); i<currSize; i++)
+  size_t i = d_decls.size();
+  while (i > lastSize)
   {
+    i--;
     // Check if overloaded, which is the case if the last overloaded
     // declaration had the same name.
     if (!d_overloadedDecls.empty() && d_overloadedDecls.back()==d_decls[i])
@@ -225,6 +227,7 @@ void State::popScope()
       its->second = ai->d_overloads.back();
       continue;
     }
+    Trace("overload") << "** unbind " << d_decls[i] << std::endl;
     d_symTable.erase(d_decls[i]);
   }
   d_decls.resize(lastSize);

tests/CMakeLists.txt

@@ -128,6 +128,7 @@ set(ethos_test_file_list
     simple-lra-reference.eo
     left-cons.eo
     overload-standalone.eo
+    simul-overload.eo
 )
 
 if(ENABLE_ORACLES)

tests/simul-overload.eo

@@ -0,0 +1,19 @@
+
+
+(declare-const = (-> (! Type :var A :implicit) A A Bool))
+
+(declare-rule refl ((T Type) (t T))
+    :args (t)
+    :conclusion (= t t)
+)
+(declare-type @List ())
+(declare-const @list.nil @List)
+(declare-const @list (-> (! Type :var T :implicit) T @List @List) :right-assoc-nil @list.nil)
+(declare-const forall (-> @List Bool Bool) :binder @list)
+
+(declare-type Int ())
+(declare-const a Int)
+(declare-const b Int)
+
+(step @p99 :rule refl :args ((forall ((a Int) (b Int)) true)))
+(step @p106 :rule refl :args (a))