Skip to content

Commit

Permalink
Extract method _symbol_ident
Browse files Browse the repository at this point in the history
  • Loading branch information
tothtamas28 committed Jan 8, 2025
1 parent d7871d9 commit 92fa2bb
Showing 1 changed file with 5 additions and 1 deletion.
6 changes: 5 additions & 1 deletion pyk/src/pyk/k2lean4/k2lean4.py
Original file line number Diff line number Diff line change
Expand Up @@ -46,10 +46,14 @@ def _symbol_ctor(self, sort: str, symbol: str) -> Ctor:
param_sorts = (
check_type(sort, SortApp).name for sort in self.defn.symbols[symbol].param_sorts
) # TODO eliminate check_type
symbol = self._symbol_ident(symbol)
binders = tuple(ExplBinder((f'x{i}',), Term(sort)) for i, sort in enumerate(param_sorts))
symbol = symbol.replace('-', '_')
return Ctor(symbol, Signature(binders, Term(sort)))

@staticmethod
def _symbol_ident(symbol: str) -> str:
return symbol.replace('-', '_')

def _collections(self) -> list[Command]:
return [self._collection(sort) for sort in sorted(self.defn.collections)]

Expand Down

0 comments on commit 92fa2bb

Please sign in to comment.