Merge branch 'develop' into nailgun-location

deps/hs-backend-booster_release

@@ -1 +1 @@
-ac35589bb31831b346e143bfa98c51e670237b8e
+c289a1a29575f9e5156fae75fb34e1c97cfffd02

flake.nix

@@ -1,9 +1,9 @@
 {
   description = "K Framework";
   inputs = {
-    haskell-backend.url = "github:runtimeverification/haskell-backend/eebe4e9fd9dd6c606b37a384dbbfecca85943a38";
+    haskell-backend.url = "github:runtimeverification/haskell-backend/b2bade8ce62e5f3add32d87e98244ceb31790f9f";
     booster-backend = {
-      url = "github:runtimeverification/hs-backend-booster/ac35589bb31831b346e143bfa98c51e670237b8e";
+      url = "github:runtimeverification/hs-backend-booster/c289a1a29575f9e5156fae75fb34e1c97cfffd02";
       inputs.nixpkgs.follows = "haskell-backend/nixpkgs";
       inputs.haskell-backend.follows = "haskell-backend";
       inputs.stacklock2nix.follows = "haskell-backend/stacklock2nix";

haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java

@@ -380,7 +380,12 @@ private RewriterResult executeKoreCommands(
       public RewriterResult prove(Module rules, Boolean reuseDef) {
         Module kompiledModule = KoreBackend.getKompiledModule(module, true);
         ModuleToKORE converter =
-            new ModuleToKORE(kompiledModule, def.topCellInitializer, kompileOptions, kem);
+            new ModuleToKORE(
+                kompiledModule,
+                def.topCellInitializer,
+                kompileOptions,
+                kem,
+                kProveOptions.allowFuncClaims);
         String defPath =
             reuseDef
                 ? files.resolveKompiled("definition.kore").getAbsolutePath()

k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a4-spec.k

@@ -6,7 +6,7 @@ module A4-SPEC
   import TEST
   imports ML-SYNTAX
 
-  claim c => 2 #And {3 #Equals n}
+  claim <k> c => 2 #And {3 #Equals n} </k>
   rule {n #Equals 3} => #Top [simplification, comm] // the comm attribute is stripped because it has a different meaning in the backend
   // rule {3 #Equals n} => #Top [simplification] // should be generated by the above
 endmodule

k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a5-spec.k

@@ -6,7 +6,7 @@ module A5-SPEC
   import TEST
   imports ML-SYNTAX
 
-  claim c => 2 #And n +Int n
+  claim <k> c => 2 #And n +Int n </k>
   rule n +Int n => #Top [simplification, comm]
   // the comm attribute is stripped because it has a different meaning in the backend
   // even if comm, the body is identical so we don't generate anything extra

kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java

@@ -117,15 +117,22 @@ public enum SentenceType {
   private final Set<String> mlBinders = new HashSet<>();
   private final KompileOptions options;
 
+  // for now these two variables are coupled to enable the functional claim check
   private final KExceptionManager kem;
+  private final boolean allowFuncClaims;
 
   public ModuleToKORE(Module module, KLabel topCellInitializer, KompileOptions options) {
-    this(module, topCellInitializer, options, null);
+    this(module, topCellInitializer, options, null, false);
   }
 
   public ModuleToKORE(
-      Module module, KLabel topCellInitializer, KompileOptions options, KExceptionManager kem) {
+      Module module,
+      KLabel topCellInitializer,
+      KompileOptions options,
+      KExceptionManager kem,
+      boolean allowFuncClaims) {
     this.kem = kem;
+    this.allowFuncClaims = allowFuncClaims;
     this.module = module;
     this.addSortInjections = new AddSortInjections(module);
     this.topCellInitializer = topCellInitializer;
@@ -1057,6 +1064,9 @@ private RuleInfo getRuleInfo(RuleOrClaim rule, boolean heatCoolEq, String topCel
         productionSortStr = topCellSortStr;
       }
       owise = rule.att().contains(Att.OWISE());
+    } else if (leftPattern instanceof KToken kt) {
+      productionSort = kt.sort();
+      productionSortStr = getSortStr(productionSort);
     }
 
     return new RuleInfo(
@@ -1107,7 +1117,7 @@ private void convertRule(
       assertNoExistentials(rule, existentials);
       if (rule instanceof Claim) {
         sb.append("  claim{R");
-        if (kem != null) // TODO: remove once
+        if (!allowFuncClaims) // TODO: remove once
           // https://github.com/runtimeverification/haskell-backend/issues/3010 is
           // implemented
           kem.registerCompilerWarning(
@@ -1348,38 +1358,38 @@ private void convertRule(
       } else {
         // LHS for claims
         sb.append("  claim{} ");
-        sb.append(String.format("\\implies{%s} (\n    ", topCellSortStr));
-        sb.append(String.format("  \\and{%s} (\n      ", topCellSortStr));
-        convertSideCondition(requires, topCellSortStr, sb);
+        sb.append(String.format("\\implies{%s} (\n    ", ruleInfo.productionSortStr));
+        sb.append(String.format("  \\and{%s} (\n      ", ruleInfo.productionSortStr));
+        convertSideCondition(requires, ruleInfo.productionSortStr, sb);
         sb.append(", ");
         convert(left, sb);
         sb.append("), ");
       }
 
       // generate rule RHS
       if (sentenceType == SentenceType.ALL_PATH) {
-        sb.append(String.format("%s{%s} (\n      ", ALL_PATH_OP, topCellSortStr));
+        sb.append(String.format("%s{%s} (\n      ", ALL_PATH_OP, ruleInfo.productionSortStr));
       } else if (sentenceType == SentenceType.ONE_PATH) {
-        sb.append(String.format("%s{%s} (\n      ", ONE_PATH_OP, topCellSortStr));
+        sb.append(String.format("%s{%s} (\n      ", ONE_PATH_OP, ruleInfo.productionSortStr));
       }
       if (!existentials.isEmpty()) {
         for (KVariable exists : existentials) {
-          sb.append(String.format(" \\exists{%s} (", topCellSortStr));
+          sb.append(String.format(" \\exists{%s} (", ruleInfo.productionSortStr));
           convert((K) exists, sb);
           sb.append(", ");
         }
         sb.append("\n      ");
       }
-      sb.append(String.format("\\and{%s} (\n      ", topCellSortStr));
+      sb.append(String.format("\\and{%s} (\n      ", ruleInfo.productionSortStr));
 
       if (options.enableKoreAntileft) {
-        convertSideCondition(ensures, topCellSortStr, sb);
+        convertSideCondition(ensures, ruleInfo.productionSortStr, sb);
         sb.append(", ");
         convert(right, sb);
       } else {
         convert(right, sb);
         sb.append(", ");
-        convertSideCondition(ensures, topCellSortStr, sb);
+        convertSideCondition(ensures, ruleInfo.productionSortStr, sb);
       }
 
       sb.append(')');

kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java

@@ -66,7 +66,7 @@ private boolean skipSentence(Sentence s) {
   // cell mentioned is the automatically-added <generatedCounter> cell.
   private boolean shouldConsider(List<K> items, boolean isClaim) {
     if (items.size() == 1) {
-      return true;
+      return !isClaim;
     } else if (items.size() == 2 && isClaim) {
       K second = items.get(1);
       if (second instanceof KApply app) {

kernel/src/main/java/org/kframework/compile/AddImplicitCounterCell.java

@@ -21,6 +21,21 @@ public AddImplicitCounterCell() {}
 
   public Sentence apply(Module m, Sentence s) {
     if (s instanceof Claim claim) {
+      Set<KVariable> freshVars = new HashSet<>();
+      VisitK visitor =
+          new VisitK() {
+            @Override
+            public void apply(KVariable var) {
+              if (ResolveFreshConstants.isFreshVar(var)) freshVars.add(var);
+            }
+          };
+      visitor.apply(claim.body());
+      visitor.apply(claim.requires());
+      visitor.apply(claim.ensures());
+      // do not add <generatedCounter> if the claim doesn't contain cells or fresh vars
+      if (!ConcretizeCells.hasCells(claim.body()) && freshVars.isEmpty()) {
+        return s;
+      }
       return claim.newInstance(
           apply(claim.body(), m), claim.requires(), claim.ensures(), claim.att());
     }

kernel/src/main/java/org/kframework/compile/ConcretizeCells.java

@@ -1,8 +1,12 @@
 // Copyright (c) K Team. All Rights Reserved.
 package org.kframework.compile;
 
+import java.util.stream.Stream;
+import org.kframework.attributes.Att;
 import org.kframework.definition.*;
 import org.kframework.definition.Module;
+import org.kframework.kore.K;
+import org.kframework.kore.KRewrite;
 
 /**
  * Apply the configuration concretization process. The implicit {@code <k>} cell is added by another
@@ -60,6 +64,9 @@ public ConcretizeCells(
   }
 
   public Sentence concretize(Module m, Sentence s) {
+    if (s instanceof Claim c && !hasCells(c.body())) {
+      return s;
+    }
     s = addRootCell.addImplicitCells(s, m);
     s = addParentCells.concretize(s);
     s = closeCells.close(s);
@@ -69,4 +76,20 @@ public Sentence concretize(Module m, Sentence s) {
     s = sortCells.postprocess(s);
     return s;
   }
+
+  public static boolean hasCells(K item) {
+    if (IncompleteCellUtils.flattenCells(item).stream()
+        .anyMatch(k -> k.att().get(Production.class).att().contains(Att.CELL()))) {
+      return true;
+    }
+
+    if (item instanceof KRewrite rew) {
+      return Stream.concat(
+              IncompleteCellUtils.flattenCells(rew.left()).stream(),
+              IncompleteCellUtils.flattenCells(rew.right()).stream())
+          .anyMatch(ConcretizeCells::hasCells);
+    }
+
+    return false;
+  }
 }

kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java

@@ -102,11 +102,15 @@ private Rule resolve(Rule rule) {
     return withFresh;
   }
 
+  public static boolean isFreshVar(KVariable kvar) {
+    return kvar.name().startsWith("!");
+  }
+
   private void analyze(K term) {
     new VisitK() {
       @Override
       public void apply(KVariable k) {
-        if (k.name().startsWith("!")) {
+        if (isFreshVar(k)) {
           freshVars.add(k);
         }
         super.apply(k);

kernel/src/main/java/org/kframework/kprove/KProveOptions.java

@@ -109,4 +109,10 @@ public synchronized File specFile(FileUtil files) {
       descriptionKey = "file",
       description = "If set, emit the JSON serialization of the spec module to the specified file.")
   public String emitJsonSpec = null;
+
+  @Parameter(
+      names = "--allow-func-claims",
+      description = "Allow functional claims to be printed in kore format. Use with --dry-run.",
+      hidden = true)
+  public boolean allowFuncClaims = false;
 }

kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java

@@ -66,6 +66,7 @@ public enum Status {
   private final boolean debug;
   private final Module mod;
   private final java.util.Set<SortHead> sorts;
+  private final Map<ProductionReference, Integer> prIds = new IdentityHashMap<>();
 
   // logic QF_DT is best if it exists as it will be faster than ALL. However, some z3 versions do
   // not have this logic.
@@ -593,15 +594,15 @@ public String apply(Term t) {
       boolean isTopSort =
           expectedSort.equals(Sorts.RuleContent()) || expectedSort.name().equals("#RuleBody");
       int id = nextId;
-      boolean shared = pr.id().isPresent() && variablesById.size() > pr.id().get();
+      boolean shared = prIds.containsKey(pr) && variablesById.size() > prIds.get(pr);
       if (!shared) {
         // if this is the first time reaching this term, initialize data structures with the
         // variables associated with
         // this term.
         nextId++;
         variablesById.add(new ArrayList<>());
         cacheById.add(new HashSet<>());
-        pr.setId(Optional.of(id));
+        prIds.put(pr, id);
         for (Sort param : iterable(pr.production().params())) {
           String name = "FreshVar" + param.name() + locStr(pr);
           if (!variables.contains(name)) {
@@ -612,7 +613,7 @@ public String apply(Term t) {
         }
       } else {
         // get cached id
-        id = pr.id().get();
+        id = prIds.get(pr);
       }
       if (pr instanceof TermCons tc) {
         boolean wasStrict = isStrictEquality;
@@ -682,7 +683,7 @@ public String apply(Term t) {
             nextId++;
             variablesById.add(new ArrayList<>());
             cacheById.add(new HashSet<>());
-            pr.setId(Optional.of(id));
+            prIds.put(pr, id);
             if (isAnonVar(c)) {
               name = "Var" + c.value() + locStr(c);
               isStrictEquality = true;
@@ -799,7 +800,7 @@ private String printSort(Sort s, Optional<ProductionReference> t, boolean isIncr
     Map<Sort, String> params = new HashMap<>();
     if (t.isPresent()) {
       if (t.get().production().params().nonEmpty()) {
-        int id = t.get().id().get();
+        int id = prIds.get(t.get());
         List<String> names = variablesById.get(id);
         Seq<Sort> formalParams = t.get().production().params();
         assert (names.size() == formalParams.size());
@@ -945,8 +946,8 @@ void pushNotModel() {
   }
 
   public Seq<Sort> getArgs(ProductionReference pr) {
-    if (pr.id().isPresent()) {
-      int id = pr.id().get();
+    if (prIds.containsKey(pr)) {
+      int id = prIds.get(pr);
       List<String> names = variablesById.get(id);
       return names.stream().map(this::getValue).collect(Collections.toList());
     } else {
@@ -1023,7 +1024,7 @@ private void reset() {
     }
   }
 
-  private static String locStr(ProductionReference pr) {
+  private String locStr(ProductionReference pr) {
     String suffix = "";
     if (pr.production().klabel().isDefined()) {
       suffix = "_" + pr.production().klabel().get().name().replace("|", "");
@@ -1040,7 +1041,7 @@ private static String locStr(ProductionReference pr) {
           + l.endColumn()
           + suffix;
     }
-    return pr.id().get() + suffix;
+    return prIds.get(pr) + suffix;
   }
 
   private StringBuilder sb = new StringBuilder();