Merge branch 'develop' into connected

deps/hs-backend-booster_release

@@ -1 +1 @@
-36d54e028bd6c5720063ae562758bd7e4848f00d
+88ffab54a7266d8c98d5c039ef81143d1d24f3f0

flake.nix

@@ -3,7 +3,7 @@
   inputs = {
     haskell-backend.url = "github:runtimeverification/haskell-backend/093af3153a5e07626d9b2e628d7ad4fc77c5a723";
     booster-backend = {
-      url = "github:runtimeverification/hs-backend-booster/36d54e028bd6c5720063ae562758bd7e4848f00d";
+      url = "github:runtimeverification/hs-backend-booster/88ffab54a7266d8c98d5c039ef81143d1d24f3f0";
       inputs.nixpkgs.follows = "haskell-backend/nixpkgs";
       inputs.haskell-backend.follows = "haskell-backend";
       inputs.stacklock2nix.follows = "haskell-backend/stacklock2nix";

k-distribution/tests/regression-new/total-proj/1.test

@@ -0,0 +1 @@
+foo()

k-distribution/tests/regression-new/total-proj/1.test.out

@@ -0,0 +1,3 @@
+<k>
+  false ~> .K
+</k>

k-distribution/tests/regression-new/total-proj/Makefile

@@ -0,0 +1,6 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_BACKEND=haskell
+
+include ../../../include/kframework/ktest.mak

k-distribution/tests/regression-new/total-proj/test.k

@@ -0,0 +1,15 @@
+module TEST
+  imports INT
+  imports BOOL
+  imports LIST
+
+  configuration <k> $PGM:Pgm </k>
+
+  syntax Pgm ::= foo() | Pgm2
+  syntax Pgm2 ::= bar(baz: Int)
+
+  rule foo() => ?X:Pgm2
+  rule X:Pgm2 => baz(X)
+  rule I:Int => false
+
+endmodule

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

@@ -154,9 +154,12 @@ public Function<Definition, Definition> steps() {
     DefinitionTransformer generateSortPredicateRules =
         DefinitionTransformer.from(
             new GenerateSortPredicateRules()::gen, "adding sort predicate rules");
-    DefinitionTransformer generateSortProjections =
-        DefinitionTransformer.from(
-            new GenerateSortProjections(kompileOptions.coverage)::gen, "adding sort projections");
+    Function1<Definition, Definition> generateSortProjections =
+        d ->
+            DefinitionTransformer.from(
+                    new GenerateSortProjections(kompileOptions.coverage, d.mainModule())::gen,
+                    "adding sort projections")
+                .apply(d);
     DefinitionTransformer subsortKItem =
         DefinitionTransformer.from(Kompile::subsortKItem, "subsort all sorts to KItem");
     Function1<Definition, Definition> addCoolLikeAtt =
@@ -377,8 +380,11 @@ public Function<Module, Module> specificationSteps(Definition def) {
         ModuleTransformer.fromSentenceTransformer(
             new ConcretizeCells(configInfo, labelInfo, sortInfo, mod)::concretize,
             "concretizing configuration");
-    ModuleTransformer generateSortProjections =
-        ModuleTransformer.from(new GenerateSortProjections(false)::gen, "adding sort projections");
+    Function1<Module, Module> generateSortProjections =
+        m ->
+            ModuleTransformer.from(
+                    new GenerateSortProjections(false, m)::gen, "adding sort projections")
+                .apply(m);
 
     return m ->
         resolveComm

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

@@ -28,13 +28,16 @@
 public class GenerateSortProjections {
 
   private Module mod;
+  private final Module mainMod;
   private final boolean cover;
 
-  public GenerateSortProjections(boolean cover) {
+  public GenerateSortProjections(boolean cover, Module mainMod) {
+    this.mainMod = mainMod;
     this.cover = cover;
   }
 
   public GenerateSortProjections(Module mod) {
+    this.mainMod = null;
     this.mod = mod;
     this.cover = false;
   }
@@ -133,13 +136,30 @@ public Stream<? extends Sentence> gen(Production prod) {
     if (!hasName) {
       return Stream.empty();
     }
+    boolean total = false;
+    if (mainMod != null) {
+      if (stream(
+                  mainMod
+                      .productionsForSort()
+                      .get(prod.sort().head())
+                      .getOrElse(() -> Collections.<Production>Set()))
+              .filter(p -> !p.att().contains(Att.FUNCTION()))
+              .count()
+          == 1) {
+        total = true;
+      }
+    }
     i = 0;
     for (NonTerminal nt : iterable(prod.nonterminals())) {
       if (nt.name().isDefined()) {
         KLabel lbl = getProjectLbl(prod.klabel().get().name(), nt.name().get());
         if (mod.definedKLabels().contains(lbl)) {
           return Stream.empty();
         }
+        Att att = Att.empty().add(Att.FUNCTION());
+        if (total) {
+          att = att.add(Att.TOTAL());
+        }
         sentences.add(
             Production(
                 lbl,
@@ -149,7 +169,7 @@ public Stream<? extends Sentence> gen(Production prod) {
                     Terminal("("),
                     NonTerminal(prod.sort()),
                     Terminal(")")),
-                Att.empty().add(Att.FUNCTION())));
+                att));
         sentences.add(
             Rule(
                 KRewrite(KApply(lbl, KApply(prod.klabel().get(), KList(vars))), vars.get(i)),

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

@@ -17,6 +17,14 @@
 import org.kframework.definition.Sentence;
 import org.kframework.kore.*;
 
+/**
+ * MinimizeTermConstruction.
+ *
+ * <p>Looks for places where #as patterns can be used to reduce the number of constructors in
+ * rewrites:
+ *
+ * <p>`P1 => P2[P1]` -> `P1 #as X => P2[X]`
+ */
 public class MinimizeTermConstruction {
 
   private final Set<KVariable> vars = new HashSet<>();