Require programs and oracles to have at least one argument (#135)

Also drops support for general extensions to the syntax for
program/declare-rule, which we decided not to focus on.

Author: ajreynol

NEWS.md

@@ -18,6 +18,7 @@ ethos 0.1.2 prerelease
 - The option `--print-let` has been renamed to `--print-dag` and is now enabled by default. The printer is changed to use `eo::define` instead of `let`.
 - Ethos now explicitly forbids `:var`, `:implicit`, and `:opaque` on return types.
 - The option `--binder-fresh`, which specified for fresh variables to be constructed when parsing binders, has been removed.
+- Programs and oracles now are explicitly required to have at least one argument.
 
 ethos 0.1.1
 ===========

src/cmd_parser.cpp

@@ -161,6 +161,10 @@ bool CmdParser::parseNextCommand()
       sk = Kind::CONST;
       if (tok==Token::DECLARE_ORACLE_FUN)
       {
+        if (sorts.empty())
+        {
+          d_lex.parseError("Oracle functions must have at least one argument");
+        }
         ck = Attr::ORACLE;
         sk = Kind::ORACLE;
         std::string oname = d_eparser.parseSymbol();
@@ -360,14 +364,6 @@ bool CmdParser::parseNextCommand()
       }
       d_state.pushScope();
       std::string name = d_eparser.parseSymbol();
-      if (d_lex.peekToken()==Token::KEYWORD)
-      {
-        std::string keyword = d_eparser.parseKeyword();
-        if (keyword!="ethos")
-        {
-          d_lex.parseError("Unsupported rule format");
-        }
-      }
       std::vector<Expr> vs =
           d_eparser.parseAndBindSortedVarList(Kind::PROOF_RULE);
       Expr assume;
@@ -717,14 +713,6 @@ bool CmdParser::parseNextCommand()
     case Token::PROGRAM:
     {
       std::string name = d_eparser.parseSymbol();
-      if (d_lex.peekToken()==Token::KEYWORD)
-      {
-        std::string keyword = d_eparser.parseKeyword();
-        if (keyword!="ethos")
-        {
-          d_lex.parseError("Unsupported program format");
-        }
-      }
       // push the scope
       d_state.pushScope();
       std::vector<Expr> vars =
@@ -736,6 +724,10 @@ bool CmdParser::parseNextCommand()
       {
         progType = d_state.mkProgramType(argTypes, retType);
       }
+      else
+      {
+        d_lex.parseError("Programs must have at least one argument");
+      }
       // it may have been forward declared
       Expr pprev = d_state.getVar(name);
       Expr pvar;

user_manual.md

@@ -1275,16 +1275,6 @@ The selectors of a constructor (which are never ambiguous) are returned independ
 
 The generic syntax for a `declare-rule` command accepted by `ethos` is:
 
-```smt
-(declare-rule <symbol> <keyword>? <sexpr>*)
-```
-
-When parsing this command, `ethos` will determine the format of the expected arguments based on the given keyword.
-If the `<keyword>` is not provided, then we assume it has been marked `:ethos`.
-All rules not marked with `:ethos` are not supported by the checker and will cause it to terminate.
-
-If the keyword is `:ethos`, then the expected syntax that follows is given below:
-
 ```smt
 (declare-rule <symbol> :ethos (<typed-param>*) <assumption>? <premises>? <arguments>? <reqs>? :conclusion <term> <attr>*)
 where
@@ -1456,22 +1446,12 @@ Locally assumptions can be arbitrarily nested, for example the above can be exte
 
 ## Side Conditions
 
-Similar to `declare-rule`, Ethos supports an extensible syntax for programs whose generic syntax is given by:
-
-```smt
-(program <symbol> <keyword>? <sexpr>*)
-```
-
-When parsing this command, `ethos` will determine the format of the expected arguments based on the given keyword.
-If the `<keyword>` is not provided, then we assume it has been marked `:ethos`.
-All programs not marked with `:ethos` are not supported by the checker and will cause it to terminate.
-
-If the keyword is `:ethos`, then the expected syntax that follows is given below, and is used for defining recursive programs.
+Ethos supports a `program` command for defining recursive programs.
 In particular, in Ethos, a program is an ordered list of rewrite rules.
 The syntax for this command is as follows.
 
 ```smt
-(program <symbol> :ethos (<typed-param>*) (<type>*) <type> ((<term> <term>)+))
+(program <symbol> :ethos (<typed-param>*) (<type>+) <type> ((<term> <term>)+))
 ```
 
 This command declares a program named `<symbol>`.
@@ -1882,7 +1862,7 @@ The syntax and semantics of such functions are described in this [paper](https:/
 In particular, Ethos supports the command:
 
 ```smt
-(declare-oracle-fun <symbol> (<type>*) <type> <symbol>)
+(declare-oracle-fun <symbol> (<type>+) <type> <symbol>)
 ```
 
 Like the `declare-fun` command from SMT-LIB, this command declares a constant named `<symbol>` whose type is given by the argument types and return type.
@@ -1984,15 +1964,13 @@ When streaming input to Ethos, we assume the input is being given for a proof fi
     (assume-push <symbol> <term>) |
     (declare-consts <lit-category> <type>) |
     (declare-parameterized-const <symbol> (<typed-param>*) <type> <attr>*) |
-    (declare-oracle-fun <symbol> (<type>*) <type> <symbol>) |
-    (declare-rule <symbol> <keyword> <sexpr>*) |
+    (declare-oracle-fun <symbol> (<type>+) <type> <symbol>) |
     (declare-rule <symbol> (<typed-param>*) <assumption>? <premises>? <arguments>? <reqs>? :conclusion <term> <attr>*) |
     (declare-type <symbol> (<type>*)) |
     (define <symbol> (<typed-param>*) <term> <attr>*) |
     (define-type <symbol> (<type>*) <type>) |
     (include <string>) |
-    (program <symbol> <keyword> <sexpr>*) |
-    (program <symbol> (<typed-param>*) (<type>*) <type> ((<term> <term>)+)) |
+    (program <symbol> (<typed-param>*) (<type>+) <type> ((<term> <term>)+)) |
     (reference <string> <symbol>?) |
     (step <symbol> <term>? :rule <symbol> <simple-premises>? <arguments>?) |
     (step-pop <symbol> <term>? :rule <symbol> <simple-premises>? <arguments>?) |