MCPcopy Create free account
hub / github.com/BasisResearch/lean.py / _build_structs

Function _build_structs

lean_py/_runtime.py:153–177  ·  view source on GitHub ↗

Dynamically create ctypes Structure classes from the model.

(model: HeaderModel)

Source from the content-addressed store, hash-verified

151
152
153def _build_structs(model: HeaderModel) -> dict[str, type]:
154 """Dynamically create ctypes Structure classes from the model."""
155 structs: dict[str, type] = {}
156
157 # Build lean_object first (others depend on it)
158 lean_obj_def = next((s for s in model.structs if s.name == "lean_object"), None)
159 if lean_obj_def:
160 lean_object = _make_struct(lean_obj_def, structs)
161 structs["lean_object"] = lean_object
162 structs["_LeanObjectPtr"] = POINTER(lean_object)
163 # Register pointer aliases in type map
164 _TYPE_MAP["lean_object *"] = structs["_LeanObjectPtr"]
165 _TYPE_MAP["lean_obj_arg"] = structs["_LeanObjectPtr"]
166 _TYPE_MAP["b_lean_obj_arg"] = structs["_LeanObjectPtr"]
167 _TYPE_MAP["u_lean_obj_arg"] = structs["_LeanObjectPtr"]
168 _TYPE_MAP["lean_obj_res"] = structs["_LeanObjectPtr"]
169 _TYPE_MAP["b_lean_obj_res"] = structs["_LeanObjectPtr"]
170
171 # Build remaining structs
172 for sdef in model.structs:
173 if sdef.name == "lean_object":
174 continue
175 structs[sdef.name] = _make_struct(sdef, structs)
176
177 return structs
178
179
180def _make_struct(sdef: StructDef, known: dict[str, type]) -> type:

Callers 1

_ensure_builtFunction · 0.85

Calls 1

_make_structFunction · 0.85

Tested by

no test coverage detected