diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-17 17:11:35 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-17 17:11:35 +0000 |
commit | 73d8c7a4f4896455fef39c44c80bf3df30a52d89 (patch) | |
tree | 9a515d8f3290f2842ab8ec4ae66433bbfb5c529e /src/parser | |
parent | 105503064be6a198dd864d1e95d6d79e1af51d25 (diff) |
from meeting
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/parser.h | 64 | ||||
-rw-r--r-- | src/parser/parser_exception.h | 37 |
2 files changed, 101 insertions, 0 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h new file mode 100644 index 000000000..967f20e95 --- /dev/null +++ b/src/parser/parser.h @@ -0,0 +1,64 @@ +/********************* -*- C++ -*- */ +/** parser.h + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 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. + ** + ** Parser abstraction. + **/ + +#ifndef __CVC4_PARSER_H +#define __CVC4_PARSER_H + +#include "core/exception.h" +#include "core/lang.h" + +namespace CVC4 { + + class ValidityChecker; + class Expr; + + // Internal parser state and other data + class ParserData; + + class Parser { + private: + ParserData* d_data; + // Internal methods for constructing and destroying the actual parser + void initParser(); + void deleteParser(); + public: + // Constructors + Parser(ValidityChecker* vc, InputLanguage lang, + // The 'interactive' flag is ignored when fileName != "" + bool interactive = true, + const std::string& fileName = ""); + Parser(ValidityChecker* vc, InputLanguage lang, std::istream& is, + bool interactive = false); + // Destructor + ~Parser(); + // Read the next command. + Expr next(); + // Check if we are done (end of input has been reached) + bool done() const; + // The same check can be done by using the class Parser's value as + // a Boolean + operator bool() const { return done(); } + void printLocation(std::ostream & out) const; + // Reset any local data that depends on validity checker + void reset(); + }; // end of class Parser + + // The global pointer to ParserTemp. Each instance of class Parser + // sets this pointer before any calls to the lexer. We do it this + // way because flex and bison use global vars, and we want each + // Parser object to appear independent. + class ParserTemp; + extern ParserTemp* parserTemp; + +}/* CVC4 namespace */ + +#endif /* __CVC4_PARSER_H */ diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h new file mode 100644 index 000000000..18f027e44 --- /dev/null +++ b/src/parser/parser_exception.h @@ -0,0 +1,37 @@ +/********************* -*- C++ -*- */ +/** parser_exception.h + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 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. + ** + ** Exception class. + **/ + +#ifndef __CVC4_PARSER_EXCEPTION_H +#define __CVC4_PARSER_EXCEPTION_H + +#include "core/exception.h" +#include <string> +#include <iostream> + +namespace CVC4 { + + class ParserException: public Exception { + public: + // Constructors + ParserException() { } + ParserException(const std::string& msg): Exception(msg) { } + ParserException(const char* msg): Exception(msg) { } + // Destructor + virtual ~ParserException() { } + virtual std::string toString() const { + return "Parse Error: " + d_msg; + } + }; // end of class ParserException + +}/* CVC4 namespace */ + +#endif /* __CVC4_PARSER_EXCEPTION_H */ |