From cf76566d9892a67cd6ae085b06cfdc8e8ca9776f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Mon, 20 Jan 2025 09:44:15 +0100
Subject: [PATCH]  Generate an axiom for each function signature  (#4736)

Closes #4726

K function production

```k
syntax Int ::= foo ( Int ) [function]
```

becomes

```lean
axiom foo (x : SortInt) : Option SortInt
```
---
 pyk/src/pyk/k2lean4/k2lean4.py | 21 ++++++++++++++++++++-
 pyk/src/pyk/k2lean4/model.py   | 18 ++++++++++++++++++
 2 files changed, 38 insertions(+), 1 deletion(-)

diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/k2lean4/k2lean4.py
index 56c5da967d..f393da660b 100644
--- a/pyk/src/pyk/k2lean4/k2lean4.py
+++ b/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
diff --git a/pyk/src/pyk/k2lean4/model.py b/pyk/src/pyk/k2lean4/model.py
index 6ca0ad23fe..c53e4c2a53 100644
--- a/pyk/src/pyk/k2lean4/model.py
+++ b/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):