additional work on parser hookup, configuration + build

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 */