Adding arguments to kprove flags (#3648)

Follow up of #3619,  #3638, and #3642!

This PR enhances the usability of `kprove --help` and `kprove
--help-hidden` by providing flag descriptors to help the user understand
when an argument needs to be provided to the flag.


Ex.:

Before
``` 
Usage: kprove [options] <file>
  Options:
    --branching-allowed
      Number of branching events allowed before a forcible stop.
      Default: 2147483647
```

Now:
```
Usage: kprove [options] <file>
  Options:
    --branching-allowed <value>
      Number of branching events allowed before a forcible stop.
      Default: 2147483647
```

Among others, this PR introduces the following arguments to the
respective parameters:

parameter | argument
-- | --
--branching-allowed | \<number>
--claims | \<labels>
--color | \<mode>
--debug-script | \<file>
--default-claim-type | \<type>
--definition | \<path>
--depth | \<number>
--emit-json-spec | \<file>
--exclude | \<labels>
--output, -o | \<mode>
--output-file | \<file>
--output-flatten | \<KLabels>
--output-omit | \<KLabels>
--output-tokast | \<KLabels>
--output-tokenize | \<KLabels>
--spec-module, -sm |  \<name>
--trusted | \<labels>
--haskell-backend-command | \<command>
--haskell-backend-home | \<directory>
--smt-timeout | \<milliseconds>

haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java

@@ -9,13 +9,16 @@
 @RequestScoped
 public class HaskellKRunOptions {
 
-    @Parameter(names="--haskell-backend-command", description="Command to run the Haskell backend execution engine.", hidden = true)
+    @Parameter(names="--haskell-backend-command", descriptionKey = "command",
+            description="Command to run the Haskell backend execution engine.", hidden = true)
     public String haskellBackendCommand = "kore-exec";
 
-    @Parameter(names="--haskell-backend-home", description="Directory where the Haskell backend source installation resides.", hidden = true)
+    @Parameter(names="--haskell-backend-home", descriptionKey = "directory",
+            description="Directory where the Haskell backend source installation resides.", hidden = true)
     public String haskellBackendHome = System.getenv("KORE_HOME");
 
-    @Parameter(names="--default-claim-type", converter = SentenceTypeConverter.class, description="Default type for claims. Values: [all-path|one-path].")
+    @Parameter(names="--default-claim-type", descriptionKey = "type", converter = SentenceTypeConverter.class,
+            description="Default type for claims. Values: [all-path|one-path].")
     public ModuleToKORE.SentenceType defaultClaimType = ModuleToKORE.SentenceType.ALL_PATH;
 
     public static class SentenceTypeConverter extends BaseEnumConverter<ModuleToKORE.SentenceType> {

kernel/src/main/java/org/kframework/kast/KastOptions.java

@@ -128,7 +128,7 @@ public Sort convert(String arg) {
         }
     }
 
-    @Parameter(names={"--module", "-m"}, descriptionKey = "module",
+    @Parameter(names={"--module", "-m"}, descriptionKey = "name",
             description="Parse text in the specified module. Defaults to the syntax module of the definition.")
     public String module;
 

kernel/src/main/java/org/kframework/kompile/KompileOptions.java

@@ -52,7 +52,9 @@ GlobalOptions getGlobalOptions_UseOnlyInGuiceProvider() {
     @Parameter(names="--backend", description="Choose a backend. <backend> is one of [llvm|haskell|kore]. Each creates the kompiled K definition.", descriptionKey = "backend")
     public String backend = Backends.LLVM;
 
-    @Parameter(names="--main-module", description="Specify main module in which a program starts to execute. This information is used by 'krun'. The default is the name of the given K definition file without the extension (.k).")
+    @Parameter(names="--main-module", descriptionKey = "name",
+            description="Specify main module in which a program starts to execute. This information is used by 'krun'. " +
+            "The default is the name of the given K definition file without the extension (.k).")
     private String mainModule;
 
     public String mainModule(FileUtil files) {
@@ -62,7 +64,8 @@ public String mainModule(FileUtil files) {
         return mainModule;
     }
 
-    @Parameter(names="--syntax-module", description="Specify main module for syntax. This information is used by 'krun'. (Default: <main-module>-SYNTAX).", descriptionKey = "module")
+    @Parameter(names="--syntax-module", descriptionKey = "name",
+            description="Specify main module for syntax. This information is used by 'krun'. (Default: <main-module>-SYNTAX).")
     private String syntaxModule;
 
     public String syntaxModule(FileUtil files) {

kernel/src/main/java/org/kframework/kprove/KProveOptions.java

@@ -55,33 +55,40 @@ public synchronized File specFile(FileUtil files) {
     @ParametersDelegate
     public PrintOptions print = new PrintOptions();
 
-    @Parameter(names="--branching-allowed", arity = 1, description="Number of branching events allowed before a forcible stop.")
+    @Parameter(names="--branching-allowed", descriptionKey = "number", arity = 1,
+            description="Number of branching events allowed before a forcible stop.")
     public int branchingAllowed = Integer.MAX_VALUE;
 
-    @Parameter(names={"--spec-module", "-sm"}, description="Name of module containing specification to prove")
+    @Parameter(names={"--spec-module", "-sm"}, descriptionKey = "name",
+            description="Name of module containing specification to prove")
     public String specModule;
 
-    @Parameter(names="--depth", description="The maximum number of computational steps to prove")
+    @Parameter(names="--depth", descriptionKey = "number",
+            description="The maximum number of computational steps to prove")
     public Integer depth;
 
-    @Parameter(names="--trusted", description="Mark this comma separated list of claims as [trusted]")
+    @Parameter(names="--trusted", descriptionKey = "labels",
+            description="Mark this comma separated list of claims as [trusted]")
     public List<String> trusted = null;
 
-    @Parameter(names="--exclude", description="Exclude this comma separated list of claims")
+    @Parameter(names="--exclude", descriptionKey = "labels", description="Exclude this comma separated list of claims")
     public List<String> exclude = null;
 
-    @Parameter(names="--claims", description="Only keep this comma separated list of claims")
+    @Parameter(names="--claims", descriptionKey = "labels", description="Only keep this comma separated list of claims")
     public List<String> claims = null;
 
-    @Parameter(names="--debugger", description="Launch proof in an interactive debugger. Currently only supported by the Haskell backend.")
+    @Parameter(names="--debugger",
+            description="Launch proof in an interactive debugger. Currently only supported by the Haskell backend.")
     public boolean debugger;
 
-    @Parameter(names="--debug-script", description="Run script passed in specified file when the debugger starts. Used with --debugger.")
+    @Parameter(names="--debug-script", descriptionKey = "file",
+            description="Run script passed in specified file when the debugger starts. Used with --debugger.")
     public String debugScript;
 
     @Parameter(names="--emit-json", description="Emit JSON serialized main definition for proving.")
     public boolean emitJson = false;
 
-    @Parameter(names="--emit-json-spec", description="If set, emit the JSON serialization of the spec module to the specified file.")
+    @Parameter(names="--emit-json-spec", descriptionKey = "file",
+            description="If set, emit the JSON serialization of the spec module to the specified file.")
     public String emitJsonSpec = null;
 }

kernel/src/main/java/org/kframework/utils/options/OutputDirectoryOptions.java

@@ -13,9 +13,13 @@ public OutputDirectoryOptions() {}
     @Inject
     public OutputDirectoryOptions(Void v) {}
 
-    @Parameter(names={"--directory", "-d"}, description="[DEPRECATED] Path to the directory in which the output resides. An output can be either a kompiled K definition or a document which depends on the type of backend. The default is the directory containing the main definition file.", descriptionKey = "path", hidden = true)
+    @Parameter(names={"--directory", "-d"},
+            description="[DEPRECATED] Path to the directory in which the output resides. An output can be either a " +
+                    "kompiled K definition or a document which depends on the type of backend. The default is the " +
+                    "directory containing the main definition file.", descriptionKey = "path", hidden = true)
     public String directory;
 
-    @Parameter(names={"--output-definition", "-o"}, description="Path to the exact directory in which the output resides.", descriptionKey = "path")
+    @Parameter(names={"--output-definition", "-o"},
+            description="Path to the exact directory in which the output resides.", descriptionKey = "path")
     public String outputDirectory;
 }

kernel/src/main/java/org/kframework/utils/options/SMTOptions.java

@@ -14,7 +14,8 @@ public SMTOptions() {}
     @Inject
     public SMTOptions(Void v) {}
 
-    @Parameter(names="--smt", converter=SMTSolverConverter.class, description="SMT solver to use for checking constraints. <executable> is one of [z3|none].", descriptionKey = "executable", hidden = true)
+    @Parameter(names="--smt", descriptionKey = "executable", converter=SMTSolverConverter.class,
+            description="SMT solver to use for checking constraints. <executable> is one of [z3|none].", hidden = true)
     public SMTSolver smt = SMTSolver.Z3;
 
     public static class SMTSolverConverter extends BaseEnumConverter<SMTSolver> {
@@ -29,25 +30,30 @@ public Class<SMTSolver> enumClass() {
         }
     }
 
-    @Parameter(names="--ignore-missing-smtlib-warning", description="Suppress warning when SMTLib translation fails.", hidden = true)
+    @Parameter(names="--ignore-missing-smtlib-warning",
+            description="Suppress warning when SMTLib translation fails.", hidden = true)
     public boolean ignoreMissingSMTLibWarning = false;
 
-    @Parameter(names="--floats-as-po", description="Abstracts floating-point values as a partial order relation.", hidden = true)
+    @Parameter(names="--floats-as-po",
+            description="Abstracts floating-point values as a partial order relation.", hidden = true)
     public boolean floatsAsPO = false;
 
     @Parameter(names="--maps-as-int-array", description="Abstracts map values as an array of ints.", hidden = true)
     public boolean mapAsIntArray = false;
 
-    @Parameter(names={"--smt-prelude", "--smt_prelude"}, description="Path to the SMT prelude file.", descriptionKey = "path", hidden = true)
+    @Parameter(names={"--smt-prelude", "--smt_prelude"},
+            description="Path to the SMT prelude file.", descriptionKey = "path", hidden = true)
     public String smtPrelude;
 
-    @Parameter(names="--smt-timeout", description="Timeout for calls to the SMT solver, in milliseconds.", hidden = true)
+    @Parameter(names="--smt-timeout", descriptionKey = "milliseconds",
+            description="Timeout for calls to the SMT solver, in milliseconds.", hidden = true)
     public Integer smtTimeout = null;
 
     @Parameter(names="--z3-jni", description="Invokes Z3 as JNI library. Default is external process. " +
             "JNI is slightly faster, but can potentially lead to JVM crash.", hidden = true)
     public boolean z3JNI = false;
 
-    @Parameter(names="--z3-tactic", description="The path to solver tactic to use to check satisfiability in Z3.", descriptionKey = "solver", hidden = true)
+    @Parameter(names="--z3-tactic", descriptionKey = "solver",
+            description="The path to solver tactic to use to check satisfiability in Z3.", hidden = true)
     public String z3Tactic;
 }