Add klean command (#4749)

Enables generating a Lean 4 project from a K definition from the command
line.

---------

Co-authored-by: Juan C. <[email protected]>

flake.nix

@@ -84,7 +84,7 @@
 
             mk-k-framework = { haskell-backend-bins, llvm-kompile-libs }:
               prev.callPackage ./nix/k.nix {
-                mvnHash = "sha256-DVuyqwG11OY4uaaGwXTZOtyWefGye8l3yMSp3Cc7SeI=";
+                mvnHash = "sha256-cdSX3vKp5wXPz/qQbKoUBoDEyZ4f1yQ7+lc/yy6aJZk=";
                 manualMvnArtifacts = [
                   "org.scala-lang:scala-compiler:2.13.13"
                   "ant-contrib:ant-contrib:1.0b3"

pyk/pyproject.toml

@@ -55,6 +55,7 @@ pyk = "pyk.__main__:main"
 pyk-covr = "pyk.kcovr:main"
 kbuild = "pyk.kbuild.__main__:main"
 kdist = "pyk.kdist.__main__:main"
+klean = "pyk.klean.__main__:main"
 krepl = "pyk.krepl.__main__:main"
 kore-exec-covr = "pyk.kore_exec_covr.__main__:main"
 

pyk/src/pyk/klean/__main__.py

@@ -0,0 +1,109 @@
+from __future__ import annotations
+
+from argparse import ArgumentParser
+from pathlib import Path
+from typing import TYPE_CHECKING
+
+from pyk.cli.utils import dir_path
+from pyk.kore.internal import KoreDefn
+
+if TYPE_CHECKING:
+    from argparse import Namespace
+    from collections.abc import Iterable
+
+
+def main() -> None:
+    import logging
+    import sys
+
+    from pyk.cli.utils import LOG_FORMAT
+
+    args = sys.argv
+    level, args = _extract_log_level(args)
+    logging.basicConfig(level=level, format=LOG_FORMAT)
+
+    klean(args)
+
+
+def _extract_log_level(args: list[str]) -> tuple[int, list[str]]:
+    from pyk.cli.args import KCLIArgs
+    from pyk.cli.utils import loglevel
+
+    parser = KCLIArgs().logging_args
+    ns, rest = parser.parse_known_args(args)
+    level = loglevel(ns)
+    return level, rest
+
+
+def klean(args: Iterable[str]) -> None:
+    from .generate import generate
+
+    ns = _parse_args(args)
+    defn = _load_defn(ns.definition_dir)
+    if ns.rules:
+        defn = defn.filter_rewrites(ns.rules)
+    defn = defn.project_to_rewrites()
+    generate(
+        defn=defn,
+        output_dir=ns.output_dir,
+        context={
+            'package_name': ns.package_name,
+            'library_name': ns.library_name,
+        },
+    )
+
+
+def _parse_args(args: Iterable[str]) -> Namespace:
+    parser = _parser()
+    args = list(args)[1:]
+    ns = parser.parse_args(args)
+
+    if ns.library_name is None:
+        ns.library_name = ''.join(word.capitalize() for word in ns.package_name.split('-'))
+
+    if ns.output_dir is None:
+        ns.output_dir = Path()
+
+    return ns
+
+
+def _parser() -> ArgumentParser:
+    parser = ArgumentParser(description='Generate a Lean 4 project from a K definition')
+    parser.add_argument('definition_dir', metavar='DEFN_DIR', type=dir_path, help='definition directory')
+    parser.add_argument('package_name', metavar='PKG_NAME', help='name of the generated Lean 4 package (in kebab-case)')
+    parser.add_argument(
+        '-o',
+        '--output',
+        dest='output_dir',
+        metavar='DIR',
+        type=dir_path,
+        help='output directory (default: .)',
+    )
+    parser.add_argument(
+        '-l',
+        '--library',
+        dest='library_name',
+        metavar='NAME',
+        help='name of the generated Lean library (default: package name in PascalCase)',
+    )
+    parser.add_argument(
+        '-r',
+        '--rule',
+        dest='rules',
+        metavar='LABEL',
+        action='append',
+        help='labels of rules to include (default: all)',
+    )
+    return parser
+
+
+def _load_defn(definition_dir: Path) -> KoreDefn:
+    from ..kore.parser import KoreParser
+
+    kore_text = (definition_dir / 'definition.kore').read_text()
+    definition = KoreParser(kore_text).definition()
+    return KoreDefn.from_definition(definition)
+
+
+if __name__ == '__main__':
+    main()

pyk/src/pyk/klean/generate.py

@@ -3,29 +3,28 @@
 from pathlib import Path
 from typing import TYPE_CHECKING, TypedDict
 
-from ..kore.internal import KoreDefn
 from .k2lean4 import K2Lean4
 from .model import Module
 
 if TYPE_CHECKING:
     from collections.abc import Callable, Iterable
 
+    from ..kore.internal import KoreDefn
+
 
 class GenContext(TypedDict):
     package_name: str
     library_name: str
 
 
 def generate(
-    definition_dir: str | Path,
+    defn: KoreDefn,
     context: GenContext,
     *,
     output_dir: str | Path | None = None,
 ) -> Path:
-    definition_dir = Path(definition_dir)
     output_dir = Path(output_dir) if output_dir is not None else Path('.')
 
-    defn = _load_defn(definition_dir)
     k2lean4 = K2Lean4(defn)
     genmodel = {
         'Sorts': (k2lean4.sort_module, ['Prelude']),
@@ -55,17 +54,6 @@ def _gen_template(output_dir: Path, context: GenContext) -> Path:
     return res
 
 
-def _load_defn(definition_dir: Path) -> KoreDefn:
-    from ..kore.parser import KoreParser
-
-    kore_text = (definition_dir / 'definition.kore').read_text()
-    definition = KoreParser(kore_text).definition()
-
-    defn = KoreDefn.from_definition(definition)
-    defn = defn.project_to_rewrites()
-    return defn
-
-
 def _gen_modules(
     library_name: str,
     genmodel: dict[str, tuple[Callable[[], Module], list[str]]],

pyk/src/tests/integration/klean/test_generate.py

@@ -6,6 +6,8 @@
 import pytest
 
 from pyk import klean
+from pyk.kore.internal import KoreDefn
+from pyk.kore.parser import KoreParser
 from pyk.utils import run_process_2
 
 if TYPE_CHECKING:
@@ -15,10 +17,15 @@
 
 
 @pytest.fixture
-def imp_definition(kompile: Kompiler) -> Path:
+def imp_defn(kompile: Kompiler) -> KoreDefn:
     from ..utils import K_FILES
 
-    return kompile(main_file=K_FILES / 'imp.k')
+    definition_dir = kompile(main_file=K_FILES / 'imp.k')
+    kore_text = (definition_dir / 'definition.kore').read_text()
+    definition = KoreParser(kore_text).definition()
+    defn = KoreDefn.from_definition(definition)
+    defn = defn.project_to_rewrites()
+    return defn
 
 
 @pytest.fixture
@@ -31,11 +38,11 @@ def skip_if_no_lake() -> None:
 
 def test_generate(
     skip_if_no_lake: None,
-    imp_definition: Path,
+    imp_defn: KoreDefn,
     tmp_path: Path,
 ) -> None:
     project_dir = klean.generate(
-        definition_dir=imp_definition,
+        defn=imp_defn,
         output_dir=tmp_path,
         context={
             'package_name': 'klean-imp',