Merge branch 'develop' into refactor-assoc

.github/workflows/release.yml

@@ -440,7 +440,16 @@ jobs:
           packages-dir: pyk/dist
           user: __token__
           password: ${{ secrets.PYPI_TOKEN }}
-
+      - name: Wait for PyPi to publish Pyk
+        run: |
+          while true; do
+            VERSION=$(cat package/version)
+            if curl --fail --silent --location --head "https://pypi.org/project/kframework/$VERSION"; then
+              break
+            fi
+            sleep 10
+          done
+  
   notify-dependents:
     name: 'Notify Dependents'
     runs-on: ubuntu-latest

deps/haskell-backend_release

@@ -1 +1 @@
-v0.1.19
+v0.1.25

deps/llvm-backend_release

@@ -1 +1 @@
-0.1.51
+0.1.52

flake.nix

@@ -1,11 +1,11 @@
 {
   description = "K Framework";
   inputs = {
-    haskell-backend.url = "github:runtimeverification/haskell-backend/v0.1.19";
+    haskell-backend.url = "github:runtimeverification/haskell-backend/v0.1.25";
     nixpkgs.follows = "llvm-backend/nixpkgs";
     flake-utils.url = "github:numtide/flake-utils";
     llvm-backend = {
-      url = "github:runtimeverification/llvm-backend/v0.1.51";
+      url = "github:runtimeverification/llvm-backend/v0.1.52";
       inputs.utils.follows = "flake-utils";
     };
     rv-utils.url = "github:runtimeverification/rv-nix-tools";

k-distribution/include/kframework/builtin/domains.md

@@ -488,7 +488,7 @@ module RANGEMAP
 ### Range, bounded inclusively below and exclusively above.
 
 ```k
-  syntax Range ::= "[" KItem "," KItem ")"    [klabel(Rangemap:Range), symbol]
+  syntax Range ::= "[" KItem "," KItem ")"    [klabel(RangeMap:Range), symbol]
 
   syntax RangeMap [hook(RANGEMAP.RangeMap)]
 ```

pyk/src/pyk/kast/manip.py

@@ -84,7 +84,9 @@ def sort_assoc_label(label: str, kast: KInner) -> KInner:
 
 def sort_ac_collections(kast: KInner) -> KInner:
     def _sort_ac_collections(_kast: KInner) -> KInner:
-        if type(_kast) is KApply and (_kast.label.name in {'_Set_', '_Map_'} or _kast.label.name.endswith('CellMap_')):
+        if type(_kast) is KApply and (
+            _kast.label.name in {'_Set_', '_Map_', '_RangeMap_'} or _kast.label.name.endswith('CellMap_')
+        ):
             return sort_assoc_label(_kast.label.name, _kast)
         return _kast
 

pyk/src/pyk/kast/outer.py

@@ -859,7 +859,16 @@ def cell_collection_productions(self) -> tuple[KProduction, ...]:
     def _is_function(prod: KProduction) -> bool:
         def is_not_actually_function(label: str) -> bool:
             is_cell_map_constructor = label.endswith('CellMapItem') or label.endswith('CellMap_')
-            is_builtin_data_constructor = label in {'_Set_', '_List_', '_Map_', 'SetItem', 'ListItem', '_|->_'}
+            is_builtin_data_constructor = label in {
+                '_Set_',
+                '_List_',
+                '_Map_',
+                '_RangeMap_',
+                'SetItem',
+                'ListItem',
+                '_|->_',
+                '_r|->_',
+            }
             return is_cell_map_constructor or is_builtin_data_constructor
 
         return (Atts.FUNCTION in prod.att or Atts.FUNCTIONAL in prod.att) and not (

pyk/src/pyk/kore/match.py

@@ -86,6 +86,28 @@ def match_map(pattern: Pattern, *, cell: str | None = None) -> tuple[tuple[Patte
     return tuple(entries)
 
 
+def match_rangemap(pattern: Pattern) -> tuple[tuple[tuple[Pattern, Pattern], Pattern], ...]:
+    stop_symbol = "Lbl'Stop'RangeMap"
+    cons_symbol = "Lbl'Unds'RangeMap'Unds'"
+    item_symbol = "Lbl'Unds'r'Pipe'-'-GT-Unds'"
+
+    if type(pattern) is App:
+        match_app(pattern, stop_symbol)
+        return ()
+
+    assoc = match_left_assoc(pattern)
+    cons = match_app(assoc.app, cons_symbol)
+    items = (match_app(arg, item_symbol) for arg in cons.args)
+    entries = ((_match_range(item.args[0]), item.args[1]) for item in items)
+    return tuple(entries)
+
+
+def _match_range(pattern: Pattern) -> tuple[Pattern, Pattern]:
+    range_symbol = "LblRangeMap'Coln'Range"
+    range = match_app(pattern, range_symbol)
+    return (range.args[0], range.args[1])
+
+
 def kore_bool(pattern: Pattern) -> bool:
     dv = match_dv(pattern, BOOL)
     match dv.value.value:
@@ -253,6 +275,16 @@ def res(pattern: Pattern) -> tuple[tuple[K, V], ...]:
     return res
 
 
+def kore_rangemap_of(
+    key: Callable[[Pattern], K],
+    value: Callable[[Pattern], V],
+) -> Callable[[Pattern], tuple[tuple[tuple[K, K], V], ...]]:
+    def res(pattern: Pattern) -> tuple[tuple[tuple[K, K], V], ...]:
+        return tuple(((key(k[0]), key(k[1])), value(v)) for k, v in match_rangemap(pattern))
+
+    return res
+
+
 def case_symbol(
     *cases: tuple[str, Callable[[App], T]],
     default: Callable[[App], T] | None = None,

pyk/src/pyk/kore/prelude.py

@@ -250,6 +250,24 @@ def map_pattern(*args: tuple[Pattern, Pattern], cell: str | None = None) -> Patt
     return LeftAssoc(cons_symbol, args=(App(item_symbol, args=arg) for arg in args))
 
 
+STOP_RANGEMAP: Final = App("Lbl'Stop'RangeMap")
+LBL_RANGEMAP: Final = SymbolId("Lbl'Unds'RangeMap'Unds'")
+LBL_RANGEMAP_ITEM: Final = SymbolId("Lbl'Unds'r'Pipe'-'-GT-Unds'")
+LBL_RANGEMAP_RANGE: Final = SymbolId("LblRangeMap'Coln'Range")
+
+
+def rangemap_pattern(*args: tuple[tuple[Pattern, Pattern], Pattern]) -> Pattern:
+    if not args:
+        return STOP_RANGEMAP
+
+    return LeftAssoc(
+        App(
+            LBL_RANGEMAP,
+            args=(App(LBL_RANGEMAP_ITEM, args=(App(LBL_RANGEMAP_RANGE, args=arg[0]), arg[1])) for arg in args),
+        )
+    )
+
+
 # ----
 # JSON
 # ----