Merge pull request #5 from life4/upgrade-annotations

Upgrade annotations

deal_solver/_annotations.py

@@ -11,7 +11,7 @@
 from ._types import AstNode
 
 
-SIMPLE_SORTS: typing.Mapping[str, typing.Type[ProxySort]]
+SIMPLE_SORTS: typing.Mapping[str, type[ProxySort]]
 SIMPLE_SORTS = MappingProxyType({
     'bool':     types.bool,
     'int':      types.int,
@@ -38,7 +38,7 @@
 
 
 class Generic(typing.NamedTuple):
-    type: typing.Type[ProxySort]
+    type: type[ProxySort]
     arity: int
 
 

deal_solver/_ast.py

@@ -1,15 +1,14 @@
 from __future__ import annotations
 
 from contextlib import suppress
-from typing import Optional, Tuple
 
 import astroid
 from astroid.exceptions import InferenceError
 
 from ._types import AstNode
 
 
-def get_name(expr) -> Optional[str]:
+def get_name(expr) -> str | None:
     if isinstance(expr, astroid.Name):
         return expr.name
     if isinstance(expr, astroid.Attribute):
@@ -20,7 +19,7 @@ def get_name(expr) -> Optional[str]:
     return None
 
 
-def get_full_name(expr) -> Tuple[str, str]:
+def get_full_name(expr) -> tuple[str, str]:
     assert expr.parent is not None
 
     if type(expr.parent) is astroid.Module:
@@ -38,7 +37,7 @@ def get_full_name(expr) -> Tuple[str, str]:
     return path, func_name
 
 
-def infer(expr: astroid.NodeNG) -> Tuple[AstNode, ...]:
+def infer(expr: astroid.NodeNG) -> tuple[AstNode, ...]:
     with suppress(InferenceError, RecursionError):
         guesses = expr.infer()
         if guesses is astroid.Uninferable:  # pragma: no cover

deal_solver/_cached_property.py

@@ -1,6 +1,6 @@
 from __future__ import annotations
 
-from typing import Any, Callable, Generic, Optional, Type, TypeVar, overload
+from typing import Any, Callable, Generic, TypeVar, overload
 
 
 T = TypeVar('T')
@@ -13,11 +13,11 @@ def __init__(self, func: Callable[[Any], T]) -> None:
         self.func = func  # type: ignore
 
     @overload
-    def __get__(self, instance: None, owner: Optional[Type[Any]] = ...) -> 'cached_property[T]':
+    def __get__(self, instance: None, owner: type[Any] | None = ...) -> cached_property[T]:
         pass
 
     @overload
-    def __get__(self, instance, owner: Optional[Type[Any]] = ...) -> T:
+    def __get__(self, instance, owner: type[Any] | None = ...) -> T:
         pass
 
     def __get__(self, obj, cls):

deal_solver/_context/_context.py

@@ -1,8 +1,6 @@
-
 from __future__ import annotations
 
 import typing
-from typing import Optional
 
 import z3
 
@@ -20,17 +18,17 @@ class Context(typing.NamedTuple):
     # Since z3 freaks out when we provide an explicit context
     # (supposedly, because we forget to pass it in some places),
     # this value is always None at the moment.
-    z3_ctx: typing.Optional[z3.Context]
+    z3_ctx: z3.Context | None
 
     # Scope holds z3 values for all variables executed up to the current line.
     scope: Scope
 
     # Given are checks that we don't validate but assume them to be always true.
     # For example, post-conditions of all functions the current function calls.
-    given: Layer['BoolSort']
+    given: Layer[BoolSort]
 
     # Expected are checks we do validate. For example, all `assert` statements.
-    expected: Layer['BoolSort']
+    expected: Layer[BoolSort]
 
     exceptions: Layer[ExceptionInfo]    # all raised exceptions
     returns: Layer[ReturnInfo]          # all returned values
@@ -40,13 +38,13 @@ class Context(typing.NamedTuple):
     trace: Trace
 
     # exceptions occured during evaluation
-    skips: typing.List[Exception]
+    skips: list[Exception]
 
     # the user-provided function to extract contracts from called functions
     get_contracts: typing.Callable[[typing.Any], typing.Iterator]
 
     @classmethod
-    def make_empty(cls, *, get_contracts, **kwargs) -> 'Context':
+    def make_empty(cls, *, get_contracts, **kwargs) -> Context:
         obj = cls(
             z3_ctx=None,
             scope=Scope.make_empty(),
@@ -61,15 +59,15 @@ def make_empty(cls, *, get_contracts, **kwargs) -> 'Context':
         return obj.evolve(**kwargs)
 
     @property
-    def interrupted(self) -> 'BoolSort':
+    def interrupted(self) -> BoolSort:
         from .._proxies import or_expr
         return or_expr(
             *[exc.cond.m_bool(ctx=self) for exc in self.exceptions],
             *[ret.cond.m_bool(ctx=self) for ret in self.returns],
             ctx=self,
         )
 
-    def add_exception(self, exc: type, msg: str = '', cond: Optional['BoolSort'] = None) -> None:
+    def add_exception(self, exc: type, msg: str = '', cond: BoolSort | None = None) -> None:
         if cond is None:
             from .._proxies import BoolSort
             cond = BoolSort.val(True, ctx=self)
@@ -82,7 +80,7 @@ def add_exception(self, exc: type, msg: str = '', cond: Optional['BoolSort'] = N
         ))
 
     @property
-    def return_value(self) -> typing.Optional['ProxySort']:
+    def return_value(self) -> ProxySort | None:
         returns = list(self.returns)
         if not returns:
             return None
@@ -92,10 +90,10 @@ def return_value(self) -> typing.Optional['ProxySort']:
         return result.value
 
     @property
-    def evolve(self) -> typing.Callable[..., 'Context']:
+    def evolve(self) -> typing.Callable[..., Context]:
         return self._replace
 
-    def make_child(self) -> 'Context':
+    def make_child(self) -> Context:
         return self.evolve(
             scope=self.scope.make_child(),
             given=self.given.make_child(),

deal_solver/_context/_layer.py

@@ -13,16 +13,16 @@
 
 class ExceptionInfo(typing.NamedTuple):
     name: str               # exception name
-    names: typing.Set[str]  # exception name and names of all its bases
-    cond: 'BoolSort'        # indicates if the exception is raised
+    names: set[str]  # exception name and names of all its bases
+    cond: BoolSort        # indicates if the exception is raised
     message: str = ''
 
 
 class ReturnInfo(typing.NamedTuple):
-    value: 'ProxySort'
-    cond: 'BoolSort'
+    value: ProxySort
+    cond: BoolSort
 
-    def merge(self, other: 'ReturnInfo', ctx: 'Context') -> 'ReturnInfo':
+    def merge(self, other: ReturnInfo, ctx: Context) -> ReturnInfo:
         from .._proxies import if_expr, or_expr
 
         cls = type(self)
@@ -35,8 +35,8 @@ def merge(self, other: 'ReturnInfo', ctx: 'Context') -> 'ReturnInfo':
 class Layer(typing.Generic[T]):
     __slots__ = ['layer', 'parent']
 
-    layer: typing.List[T]
-    parent: typing.Optional['Layer[T]']
+    layer: list[T]
+    parent: Layer[T] | None
 
     def __init__(self, parent=None) -> None:
         self.layer = []
@@ -45,7 +45,7 @@ def __init__(self, parent=None) -> None:
     def add(self, item: T) -> None:
         self.layer.append(item)
 
-    def make_child(self) -> 'Layer[T]':
+    def make_child(self) -> Layer[T]:
         cls = type(self)
         return cls(parent=self)
 

deal_solver/_context/_scope.py

@@ -10,34 +10,34 @@
 class Scope:
     __slots__ = ['layer', 'parent']
 
-    layer: typing.Dict[str, 'ProxySort']
-    parent: typing.Optional['Scope']
+    layer: dict[str, ProxySort]
+    parent: Scope | None
 
-    def __init__(self, parent: typing.Optional['Scope'], vars) -> None:
+    def __init__(self, parent: Scope | None, vars) -> None:
         self.parent = parent
         self.layer = vars
 
     @classmethod
-    def make_empty(cls) -> 'Scope':
+    def make_empty(cls) -> Scope:
         return cls(
             vars=dict(),
             parent=None,
         )
 
-    def make_child(self) -> 'Scope':
+    def make_child(self) -> Scope:
         cls = type(self)
         return cls(
             parent=self,
             vars=dict(),
         )
 
-    def get(self, name: str) -> typing.Optional['ProxySort']:
+    def get(self, name: str) -> ProxySort | None:
         var = self.layer.get(name)
         if var is not None:
             return var
         if self.parent is not None:
             return self.parent.get(name=name)
         return None
 
-    def set(self, name: str, value: 'ProxySort') -> None:
+    def set(self, name: str, value: ProxySort) -> None:
         self.layer[name] = value

deal_solver/_eval_contracts.py

@@ -18,13 +18,13 @@ class Contract(typing.NamedTuple):
       and many nodes for `raises` (which are exceptions).
     """
     name: str
-    args: typing.List[AstNode]
+    args: list[AstNode]
 
 
 class Contracts(typing.NamedTuple):
     pre: Goal
     post: Goal
-    raises: typing.Set[str]
+    raises: set[str]
 
 
 def eval_contracts(func: astroid.FunctionDef, ctx: Context) -> Contracts:
@@ -51,7 +51,7 @@ def eval_contracts(func: astroid.FunctionDef, ctx: Context) -> Contracts:
     return goals
 
 
-def _eval_pre(ctx: Context, args: list) -> typing.Optional[BoolSort]:
+def _eval_pre(ctx: Context, args: list) -> BoolSort | None:
     contract = args[0]
     if not isinstance(contract, astroid.Lambda):
         return None

deal_solver/_eval_stmt.py

@@ -154,7 +154,7 @@ def eval_if_else(node: astroid.If, ctx: Context) -> None:
 
 @eval_stmt.register(astroid.Raise)
 def eval_raise(node: astroid.Raise, ctx: Context) -> None:
-    names: typing.Set[str] = set()
+    names: set[str] = set()
     for exc in (node.exc, node.cause):
         if exc is None:
             continue

deal_solver/_exceptions.py

@@ -1,4 +1,3 @@
-
 from __future__ import annotations
 
 

deal_solver/_funcs/_builtins.py

@@ -1,7 +1,5 @@
 from __future__ import annotations
 
-from typing import Optional
-
 import z3
 
 from .._context import Context
@@ -41,7 +39,7 @@ def builtins_sum(items: ProxySort, ctx: Context, **kwargs) -> ProxySort:
 
 # TODO: support more than 2 explicit arguments.
 @register('builtins.min')
-def builtins_min(a: ProxySort, b: Optional[ProxySort] = None, *, ctx: Context, **kwargs) -> ProxySort:
+def builtins_min(a: ProxySort, b: ProxySort | None = None, *, ctx: Context, **kwargs) -> ProxySort:
     if b is not None:
         return if_expr(a.m_lt(b, ctx=ctx), a, b, ctx=ctx)
 
@@ -71,7 +69,7 @@ def builtins_min(a: ProxySort, b: Optional[ProxySort] = None, *, ctx: Context, *
 
 
 @register('builtins.max')
-def builtins_max(a: ProxySort, b: Optional[ProxySort] = None, *, ctx: Context, **kwargs) -> ProxySort:
+def builtins_max(a: ProxySort, b: ProxySort | None = None, *, ctx: Context, **kwargs) -> ProxySort:
     if b is not None:
         return if_expr(a.m_gt(b, ctx=ctx), a, b, ctx=ctx)
 
@@ -124,7 +122,7 @@ def builtins_abs(x: ProxySort, ctx: Context, **kwargs) -> ProxySort:
 
 
 @register('builtins.len')
-def builtins_len(items: ProxySort, ctx: 'Context', **kwargs) -> IntSort:
+def builtins_len(items: ProxySort, ctx: Context, **kwargs) -> IntSort:
     return items.m_len(ctx=ctx)
 
 

deal_solver/_funcs/_registry.py

@@ -5,7 +5,7 @@
 
 
 T = typing.TypeVar('T', bound=typing.Callable)
-FUNCTIONS: typing.Dict[str, typing.Any] = dict()
+FUNCTIONS: dict[str, typing.Any] = dict()
 
 
 def init_all():

deal_solver/_goal.py

@@ -1,12 +1,12 @@
 from __future__ import annotations
 
-from typing import Iterator, List
+from typing import Iterator
 
 from ._proxies import BoolSort
 
 
 class Goal:
-    _items: List[BoolSort]
+    _items: list[BoolSort]
 
     def __init__(self) -> None:
         self._items = []

deal_solver/_model.py

@@ -35,7 +35,7 @@ class Model:
     def __init__(self, model: z3.ModelRef) -> None:
         self._model = model
 
-    def __iter__(self) -> typing.Iterator[typing.Tuple[str, object]]:
+    def __iter__(self) -> typing.Iterator[tuple[str, object]]:
         for decl in self._model.decls():
             name = decl.name()
             z3_val = self._model[decl]