Class LeanInductiveValue

lean_py/marshal.py:232–289

A Python representation of a Lean inductive constructor. Attributes: ctor: the constructor name (unqualified). tag: integer tag. fields: tuple of decoded Python field values in declaration order. Supports Python 3.10+ structural pattern matching:: matc

class LeanInductiveValue:
    """A Python representation of a Lean inductive constructor.

    Attributes:
        ctor:   the constructor name (unqualified).
        tag:    integer tag.
        fields: tuple of decoded Python field values in declaration order.

    Supports Python 3.10+ structural pattern matching::

        match name_value:
            case Name.str(parent, leaf):
                print(f"name: {leaf}")
            case Name.anonymous():
                print("anonymous")

    Fields can also be accessed by index (``value._0``, ``value._1``, etc.).
    """

    __slots__ = ("ctor", "tag", "fields", "_type_name")
    __match_args__ = ("ctor", "tag", "fields")

    def __init__(self, type_name: str, ctor: str, tag: int, fields: tuple) -> None:
        self._type_name = type_name
        self.ctor = ctor
        self.tag = tag
        self.fields = fields

    def __getattr__(self, name: str) -> Any:
        if name.startswith("_") and name[1:].isdigit():
            idx = int(name[1:])
            if idx < len(self.fields):
                return self.fields[idx]
            raise AttributeError(f"field index {idx} out of range (have {len(self.fields)} fields)")
        raise AttributeError(name)

    def __repr__(self) -> str:
        if not self.fields:
            return f"{self._type_name}.{self.ctor}"
        return f"{self._type_name}.{self.ctor}({', '.join(repr(f) for f in self.fields)})"

    def __eq__(self, other: object) -> bool:
        if isinstance(other, LeanInductiveValue):
            return (self._type_name, self.tag, self.fields) == (
                other._type_name,
                other.tag,
                other.fields,
            )
        if type(other) is _CtorMeta:
            return (
                self._type_name == other._type_name  # type: ignore[attr-defined]
                and self.ctor == other._ctor_name  # type: ignore[attr-defined]
                and self.fields == ()
            )
        return NotImplemented

    def __hash__(self) -> int:
        return hash((self._type_name, self.tag, self.fields))