diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-25 00:42:52 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-25 00:42:52 +0000 |
commit | 2a1ac62e56d43893c59c4c2d91bcaca0dd7ce417 (patch) | |
tree | 5d2e6b493d8d366ab75163effaf13191dbf0bd71 /src/parser | |
parent | 06b391f721c8e9de4835e5a5bf2c60383ea7f8e9 (diff) |
additional work on parser hookup, configuration + build
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/Makefile.am | 18 | ||||
-rw-r--r-- | src/parser/parser.cpp | 86 | ||||
-rw-r--r-- | src/parser/parser.h | 66 | ||||
-rw-r--r-- | src/parser/parser_exception.h | 25 | ||||
-rw-r--r-- | src/parser/parser_state.cpp | 25 | ||||
-rw-r--r-- | src/parser/parser_state.h | 52 | ||||
-rw-r--r-- | src/parser/pl.ypp | 3 | ||||
-rw-r--r-- | src/parser/symbol_table.cpp | 37 | ||||
-rw-r--r-- | src/parser/symbol_table.h | 17 |
9 files changed, 230 insertions, 99 deletions
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 7965b88f9..8d8730d68 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -5,19 +5,21 @@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libparser.la libparser_la_SOURCES = \ + parser.cpp \ + parser_state.cpp \ + symbol_table.cpp \ pl_scanner.lpp \ - pl.ypp # \ - # smtlib_scanner.lpp \ - # smtlib.ypp \ - # parser.cpp + pl.ypp +# smtlib_scanner.lpp \ +# smtlib.ypp BUILT_SOURCES = \ pl_scanner.cpp \ pl.cpp \ - pl.hpp # \ - # smtlib_scanner.cpp \ - # smtlib.cpp \ - # smtlib.hpp + pl.hpp \ + smtlib_scanner.cpp \ + smtlib.cpp \ + smtlib.hpp # produce headers too AM_YFLAGS = -d diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 89170beeb..42ff506fa 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -8,19 +8,87 @@ ** information. ** ** Parser implementation. - ** - ** The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University **/ -#include "parser.h" -#include "parser_temp.h" -#include "parser_exception.h" +#include "parser/parser.h" +#include "parser/parser_state.h" +#include "parser/parser_exception.h" +#include "parser/pl.hpp" +//#include "parser/smtlib.hpp" + +// The communication entry points of the actual parsers + +// for presentation language (PL.y and PL.lex) +extern int PLparse(); +extern void *PL_createBuffer(int); +extern void PL_deleteBuffer(void *); +extern void PL_switchToBuffer(void *); +extern int PL_bufSize(); +extern void *PL_bufState(); +void PL_setInteractive(bool); + +// for smtlib language (smtlib.y and smtlib.lex) +extern int smtlibparse(); +extern void *smtlib_createBuffer(int); +extern void smtlib_deleteBuffer(void *); +extern void smtlib_switchToBuffer(void *); +extern int smtlib_bufSize(); +extern void *smtlibBufState(); +void smtlib_setInteractive(bool); namespace CVC4 { +namespace parser { -ParserTemp *parserTemp; +ParserState *parserState; -}/* CVC4 namespace */ +Parser::Parser(CVC4::SmtEngine* smt, Language lang, std::istream& is, CVC4::Options* opts, bool interactive) throw() + : d_smt(smt), + d_is(is), + d_opts(opts), + d_lang(lang), + d_interactive(interactive), + d_buffer(0) { + + parserState->lineNum = 1; + switch(d_lang) { + case PL: + d_buffer = ::PL_createBuffer(::PL_bufSize()); + break; + case SMTLIB: + //d_buffer = ::smtlib_createBuffer(::smtlib_bufSize()); + break; + default: + Unhandled(); + } +} +Parser::~Parser() throw() { + switch(d_lang) { + case PL: + ::PL_deleteBuffer(d_buffer); + break; + case SMTLIB: + //::smtlib_deleteBuffer(d_buffer); + break; + default: + Unhandled(); + } +} + +CVC4::Command* Parser::next() throw() { + return 0; +} + +bool Parser::done() const throw() { + return false; +} + +void Parser::printLocation(std::ostream & out) const throw() { +} + +void Parser::reset() throw() { +} + + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/parser.h b/src/parser/parser.h index 73565b8c4..8103238b3 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -13,47 +13,45 @@ #ifndef __CVC4__PARSER__PARSER_H #define __CVC4__PARSER__PARSER_H +#include <iostream> + #include "util/exception.h" #include "parser/language.h" +#include "parser/parser_state.h" #include "util/command.h" +#include "util/options.h" +#include "expr/expr.h" +#include "smt/smt_engine.h" +#include "util/assert.h" namespace CVC4 { namespace parser { - 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(CVC4::SmtEngine* smt, Language lang, std::istream& is, Options* opts, bool interactive = false); - // Destructor - ~Parser(); - // Read the next command. - CVC4::Command* 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; +class Parser { + + CVC4::SmtEngine *d_smt; + std::istream &d_is; + CVC4::Options *d_opts; + Language d_lang; + bool d_interactive; + void *d_buffer; + +public: + // Constructors + Parser(CVC4::SmtEngine* smt, Language lang, std::istream& is, CVC4::Options* opts, bool interactive = false) throw(); + // Destructor + ~Parser() throw(); + // Read the next command. + CVC4::Command* next() throw(); + // Check if we are done (end of input has been reached) + bool done() const throw(); + // The same check can be done by using the class Parser's value as + // a Boolean + operator bool() const throw() { return done(); } + void printLocation(std::ostream & out) const throw(); + // Reset any local data that depends on SmtEngine + void reset() throw(); +}; // end of class Parser }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index 89490fad8..b2cf8bc55 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -14,24 +14,25 @@ #define __CVC4__PARSER__PARSER_EXCEPTION_H #include "util/exception.h" +#include "cvc4_config.h" #include <string> #include <iostream> namespace CVC4 { namespace parser { - 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 +class CVC4_PUBLIC 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::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/parser_state.cpp b/src/parser/parser_state.cpp new file mode 100644 index 000000000..654fbfe32 --- /dev/null +++ b/src/parser/parser_state.cpp @@ -0,0 +1,25 @@ +/********************* -*- C++ -*- */ +/** parser_state.cpp + ** 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 state implementation. + **/ + +#include <string> +#include "parser/parser_state.h" +#include "parser/parser_exception.h" + +namespace CVC4 { +namespace parser { + +void ParserState::error(const std::string& s) throw(ParserException*) { + throw new ParserException(s); +} + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h index 0fbedb958..2bcc08bef 100644 --- a/src/parser/parser_state.h +++ b/src/parser/parser_state.h @@ -22,6 +22,7 @@ #include "expr/expr.h" #include "expr/expr_manager.h" #include "parser/symbol_table.h" +#include "parser/parser_exception.h" #include "util/exception.h" namespace CVC4 { @@ -41,8 +42,8 @@ private: // The currently used prompt std::string prompt; public: - SmtEngine* smtEngine; - ExprManager* exprManager; + CVC4::SmtEngine* smtEngine; + CVC4::ExprManager* exprManager; SymbolTable* symbolTable; std::istream* is; // The current input line @@ -50,7 +51,7 @@ public: // File name std::string fileName; // The last parsed Expr - Expr expr; + CVC4::Expr expr; // Whether we are done or not bool done; // Whether we are running interactive @@ -64,37 +65,38 @@ public: // Did we encounter a formula query (smtlib) bool queryParsed; // Default constructor - ParserState() : d_uid(0), - prompt1("CVC> "), - prompt2("- "), - prompt("CVC> "), - smtEngine(0), - exprManager(0), - symbolTable(0), - is(0), - lineNum(1), - fileName(), - expr(Expr::null()), - done(false), - interactive(false), - arrFlag(false), - bvFlag(false), - bvSize(0), - queryParsed(false) { } + ParserState() throw() + : d_uid(0), + prompt1("CVC> "), + prompt2("- "), + prompt("CVC> "), + smtEngine(0), + exprManager(0), + symbolTable(0), + is(0), + lineNum(1), + fileName(), + expr(CVC4::Expr::null()), + done(false), + interactive(false), + arrFlag(false), + bvFlag(false), + bvSize(0), + queryParsed(false) { } // Parser error handling (implemented in parser.cpp) - int error(const std::string& s); + void error(const std::string& s) throw(ParserException*) __attribute__((noreturn)); // Get the next uniqueID as a string - std::string uniqueID() { + std::string uniqueID() throw() { std::ostringstream ss; ss << d_uid++; return ss.str(); } // Get the current prompt - std::string getPrompt() { return prompt; } + std::string getPrompt() throw() { return prompt; } // Set the prompt to the main one - void setPrompt1() { prompt = prompt1; } + void setPrompt1() throw() { prompt = prompt1; } // Set the prompt to the secondary one - void setPrompt2() { prompt = prompt2; } + void setPrompt2() throw() { prompt = prompt2; } }; }/* CVC4::parser namespace */ diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp index 20687b783..a4aa7ef70 100644 --- a/src/parser/pl.ypp +++ b/src/parser/pl.ypp @@ -54,7 +54,8 @@ int PLerror(const char *s) std::ostringstream ss; ss << CVC4::parser::parserState->fileName << ":" << CVC4::parser::parserState->lineNum << ": " << s; - return CVC4::parser::parserState->error(ss.str()); + CVC4::parser::parserState->error(ss.str()); + return 0;// dead code; error() above throws an exception } #define YYLTYPE_IS_TRIVIAL 1 diff --git a/src/parser/symbol_table.cpp b/src/parser/symbol_table.cpp new file mode 100644 index 000000000..296c07731 --- /dev/null +++ b/src/parser/symbol_table.cpp @@ -0,0 +1,37 @@ +/********************* -*- C++ -*- */ +/** symbol_table.cpp + ** 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. + ** + **/ + +#include <string> +#include <list> +#include <vector> + +#include "expr/expr.h" +#include "parser/symbol_table.h" + +namespace CVC4 { +namespace parser { + +void SymbolTable::defineVar(const std::string, const void*) throw() { + +} + +void SymbolTable::defineVarList(const std::list<std::string>*, const void*) throw() { +} + +void SymbolTable::defineVarList(const std::vector<std::string>*, const void*) throw() { +} + +// Type& SymbolTable::lookupType(const std::string&); +Expr& SymbolTable::lookupVar(const std::string*) throw() { +} + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h index 3339ab67a..9135343f5 100644 --- a/src/parser/symbol_table.h +++ b/src/parser/symbol_table.h @@ -7,11 +7,6 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** Extra state of the parser shared by the lexer and parser. - ** - ** The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University **/ #include <string> @@ -21,17 +16,19 @@ #include "expr/expr.h" namespace CVC4 { +namespace parser { class SymbolTable { public: // FIXME: No definitions for Type yet // void defineType(const std::string&, const Type&); - void defineVar(const std::string, const void*); - void defineVarList(const std::list<std::string>*, const void*); - void defineVarList(const std::vector<std::string>*, const void*); + void defineVar(const std::string, const void*) throw(); + void defineVarList(const std::list<std::string>*, const void*) throw(); + void defineVarList(const std::vector<std::string>*, const void*) throw(); // Type& lookupType(const std::string&); - Expr& lookupVar(const std::string*); + Expr& lookupVar(const std::string*) throw(); }; -} +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ |