Minor refactorings, in response to code review (Bug #73)

8 files changed, 26 insertions, 30 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 6a2640080..bb665ef81 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -184,9 +184,9 @@ Type* ExprManager::mkSort(const std::string& name) {
   return d_nodeManager->mkSort(name);
 }
 
-Expr ExprManager::mkVar(Type* type, const std::string& name) {
+Expr ExprManager::mkVar(const std::string& name, Type* type) {
   NodeManagerScope nms(d_nodeManager);
-  return Expr(this, new Node(d_nodeManager->mkVar(type, name)));
+  return Expr(this, new Node(d_nodeManager->mkVar(name, type)));
 }
 
 Expr ExprManager::mkVar(Type* type) {
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 1c1d6dbd7..82698732c 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -192,7 +192,7 @@ public:
   Type* mkSort(const std::string& name);
 
   // variables are special, because duplicates are permitted
-  Expr mkVar(Type* type, const std::string& name);
+  Expr mkVar(const std::string& name, Type* type);
   Expr mkVar(Type* type);
 
   /** Returns the minimum arity of the given kind. */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 83f28a842..2b403ad36 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -270,11 +270,11 @@ public:
   Node mkNode(Kind kind, const std::vector<NodeTemplate<ref_count> >& children);
 
   /**
-   * Create a variable with the given type and name.  NOTE that no
-   * lookup is done on the name.  If you mkVar(type, "a") and then
-   * mkVar(type, "a") again, you have two variables.
+   * Create a variable with the given name and type.  NOTE that no
+   * lookup is done on the name.  If you mkVar("a", type) and then
+   * mkVar("a", type) again, you have two variables.
    */
-  Node mkVar(Type* type, const std::string& name);
+  Node mkVar(const std::string& name, Type* type);
 
   /** Create a variable with the given type. */
   Node mkVar(Type* type);
@@ -767,7 +767,7 @@ inline Node NodeManager::mkNode(Kind kind,
   return NodeBuilder<>(this, kind).append(children);
 }
 
-inline Node NodeManager::mkVar(Type* type, const std::string& name) {
+inline Node NodeManager::mkVar(const std::string& name, Type* type) {
   Node n = mkVar(type);
   n.setAttribute(expr::VarNameAttr(), name);
   return n;
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 3d9006e04..61d61821b 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -127,8 +127,6 @@ AntlrInput::recoverFromMismatchedToken(pANTLR3_BASE_RECOGNIZER recognizer,
   }
 
   if(recognizer->mismatchIsMissingToken(recognizer, is, follow)) {
-    // We can fake the missing token and proceed
-    //
     matchedSymbol = recognizer->getMissingSymbol(recognizer, is,
                                                  recognizer->state->exception,
                                                  ttype, follow);
@@ -136,11 +134,8 @@ AntlrInput::recoverFromMismatchedToken(pANTLR3_BASE_RECOGNIZER recognizer,
     recognizer->state->exception->message = (void*)ANTLR3_MISSING_TOKEN_EXCEPTION_NAME;
     recognizer->state->exception->token = matchedSymbol;
     recognizer->state->exception->expecting = ttype;
-
-    // Print out the error after we insert so that ANTLRWorks sees the
-    // token in the exception.
-    //
   }
+
   reportError(recognizer);
   Unreachable("reportError should have thrown exception in AntlrInput::recoverFromMismatchedToken");
 }
@@ -178,7 +173,8 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
       if(ex->expecting == ANTLR3_TOKEN_EOF) {
         ss << "Expected end of file.";
       } else {
-        ss << "Expected " << tokenNames[ex->expecting] << ".";
+        ss << "Expected " << tokenNames[ex->expecting]
+           << ", found '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'.";
       }
     }
     break;
@@ -235,14 +231,12 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
     break;
 
   case ANTLR3_NO_VIABLE_ALT_EXCEPTION:
-
     // We could not pick any alt decision from the input given
     // so god knows what happened - however when you examine your grammar,
     // you should. It means that at the point where the current token occurred
     // that the DFA indicates nowhere to go from here.
     //
-    ss << "Cannot match to any predicted input.";
-
+    ss << "Unexpected token: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'.";
     break;
 
   case ANTLR3_MISMATCHED_SET_EXCEPTION:
@@ -258,7 +252,8 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
     // possible tokens at this point, but we did not see any
     // member of that set.
     //
-    ss << "Unexpected input. Expected one of : ";
+    ss << "Unexpected input: '" << tokenText((pANTLR3_COMMON_TOKEN)ex->token)
+       << "'. Expected one of: ";
 
     // What tokens could we have accepted at this point in the
     // parse?
@@ -296,7 +291,8 @@ void AntlrInput::reportError(pANTLR3_BASE_RECOGNIZER recognizer) {
     // but found a token that ended that sequence earlier than
     // we should have done.
     //
-    ss << "Missing elements.";
+    ss << "Sequence terminated early by token: '"
+       << tokenText((pANTLR3_COMMON_TOKEN)ex->token) << "'.";
     break;
 
   default:
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 428e2432e..16bde1de3 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -138,7 +138,7 @@ declType[CVC4::Type*& t, std::vector<std::string>& idList]
 }
   : /* A sort declaration (e.g., "T : TYPE") */
     TYPE_TOK 
-    { PARSER_STATE->newSorts(idList); 
+    { PARSER_STATE->mkSorts(idList); 
       t = EXPR_MANAGER->kindType(); }
   | /* A variable declaration */
     type[t] { PARSER_STATE->mkVars(idList,t); }
diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp
index 9e8ff577e..6cc8f6d9c 100644
--- a/src/parser/parser_state.cpp
+++ b/src/parser/parser_state.cpp
@@ -94,7 +94,7 @@ bool ParserState::isPredicate(const std::string& name) {
 Expr 
 ParserState::mkVar(const std::string& name, Type* type) {
   Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl;
-  Expr expr = d_exprManager->mkVar(type, name);
+  Expr expr = d_exprManager->mkVar(name, type);
   defineVar(name,expr);
   return expr;
 }
@@ -104,7 +104,7 @@ ParserState::mkVars(const std::vector<std::string> names,
                     Type* type) {
   std::vector<Expr> vars;
   for(unsigned i = 0; i < names.size(); ++i) {
-    vars.push_back(mkVar(names[i], type));
+    vars.push_back(mkVar(names[i],type));
   }
   return vars;
 }
@@ -126,14 +126,14 @@ ParserState::undefineVar(const std::string& name) {
 void
 ParserState::setLogic(const std::string& name) {
   if( name == "QF_UF" ) {
-    newSort("U");
+    mkSort("U");
   } else {
     Unhandled(name);
   }
 }
 
 Type*
-ParserState::newSort(const std::string& name) {
+ParserState::mkSort(const std::string& name) {
   Debug("parser") << "newSort(" << name << ")" << std::endl;
   Assert( !isDeclared(name, SYM_SORT) ) ;
   Type* type = d_exprManager->mkSort(name);
@@ -143,10 +143,10 @@ ParserState::newSort(const std::string& name) {
 }
 
 const std::vector<Type*>
-ParserState::newSorts(const std::vector<std::string>& names) {
+ParserState::mkSorts(const std::vector<std::string>& names) {
   std::vector<Type*> types;
   for(unsigned i = 0; i < names.size(); ++i) {
-    types.push_back(newSort(names[i]));
+    types.push_back(mkSort(names[i]));
   }
   return types;
 }
diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h
index 07f85623c..dc188b7d1 100644
--- a/src/parser/parser_state.h
+++ b/src/parser/parser_state.h
@@ -230,13 +230,13 @@ public:
   /**
    * Creates a new sort with the given name.
    */
-  Type* newSort(const std::string& name);
+  Type* mkSort(const std::string& name);
 
   /**
    * Creates a new sorts with the given names.
    */
   const std::vector<Type*>
-  newSorts(const std::vector<std::string>& names);
+  mkSorts(const std::vector<std::string>& names);
 
   /** Is the symbol bound to a boolean variable? */
   bool isBoolean(const std::string& name);
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index c0b184abf..160bd321f 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -322,7 +322,7 @@ sortDeclaration
 }
   : sortName[name,CHECK_UNDECLARED]
     { Debug("parser") << "sort decl: '" << name << "'" << std::endl;
-      PARSER_STATE->newSort(name); }
+      PARSER_STATE->mkSort(name); }
   ;
   
 /**