From c0098ad3da1c1fd84f4cc3c9155a4a820aeb1ba2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Wed, 8 Jan 2025 14:57:36 +0000 Subject: [PATCH] Re-implement `_symbol_ident` --- pyk/src/pyk/k2lean4/k2lean4.py | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/k2lean4/k2lean4.py index ef04c457c0..0b0f2583c5 100644 --- a/pyk/src/pyk/k2lean4/k2lean4.py +++ b/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 @@ -52,7 +61,12 @@ def _symbol_ctor(self, sort: str, symbol: str) -> Ctor: @staticmethod def _symbol_ident(symbol: str) -> str: - return symbol.replace('-', '_') + 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)]