Fix handling of overloaded symbols in standalone positions (#84)

Previously we were using a policy of handling overloaded symbols that
did not update the symbol table when a symbol was overloaded but instead
kept a reference to it via the original expression. When an overloaded
expression was applied, it would be disambiguated based on the other
expressions that had the same name.

This was incorrect for overloaded symbols that appear in unapplied
positions, where we would always take the oldest expression.

This fixes the issue by always updating the symbol table and by carrying
the overloads to the new expression. This simplifies the logic a bit
when expressions are unbound.

NEWS.md

@@ -7,7 +7,8 @@ ethos 0.1.1 prerelease
 - Adds a new option `--normalize-num`, which also only applies when reference parsing. This option treats numerals as rationals, which can be used when parsing SMT-LIB inputs in logics where numerals are shorthand for rationals.
 - Makes the `set-option` command available in proofs and Eunoia files.
 - Adds `--include=X` and `--reference=X` to the command line interface for including (reference) files.
-- Fixed a bug when applying operators with opaque arguments.
+- Fixed the disambiguation of overloaded symbols that are not applied to arguments.
+- Fixed the interpretation of operators that combine opaque and ordinary arguments.
 
 ethos 0.1.0
 ===========

src/expr_info.h

@@ -34,7 +34,10 @@ class AppInfo
   Expr d_attrConsTerm;
   /** Associated kind */
   Kind d_kind;
-  /** Overloading */
+  /**
+   * The symbols that are overloads of this symbol at the time this symbol was
+   * bound, including itself. This vector is either empty or has size >=2.
+   */
   std::vector<Expr> d_overloads;
 };
 

src/state.cpp

@@ -213,18 +213,16 @@ void State::popScope()
     if (!d_overloadedDecls.empty() && d_overloadedDecls.back()==d_decls[i])
     {
       d_overloadedDecls.pop_back();
+      std::map<std::string, Expr>::iterator its = d_symTable.find(d_decls[i]);
+      Assert (its!=d_symTable.end());
       // it should be overloaded
-      AppInfo* ai = getAppInfo(d_symTable[d_decls[i]].getValue());
+      AppInfo* ai = getAppInfo(its->second.getValue());
       Assert (ai!=nullptr);
-      Assert (!ai->d_overloads.empty());
+      // we always have at least 2 overloads
+      Assert (ai->d_overloads.size()>=2);
+      // was overloaded, we revert the binding
       ai->d_overloads.pop_back();
-      if (ai->d_overloads.size()==1)
-      {
-        Trace("overload") << "** no-overload: " << d_decls[i] << std::endl;
-        // no longer overloaded since the overload vector is now size one
-        ai->d_overloads.clear();
-      }
-      // was overloaded, so we don't unbind
+      its->second = ai->d_overloads.back();
       continue;
     }
     d_symTable.erase(d_decls[i]);
@@ -723,7 +721,7 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
               }
               i++;
             }
-            Trace("type_checker") << "...return for " << children[0] << std::endl;// << ": " << Expr(curr) << std::endl;
+            Trace("type_checker") << "...return for " << children[0] << std::endl;
             return Expr(curr);
           }
           // otherwise partial??
@@ -1080,22 +1078,31 @@ bool State::bind(const std::string& name, const Expr& e)
   std::map<std::string, Expr>::iterator its = d_symTable.find(name);
   if (its!=d_symTable.end())
   {
+    Trace("overload") << "** overload: " << name << std::endl;
     // if already bound, we overload
     AppInfo& ai = d_appData[its->second.getValue()];
-    // if the first time overloading, add the original
-    if (ai.d_overloads.empty())
+    std::vector<Expr>& ov = ai.d_overloads;
+    AppInfo& ain = d_appData[e.getValue()];
+    std::vector<Expr>& ovn = ain.d_overloads;
+    if (ov.empty())
+    {
+      // if first time overloading, add the original symbol
+      ovn.emplace_back(its->second);
+    }
+    else
     {
-      Trace("overload") << "** overload: " << name << std::endl;
-      ai.d_overloads.push_back(its->second);
+      // Otherwise, carry all of the overloads from the previous symbol.
+      // Note that since we carry the overloads for each symbol, the space
+      // required here is quadratic, but the number of overloads per symbol
+      // should be very small.
+      ovn.insert(ovn.end(), ov.begin(), ov.end());
     }
-    ai.d_overloads.push_back(e);
+    ovn.emplace_back(e);
     // add to declaration
     if (!d_declsSizeCtx.empty())
     {
-      d_decls.emplace_back(name);
       d_overloadedDecls.emplace_back(name);
     }
-    return true;
   }
   // Trace("state-debug") << "bind " << name << " -> " << &e << std::endl;
   d_symTable[name] = e;

tests/CMakeLists.txt

@@ -126,6 +126,7 @@ set(ethos_test_file_list
     simple-reference.eo
     simple-quant-reference.eo
     simple-lra-reference.eo
+    overload-standalone.eo
 )
 
 if(ENABLE_ORACLES)

tests/overload-standalone.eo

@@ -0,0 +1,14 @@
+(declare-const or (-> Bool Bool Bool) :right-assoc-nil false)
+(declare-const = (-> (! Type :var T :implicit) T T Bool))
+
+(declare-const a Bool)
+(declare-const b Bool)
+
+(define singleton-list ((T Type :implicit) (f (-> T T T)) (a T)) (eo::cons f a (eo::nil f)))
+
+(declare-rule refl ((T Type) (t T))
+  :args (t)
+  :conclusion (= t t)
+)
+
+(step @p0 (= (or b) (or b)) :rule refl :args ((singleton-list or b)))