From 4a565cdd2eb13eb28e091702bf1f7f245b369cbe Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Thu, 9 Jan 2025 09:20:58 +0000 Subject: [PATCH 1/6] Extract cell type generation into a separate step --- pyk/src/pyk/k2lean4/k2lean4.py | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/k2lean4/k2lean4.py index 0b0f2583c5..c2d07a2787 100644 --- a/pyk/src/pyk/k2lean4/k2lean4.py +++ b/pyk/src/pyk/k2lean4/k2lean4.py @@ -29,13 +29,15 @@ class K2Lean4: def sort_module(self) -> Module: commands = [] commands += self._inductives() + commands += self._cells() commands += self._collections() return Module(commands=commands) def _inductives(self) -> list[Command]: def is_inductive(sort: str) -> bool: decl = self.defn.sorts[sort] - return not decl.hooked and 'hasDomainValues' not in decl.attrs_by_key + attrs = decl.attrs_by_key + return not decl.hooked and 'hasDomainValues' not in attrs and not decl.name.endswith('Cell') sorts = sorted(sort for sort in self.defn.sorts if is_inductive(sort)) return [self._inductive(sort) for sort in sorts] @@ -59,6 +61,14 @@ def _symbol_ctor(self, sort: str, symbol: str) -> Ctor: binders = tuple(ExplBinder((f'x{i}',), Term(sort)) for i, sort in enumerate(param_sorts)) return Ctor(symbol, Signature(binders, Term(sort))) + def _cells(self) -> list[Command]: + def is_cell(sort: str) -> bool: + decl = self.defn.sorts[sort] + return decl.name.endswith('Cell') + + sorts = sorted(sort for sort in self.defn.sorts if is_cell(sort)) + return [self._inductive(sort) for sort in sorts] + @staticmethod def _symbol_ident(symbol: str) -> str: if symbol.startswith('Lbl'): From 33702a7b2cc87606681c1d4ad98d40cb654748df Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Thu, 9 Jan 2025 10:05:34 +0000 Subject: [PATCH 2/6] Extract function `_param_sorts` --- pyk/src/pyk/k2lean4/k2lean4.py | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/k2lean4/k2lean4.py index c2d07a2787..03b22f33a3 100644 --- a/pyk/src/pyk/k2lean4/k2lean4.py +++ b/pyk/src/pyk/k2lean4/k2lean4.py @@ -7,13 +7,13 @@ 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 ..kore.syntax import SymbolDecl from .model import Command @@ -54,9 +54,8 @@ def _inj_ctor(self, sort: str, subsort: str) -> Ctor: return Ctor(f'inj_{subsort}', Signature((ExplBinder(('x',), Term(subsort)),), Term(sort))) 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 + decl = self.defn.symbols[symbol] + param_sorts = _param_sorts(decl) symbol = self._symbol_ident(symbol) binders = tuple(ExplBinder((f'x{i}',), Term(sort)) for i, sort in enumerate(param_sorts)) return Ctor(symbol, Signature(binders, Term(sort))) @@ -84,7 +83,7 @@ def _collections(self) -> list[Command]: def _collection(self, sort: str) -> Abbrev: coll = self.defn.collections[sort] elem = self.defn.symbols[coll.element] - sorts = ' '.join(check_type(sort, SortApp).name for sort in elem.param_sorts) # TODO eliminate check_type + sorts = ' '.join(_param_sorts(elem)) assert sorts match coll.kind: case CollectionKind.LIST: @@ -94,3 +93,9 @@ def _collection(self, sort: str) -> Abbrev: case CollectionKind.SET: val = Term(f'SetHook {sorts}') return Abbrev(sort, val, Signature((), Term('Type'))) + + +def _param_sorts(decl: SymbolDecl) -> list[str]: + from ..utils import check_type + + return [check_type(sort, SortApp).name for sort in decl.param_sorts] # TODO eliminate check_type From f9c162109d7f0a91712ad5860ba64fbde9a62657 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Thu, 9 Jan 2025 10:05:59 +0000 Subject: [PATCH 3/6] Sort cell type definitions topologically --- pyk/src/pyk/k2lean4/k2lean4.py | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/k2lean4/k2lean4.py index 03b22f33a3..0fc7d9df47 100644 --- a/pyk/src/pyk/k2lean4/k2lean4.py +++ b/pyk/src/pyk/k2lean4/k2lean4.py @@ -2,6 +2,7 @@ import re from dataclasses import dataclass +from graphlib import TopologicalSorter from typing import TYPE_CHECKING from ..konvert import unmunge @@ -65,7 +66,16 @@ def is_cell(sort: str) -> bool: decl = self.defn.sorts[sort] return decl.name.endswith('Cell') - sorts = sorted(sort for sort in self.defn.sorts if is_cell(sort)) + def ordering(sorts: list[str]) -> dict[str, list[str]]: + res: dict[str, list[str]] = {} + for sort in sorts: + (ctor,) = self.defn.constructors[sort] # Cells have exactly one constructor + decl = self.defn.symbols[ctor] + res[sort] = [sort for sort in _param_sorts(decl) if is_cell(sort)] + return res + + sorts = [sort for sort in self.defn.sorts if is_cell(sort)] + sorts = list(TopologicalSorter(ordering(sorts)).static_order()) return [self._inductive(sort) for sort in sorts] @staticmethod From 314d400e75d40b7ad35d9bd61c9a472ac05d6ab2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Thu, 9 Jan 2025 17:27:21 +0000 Subject: [PATCH 4/6] Add custom generator logic for cell sort If the cell is a leaf, an `inductive` with a single constructor `mk` is generated. Otherwise, a `structure` is generated. --- pyk/src/pyk/k2lean4/k2lean4.py | 41 +++++++++++---- pyk/src/pyk/k2lean4/model.py | 95 ++++++++++++++++++++++++++++++++++ 2 files changed, 126 insertions(+), 10 deletions(-) diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/k2lean4/k2lean4.py index 0fc7d9df47..df94fe0b2f 100644 --- a/pyk/src/pyk/k2lean4/k2lean4.py +++ b/pyk/src/pyk/k2lean4/k2lean4.py @@ -8,7 +8,7 @@ from ..konvert import unmunge from ..kore.internal import CollectionKind from ..kore.syntax import SortApp -from .model import Abbrev, Ctor, ExplBinder, Inductive, Module, Signature, Term +from .model import Abbrev, Ctor, ExplBinder, Inductive, Module, Signature, StructCtor, Structure, Term if TYPE_CHECKING: from typing import Final @@ -62,21 +62,42 @@ def _symbol_ctor(self, sort: str, symbol: str) -> Ctor: return Ctor(symbol, Signature(binders, Term(sort))) def _cells(self) -> list[Command]: - def is_cell(sort: str) -> bool: - decl = self.defn.sorts[sort] - return decl.name.endswith('Cell') - def ordering(sorts: list[str]) -> dict[str, list[str]]: res: dict[str, list[str]] = {} for sort in sorts: - (ctor,) = self.defn.constructors[sort] # Cells have exactly one constructor - decl = self.defn.symbols[ctor] - res[sort] = [sort for sort in _param_sorts(decl) if is_cell(sort)] + (cell_ctor,) = self.defn.constructors[sort] # Cells have exactly one constructor + decl = self.defn.symbols[cell_ctor] + res[sort] = [sort for sort in _param_sorts(decl) if self._is_cell(sort)] return res - sorts = [sort for sort in self.defn.sorts if is_cell(sort)] + sorts = [sort for sort in self.defn.sorts if self._is_cell(sort)] sorts = list(TopologicalSorter(ordering(sorts)).static_order()) - return [self._inductive(sort) for sort in sorts] + return [self._cell(sort) for sort in sorts] + + def _cell(self, sort: str) -> Inductive | Structure: + (cell_ctor,) = self.defn.constructors[sort] + decl = self.defn.symbols[cell_ctor] + param_sorts = _param_sorts(decl) + + if any(not self._is_cell(sort) for sort in param_sorts): + assert len(param_sorts) == 1 + (param_sort,) = param_sorts + ctor = Ctor('mk', Signature((ExplBinder(('val',), Term(param_sort)),), Term(sort))) + return Inductive(sort, Signature((), Term('Type')), ctors=(ctor,)) + + param_names = [] + for param_sort in param_sorts: + assert param_sort.startswith('Sort') + assert param_sort.endswith('Cell') + name = param_sort[4:-4] + name = name[0].lower() + name[1:] + param_names.append(name) + fields = tuple(ExplBinder((name,), Term(sort)) for name, sort in zip(param_names, param_sorts, strict=True)) + return Structure(sort, Signature((), Term('Type')), ctor=StructCtor(fields)) + + @staticmethod + def _is_cell(sort: str) -> bool: + return sort.endswith('Cell') @staticmethod def _symbol_ident(symbol: str) -> str: diff --git a/pyk/src/pyk/k2lean4/model.py b/pyk/src/pyk/k2lean4/model.py index fdbc630014..7a5c2af6c0 100644 --- a/pyk/src/pyk/k2lean4/model.py +++ b/pyk/src/pyk/k2lean4/model.py @@ -117,6 +117,101 @@ def __str__(self) -> str: return '\n'.join(lines) +@final +@dataclass(frozen=True) +class Structure(Declaration): + ident: DeclId + signature: Signature | None + extends: tuple[Term, ...] + ctor: StructCtor | None + deriving: tuple[str, ...] + modifiers: Modifiers | None + + def __init__( + self, + ident: str | DeclId, + signature: Signature | None = None, + extends: Iterable[Term] | None = None, + ctor: StructCtor | None = None, + deriving: Iterable[str] | None = None, + modifiers: Modifiers | None = None, + ): + ident = DeclId(ident) if isinstance(ident, str) else ident + extends = tuple(extends) if extends is not None else () + deriving = tuple(deriving) if deriving is not None else () + object.__setattr__(self, 'ident', ident) + object.__setattr__(self, 'signature', signature) + object.__setattr__(self, 'extends', extends) + object.__setattr__(self, 'ctor', ctor) + object.__setattr__(self, 'deriving', deriving) + object.__setattr__(self, 'modifiers', modifiers) + + def __str__(self) -> str: + lines = [] + + modifiers = f'{self.modifiers} ' if self.modifiers else '' + binders = ( + ' '.join(str(binder) for binder in self.signature.binders) + if self.signature and self.signature.binders + else '' + ) + binders = f' {binders}' if binders else '' + extends = ', '.join(str(extend) for extend in self.extends) + 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}') + + if self.deriving: + lines.append(f' deriving {self.deriving}') + + if self.ctor: + lines.extend(f' {line}' for line in str(self.ctor).splitlines()) + + return '\n'.join(lines) + + +@final +@dataclass(frozen=True) +class StructCtor: + fields: tuple[Binder, ...] # TODO implement StructField + ident: StructIdent | None + + def __init__( + self, + fields: Iterable[Binder], + ident: str | StructIdent | None = None, + ): + fields = tuple(fields) + ident = StructIdent(ident) if isinstance(ident, str) else ident + object.__setattr__(self, 'fields', fields) + object.__setattr__(self, 'ident', ident) + + def __str__(self) -> str: + lines = [] + if self.ident: + lines.append(f'{self.ident} ::') + for field in self.fields: + if isinstance(field, ExplBinder) and len(field.idents) == 1: + (ident,) = field.idents + ty = '' if field.ty is None else f' : {field.ty}' + lines.append(f'{ident}{ty}') + else: + lines.append(str(field)) + return '\n'.join(lines) + + +@final +@dataclass(frozen=True) +class StructIdent: + ident: str + modifiers: Modifiers | None = None + + def __str__(self) -> str: + modifiers = f'{self.modifiers} ' if self.modifiers else '' + return f'{modifiers}{ self.ident}' + + @final @dataclass(frozen=True) class DeclId: From 27023c5552e181cab19081408028ed0645a51078 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Fri, 10 Jan 2025 18:27:47 +0000 Subject: [PATCH 5/6] Generate a `structure` even for leaf cells --- pyk/src/pyk/k2lean4/k2lean4.py | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/k2lean4/k2lean4.py index df94fe0b2f..373aeb2d1d 100644 --- a/pyk/src/pyk/k2lean4/k2lean4.py +++ b/pyk/src/pyk/k2lean4/k2lean4.py @@ -74,24 +74,25 @@ def ordering(sorts: list[str]) -> dict[str, list[str]]: sorts = list(TopologicalSorter(ordering(sorts)).static_order()) return [self._cell(sort) for sort in sorts] - def _cell(self, sort: str) -> Inductive | Structure: + def _cell(self, sort: str) -> Structure: (cell_ctor,) = self.defn.constructors[sort] decl = self.defn.symbols[cell_ctor] param_sorts = _param_sorts(decl) - if any(not self._is_cell(sort) for sort in param_sorts): + param_names: list[str] + + if all(self._is_cell(sort) for sort in param_sorts): + param_names = [] + for param_sort in param_sorts: + assert param_sort.startswith('Sort') + assert param_sort.endswith('Cell') + name = param_sort[4:-4] + name = name[0].lower() + name[1:] + param_names.append(name) + else: assert len(param_sorts) == 1 - (param_sort,) = param_sorts - ctor = Ctor('mk', Signature((ExplBinder(('val',), Term(param_sort)),), Term(sort))) - return Inductive(sort, Signature((), Term('Type')), ctors=(ctor,)) - - param_names = [] - for param_sort in param_sorts: - assert param_sort.startswith('Sort') - assert param_sort.endswith('Cell') - name = param_sort[4:-4] - name = name[0].lower() + name[1:] - param_names.append(name) + param_names = ['val'] + fields = tuple(ExplBinder((name,), Term(sort)) for name, sort in zip(param_names, param_sorts, strict=True)) return Structure(sort, Signature((), Term('Type')), ctor=StructCtor(fields)) From 147e15d4828d2c39ea4f86cae65b0c4cdd13fba0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Mon, 13 Jan 2025 09:45:38 +0000 Subject: [PATCH 6/6] Revert "Generate a `structure` even for leaf cells" This reverts commit 27023c5552e181cab19081408028ed0645a51078. --- pyk/src/pyk/k2lean4/k2lean4.py | 27 +++++++++++++-------------- 1 file changed, 13 insertions(+), 14 deletions(-) diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/k2lean4/k2lean4.py index 373aeb2d1d..df94fe0b2f 100644 --- a/pyk/src/pyk/k2lean4/k2lean4.py +++ b/pyk/src/pyk/k2lean4/k2lean4.py @@ -74,25 +74,24 @@ def ordering(sorts: list[str]) -> dict[str, list[str]]: sorts = list(TopologicalSorter(ordering(sorts)).static_order()) return [self._cell(sort) for sort in sorts] - def _cell(self, sort: str) -> Structure: + def _cell(self, sort: str) -> Inductive | Structure: (cell_ctor,) = self.defn.constructors[sort] decl = self.defn.symbols[cell_ctor] param_sorts = _param_sorts(decl) - param_names: list[str] - - if all(self._is_cell(sort) for sort in param_sorts): - param_names = [] - for param_sort in param_sorts: - assert param_sort.startswith('Sort') - assert param_sort.endswith('Cell') - name = param_sort[4:-4] - name = name[0].lower() + name[1:] - param_names.append(name) - else: + if any(not self._is_cell(sort) for sort in param_sorts): assert len(param_sorts) == 1 - param_names = ['val'] - + (param_sort,) = param_sorts + ctor = Ctor('mk', Signature((ExplBinder(('val',), Term(param_sort)),), Term(sort))) + return Inductive(sort, Signature((), Term('Type')), ctors=(ctor,)) + + param_names = [] + for param_sort in param_sorts: + assert param_sort.startswith('Sort') + assert param_sort.endswith('Cell') + name = param_sort[4:-4] + name = name[0].lower() + name[1:] + param_names.append(name) fields = tuple(ExplBinder((name,), Term(sort)) for name, sort in zip(param_names, param_sorts, strict=True)) return Structure(sort, Signature((), Term('Type')), ctor=StructCtor(fields))