Add Python implementations of key static inline functions.
(class_dict: dict, structs: dict, constants: dict)
| 318 | |
| 319 | |
| 320 | def _add_inline_methods(class_dict: dict, structs: dict, constants: dict): |
| 321 | """Add Python implementations of key static inline functions.""" |
| 322 | LeanObjectPtr = structs["_LeanObjectPtr"] |
| 323 | _SCALAR_BIT = 1 |
| 324 | |
| 325 | def _ptr_int(o): |
| 326 | if o is None: |
| 327 | return 0 |
| 328 | return ctypes.cast(o, c_void_p).value or 0 |
| 329 | |
| 330 | def lean_is_scalar(self, o): |
| 331 | return _ptr_int(o) & _SCALAR_BIT == 1 |
| 332 | |
| 333 | def lean_box(self, n): |
| 334 | if isinstance(n, int): |
| 335 | ptr_val = (n << 1) | 1 |
| 336 | else: |
| 337 | ptr_val = (_ptr_int(n) << 1) | 1 |
| 338 | return ctypes.cast(c_void_p(ptr_val), LeanObjectPtr) |
| 339 | |
| 340 | def lean_unbox(self, o): |
| 341 | return _ptr_int(o) >> 1 |
| 342 | |
| 343 | def lean_ptr_tag(self, o): |
| 344 | return o.contents.m_tag |
| 345 | |
| 346 | def lean_ptr_other(self, o): |
| 347 | return o.contents.m_other |
| 348 | |
| 349 | def lean_is_mt(self, o): |
| 350 | return o.contents.m_rc < 0 |
| 351 | |
| 352 | def lean_is_st(self, o): |
| 353 | return o.contents.m_rc > 0 |
| 354 | |
| 355 | def lean_is_persistent(self, o): |
| 356 | return o.contents.m_rc == 0 |
| 357 | |
| 358 | def lean_has_rc(self, o): |
| 359 | return o.contents.m_rc != 0 |
| 360 | |
| 361 | def lean_inc_ref(self, o): |
| 362 | if o is None: |
| 363 | return |
| 364 | helper = self._find_leanpy_helper("leanpy_inc_ref") |
| 365 | if helper is not None: |
| 366 | helper.argtypes = [c_void_p] |
| 367 | helper.restype = None |
| 368 | helper(_ptr_as_int(o)) |
| 369 | return |
| 370 | if o.contents.m_rc > 0: |
| 371 | o.contents.m_rc += 1 |
| 372 | |
| 373 | def lean_inc_ref_n(self, o, n): |
| 374 | if o is None: |
| 375 | return |
| 376 | helper = self._find_leanpy_helper("leanpy_inc_ref_n") |
| 377 | if helper is not None: |