src/parser/input.h

   1 /*********************                                                        */
   2 /** input.h
   3  ** Original author: cconway
   4  ** Major contributors: none
   5  ** Minor contributors (to current version): mdeters
   6  ** This file is part of the CVC4 prototype.
   7  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   8  ** Courant Institute of Mathematical Sciences
   9  ** New York University
  10  ** See the file COPYING in the top-level source directory for licensing
  11  ** information.
  12  **
  13  ** Parser abstraction.
  14  **/
  15
  16 #include "cvc4parser_public.h"
  17
  18 #ifndef __CVC4__PARSER__INPUT_H
  19 #define __CVC4__PARSER__INPUT_H
  20
  21 #include <string>
  22
  23 #include "expr/expr.h"
  24 #include "parser/parser_exception.h"
  25 #include "parser/parser_options.h"
  26
  27 namespace CVC4 {
  28
  29 // Forward declarations
  30 class ExprManager;
  31 class Command;
  32 class Type;
  33
  34 namespace parser {
  35
  36 class ParserState;
  37
  38 /**
  39  * An input to be parsed. This class serves two purposes: to the client, it provides
  40  * the methods <code>parseNextCommand</code> and <code>parseNextExpression</code> to
  41  * extract a stream of <code>Command</code>'s and <code>Expr</code>'s from the input;
  42  * to the parser, it provides a repository for state data, like the variable symbol
  43  * table, and a variety of convenience functions for updating and checking the state.
  44  *
  45  * An Input should be created using the static factory methods,
  46  * e.g., <code>newFileParser</code> and <code>newStringInput</code>, and
  47  * should be deleted when done.
  48  */
  49 class CVC4_PUBLIC Input {
  50   friend class ParserState;
  51
  52   /** Whether to de-allocate the input */
  53   //  bool d_deleteInput;
  54
  55   ParserState *d_parserState;
  56
  57 public:
  58
  59   /**
  60    * Create a new parser for the given file.
  61    * @param exprManager the ExprManager to use
  62    * @param filename the path of the file to parse
  63    */
  64   Input(ExprManager* exprManager, const std::string& filename);
  65
  66   /**
  67    * Destructor.
  68    */
  69   virtual ~Input();
  70
  71   /** Create an input for the given file.
  72     *
  73     * @param exprManager the ExprManager for creating expressions from the input
  74     * @param lang the input language
  75     * @param filename the input filename
  76     */
  77    static Input* newFileInput(ExprManager* exprManager, InputLanguage lang, const std::string& filename, bool useMmap=false);
  78
  79   /** Create an input for the given stream.
  80    *
  81    * @param exprManager the ExprManager for creating expressions from the input
  82    * @param lang the input language
  83    * @param input the input stream
  84    * @param name the name of the stream, for use in error messages
  85    */
  86   //static Parser* getNewParser(ExprManager* exprManager, InputLanguage lang, std::istream& input, const std::string& name);
  87
  88   /** Create an input for the given string
  89    *
  90    * @param exprManager the ExprManager for creating expressions from the input
  91    * @param lang the input language
  92    * @param input the input string
  93    * @param name the name of the stream, for use in error messages
  94    */
  95   static Input* newStringInput(ExprManager* exprManager, InputLanguage lang, const std::string& input, const std::string& name);
  96
  97   /**
  98     * Check if we are done -- either the end of input has been reached, or some
  99     * error has been encountered.
 100     * @return true if parser is done
 101     */
 102   bool done() const;
 103
 104   /** Enable semantic checks during parsing. */
 105   void enableChecks();
 106
 107   /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
 108   void disableChecks();
 109
 110   /**
 111    * Parse the next command of the input. If EOF is encountered a EmptyCommand
 112    * is returned and done flag is set.
 113    *
 114    * @throws ParserException if an error is encountered during parsing.
 115    */
 116   Command* parseNextCommand() throw(ParserException);
 117
 118   /**
 119    * Parse the next expression of the stream. If EOF is encountered a null
 120    * expression is returned and done flag is set.
 121    * @return the parsed expression
 122    * @throws ParserException if an error is encountered during parsing.
 123    */
 124   Expr parseNextExpression() throw(ParserException);
 125
 126
 127 protected:
 128
 129   /** Called by <code>parseNextCommand</code> to actually parse a command from
 130    * the input by invoking the implementation-specific parsing method.  Returns
 131    * <code>NULL</code> if there is no command there to parse.
 132    *
 133    * @throws ParserException if an error is encountered during parsing.
 134    */
 135   virtual Command* doParseCommand() throw(ParserException) = 0;
 136
 137   /** Called by <code>parseNextExpression</code> to actually parse an
 138    * expression from the input by invoking the implementation-specific
 139    * parsing method. Returns a null <code>Expr</code> if there is no
 140    * expression there to parse.
 141    *
 142    * @throws ParserException if an error is encountered during parsing.
 143    */
 144   virtual Expr doParseExpr() throw(ParserException) = 0;
 145
 146   inline ParserState* getParserState() const {
 147     return d_parserState;
 148   }
 149
 150 private:
 151
 152   /** Throws a <code>ParserException</code> with the given error message.
 153    * Implementations should fill in the <code>ParserException</code> with
 154    * line number information, etc. */
 155   virtual void parseError(const std::string& msg) throw (ParserException) = 0;
 156
 157 }; // end of class Input
 158
 159 }/* CVC4::parser namespace */
 160 }/* CVC4 namespace */
 161
 162 #endif /* __CVC4__PARSER__INPUT_H */