diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-04-10 00:44:20 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-04-10 00:44:20 +0000 |
commit | 969b144a5f9630d646afdf0ff0a053df38d0ed1a (patch) | |
tree | 92eb38ad161abfe3af979a86285549168d118c5e /src/parser/parser.h | |
parent | 8495ee8e7de4a7e472d72cfb20290940c59794e3 (diff) |
merge from replay branch
Diffstat (limited to 'src/parser/parser.h')
-rw-r--r-- | src/parser/parser.h | 86 |
1 files changed, 73 insertions, 13 deletions
diff --git a/src/parser/parser.h b/src/parser/parser.h index 9765f352b..15fe5126c 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -2,10 +2,10 @@ /*! \file parser.h ** \verbatim ** Original author: cconway - ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -25,16 +25,17 @@ #include <set> #include <list> -#include "input.h" -#include "parser_exception.h" +#include "parser/input.h" +#include "parser/parser_exception.h" +#include "expr/expr.h" #include "expr/declaration_scope.h" #include "expr/kind.h" +#include "expr/expr_stream.h" namespace CVC4 { // Forward declarations class BooleanType; -class Expr; class ExprManager; class Command; class FunctionType; @@ -106,8 +107,19 @@ class CVC4_PUBLIC Parser { /** The input that we're parsing. */ Input *d_input; - /** The symbol table */ - DeclarationScope d_declScope; + /** + * The declaration scope that is "owned" by this parser. May or + * may not be the current declaration scope in use. + */ + DeclarationScope d_declScopeAllocated; + + /** + * This current symbol table used by this parser. Initially points + * to d_declScopeAllocated, but can be changed (making this parser + * delegate its definitions and lookups to another parser). + * See useDeclarationsFrom(). + */ + DeclarationScope* d_declScope; /** The name of the input file. */ // std::string d_filename; @@ -361,12 +373,60 @@ public: d_input->parseError(msg); } - inline void pushScope() { d_declScope.pushScope(); } - inline void popScope() { d_declScope.popScope(); } -}; // class Parser + inline void pushScope() { d_declScope->pushScope(); } + inline void popScope() { d_declScope->popScope(); } -} // namespace parser + /** + * Set the current symbol table used by this parser. + * From now on, this parser will perform its definitions and + * lookups in the declaration scope of the "parser" argument + * (but doesn't re-delegate if the other parser's declaration scope + * changes later). A NULL argument restores this parser's + * "primordial" declaration scope assigned at its creation. Calling + * p->useDeclarationsFrom(p) is a no-op. + * + * This feature is useful when e.g. reading out-of-band expression data: + * 1. Parsing --replay log files produced with --replay-log. + * 2. Perhaps a multi-query benchmark file is being single-stepped + * with intervening queries on stdin that must reference + * + * However, the feature must be used carefully. Pushes and pops + * should be performed with the correct current declaration scope. + * Care must be taken to match up declaration scopes, of course; + * If variables in the deferred-to parser go out of scope, the + * secondary parser will give errors that they are undeclared. + * Also, an outer-scope variable shadowed by an inner-scope one of + * the same name may be temporarily inaccessible. + * + * In short, caveat emptor. + */ + void useDeclarationsFrom(Parser* parser) { + if(parser == NULL) { + d_declScope = &d_declScopeAllocated; + } else { + d_declScope = parser->d_declScope; + } + } -} // namespace CVC4 + /** + * An expression stream interface for a parser. This stream simply + * pulls expressions from the given Parser object. + * + * Here, the ExprStream base class allows a Parser (from the parser + * library) and core components of CVC4 (in the core library) to + * communicate without polluting the public interface or having them + * reach into private (undocumented) interfaces. + */ + class ExprStream : public CVC4::ExprStream { + Parser* d_parser; + public: + ExprStream(Parser* parser) : d_parser(parser) {} + ~ExprStream() { delete d_parser; } + Expr nextExpr() { return d_parser->nextExpression(); } + };/* class Parser::ExprStream */ +};/* class Parser */ + +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ #endif /* __CVC4__PARSER__PARSER_STATE_H */ |