Allows printing Kore JSON with pyk print (#568)

This small change extends the functionality of the `pyk` executable with
pretty-printing of Kore JSON files. This is useful for diffing up bug
reports submitted to the Haskell backend team.

---------

Co-authored-by: devops <[email protected]>

Author: geo2a

package/version

@@ -1 +1 @@
-0.1.393
+0.1.394

pyproject.toml

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

src/pyk/__main__.py

@@ -3,6 +3,7 @@
 import logging
 import sys
 from argparse import ArgumentParser, FileType
+from enum import Enum
 from pathlib import Path
 from typing import TYPE_CHECKING
 
@@ -31,6 +32,11 @@
 _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.
@@ -53,8 +59,13 @@ def main() -> None:
 def exec_print(args: Namespace) -> None:
     kompiled_dir: Path = args.definition_dir
     printer = KPrint(kompiled_dir)
-    _LOGGER.info(f'Reading Kast from file: {args.term.name}')
-    term = KInner.from_json(args.term.read())
+    if args.input == PrintInput.KORE_JSON:
+        _LOGGER.info(f'Reading Kore JSON from file: {args.term.name}')
+        kore = Pattern.from_json(args.term.read())
+        term = printer.kore_to_kast(kore)
+    else:
+        _LOGGER.info(f'Reading Kast JSON from file: {args.term.name}')
+        term = KInner.from_json(args.term.read())
     if is_top(term):
         args.output_file.write(printer.pretty_print(term))
         _LOGGER.info(f'Wrote file: {args.output_file.name}')
@@ -147,7 +158,8 @@ def create_argument_parser() -> ArgumentParser:
         help='Pretty print a term.',
         parents=[k_cli_args.logging_args, definition_args, k_cli_args.display_args],
     )
-    print_args.add_argument('term', type=FileType('r'), help='Input term (in JSON).')
+    print_args.add_argument('term', type=FileType('r'), help='Input term (in format specified with --input).')
+    print_args.add_argument('--input', default=PrintInput.KAST_JSON, type=PrintInput, choices=list(PrintInput))
     print_args.add_argument('--omit-labels', default='', nargs='?', help='List of labels to omit from output.')
     print_args.add_argument(
         '--keep-cells', default='', nargs='?', help='List of cells with primitive values to keep in output.'