Enough parsing for tonight. Added:

* Everything goes through the ParserState instead of coding in lex/yacc files
* Bare Boolean SMT lexer/parser
* Basic commands
To be completed: ParserState method implementations, parser.h/parser.cpp, make it compile and run...

1 files changed, 76 insertions, 36 deletions

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 8103238b3..765fb0553 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -13,46 +13,86 @@
 #ifndef __CVC4__PARSER__PARSER_H
 #define __CVC4__PARSER__PARSER_H
 
+#include <string>
 #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 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();
+namespace CVC4
+{
+namespace parser
+{
+
+// Forward declarations
+class Expr;
+class Command;
+class ExprManager;
+class ParserState;
+
+/**
+ * The parser.
+ */
+class Parser
+{
+  private:
+
+    /** Internal parser state we are keeping */
+    ParserState* d_data;
+
+    /** Initialize the parser */
+    void initParser();
+
+    /** Remove the parser components */
+    void deleteParser();
+
+  public:
+
+    /** The supported input languages */
+    enum InputLanguage {
+      /** SMT-LIB language */
+      INPUT_SMTLIB,
+      /** CVC language */
+      INPUT_CVC
+    };
+
+    /**
+     * Constructor for parsing out of a file.
+     * @param em the expression manager to use
+     * @param lang the language syntax to use
+     * @param file_name the file to parse
+     */
+    Parser(ExprManager* em, InputLanguage lang, const std::string& file_name);
+
+    /**
+     * Destructor.
+     */
+    ~Parser();
+
+    /** Parse a command */
+    Command parseNextCommand();
+
+    /** Parse an expression of the stream */
+    Expr parseNextExpression();
+
+    // 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(); }
+
+    /** Prints the location to the output stream */
+    void printLocation(std::ostream& out) const;
+
+    /** Reset any local data */
+    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.
+ */
+extern ParserState* _global_parser_state;
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */