minor fixes, plus experimental readline support in InteractiveShell

1 files changed, 210 insertions, 39 deletions

diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index cd7947e2e..cf04dacdf 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -12,9 +12,19 @@
  ** information.\endverbatim
  **
  ** \brief Interactive shell for CVC4
+ **
+ ** This file is the implementation for the CVC4 interactive shell.
+ ** The shell supports the readline library.
  **/
 
 #include <iostream>
+#include <vector>
+#include <string>
+#include <set>
+#include <algorithm>
+#include <utility>
+
+#include "cvc4autoconfig.h"
 
 #include "interactive_shell.h"
 
@@ -23,29 +33,95 @@
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "util/options.h"
+#include "util/language.h"
+
+#include <string.h>
+
+#if HAVE_LIBREADLINE
+#  include <readline/readline.h>
+#  include <readline/history.h>
+#  include <ext/stdio_filebuf.h>
+#endif /* HAVE_LIBREADLINE */
 
 using namespace std;
 
 namespace CVC4 {
 
 using namespace parser;
+using namespace language;
 
 const string InteractiveShell::INPUT_FILENAME = "<shell>";
 
+#if HAVE_LIBREADLINE
+
+using __gnu_cxx::stdio_filebuf;
+
+//char** commandCompletion(const char* text, int start, int end);
+char* commandGenerator(const char* text, int state);
+
+static const char* const cvc_commands[] = {
+#include "cvc_tokens.h"
+};/* cvc_commands */
+
+static const char* const smt_commands[] = {
+#include "smt_tokens.h"
+};/* smt_commands */
+
+static const char* const smt2_commands[] = {
+#include "smt2_tokens.h"
+};/* smt2_commands */
+
+static const char* const* commandsBegin;
+static const char* const* commandsEnd;
+
+static set<string> s_declarations;
+
+#endif /* HAVE_LIBREADLINE */
+
 InteractiveShell::InteractiveShell(ExprManager& exprManager,
-                                   const Options& options) : 
-   d_in(*options.in),
-   d_out(*options.out),
-   d_language(options.inputLanguage) {
-   ParserBuilder parserBuilder(&exprManager,INPUT_FILENAME,options);
-   /* Create parser with bogus input. */
-   d_parser = parserBuilder.withStringInput("").build();
+                                   const Options& options) :
+  d_in(*options.in),
+  d_out(*options.out),
+  d_language(options.inputLanguage),
+  d_quit(false) {
+  ParserBuilder parserBuilder(&exprManager,INPUT_FILENAME,options);
+  /* Create parser with bogus input. */
+  d_parser = parserBuilder.withStringInput("").build();
+
+#if HAVE_LIBREADLINE
+  if(d_in == cin) {
+    ::rl_readline_name = "CVC4";
+    ::rl_completion_entry_function = commandGenerator;
+
+    switch(OutputLanguage lang = toOutputLanguage(d_language)) {
+    case output::LANG_CVC4:
+      commandsBegin = cvc_commands;
+      commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands);
+      break;
+    case output::LANG_SMTLIB:
+      commandsBegin = smt_commands;
+      commandsEnd = smt_commands + sizeof(smt_commands) / sizeof(*smt_commands);
+      break;
+    case output::LANG_SMTLIB_V2:
+      commandsBegin = smt2_commands;
+      commandsEnd = smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands);
+      break;
+    default: Unhandled(lang);
+    }
+    d_usingReadline = true;
+  } else {
+    d_usingReadline = false;
+  }
+#else /* HAVE_LIBREADLINE */
+  d_usingReadline = false;
+#endif /* HAVE_LIBREADLINE */
 }/* InteractiveShell::InteractiveShell() */
 
 
 Command* InteractiveShell::readCommand() {
-  /* Don't do anything if the input is closed. */
-  if( d_in.eof() ) {
+  /* Don't do anything if the input is closed or if we've seen a
+   * QuitCommand. */
+  if( d_in.eof() || d_quit ) {
     return NULL;
   }
 
@@ -54,23 +130,35 @@ Command* InteractiveShell::readCommand() {
     throw ParserException("Interactive input broken.");
   }
 
+  char* lineBuf;
   string input;
+  stringbuf sb;
+  string line;
 
   /* Prompt the user for input. */
-  d_out << "CVC4> " << flush;
-  while(true) {
-    stringbuf sb;
-    string line;
+  if(d_usingReadline) {
+#if HAVE_LIBREADLINE
+  lineBuf = ::readline("CVC4> ");
+  if(lineBuf != NULL && lineBuf[0] != '\0') {
+    ::add_history(lineBuf);
+  }
+  line = lineBuf == NULL ? "" : lineBuf;
+  free(lineBuf);
+#endif /* HAVE_LIBREADLINE */
+  } else {
+    d_out << "CVC4> " << flush;
 
     /* Read a line */
     d_in.get(sb,'\n');
     line = sb.str();
-    // cout << "Input was '" << input << "'" << endl << flush;
+  }
+  while(true) {
+    Debug("interactive") << "Input now '" << input << line << "'" << endl << flush;
 
     Assert( !(d_in.fail() && !d_in.eof()) || line.empty() );
 
     /* Check for failure. */
-    if( d_in.fail() && !d_in.eof() ) {
+    if(d_in.fail() && !d_in.eof()) {
       /* This should only happen if the input line was empty. */
       Assert( line.empty() );
       d_in.clear();
@@ -78,13 +166,14 @@ Command* InteractiveShell::readCommand() {
 
     /* Strip trailing whitespace. */
     int n = line.length() - 1;
-    while( !line.empty() && isspace(line[n]) ) { 
-      line.erase(n,1); 
+    while( !line.empty() && isspace(line[n]) ) {
+      line.erase(n,1);
       n--;
     }
 
     /* If we hit EOF, we're done. */
-    if( d_in.eof() ) {
+    if( (!d_usingReadline && d_in.eof()) ||
+        (d_usingReadline && lineBuf == NULL) ) {
       input += line;
 
       if( input.empty() ) {
@@ -92,54 +181,136 @@ Command* InteractiveShell::readCommand() {
         return NULL;
       }
 
-      /* Some input left to parse, but nothing left to read. 
+      /* Some input left to parse, but nothing left to read.
          Jump out of input loop. */
       break;
     }
 
-    /* Extract the newline delimiter from the stream too */
-    int c CVC4_UNUSED = d_in.get();
-    Assert( c == '\n' );
-
-    // cout << "Next char is '" << (char)c << "'" << endl << flush;
+    if(!d_usingReadline) {
+      /* Extract the newline delimiter from the stream too */
+      int c CVC4_UNUSED = d_in.get();
+      Assert( c == '\n' );
+      Debug("interactive") << "Next char is '" << (char)c << "'" << endl << flush;
+    }
 
     input += line;
-    
+
     /* If the last char was a backslash, continue on the next line. */
     n = input.length() - 1;
     if( !line.empty() && input[n] == '\\' ) {
       input[n] = '\n';
-      d_out << "... > " << flush;
+      if(d_usingReadline) {
+#if HAVE_LIBREADLINE
+        lineBuf = ::readline("... > ");
+        if(lineBuf != NULL && lineBuf[0] != '\0') {
+          ::add_history(lineBuf);
+        }
+        line = lineBuf == NULL ? "" : lineBuf;
+        free(lineBuf);
+#endif /* HAVE_LIBREADLINE */
+      } else {
+        d_out << "... > " << flush;
+
+        /* Read a line */
+        d_in.get(sb,'\n');
+        line = sb.str();
+      }
     } else {
       /* No continuation, we're done. */
-      //cout << "Leaving input loop." << endl << flush;
+      Debug("interactive") << "Leaving input loop." << endl << flush;
       break;
     }
   }
 
   d_parser->setInput(Input::newStringInput(d_language,input,INPUT_FILENAME));
-  // Parser *parser = 
-  //   d_parserBuilder
-  //       .withStringInput(input)
-  //       .withStateFrom(d_lastParser)
-  //       .build();
 
   /* There may be more than one command in the input. Build up a
      sequence. */
   CommandSequence *cmd_seq = new CommandSequence();
   Command *cmd;
 
-  while( (cmd = d_parser->nextCommand()) ) {
-    cmd_seq->addCommand(cmd);
+  try {
+    while( (cmd = d_parser->nextCommand()) ) {
+      cmd_seq->addCommand(cmd);
+      if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
+        d_quit = true;
+        break;
+      } else {
+#if HAVE_LIBREADLINE
+        DeclarationCommand* dcmd =
+          dynamic_cast<DeclarationCommand*>(cmd);
+        if(dcmd != NULL) {
+          const vector<string>& ids = dcmd->getDeclaredSymbols();
+          s_declarations.insert(ids.begin(), ids.end());
+        }
+#endif /* HAVE_LIBREADLINE */
+      }
+    }
+  } catch(ParserException& pe) {
+    d_out << pe << endl;
+    // We can't really clear out the sequence and abort the current line,
+    // because the parse error might be for the second command on the
+    // line.  The first ones haven't yet been executed by the SmtEngine,
+    // but the parser state has already made the variables and the mappings
+    // in the symbol table.  So unfortunately, either we exit CVC4 entirely,
+    // or we commit to the current line up to the command with the parse
+    // error.
+    //
+    // FIXME: does that mean e.g. that a pushed LET scope might not yet have
+    // been popped?!
+    //
+    //delete cmd_seq;
+    //cmd_seq = new CommandSequence();
   }
 
-  // if( d_lastParser ) {
-  //   delete d_lastParser;
-  // }
-  // d_lastParser = parser;
-
   return cmd_seq;
 }/* InteractiveShell::readCommand() */
 
+#if HAVE_LIBREADLINE
+
+/*char** commandCompletion(const char* text, int start, int end) {
+  Debug("rl") << "text: " << text << endl;
+  Debug("rl") << "start: " << start << " end: " << end << endl;
+  return rl_completion_matches(text, commandGenerator);
+}*/
+
+// For some reason less<string> crashes on us; oh well,
+// we don't need to copy into string anyway.
+// Can't use less<const char*> because it compares pointers(?).
+struct stringLess {
+  bool operator()(const char* s1, const char* s2) {
+    size_t l1 = strlen(s1), l2 = strlen(s2);
+    return strncmp(s1, s2, l1 <= l2 ? l1 : l2) == -1;
+  }
+};/* struct string_less */
+
+char* commandGenerator(const char* text, int state) {
+  static CVC4_THREADLOCAL(const char* const*) rlPointer;
+  static CVC4_THREADLOCAL(set<string>::const_iterator*) rlDeclaration;
+
+  const char* const* i = lower_bound(commandsBegin, commandsEnd, text, stringLess());
+  const char* const* j = upper_bound(commandsBegin, commandsEnd, text, stringLess());
+
+  set<string>::const_iterator ii = lower_bound(s_declarations.begin(), s_declarations.end(), text, less<string>());
+  set<string>::const_iterator jj = upper_bound(s_declarations.end(), s_declarations.end(), text, less<string>());
+
+  if(rlDeclaration == NULL) {
+    rlDeclaration = new set<string>::const_iterator();
+  }
+
+  if(state == 0) {
+    rlPointer = i;
+    *rlDeclaration = ii;
+  }
+
+  if(rlPointer != j) {
+    return strdup(*rlPointer++);
+  }
+
+  return *rlDeclaration == jj ? NULL : strdup((*(*rlDeclaration)++).c_str());
+}
+
+#endif /* HAVE_LIBREADLINE */
+
 }/* CVC4 namespace */