src/parser/antlr_input.h

   1 /*********************                                                        */
   2 /** antlr_input.h
   3  ** Original author: cconway
   4  ** Major contributors: none
   5  ** Minor contributors (to current version): none
   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  ** Base for ANTLR parser classes.
  14  **/
  15
  16 #include "cvc4parser_private.h"
  17
  18 #ifndef __CVC4__PARSER__ANTLR_PARSER_H
  19 #define __CVC4__PARSER__ANTLR_PARSER_H
  20
  21 #include <vector>
  22 #include <string>
  23 #include <iostream>
  24 #include <antlr3.h>
  25
  26 #include "expr/expr.h"
  27 #include "expr/expr_manager.h"
  28 #include "parser/input.h"
  29 #include "parser/symbol_table.h"
  30 #include "util/Assert.h"
  31
  32 namespace CVC4 {
  33
  34 class Command;
  35 class Type;
  36 class FunctionType;
  37
  38 namespace parser {
  39
  40 /**
  41  * Wrapper for an ANTLR parser that includes convenience methods to set up input and token streams.
  42  */
  43 class AntlrInput : public Input {
  44   /** The token lookahead used to lex and parse the input. This should usually be equal to
  45    * <code>K</code> for an LL(k) grammar. */
  46   unsigned int d_lookahead;
  47
  48   /** The ANTLR3 lexer associated with this input. This will be <code>NULL</code> initially. It
  49    *  must be set by a call to <code>setLexer</code>, preferably in the subclass constructor. */
  50   pANTLR3_LEXER d_lexer;
  51
  52   /** The ANTLR3 parser associated with this input. This will be <code>NULL</code> initially. It
  53    *  must be set by a call to <code>setParser</code>, preferably in the subclass constructor.
  54    *  The <code>super</code> field of <code>d_parser</code> will be set to <code>this</code> and
  55    *  <code>reportError</code> will be set to <code>AntlrInput::reportError</code>. */
  56   pANTLR3_PARSER d_parser;
  57
  58   /** The ANTLR3 token stream associated with this input. We only need this so we can free it on exit.
  59    *  This is set by <code>setLexer</code>.
  60    *  NOTE: We assume that we <em>can</em> free it on exit. No sharing! */
  61   pANTLR3_COMMON_TOKEN_STREAM d_tokenStream;
  62
  63   /** The ANTLR3 token stream associated with this input. We only need this so we can free it on exit.
  64    *  NOTE: We assume that we <em>can</em> free it on exit. No sharing! */
  65   pANTLR3_INPUT_STREAM d_input;
  66
  67   /** Turns an ANTLR3 exception into a message for the user and calls <code>parseError</code>. */
  68   static void reportError(pANTLR3_BASE_RECOGNIZER recognizer);
  69
  70 public:
  71
  72   /** Create a file input.
  73    *
  74    * @param exprManager the manager to use when building expressions from the input
  75    * @param filename the path of the file to read
  76    * @param lookahead the lookahead needed to parse the input (i.e., k for an LL(k) grammar)
  77    * @param useMmap <code>true</code> if the input should use memory-mapped I/O; otherwise, the
  78    * input will use the standard ANTLR3 I/O implementation.
  79    */
  80   AntlrInput(ExprManager* exprManager, const std::string& filename, unsigned int lookahead, bool useMmap);
  81
  82   /** Create an input from an istream. */
  83   // AntlrParser(ExprManager* em, std::istream& input, const std::string& name, unsigned int lookahead);
  84
  85   /** Create a string input.
  86    *
  87    * @param exprManager the manager to use when building expressions from the input
  88    * @param input the string to read
  89    * @param name the "filename" to use when reporting errors
  90    * @param lookahead the lookahead needed to parse the input (i.e., k for an LL(k) grammar)
  91    */
  92   AntlrInput(ExprManager* exprManager, const std::string& input, const std::string& name, unsigned int lookahead);
  93
  94   /** Destructor. Frees the token stream and closes the input. */
  95   ~AntlrInput();
  96
  97   /** Retrieve the text associated with a token. */
  98   inline static std::string tokenText(pANTLR3_COMMON_TOKEN token);
  99
 100 protected:
 101
 102   /**
 103    * Throws a <code>ParserException</code> with the given message.
 104    */
 105   void parseError(const std::string& msg) throw (ParserException);
 106
 107   /** Retrieve the input stream for this parser. */
 108   pANTLR3_INPUT_STREAM getInputStream();
 109   /** Retrieve the token stream for this parser. Must not be called before
 110    * <code>setLexer()</code>. */
 111   pANTLR3_COMMON_TOKEN_STREAM getTokenStream();
 112
 113   /** Set the ANTLR lexer for this parser. */
 114   void setLexer(pANTLR3_LEXER pLexer);
 115
 116   /** Set the ANTLR parser implementation for this parser. */
 117   void setParser(pANTLR3_PARSER pParser);
 118 };
 119
 120 std::string AntlrInput::tokenText(pANTLR3_COMMON_TOKEN token) {
 121   ANTLR3_MARKER start = token->getStartIndex(token);
 122   ANTLR3_MARKER end = token->getStopIndex(token);
 123   /* start and end are boundary pointers. The text is a string
 124    * of (end-start+1) bytes beginning at start. */
 125   std::string txt( (const char *)start, end-start+1 );
 126   Debug("parser-extra") << "tokenText: start=" << start << std::endl
 127                         <<  "end=" << end << std::endl
 128                         <<  "txt='" << txt << "'" << std::endl;
 129   return txt;
 130 }
 131
 132 }/* CVC4::parser namespace */
 133 }/* CVC4 namespace */
 134
 135 #endif /* __CVC4__PARSER__ANTLR_PARSER_H */