Remove old workaround (#4485)

In 7ba37fb (8 years ago), we disabled cell collection syntax productions when parsing rules because of OOMs in the compiler. We haven't needed to use this syntax since then, but @PetarMax recently identified a lemma that required being able to do so. --------- Co-authored-by: Petar Maksimović <PetarMax@users.noreply.github.com>
runtimeverification · Jun 27, 2024 · bf1e5e7 · bf1e5e7
1 parent 137574d
commit bf1e5e7
Show file tree

Hide file tree

Showing 10 changed files with 111 additions and 7 deletions.
diff --git a/k-distribution/tests/regression-new/star-multiplicity-concat/1.test b/k-distribution/tests/regression-new/star-multiplicity-concat/1.test
@@ -0,0 +1 @@
+#putCells
diff --git a/k-distribution/tests/regression-new/star-multiplicity-concat/1.test.out b/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>
diff --git a/k-distribution/tests/regression-new/star-multiplicity-concat/Makefile b/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
diff --git a/k-distribution/tests/regression-new/star-multiplicity-concat/test.k b/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
diff --git a/k-frontend/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java b/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

diff --git a/pyk/regression-new/include/ktest.mak b/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)

diff --git a/pyk/regression-new/star-multiplicity-concat/1.test b/pyk/regression-new/star-multiplicity-concat/1.test
@@ -0,0 +1 @@
+#putCells
diff --git a/pyk/regression-new/star-multiplicity-concat/1.test.out b/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>
diff --git a/pyk/regression-new/star-multiplicity-concat/Makefile b/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
diff --git a/pyk/regression-new/star-multiplicity-concat/test.k b/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