Proper implementation

src/expr.cpp

@@ -206,20 +206,31 @@ std::string Expr::getSymbol() const
 
 ExprValue* Expr::getValue() const { return d_value; }
 
-size_t Expr::getFunctionArity() const
+std::pair<std::vector<Expr>, Expr> Expr::getFunctionType() const
 {
   Expr et = *this;
-  size_t arity = 0;
+  std::vector<Expr> args;
   while (et.getKind()==Kind::FUNCTION_TYPE)
   {
-    arity += et.getNumChildren()-1;
-    et = et[et.getNumChildren()-1];
+    size_t nchild = et.getNumChildren();
+    for (size_t i=0; i<nchild-1; i++)
+    {
+      args.push_back(et[i]);
+    }
+    et = et[nchild-1];
+    // strip off requires
     while (et.getKind()==Kind::EVAL_REQUIRES)
     {
       et = et[2];
     }
   }
-  return arity;
+  return std::pair<std::vector<Expr>, Expr>(args, et);
+}
+
+size_t Expr::getFunctionArity() const
+{
+  std::pair<std::vector<Expr>, Expr> ftype = getFunctionType();
+  return ftype.first.size();
 }
 
 /**

src/expr.h

@@ -157,6 +157,8 @@ class Expr
   std::string getSymbol() const;
   /** Get underlying value */
   ExprValue* getValue() const;
+  /** Get function */
+  std::pair<std::vector<Expr>, Expr> getFunctionType() const;
   /** Get arity, where this is a function type. Used for overloading. */
   size_t getFunctionArity() const;
  private:

src/state.cpp

@@ -825,9 +825,10 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
       Trace("overload") << "process alf.as " << children[0] << " " << children[1] << std::endl;
       AppInfo* ai = getAppInfo(vchildren[0]);
       Expr ret = children[0];
+      std::pair<std::vector<Expr>, Expr> ftype = children[1].getFunctionType();
       if (ai!=nullptr && !ai->d_overloads.empty())
       {
-        size_t arity = children[1].getFunctionArity();
+        size_t arity = ftype.first.size();
         Trace("overload") << "...overloaded, check arity " << arity << std::endl;
         // look up the overload
         std::map<size_t, Expr>::iterator ito = ai->d_overloads.find(arity);
@@ -841,11 +842,21 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
       {
         Trace("overload") << "...not overloaded" << std::endl;
       }
-      Expr tret = d_tc.getType(ret);
-      Trace("overload") << "Compare " << tret << " " << children[1] << std::endl;
-      // must be matchable
-      Ctx ctx;
-      if (d_tc.match(tret.getValue(), vchildren[1], ctx))
+      Trace("overload") << "Apply " << ret << " of type " << d_tc.getType(ret) <<  " to children of types:" << std::endl;
+      std::vector<Expr> cchildren;
+      cchildren.push_back(ret);
+      for (const Expr& t : ftype.first)
+      {
+        Trace("overload") << "- " << t << std::endl;
+        cchildren.push_back(getBoundVar("as.v", t));
+      }
+      std::stringstream ss;
+      Expr cret = mkExpr(Kind::APPLY, cchildren);
+      Expr tcret = d_tc.getType(cret, &ss);
+      Trace("overload") << "Range expected/computed: " << ftype.second << " " << tcret << ", err " << ss.str() << std::endl;
+      // if succeeded, we return the disambiguated return, otherwise the alf.as does not evaluate
+      // and we construct the (bogus) term below.
+      if (ftype.second==tcret)
       {
         return ret;
       }

src/type_checker.h

@@ -77,12 +77,12 @@ class TypeChecker
    * operator does not evaluate.
    */
   Expr evaluateLiteralOp(Kind k, const std::vector<ExprValue*>& args);
+ private:
   /**
    * Match expression a with b. If this returns true, then ctx is a substitution
    * that when applied to b gives a. The substitution
    */
   bool match(ExprValue* a, ExprValue* b, Ctx& ctx);
- private:
   /** Same as above, but takes a cache of pairs we have already visited */
   bool match(ExprValue* a,
              ExprValue* b,