summaryrefslogtreecommitdiff
path: root/src/parser/antlr_input.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/parser/antlr_input.cpp')
-rw-r--r--src/parser/antlr_input.cpp225
1 files changed, 225 insertions, 0 deletions
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
new file mode 100644
index 000000000..675a04510
--- /dev/null
+++ b/src/parser/antlr_input.cpp
@@ -0,0 +1,225 @@
+/********************* */
+/** input.cpp
+ ** Original author: cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** A super-class for ANTLR-generated input language parsers
+ **/
+
+#include <limits.h>
+#include <antlr3.h>
+
+#include "antlr_input.h"
+#include "input.h"
+#include "bounded_token_buffer.h"
+#include "bounded_token_factory.h"
+#include "memory_mapped_input_buffer.h"
+#include "parser_exception.h"
+#include "parser.h"
+
+#include "expr/command.h"
+#include "expr/type.h"
+#include "parser/cvc/cvc_input.h"
+#include "parser/smt/smt_input.h"
+#include "parser/smt2/smt2_input.h"
+#include "util/output.h"
+#include "util/Assert.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::parser;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace parser {
+
+AntlrInputStream::AntlrInputStream(std::string name, pANTLR3_INPUT_STREAM input) :
+ InputStream(name),
+ d_input(input) {
+}
+
+AntlrInputStream::~AntlrInputStream() {
+ d_input->free(d_input);
+}
+
+pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const {
+ return d_input;
+}
+
+AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap) {
+ if( useMmap ) {
+ return new AntlrInputStream( name, MemoryMappedInputBufferNew(name) );
+ } else {
+ return new AntlrInputStream( name, antlr3AsciiFileStreamNew((pANTLR3_UINT8) name.c_str()) );
+ }
+/*
+ if( d_inputStream == NULL ) {
+ throw ParserException("Couldn't open file: " + filename);
+ }
+*/
+}
+
+AntlrInputStream* AntlrInputStream::newStringInputStream(const std::string& input, const std::string& name) /*throw (InputStreamException) */{
+ char* inputStr = strdup(input.c_str());
+ char* nameStr = strdup(name.c_str());
+/*
+ if( inputStr==NULL || nameStr==NULL ) {
+ throw InputStreamException("Couldn't initialize string input: '" + input + "'");
+ }
+*/
+ return new AntlrInputStream( name,
+ antlr3NewAsciiStringInPlaceStream(
+ (pANTLR3_UINT8)inputStr,input.size(),
+ (pANTLR3_UINT8)nameStr) );
+}
+
+AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream *inputStream) {
+ AntlrInput* input;
+
+ switch(lang) {
+ case LANG_CVC4: {
+ input = new CvcInput(inputStream);
+ break;
+ }
+ case LANG_SMTLIB:
+ input = new SmtInput(inputStream);
+ break;
+
+ case LANG_SMTLIB_V2:
+ input = new Smt2Input(inputStream);
+ break;
+
+ default:
+ Unhandled(lang);
+ }
+ return input;
+}
+
+AntlrInput::AntlrInput(AntlrInputStream *inputStream, unsigned int lookahead) :
+ Input(inputStream),
+ d_lookahead(lookahead),
+ d_lexer(NULL),
+ d_parser(NULL),
+ d_antlr3InputStream( inputStream->getAntlr3InputStream() ),
+ d_tokenStream(NULL) {
+}
+
+/*
+AntlrParser::AntlrParser(ExprManager* exprManager, std::istream& input, const std::string& name, unsigned int lookahead)
+ Parser(exprManager,name),
+ d_lookahead(lookahead) {
+
+}
+*/
+
+/*
+AntlrInput::Input(ExprManager* exprManager, const std::string& input, const std::string& name, unsigned int lookahead) :
+ Input(exprManager,name),
+ d_lookahead(lookahead),
+ d_lexer(NULL),
+ d_parser(NULL),
+ d_tokenStream(NULL) {
+
+ char* inputStr = strdup(input.c_str());
+ char* nameStr = strdup(name.c_str());
+ if( inputStr==NULL || nameStr==NULL ) {
+ throw ParserException("Couldn't initialize string input: '" + input + "'");
+ }
+ d_inputStream = antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8)inputStr,input.size(),(pANTLR3_UINT8)nameStr);
+ if( d_inputStream == NULL ) {
+ throw ParserException("Couldn't create input stream for string: '" + input + "'");
+ }
+
+}
+*/
+
+AntlrInput::~AntlrInput() {
+ d_tokenStream->free(d_tokenStream);
+}
+
+pANTLR3_COMMON_TOKEN_STREAM AntlrInput::getTokenStream() {
+ return d_tokenStream;
+}
+
+void AntlrInput::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) {
+ pANTLR3_LEXER lexer = (pANTLR3_LEXER)(recognizer->super);
+ AlwaysAssert(lexer!=NULL);
+ Parser *parser = (Parser*)(lexer->super);
+ AlwaysAssert(parser!=NULL);
+ AntlrInput *input = (AntlrInput*) parser->getInput();
+ AlwaysAssert(input!=NULL);
+
+ // Call the error display routine
+ input->parseError("Error finding next token.");
+}
+
+void AntlrInput::parseError(const std::string& message)
+ throw (ParserException) {
+ Debug("parser") << "Throwing exception: "
+ << getInputStream()->getName() << ":"
+ << d_lexer->getLine(d_lexer) << "."
+ << d_lexer->getCharPositionInLine(d_lexer) << ": "
+ << message << endl;
+ throw ParserException(message, getInputStream()->getName(),
+ d_lexer->getLine(d_lexer),
+ d_lexer->getCharPositionInLine(d_lexer));
+}
+
+
+void AntlrInput::setAntlr3Lexer(pANTLR3_LEXER pLexer) {
+ d_lexer = pLexer;
+
+ pANTLR3_TOKEN_FACTORY pTokenFactory = d_lexer->rec->state->tokFactory;
+ if( pTokenFactory != NULL ) {
+ pTokenFactory->close(pTokenFactory);
+ }
+
+ /* 2*lookahead should be sufficient, but we give ourselves some breathing room. */
+ pTokenFactory = BoundedTokenFactoryNew(d_antlr3InputStream, 2*d_lookahead);
+ if( pTokenFactory == NULL ) {
+ throw ParserException("Couldn't create token factory.");
+ }
+ d_lexer->rec->state->tokFactory = pTokenFactory;
+
+ pBOUNDED_TOKEN_BUFFER buffer = BoundedTokenBufferSourceNew(d_lookahead, d_lexer->rec->state->tokSource);
+ if( buffer == NULL ) {
+ throw ParserException("Couldn't create token buffer.");
+ }
+
+ d_tokenStream = buffer->commonTstream;
+
+ // Override default lexer error reporting
+ d_lexer->rec->reportError = &lexerError;
+}
+
+void AntlrInput::setParser(Parser *parser) {
+ // ANTLR isn't using super in the lexer or the parser, AFAICT.
+ // We could also use @lexer/parser::context to add a field to the generated
+ // objects, but then it would have to be declared separately in every
+ // language's grammar and we'd have to in the address of the field anyway.
+ d_lexer->super = parser;
+ d_parser->super = parser;
+
+}
+
+void AntlrInput::setAntlr3Parser(pANTLR3_PARSER pParser) {
+ d_parser = pParser;
+// d_parser->rec->match = &match;
+ d_parser->rec->reportError = &reportError;
+ /* Don't try to recover from a parse error. */
+ // [chris 4/5/2010] Not clear on why this cast is necessary, but I get an error if I remove it.
+ d_parser->rec->recoverFromMismatchedToken =
+ (void* (*)(ANTLR3_BASE_RECOGNIZER_struct*, ANTLR3_UINT32, ANTLR3_BITSET_LIST_struct*))
+ d_parser->rec->mismatch;
+}
+
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback