Options classes (runtimeverification/pyk#976)

Adds `Options` class hierarchy which stores all the parameters
associated with command line options for pyk, and is extendable by
downstream projects. This is a part of the changes pulled out from #967.
- Adds `Options` which automatically populates its fields from a
prepared `dict` from the parsed command line args and sets default
values when the values are missing
- Adds `LoggingOptions`, etc., which are groups of options that can be
inherited by commands
- Adds `ProveOptions`, etc. which are directly associated with
particular pyk commands but otherwise behave the same
- `exec_*` functions now take the corresponding `*Options` type instead
of generic `Namespace`
- Defaults are no longer set at the argparse level since they are now
set in `Options` constructor.

---------

Co-authored-by: devops <devops@runtimeverification.com>

pyk/docs/conf.py

@@ -9,8 +9,8 @@
 project = 'pyk'
 author = 'Runtime Verification, Inc'
 copyright = '2024, Runtime Verification, Inc'
-version = '0.1.711'
-release = '0.1.711'
+version = '0.1.712'
+release = '0.1.712'
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

pyk/package/version

@@ -1 +1 @@
-0.1.711
+0.1.712

pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.711"
+version = "0.1.712"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

pyk/src/pyk/cli/args.py

@@ -1,16 +1,156 @@
 from __future__ import annotations
 
+import sys
 from argparse import ArgumentParser
 from functools import cached_property
-from typing import TYPE_CHECKING
+from typing import IO, TYPE_CHECKING, Any
 
-from ..utils import ensure_dir_path
+from pyk.utils import ensure_dir_path
+
+from .cli import Options
 from .utils import bug_report_arg, file_path
 
 if TYPE_CHECKING:
-    from typing import TypeVar
+    from pathlib import Path
+
+    from ..utils import BugReport
+
+
+class LoggingOptions(Options):
+    debug: bool
+    verbose: bool
+
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {
+            'verbose': False,
+            'debug': False,
+        }
+
+
+class OutputFileOptions(Options):
+    output_file: IO[Any]
+
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {
+            'output_file': sys.stdout,
+        }
+
+
+class DefinitionOptions(Options):
+    definition_dir: Path
+
+
+class DisplayOptions(Options):
+    minimize: bool
+
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {
+            'minimize': True,
+        }
+
+
+class KDefinitionOptions(Options):
+    includes: list[str]
+    main_module: str | None
+    syntax_module: str | None
+    spec_module: str | None
+    md_selector: str
+
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {
+            'spec_module': None,
+            'main_module': None,
+            'syntax_module': None,
+            'md_selector': 'k',
+            'includes': [],
+        }
+
+
+class SaveDirOptions(Options):
+    save_directory: Path | None
+
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {
+            'save_directory': None,
+        }
+
+
+class SpecOptions(SaveDirOptions):
+    spec_file: Path
+    claim_labels: list[str] | None
+    exclude_claim_labels: list[str]
+
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {
+            'claim_labels': None,
+            'exclude_claim_labels': [],
+        }
+
+
+class KompileOptions(Options):
+    emit_json: bool
+    ccopts: list[str]
+    llvm_kompile: bool
+    llvm_library: bool
+    enable_llvm_debug: bool
+    read_only: bool
+    o0: bool
+    o1: bool
+    o2: bool
+    o3: bool
+
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {
+            'emit_json': True,
+            'llvm_kompile': False,
+            'llvm_library': False,
+            'enable_llvm_debug': False,
+            'read_only': False,
+            'o0': False,
+            'o1': False,
+            'o2': False,
+            'o3': False,
+            'ccopts': [],
+        }
+
+
+class ParallelOptions(Options):
+    workers: int
+
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {
+            'workers': 1,
+        }
+
+
+class BugReportOptions(Options):
+    bug_report: BugReport | None
+
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {'bug_report': None}
+
+
+class SMTOptions(Options):
+    smt_timeout: int
+    smt_retry_limit: int
+    smt_tactic: str | None
 
-    T = TypeVar('T')
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {
+            'smt_timeout': 300,
+            'smt_retry_limit': 10,
+            'smt_tactic': None,
+        }
 
 
 class KCLIArgs:
@@ -122,8 +262,8 @@ def definition_args(self) -> ArgumentParser:
         args.add_argument(
             '-I', type=str, dest='includes', default=[], action='append', help='Directories to lookup K definitions in.'
         )
-        args.add_argument('--main-module', default=None, type=str, help='Name of the main module.')
-        args.add_argument('--syntax-module', default=None, type=str, help='Name of the syntax module.')
+        args.add_argument('--main-module', type=str, help='Name of the main module.')
+        args.add_argument('--syntax-module', type=str, help='Name of the syntax module.')
         args.add_argument(
             '--md-selector',
             type=str,

pyk/src/pyk/cli/cli.py

@@ -0,0 +1,18 @@
+from __future__ import annotations
+
+from typing import Any
+
+
+class Options:
+    def __init__(self, args: dict[str, Any]) -> None:
+        # Get defaults from this and all superclasses that define them, preferring the most specific class
+        defaults: dict[str, Any] = {}
+        for cl in reversed(type(self).mro()):
+            if hasattr(cl, 'default'):
+                defaults = defaults | cl.default()
+
+        # Overwrite defaults with args from command line
+        _args = defaults | args
+
+        for attr, val in _args.items():
+            self.__setattr__(attr, val)

pyk/src/pyk/cli/pyk.py

@@ -0,0 +1,145 @@
+from __future__ import annotations
+
+from enum import Enum
+from typing import IO, TYPE_CHECKING, Any
+
+from pyk.ktool.kompile import KompileBackend
+
+from .args import DefinitionOptions, DisplayOptions, KDefinitionOptions, LoggingOptions, OutputFileOptions
+
+if TYPE_CHECKING:
+    from collections.abc import Iterable
+    from pathlib import Path
+
+    from pyk.ktool import TypeInferenceMode
+
+
+def generate_options(args: dict[str, Any]) -> LoggingOptions:
+    command = args['command']
+    match command:
+        case 'json-to-kore':
+            return JsonToKoreOptions(args)
+        case 'kore-to-json':
+            return KoreToJsonOptions(args)
+        case 'coverage':
+            return CoverageOptions(args)
+        case 'graph-imports':
+            return GraphImportsOptions(args)
+        case 'rpc-kast':
+            return RPCKastOptions(args)
+        case 'rpc-print':
+            return RPCPrintOptions(args)
+        case 'print':
+            return PrintOptions(args)
+        case 'prove-legacy':
+            return ProveLegacyOptions(args)
+        case 'prove':
+            return ProveOptions(args)
+        case 'kompile':
+            return KompileCommandOptions(args)
+        case 'run':
+            return RunOptions(args)
+        case _:
+            raise ValueError(f'Unrecognized command: {command}')
+
+
+class PrintInput(Enum):
+    KORE_JSON = 'kore-json'
+    KAST_JSON = 'kast-json'
+
+
+class JsonToKoreOptions(LoggingOptions):
+    ...
+
+
+class KoreToJsonOptions(LoggingOptions):
+    ...
+
+
+class CoverageOptions(DefinitionOptions, OutputFileOptions, LoggingOptions):
+    coverage_file: IO[Any]
+
+
+class GraphImportsOptions(DefinitionOptions, LoggingOptions):
+    ...
+
+
+class RPCKastOptions(OutputFileOptions, LoggingOptions):
+    reference_request_file: IO[Any]
+    response_file: IO[Any]
+
+
+class RPCPrintOptions(DefinitionOptions, OutputFileOptions, LoggingOptions):
+    input_file: IO[Any]
+
+
+class PrintOptions(DefinitionOptions, OutputFileOptions, DisplayOptions, LoggingOptions):
+    term: IO[Any]
+    input: PrintInput
+    minimize: bool
+    omit_labels: str | None
+    keep_cells: str | None
+
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {
+            'input': PrintInput.KAST_JSON,
+            'omit_labels': None,
+            'keep_cells': None,
+        }
+
+
+class ProveLegacyOptions(DefinitionOptions, OutputFileOptions, LoggingOptions):
+    main_file: Path
+    spec_file: Path
+    spec_module: str
+    k_args: Iterable[str]
+
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {
+            'k_args': [],
+        }
+
+
+class KompileCommandOptions(LoggingOptions, KDefinitionOptions):
+    definition_dir: Path | None
+    main_file: str
+    backend: KompileBackend
+    type_inference_mode: TypeInferenceMode | None
+
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {
+            'definition_dir': None,
+            'backend': KompileBackend.LLVM,
+            'type_inference_mode': None,
+        }
+
+
+class ProveOptions(LoggingOptions):
+    spec_file: Path
+    definition_dir: Path | None
+    spec_module: str | None
+    type_inference_mode: TypeInferenceMode | None
+    failure_info: bool
+
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {
+            'definition_dir': None,
+            'spec_module': None,
+            'type_inference_mode': None,
+            'failure_info': False,
+        }
+
+
+class RunOptions(LoggingOptions):
+    pgm_file: str
+    definition_dir: Path | None
+
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {
+            'definition_dir': None,
+        }