Parser tweaks to address review

Private members of Input moved to new class ParserState

1 files changed, 42 insertions, 209 deletions

diff --git a/src/parser/input.h b/src/parser/input.h
index ad888c6cc..0e924364d 100644
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -15,101 +15,44 @@
 
 #include "cvc4parser_public.h"
 
-#ifndef __CVC4__PARSER__PARSER_H
-#define __CVC4__PARSER__PARSER_H
+#ifndef __CVC4__PARSER__INPUT_H
+#define __CVC4__PARSER__INPUT_H
 
 #include <string>
-#include <iostream>
 
 #include "expr/expr.h"
-#include "expr/kind.h"
 #include "parser/parser_exception.h"
 #include "parser/parser_options.h"
-#include "parser/symbol_table.h"
-#include "util/Assert.h"
 
 namespace CVC4 {
 
 // Forward declarations
-class BooleanType;
 class ExprManager;
 class Command;
-class FunctionType;
-class KindType;
 class Type;
 
 namespace parser {
 
-/** Types of check for the symols */
-enum DeclarationCheck {
-  /** Enforce that the symbol has been declared */
-  CHECK_DECLARED,
-  /** Enforce that the symbol has not been declared */
-  CHECK_UNDECLARED,
-  /** Don't check anything */
-  CHECK_NONE
-};
-
-/** Returns a string representation of the given object (for
-    debugging). */
-inline std::string toString(DeclarationCheck check) {
-  switch(check) {
-  case CHECK_NONE: return "CHECK_NONE";
-  case CHECK_DECLARED:  return "CHECK_DECLARED";
-  case CHECK_UNDECLARED: return "CHECK_UNDECLARED";
-  default: Unreachable();
-  }
-}
-
-/**
- * Types of symbols. Used to define namespaces.
- */
-enum SymbolType {
-  /** Variables */
-  SYM_VARIABLE,
-  /** Sorts */
-  SYM_SORT
-};
-
-/** Returns a string representation of the given object (for
-    debugging). */
-inline std::string toString(SymbolType type) {
-  switch(type) {
-  case SYM_VARIABLE: return "SYM_VARIABLE";
-  case SYM_SORT: return "SYM_SORT";
-  default: Unreachable();
-  }
-}
+class ParserState;
 
 /**
- * The parser. The parser should be obtained by calling the static methods
- * getNewParser, and should be deleted when done.
+ * An input to be parsed. This class serves two purposes: to the client, it provides
+ * the methods <code>parseNextCommand</code> and <code>parseNextExpression</code> to
+ * extract a stream of <code>Command</code>'s and <code>Expr</code>'s from the input;
+ * to the parser, it provides a repository for state data, like the variable symbol
+ * table, and a variety of convenience functions for updating and checking the state.
  *
- * This class includes convenience methods for interacting with the ExprManager
- * from within a grammar.
+ * An Input should be created using the static factory methods,
+ * e.g., <code>newFileParser</code> and <code>newStringInput</code>, and
+ * should be deleted when done.
  */
 class CVC4_PUBLIC Input {
+  friend class ParserState;
 
   /** Whether to de-allocate the input */
-//  bool d_deleteInput;
-
-  /** The expression manager */
-  ExprManager* d_exprManager;
-
-  /** The symbol table lookup */
-  SymbolTable<Expr> d_varSymbolTable;
-
-  /** The sort table */
-  SymbolTable<Type*> d_sortTable;
-
-  /** The name of the input file. */
-  std::string d_filename;
-
-  /** Are we done */
-  bool d_done;
+  //  bool d_deleteInput;
 
-  /** Are semantic checks enabled during parsing? */
-  bool d_checksEnabled;
+  ParserState *d_parserState;
 
 public:
 
@@ -123,17 +66,17 @@ public:
   /**
    * Destructor.
    */
-  ~Input();
+  virtual ~Input();
 
-  /** Create a parser for the given file.
+  /** Create an input for the given file.
     *
     * @param exprManager the ExprManager for creating expressions from the input
     * @param lang the input language
     * @param filename the input filename
     */
-   static Input* newFileParser(ExprManager* exprManager, InputLanguage lang, const std::string& filename, bool useMmap=false);
+   static Input* newFileInput(ExprManager* exprManager, InputLanguage lang, const std::string& filename, bool useMmap=false);
 
-  /** Create a parser for the given input stream.
+  /** Create an input for the given stream.
    *
    * @param exprManager the ExprManager for creating expressions from the input
    * @param lang the input language
@@ -142,19 +85,27 @@ public:
    */
   //static Parser* getNewParser(ExprManager* exprManager, InputLanguage lang, std::istream& input, const std::string& name);
 
-  /** Create a parser for the given input string
+  /** Create an input for the given string
    *
    * @param exprManager the ExprManager for creating expressions from the input
    * @param lang the input language
    * @param input the input string
    * @param name the name of the stream, for use in error messages
    */
-  static Input* newStringParser(ExprManager* exprManager, InputLanguage lang, const std::string& input, const std::string& name);
+  static Input* newStringInput(ExprManager* exprManager, InputLanguage lang, const std::string& input, const std::string& name);
 
-  /** Get the <code>ExprManager</code> associated with this input. */
-  inline ExprManager* getExprManager() const {
-    return d_exprManager;
-  }
+  /**
+    * Check if we are done -- either the end of input has been reached, or some
+    * error has been encountered.
+    * @return true if parser is done
+    */
+  bool done() const;
+
+  /** Enable semantic checks during parsing. */
+  void enableChecks();
+
+  /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
+  void disableChecks();
 
   /**
    * Parse the next command of the input. If EOF is encountered a EmptyCommand
@@ -172,127 +123,6 @@ public:
    */
   Expr parseNextExpression() throw(ParserException);
 
-  /**
-   * Check if we are done -- either the end of input has been reached, or some
-   * error has been encountered.
-   * @return true if parser is done
-   */
-  bool done() const;
-
-  /** Enable semantic checks during parsing. */
-  void enableChecks();
-
-  /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
-  void disableChecks();
-
-  /** Get the name of the input file. */
-  inline const std::string getFilename() {
-    return d_filename;
-  }
-
-  /**
-   * Sets the logic for the current benchmark. Declares any logic symbols.
-   *
-   * @param name the name of the logic (e.g., QF_UF, AUFLIA)
-   */
-  void setLogic(const std::string& name);
-
-  /**
-     * Returns a variable, given a name and a type.
-     * @param var_name the name of the variable
-     * @return the variable expression
-     */
-    Expr getVariable(const std::string& var_name);
-
-    /**
-     * Returns a sort, given a name
-     */
-    Type* getSort(const std::string& sort_name);
-
-    /**
-     * Checks if a symbol has been declared.
-     * @param name the symbol name
-     * @param type the symbol type
-     * @return true iff the symbol has been declared with the given type
-     */
-    bool isDeclared(const std::string& name, SymbolType type = SYM_VARIABLE);
-
-    /**
-     * Checks if the declaration policy we want to enforce holds
-     * for the given symbol.
-     * @param name the symbol to check
-     * @param check the kind of check to perform
-     * @param type the type of the symbol
-     * @throws ParserException if checks are enabled and the check fails
-     */
-    void checkDeclaration(const std::string& name,
-                          DeclarationCheck check,
-                          SymbolType type = SYM_VARIABLE)
-      throw (ParserException);
-
-    /**
-     * Checks whether the given name is bound to a function.
-     * @param name the name to check
-     * @throws ParserException if checks are enabled and name is not bound to a function
-     */
-    void checkFunction(const std::string& name) throw (ParserException);
-
-    /**
-     * Check that <code>kind</code> can accept <code>numArgs</codes> arguments.
-     * @param kind the built-in operator to check
-     * @param numArgs the number of actual arguments
-     * @throws ParserException if checks are enabled and the operator <code>kind</code> cannot be
-     * applied to <code>numArgs</code> arguments.
-     */
-    void checkArity(Kind kind, unsigned int numArgs) throw (ParserException);
-
-    /**
-     * Returns the type for the variable with the given name.
-     * @param name the symbol to lookup
-     * @param type the (namespace) type of the symbol
-     */
-    Type* getType(const std::string& var_name,
-                        SymbolType type = SYM_VARIABLE);
-
-    /** Create a new CVC4 variable expression of the given type. */
-    Expr mkVar(const std::string& name, Type* type);
-
-    /** Create a set of new CVC4 variable expressions of the given
-        type. */
-    const std::vector<Expr>
-    mkVars(const std::vector<std::string> names,
-           Type* type);
-
-
-    /** Create a new variable definition (e.g., from a let binding). */
-    void defineVar(const std::string& name, const Expr& val);
-    /** Remove a variable definition (e.g., from a let binding). */
-    void undefineVar(const std::string& name);
-
-    /**
-     * Creates a new sort with the given name.
-     */
-    Type* newSort(const std::string& name);
-
-    /**
-     * Creates a new sorts with the given names.
-     */
-    const std::vector<Type*>
-    newSorts(const std::vector<std::string>& names);
-
-    /** Is the symbol bound to a boolean variable? */
-    bool isBoolean(const std::string& name);
-
-    /** Is the symbol bound to a function? */
-    bool isFunction(const std::string& name);
-
-    /** Is the symbol bound to a predicate? */
-    bool isPredicate(const std::string& name);
-
-    /** Throws a <code>ParserException</code> with the given error message.
-     * Implementations should fill in the <code>ParserException</code> with
-     * line number information, etc. */
-    virtual void parseError(const std::string& msg) throw (ParserException) = 0;
 
 protected:
 
@@ -313,17 +143,20 @@ protected:
    */
   virtual Expr doParseExpr() throw(ParserException) = 0;
 
-private:
+  inline ParserState* getParserState() const {
+    return d_parserState;
+  }
 
-  /** Sets the done flag */
-  void setDone(bool done = true);
+private:
 
-  /** Lookup a symbol in the given namespace. */
-  Expr getSymbol(const std::string& var_name, SymbolType type);
+  /** Throws a <code>ParserException</code> with the given error message.
+   * Implementations should fill in the <code>ParserException</code> with
+   * line number information, etc. */
+  virtual void parseError(const std::string& msg) throw (ParserException) = 0;
 
-}; // end of class Parser
+}; // end of class Input
 
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__PARSER__PARSER_H */
+#endif /* __CVC4__PARSER__INPUT_H */