From 421446830d238e4a82fb0407621b2876b6e46a74 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Tue, 16 Feb 2010 19:35:34 +0000 Subject: [PATCH] Moving parser error checking into AntlrParser --- src/parser/antlr_parser.cpp | 44 ++++++++++++++++++++++++++++++++++--- src/parser/antlr_parser.h | 22 +++++++++++++++++-- src/parser/cvc/cvc_parser.g | 16 +++----------- src/parser/smt/smt_parser.g | 28 ++--------------------- 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 kind can accept numArgs arguments. + * @param kind the built-in operator to check + * @param numArgs the number of actual arguments + * @throws SemanticException if the operator kind cannot be + * applied to numArgs 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; - } - } ; -- 2.30.2