src/parser/input.h

   1 /*********************                                                        */
   2 /*! \file input.h
   3  ** \verbatim
   4  ** Original author: cconway
   5  ** Major contributors: mdeters
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Base for parser inputs.
  15  **
  16  ** Base for parser inputs.
  17  **/
  18
  19 #include "cvc4parser_public.h"
  20
  21 #ifndef __CVC4__PARSER__INPUT_H
  22 #define __CVC4__PARSER__INPUT_H
  23
  24 #include <iostream>
  25 #include <string>
  26 #include <stdio.h>
  27 #include <vector>
  28
  29 #include "expr/expr.h"
  30 #include "expr/expr_manager.h"
  31 #include "parser/parser_exception.h"
  32 #include "util/Assert.h"
  33 #include "util/language.h"
  34
  35 namespace CVC4 {
  36
  37 class Command;
  38 class Type;
  39 class FunctionType;
  40
  41 namespace parser {
  42
  43 class CVC4_PUBLIC InputStreamException : public Exception {
  44
  45 public:
  46   InputStreamException(const std::string& msg);
  47   virtual ~InputStreamException() throw() { }
  48 };
  49
  50 /** Wrapper around an input stream. */
  51 class InputStream {
  52
  53   /** The name of this input stream. */
  54   std::string d_name;
  55
  56   /** Indicates whether the input file is a temporary that we should
  57     * delete on exit. */
  58   bool d_fileIsTemporary;
  59
  60 protected:
  61
  62   /** Initialize the input stream with a name. */
  63   InputStream(std::string name, bool isTemporary=false) :
  64     d_name(name),
  65     d_fileIsTemporary(isTemporary) {
  66   }
  67
  68 public:
  69
  70   /** Destructor. */
  71   virtual ~InputStream() {
  72     if( d_fileIsTemporary ) {
  73       remove(d_name.c_str());
  74     }
  75   }
  76
  77   /** Get the name of this input stream. */
  78   const std::string getName() const;
  79 };
  80
  81 class Parser;
  82
  83 /**
  84  * An input to be parsed. The static factory methods in this class (e.g.,
  85  * <code>newFileInput</code>, <code>newStringInput</code>) create a parser
  86  * for the given input language and attach it to an input source of the
  87  * appropriate type.
  88  */
  89 class CVC4_PUBLIC Input {
  90   friend class Parser; // for parseError, parseCommand, parseExpr
  91   friend class ParserBuilder;
  92
  93   /** The input stream. */
  94   InputStream *d_inputStream;
  95
  96   /* Since we own d_inputStream and it needs to be freed, we need to prevent
  97    * copy construction and assignment.  Mark them private and do not define
  98    * them.
  99    */
 100   Input(const Input& input) CVC4_UNUSED;
 101   Input& operator=(const Input& input) CVC4_UNUSED;
 102
 103 public:
 104
 105   /** Create an input for the given file.
 106     *
 107     * @param lang the input language
 108     * @param filename the input filename
 109     * @param useMmap true if the parser should use memory-mapped I/O (default: false)
 110     */
 111   static Input* newFileInput(InputLanguage lang,
 112                              const std::string& filename,
 113                              bool useMmap = false)
 114     throw (InputStreamException, AssertionException);
 115
 116   /** Create an input for the given stream.
 117    *
 118    * @param lang the input language
 119    * @param input the input stream
 120    * @param name the name of the stream, for use in error messages
 121    */
 122   static Input* newStreamInput(InputLanguage lang,
 123                                std::istream& input,
 124                                const std::string& name,
 125                                bool lineBuffered = false)
 126     throw (InputStreamException, AssertionException);
 127
 128   /** Create an input for the given string
 129    *
 130    * @param lang the input language
 131    * @param input the input string
 132    * @param name the name of the stream, for use in error messages
 133    */
 134   static Input* newStringInput(InputLanguage lang,
 135                                const std::string& input,
 136                                const std::string& name)
 137     throw (InputStreamException, AssertionException);
 138
 139
 140   /** Destructor. Frees the input stream and closes the input. */
 141   virtual ~Input();
 142
 143   /** Retrieve the remaining text in this input. */
 144   virtual std::string getUnparsedText() = 0;
 145
 146   /** Get the language that this Input is reading. */
 147   virtual InputLanguage getLanguage() const throw() = 0;
 148
 149 protected:
 150
 151   /** Create an input.
 152    *
 153    * @param inputStream the input stream
 154    */
 155   Input(InputStream& inputStream);
 156
 157   /** Retrieve the input stream for this parser. */
 158   InputStream *getInputStream();
 159
 160   /** Parse a command from the input by invoking the
 161    * implementation-specific parsing method.  Returns
 162    * <code>NULL</code> if there is no command there to parse.
 163    *
 164    * @throws ParserException if an error is encountered during parsing.
 165    */
 166   virtual Command* parseCommand()
 167     throw (ParserException, TypeCheckingException, AssertionException) = 0;
 168
 169   /**
 170    * Throws a <code>ParserException</code> with the given message.
 171    */
 172   virtual void parseError(const std::string& msg)
 173     throw (ParserException, AssertionException) = 0;
 174
 175   /** Parse an expression from the input by invoking the
 176    * implementation-specific parsing method. Returns a null
 177    * <code>Expr</code> if there is no expression there to parse.
 178    *
 179    * @throws ParserException if an error is encountered during parsing.
 180    */
 181   virtual Expr parseExpr()
 182     throw (ParserException, TypeCheckingException, AssertionException) = 0;
 183
 184   /** Set the Parser object for this input. */
 185   virtual void setParser(Parser& parser) = 0;
 186
 187 };/* class Input */
 188
 189 }/* CVC4::parser namespace */
 190 }/* CVC4 namespace */
 191
 192 #endif /* __CVC4__PARSER__ANTLR_INPUT_H */