Generate an axiom for each function signature

pyk/src/pyk/k2lean4/k2lean4.py

@@ -13,8 +13,10 @@
 from .model import (
     Alt,
     AltsFieldVal,
+    Axiom,
     Ctor,
     ExplBinder,
+    ImplBinder,
     Inductive,
     Instance,
     InstField,
@@ -33,7 +35,7 @@
 
     from ..kore.internal import KoreDefn
     from ..kore.syntax import SymbolDecl
-    from .model import Command, Declaration, FieldVal
+    from .model import Binder, Command, Declaration, FieldVal
 
 
 _VALID_LEAN_IDENT: Final = re.compile(
@@ -207,6 +209,23 @@ def inj(subsort: str, supersort: str, x: str) -> Term:
 
         return res
 
+    def func_module(self) -> Module:
+        commands = [self._transform_func(func) for func in self.defn.functions]
+        return Module(commands=commands)
+
+    def _transform_func(self, func: str) -> Axiom:
+        ident = self._symbol_ident(func)
+        decl = self.defn.symbols[func]
+        sort_params = [var.name for var in decl.symbol.vars]
+        param_sorts = [sort.name for sort in decl.param_sorts]
+        sort = decl.sort.name
+
+        binders: list[Binder] = []
+        if sort_params:
+            binders.append(ImplBinder(sort_params, Term('Type')))
+        binders.extend(ExplBinder((f'x{i}',), Term(sort)) for i, sort in enumerate(param_sorts))
+        return Axiom(ident, Signature(binders, Term(f'Option {sort}')))
+
 
 def _param_sorts(decl: SymbolDecl) -> list[str]:
     from ..utils import check_type

pyk/src/pyk/k2lean4/model.py

@@ -49,6 +49,24 @@ class Declaration(Command, ABC):
     modifiers: Modifiers | None
 
 
+@final
+@dataclass
+class Axiom(Declaration):
+    ident: DeclId
+    signature: Signature
+    modifiers: Modifiers | None
+
+    def __init__(self, ident: str | DeclId, signature: Signature, modifiers: Modifiers | None = None):
+        ident = DeclId(ident) if isinstance(ident, str) else ident
+        object.__setattr__(self, 'ident', ident)
+        object.__setattr__(self, 'signature', signature)
+        object.__setattr__(self, 'modifiers', modifiers)
+
+    def __str__(self) -> str:
+        modifiers = f'{self.modifiers} ' if self.modifiers else ''
+        return f'{modifiers}axiom {self.ident} {self.signature}'
+
+
 @final
 @dataclass
 class Abbrev(Declaration):