** Don't fear the files-changed list, almost all changes are in the **

[cvc5.git] / src / parser / cvc / cvc_input.h

diff --git a/src/parser/cvc/cvc_input.h b/src/parser/cvc/cvc_input.h
index 65912340149ce031d7bcdc032a50ca69ff02749d..64c6beea7c4a31cab93797bda5573d07f1786dfe 100644 (file)
--- a/src/parser/cvc/cvc_input.h
+++ b/src/parser/cvc/cvc_input.h
@@ -1,12 +1,25 @@
-/*
- * cvc_parser.h
- *
- *  Created on: Mar 5, 2010
- *      Author: chris
- */
+/*********************                                                        */
+/*! \file cvc_input.h
+ ** \verbatim
+ ** Original author: cconway
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add file-specific comments here ]].
+ **
+ ** [[ Add file-specific comments here ]]
+ **/
+
+#include "cvc4parser_private.h"
 
-#ifndef CVC_PARSER_H_
-#define CVC_PARSER_H_
+#ifndef __CVC4__PARSER__CVC_INPUT_H
+#define __CVC4__PARSER__CVC_INPUT_H
 
 #include "parser/antlr_input.h"
 #include "parser/cvc/generated/CvcLexer.h"
@@ -23,26 +36,59 @@ class ExprManager;
 namespace parser {
 
 class CvcInput : public AntlrInput {
+  /** The ANTLR3 CVC lexer for the input. */
+  pCvcLexer d_pCvcLexer;
+
+  /** The ANTLR3 CVC parser for the input. */
+  pCvcParser d_pCvcParser;
+
 public:
-  CvcInput(ExprManager* exprManager, const std::string& filename, bool useMmap);
-  CvcInput(ExprManager* exprManager, const std::string& input, const std::string& name);
+
+  /** Create an input.
+   *
+   * @param inputStream the input to parse
+   */
+  CvcInput(AntlrInputStream& inputStream);
+
+  /** Create a string input.
+   *
+   * @param exprManager the manager to use when building expressions from the input
+   * @param input the string to read
+   * @param name the "filename" to use when reporting errors
+   */
+/*
+  CvcInput(ExprManager* exprManager, const std::string& input,
+           const std::string& name);
+*/
+
+  /* Destructor. Frees the lexer and the parser. */
   ~CvcInput();
 
 protected:
-  Command* doParseCommand() throw(ParserException);
-  Expr doParseExpr() throw(ParserException);
-  pANTLR3_LEXER getLexer();
-  pANTLR3_LEXER createLexer(pANTLR3_INPUT_STREAM input);
-  pANTLR3_PARSER createParser(pANTLR3_COMMON_TOKEN_STREAM tokenStream);
+
+  /** Parse a command from the input. Returns <code>NULL</code> if there is
+   * no command there to parse.
+   *
+   * @throws ParserException if an error is encountered during parsing.
+   */
+  Command* parseCommand() throw(ParserException);
+
+  /** Parse an expression from the input. Returns a null <code>Expr</code>
+   * if there is no expression there to parse.
+   *
+   * @throws ParserException if an error is encountered during parsing.
+   */
+  Expr parseExpr() throw(ParserException);
 
 private:
+
+  /** Initialize the class. Called from the constructors once the input stream
+   * is initialized. */
   void init();
-  pCvcLexer d_pCvcLexer;
-  pCvcParser d_pCvcParser;
-}; // class CvcInput
 
-} // namespace parser
+}; // class CvcInput
 
-} // namespace CVC4
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
 
-#endif /* CVC_PARSER_H_ */
+#endif /* __CVC4__PARSER__CVC_INPUT_H */