Requires in haskell is LHS (#2690)

Co-authored-by: Radu Mereuta <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · Jun 29, 2022 · 207ff55 · 207ff55
1 parent f132621
commit 207ff55
Show file tree

Hide file tree

Showing 4 changed files with 32 additions and 3 deletions.
diff --git a/k-distribution/tests/regression-new/checkWarns/checkRHSHaskell.k b/k-distribution/tests/regression-new/checkWarns/checkRHSHaskell.k
@@ -0,0 +1,25 @@
+// This should kompile just fine for the haskell backend, variables
+// in the requires clause should be considered as part of LHS for haskell backend.
+// https://github.com/runtimeverification/k/issues/2687
+
+module CHECKRHSHASKELL-SYNTAX
+
+endmodule
+
+module CHECKRHSHASKELL
+    imports CHECKRHSHASKELL-SYNTAX
+    imports MAP
+    imports INT
+    imports BOOL
+
+    syntax Pgm ::= "a" | "b"
+
+    rule <k> a => b </k>
+
+    syntax Int ::= f ( Int ) [function, functional, no-evaluators]
+
+    configuration <k> $PGM:Pgm </k>
+
+    rule <k> a => b </k> requires f(_X) ==Int 3
+
+endmodule
diff --git a/k-distribution/tests/regression-new/checkWarns/checkRHSHaskell.k.out b/k-distribution/tests/regression-new/checkWarns/checkRHSHaskell.k.out
diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckRHSVariables.java b/kernel/src/main/java/org/kframework/compile/checks/CheckRHSVariables.java
@@ -3,10 +3,12 @@
 
 import com.google.common.collect.Sets;
 import org.kframework.attributes.Att;
+import org.kframework.backend.Backends;
 import org.kframework.compile.GatherVarsVisitor;
 import org.kframework.definition.Claim;
 import org.kframework.definition.Context;
 import org.kframework.definition.ContextAlias;
+import org.kframework.definition.Rule;
 import org.kframework.definition.RuleOrClaim;
 import org.kframework.definition.Sentence;
 import org.kframework.kore.K;
@@ -31,18 +33,20 @@
 public class CheckRHSVariables {
     private final Set<KEMException> errors;
     private final boolean errorExistential;
+    private final String backend;
 
-    public CheckRHSVariables(Set<KEMException> errors, boolean errorExistential) {
+    public CheckRHSVariables(Set<KEMException> errors, boolean errorExistential, String backend) {
         this.errors = errors;
         this.errorExistential = errorExistential;
+        this.backend = backend;
     }
     private void check(RuleOrClaim rule) {
         resetVars();
         Set<String> unboundVariableNames = getUnboundVarNames(rule);
         boolean errorExistential = this.errorExistential && !(rule.att().contains(Att.LABEL()) && rule.att().get(Att.LABEL()).equals("STDIN-STREAM.stdinUnblock"));
         gatherVars(true, rule.body(), errorExistential);
         gatherVars(false, rule.ensures(), errorExistential);
-        if (rule instanceof Claim) {
+        if (rule instanceof Claim || (rule instanceof Rule && backend.equals(Backends.HASKELL))) {
             gatherVars(true, rule.requires(), errorExistential);
             check(rule.body(), true, false, unboundVariableNames);
             check(rule.requires(), true, false, unboundVariableNames);

diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java
@@ -465,7 +465,7 @@ public void proverChecksX(Module specModule, Module mainDefModule) {
     public void structuralChecks(scala.collection.Set<Module> modules, Module mainModule, Option<Module> kModule, Set<String> excludedModuleTags) {
         boolean isSymbolic = excludedModuleTags.contains(Att.CONCRETE());
         boolean isKast = excludedModuleTags.contains(Att.KORE());
-        CheckRHSVariables checkRHSVariables = new CheckRHSVariables(errors, !isSymbolic);
+        CheckRHSVariables checkRHSVariables = new CheckRHSVariables(errors, !isSymbolic, kompileOptions.backend);
         stream(modules).forEach(m -> stream(m.localSentences()).forEach(checkRHSVariables::check));
 
         stream(modules).forEach(m -> stream(m.localSentences()).forEach(new CheckAtt(errors, kem, mainModule, isSymbolic && isKast)::check));