A pair of py↔lean conversion functions for a particular `TypeRepr`. For types that can appear as inline scalar fields inside a ``lean_ctor_object`` (Bool, enum inductives, UInt*, etc.), the three ``ctor_scalar_*`` attributes describe how to read/write them: - ``ctor_scalar_size``:
| 120 | |
| 121 | |
| 122 | class TypeWrapper: |
| 123 | """A pair of py↔lean conversion functions for a particular `TypeRepr`. |
| 124 | |
| 125 | For types that can appear as inline scalar fields inside a |
| 126 | ``lean_ctor_object`` (Bool, enum inductives, UInt*, etc.), the three |
| 127 | ``ctor_scalar_*`` attributes describe how to read/write them: |
| 128 | |
| 129 | - ``ctor_scalar_size``: byte width (1/2/4/8), or *None* for pointer fields. |
| 130 | - ``from_ctor_scalar(raw_int) → python_value`` |
| 131 | - ``to_ctor_scalar(python_value) → raw_int`` |
| 132 | """ |
| 133 | |
| 134 | __slots__ = ( |
| 135 | "repr", |
| 136 | "from_lean", |
| 137 | "to_lean", |
| 138 | "ctype", |
| 139 | "ctor_scalar_size", |
| 140 | "from_ctor_scalar", |
| 141 | "to_ctor_scalar", |
| 142 | ) |
| 143 | |
| 144 | def __init__( |
| 145 | self, |
| 146 | type_repr: TypeRepr, |
| 147 | from_lean: Callable[[Any], Any], |
| 148 | to_lean: Callable[[Any], Any], |
| 149 | ctype: Any, |
| 150 | *, |
| 151 | ctor_scalar_size: int | None = None, |
| 152 | from_ctor_scalar: Callable[[int], Any] | None = None, |
| 153 | to_ctor_scalar: Callable[[Any], int] | None = None, |
| 154 | ) -> None: |
| 155 | self.repr = type_repr |
| 156 | self.from_lean = from_lean |
| 157 | self.to_lean = to_lean |
| 158 | self.ctype = ctype |
| 159 | self.ctor_scalar_size = ctor_scalar_size |
| 160 | self.from_ctor_scalar = from_ctor_scalar |
| 161 | self.to_ctor_scalar = to_ctor_scalar |
| 162 | |
| 163 | def __repr__(self) -> str: |
| 164 | return f"<TypeWrapper {self.repr.short()}>" |
| 165 | |
| 166 | |
| 167 | def _is_enum_tag_only(ti: TypeInfo) -> bool: |
no outgoing calls
no test coverage detected