Move pyk.prelude into pyk.kast (#4803)

* Move `pyk.prelude` into `pyk.kast`
* Eliminate circularity between `pyk.kast.outer`, `pyk.kast.manip` and
`pyk.kast.prelude`

---------

Co-authored-by: Everett Hildenbrandt <[email protected]>

Author: tothtamas28

pyk/src/pyk/__main__.py

@@ -29,6 +29,8 @@
     split_config_and_constraints,
 )
 from .kast.outer import KFlatModule, read_kast_definition
+from .kast.prelude.k import GENERATED_TOP_CELL
+from .kast.prelude.ml import is_top, mlAnd, mlOr
 from .kast.pretty import PrettyPrinter
 from .kast.utils import parse_outer
 from .kcfg import KCFGExplore
@@ -40,8 +42,6 @@
 from .ktool.kprove import KProve
 from .ktool.krun import KRun
 from .ktool.prove_rpc import ProveRpc
-from .prelude.k import GENERATED_TOP_CELL
-from .prelude.ml import is_top, mlAnd, mlOr
 from .proof.reachability import APRFailureInfo, APRProof
 from .proof.show import APRProofNodePrinter, APRProofShow
 from .utils import check_file_path, ensure_dir_path, exit_with_process_error

pyk/src/pyk/cterm/cterm.py

@@ -21,9 +21,9 @@
     split_config_and_constraints,
     split_config_from,
 )
-from ..prelude.k import GENERATED_TOP_CELL, K
-from ..prelude.kbool import andBool, orBool
-from ..prelude.ml import is_bottom, is_top, mlAnd, mlBottom, mlEquals, mlEqualsTrue, mlImplies, mlTop
+from ..kast.prelude.k import GENERATED_TOP_CELL, K
+from ..kast.prelude.kbool import andBool, orBool
+from ..kast.prelude.ml import is_bottom, is_top, mlAnd, mlBottom, mlEquals, mlEqualsTrue, mlImplies, mlTop
 from ..utils import not_none, unique
 
 if TYPE_CHECKING:

pyk/src/pyk/cterm/symbolic.py

@@ -8,6 +8,8 @@
 from ..cterm import CSubst, CTerm
 from ..kast.inner import KApply, KLabel, KRewrite, KToken, KVariable, Subst
 from ..kast.manip import flatten_label, is_spurious_constraint, sort_ac_collections
+from ..kast.prelude.k import GENERATED_TOP_CELL, K_ITEM
+from ..kast.prelude.ml import mlAnd
 from ..kast.pretty import PrettyPrinter
 from ..konvert import kast_to_kore, kflatmodule_to_kore, kore_to_kast
 from ..kore.rpc import (
@@ -21,8 +23,6 @@
     UnsatResult,
     kore_server,
 )
-from ..prelude.k import GENERATED_TOP_CELL, K_ITEM
-from ..prelude.ml import mlAnd
 from ..utils import not_none
 
 if TYPE_CHECKING:

pyk/src/pyk/kast/formatter.py

@@ -2,7 +2,7 @@
 
 from typing import TYPE_CHECKING
 
-from ..prelude.k import K_ITEM
+from ..kast.prelude.k import K_ITEM
 from ..utils import intersperse
 from .att import Atts, Format, KAtt
 from .inner import KApply, KToken, KVariable, bottom_up

pyk/src/pyk/kast/inner.py

@@ -738,8 +738,6 @@ def unapply(self, term: KInner) -> KInner:
     @staticmethod
     def from_pred(pred: KInner) -> Subst:
         """Given a generic matching logic predicate, attempt to extract a `Subst` from it."""
-        from .manip import flatten_label
-
         subst: dict[str, KInner] = {}
         for conjunct in flatten_label('#And', pred):
             match conjunct:

pyk/src/pyk/kast/manip.py

@@ -4,9 +4,9 @@
 from collections import Counter
 from typing import TYPE_CHECKING
 
-from ..prelude.k import DOTS, GENERATED_TOP_CELL
-from ..prelude.kbool import FALSE, TRUE, andBool, impliesBool, notBool, orBool
-from ..prelude.ml import is_top, mlAnd, mlBottom, mlEquals, mlEqualsTrue, mlImplies, mlOr, mlTop
+from ..kast.prelude.k import DOTS, GENERATED_TOP_CELL
+from ..kast.prelude.kbool import FALSE, TRUE, andBool, impliesBool, notBool, orBool
+from ..kast.prelude.ml import is_top, mlAnd, mlBottom, mlEquals, mlEqualsTrue, mlImplies, mlOr, mlTop
 from ..utils import find_common_items, hash_str, unique
 from .att import EMPTY_ATT, Atts, KAtt, WithKAtt
 from .inner import (

pyk/src/pyk/kast/outer.py

@@ -13,8 +13,6 @@
 from itertools import pairwise, product
 from typing import TYPE_CHECKING, final, overload
 
-from ..prelude.kbool import TRUE
-from ..prelude.ml import ML_QUANTIFIERS
 from ..utils import FrozenDict, POSet, filter_none, not_none, single, unique
 from .att import EMPTY_ATT, Atts, Format, KAst, KAtt, WithKAtt
 from .inner import (
@@ -45,6 +43,10 @@
 _LOGGER: Final = logging.getLogger(__name__)
 
 
+_BOOL: Final = KSort('Bool')
+_TRUE: Final = KToken('true', _BOOL)
+
+
 class KOuter(KAst):
     """Represents K definitions in KAST format.
 
@@ -628,7 +630,7 @@ class KRule(KRuleLike):
     ensures: KInner
     att: KAtt
 
-    def __init__(self, body: KInner, requires: KInner = TRUE, ensures: KInner = TRUE, att: KAtt = EMPTY_ATT):
+    def __init__(self, body: KInner, requires: KInner = _TRUE, ensures: KInner = _TRUE, att: KAtt = EMPTY_ATT):
         object.__setattr__(self, 'body', body)
         object.__setattr__(self, 'requires', requires)
         object.__setattr__(self, 'ensures', ensures)
@@ -638,8 +640,8 @@ def __init__(self, body: KInner, requires: KInner = TRUE, ensures: KInner = TRUE
     def _from_dict(cls: type[KRule], d: Mapping[str, Any]) -> KRule:
         return KRule(
             body=KInner.from_dict(d['body']),
-            requires=KInner.from_dict(d['requires']) if d.get('requires') else TRUE,
-            ensures=KInner.from_dict(d['ensures']) if d.get('ensures') else TRUE,
+            requires=KInner.from_dict(d['requires']) if d.get('requires') else _TRUE,
+            ensures=KInner.from_dict(d['ensures']) if d.get('ensures') else _TRUE,
             att=KAtt.from_dict(d['att']) if d.get('att') else EMPTY_ATT,
         )
 
@@ -684,7 +686,7 @@ class KClaim(KRuleLike):
     ensures: KInner
     att: KAtt
 
-    def __init__(self, body: KInner, requires: KInner = TRUE, ensures: KInner = TRUE, att: KAtt = EMPTY_ATT):
+    def __init__(self, body: KInner, requires: KInner = _TRUE, ensures: KInner = _TRUE, att: KAtt = EMPTY_ATT):
         object.__setattr__(self, 'body', body)
         object.__setattr__(self, 'requires', requires)
         object.__setattr__(self, 'ensures', ensures)
@@ -694,8 +696,8 @@ def __init__(self, body: KInner, requires: KInner = TRUE, ensures: KInner = TRUE
     def _from_dict(cls: type[KClaim], d: Mapping[str, Any]) -> KClaim:
         return KClaim(
             body=KInner.from_dict(d['body']),
-            requires=KInner.from_dict(d['requires']) if d.get('requires') else TRUE,
-            ensures=KInner.from_dict(d['ensures']) if d.get('ensures') else TRUE,
+            requires=KInner.from_dict(d['requires']) if d.get('requires') else _TRUE,
+            ensures=KInner.from_dict(d['ensures']) if d.get('ensures') else _TRUE,
             att=KAtt.from_dict(d['att']) if d.get('att') else EMPTY_ATT,
         )
 
@@ -753,7 +755,7 @@ class KContext(KSentence):
     requires: KInner
     att: KAtt
 
-    def __init__(self, body: KInner, requires: KInner = TRUE, att: KAtt = EMPTY_ATT):
+    def __init__(self, body: KInner, requires: KInner = _TRUE, att: KAtt = EMPTY_ATT):
         object.__setattr__(self, 'body', body)
         object.__setattr__(self, 'requires', requires)
         object.__setattr__(self, 'att', att)
@@ -762,7 +764,7 @@ def __init__(self, body: KInner, requires: KInner = TRUE, att: KAtt = EMPTY_ATT)
     def _from_dict(cls: type[KContext], d: Mapping[str, Any]) -> KContext:
         return KContext(
             body=KInner.from_dict(d['body']),
-            requires=KInner.from_dict(d['requires']) if d.get('requires') else TRUE,
+            requires=KInner.from_dict(d['requires']) if d.get('requires') else _TRUE,
             att=KAtt.from_dict(d['att']) if d.get('att') else EMPTY_ATT,
         )
 
@@ -1400,6 +1402,8 @@ def _add_ksequence_under_k_productions(_kast: KInner) -> KInner:
 
     def sort_vars(self, kast: KInner, sort: KSort | None = None) -> KInner:
         """Return the original term with all the variables having the sorts added or specialized, failing if recieving conflicting sorts for a given variable."""
+        ml_quantifiers = {'#Exists', '#Forall'}
+
         if type(kast) is KVariable and kast.sort is None and sort is not None:
             return kast.let(sort=sort)
 
@@ -1422,7 +1426,7 @@ def merge_variables(
             if isinstance(term, KVariable):
                 result[term.name].append(term)
             elif isinstance(term, KApply):
-                if term.label.name in ML_QUANTIFIERS:
+                if term.label.name in ml_quantifiers:
                     var = get_quantifier_variable(term)
                     result[var.name].append(var)
             return result
@@ -1444,7 +1448,7 @@ def transform(
             occurrences = merge_variables(term, child_variables)
 
             if isinstance(term, KApply):
-                if term.label.name in ML_QUANTIFIERS:
+                if term.label.name in ml_quantifiers:
                     var = get_quantifier_variable(term)
                     subst: dict[str, KVariable] = {}
                     add_var_to_subst(var.name, occurrences[var.name], subst)

pyk/src/pyk/prelude/__init__.py renamed to pyk/src/pyk/kast/prelude/__init__.py

@@ -1,7 +1,7 @@
 from typing import Final
 
-from ..dequote import bytes_decode, bytes_encode, dequote_bytes, enquote_bytes
-from ..kast.inner import KSort, KToken
+from ...dequote import bytes_decode, bytes_encode, dequote_bytes, enquote_bytes
+from ..inner import KSort, KToken
 
 BYTES: Final = KSort('Bytes')
 

pyk/src/pyk/prelude/bytes.py renamed to pyk/src/pyk/kast/prelude/bytes.py

@@ -2,13 +2,13 @@
 
 from typing import TYPE_CHECKING
 
-from ..kast.inner import KApply, KLabel, KSort, build_assoc
+from ..inner import KApply, KLabel, KSort, build_assoc
 
 if TYPE_CHECKING:
     from collections.abc import Iterable
     from typing import Final
 
-    from ..kast import KInner
+    from .. import KInner
 
 SET: Final = KSort('Set')
 LIST: Final = KSort('List')

pyk/src/pyk/prelude/collections.py renamed to pyk/src/pyk/kast/prelude/collections.py

@@ -2,12 +2,12 @@
 
 from typing import TYPE_CHECKING
 
-from ..kast.inner import KApply, KLabel, KSort, KToken
+from ..inner import KApply, KLabel, KSort, KToken
 
 if TYPE_CHECKING:
     from typing import Final
 
-    from ..kast import KInner
+    from .. import KInner
 
 
 K: Final = KSort('K')

pyk/src/pyk/prelude/k.py renamed to pyk/src/pyk/kast/prelude/k.py

@@ -2,17 +2,19 @@
 
 from typing import TYPE_CHECKING
 
-from ..kast.inner import KApply, KLabel, KSort, KToken, build_assoc
-from ..utils import unique
+from ...utils import unique
+from ..inner import KApply, KLabel, KToken, build_assoc
+from ..outer import _BOOL, _TRUE
 
 if TYPE_CHECKING:
     from collections.abc import Iterable
     from typing import Final
 
-    from ..kast import KInner
+    from .. import KInner
 
-BOOL: Final = KSort('Bool')
-TRUE: Final = KToken('true', BOOL)
+
+BOOL: Final = _BOOL
+TRUE: Final = _TRUE
 FALSE: Final = KToken('false', BOOL)
 
 

pyk/src/pyk/prelude/kbool.py renamed to pyk/src/pyk/kast/prelude/kbool.py

@@ -2,12 +2,12 @@
 
 from typing import TYPE_CHECKING
 
-from ..kast.inner import KApply, KSort, KToken
+from ..inner import KApply, KSort, KToken
 
 if TYPE_CHECKING:
     from typing import Final
 
-    from ..kast import KInner
+    from .. import KInner
 
 INT: Final = KSort('Int')
 

pyk/src/pyk/prelude/kint.py renamed to pyk/src/pyk/kast/prelude/kint.py

@@ -2,24 +2,16 @@
 
 from typing import TYPE_CHECKING
 
-from pyk.utils import single
-
-from ..kast.inner import KApply, KLabel, build_assoc, flatten_label
+from ...utils import single
+from ..inner import KApply, KLabel, build_assoc, flatten_label
 from .k import GENERATED_TOP_CELL, K_ITEM, K
 from .kbool import BOOL, FALSE, TRUE
 
 if TYPE_CHECKING:
     from collections.abc import Iterable
-    from typing import Final
-
-    from ..kast import KInner
-    from ..kast.inner import KSort, KVariable
-
 
-ML_QUANTIFIERS: Final = {
-    '#Exists',
-    '#Forall',
-}
+    from .. import KInner
+    from ..inner import KSort, KVariable
 
 
 def _is_top(term: KInner) -> bool:

pyk/src/pyk/prelude/ml.py renamed to pyk/src/pyk/kast/prelude/ml.py

@@ -1,7 +1,7 @@
 from typing import Final
 
-from ..dequote import dequote_string, enquote_string
-from ..kast.inner import KSort, KToken
+from ...dequote import dequote_string, enquote_string
+from ..inner import KSort, KToken
 
 STRING: Final = KSort('String')
 

pyk/src/pyk/prelude/string.py renamed to pyk/src/pyk/kast/prelude/string.py

@@ -8,7 +8,7 @@
 from .string import stringToken
 
 if TYPE_CHECKING:
-    from ..kast.inner import KToken
+    from ..inner import KToken
 
 
 def token(x: bool | int | str | bytes) -> KToken:

pyk/src/pyk/prelude/utils.py renamed to pyk/src/pyk/kast/prelude/utils.py

@@ -5,7 +5,7 @@
 from functools import cached_property
 from typing import TYPE_CHECKING
 
-from ..prelude.kbool import TRUE
+from ..kast.prelude.kbool import TRUE
 from .att import Atts, KAtt
 from .inner import KApply, KAs, KInner, KLabel, KRewrite, KSequence, KSort, KToken, KVariable
 from .manip import flatten_label, sort_ac_collections, undo_aliases

pyk/src/pyk/kast/pretty.py

@@ -13,9 +13,9 @@
     push_down_rewrites,
     replace_rewrites_with_implies,
 )
+from ..kast.prelude.ml import is_top, mlAnd
 from ..kast.pretty import PrettyPrinter
 from ..kore.rpc import LogRewrite, RewriteSuccess
-from ..prelude.ml import is_top, mlAnd
 from ..utils import not_none, shorten_hashes, single, unique
 from .kcfg import KCFG, Abstract, Branch, NDBranch, Step, Stuck, Vacuous
 from .semantics import DefaultSemantics

pyk/src/pyk/kcfg/explore.py

@@ -21,7 +21,7 @@
     sort_ac_collections,
 )
 from ..kast.outer import KFlatModule
-from ..prelude.kbool import andBool
+from ..kast.prelude.kbool import andBool
 from ..utils import ensure_dir_path, not_none
 
 if TYPE_CHECKING:

pyk/src/pyk/kcfg/kcfg.py

@@ -17,8 +17,8 @@
     sort_ac_collections,
 )
 from ..kast.outer import KRule
-from ..prelude.k import DOTS
-from ..prelude.ml import mlAnd
+from ..kast.prelude.k import DOTS
+from ..kast.prelude.ml import mlAnd
 from ..utils import add_indent, ensure_dir_path
 from .kcfg import KCFG
 

pyk/src/pyk/kcfg/show.py

@@ -13,7 +13,7 @@
 from ..cterm import CTerm
 from ..kast.inner import KApply, KRewrite
 from ..kast.manip import flatten_label, minimize_term, push_down_rewrites
-from ..prelude.kbool import TRUE
+from ..kast.prelude.kbool import TRUE
 from ..utils import ROOT, shorten_hashes, single
 from .kcfg import KCFG
 from .show import KCFGShow

pyk/src/pyk/kcfg/tui.py

@@ -8,6 +8,11 @@
 from ..kast.inner import KApply, KLabel, KRewrite, KSequence, KSort, KToken, KVariable, top_down
 from ..kast.manip import bool_to_ml_pred, extract_lhs, extract_rhs, flatten_label, ml_pred_to_bool, var_occurrences
 from ..kast.outer import KRule
+from ..kast.prelude.bytes import BYTES, pretty_bytes_str
+from ..kast.prelude.k import K_ITEM, K, inj
+from ..kast.prelude.kbool import BOOL, TRUE, andBool
+from ..kast.prelude.ml import mlAnd
+from ..kast.prelude.string import STRING, pretty_string
 from ..kore.prelude import BOOL as KORE_BOOL
 from ..kore.prelude import SORT_K
 from ..kore.prelude import TRUE as KORE_TRUE
@@ -29,11 +34,6 @@
     String,
     Top,
 )
-from ..prelude.bytes import BYTES, pretty_bytes_str
-from ..prelude.k import K_ITEM, K, inj
-from ..prelude.kbool import BOOL, TRUE, andBool
-from ..prelude.ml import mlAnd
-from ..prelude.string import STRING, pretty_string
 from ._utils import munge
 
 if TYPE_CHECKING: