Moving parser error checking into AntlrParser

4 files changed, 66 insertions, 44 deletions

diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index 24d0ac3d7..af3ce9d1b 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -297,12 +297,21 @@ void AntlrParser::parseError(string message)
 
 bool AntlrParser::checkDeclaration(string varName, 
                                    DeclarationCheck check,
-                                   SymbolType type) {
+                                   SymbolType type)
+    throw (antlr::SemanticException) {
   switch(check) {
   case CHECK_DECLARED:
-    return isDeclared(varName, type);
+    if( !isDeclared(varName, type) ) {
+      parseError("Symbol " + varName + " not declared");
+    } else {
+      return true;
+    }
   case CHECK_UNDECLARED:
-    return !isDeclared(varName, type);
+    if( isDeclared(varName, type) ) {
+      parseError("Symbol " + varName + " previously declared");
+    } else {
+      return true;
+    }
   case CHECK_NONE:
     return true;
   default:
@@ -310,5 +319,34 @@ bool AntlrParser::checkDeclaration(string varName,
   }
 }
 
+bool AntlrParser::checkFunction(string name)   
+  throw (antlr::SemanticException) {
+  if( !isFunction(name) ) {
+    parseError("Expecting function symbol, found '" + name + "'");
+  } 
+
+  return true;
+}
+
+bool AntlrParser::checkArity(Kind kind, unsigned int numArgs)
+  throw (antlr::SemanticException) {
+  unsigned int min = minArity(kind);
+  unsigned int max = maxArity(kind);
+
+  if( numArgs < min || numArgs > max ) {
+    stringstream ss;
+    ss << "Expecting ";
+    if( numArgs < min ) {
+      ss << "at least " << min << " ";
+    } else {
+      ss << "at most " << max << " ";
+    }
+    ss << "arguments for operator '" << kind << "', ";
+    ss << "found " << numArgs;
+    parseError(ss.str());
+  }
+  return true;
+}
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index eec444af9..52b4b4490 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -147,14 +147,32 @@ protected:
    * Return true if the the declaration policy we want to enforce holds
    * for the given symbol.
    * @param name the symbol to check
-   * @oaram check the kind of check to perform
+   * @param check the kind of check to perform
    * @param type the type of the symbol
    * @return true if the check holds
+   * @throws SemanticException if the check fails
    */
   bool checkDeclaration(std::string name, 
                         DeclarationCheck check,
-                        SymbolType type = SYM_VARIABLE);
+                        SymbolType type = SYM_VARIABLE)
+    throw (antlr::SemanticException);
 
+  /**
+   * Returns true if the given name is bound to a function.
+   * @param name the name to check
+   * @return true if name is bound to a function
+   * @throws SemanticException if name is not bound to a function
+   */
+  bool checkFunction(std::string name) throw (antlr::SemanticException);
+
+  /**
+   * Check that <code>kind</code> can accept <code>numArgs</codes> arguments.
+   * @param kind the built-in operator to check
+   * @param numArgs the number of actual arguments
+   * @throws SemanticException if the operator <code>kind</code> cannot be
+   * applied to <code>numArgs</code> arguments.
+   */
+  bool checkArity(Kind kind, unsigned int numArgs) throw (antlr::SemanticException);
 
   /** 
    * Returns the type for the variable with the given name. 
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index 926430a5c..e953244df 100644
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -153,15 +153,8 @@ identifier[DeclarationCheck check = CHECK_NONE,
            SymbolType type = SYM_VARIABLE] 
 returns [std::string id]
   : x:IDENTIFIER
-    { id = x->getText(); }
-    { checkDeclaration(id, check, type) }?
-    exception catch [antlr::SemanticException& ex] {
-      switch (check) {
-        case CHECK_DECLARED: parseError("Symbol " + id + " not declared");
-        case CHECK_UNDECLARED: parseError("Symbol " + id + " already declared");
-        default: throw ex;
-      }
-    }
+    { id = x->getText(); 
+      AlwaysAssert( checkDeclaration(id, check, type) ); }
   ;
 
 /**
@@ -388,9 +381,6 @@ functionSymbol[DeclarationCheck check = CHECK_NONE] returns [CVC4::Expr f]
   std::string name;
 }  
   : name = identifier[check,SYM_FUNCTION]
-    { AlwaysAssert( isFunction(name) );  
+    { AlwaysAssert( checkFunction(name) );  
       f = getFunction(name); }
-    exception catch [CVC4::AssertionException& ex] {
-      parseError("Expected function symbol, found: " + name);
-    }
   ;
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index fc38871b0..a9f06d92c 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -123,21 +123,8 @@ annotatedFormula returns [CVC4::Expr formula]
 }
   : /* a built-in operator application */
     LPAREN kind = builtinOp annotatedFormulas[args] RPAREN 
-    { AlwaysAssert( args.size() >= minArity(kind) 
-                    && args.size() <= maxArity(kind) );
+    { AlwaysAssert( checkArity(kind, args.size()) );
       formula = mkExpr(kind,args); }
-      exception catch [CVC4::AssertionException& ex] {
-        stringstream ss;
-        ss << "Expected ";
-        if( args.size() < minArity(kind) ) {
-          ss << "at least " << minArity(kind) << " ";
-        } else {
-          ss << "at most " << maxArity(kind) << " ";
-        }
-        ss << "arguments for operator '" << kind << "'. ";
-        ss << "Found: " << args.size();
-        parseError(ss.str());
-      }
 
   | /* A non-built-in function application */
 
@@ -226,12 +213,8 @@ functionSymbol returns [CVC4::Expr fun]
   string name;
 }
   : name = functionName[CHECK_DECLARED]
-    { AlwaysAssert( isFunction(name) );
+    { AlwaysAssert( checkFunction(name) );
       fun = getFunction(name); }
-    exception catch [CVC4::AssertionException& ex] {
-      parseError("Expected function symbol, found: " + name);
-    }
-
   ;
   
 /**
@@ -334,12 +317,5 @@ returns [std::string id]
   : x:IDENTIFIER
     { id = x->getText();
       AlwaysAssert( checkDeclaration(id, check,type) ); }
-    exception catch [CVC4::AssertionException& ex] {
-      switch (check) {
-        case CHECK_DECLARED: parseError("Symbol " + id + " not declared");
-        case CHECK_UNDECLARED: parseError("Symbol " + id + " already declared");
-        default: throw ex;
-      }
-    }
   ;