|
1 | 1 | from __future__ import annotations
|
2 | 2 |
|
3 | 3 | import logging
|
| 4 | +from collections.abc import Callable |
4 | 5 | from typing import TYPE_CHECKING, NamedTuple
|
5 | 6 |
|
6 |
| -from pyk.cterm import CTerm |
| 7 | +from pyk.cterm import CTerm, CTermSymbolic |
7 | 8 | from pyk.kast import KInner
|
8 | 9 | from pyk.kast.inner import (
|
9 | 10 | KApply,
|
|
12 | 13 | KSort,
|
13 | 14 | KToken,
|
14 | 15 | KVariable,
|
| 16 | + Subst, |
15 | 17 | bottom_up,
|
16 | 18 | build_assoc,
|
17 | 19 | build_cons,
|
18 | 20 | top_down,
|
19 | 21 | )
|
20 | 22 | from pyk.kast.manip import abstract_term_safely, flatten_label, set_cell
|
21 | 23 | from pyk.kast.pretty import paren
|
22 |
| -from pyk.kcfg.kcfg import Step |
| 24 | +from pyk.kcfg.kcfg import KCFGExtendResult, Step |
23 | 25 | from pyk.kcfg.semantics import DefaultSemantics
|
24 | 26 | from pyk.kcfg.show import NodePrinter
|
25 | 27 | from pyk.ktool.kprove import KProve
|
|
33 | 35 | from pyk.proof.show import APRProofNodePrinter
|
34 | 36 |
|
35 | 37 | if TYPE_CHECKING:
|
36 |
| - from collections.abc import Callable, Iterable |
| 38 | + from collections.abc import Iterable |
37 | 39 | from pathlib import Path
|
38 | 40 | from typing import Final
|
39 | 41 |
|
40 |
| - from pyk.cterm import CTermSymbolic |
41 |
| - from pyk.kast.inner import KAst, Subst |
| 42 | + from pyk.kast.inner import KAst |
42 | 43 | from pyk.kast.outer import KFlatModule
|
43 | 44 | from pyk.kcfg import KCFG
|
44 |
| - from pyk.kcfg.semantics import KCFGExtendResult |
45 | 45 | from pyk.ktool.kprint import SymbolTable
|
46 | 46 | from pyk.utils import BugReport
|
47 | 47 |
|
48 | 48 | _LOGGER: Final = logging.getLogger(__name__)
|
49 | 49 |
|
| 50 | +CustomStepImpl = Callable[[Subst, CTerm, CTermSymbolic], KCFGExtendResult | None] |
| 51 | + |
50 | 52 |
|
51 | 53 | class CustomStep(NamedTuple):
|
52 | 54 | """Encapsulates a custom step definition consisting of an abstract pattern and its execution function."""
|
53 | 55 |
|
54 | 56 | pattern: KSequence
|
55 |
| - exec_fn: Callable[[Subst, CTerm, CTermSymbolic], KCFGExtendResult | None] |
| 57 | + exec_fn: CustomStepImpl |
56 | 58 |
|
57 | 59 | def check_pattern_match(self, cterm: CTerm) -> bool:
|
58 | 60 | return self.pattern.match(cterm.cell('K_CELL')) is not None
|
|
0 commit comments