fix bug in or patterns when used outside of a rewrite (#340)

* fix bug in or patterns when used outside of a rewrite * expand macros prior to GuardOrPatterns * support anonymous variables in or patterns
runtimeverification · Mar 8, 2019 · 3e98406 · 3e98406
1 parent 1a38233
commit 3e98406
Show file tree

Hide file tree

Showing 14 changed files with 140 additions and 13 deletions.
diff --git a/k-distribution/tests/regression-new/or-llvm/4.test b/k-distribution/tests/regression-new/or-llvm/4.test
@@ -0,0 +1 @@
+test(foo)
diff --git a/k-distribution/tests/regression-new/or-llvm/4.test.out b/k-distribution/tests/regression-new/or-llvm/4.test.out
@@ -0,0 +1,3 @@
+<k>
+  2 ~> test ( foo )
+</k>
diff --git a/k-distribution/tests/regression-new/or-llvm/5.test b/k-distribution/tests/regression-new/or-llvm/5.test
@@ -0,0 +1 @@
+test(bar)
diff --git a/k-distribution/tests/regression-new/or-llvm/5.test.out b/k-distribution/tests/regression-new/or-llvm/5.test.out
@@ -0,0 +1,3 @@
+<k>
+  2 ~> test ( bar )
+</k>
diff --git a/k-distribution/tests/regression-new/or-llvm/6.test b/k-distribution/tests/regression-new/or-llvm/6.test
@@ -0,0 +1 @@
+test(test2(baz,baz))
diff --git a/k-distribution/tests/regression-new/or-llvm/6.test.out b/k-distribution/tests/regression-new/or-llvm/6.test.out
@@ -0,0 +1,3 @@
+<k>
+  1
+</k>
diff --git a/k-distribution/tests/regression-new/or-llvm/7.test b/k-distribution/tests/regression-new/or-llvm/7.test
@@ -0,0 +1 @@
+test(test(test2(baz,baz)))
diff --git a/k-distribution/tests/regression-new/or-llvm/7.test.out b/k-distribution/tests/regression-new/or-llvm/7.test.out
@@ -0,0 +1,3 @@
+<k>
+  1
+</k>
diff --git a/k-distribution/tests/regression-new/or-llvm/test.k b/k-distribution/tests/regression-new/or-llvm/test.k
@@ -4,7 +4,9 @@ module TEST
   imports INT
   imports BOOL
 
-  syntax KItem ::= "foo" | "bar" | "baz"
+  syntax KItem ::= "foo" | "bar" | "baz" | test(K) | test2(K, K)
   rule foo #Or bar #Or baz => 0
+  rule (.K => 2) ~> test(foo #Or bar)
+  rule test(test2(baz,_) #Or test(test2(baz,_))) => 1
 
 endmodule
diff --git a/k-distribution/tests/regression-new/or-ocaml/test.k b/k-distribution/tests/regression-new/or-ocaml/test.k
diff --git a/k-distribution/tests/regression-new/or-ocaml/test.k b/k-distribution/tests/regression-new/or-ocaml/test.k
@@ -0,0 +1 @@
+../or-llvm/test.k
diff --git a/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java b/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java
@@ -13,6 +13,7 @@
 import org.kframework.compile.GeneratedTopFormat;
 import org.kframework.compile.GenerateSortPredicateRules;
 import org.kframework.compile.GenerateSortPredicateSyntax;
+import org.kframework.compile.GuardOrPatterns;
 import org.kframework.compile.LabelInfo;
 import org.kframework.compile.LabelInfoFromModule;
 import org.kframework.compile.MinimizeTermConstruction;
@@ -112,6 +113,7 @@ public Function<Definition, Definition> steps() {
         DefinitionTransformer resolveStrict = DefinitionTransformer.from(new ResolveStrict(kompileOptions)::resolve, "resolving strict and seqstrict attributes");
         DefinitionTransformer resolveHeatCoolAttribute = DefinitionTransformer.fromSentenceTransformer(new ResolveHeatCoolAttribute(new HashSet<>(kompileOptions.transition), heatCoolConditions)::resolve, "resolving heat and cool attributes");
         DefinitionTransformer resolveAnonVars = DefinitionTransformer.fromSentenceTransformer(new ResolveAnonVar()::resolve, "resolving \"_\" vars");
+        DefinitionTransformer guardOrs = DefinitionTransformer.fromSentenceTransformer(new GuardOrPatterns()::resolve, "resolving or patterns");
         DefinitionTransformer resolveSemanticCasts =
                 DefinitionTransformer.fromSentenceTransformer(new ResolveSemanticCasts(true)::resolve, "resolving semantic casts");
         DefinitionTransformer resolveFun = DefinitionTransformer.from(new ResolveFun()::resolve, "resolving #fun");
@@ -132,6 +134,7 @@ public Function<Definition, Definition> steps() {
                 .andThen(resolveHeatCoolAttribute)
                 .andThen(resolveSemanticCasts)
                 .andThen(expandMacros)
+                .andThen(guardOrs)
                 .andThen(generateSortPredicateSyntax)
                 .andThen(AddImplicitComputationCell::transformDefinition)
                 .andThen(resolveFreshConstants)

diff --git a/kernel/src/main/java/org/kframework/compile/GuardOrPatterns.java b/kernel/src/main/java/org/kframework/compile/GuardOrPatterns.java
@@ -0,0 +1,103 @@
+// Copyright (c) 2019 K Team. All Rights Reserved.
+package org.kframework.compile;
+
+import org.kframework.builtin.KLabels;
+import org.kframework.definition.Context;
+import org.kframework.definition.Production;
+import org.kframework.definition.Rule;
+import org.kframework.definition.Sentence;
+import org.kframework.kore.*;
+
+import java.util.HashSet;
+import java.util.Set;
+
+import static org.kframework.kore.KORE.*;
+
+public class GuardOrPatterns {
+
+    private Set<KVariable> vars = new HashSet<>();
+
+    void resetVars() {
+        vars.clear();
+    }
+
+    private Rule resolve(Rule rule) {
+        resetVars();
+        gatherVars(rule.body());
+        gatherVars(rule.requires());
+        gatherVars(rule.ensures());
+        return new Rule(
+                transform(rule.body()),
+                transform(rule.requires()),
+                transform(rule.ensures()),
+                rule.att());
+    }
+
+    private Context resolve(Context context) {
+        resetVars();
+        gatherVars(context.body());
+        gatherVars(context.requires());
+        return new Context(
+                transform(context.body()),
+                transform(context.requires()),
+                context.att());
+    }
+
+    public K resolveK(K k) {
+        resetVars();;
+        gatherVars(k);
+        return transform(k);
+    }
+
+    public synchronized Sentence resolve(Sentence s) {
+        if (s instanceof Rule) {
+            return resolve((Rule) s);
+        } else if (s instanceof Context) {
+            return resolve((Context) s);
+        } else {
+            return s;
+        }
+    }
+
+    void gatherVars(K term) {
+        new VisitK() {
+            @Override
+            public void apply(KVariable v) {
+                vars.add(v);
+                super.apply(v);
+            }
+        }.apply(term);
+    }
+
+    K transform(K term) {
+        return new TransformK() {
+            @Override
+            public K apply(KApply k) {
+              if (k.klabel().equals(KLabels.ML_OR)) {
+                return KAs(k, newDotVariable());
+              }
+              return super.apply(k);
+            }
+
+            @Override
+            public K apply(KAs k) {
+              return k;
+            }
+
+            @Override
+            public K apply(KRewrite k) {
+              return KRewrite(k.left(), apply(k.right()), k.att());
+            }
+        }.apply(term);
+    }
+
+    private int counter = 0;
+    KVariable newDotVariable() {
+        KVariable newLabel;
+        do {
+            newLabel = KVariable("_" + (counter++), Att().add("anonymous"));
+        } while (vars.contains(newLabel));
+        vars.add(newLabel);
+        return newLabel;
+    }
+}
diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java
@@ -152,12 +152,14 @@ public static Function<Definition, Definition> defaultSteps(KompileOptions kompi
         DefinitionTransformer resolveStrict = DefinitionTransformer.from(new ResolveStrict(kompileOptions)::resolve, "resolving strict and seqstrict attributes");
         DefinitionTransformer resolveHeatCoolAttribute = DefinitionTransformer.fromSentenceTransformer(new ResolveHeatCoolAttribute(new HashSet<>(kompileOptions.transition), EnumSet.of(HEAT_RESULT, COOL_RESULT_CONDITION, COOL_RESULT_INJECTION))::resolve, "resolving heat and cool attributes");
         DefinitionTransformer resolveAnonVars = DefinitionTransformer.fromSentenceTransformer(new ResolveAnonVar()::resolve, "resolving \"_\" vars");
+        DefinitionTransformer guardOrs = DefinitionTransformer.fromSentenceTransformer(new GuardOrPatterns()::resolve, "resolving or patterns");
         DefinitionTransformer resolveSemanticCasts =
                 DefinitionTransformer.fromSentenceTransformer(new ResolveSemanticCasts(kompileOptions.backend.equals(Backends.JAVA))::resolve, "resolving semantic casts");
         DefinitionTransformer resolveFun = DefinitionTransformer.from(new ResolveFun()::resolve, "resolving #fun");
         DefinitionTransformer resolveFunctionWithConfig = DefinitionTransformer.fromSentenceTransformer(new ResolveFunctionWithConfig()::resolve, "resolving functions with config context");
         DefinitionTransformer generateSortPredicateSyntax = DefinitionTransformer.from(new GenerateSortPredicateSyntax()::gen, "adding sort predicate productions");
         DefinitionTransformer subsortKItem = DefinitionTransformer.from(Kompile::subsortKItem, "subsort all sorts to KItem");
+        DefinitionTransformer expandMacros = DefinitionTransformer.fromSentenceTransformer((m, s) -> new ExpandMacros(m, files, kompileOptions, false).expand(s), "expand macros");
         GenerateCoverage cov = new GenerateCoverage(kompileOptions.coverage, files);
         DefinitionTransformer genCoverage = DefinitionTransformer.fromRuleBodyTransformerWithRule(cov::gen, "generate coverage instrumentation");
         DefinitionTransformer numberSentences = DefinitionTransformer.fromSentenceTransformer(new NumberSentences()::number, "number sentences uniquely");
@@ -173,6 +175,8 @@ public static Function<Definition, Definition> defaultSteps(KompileOptions kompi
                 .andThen(numberSentences)
                 .andThen(resolveHeatCoolAttribute)
                 .andThen(resolveSemanticCasts)
+                .andThen(expandMacros)
+                .andThen(guardOrs)
                 .andThen(generateSortPredicateSyntax)
                 .andThen(Kompile::resolveFreshConstants)
                 .andThen(AddImplicitComputationCell::transformDefinition)

diff --git a/ocaml-backend/src/main/java/org/kframework/backend/ocaml/DefinitionToOcaml.java b/ocaml-backend/src/main/java/org/kframework/backend/ocaml/DefinitionToOcaml.java
@@ -2700,7 +2700,11 @@ private void applyVarRhs(String varOccurrance, StringBuilder sb, KLabel listVar)
         }
     }
 
-    private void applyVarLhs(KVariable k, StringBuilder sb, VarInfo vars) {
+    private void applyVarLhs(KVariable k, StringBuilder sb, VarInfo vars, boolean inOr) {
+        if (inOr && k.att().contains("anonymous")) {
+          sb.append("_");
+          return;
+        }
         String varName = encodeStringToVariable(k.name());
         vars.vars.put(k, varName);
         Sort s = k.att().getOptional(Sort.class).orElse(Sort(""));
@@ -2737,6 +2741,7 @@ public Visitor(StringBuilder sb, boolean rhs, VarInfo vars, boolean useNativeBoo
         private boolean inBooleanExp;
         private boolean topAnywherePre;
         private boolean topAnywherePost;
+        private boolean inOr = false;
 
         @Override
         public void apply(KApply k) {
@@ -2757,9 +2762,12 @@ public void apply(KApply k) {
             }
             if (k.klabel().equals(KLabels.ML_OR)) {
                 sb.append("((");
+                boolean wasInOr = inOr;
+                inOr = true;
                 apply(k.items().get(0));
                 sb.append(")|(");
                 apply(k.items().get(1));
+                inOr = wasInOr;
                 sb.append("))");
                 return;
             }
@@ -3040,7 +3048,7 @@ public void apply(KVariable k) {
             if (rhs) {
                 applyVarRhs(k, sb, vars);
             } else {
-                applyVarLhs(k, sb, vars);
+                applyVarLhs(k, sb, vars, inOr);
             }
             if (inBooleanExp) {
                 sb.append("])");