diff --git a/k-distribution/tests/regression-new/or-llvm/4.test b/k-distribution/tests/regression-new/or-llvm/4.test new file mode 100644 index 00000000000..c55933e26e1 --- /dev/null +++ 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 new file mode 100644 index 00000000000..5738e563cd6 --- /dev/null +++ b/k-distribution/tests/regression-new/or-llvm/4.test.out @@ -0,0 +1,3 @@ + + 2 ~> test ( foo ) + diff --git a/k-distribution/tests/regression-new/or-llvm/5.test b/k-distribution/tests/regression-new/or-llvm/5.test new file mode 100644 index 00000000000..e25090f8cda --- /dev/null +++ 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 new file mode 100644 index 00000000000..410b3807c08 --- /dev/null +++ b/k-distribution/tests/regression-new/or-llvm/5.test.out @@ -0,0 +1,3 @@ + + 2 ~> test ( bar ) + diff --git a/k-distribution/tests/regression-new/or-llvm/6.test b/k-distribution/tests/regression-new/or-llvm/6.test new file mode 100644 index 00000000000..82f449fba61 --- /dev/null +++ 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 new file mode 100644 index 00000000000..9589fd94e27 --- /dev/null +++ b/k-distribution/tests/regression-new/or-llvm/6.test.out @@ -0,0 +1,3 @@ + + 1 + diff --git a/k-distribution/tests/regression-new/or-llvm/7.test b/k-distribution/tests/regression-new/or-llvm/7.test new file mode 100644 index 00000000000..243c12c2fe0 --- /dev/null +++ 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 new file mode 100644 index 00000000000..9589fd94e27 --- /dev/null +++ b/k-distribution/tests/regression-new/or-llvm/7.test.out @@ -0,0 +1,3 @@ + + 1 + diff --git a/k-distribution/tests/regression-new/or-llvm/test.k b/k-distribution/tests/regression-new/or-llvm/test.k index 31652cd391e..4750fd9b4eb 100644 --- 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 deleted file mode 100644 index 31652cd391e..00000000000 --- a/k-distribution/tests/regression-new/or-ocaml/test.k +++ /dev/null @@ -1,10 +0,0 @@ -// Copyright (c) 2019 K Team. All Rights Reserved. - -module TEST - imports INT - imports BOOL - - syntax KItem ::= "foo" | "bar" | "baz" - rule foo #Or bar #Or baz => 0 - -endmodule diff --git a/k-distribution/tests/regression-new/or-ocaml/test.k b/k-distribution/tests/regression-new/or-ocaml/test.k new file mode 120000 index 00000000000..3f233bbf9e6 --- /dev/null +++ b/k-distribution/tests/regression-new/or-ocaml/test.k @@ -0,0 +1 @@ +../or-llvm/test.k \ No newline at end of file diff --git a/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java b/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java index f4ad83bb1a1..4d73a3fe3a2 100644 --- 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 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 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 new file mode 100644 index 00000000000..89adf04bac8 --- /dev/null +++ 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 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 index 4b762ddeeac..6099b9bddc7 100644 --- 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 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 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 index c4c7f3ddc90..06c55be8d49 100644 --- 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("])");