Implement method '_def_binders'

pyk/src/pyk/k2lean4/k2lean4.py

@@ -287,7 +287,7 @@ def _rewrite_ctor(self, rule: RewriteRule) -> Ctor:
         pattern = elim_aliases(And(SortApp('Foo'), (req, rule.lhs, rule.rhs)))
 
         # Step 2: eliminate function application
-        free = (f"Var'Unds'val{i}" for i in count())
+        free = (f"Var'Unds'Val{i}" for i in count())
         pattern, defs = self._elim_fun_apps(pattern, free)
 
         # Step 3: create binders
@@ -313,17 +313,22 @@ def _rewrite_name(rule: RewriteRule) -> str:
             return rule.label.replace('-', '_').replace('.', '_')
         return f'_{rule.uid[:7]}'
 
+    @staticmethod
+    def _var_ident(name: str) -> str:
+        assert name.startswith('Var')
+        return K2Lean4._symbol_ident(name[3:])
+
     def _elim_fun_apps(self, pattern: Pattern, free: Iterator[str]) -> tuple[Pattern, dict[str, Pattern]]:
         """Replace ``foo(bar(x))`` with ``z`` and return mapping ``{y: bar(x), z: foo(y)}`` with ``y``, ``z`` fresh variables."""
         defs: dict[str, Pattern] = {}
 
         def abstract_funcs(pattern: Pattern) -> Pattern:
             if isinstance(pattern, App) and pattern.symbol in self.defn.functions:
                 name = next(free)
+                ident = self._var_ident(name)
+                defs[ident] = pattern
                 sort = self.symbol_table.infer_sort(pattern)
-                var = EVar(name, sort)
-                defs[name] = pattern
-                return var
+                return EVar(name, sort)
             return pattern
 
         return pattern.bottom_up(abstract_funcs), defs
@@ -344,14 +349,11 @@ def _free_binders(self, pattern: Pattern) -> list[Binder]:
         )
         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
-        return []
+        return [
+            ExplBinder((f'def{ident}',), Term(f'{self._transform_pattern(pattern)} = some {ident}'))
+            for ident, pattern in defs.items()
+        ]
 
     def _transform_pattern(self, pattern: Pattern) -> Term:
         match pattern: