From ad9cefdff2c2271eaf4fae4254195c0d0e789003 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Tue, 17 Dec 2024 09:45:54 +0000 Subject: [PATCH 1/6] Add approximate abstract syntax for Lean 4 inductive types --- pyk/src/pyk/k2lean4/__init__.py | 0 pyk/src/pyk/k2lean4/model.py | 306 ++++++++++++++++++++++++++++++++ 2 files changed, 306 insertions(+) create mode 100644 pyk/src/pyk/k2lean4/__init__.py create mode 100644 pyk/src/pyk/k2lean4/model.py diff --git a/pyk/src/pyk/k2lean4/__init__.py b/pyk/src/pyk/k2lean4/__init__.py new file mode 100644 index 00000000000..e69de29bb2d diff --git a/pyk/src/pyk/k2lean4/model.py b/pyk/src/pyk/k2lean4/model.py new file mode 100644 index 00000000000..f716a48c362 --- /dev/null +++ b/pyk/src/pyk/k2lean4/model.py @@ -0,0 +1,306 @@ +from __future__ import annotations + +from abc import ABC +from dataclasses import dataclass +from enum import Enum +from typing import TYPE_CHECKING, final + +if TYPE_CHECKING: + from collections.abc import Iterable + + +def indent(text: str, n: int) -> str: + indent = n * ' ' + res = [] + for line in text.splitlines(): + res.append(f'{indent}{line}' if line else '') + return '\n'.join(res) + + +@final +@dataclass(frozen=True) +class Module: + commands: tuple[Command, ...] + + def __init__(self, commands: Iterable[Command] | None = None): + commands = tuple(commands) if commands is not None else () + object.__setattr__(self, 'commands', commands) + + def __str__(self) -> str: + return '\n\n'.join(str(command) for command in self.commands) + + +class Command(ABC): ... + + +class Mutual(Command): + commands: tuple[Command, ...] + + def __init__(self, commands: Iterable[Command] | None = None): + commands = tuple(commands) if commands is not None else () + object.__setattr__(self, 'commands', commands) + + def __str__(self) -> str: + commands = '\n\n'.join(indent(str(command), 2) for command in self.commands) + return f'mutual\n{commands}\nend' + + +class Declaration(Command, ABC): + modifiers: Modifiers | None + + +@final +@dataclass +class Abbrev(Declaration): + ident: DeclId + val: Term # declVal + signature: Signature | None + modifiers: Modifiers | None + + def __init__( + self, + ident: str | DeclId, + val: Term, + signature: Signature | None = None, + modifiers: Modifiers | None = None, + ): + ident = DeclId(ident) if isinstance(ident, str) else ident + object.__setattr__(self, 'ident', ident) + object.__setattr__(self, 'val', val) + object.__setattr__(self, 'signature', signature) + object.__setattr__(self, 'modifiers', modifiers) + + 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}' + + +@final +@dataclass(frozen=True) +class Inductive(Declaration): + ident: DeclId + signature: Signature | None + ctors: tuple[Ctor, ...] + deriving: tuple[str, ...] + modifiers: Modifiers | None + + def __init__( + self, + ident: str | DeclId, + signature: Signature | None = None, + ctors: Iterable[Ctor] | None = None, + deriving: Iterable[str] | None = None, + modifiers: Modifiers | None = None, + ): + ident = DeclId(ident) if isinstance(ident, str) else ident + ctors = tuple(ctors) if ctors 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, 'ctors', ctors) + object.__setattr__(self, 'deriving', deriving) + object.__setattr__(self, 'modifiers', modifiers) + + def __str__(self) -> str: + modifiers = f'{self.modifiers} ' if self.modifiers else '' + 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}') + for ctor in self.ctors: + lines.append(f' | {ctor}') + if deriving: + lines.append(f' deriving {deriving}') + return '\n'.join(lines) + + +@final +@dataclass(frozen=True) +class DeclId: + val: str + uvars: tuple[str, ...] + + def __init__(self, val: str, uvars: Iterable[str] | None = None): + uvars = tuple(uvars) if uvars is not None else () + object.__setattr__(self, 'val', val) + object.__setattr__(self, 'uvars', uvars) + + def __str__(self) -> str: + uvars = ', '.join(self.uvars) + uvars = '.{' + uvars + '}' if uvars else '' + return f'{self.val}{uvars}' + + +@final +@dataclass(frozen=True) +class Ctor: + ident: str + signature: Signature | None = None + modifiers: Modifiers | None = None + + def __str__(self) -> str: + modifiers = f'{self.modifiers} ' if self.modifiers else '' + signature = f' {self.signature}' if self.signature else '' + return f'{modifiers}{self.ident}{signature}' + + +@final +@dataclass(frozen=True) +class Signature: + binders: tuple[Binder, ...] + ty: Term | None + + def __init__(self, binders: Iterable[Binder] | None = None, ty: Term | None = None): + binders = tuple(binders) if binders is not None else () + object.__setattr__(self, 'binders', binders) + object.__setattr__(self, 'ty', ty) + + def __str__(self) -> str: + binders = ' '.join(str(binder) for binder in self.binders) + sep = ' ' if self.binders else '' + ty = f'{sep}: {self.ty}' if self.ty else '' + return f'{binders}{ty}' + + +class Binder(ABC): ... + + +class BracketBinder(Binder, ABC): ... + + +@final +@dataclass(frozen=True) +class ExplBinder(BracketBinder): + idents: tuple[str, ...] + ty: Term | None + + def __init__(self, idents: Iterable[str], ty: Term | None = None): + object.__setattr__(self, 'idents', tuple(idents)) + object.__setattr__(self, 'ty', ty) + + def __str__(self) -> str: + idents = ' '.join(self.idents) + ty = '' if self.ty is None else f' : {self.ty}' + return f'({idents}{ty})' + + +@final +@dataclass(frozen=True) +class ImplBinder(BracketBinder): + idents: tuple[str, ...] + ty: Term | None + strict: bool + + def __init__(self, idents: Iterable[str], ty: Term | None = None, *, strict: bool | None = None): + object.__setattr__(self, 'idents', tuple(idents)) + object.__setattr__(self, 'ty', ty) + object.__setattr__(self, 'strict', bool(strict)) + + def __str__(self) -> str: + ldelim, rdelim = ['⦃', '⦄'] if self.strict else ['{', '}'] + idents = ' '.join(self.idents) + ty = '' if self.ty is None else f' : {self.ty}' + return f'{ldelim}{idents}{ty}{rdelim}' + + +@final +@dataclass(frozen=True) +class InstBinder(BracketBinder): + ty: Term + ident: str | None + + def __init__(self, ty: Term, ident: str | None = None): + object.__setattr__(self, 'ty', ty) + object.__setattr__(self, 'ident', ident) + + def __str__(self) -> str: + ident = f'{self.ident} : ' if self.ident else '' + return f'[{ident}{self.ty}]' + + +@final +@dataclass(frozen=True) +class Term: + term: str # TODO: refine + + def __str__(self) -> str: + return self.term + + +@final +@dataclass(frozen=True) +class Modifiers: + attrs: tuple[Attr, ...] + visibility: Visibility | None + noncomputable: bool + unsafe: bool + totality: Totality | None + + def __init__( + self, + *, + attrs: Iterable[str | Attr] | None = None, + visibility: str | Visibility | None = None, + noncomputable: bool | None = None, + unsafe: bool | None = None, + totality: str | Totality | None = None, + ): + attrs = tuple(Attr(attr) if isinstance(attr, str) else attr for attr in attrs) if attrs is not None else () + visibility = Visibility(visibility) if isinstance(visibility, str) else visibility + noncomputable = bool(noncomputable) + unsafe = bool(unsafe) + totality = Totality(totality) if isinstance(totality, str) else totality + object.__setattr__(self, 'attrs', attrs) + object.__setattr__(self, 'visibility', visibility) + object.__setattr__(self, 'noncomputable', noncomputable) + object.__setattr__(self, 'unsafe', unsafe) + object.__setattr__(self, 'totality', totality) + + def __str__(self) -> str: + chunks = [] + if self.attrs: + attrs = ', '.join(str(attr) for attr in self.attrs) + chunks.append(f'@[{attrs}]') + if self.visibility: + chunks.append(self.visibility.value) + if self.noncomputable: + chunks.append('noncomputable') + if self.unsafe: + chunks.append('unsafe') + if self.totality: + chunks.append(self.totality.value) + return ' '.join(chunks) + + +@final +@dataclass(frozen=True) +class Attr: + attr: str + kind: AttrKind | None + + def __init__(self, attr: str, kind: AttrKind | None = None): + object.__setattr__(self, 'attr', attr) + object.__setattr__(self, 'kind', kind) + + def __str__(self) -> str: + if self.kind: + return f'{self.kind.value} {self.attr}' + return self.attr + + +class AttrKind(Enum): + SCOPED = 'scoped' + LOCAL = 'local' + + +class Visibility(Enum): + PRIVATE = 'private' + PROTECTED = 'protected' + + +class Totality(Enum): + PARTIAL = 'partial' + NONREC = 'nonrec' From aeb1e574e6205d8e4b08c06d4dd62b549a942356 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Tue, 17 Dec 2024 15:58:42 +0000 Subject: [PATCH 2/6] Generate inductive types --- pyk/src/pyk/k2lean4/k2lean4.py | 47 ++++++++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) create mode 100644 pyk/src/pyk/k2lean4/k2lean4.py diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/k2lean4/k2lean4.py new file mode 100644 index 00000000000..e232238d211 --- /dev/null +++ b/pyk/src/pyk/k2lean4/k2lean4.py @@ -0,0 +1,47 @@ +from __future__ import annotations + +from dataclasses import dataclass +from typing import TYPE_CHECKING + +from ..kore.syntax import SortApp +from ..utils import check_type +from .model import Ctor, ExplBinder, Inductive, Module, Signature, Term + +if TYPE_CHECKING: + from ..kore.internal import KoreDefn + from .model import Command + + +@dataclass(frozen=True) +class K2Lean4: + defn: KoreDefn + + def sort_module(self) -> Module: + commands = [] + commands += self._inductives() + return Module(commands=self._inductives()) + + 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 + + sorts = sorted(sort for sort in self.defn.sorts if is_inductive(sort)) + return [self._inductive(sort) for sort in sorts] + + def _inductive(self, sort: str) -> Inductive: + subsorts = sorted(self.defn.subsorts.get(sort, ())) + symbols = sorted(self.defn.ctor_symbols.get(sort, ())) + ctors: list[Ctor] = [] + ctors.extend(self._inj_ctor(sort, subsort) for subsort in subsorts) + ctors.extend(self._symbol_ctor(sort, symbol) for symbol in symbols) + return Inductive(sort, Signature((), Term('Type')), ctors=ctors) + + 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) + 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))) From c9575417893d2d062efefed3331c939a16e775d7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Fri, 20 Dec 2024 12:26:49 +0000 Subject: [PATCH 3/6] Rename property `ctor_symbols` to `constructors` --- pyk/src/pyk/k2lean4/k2lean4.py | 2 +- pyk/src/pyk/kore/internal.py | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/k2lean4/k2lean4.py index e232238d211..d4b86146da8 100644 --- a/pyk/src/pyk/k2lean4/k2lean4.py +++ b/pyk/src/pyk/k2lean4/k2lean4.py @@ -31,7 +31,7 @@ def is_inductive(sort: str) -> bool: def _inductive(self, sort: str) -> Inductive: subsorts = sorted(self.defn.subsorts.get(sort, ())) - symbols = sorted(self.defn.ctor_symbols.get(sort, ())) + symbols = sorted(self.defn.constructors.get(sort, ())) ctors: list[Ctor] = [] ctors.extend(self._inj_ctor(sort, subsort) for subsort in subsorts) ctors.extend(self._symbol_ctor(sort, symbol) for symbol in symbols) diff --git a/pyk/src/pyk/kore/internal.py b/pyk/src/pyk/kore/internal.py index 9d21f91f9eb..48f4c58099a 100644 --- a/pyk/src/pyk/kore/internal.py +++ b/pyk/src/pyk/kore/internal.py @@ -55,7 +55,7 @@ def from_definition(defn: Definition) -> KoreDefn: ) @cached_property - def ctor_symbols(self) -> FrozenDict[str, tuple[str, ...]]: + def constructors(self) -> FrozenDict[str, tuple[str, ...]]: grouped: dict[str, list[str]] = {} for symbol, decl in self.symbols.items(): if not 'constructor' in decl.attrs_by_key: @@ -130,7 +130,7 @@ def _config_symbols(self) -> set[str]: if sort in done: continue done.add(sort) - symbols = self.ctor_symbols.get(sort, ()) + symbols = self.constructors.get(sort, ()) pending.extend(sort for symbol in symbols for sort in self._symbol_sorts(symbol)) res.update(symbols) return res From 2cab5bd2ac1f0d250cb71af724c25d312e5d824a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Fri, 20 Dec 2024 12:23:29 +0000 Subject: [PATCH 4/6] Add property `collections` to `KoreDefn` --- pyk/src/pyk/kore/internal.py | 63 ++++++++++++++++++++++++++++++++++-- 1 file changed, 61 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/kore/internal.py b/pyk/src/pyk/kore/internal.py index 48f4c58099a..b43d377c6d9 100644 --- a/pyk/src/pyk/kore/internal.py +++ b/pyk/src/pyk/kore/internal.py @@ -1,18 +1,66 @@ from __future__ import annotations from dataclasses import dataclass +from enum import Enum from functools import cached_property -from typing import TYPE_CHECKING, final +from typing import TYPE_CHECKING, NamedTuple, final from ..utils import FrozenDict, POSet, check_type from .manip import collect_symbols from .rule import FunctionRule, RewriteRule, Rule -from .syntax import App, Axiom, SortApp, SortDecl, Symbol, SymbolDecl +from .syntax import App, Axiom, SortApp, SortDecl, String, Symbol, SymbolDecl if TYPE_CHECKING: from .syntax import Definition +class CollectionKind(Enum): + LIST = 'List' + MAP = 'Map' + SET = 'Set' + + +class Collection(NamedTuple): + sort: str + concat: str + element: str + unit: str + kind: CollectionKind + + @staticmethod + def from_decl(decl: SortDecl) -> Collection: + if not 'element' in decl.attrs_by_key: + raise ValueError(f'Not a sort declaration: {decl.text}') + sort = decl.name + concat = Collection._extract_label(decl, 'concat') + element = Collection._extract_label(decl, 'element') + unit = Collection._extract_label(decl, 'unit') + kind = CollectionKind(Collection._extract_string(decl, 'hook').split('.')[1]) # 'MAP.Map' -> CollectionKind.MAP + return Collection( + sort=sort, + concat=concat, + element=element, + unit=unit, + kind=kind, + ) + + @staticmethod + def _extract_label(decl: SortDecl, attr: str) -> str: + match decl.attrs_by_key[attr]: + case App(attr, args=(App(res),)): + return res + case _: + raise AssertionError() + + @staticmethod + def _extract_string(decl: SortDecl, attr: str) -> str: + match decl.attrs_by_key[attr]: + case App(attr, args=(String(res),)): + return res + case _: + raise AssertionError() + + @final @dataclass(frozen=True) class KoreDefn: @@ -64,6 +112,17 @@ def constructors(self) -> FrozenDict[str, tuple[str, ...]]: grouped.setdefault(sort, []).append(symbol) return FrozenDict((sort, tuple(symbols)) for sort, symbols in grouped.items()) + @cached_property + def collections(self) -> FrozenDict[str, Collection]: + colls: dict[str, Collection] = {} + for sort, decl in self.sorts.items(): + if not 'element' in decl.attrs_by_key: + continue + coll = Collection.from_decl(decl) + assert sort == coll.sort + colls[sort] = coll + return FrozenDict(colls) + def let( self, *, From e97e68caefc10c4cac84806efa49efd8e8c158dd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Thu, 19 Dec 2024 16:45:14 +0000 Subject: [PATCH 5/6] Add prelude --- pyk/src/pyk/k2lean4/Prelude.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 pyk/src/pyk/k2lean4/Prelude.lean diff --git a/pyk/src/pyk/k2lean4/Prelude.lean b/pyk/src/pyk/k2lean4/Prelude.lean new file mode 100644 index 00000000000..ce14a59bfd8 --- /dev/null +++ b/pyk/src/pyk/k2lean4/Prelude.lean @@ -0,0 +1,10 @@ +abbrev SortBool : Type := Int +abbrev SortBytes: Type := ByteArray +abbrev SortId : Type := String +abbrev SortInt : Type := Int +abbrev SortString : Type := String +abbrev SortStringBuffer : Type := String + +abbrev ListHook (E : Type) : Type := List E +abbrev MapHook (K : Type) (V : Type) : Type := List (K × V) +abbrev SetHook (E : Type) : Type := List E From 0269c7a12cb099a31f3d47e80f4582efc0fcfcac Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?= Date: Fri, 20 Dec 2024 14:09:23 +0000 Subject: [PATCH 6/6] Generate an `abbrev` for each collection --- pyk/src/pyk/k2lean4/k2lean4.py | 27 ++++++++++++++++++++++++--- pyk/src/pyk/kore/internal.py | 8 +++++++- 2 files changed, 31 insertions(+), 4 deletions(-) diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/k2lean4/k2lean4.py index d4b86146da8..892aef8d7b7 100644 --- a/pyk/src/pyk/k2lean4/k2lean4.py +++ b/pyk/src/pyk/k2lean4/k2lean4.py @@ -3,9 +3,10 @@ from dataclasses import dataclass from typing import TYPE_CHECKING +from ..kore.internal import CollectionKind from ..kore.syntax import SortApp from ..utils import check_type -from .model import Ctor, ExplBinder, Inductive, Module, Signature, Term +from .model import Abbrev, Ctor, ExplBinder, Inductive, Module, Signature, Term if TYPE_CHECKING: from ..kore.internal import KoreDefn @@ -19,7 +20,8 @@ class K2Lean4: def sort_module(self) -> Module: commands = [] commands += self._inductives() - return Module(commands=self._inductives()) + commands += self._collections() + return Module(commands=commands) def _inductives(self) -> list[Command]: def is_inductive(sort: str) -> bool: @@ -41,7 +43,26 @@ 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) + param_sorts = ( + check_type(sort, SortApp).name for sort in self.defn.symbols[symbol].param_sorts + ) # TODO eliminate check_type 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))) + + def _collections(self) -> list[Command]: + return [self._collection(sort) for sort in sorted(self.defn.collections)] + + 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 + assert sorts + match coll.kind: + case CollectionKind.LIST: + val = Term(f'ListHook {sorts}') + case CollectionKind.MAP: + val = Term(f'MapHook {sorts}') + case CollectionKind.SET: + val = Term(f'SetHook {sorts}') + return Abbrev(sort, val, Signature((), Term('Type'))) diff --git a/pyk/src/pyk/kore/internal.py b/pyk/src/pyk/kore/internal.py index b43d377c6d9..95eb918bc74 100644 --- a/pyk/src/pyk/kore/internal.py +++ b/pyk/src/pyk/kore/internal.py @@ -189,7 +189,13 @@ def _config_symbols(self) -> set[str]: if sort in done: continue done.add(sort) - symbols = self.constructors.get(sort, ()) + + symbols: list[str] = [] + if sort in self.collections: + coll = self.collections[sort] + symbols += (coll.concat, coll.element, coll.unit) + symbols += self.constructors.get(sort, ()) + pending.extend(sort for symbol in symbols for sort in self._symbol_sorts(symbol)) res.update(symbols) return res