add toml support for pyk options

docs/conf.py

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

package/version

@@ -1 +1 @@
-0.1.779
+0.1.780

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.779"
+version = "0.1.780"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/pyk/__main__.py

@@ -3,17 +3,14 @@
 import json
 import logging
 import sys
-from argparse import ArgumentParser, FileType
 from collections.abc import Iterable
-from enum import Enum
 from pathlib import Path
 from typing import TYPE_CHECKING
 
 from graphviz import Digraph
 
-from .cli.args import KCLIArgs
-from .cli.pyk import generate_options
-from .cli.utils import LOG_FORMAT, dir_path, file_path, loglevel
+from .cli.pyk import PrintInput, create_argument_parser, generate_options, parse_toml_args
+from .cli.utils import LOG_FORMAT, loglevel
 from .coverage import get_rule_by_id, strip_coverage_logger
 from .cterm import CTerm
 from .kast.inner import KInner
@@ -30,7 +27,6 @@
 from .kore.parser import KoreParser
 from .kore.rpc import ExecuteResult, StopReason
 from .kore.syntax import Pattern, kore_term
-from .ktool import TypeInferenceMode
 from .ktool.kompile import Kompile, KompileBackend
 from .ktool.kprint import KPrint
 from .ktool.kprove import KProve
@@ -61,11 +57,6 @@
 _LOGGER: Final = logging.getLogger(__name__)
 
 
-class PrintInput(Enum):
-    KORE_JSON = 'kore-json'
-    KAST_JSON = 'kast-json'
-
-
 def main() -> None:
     # KAST terms can end up nested quite deeply, because of the various assoc operators (eg. _Map_, _Set_, ...).
     # Most pyk operations are defined recursively, meaning you get a callstack the same depth as the term.
@@ -74,10 +65,12 @@ def main() -> None:
 
     cli_parser = create_argument_parser()
     args = cli_parser.parse_args()
+    toml_args = parse_toml_args(args)
 
-    stripped_args = {
+    stripped_args = toml_args | {
         key: val for (key, val) in vars(args).items() if val is not None and not (isinstance(val, Iterable) and not val)
     }
+
     options = generate_options(stripped_args)
 
     logging.basicConfig(level=loglevel(args), format=LOG_FORMAT)
@@ -375,121 +368,5 @@ def exec_json_to_kore(options: JsonToKoreOptions) -> None:
     sys.stdout.write('\n')
 
 
-def create_argument_parser() -> ArgumentParser:
-    k_cli_args = KCLIArgs()
-
-    pyk_args = ArgumentParser()
-    pyk_args_command = pyk_args.add_subparsers(dest='command', required=True)
-
-    print_args = pyk_args_command.add_parser(
-        'print',
-        help='Pretty print a term.',
-        parents=[k_cli_args.logging_args, k_cli_args.display_args],
-    )
-    print_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.')
-    print_args.add_argument('term', type=FileType('r'), help='Input term (in format specified with --input).')
-    print_args.add_argument('--input', type=PrintInput, choices=list(PrintInput))
-    print_args.add_argument('--omit-labels', nargs='?', help='List of labels to omit from output.')
-    print_args.add_argument('--keep-cells', nargs='?', help='List of cells with primitive values to keep in output.')
-    print_args.add_argument('--output-file', type=FileType('w'))
-
-    rpc_print_args = pyk_args_command.add_parser(
-        'rpc-print',
-        help='Pretty-print an RPC request/response',
-        parents=[k_cli_args.logging_args],
-    )
-    rpc_print_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.')
-    rpc_print_args.add_argument(
-        'input_file',
-        type=FileType('r'),
-        help='An input file containing the JSON RPC request or response with KoreJSON payload.',
-    )
-    rpc_print_args.add_argument('--output-file', type=FileType('w'))
-
-    rpc_kast_args = pyk_args_command.add_parser(
-        'rpc-kast',
-        help='Convert an "execute" JSON RPC response to a new "execute" or "simplify" request, copying parameters from a reference request.',
-        parents=[k_cli_args.logging_args],
-    )
-    rpc_kast_args.add_argument(
-        'reference_request_file',
-        type=FileType('r'),
-        help='An input file containing a JSON RPC request to server as a reference for the new request.',
-    )
-    rpc_kast_args.add_argument(
-        'response_file',
-        type=FileType('r'),
-        help='An input file containing a JSON RPC response with KoreJSON payload.',
-    )
-    rpc_kast_args.add_argument('--output-file', type=FileType('w'))
-
-    prove_legacy_args = pyk_args_command.add_parser(
-        'prove-legacy',
-        help='Prove an input specification (using kprovex).',
-        parents=[k_cli_args.logging_args],
-    )
-    prove_legacy_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.')
-    prove_legacy_args.add_argument('main_file', type=str, help='Main file used for kompilation.')
-    prove_legacy_args.add_argument('spec_file', type=str, help='File with the specification module.')
-    prove_legacy_args.add_argument('spec_module', type=str, help='Module with claims to be proven.')
-    prove_legacy_args.add_argument('--output-file', type=FileType('w'))
-    prove_legacy_args.add_argument('kArgs', nargs='*', help='Arguments to pass through to K invocation.')
-
-    kompile_args = pyk_args_command.add_parser(
-        'kompile',
-        help='Kompile the K specification.',
-        parents=[k_cli_args.logging_args, k_cli_args.warning_args, k_cli_args.definition_args, k_cli_args.kompile_args],
-    )
-    kompile_args.add_argument('main_file', type=str, help='File with the specification module.')
-
-    run_args = pyk_args_command.add_parser(
-        'run',
-        help='Run a given program using the K definition.',
-        parents=[k_cli_args.logging_args],
-    )
-    run_args.add_argument('pgm_file', type=str, help='File program to run in it.')
-    run_args.add_argument('--definition', type=dir_path, dest='definition_dir', help='Path to definition to use.')
-
-    prove_args = pyk_args_command.add_parser(
-        'prove',
-        help='Prove an input specification (using RPC based prover).',
-        parents=[k_cli_args.logging_args],
-    )
-    prove_args.add_argument('spec_file', type=file_path, help='File with the specification module.')
-    prove_args.add_argument('--definition', type=dir_path, dest='definition_dir', help='Path to definition to use.')
-    prove_args.add_argument('--spec-module', dest='spec_module', type=str, help='Module with claims to be proven.')
-    prove_args.add_argument(
-        '--type-inference-mode', type=TypeInferenceMode, help='Mode for doing K rule type inference in.'
-    )
-    prove_args.add_argument(
-        '--failure-info',
-        default=None,
-        action='store_true',
-        help='Print out more information about proof failures.',
-    )
-
-    graph_imports_args = pyk_args_command.add_parser(
-        'graph-imports',
-        help='Graph the imports of a given definition.',
-        parents=[k_cli_args.logging_args],
-    )
-    graph_imports_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.')
-
-    coverage_args = pyk_args_command.add_parser(
-        'coverage',
-        help='Convert coverage file to human readable log.',
-        parents=[k_cli_args.logging_args],
-    )
-    coverage_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.')
-    coverage_args.add_argument('coverage_file', type=FileType('r'), help='Coverage file to build log for.')
-    coverage_args.add_argument('-o', '--output', type=FileType('w'))
-
-    pyk_args_command.add_parser('kore-to-json', help='Convert textual KORE to JSON', parents=[k_cli_args.logging_args])
-
-    pyk_args_command.add_parser('json-to-kore', help='Convert JSON to textual KORE', parents=[k_cli_args.logging_args])
-
-    return pyk_args
-
-
 if __name__ == '__main__':
     main()

src/pyk/cli/args.py

@@ -25,6 +25,12 @@ def default() -> dict[str, Any]:
             'debug': False,
         }
 
+    @staticmethod
+    def from_option_string() -> dict[str, Any]:
+        return {
+            'v': 'verbose',
+        }
+
 
 class WarningOptions(Options):
     warnings: Warnings | None
@@ -37,6 +43,13 @@ def default() -> dict[str, Any]:
             'warning_to_error': False,
         }
 
+    @staticmethod
+    def from_option_string() -> dict[str, Any]:
+        return {
+            'w': 'warnings',
+            'w2e': 'warning_to_error',
+        }
+
 
 class OutputFileOptions(Options):
     output_file: IO[Any]
@@ -51,6 +64,13 @@ def default() -> dict[str, Any]:
 class DefinitionOptions(Options):
     definition_dir: Path
 
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {
+            'output-definition': 'definition_dir',
+            'definition': 'definition_dir',
+        }
+
 
 class DisplayOptions(Options):
     minimize: bool
@@ -79,6 +99,12 @@ def default() -> dict[str, Any]:
             'includes': [],
         }
 
+    @staticmethod
+    def from_option_string() -> dict[str, str]:
+        return {
+            'includes': 'includes',
+        }
+
 
 class SaveDirOptions(Options):
     save_directory: Path | None
@@ -102,6 +128,13 @@ def default() -> dict[str, Any]:
             'exclude_claim_labels': [],
         }
 
+    @staticmethod
+    def from_option_string() -> dict[str, str]:
+        return SaveDirOptions.from_option_string() | {
+            'claim': 'claim_labels',
+            'exclude-claim': 'exclude_claim_labels',
+        }
+
 
 class KompileOptions(Options):
     emit_json: bool
@@ -148,6 +181,18 @@ def default() -> dict[str, Any]:
             'no_exc_wrap': False,
         }
 
+    @staticmethod
+    def from_option_string() -> dict[str, str]:
+        return {
+            'with-llvm-library': 'llvm_library',
+            'read-only-kompiled-directory': 'read_only',
+            'ccopt': 'ccopts',
+            'O0': 'o0',
+            'O1': 'o1',
+            'O2': 'o2',
+            'O3': 'o3',
+        }
+
 
 class ParallelOptions(Options):
     workers: int
@@ -158,6 +203,12 @@ def default() -> dict[str, Any]:
             'workers': 1,
         }
 
+    @staticmethod
+    def from_option_string() -> dict[str, str]:
+        return {
+            'j': 'workers',
+        }
+
 
 class BugReportOptions(Options):
     bug_report: BugReport | None
@@ -181,6 +232,26 @@ def default() -> dict[str, Any]:
         }
 
 
+class ConfigArgs:
+    @cached_property
+    def config_args(self) -> ArgumentParser:
+        args = ArgumentParser(add_help=False)
+        args.add_argument(
+            '--config-file',
+            dest='config_file',
+            type=file_path,
+            default=Path('./pyk.toml'),
+            help='Path to Pyk config file.',
+        )
+        args.add_argument(
+            '--config-profile',
+            dest='config_profile',
+            default='default',
+            help='Config profile to be used.',
+        )
+        return args
+
+
 class KCLIArgs:
     @cached_property
     def logging_args(self) -> ArgumentParser:

src/pyk/cli/cli.py

@@ -16,3 +16,7 @@ def __init__(self, args: dict[str, Any]) -> None:
 
         for attr, val in _args.items():
             self.__setattr__(attr, val)
+
+    @staticmethod
+    def from_option_string() -> dict[str, str]:
+        return {}