Generate lake project (#4748)

* Make `cookiecutter` a runtime dependency
* Add logic for project generation
* Add integration test for project generatiion

.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-DVuyqwG11OY4uaaGwXTZOtyWefGye8l3yMSp3Cc7SeI=";
                 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"
@@ -91,3 +92,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/generate.py

@@ -0,0 +1,87 @@
+from __future__ import annotations
+
+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
+
+
+class GenContext(TypedDict):
+    package_name: str
+    library_name: str
+
+
+def generate(
+    definition_dir: str | Path,
+    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']),
+        '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 _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]]],
+) -> 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]
@@ -334,14 +344,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