Skip to content

Commit a7a916a

Browse files
committed
refactor a better way for as_rules
1 parent ae7ad30 commit a7a916a

File tree

1 file changed

+7
-2
lines changed

1 file changed

+7
-2
lines changed

pyk/src/pyk/proof/reachability.py

Lines changed: 7 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,7 @@
2626
from pathlib import Path
2727
from typing import Any, Final, TypeVar
2828

29-
from ..kast.outer import KClaim, KDefinition, KFlatModuleList
29+
from ..kast.outer import KClaim, KDefinition, KFlatModuleList, KRuleLike
3030
from ..kcfg import KCFGExplore
3131
from ..kcfg.explore import KCFGExtendResult
3232
from ..kcfg.kcfg import CSubst, NodeIdLike
@@ -444,7 +444,12 @@ def as_rules(self, priority: int = 20, direct_rule: bool = False) -> list[KRule]
444444
or (self.admitted and not self.kcfg.predecessors(self.target))
445445
):
446446
return [self.as_rule(priority=priority)]
447-
return [rule for rule in self.kcfg.to_rules(self.rule_id, priority=priority) if isinstance(rule, KRule)]
447+
448+
def _return_rule(r: KRuleLike) -> KRule:
449+
assert isinstance(r, KRule)
450+
return r
451+
452+
return [_return_rule(rule) for rule in self.kcfg.to_rules(self.rule_id, priority=priority)]
448453

449454
def as_rule(self, priority: int = 20) -> KRule:
450455
_edge = KCFG.Edge(self.kcfg.node(self.init), self.kcfg.node(self.target), depth=0, rules=())

0 commit comments

Comments
 (0)