(self, ti: TypeInfo, value: Any)
| 556 | return LeanInductiveValue(ti.name, ctor.name, tag, fields) |
| 557 | |
| 558 | def _encode_inductive(self, ti: TypeInfo, value: Any) -> Any: |
| 559 | # Accept LeanInductiveValue, _CtorMeta classes, or (ctor_name, *args) tuple. |
| 560 | if type(value) is _CtorMeta: |
| 561 | ctor = next((c for c in ti.ctors if c.name == value._ctor_name), None) # type: ignore[attr-defined] |
| 562 | if ctor is None: |
| 563 | raise ValueError(f"unknown ctor {value._ctor_name} for {ti.name}") # type: ignore[attr-defined] |
| 564 | field_values = () |
| 565 | elif isinstance(value, LeanInductiveValue): |
| 566 | ctor = next((c for c in ti.ctors if c.name == value.ctor), None) |
| 567 | if ctor is None: |
| 568 | raise ValueError(f"unknown ctor {value.ctor} for {ti.name}") |
| 569 | field_values = value.fields |
| 570 | elif isinstance(value, tuple) and value and isinstance(value[0], str): |
| 571 | ctor = next((c for c in ti.ctors if c.name == value[0]), None) |
| 572 | if ctor is None: |
| 573 | raise ValueError(f"unknown ctor {value[0]} for {ti.name}") |
| 574 | field_values = value[1:] |
| 575 | else: |
| 576 | raise TypeError(f"cannot encode {value!r} as {ti.name}") |
| 577 | if len(field_values) != len(ctor.fields): |
| 578 | raise ValueError( |
| 579 | f"{ti.name}.{ctor.name}: expected {len(ctor.fields)} fields, " |
| 580 | f"got {len(field_values)}" |
| 581 | ) |
| 582 | if not ctor.fields: |
| 583 | # Check for nullary smart constructors (e.g. Level.zero). |
| 584 | smart = self._smart_ctors.get((ti.name, ctor.name)) |
| 585 | if smart is not None: |
| 586 | return smart(self.ffi, self._lean_object_ptr, []) |
| 587 | return self.ffi.lean_box(ctor.tag) |
| 588 | |
| 589 | # If a smart constructor exists, encode children for it and call. |
| 590 | smart = self._smart_ctors.get((ti.name, ctor.name)) |
| 591 | if smart is not None: |
| 592 | children = [] |
| 593 | for ftype, fv in zip(ctor.fields, field_values): # type: ignore[var-annotated] |
| 594 | fwrap = self.wrapper_for(ftype) |
| 595 | children.append(fwrap.to_lean(fv)) |
| 596 | return smart(self.ffi, self._lean_object_ptr, children) |
| 597 | |
| 598 | # Default: allocate a ctor with the correct scalar layout. |
| 599 | obj_indices, scalar_plan, scalar_sz = self._ctor_field_layout(ctor) |
| 600 | num_objs = len(obj_indices) |
| 601 | obj = self.ffi.lean_alloc_ctor(ctor.tag, num_objs, scalar_sz) |
| 602 | |
| 603 | # Pointer fields. |
| 604 | for obj_pos, decl_idx in enumerate(obj_indices): |
| 605 | fwrap = self.wrapper_for(ctor.fields[decl_idx]) |
| 606 | child = fwrap.to_lean(field_values[decl_idx]) |
| 607 | self.ffi.lean_ctor_set(obj, obj_pos, child) |
| 608 | |
| 609 | # Scalar fields — use each wrapper's to_ctor_scalar. |
| 610 | scalar_base = num_objs * _PTR_SIZE |
| 611 | for decl_idx, byte_off, byte_sz in scalar_plan: |
| 612 | fwrap = self.wrapper_for(ctor.fields[decl_idx]) |
| 613 | raw = fwrap.to_ctor_scalar(field_values[decl_idx]) # type: ignore[misc] |
| 614 | setter = getattr(self.ffi, self._SCALAR_SETTERS[byte_sz]) |
| 615 | setter(obj, scalar_base + byte_off, raw) |
no test coverage detected