Generate a structure even for leaf cells

pyk/src/pyk/k2lean4/k2lean4.py

@@ -74,24 +74,25 @@ def ordering(sorts: list[str]) -> dict[str, list[str]]:
         sorts = list(TopologicalSorter(ordering(sorts)).static_order())
         return [self._cell(sort) for sort in sorts]
 
-    def _cell(self, sort: str) -> Inductive | Structure:
+    def _cell(self, sort: str) -> Structure:
         (cell_ctor,) = self.defn.constructors[sort]
         decl = self.defn.symbols[cell_ctor]
         param_sorts = _param_sorts(decl)
 
-        if any(not self._is_cell(sort) for sort in param_sorts):
+        param_names: list[str]
+
+        if all(self._is_cell(sort) for sort in param_sorts):
+            param_names = []
+            for param_sort in param_sorts:
+                assert param_sort.startswith('Sort')
+                assert param_sort.endswith('Cell')
+                name = param_sort[4:-4]
+                name = name[0].lower() + name[1:]
+                param_names.append(name)
+        else:
             assert len(param_sorts) == 1
-            (param_sort,) = param_sorts
-            ctor = Ctor('mk', Signature((ExplBinder(('val',), Term(param_sort)),), Term(sort)))
-            return Inductive(sort, Signature((), Term('Type')), ctors=(ctor,))
-
-        param_names = []
-        for param_sort in param_sorts:
-            assert param_sort.startswith('Sort')
-            assert param_sort.endswith('Cell')
-            name = param_sort[4:-4]
-            name = name[0].lower() + name[1:]
-            param_names.append(name)
+            param_names = ['val']
+
         fields = tuple(ExplBinder((name,), Term(sort)) for name, sort in zip(param_names, param_sorts, strict=True))
         return Structure(sort, Signature((), Term('Type')), ctor=StructCtor(fields))