Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Avoid clashes of generated declarations and Lean 4 #4742

Open
wants to merge 3 commits into
base: develop
Choose a base branch
from
Open

Avoid clashes of generated declarations and Lean 4 #4742

Changes from 2 commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
ae2e02b
Mask names of generated definitions
JuanCoRo Jan 21, 2025
6c969da
Small improvements
JuanCoRo Jan 21, 2025
9074215
cleanup
JuanCoRo Jan 21, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 22 additions & 5 deletions pyk/src/pyk/k2lean4/model.py
View file
Open in desktop
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should be handled in the generator, and maybe checked in the model.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'll leave this as a future item if/when work on this PR resumes.

Original file line number Diff line number Diff line change
Expand Up @@ -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 declaration
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

end and where are keywords, ite is probably just a predefined function.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I changed it to _LEAN_WORDS. Let me know if this notation is not desired, or if we should separate into two sets depending on keyword or definition.



def indent(text: str, n: int) -> str:
Expand All @@ -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 and is not '' else f'{name}Mask'


@final
@dataclass(frozen=True)
class Module:
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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:
Expand Down Expand Up @@ -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}'
Expand Down Expand Up @@ -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
Expand All @@ -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}')
Expand Down
Loading