File inclusion in Smt2 parser.

The extended command (include-file "filename") now includes file content.

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index cd622b8a61d769c3708e80b9a2f028c5a9a9ec90..d498d3c548826072850a1d5c94d00a0c2cbf78de 100644 (file)
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -46,9 +46,10 @@ namespace parser {
 AntlrInputStream::AntlrInputStream(std::string name, 
                                    pANTLR3_INPUT_STREAM input,
                                    bool fileIsTemporary) :
-  InputStream(name,fileIsTemporary),
+  InputStream(name, fileIsTemporary),
   d_input(input) {
   assert( input != NULL );
+  input->fileName = input->strFactory->newStr8(input->strFactory, (pANTLR3_UINT8)name.c_str());
 }
 
 AntlrInputStream::~AntlrInputStream() {
@@ -286,16 +287,18 @@ void AntlrInput::warning(const std::string& message) {
 void AntlrInput::parseError(const std::string& message, bool eofException)
   throw (ParserException) {
   Debug("parser") << "Throwing exception: "
-      << getInputStream()->getName() << ":"
+      << (const char*)d_lexer->rec->state->tokSource->fileName->chars << ":"
       << d_lexer->getLine(d_lexer) << "."
       << d_lexer->getCharPositionInLine(d_lexer) << ": "
       << message << endl;
   if(eofException) {
-    throw ParserEndOfFileException(message, getInputStream()->getName(),
+    throw ParserEndOfFileException(message,
+                                   (const char*)d_lexer->rec->state->tokSource->fileName->chars,
                                    d_lexer->getLine(d_lexer),
                                    d_lexer->getCharPositionInLine(d_lexer));
   } else {
-    throw ParserException(message, getInputStream()->getName(),
+    throw ParserException(message,
+                          (const char*)d_lexer->rec->state->tokSource->fileName->chars,
                           d_lexer->getLine(d_lexer),
                           d_lexer->getCharPositionInLine(d_lexer));
   }

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 133cedfbd84d7957c901d3e648f73415e53de192..29bc8d40f9695f0368480bdd5a880519581b1414 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -188,7 +188,23 @@ parseExpr returns [CVC4::parser::smt2::myExpr expr]
  * @return the parsed command, or NULL if we've reached the end of the input
  */
 parseCommand returns [CVC4::Command* cmd = NULL]
+@declarations {
+  std::string name;
+}
   : LPAREN_TOK c = command RPAREN_TOK { $cmd = c; }
+
+    /* This extended command has to be in the outermost production so that
+     * the RPAREN_TOK is properly eaten and we are in a good state to read
+     * the included file's tokens. */
+  | LPAREN_TOK INCLUDE_TOK str[name] RPAREN_TOK
+    { if(PARSER_STATE->strictModeEnabled()) {
+        PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode.");
+      }
+      PARSER_STATE->includeFile(name);
+      // The command of the included file will be produced at the next parseCommand() call
+      cmd = new EmptyCommand("include::" + name);
+    }
+
   | EOF { $cmd = 0; }
   ;
 
@@ -1464,6 +1480,7 @@ DECLARE_PREDS_TOK : 'declare-preds';
 DEFINE_TOK : 'define';
 DECLARE_CONST_TOK : 'declare-const';
 SIMPLIFY_TOK : 'simplify';
+INCLUDE_TOK : 'include-file';
 
 // attributes
 ATTRIBUTE_PATTERN_TOK : ':pattern';

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index c042c39926e7adefcd6beeefe5003a647e71ead4..be4907e8e68aa30e0a3ccac9d32343326e538c49 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -19,6 +19,11 @@
 #include "parser/parser.h"
 #include "parser/smt1/smt1.h"
 #include "parser/smt2/smt2.h"
+#include "parser/antlr_input.h"
+
+// ANTLR defines these, which is really bad!
+#undef true
+#undef false
 
 namespace CVC4 {
 namespace parser {
@@ -200,5 +205,60 @@ void Smt2::checkThatLogicIsSet() {
   }
 }
 
+/* The include are managed in the lexer but called in the parser */
+// Inspired by http://www.antlr3.org/api/C/interop.html
+
+static bool newInputStream(const std::string& filename, pANTLR3_LEXER lexer) {
+  Debug("parser") << "Including " << filename << std::endl;
+  // Create a new input stream and take advantage of built in stream stacking
+  // in C target runtime.
+  //
+  pANTLR3_INPUT_STREAM    in;
+#ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
+  in = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str());
+#else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
+  in = antlr3FileStreamNew((pANTLR3_UINT8) filename.c_str(), ANTLR3_ENC_8BIT);
+#endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
+  if( in == NULL ) {
+    Debug("parser") << "Can't open " << filename << std::endl;
+    return false;
+  }
+  // Same thing as the predefined PUSHSTREAM(in);
+  lexer->pushCharStream(lexer, in);
+  // restart it
+  //lexer->rec->state->tokenStartCharIndex      = -10;
+  //lexer->emit(lexer);
+
+  // Note that the input stream is not closed when it EOFs, I don't bother
+  // to do it here, but it is up to you to track streams created like this
+  // and destroy them when the whole parse session is complete. Remember that you
+  // don't want to do this until all tokens have been manipulated all the way through
+  // your tree parsers etc as the token does not store the text it just refers
+  // back to the input stream and trying to get the text for it will abort if you
+  // close the input stream too early.
+
+  //TODO what said before
+  return true;
+}
+
+void Smt2::includeFile(const std::string& filename) {
+  // Get the lexer
+  AntlrInput* ai = static_cast<AntlrInput*>(getInput());
+  pANTLR3_LEXER lexer = ai->getAntlr3Lexer();
+  // get the name of the current stream "Does it work inside an include?"
+  const std::string inputName = ai->getInputStreamName();
+
+  // Find the directory of the current input file
+  std::string path;
+  size_t pos = inputName.rfind('/');
+  if(pos != std::string::npos) {
+    path = std::string(inputName, 0, pos + 1);
+  }
+  path.append(filename);
+  if(!newInputStream(path, lexer)) {
+    parseError("Couldn't open include file `" + path + "'");
+  }
+}
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 7a464c77326108ef65f0a0b4dcd60d5563cad8b7..c50a0972b15a30344993c5b80c3188b523708476 100644 (file)
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -85,6 +85,8 @@ public:
     }
   }
 
+  void includeFile(const std::string& filename);
+
   bool isAbstractValue(const std::string& name) {
     return name.length() >= 2 && name[0] == '@' && name[1] != '0' &&
       name.find_first_not_of("0123456789", 1) == std::string::npos;