Fixes for anywhere rules and strategies (runtimeverification#216)

dwightguth · web-flow · commit b61559a1dcd9 · 2018-12-11T10:38:29.000-06:00
* remove StrategyApply and StrategyApplied sorts

* support anywhere rules

* fix parse error
diff --git a/k-distribution/include/builtin/domains.k b/k-distribution/include/builtin/domains.k
@@ -1299,11 +1299,9 @@ module STRATEGY
 
     syntax Strategy ::= #STUCK() [symbol]
 
-    syntax StrategyApply ::= "^" #RuleTag                      [klabel(#applyRule), symbol]
+    syntax Strategy ::= "^" #RuleTag                      [klabel(#applyRule), symbol]
 
-    syntax StrategyApplied ::= "~" #RuleTag                    [klabel(#appliedRule), symbol]
-
-    syntax Strategy ::= StrategyApply | StrategyApplied
+    syntax Strategy ::= "~" #RuleTag                    [klabel(#appliedRule), symbol]
 
     configuration <s> $STRATEGY:K  </s>
 endmodule
@@ -1360,8 +1358,8 @@ module BASIC-STRATEGY
 
     rule <s> true ~> #FROZEN(CONFIGURATION:K) => true ...</s>
 
-//    rule <s> #STUCK ~> X:StrategyApply => false ...</s>
-    rule <s> X:StrategyApplied => true ...</s>
+//    rule <s> #STUCK ~> #applyRule(_) => false ...</s>
+    rule <s> #appliedRule(_) => true ...</s>
 
     rule <s> A:Strategy ; B:Strategy => A ~> #SHOLE ; B ...</s> when notBool(isBool(A))
 
@@ -1372,7 +1370,7 @@ module BASIC-STRATEGY
     rule <s> false ; B:Strategy => false ...</s>
 
 // the second rule is stupid -- just made to sidestep what is likely a KSEQ normalization bug
-    rule <s> #STUCK() ~> A:StrategyApply => false ...</s>
+    rule <s> #STUCK() ~> #applyRule(_) => false ...</s>
     rule <s> #STUCK() ~> false => false ...</s>
 
 endmodule
diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
@@ -141,7 +141,7 @@ public String convert(boolean heatCoolEq) {
             if (left instanceof KApply) {
                 KApply kapp = (KApply) left;
                 Production prod = production(kapp);
-                if (prod.att().contains(Attribute.FUNCTION_KEY)) {
+                if (prod.att().contains(Attribute.FUNCTION_KEY) || rule.att().contains(Attribute.ANYWHERE_KEY)) {
                     functionRules.put(kapp.klabel(), rule);
                 }
             }
@@ -571,7 +571,7 @@ private void convertRule(Rule rule, boolean heatCoolEq, Sort topCellSort, Map<St
                     .map(i -> (NonTerminal) i)
                     .map(NonTerminal::sort).collect(Collectors.toList());
             productionLabel = production.klabel().get();
-            if (isFunction(prod)) {
+            if (isFunction(prod) || rule.att().contains(Attribute.ANYWHERE_KEY)) {
                 leftChildren = ((KApply) left).items();
                 equation = true;
             } else if ((rule.att().contains("heat") || rule.att().contains("cool")) && heatCoolEq) {
@@ -673,7 +673,7 @@ private void convertRule(Rule rule, boolean heatCoolEq, Sort topCellSort, Map<St
                 convert(consideredAttributes, rule.att());
                 sb.append("\n\n");
             }
-        } else if (!rule.att().contains(Attribute.MACRO_KEY) && !rule.att().contains(Attribute.ALIAS_KEY) && !rule.att().contains(Attribute.ANYWHERE_KEY)) {
+        } else if (!rule.att().contains(Attribute.MACRO_KEY) && !rule.att().contains(Attribute.ALIAS_KEY)) {
             if (rulesAsClaims) {
                 sb.append("  claim{} ");
             } else {
@@ -876,9 +876,15 @@ private Att addKoreAttributes(Production prod, SetMultimap<KLabel, Rule> functio
                 (prod.att().contains(Attribute.FUNCTION_KEY) && prod.att().contains(Attribute.UNIT_KEY))) {
             isConstructor = false;
         }
+        boolean isAnywhere = false;
+        if (overloads.contains(prod)) {
+            isConstructor = false;
+            isAnywhere = true;
+        }
         for (Rule r : functionRules.get(prod.klabel().get())) {
             if (r.att().contains(Attribute.ANYWHERE_KEY)) {
                 isConstructor = false;
+                isAnywhere = true;
             }
         }
         Att att = prod.att().remove("constructor");
@@ -891,7 +897,7 @@ private Att addKoreAttributes(Production prod, SetMultimap<KLabel, Rule> functio
         if (isFunctional) {
             att = att.add("functional");
         }
-        if (overloads.contains(prod)) {
+        if (isAnywhere) {
             att = att.add("anywhere");
         }
         return att;
