Allow special characters in generated Lean 4 identifiers (#4729)

Closes #4722

Author: tothtamas28

pyk/src/pyk/k2lean4/__init__.py

@@ -0,0 +1 @@
+from .k2lean4 import K2Lean4

pyk/src/pyk/k2lean4/k2lean4.py

@@ -1,18 +1,27 @@
 from __future__ import annotations
 
+import re
 from dataclasses import dataclass
 from typing import TYPE_CHECKING
 
+from ..konvert import unmunge
 from ..kore.internal import CollectionKind
 from ..kore.syntax import SortApp
 from ..utils import check_type
 from .model import Abbrev, Ctor, ExplBinder, Inductive, Module, Signature, Term
 
 if TYPE_CHECKING:
+    from typing import Final
+
     from ..kore.internal import KoreDefn
     from .model import Command
 
 
+_VALID_LEAN_IDENT: Final = re.compile(
+    "_[a-zA-Z0-9_?!']+|[a-zA-Z][a-zA-Z0-9_?!']*"
+)  # Simplified to characters permitted in KORE in the first place
+
+
 @dataclass(frozen=True)
 class K2Lean4:
     defn: KoreDefn
@@ -46,10 +55,19 @@ def _symbol_ctor(self, sort: str, symbol: str) -> Ctor:
         param_sorts = (
             check_type(sort, SortApp).name for sort in self.defn.symbols[symbol].param_sorts
         )  # TODO eliminate check_type
+        symbol = self._symbol_ident(symbol)
         binders = tuple(ExplBinder((f'x{i}',), Term(sort)) for i, sort in enumerate(param_sorts))
-        symbol = symbol.replace('-', '_')
         return Ctor(symbol, Signature(binders, Term(sort)))
 
+    @staticmethod
+    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
+
     def _collections(self) -> list[Command]:
         return [self._collection(sort) for sort in sorted(self.defn.collections)]
 

pyk/src/pyk/k2lean4/model.py

@@ -73,7 +73,7 @@ def __init__(
     def __str__(self) -> str:
         modifiers = f'{self.modifiers} ' if self.modifiers else ''
         signature = f' {self.signature}' if self.signature else ''
-        return f'{modifiers} abbrev {self.ident}{signature} := {self.val}'
+        return f'{modifiers}abbrev {self.ident}{signature} := {self.val}'
 
 
 @final