From 5d40d2f87ae59b74ab979d8f625a5231eaba1e5a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Wed, 22 Jan 2025 12:17:13 +0000
Subject: [PATCH] Implement method `_free_binders`

---
 pyk/src/pyk/k2lean4/k2lean4.py | 26 +++++++++++++++++++++-----
 1 file changed, 21 insertions(+), 5 deletions(-)

diff --git a/pyk/src/pyk/k2lean4/k2lean4.py b/pyk/src/pyk/k2lean4/k2lean4.py
index 145b6cddb1..f4493a42c6 100644
--- a/pyk/src/pyk/k2lean4/k2lean4.py
+++ b/pyk/src/pyk/k2lean4/k2lean4.py
@@ -9,7 +9,7 @@
 
 from ..konvert import unmunge
 from ..kore.internal import CollectionKind
-from ..kore.manip import elim_aliases
+from ..kore.manip import elim_aliases, free_occs
 from ..kore.syntax import DV, And, App, EVar, SortApp, String, Top
 from ..utils import FrozenDict, POSet
 from .model import (
@@ -314,8 +314,25 @@ def _elim_fun_apps(self, pattern: Pattern, free: Iterator[str]) -> tuple[Pattern
         return pattern, {}
 
     def _free_binders(self, pattern: Pattern) -> list[Binder]:
-        # TODO
-        return []
+        free_vars = {occ for _, occs in free_occs(pattern).items() for occ in occs}
+        grouped_vars: dict[str, set[str]] = {}
+        for var in free_vars:
+            match var:
+                case EVar(name, SortApp(sort)):
+                    ident = self._var_ident(name)
+                    assert ident not in grouped_vars.get(sort, ())
+                    grouped_vars.setdefault(sort, set()).add(ident)
+                case _:
+                    raise AssertionError()
+        sorted_vars: dict[str, list[str]] = dict(
+            sorted(((sort, sorted(idents)) for sort, idents in grouped_vars.items()), key=lambda item: item[1][0])
+        )
+        return [ImplBinder(idents, Term(sort)) for sort, idents in sorted_vars.items()]
+
+    @staticmethod
+    def _var_ident(name: str) -> str:
+        assert name.startswith('Var')
+        return K2Lean4._symbol_ident(name[3:])
 
     def _def_binders(self, defs: Mapping[str, Pattern]) -> list[Binder]:
         # TODO
@@ -333,8 +350,7 @@ def _transform_pattern(self, pattern: Pattern) -> Term:
                 raise ValueError(f'Unsupported pattern: {pattern.text}')
 
     def _transform_evar(self, name: str) -> Term:
-        assert name.startswith('Var')
-        return Term(self._symbol_ident(name[3:]))
+        return Term(self._var_ident(name))
 
     def _transform_dv(self, sort: str, value: str) -> Term:
         match sort: