Merge remote-tracking branch 'origin/develop'

runtimeverification · Feb 9, 2024 · 6cf6880 · 6cf6880
2 parents df280ae + 0a498c3
commit 6cf6880
Show file tree

Hide file tree

Showing 5 changed files with 24 additions and 12 deletions.
diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java
@@ -44,7 +44,7 @@ public HaskellBackend(
   @Override
   public void accept(Backend.Holder h) {
     Stopwatch sw = new Stopwatch(globalOptions);
-    String kore = getKompiledString(h.def);
+    String kore = getKompiledString(h.def, true);
     h.def = null;
     files.saveToKompiled("definition.kore", kore);
     sw.printIntermediate("  Print definition.kore");

diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java
@@ -365,7 +365,7 @@ private RewriterResult executeKoreCommands(
 
       @Override
       public RewriterResult prove(Module rules, Boolean reuseDef) {
-        Module kompiledModule = KoreBackend.getKompiledModule(module);
+        Module kompiledModule = KoreBackend.getKompiledModule(module, true);
         ModuleToKORE converter =
             new ModuleToKORE(
                 kompiledModule,

diff --git a/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java b/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java
@@ -57,16 +57,21 @@ public KoreBackend(
   @Override
   public void accept(Backend.Holder h) {
     CompiledDefinition def = h.def;
-    String kore = getKompiledString(def);
+    String kore = getKompiledString(def, true);
     File defFile = kompileOptions.outerParsing.mainDefinitionFile(files);
     String name = defFile.getName();
     String basename = FilenameUtils.removeExtension(name);
     files.saveToDefinitionDirectory(basename + ".kore", kore);
   }
 
-  /** Convert a CompiledDefinition to a String of a KORE definition. */
-  protected String getKompiledString(CompiledDefinition def) {
-    Module mainModule = getKompiledModule(def.kompiledDefinition.mainModule());
+  /**
+   * Convert a CompiledDefinition to a String of a KORE definition.
+   *
+   * @param hasAnd whether the backend in question supports and-patterns during pattern matching.
+   */
+  protected String getKompiledString(
+      CompiledDefinition def, @SuppressWarnings("unused") boolean hasAnd) {
+    Module mainModule = getKompiledModule(def.kompiledDefinition.mainModule(), hasAnd);
     ModuleToKORE converter =
         new ModuleToKORE(mainModule, def.topCellInitializer, def.kompileOptions);
     return getKompiledString(converter, files, heatCoolEquations, tool);
@@ -94,18 +99,20 @@ public static String getKompiledStringAndWriteSyntaxMacros(
     return semantics.toString();
   }
 
-  public static Module getKompiledModule(Module mainModule) {
+  public static Module getKompiledModule(Module mainModule, boolean hasAnd) {
     mainModule =
         ModuleTransformer.fromSentenceTransformer(
                 new AddSortInjections(mainModule)::addInjections, "Add sort injections")
             .apply(mainModule);
     mainModule =
         ModuleTransformer.from(new RemoveUnit()::apply, "Remove unit applications for collections")
             .apply(mainModule);
-    mainModule =
-        ModuleTransformer.fromSentenceTransformer(
-                new MinimizeTermConstruction(mainModule)::resolve, "Minimize term construction")
-            .apply(mainModule);
+    if (hasAnd) {
+      mainModule =
+          ModuleTransformer.fromSentenceTransformer(
+                  new MinimizeTermConstruction(mainModule)::resolve, "Minimize term construction")
+              .apply(mainModule);
+    }
     return mainModule;
   }
 

diff --git a/kernel/src/main/java/org/kframework/utils/errorsystem/KExceptionManager.java b/kernel/src/main/java/org/kframework/utils/errorsystem/KExceptionManager.java
@@ -91,6 +91,11 @@ public void registerCriticalWarning(ExceptionType type, String message, Throwabl
     register(type, KExceptionGroup.CRITICAL, message, e, null, null);
   }
 
+  @SuppressWarnings("unused")
+  public void registerInternalWarning(ExceptionType type, String message) {
+    register(type, KExceptionGroup.INTERNAL, message, null, null, null);
+  }
+
   public void registerInternalWarning(ExceptionType type, String message, Throwable e) {
     register(type, KExceptionGroup.INTERNAL, message, e, null, null);
   }

diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java
@@ -49,7 +49,7 @@ public LLVMBackend(
   @Override
   public void accept(Backend.Holder h) {
     Stopwatch sw = new Stopwatch(globalOptions);
-    String kore = getKompiledString(h.def);
+    String kore = getKompiledString(h.def, true);
     h.def = null;
     files.saveToKompiled("definition.kore", kore);
     sw.printIntermediate("  Print definition.kore");