Support include and reference on command line (#78)

NEWS.md

@@ -6,6 +6,7 @@ ethos 0.1.1 prerelease
 - When parsing Eunoia signatures, decimals and hexidecimals are never normalized, variables in binders are always unique for their name and type, and let is never treated as a builtin way of specifying macros. The options `--no-normalize-dec`, `--no-normalize-hex`, `--binder-fresh`, and `--no-parse-let` now only apply when parsing proofs and reference files.
 - Adds a new option `--normalize-num`, which also only applies when reference parsing. This option treats numerals as rationals, which can be used when parsing SMT-LIB inputs in logics where numerals are shorthand for rationals.
 - Makes the `set-option` command available in proofs and Eunoia files.
+- Adds `--include=X` and `--reference=X` to the command line interface for including (reference) files.
 - Fixed a bug when applying operators with opaque arguments.
 
 ethos 0.1.0

src/lexer.cpp

@@ -182,12 +182,10 @@ const char* Lexer::tokenStr() const
 
 Token Lexer::nextTokenInternal()
 {
- //Trace("lexer-debug") << "Call nextToken" << std::endl;
  d_token.clear();
  Token ret = computeNextToken();
  // null terminate?
  d_token.push_back(0);
- //Trace("lexer-debug") << "Return nextToken " << ret << " / " << tokenStr() << std::endl;
  return ret;
 }
 

src/main.cpp

@@ -22,6 +22,8 @@ int main( int argc, char* argv[] )
 {
  Options opts;
  Stats stats;
+ State s(opts, stats);
+ Plugin* plugin = nullptr;
  // read the options
  size_t i = 1;
  std::string file;
@@ -45,17 +47,32 @@ int main( int argc, char* argv[] )
  continue;
  }
  }
+ bool isInclude = (arg.compare(0, 10, "--include=") == 0);
+ if (isInclude || arg.compare(0, 12, "--reference=") == 0)
+ {
+ size_t first = arg.find_first_of("=");
+ std::string file = arg.substr(first + 1);
+ // cannot provide reference
+ Expr refNf;
+ if (!s.includeFile(file, isInclude, !isInclude, refNf))
+ {
+ EO_FATAL() << "Error: cannot include file " << file;
+ }
+ continue;
+ }
  if (arg == "--help")
  {
  std::stringstream out;
  out << " --binder-fresh: binders generate fresh variables when parsed in proof files." << std::endl;
+ out << " --include=X: includes the file specified by X." << std::endl;
  out << " --help: displays this message." << std::endl;
  out << " --normalize-num: treat numeral literals as syntax sugar for rational literals." << std::endl;
  out << " --no-normalize-dec: do not treat decimal literals as syntax sugar for rational literals." << std::endl;
  out << " --no-normalize-hex: do not treat hexadecimal literals as syntax sugar for binary literals." << std::endl;
  out << " --no-parse-let: do not treat let as a builtin symbol for specifying terms having shared subterms." << std::endl;
  out << " --no-print-let: do not letify the output of terms in error messages and trace messages." << std::endl;
  out << "--no-rule-sym-table: do not use a separate symbol table for proof rules and declared terms." << std::endl;
+ out << " --reference=X: includes the file specified by X as a reference file." << std::endl;
  out << " --show-config: displays the build information for this binary." << std::endl;
  out << " --stats: enables detailed statistics." << std::endl;
  out << " --stats-compact: print statistics in a compact format." << std::endl;
@@ -94,12 +111,11 @@ int main( int argc, char* argv[] )
  {
 // enable all traces
 #ifdef EO_TRACING
- TraceChannel.on("compiler");
  TraceChannel.on("expr_parser");
+ TraceChannel.on("oracles");
  TraceChannel.on("state");
- TraceChannel.on("type_checker");
- TraceChannel.on("compile");
  TraceChannel.on("step");
+ TraceChannel.on("type_checker");
 #else
  EO_FATAL() << "Error: tracing not enabled in this build";
 #endif
@@ -123,8 +139,6 @@ int main( int argc, char* argv[] )
  EO_FATAL() << "Error: mulitple files specified, \"" << file << "\" and \"" << arg << "\"";
  }
  }
- State s(opts, stats);
- Plugin * plugin = nullptr;
  // NOTE: initialization of plugin goes here
  if (plugin!=nullptr)
  {

user_manual.md

@@ -1681,6 +1681,8 @@ Ethos supports the following commands for file inclusion:
 - `(include <string>)`, which includes the file indicated by the given string. The path to the file is taken relative to the directory of the file that includes it.
 - `(reference <string> <symbol>?)`, which similar to `include` includes the file indicated by the given string, and furthermore marks that file as being the _reference input_ for the current run of the checker (see below). The optional symbol can refer to a normalization routine (see below).
 
+Additionally, files may be included or referenced on the command line with the options `--include=X` and `--reference=X` respectively.
+
 ### Validation Proofs via Reference Inputs
 
 When Ethos encounters a command of the form `(reference <string>)`, the checker enables a further set of checks that ensures that all assumptions in proofs correspond to assertions from the file referenced by the given string.
@@ -1787,8 +1789,10 @@ The user is responsible for ensure that e.g. the proof contains a step with a de
 The Ethos command line interface can be invoked by `ethos <option>* <file>` where `<option>` is one of the following:
 
 - `--help`: displays a help message.
+- `--include=X`: includes the file specified by `X`.
 - `--no-print-let`: do not letify the output of terms in error messages and trace messages.
 - `--no-rule-sym-table`: do not use a separate symbol table for proof rules and declared terms.
+- `--reference=X`: includes the file specified by `X` as a reference file.
 - `--show-config`: displays the build information for the given binary.
 - `--stats`: enables detailed statistics.
 - `--stats-compact`: print statistics in a compact format.
@@ -1804,8 +1808,10 @@ They do not impact how signature files (*.eo) are parsed:
 - `--no-normalize-hex`: do not treat hexadecimal literals as syntax sugar for binary literals.
 - `--no-parse-let`: do not treat `let` as a builtin symbol for specifying a macro.
 
-Most of the above options can also be set via `set-option` commands within proofs or Eunoia scripts. 
+Most of the above options can also be set via `set-option` commands within proofs or Eunoia scripts.
 For example, the command `(set-option binder-fresh true)` tells Ethos to generate fresh variables when parsing binders always.
+Further note that option names in this interface should exclude `no-`, which is equivalent to setting the value of the option to false.
+For example, `(set-option normalize-dec false)` is equivalent to the command line option `--no-normalize-dec`.
 
 <a name="full-syntax"></a>