diff --git a/pyk/src/pyk/kast/_ast_to_kast.py b/pyk/src/pyk/kast/_ast_to_kast.py index 263dd19b217..d581c989d45 100644 --- a/pyk/src/pyk/kast/_ast_to_kast.py +++ b/pyk/src/pyk/kast/_ast_to_kast.py @@ -2,17 +2,15 @@ import logging from functools import singledispatch -from typing import TYPE_CHECKING +from typing import TYPE_CHECKING, Any from .att import EMPTY_ATT, Atts -from .outer import KAtt, KDefinition, KFlatModule, KImport, KRequire, KSentence # noqa: TC002 -from .outer_syntax import Att, Definition, Import, Module, Require, Sentence # noqa: TC002 +from .outer import KAst, KAtt, KDefinition, KFlatModule, KImport, KRequire, KSentence +from .outer_syntax import AST, Att, Definition, Import, Module, Require, Sentence # noqa: TC001 if TYPE_CHECKING: - from typing import Any, Final + from typing import Final - from .outer import KAst - from .outer_syntax import AST _LOGGER: Final = logging.getLogger(__name__) diff --git a/pyk/src/pyk/kllvm/hints/prooftrace.py b/pyk/src/pyk/kllvm/hints/prooftrace.py index 36028cd99f2..4b98d0f0f1e 100644 --- a/pyk/src/pyk/kllvm/hints/prooftrace.py +++ b/pyk/src/pyk/kllvm/hints/prooftrace.py @@ -26,7 +26,7 @@ # isort: on if TYPE_CHECKING: - from collections.abc import Generator + from collections.abc import Iterator from pathlib import Path from _kllvm.prooftrace import Argument @@ -568,7 +568,7 @@ def __repr__(self) -> str: """ return self._rewrite_trace_iterator.__repr__() - def __iter__(self) -> Generator[LLVMEventAnnotated, None, None]: + def __iter__(self) -> Iterator[LLVMEventAnnotated]: """Yield LLVMEventAnnotated options. This method is an iterator that yields LLVMEventAnnotated options. diff --git a/pyk/src/pyk/kore_exec_covr/kore_exec_covr.py b/pyk/src/pyk/kore_exec_covr/kore_exec_covr.py index 8e1995db6a5..4792514d18c 100644 --- a/pyk/src/pyk/kore_exec_covr/kore_exec_covr.py +++ b/pyk/src/pyk/kore_exec_covr/kore_exec_covr.py @@ -2,7 +2,7 @@ import logging import re -from collections import defaultdict +from collections import Counter from enum import Enum from typing import TYPE_CHECKING @@ -39,8 +39,8 @@ def parse_rule_applications(haskell_backend_oneline_log_file: Path) -> dict[Hask It seems likely that those are generated projection rules. We report their applications in bulk with UNKNOWN location. """ - rewrites: dict[str, int] = defaultdict(int) - simplifications: dict[str, int] = defaultdict(int) + rewrites: dict[str, int] = Counter() + simplifications: dict[str, int] = Counter() log_entries = haskell_backend_oneline_log_file.read_text().splitlines() for log_entry in log_entries: diff --git a/pyk/src/tests/integration/proof/test_imp.py b/pyk/src/tests/integration/proof/test_imp.py index 517051b001b..4cca73aa545 100644 --- a/pyk/src/tests/integration/proof/test_imp.py +++ b/pyk/src/tests/integration/proof/test_imp.py @@ -1516,7 +1516,7 @@ def test_all_path_reachability_prove_parallel( proof_status: ProofStatus, expected_leaf_number: int, tmp_path_factory: TempPathFactory, - create_prover: Callable[[int, Iterable[str]], Prover], + create_prover: Callable[[int | None, Iterable[str]], Prover], ) -> None: proof_dir = tmp_path_factory.mktemp(f'apr_tmp_proofs-{test_id}') spec_modules = kprove.parse_modules(Path(spec_file), module_name=spec_module)