Add convenience helper methods.
(class_dict: dict, structs: dict)
| 691 | |
| 692 | |
| 693 | def _add_helper_methods(class_dict: dict, structs: dict): |
| 694 | """Add convenience helper methods.""" |
| 695 | |
| 696 | def mk_string(self, s): |
| 697 | """Create a Lean string from a Python string.""" |
| 698 | if isinstance(s, str): |
| 699 | s = s.encode("utf-8") |
| 700 | return self.lean_mk_string(s) |
| 701 | |
| 702 | def io_result_show_error(self, res): |
| 703 | """Display an IO error result.""" |
| 704 | self.lean_io_result_show_error(res) |
| 705 | |
| 706 | class_dict["mk_string"] = mk_string |
| 707 | class_dict["io_result_show_error"] = io_result_show_error |
| 708 | |
| 709 | |
| 710 | # ============================================================================ |
| 711 | # Module-level singleton |
| 712 | # ============================================================================ |
| 713 | |
| 714 | _ffi_initialized = False |
| 715 | _cached_model: HeaderModel | None = None |
| 716 | _cached_structs: dict[str, type] | None = None |
| 717 | _LeanFFI: type | None = None |
| 718 | |
| 719 | |
| 720 | def _ensure_built(): |
| 721 | """Ensure the runtime types are built (lazy init).""" |
| 722 | global _cached_model, _cached_structs, _LeanFFI |
| 723 | if _LeanFFI is not None: |
| 724 | return |
| 725 | _cached_model = get_header_model() |
| 726 | _cached_structs = _build_structs(_cached_model) |
| 727 | _LeanFFI = _build_ffi_class(_cached_model, _cached_structs) |
| 728 | |
| 729 | |
| 730 | def get_structs() -> dict[str, type]: |
| 731 | """Get the dynamically created struct types.""" |