Human-readable string for an ASTSort.
(s: ASTSort)
| 1461 | |
| 1462 | |
| 1463 | def _sort_repr(s: ASTSort) -> str: |
| 1464 | """Human-readable string for an ASTSort.""" |
| 1465 | if isinstance(s, PropSort): |
| 1466 | return "Prop" |
| 1467 | if isinstance(s, IntASTSort): |
| 1468 | return "Int" |
| 1469 | if isinstance(s, NatASTSort): |
| 1470 | return "Nat" |
| 1471 | if isinstance(s, RealASTSort): |
| 1472 | return "Real" |
| 1473 | if isinstance(s, BitvecASTSort): |
| 1474 | return f"(BitVec {s.width})" |
| 1475 | if isinstance(s, StringASTSort): |
| 1476 | return "String" |
| 1477 | if isinstance(s, UninterpASTSort): |
| 1478 | return s.name |
| 1479 | if isinstance(s, ArrowASTSort): |
| 1480 | return f"({_sort_repr(s.dom)} \u2192 {_sort_repr(s.cod)})" |
| 1481 | if isinstance(s, InductiveASTSort): |
| 1482 | return s.name |
| 1483 | if isinstance(s, CharASTSort): |
| 1484 | return "Char" |
| 1485 | if isinstance(s, SeqASTSort): |
| 1486 | return f"(Seq {_sort_repr(s.elem)})" |
| 1487 | return str(s) |
| 1488 | |
| 1489 | |
| 1490 | # --------------------------------------------------------------------------- |