Use new infer_variance flag instead of manually specifying type variable

variance

Author: qthibeault

banquo/_banquo_impl.pyi

@@ -9,7 +9,7 @@ from .operators import Bounds, M, M_ge, M_le, M_neg, M_neg_ge
 
 class PanicException(Exception): ...
 
-T = TypeVar("T", covariant=True)
+_T = TypeVar("_T", infer_variance=True)
 
 class Top(Any):  # pyright: ignore[reportAny, reportExplicitAny]
     def __le__(self, other: object) -> bool: ...
@@ -27,54 +27,54 @@ class Bottom(Any):  # pyright: ignore[reportAny, reportExplicitAny]
     def __ge__(self, other: object) -> bool: ...
     def __gt__(self, other: object) -> bool: ...
 
-class Trace(Generic[_T_co]):
-    def __new__(cls, elements: dict[float, _T_co] | Trace[_T_co]) -> Self: ...
-    def __getitem__(self, value: float) -> _T_co: ...
+class Trace(Generic[_T]):
+    def __new__(cls, elements: dict[float, _T] | Trace[_T]) -> Self: ...
+    def __getitem__(self, value: float) -> _T: ...
     def times(self) -> Iterable[float]: ...
-    def states(self) -> Iterable[_T_co]: ...
-    def at_time(self, time: float) -> _T_co | None: ...
+    def states(self) -> Iterable[_T]: ...
+    def at_time(self, time: float) -> _T | None: ...
 
 class Predicate(Formula[dict[str, float], float]):
     def __new__(cls, coefficients: dict[str, float], constant: float) -> Self: ...
     @override
     def evaluate(self, trace: Trace[dict[str, float]]) -> Trace[float]: ...
 
-S = TypeVar("S", contravariant=True)
+_S = TypeVar("_S", infer_variance=True)
 
-class Not(Formula[S, M_neg]):
-    def __new__(cls, subformula: Formula[S, M_neg]) -> Self: ...
+class Not(Formula[_S, M_neg]):
+    def __new__(cls, subformula: Formula[_S, M_neg]) -> Self: ...
     @override
-    def evaluate(self, trace: Trace[S]) -> Trace[M_neg]: ...
+    def evaluate(self, trace: Trace[_S]) -> Trace[M_neg]: ...
 
-class And(Formula[S, M_le]):
-    def __new__(cls, lhs: Formula[S, M_le], rhs: Formula[S, M_le]) -> Self: ...
+class And(Formula[_S, M_le]):
+    def __new__(cls, lhs: Formula[_S, M_le], rhs: Formula[_S, M_le]) -> Self: ...
     @override
-    def evaluate(self, trace: Trace[S]) -> Trace[M_le]: ...
+    def evaluate(self, trace: Trace[_S]) -> Trace[M_le]: ...
 
-class Or(Formula[S, M_ge]):
-    def __new__(cls, lhs: Formula[S, M_ge], rhs: Formula[S, M_ge]) -> Self: ...
+class Or(Formula[_S, M_ge]):
+    def __new__(cls, lhs: Formula[_S, M_ge], rhs: Formula[_S, M_ge]) -> Self: ...
     @override
-    def evaluate(self, trace: Trace[S]) -> Trace[M_ge]: ...
+    def evaluate(self, trace: Trace[_S]) -> Trace[M_ge]: ...
 
-class Implies(Formula[S, M_neg_ge]):
-    def __new__(cls, lhs: Formula[S, M_neg_ge], rhs: Formula[S, M_neg_ge]) -> Self: ...
+class Implies(Formula[_S, M_neg_ge]):
+    def __new__(cls, lhs: Formula[_S, M_neg_ge], rhs: Formula[_S, M_neg_ge]) -> Self: ...
     @override
-    def evaluate(self, trace: Trace[S]) -> Trace[M_neg_ge]: ...
+    def evaluate(self, trace: Trace[_S]) -> Trace[M_neg_ge]: ...
 
-class Next(Formula[S, M]):
-    def __new__(cls, subformula: Formula[S, M]) -> Self: ...
+class Next(Formula[_S, M]):
+    def __new__(cls, subformula: Formula[_S, M]) -> Self: ...
     @override
-    def evaluate(self, trace: Trace[S]) -> Trace[M]: ...
+    def evaluate(self, trace: Trace[_S]) -> Trace[M]: ...
 
-class Always(Formula[S, M_le]):
-    def __new__(cls, bounds: Bounds | None, subformula: Formula[S, M_le]) -> Self: ...
+class Always(Formula[_S, M_le]):
+    def __new__(cls, bounds: Bounds | None, subformula: Formula[_S, M_le]) -> Self: ...
     @override
-    def evaluate(self, trace: Trace[S]) -> Trace[M_le]: ...
+    def evaluate(self, trace: Trace[_S]) -> Trace[M_le]: ...
 
-class Eventually(Formula[S, M_ge]):
-    def __new__(cls, bounds: Bounds | None, subformula: Formula[S, M_ge]) -> Self: ...
+class Eventually(Formula[_S, M_ge]):
+    def __new__(cls, bounds: Bounds | None, subformula: Formula[_S, M_ge]) -> Self: ...
     @override
-    def evaluate(self, trace: Trace[S]) -> Trace[M_ge]: ...
+    def evaluate(self, trace: Trace[_S]) -> Trace[M_ge]: ...
 
 class _StlModule(ModuleType):
     class Formula(Formula[dict[str, float], float]): ...

banquo/core.py

@@ -8,8 +8,8 @@
 from ._banquo_impl import Trace as _Trace
 from .trace import Trace
 
-S = TypeVar("S", contravariant=True)
-M = TypeVar("M", covariant=True)
+S = TypeVar("S", infer_variance=True)
+M = TypeVar("M", infer_variance=True)
 
 
 class Formula(Protocol[S, M]):

banquo/operators.py

@@ -22,12 +22,12 @@
 
 Bounds: TypeAlias = tuple[float, float]
 
-S = typing.TypeVar("S")
-M = typing.TypeVar("M", covariant=True)
-M_neg = typing.TypeVar("M_neg", bound=SupportsNeg, covariant=True)
-M_le = typing.TypeVar("M_le", bound=SupportsLT, covariant=True)
-M_ge = typing.TypeVar("M_ge", bound=SupportsGT, covariant=True)
-M_neg_ge = typing.TypeVar("M_neg_ge", bound=SupportsNegGE, covariant=True)
+S = TypeVar("S", infer_variance=True)
+M = TypeVar("M", infer_variance=True)
+M_neg = TypeVar("M_neg", bound=SupportsNeg, infer_variance=True)
+M_le = TypeVar("M_le", bound=SupportsLT, infer_variance=True)
+M_ge = TypeVar("M_ge", bound=SupportsGT, infer_variance=True)
+M_neg_ge = TypeVar("M_neg_ge", bound=SupportsNegGE, infer_variance=True)
 
 
 class OperatorMixin:
@@ -132,8 +132,8 @@ def __init__(self, subformula: Formula[S, M]):
         super().__init__(_Next(_inner_or_wrap(subformula)), "")
 
 
-S_ = typing.TypeVar("S_")
-M_le_ = typing.TypeVar("M_le_", bound=SupportsLT, covariant=True)
+S_ = TypeVar("S_", infer_variance=True)
+M_le_ = TypeVar("M_le_", bound=SupportsLT, infer_variance=True)
 
 
 class Always(Operator[S, M_le]):
@@ -173,7 +173,7 @@ def with_bounds(bounds: Bounds, subformula: Formula[S_, M_le_]) -> Always[S_, M_
         return Always(_Always(bounds, _inner_or_wrap(subformula)))
 
 
-M_ge_ = typing.TypeVar("M_ge_", bound=SupportsGT, covariant=True)
+M_ge_ = TypeVar("M_ge_", bound=SupportsGT, infer_variance=True)
 
 
 class Eventually(Operator[S, M_ge]):

banquo/trace.py

@@ -6,8 +6,8 @@
 
 from ._banquo_impl import Trace as _Trace
 
-T = TypeVar("T", covariant=True)
-U = TypeVar("U", covariant=True)
+T = TypeVar("T", infer_variance=True)
+U = TypeVar("U", infer_variance=True)
 
 
 def _iter_eq(lhs: Iterable[object], rhs: Iterable[object]) -> bool: