Improvements to error messages

src/expr_parser.cpp

@@ -1338,7 +1338,7 @@ void ExprParser::bind(const std::string& name, Expr& e)
   if (!d_state.bind(name, e))
   {
     std::stringstream ss;
-    ss << "Failed to bind symbol " << name;
+    ss << "Failed to bind symbol " << name << ", since the symbol has already been defined";
     d_lex.parseError(ss.str());
   }
 }
@@ -1376,8 +1376,8 @@ Expr ExprParser::typeCheckApp(std::vector<Expr>& children)
     std::stringstream ss;
     d_state.getTypeChecker().getTypeApp(children, &ss);
     std::stringstream msg;
-    msg << "Type checking application failed:" << std::endl;
-    msg << "Children: " << children << std::endl;
+    msg << "Type checking application failed when applying " << children[0] << std::endl;
+    msg << "Children: " << std::vector<Expr>(children.begin()+1, children.end()) << std::endl;
     msg << "Message: " << ss.str() << std::endl;
     d_lex.parseError(msg.str());
   }

src/type_checker.cpp

@@ -369,9 +369,29 @@ Expr TypeChecker::getTypeAppInternal(std::vector<ExprValue*>& children,
     // incorrect arity
     if (out)
     {
-      (*out) << "Incorrect arity for " << Expr(hd)
-             << ", #argTypes=" << hdtypes.size()
-             << " #children=" << children.size();
+      (*out) << "Incorrect arity for " << Expr(hd);
+      if (hdtypes[hdtypes.size()-1]->getKind()==Kind::PROOF_TYPE)
+      {
+        // proof rule can give more information, partioned into args/premises
+        size_t npIndex1 = hdtypes.size()-1;
+        while (npIndex1>0 && hdtypes[npIndex1-1]->getKind()==Kind::PROOF_TYPE)
+        {
+          npIndex1--;
+        }
+        size_t npIndex2 = children.size()-1;
+        while (npIndex2>0 && d_state.lookupType(children[npIndex2-1])->getKind()==Kind::PROOF_TYPE)
+        {
+          npIndex2--;
+        }
+        (*out) << ", which expects " << npIndex1 << " arguments and "
+               << (hdtypes.size()-1-npIndex1) << " premises but " 
+               << npIndex2 << " arguments and "
+               << (children.size()-1-npIndex2) << " premises were provided";
+      }
+      else
+      {
+        (*out) << ", which expects " << (hdtypes.size()-1) << " arguments but " << (children.size()-1) << " were provided";
+      }
     }
     return d_null;
   }