diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-05-01 22:32:32 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-05-01 22:32:32 +0000 |
commit | bf837ea666980a0556d7881316f34be7ad1e2ea2 (patch) | |
tree | 6c0a5eae01f7967c02a0ef84c4bccbacf5dfa35f /src/main/interactive_shell.cpp | |
parent | 89b0369e887b4cf876e95dc862ae3057383370f3 (diff) |
minor fixes, plus experimental readline support in InteractiveShell
Diffstat (limited to 'src/main/interactive_shell.cpp')
-rw-r--r-- | src/main/interactive_shell.cpp | 249 |
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 */ |