Merge branch 'develop' into follows-pruning

.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,9 +1,9 @@
 {
   description = "K Framework";
   inputs = {
-    llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.51";
+    llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.52";
     haskell-backend = {
-      url = "github:runtimeverification/haskell-backend/v0.1.19";
+      url = "github:runtimeverification/haskell-backend/v0.1.25";
       inputs.rv-utils.follows = "llvm-backend/rv-utils";
     };
 

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)]
 ```

k-distribution/tests/regression-new/star-multiplicity-concat/1.test

@@ -0,0 +1 @@
+#putCells

k-distribution/tests/regression-new/star-multiplicity-concat/1.test.out

@@ -0,0 +1,22 @@
+<generatedTop>
+  <k>
+    <cell>
+      <num>
+        0
+      </num>
+      <data>
+        0
+      </data>
+    </cell> <cell>
+      <num>
+        1
+      </num>
+      <data>
+        1
+      </data>
+    </cell> ~> .K
+  </k>
+  <cells>
+    .CellCellMap
+  </cells>
+</generatedTop>

k-distribution/tests/regression-new/star-multiplicity-concat/Makefile

@@ -0,0 +1,7 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_BACKEND=llvm
+KOMPILE_FLAGS=--syntax-module TEST
+
+include ../../../include/kframework/ktest.mak

k-distribution/tests/regression-new/star-multiplicity-concat/test.k

@@ -0,0 +1,24 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+module TEST
+  imports INT
+
+  configuration
+    <k> $PGM:K </k>
+    <cells>
+      <cell multiplicity="*" type="Map">
+        <num> 0 </num>
+        <data> 0 </data>
+      </cell>
+    </cells>
+
+    syntax CellCellMap ::= #makeCell( Int, Int ) [function]
+ // ----------------------------
+    rule #makeCell( X, Y ) => CellCellMapItem(
+      <num> X </num>,
+      <cell> <num> X </num> <data> Y </data> </cell>
+    )
+
+    syntax KItem ::= "#putCells"
+ // ----------------------------
+    rule <k> #putCells => #makeCell(0,0) (#makeCell(1,1) .CellCellMap) </k>
+endmodule

k-frontend/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java

@@ -547,9 +547,6 @@ public static Tuple3<Module, Module, Module> getCombinedGrammarImpl(
           Stream.concat(prods.stream(), stream(mod.sentences()))
               .flatMap(
                   s -> {
-                    if (s instanceof Production && s.att().contains(Att.CELL_COLLECTION())) {
-                      return Stream.empty();
-                    }
                     if (s instanceof Production p && (s.att().contains(Att.CELL()))) {
                       // assuming that productions tagged with 'cell' start and end with terminals,
                       // and only have non-terminals in the middle

pyk/regression-new/include/ktest.mak

@@ -50,10 +50,6 @@ SOURCE_EXT?=$(or $(and $(wildcard $(DEF).k), k), $(or $(and $(wildcard $(DEF).md
 
 VERBOSITY?=
 
-ifeq ($(UNAME), Darwin)
-	KOMPILE_FLAGS+=--no-haskell-binary
-endif
-
 KOMPILE_FLAGS+=--no-exc-wrap --type-inference-mode checked $(VERBOSITY)
 KRUN_FLAGS+=$(VERBOSITY)
 KPROVE_FLAGS+=--type-inference-mode checked --failure-info $(VERBOSITY)

pyk/regression-new/star-multiplicity-concat/1.test

@@ -0,0 +1 @@
+#putCells

pyk/regression-new/star-multiplicity-concat/1.test.out

@@ -0,0 +1,25 @@
+<generatedTop>
+  <k>
+    <cell>
+      <num>
+        0
+      </num>
+      <data>
+        0
+      </data>
+    </cell> <cell>
+      <num>
+        1
+      </num>
+      <data>
+        1
+      </data>
+    </cell> ~> .K
+  </k>
+  <cells>
+    .CellCellMap
+  </cells>
+  <generatedCounter>
+    0
+  </generatedCounter>
+</generatedTop>

pyk/regression-new/star-multiplicity-concat/Makefile

@@ -0,0 +1,7 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_BACKEND=llvm
+KOMPILE_FLAGS=--syntax-module TEST
+
+include ../include/ktest.mak

pyk/regression-new/star-multiplicity-concat/test.k

@@ -0,0 +1,24 @@
+// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
+module TEST
+  imports INT
+
+  configuration
+    <k> $PGM:K </k>
+    <cells>
+      <cell multiplicity="*" type="Map">
+        <num> 0 </num>
+        <data> 0 </data>
+      </cell>
+    </cells>
+
+    syntax CellCellMap ::= #makeCell( Int, Int ) [function]
+ // ----------------------------
+    rule #makeCell( X, Y ) => CellCellMapItem(
+      <num> X </num>,
+      <cell> <num> X </num> <data> Y </data> </cell>
+    )
+
+    syntax KItem ::= "#putCells"
+ // ----------------------------
+    rule <k> #putCells => #makeCell(0,0) (#makeCell(1,1) .CellCellMap) </k>
+endmodule

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

@@ -252,6 +252,24 @@ def map_pattern(*args: tuple[Pattern, Pattern], cell: str | None = None) -> Patt
     return LeftAssoc(App(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
 # ----