Fix parsing bugs (runtimeverification#559)

dwightguth · ehildenb · commit a1acdfdb185b · 2019-06-19T10:53:37.000-05:00
* fix poly prods for KItem sort

* fix bug in rewrite priority visitor for nested rewrites in #fun

* add tests
diff --git a/k-distribution/tests/regression-new/amb-rew/Makefile b/k-distribution/tests/regression-new/amb-rew/Makefile
@@ -0,0 +1,6 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_FLAGS=-w2e
+
+include ../../../include/ktest.mak
diff --git a/k-distribution/tests/regression-new/amb-rew/test.k b/k-distribution/tests/regression-new/amb-rew/test.k
@@ -0,0 +1,16 @@
+module TEST-SYNTAX
+endmodule
+
+module TEST
+  imports TEST-SYNTAX
+  imports INT
+  imports MAP
+  imports ID
+
+syntax Type ::= "type"
+syntax Foo ::= foo(Map)
+
+rule foo(1 |-> 0 => 1 |-> #fun(T::Type => T |-> T)(type))
+
+
+endmodule
diff --git a/k-distribution/tests/regression-new/poly-kitem/Makefile b/k-distribution/tests/regression-new/poly-kitem/Makefile
@@ -0,0 +1,5 @@
+DEF=test
+EXT=test
+TESTDIR=.
+
+include ../../../include/ktest.mak
diff --git a/k-distribution/tests/regression-new/poly-kitem/test.k b/k-distribution/tests/regression-new/poly-kitem/test.k
@@ -0,0 +1,6 @@
+module TEST
+
+syntax KItem ::= foo(KItem)
+
+rule foo((foo(G:KItem) => foo(foo(G))))
+endmodule
diff --git a/kernel/src/main/java/org/kframework/parser/concrete2kore/disambiguation/CorrectRewritePriorityVisitor.java b/kernel/src/main/java/org/kframework/parser/concrete2kore/disambiguation/CorrectRewritePriorityVisitor.java
@@ -47,7 +47,7 @@ public Either<java.util.Set<ParseFailedException>, Term> apply(Ambiguity amb) {
         if (rewrites.size() == 0 || rewrites.size() == amb.items().size())
             return super.apply(amb);
         if (rewrites.size() == 1)
-            return Right.apply(rewrites.head());
+            return apply(rewrites.head());
         return super.apply(Ambiguity.apply(mutable(rewrites)));
     }
 
diff --git a/kernel/src/main/java/org/kframework/parser/concrete2kore/generator/RuleGrammarGenerator.java b/kernel/src/main/java/org/kframework/parser/concrete2kore/generator/RuleGrammarGenerator.java
@@ -251,7 +251,9 @@ public static ParseInModule getCombinedGrammar(Module mod, boolean strict, boole
                             }
                         }
                     }
-                    prods.add(Production(p.klabel(), returnSort, immutable(pis), p.att().add(Constants.ORIGINAL_PRD, Production.class, p)));
+                    if (!(pis.size() == 1 && pis.get(0) instanceof NonTerminal && ((NonTerminal)pis.get(0)).sort().equals(returnSort))) {
+                        prods.add(Production(p.klabel(), returnSort, immutable(pis), p.att().add(Constants.ORIGINAL_PRD, Production.class, p)));
+                    }
                 }
             }
         }
@@ -401,7 +403,7 @@ public static List<Set<Integer>> computePositions(String p) {
 
     private static List<List<Sort>> makeAllSortTuples(int size, Module mod) {
         List<List<Sort>> res = new ArrayList<>();
-        List<Sort> allSorts = stream(mod.definedSorts()).filter(s -> !isParserSort(s)).collect(Collectors.toList());
+        List<Sort> allSorts = stream(mod.definedSorts()).filter(s -> !isParserSort(s) || s.equals(Sorts.KItem())).collect(Collectors.toList());
         makeAllSortTuples(size, size, allSorts, res, new int[size]);
         return res;
     }

Original file line number	Diff line number	Diff line change
`@@ -47,7 +47,7 @@ public Either<java.util.Set<ParseFailedException>, Term> apply(Ambiguity amb) {`
`47`	`47`	`if (rewrites.size() == 0 \|\| rewrites.size() == amb.items().size())`
`48`	`48`	`return super.apply(amb);`
`49`	`49`	`if (rewrites.size() == 1)`
`50`		`- return Right.apply(rewrites.head());`
	`50`	`+ return apply(rewrites.head());`
`51`	`51`	`return super.apply(Ambiguity.apply(mutable(rewrites)));`
`52`	`52`	`}`
`53`	`53`
Original file line number	Diff line number	Diff line change
`@@ -251,7 +251,9 @@ public static ParseInModule getCombinedGrammar(Module mod, boolean strict, boole`
`251`	`251`	`}`
`252`	`252`	`}`
`253`	`253`	`}`
`254`		`- prods.add(Production(p.klabel(), returnSort, immutable(pis), p.att().add(Constants.ORIGINAL_PRD, Production.class, p)));`
	`254`	`+ if (!(pis.size() == 1 && pis.get(0) instanceof NonTerminal && ((NonTerminal)pis.get(0)).sort().equals(returnSort))) {`
	`255`	`+ prods.add(Production(p.klabel(), returnSort, immutable(pis), p.att().add(Constants.ORIGINAL_PRD, Production.class, p)));`
	`256`	`+ }`
`255`	`257`	`}`
`256`	`258`	`}`
`257`	`259`	`}`
`@@ -401,7 +403,7 @@ public static List<Set<Integer>> computePositions(String p) {`
`401`	`403`
`402`	`404`	`private static List<List<Sort>> makeAllSortTuples(int size, Module mod) {`
`403`	`405`	`List<List<Sort>> res = new ArrayList<>();`
`404`		`- List<Sort> allSorts = stream(mod.definedSorts()).filter(s -> !isParserSort(s)).collect(Collectors.toList());`
	`406`	`+ List<Sort> allSorts = stream(mod.definedSorts()).filter(s -> !isParserSort(s) \|\| s.equals(Sorts.KItem())).collect(Collectors.toList());`
`405`	`407`	`makeAllSortTuples(size, size, allSorts, res, new int[size]);`
`406`	`408`	`return res;`
`407`	`409`	`}`