From de9cb1f97086eb9411a244bdad0e25b211209295 Mon Sep 17 00:00:00 2001 From: JianhongZhao Date: Fri, 23 Aug 2024 14:28:23 +0800 Subject: [PATCH] refactor a better way for as_rules --- pyk/src/pyk/proof/reachability.py | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index e055ed48e6..9244a0c850 100644 --- a/pyk/src/pyk/proof/reachability.py +++ b/pyk/src/pyk/proof/reachability.py @@ -26,7 +26,7 @@ from pathlib import Path from typing import Any, Final, TypeVar - from ..kast.outer import KClaim, KDefinition, KFlatModuleList + from ..kast.outer import KClaim, KDefinition, KFlatModuleList, KRuleLike from ..kcfg import KCFGExplore from ..kcfg.explore import KCFGExtendResult from ..kcfg.kcfg import CSubst, NodeIdLike @@ -444,7 +444,12 @@ def as_rules(self, priority: int = 20, direct_rule: bool = False) -> list[KRule] or (self.admitted and not self.kcfg.predecessors(self.target)) ): return [self.as_rule(priority=priority)] - return [rule for rule in self.kcfg.to_rules(self.rule_id, priority=priority) if isinstance(rule, KRule)] + + def _return_rule(r: KRuleLike) -> KRule: + assert isinstance(r, KRule) + return r + + return [_return_rule(rule) for rule in self.kcfg.to_rules(self.rule_id, priority=priority)] def as_rule(self, priority: int = 20) -> KRule: _edge = KCFG.Edge(self.kcfg.node(self.init), self.kcfg.node(self.target), depth=0, rules=())