src/parser/parser.h

   1 /*********************                                           -*- C++ -*-  */
   2 /** parser.h
   3  ** This file is part of the CVC4 prototype.
   4  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
   5  ** Courant Institute of Mathematical Sciences
   6  ** New York University
   7  ** See the file COPYING in the top-level source directory for licensing
   8  ** information.
   9  **
  10  ** Parser abstraction.
  11  **/
  12
  13 #ifndef __CVC4__PARSER__PARSER_H
  14 #define __CVC4__PARSER__PARSER_H
  15
  16 #include "core/exception.h"
  17 #include "core/lang.h"
  18
  19 namespace CVC4 {
  20 namespace parser {
  21
  22   class ValidityChecker;
  23   class Expr;
  24
  25   // Internal parser state and other data
  26   class ParserData;
  27
  28   class Parser {
  29   private:
  30     ParserData* d_data;
  31     // Internal methods for constructing and destroying the actual parser
  32     void initParser();
  33     void deleteParser();
  34   public:
  35     // Constructors
  36     Parser(ValidityChecker* vc, InputLanguage lang,
  37            // The 'interactive' flag is ignored when fileName != ""
  38            bool interactive = true,
  39            const std::string& fileName = "");
  40     Parser(ValidityChecker* vc, InputLanguage lang, std::istream& is,
  41            bool interactive = false);
  42     // Destructor
  43     ~Parser();
  44     // Read the next command.
  45     Expr next();
  46     // Check if we are done (end of input has been reached)
  47     bool done() const;
  48     // The same check can be done by using the class Parser's value as
  49     // a Boolean
  50     operator bool() const { return done(); }
  51     void printLocation(std::ostream & out) const;
  52     // Reset any local data that depends on validity checker
  53     void reset();
  54   }; // end of class Parser
  55
  56   // The global pointer to ParserTemp.  Each instance of class Parser
  57   // sets this pointer before any calls to the lexer.  We do it this
  58   // way because flex and bison use global vars, and we want each
  59   // Parser object to appear independent.
  60   class ParserTemp;
  61   extern ParserTemp* parserTemp;
  62
  63 }/* CVC4::parser namespace */
  64 }/* CVC4 namespace */
  65
  66 #endif /* __CVC4__PARSER__PARSER_H */