From ae2e02bde25f882ee3634ab12a789bd800e14094 Mon Sep 17 00:00:00 2001 From: Juan Conejero Date: Tue, 21 Jan 2025 17:05:01 +0100 Subject: [PATCH 1/3] Mask names of generated definitions --- pyk/src/pyk/k2lean4/model.py | 27 ++++++++++++++++++++++----- 1 file changed, 22 insertions(+), 5 deletions(-) diff --git a/pyk/src/pyk/k2lean4/model.py b/pyk/src/pyk/k2lean4/model.py index c53e4c2a531..d8b8ce2fcf2 100644 --- a/pyk/src/pyk/k2lean4/model.py +++ b/pyk/src/pyk/k2lean4/model.py @@ -7,6 +7,9 @@ if TYPE_CHECKING: from collections.abc import Iterable + from typing import Final + +_LEAN_KEYWORDS: Final = {'ite', 'end', 'where'} # Words that cannot be a the name of a definition def indent(text: str, n: int) -> str: @@ -17,6 +20,16 @@ def indent(text: str, n: int) -> str: return '\n'.join(res) +def mask_name(name: str, mask: str | None) -> str: + """Append `mask` to `name` if `name` is in `_LEAN_KEYWORDS`.""" + if name == '': + return '' + elif name not in _LEAN_KEYWORDS: + return name + else: + return f'{name}{mask}' if mask is not None else f'{name}Mask' + + @final @dataclass(frozen=True) class Module: @@ -64,7 +77,8 @@ def __init__(self, ident: str | DeclId, signature: Signature, modifiers: Modifie def __str__(self) -> str: modifiers = f'{self.modifiers} ' if self.modifiers else '' - return f'{modifiers}axiom {self.ident} {self.signature}' + ident = mask_name(f'{self.ident}', 'Ax') + return f'{modifiers}axiom {ident} {self.signature}' @final @@ -90,8 +104,9 @@ def __init__( def __str__(self) -> str: modifiers = f'{self.modifiers} ' if self.modifiers else '' + ident = mask_name(f'{self.ident}', 'Abbr') signature = f' {self.signature}' if self.signature else '' - return f'{modifiers}abbrev {self.ident}{signature} := {self.val}' + return f'{modifiers}abbrev {ident}{signature} := {self.val}' @final @@ -122,12 +137,13 @@ def __init__( def __str__(self) -> str: modifiers = f'{self.modifiers} ' if self.modifiers else '' + ident = mask_name(f'{self.ident}', 'Ind') signature = f' {self.signature}' if self.signature else '' where = ' where' if self.ctors else '' deriving = ', '.join(self.deriving) lines = [] - lines.append(f'{modifiers}inductive {self.ident}{signature}{where}') + lines.append(f'{modifiers}inductive {ident}{signature}{where}') for ctor in self.ctors: lines.append(f' | {ctor}') if deriving: @@ -171,7 +187,7 @@ def __str__(self) -> str: modifiers = f'{self.modifiers} ' if self.modifiers else '' attr_kind = f'{self.attr_kind.value} ' if self.attr_kind else '' priority = f' (priority := {self.priority})' if self.priority is not None else '' - ident = f' {self.ident}' if self.ident else '' + ident = f' {mask_name(str(self.ident), "Inst")}' if self.ident else '' signature = f' {self.signature}' if self.signature else '' decl = f'{modifiers}{attr_kind}instance{priority}{ident}{signature}' @@ -311,6 +327,7 @@ def __str__(self) -> str: lines = [] modifiers = f'{self.modifiers} ' if self.modifiers else '' + ident = mask_name(str(self.ident), 'Struct') binders = ( ' '.join(str(binder) for binder in self.signature.binders) if self.signature and self.signature.binders @@ -321,7 +338,7 @@ def __str__(self) -> str: extends = f' extends {extends}' if extends else '' ty = f' : {self.signature.ty}' if self.signature and self.signature.ty else '' where = ' where' if self.ctor else '' - lines.append(f'{modifiers}structure {self.ident}{binders}{extends}{ty}{where}') + lines.append(f'{modifiers}structure {ident}{binders}{extends}{ty}{where}') if self.deriving: lines.append(f' deriving {self.deriving}') From 6c969da2177b94b7fcadfc0d3ff071c6b4aca97a Mon Sep 17 00:00:00 2001 From: Juan Conejero Date: Tue, 21 Jan 2025 17:43:32 +0100 Subject: [PATCH 2/3] Small improvements --- pyk/src/pyk/k2lean4/model.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/k2lean4/model.py b/pyk/src/pyk/k2lean4/model.py index d8b8ce2fcf2..dcff434b927 100644 --- a/pyk/src/pyk/k2lean4/model.py +++ b/pyk/src/pyk/k2lean4/model.py @@ -9,7 +9,7 @@ from collections.abc import Iterable from typing import Final -_LEAN_KEYWORDS: Final = {'ite', 'end', 'where'} # Words that cannot be a the name of a definition +_LEAN_KEYWORDS: Final = {'ite', 'end', 'where'} # Words that cannot be a the name of a declaration def indent(text: str, n: int) -> str: @@ -27,7 +27,7 @@ def mask_name(name: str, mask: str | None) -> str: elif name not in _LEAN_KEYWORDS: return name else: - return f'{name}{mask}' if mask is not None else f'{name}Mask' + return f'{name}{mask}' if mask is not None and is not '' else f'{name}Mask' @final From 9074215af675a10f241f88ab47dc81ced16669bb Mon Sep 17 00:00:00 2001 From: Juan Conejero Date: Tue, 21 Jan 2025 19:28:10 +0100 Subject: [PATCH 3/3] cleanup --- pyk/src/pyk/k2lean4/model.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/k2lean4/model.py b/pyk/src/pyk/k2lean4/model.py index dcff434b927..704e05315ff 100644 --- a/pyk/src/pyk/k2lean4/model.py +++ b/pyk/src/pyk/k2lean4/model.py @@ -9,7 +9,7 @@ from collections.abc import Iterable from typing import Final -_LEAN_KEYWORDS: Final = {'ite', 'end', 'where'} # Words that cannot be a the name of a declaration +_LEAN_WORDS: Final = {'ite', 'end', 'where'} # Words that cannot be a the name of a declaration def indent(text: str, n: int) -> str: @@ -24,10 +24,10 @@ def mask_name(name: str, mask: str | None) -> str: """Append `mask` to `name` if `name` is in `_LEAN_KEYWORDS`.""" if name == '': return '' - elif name not in _LEAN_KEYWORDS: + elif name not in _LEAN_WORDS: return name else: - return f'{name}{mask}' if mask is not None and is not '' else f'{name}Mask' + return f'{name}{mask}' if mask is not None and mask != '' else f'{name}Mask' @final