From 058b0aa59dc4908a5bf9e2e74f653948fe394795 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Fri, 29 Nov 2024 20:59:55 +0000
Subject: [PATCH] Nest function

---
 pyk/src/pyk/kore/rule.py | 45 ++++++++++++++++++++--------------------
 1 file changed, 22 insertions(+), 23 deletions(-)

diff --git a/pyk/src/pyk/kore/rule.py b/pyk/src/pyk/kore/rule.py
index f19beb1714..8fb49eb9d6 100644
--- a/pyk/src/pyk/kore/rule.py
+++ b/pyk/src/pyk/kore/rule.py
@@ -62,29 +62,28 @@ def from_axiom(axiom: Axiom) -> Rule:
 
     @staticmethod
     def extract_all(defn: Definition) -> list[Rule]:
-        return [Rule.from_axiom(axiom) for axiom in defn.axioms if Rule._is_rule(axiom)]
-
-    @staticmethod
-    def _is_rule(axiom: Axiom) -> bool:
-        if axiom == _INJ_AXIOM:
-            return False
-
-        if any(attr in axiom.attrs_by_key for attr in _SKIPPED_ATTRS):
-            return False
-
-        if 'simplification' in axiom.attrs_by_key:
-            match axiom.pattern:
-                case Implies(
-                    left=Top() | Equals(),
-                    right=Equals(
-                        left=Ceil() | Equals(),
-                        right=And(ops=(_, Top() | Equals())),
-                    ),
-                ):
-                    _LOGGER.info(fr'Skipping \ceil or \equals simplification rule: {axiom.text}')
-                    return False
-
-        return True
+        def is_rule(axiom: Axiom) -> bool:
+            if axiom == _INJ_AXIOM:
+                return False
+
+            if any(attr in axiom.attrs_by_key for attr in _SKIPPED_ATTRS):
+                return False
+
+            if 'simplification' in axiom.attrs_by_key:
+                match axiom.pattern:
+                    case Implies(
+                        left=Top() | Equals(),
+                        right=Equals(
+                            left=Ceil() | Equals(),
+                            right=And(ops=(_, Top() | Equals())),
+                        ),
+                    ):
+                        _LOGGER.info(fr'Skipping \ceil or \equals simplification rule: {axiom.text}')
+                        return False
+
+            return True
+
+        return [Rule.from_axiom(axiom) for axiom in defn.axioms if is_rule(axiom)]
 
 
 @final