Merge branch 'develop' into _update-deps/runtimeverification/haskell-…

…backend

.github/actions/with-k-docker/Dockerfile

@@ -31,7 +31,7 @@ RUN rm /kframework.deb
 
 ARG USER_ID=9876
 ARG GROUP_ID=9876
-RUN    groupadd -g ${GROUP_ID} user                     \
+RUN    groupadd -g ${GROUP_ID} user \
     && useradd -m -u ${USER_ID} -s /bin/sh -g user user
 
 USER user
@@ -40,3 +40,8 @@ WORKDIR /home/user
 ENV PATH=/home/user/.local/bin:${PATH}
 RUN    curl -sSL https://install.python-poetry.org | python3 - --version 1.8.5 \
     && poetry --version
+
+ENV PATH=/home/user/.elan/bin:${PATH}
+RUN    curl -O https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+    && sh elan-init.sh -y \
+    && rm elan-init.sh

flake.nix

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

nix/pyk-overlay.nix

@@ -12,10 +12,10 @@
         checkGroups = [ ];
         overrides = p2n.defaultPoetryOverrides.extend
           (self: super: {
-            pygments = super.pygments.overridePythonAttrs
+            urllib3 = super.urllib3.overridePythonAttrs
             (
               old: {
-                buildInputs = (old.buildInputs or [ ]) ++ [ super.hatchling ];
+                buildInputs = (old.buildInputs or [ ]) ++ [ super.hatch-vcs ];
               }
             );
           });

pyk/pyproject.toml

@@ -19,6 +19,7 @@ from = "src"
 python = "^3.10"
 cmd2 = "^2.4.2"
 coloredlogs = "^15.0.1"
+cookiecutter = "^2.6.0"
 filelock = "^3.9.0"
 graphviz = "^0.20.1"
 hypothesis = "^6.103.1"
@@ -54,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"
 
@@ -91,3 +93,7 @@ ignore_missing_imports = true
 [[tool.mypy.overrides]]
 module = "coloredlogs"
 ignore_missing_imports = true
+
+[[tool.mypy.overrides]]
+module = "cookiecutter.*"
+ignore_missing_imports = true

pyk/src/pyk/klean/__init__.py

@@ -0,0 +1 @@
+from .generate import GenContext, generate

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

@@ -0,0 +1,75 @@
+from __future__ import annotations
+
+from pathlib import Path
+from typing import TYPE_CHECKING, TypedDict
+
+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(
+    defn: KoreDefn,
+    context: GenContext,
+    *,
+    output_dir: str | Path | None = None,
+) -> Path:
+    output_dir = Path(output_dir) if output_dir is not None else Path('.')
+
+    k2lean4 = K2Lean4(defn)
+    genmodel = {
+        'Sorts': (k2lean4.sort_module, ['Prelude']),
+        'Func': (k2lean4.func_module, ['Sorts']),
+        'Inj': (k2lean4.inj_module, ['Sorts']),
+        'Rewrite': (k2lean4.rewrite_module, ['Func', 'Inj']),
+    }
+
+    modules = _gen_modules(context['library_name'], genmodel)
+    res = _gen_template(output_dir, context)
+    _write_modules(res, modules)
+    return res
+
+
+def _gen_template(output_dir: Path, context: GenContext) -> Path:
+    from cookiecutter.generate import generate_files
+
+    template_dir = Path(__file__).parent / 'template'
+    gen_res = generate_files(
+        repo_dir=str(template_dir),
+        output_dir=str(output_dir),
+        context={'cookiecutter': context},
+    )
+
+    res = Path(gen_res)
+    assert res.is_dir()
+    return res
+
+
+def _gen_modules(
+    library_name: str,
+    genmodel: dict[str, tuple[Callable[[], Module], list[str]]],
+) -> dict[Path, Module]:
+    def gen_module(generator: Callable[[], Module], imports: Iterable[str]) -> Module:
+        imports = tuple(f'{library_name}.{importt}' for importt in imports)
+        module = generator()
+        module = Module(imports=imports, commands=module.commands)
+        return module
+
+    return {
+        Path(library_name) / f'{name}.lean': gen_module(generator, imports)
+        for name, (generator, imports) in genmodel.items()
+    }
+
+
+def _write_modules(output_dir: Path, modules: dict[Path, Module]) -> None:
+    for path, module in modules.items():
+        (output_dir / path).write_text(str(module))

pyk/src/pyk/k2lean4/k2lean4.py → pyk/src/pyk/klean/k2lean4.py

@@ -200,10 +200,20 @@ def _symbol_ctor(self, sort: str, symbol: str) -> Ctor:
     def _symbol_ident(symbol: str) -> str:
         if symbol.startswith('Lbl'):
             symbol = symbol[3:]
-        symbol = unmunge(symbol)
-        if not _VALID_LEAN_IDENT.fullmatch(symbol):
-            symbol = f'«{symbol}»'
-        return symbol
+        return K2Lean4._escape_ident(symbol, kore=True)
+
+    @staticmethod
+    def _var_ident(var: str) -> str:
+        assert var.startswith('Var')
+        return K2Lean4._escape_ident(var[3:], kore=True)
+
+    @staticmethod
+    def _escape_ident(ident: str, *, kore: bool = False) -> str:
+        if kore:
+            ident = unmunge(ident)
+        if not _VALID_LEAN_IDENT.fullmatch(ident):
+            ident = f'«{ident}»'
+        return ident
 
     def _structure(self, sort: str) -> Structure:
         fields = self.structures[sort]
@@ -316,7 +326,9 @@ def _rewrite_ctor(self, rule: RewriteRule) -> Ctor:
 
         # Step 3: create binders
         binders: list[Binder] = []
-        binders.extend(self._free_binders(pattern))  # Binders of the form {x y : SortInt}
+        binders.extend(
+            self._free_binders(And(SortApp('Foo'), (pattern,) + tuple(defs.values())))
+        )  # Binders of the form {x y : SortInt}
         binders.extend(self._def_binders(defs))  # Binders of the form (def_y : foo x = some y)
 
         # Step 4: transform patterns
@@ -334,14 +346,10 @@ def _rewrite_ctor(self, rule: RewriteRule) -> Ctor:
     @staticmethod
     def _rewrite_name(rule: RewriteRule) -> str:
         if rule.label:
-            return rule.label.replace('-', '_').replace('.', '_')
+            label = rule.label.replace('-', '_').replace('.', '_')
+            return K2Lean4._escape_ident(label)
         return f'_{rule.uid[:7]}'
 
-    @staticmethod
-    def _var_ident(name: str) -> str:
-        assert name.startswith('Var')
-        return K2Lean4._symbol_ident(name[3:])
-
     def _elim_fun_apps(self, pattern: Pattern, free: Iterator[str]) -> tuple[Pattern, dict[str, Pattern]]:
         """Replace ``foo(bar(x))`` with ``z`` and return mapping ``{y: bar(x), z: foo(y)}`` with ``y``, ``z`` fresh variables."""
         defs: dict[str, Pattern] = {}

pyk/src/pyk/k2lean4/model.py → pyk/src/pyk/klean/model.py

@@ -20,14 +20,23 @@ def indent(text: str, n: int) -> str:
 @final
 @dataclass(frozen=True)
 class Module:
+    imports: tuple[str, ...]
     commands: tuple[Command, ...]
 
-    def __init__(self, commands: Iterable[Command] | None = None):
+    def __init__(
+        self,
+        imports: Iterable[str] | None = None,
+        commands: Iterable[Command] | None = None,
+    ):
+        imports = tuple(imports) if imports is not None else ()
         commands = tuple(commands) if commands is not None else ()
+        object.__setattr__(self, 'imports', imports)
         object.__setattr__(self, 'commands', commands)
 
     def __str__(self) -> str:
-        return '\n\n'.join(str(command) for command in self.commands)
+        imports = '\n'.join(f'import {importt}' for importt in self.imports)
+        commands = '\n\n'.join(str(command) for command in self.commands)
+        return '\n\n'.join(section for section in [imports, commands] if section)
 
 
 class Command(ABC): ...

pyk/src/pyk/klean/template/cookiecutter.json

@@ -0,0 +1,4 @@
+{
+    "package_name": null,
+    "library_name": null
+}

pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/.gitignore

@@ -0,0 +1 @@
+/.lake

pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/lakefile.toml

@@ -0,0 +1,9 @@
+name = "{{ cookiecutter.package_name }}"
+version = "0.1.0"
+defaultTargets = ["{{ cookiecutter.library_name }}"]
+weakLeanArgs = [
+    "-D maxHeartbeats=10000000"
+]
+
+[[lean_lib]]
+name = "{{ cookiecutter.library_name }}"

pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/lean-toolchain

@@ -0,0 +1 @@
+stable

pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/{{ cookiecutter.library_name }}.lean

@@ -0,0 +1 @@
+import {{ cookiecutter.library_name }}.Rewrite