Source code for fosf.syntax.base

#!/usr/bin/env python3

from __future__ import annotations

from typing import ClassVar




class Tag(str):
    """Represents a Tag symbol."""

    def __repr__(self):
        return f"Tag({super().__repr__()})"

    def __hash__(self) -> int:
        return hash(("Tag", super().__hash__()))

    def __eq__(self, other: Tag) -> bool:
        return isinstance(other, Tag) and super().__eq__(other)





class Feature(str):
    """Represents a Feature symbol."""

    def __repr__(self):
        return f"Feature({super().__repr__()})"

    def __hash__(self) -> int:
        return hash(("Feature", super().__hash__()))

    def __eq__(self, other: Feature) -> bool:
        return isinstance(other, Feature) and super().__eq__(other)





class Sort:
    def __init__(self, value: str | Sort):
        if isinstance(value, Sort) and not isinstance(value, (DisjunctiveSort, FrozenDisjunctiveSort)):
            value = value.value
        elif not isinstance(value, str):
            raise TypeError(
                f"Sort must be initialized with a str or Sort, got {type(value).__name__}")
        self.value: str = value

    def __str__(self):
        return self.value

    def __repr__(self):
        return f"Sort({self.value!r})"

    def __hash__(self):
        return hash(("Sort", self.value))

    def __eq__(self, other):
        return isinstance(other, Sort) and self.value == other.value

    def __lt__(self, other):
        return self.value < other.value





class DisjunctiveSort(Sort):
    __hash__: ClassVar[None] = None

    def __init__(self, *sorts: str | Sort):
        self.value: set[Sort] = set()
        self.add(*sorts)



    def add(self, *sorts: str | Sort):
        for sort in sorts:
            if isinstance(sort, Sort):
                self.value.add(sort)
            else:
                # TODO: check other types, e.g. str
                self.value.add(Sort(sort))




    def freeze(self) -> FrozenDisjunctiveSort:
        return FrozenDisjunctiveSort(*self.value)


    def __str__(self):
        return f'{{ {", ".join(sorted(str(s) for s in self.value))} }}'

    def __repr__(self):
        return f"DisjunctiveSort({', '.join(sorted(repr(s) for s in self.value))})"

    def __eq__(self, other):
        return isinstance(other, DisjunctiveSort) and self.value == other.value

    def __iter__(self):
        return iter(self.value)

    def __len__(self):
        return len(self.value)





class FrozenDisjunctiveSort(Sort):
    def __init__(self, *sorts: str | Sort):
        self.value: frozenset[Sort] = frozenset(Sort(sort) for sort in sorts)
        self._hash: int | None = None



    def thaw(self) -> DisjunctiveSort:
        "Convert to a mutable DisjunctiveSort."
        return DisjunctiveSort(*self.value)


    def __str__(self):
        return f'{{ {", ".join(sorted(str(s) for s in self.value))} }}'

    def __repr__(self):
        return f"FrozenDisjunctiveSort({', '.join(sorted(repr(s) for s in self.value))})"

    def __hash__(self):
        if self._hash is None:
            self._hash = hash(("DisjunctiveSort", self.value))
        return self._hash

    def __eq__(self, other):
        return isinstance(other, FrozenDisjunctiveSort) and self.value == other.value

    def __iter__(self):
        return iter(self.value)

    def __len__(self):
        return len(self.value)