Merge remote-tracking branch 'origin/develop'

runtimeverification · Feb 8, 2024 · dfc3776 · dfc3776
2 parents 5fdec96 + 59c24c1
commit dfc3776
Show file tree

Hide file tree

Showing 94 changed files with 140 additions and 2,132 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, true);
+    String kore = getKompiledString(h.def);
     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/HaskellBackendKModule.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java
@@ -48,18 +48,6 @@ public List<Pair<Class<?>, Boolean>> kompileOptions() {
     return Collections.singletonList(Pair.of(HaskellKompileOptions.class, true));
   }
 
-  @Override
-  public List<Module> getKRunModules() {
-    return Collections.singletonList(
-        new AbstractModule() {
-          @Override
-          protected void configure() {
-            binder().requireAtInjectOnConstructors();
-            installHaskellRewriter(binder());
-          }
-        });
-  }
-
   private void installHaskellRewriter(Binder binder) {
     bindOptions(HaskellBackendKModule.this::krunOptions, binder);
 

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
@@ -39,7 +39,6 @@
 import org.kframework.parser.KoreParser;
 import org.kframework.parser.kore.parser.ParseError;
 import org.kframework.rewriter.Rewriter;
-import org.kframework.rewriter.SearchType;
 import org.kframework.unparser.KPrint;
 import org.kframework.unparser.OutputModes;
 import org.kframework.utils.RunProcess;
@@ -50,7 +49,6 @@
 import org.kframework.utils.inject.RequestScoped;
 import org.kframework.utils.options.BackendOptions;
 import org.kframework.utils.options.SMTOptions;
-import scala.Tuple2;
 
 @RequestScoped
 public record HaskellRewriter(
@@ -136,22 +134,12 @@ public RewriterResult execute(K k, Optional<Integer> depth) {
 
       @Override
       public K match(K k, Rule rule) {
-        return search(k, Optional.of(0), Optional.empty(), rule, SearchType.STAR);
-      }
-
-      @Override
-      public Tuple2<RewriterResult, K> executeAndMatch(K k, Optional<Integer> depth, Rule rule) {
-        RewriterResult res = execute(k, depth);
-        return Tuple2.apply(res, match(res.k(), rule));
+        return search(k, Optional.of(0), Optional.empty(), rule);
       }
 
       @Override
       public K search(
-          K initialConfiguration,
-          Optional<Integer> depth,
-          Optional<Integer> bound,
-          Rule pattern,
-          SearchType searchType) {
+          K initialConfiguration, Optional<Integer> depth, Optional<Integer> bound, Rule pattern) {
         Module mod = getExecutionModule(module);
         String koreOutput =
             getKoreString(
@@ -216,8 +204,7 @@ public K search(
                 pgmPath,
                 "--output",
                 koreOutputFile.getAbsolutePath(),
-                "--searchType",
-                searchType.toString(),
+                "--searchType STAR",
                 "--search",
                 patternPath));
         if (depth.isPresent()) {
@@ -378,7 +365,7 @@ private RewriterResult executeKoreCommands(
 
       @Override
       public RewriterResult prove(Module rules, Boolean reuseDef) {
-        Module kompiledModule = KoreBackend.getKompiledModule(module, true);
+        Module kompiledModule = KoreBackend.getKompiledModule(module);
         ModuleToKORE converter =
             new ModuleToKORE(
                 kompiledModule,
@@ -424,12 +411,6 @@ public RewriterResult prove(Module rules, Boolean reuseDef) {
 
         return executeKoreCommands(rules, koreCommand, koreDirectory, koreOutputFile);
       }
-
-      @Override
-      public boolean equivalence(
-          Rewriter firstDef, Rewriter secondDef, Module firstSpec, Module secondSpec) {
-        throw new UnsupportedOperationException();
-      }
     };
   }
 

diff --git a/k-distribution/src/test/java/org/kframework/kore/convertors/BaseTest.java b/k-distribution/src/test/java/org/kframework/kore/convertors/BaseTest.java
@@ -99,7 +99,6 @@ protected DefinitionWithContext parseUsingOuter(File definitionFile) {
     }
     def.setItems(Outer.parse(Source.apply(definitionFile.getPath()), definitionText, null));
     def.setMainModule("TEST");
-    def.setMainSyntaxModule("TEST");
 
     ProcessGroupAttributes.apply(def);
     Context context = new Context();

diff --git a/k-distribution/src/test/java/org/kframework/kore/convertors/TstKILtoKOREIT.java b/k-distribution/src/test/java/org/kframework/kore/convertors/TstKILtoKOREIT.java
@@ -60,7 +60,7 @@ public void syntaxWithOR() throws IOException {
   }
 
   protected String convert(DefinitionWithContext defWithContext) {
-    KILtoKORE kilToKore = new KILtoKORE(defWithContext.context, false, false);
+    KILtoKORE kilToKore = new KILtoKORE(defWithContext.context, false);
     org.kframework.definition.Definition koreDef = kilToKore.apply(defWithContext.definition);
     String koreDefString = koreDef.toString();
     return koreDefString;

diff --git a/kernel/src/main/java/org/kframework/backend/Backends.java b/kernel/src/main/java/org/kframework/backend/Backends.java
@@ -2,9 +2,6 @@
 package org.kframework.backend;
 
 public class Backends {
-
-  public static final String PDF = "pdf";
-  public static final String HTML = "html";
   public static final String HASKELL = "haskell";
   public static final String LLVM = "llvm";
 }
diff --git a/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java b/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java
@@ -27,7 +27,7 @@
 import org.kframework.utils.file.FileUtil;
 import scala.Function1;
 
-public class KoreBackend extends AbstractBackend {
+public class KoreBackend implements Backend {
 
   private final KompileOptions kompileOptions;
   protected final FileUtil files;
@@ -57,20 +57,16 @@ public KoreBackend(
   @Override
   public void accept(Backend.Holder h) {
     CompiledDefinition def = h.def;
-    String kore = getKompiledString(def, true);
+    String kore = getKompiledString(def);
     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.
-   *
-   * @param hasAnd whether the backend in question supports and-patterns during pattern matching.
-   */
-  protected String getKompiledString(CompiledDefinition def, boolean hasAnd) {
-    Module mainModule = getKompiledModule(def.kompiledDefinition.mainModule(), hasAnd);
+  /** Convert a CompiledDefinition to a String of a KORE definition. */
+  protected String getKompiledString(CompiledDefinition def) {
+    Module mainModule = getKompiledModule(def.kompiledDefinition.mainModule());
     ModuleToKORE converter =
         new ModuleToKORE(mainModule, def.topCellInitializer, def.kompileOptions);
     return getKompiledString(converter, files, heatCoolEquations, tool);
@@ -98,20 +94,18 @@ public static String getKompiledStringAndWriteSyntaxMacros(
     return semantics.toString();
   }
 
-  public static Module getKompiledModule(Module mainModule, boolean hasAnd) {
+  public static Module getKompiledModule(Module mainModule) {
     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);
-    if (hasAnd) {
-      mainModule =
-          ModuleTransformer.fromSentenceTransformer(
-                  new MinimizeTermConstruction(mainModule)::resolve, "Minimize term construction")
-              .apply(mainModule);
-    }
+    mainModule =
+        ModuleTransformer.fromSentenceTransformer(
+                new MinimizeTermConstruction(mainModule)::resolve, "Minimize term construction")
+            .apply(mainModule);
     return mainModule;
   }
 
@@ -123,8 +117,7 @@ public Function<Definition, Definition> steps() {
     Function1<Definition, Definition> resolveStrict =
         d ->
             DefinitionTransformer.from(
-                    new ResolveStrict(kompileOptions, d)::resolve,
-                    "resolving strict and seqstrict attributes")
+                    new ResolveStrict(d)::resolve, "resolving strict and seqstrict attributes")
                 .apply(d);
     DefinitionTransformer resolveHeatCoolAttribute =
         DefinitionTransformer.fromSentenceTransformer(
@@ -240,7 +233,7 @@ public Function<Definition, Definition> steps() {
             .andThen(resolveFunctionWithConfig)
             .andThen(resolveStrict)
             .andThen(resolveAnonVars)
-            .andThen(d -> new ResolveContexts(kompileOptions).resolve(d))
+            .andThen(d -> new ResolveContexts().resolve(d))
             .andThen(numberSentences)
             .andThen(resolveHeatCoolAttribute)
             .andThen(resolveSemanticCasts)

diff --git a/kernel/src/main/java/org/kframework/compile/AbstractBackend.java b/kernel/src/main/java/org/kframework/compile/AbstractBackend.java
diff --git a/kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java b/kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java
@@ -27,15 +27,6 @@ public static Definition transformDefinition(Definition input) {
         .apply(input);
   }
 
-  public static Module transformModule(Module mod) {
-    ConfigurationInfoFromModule configInfo = new ConfigurationInfoFromModule(mod);
-    LabelInfo labelInfo = new LabelInfoFromModule(mod);
-    return ModuleTransformer.fromSentenceTransformer(
-            new AddImplicitComputationCell(configInfo, labelInfo)::apply,
-            "concretizing configuration")
-        .apply(mod);
-  }
-
   public Sentence apply(Module m, Sentence s) {
     if (skipSentence(s)) {
       return s;

diff --git a/kernel/src/main/java/org/kframework/compile/AddImplicitCounterCell.java b/kernel/src/main/java/org/kframework/compile/AddImplicitCounterCell.java
@@ -7,7 +7,6 @@
 import java.util.*;
 import org.kframework.builtin.KLabels;
 import org.kframework.definition.Claim;
-import org.kframework.definition.Module;
 import org.kframework.definition.Sentence;
 import org.kframework.kore.*;
 
@@ -19,7 +18,7 @@ public class AddImplicitCounterCell {
 
   public AddImplicitCounterCell() {}
 
-  public Sentence apply(Module m, Sentence s) {
+  public Sentence apply(Sentence s) {
     if (s instanceof Claim claim) {
       Set<KVariable> freshVars = new HashSet<>();
       VisitK visitor =
@@ -36,8 +35,7 @@ public void apply(KVariable var) {
       if (!ConcretizeCells.hasCells(claim.body()) && freshVars.isEmpty()) {
         return s;
       }
-      return claim.newInstance(
-          apply(claim.body(), m), claim.requires(), claim.ensures(), claim.att());
+      return claim.newInstance(apply(claim.body()), claim.requires(), claim.ensures(), claim.att());
     }
     return s;
   }
@@ -50,7 +48,7 @@ private boolean alreadyHasGeneratedCounter(List<K> items) {
         .anyMatch(cell -> ((KApply) cell).klabel().equals(KLabels.GENERATED_COUNTER_CELL));
   }
 
-  private K apply(K term, Module m) {
+  private K apply(K term) {
     List<K> items = IncompleteCellUtils.flattenCells(term);
     if (alreadyHasGeneratedCounter(items)) {
       return term;

diff --git a/kernel/src/main/java/org/kframework/compile/AddSortInjections.java b/kernel/src/main/java/org/kframework/compile/AddSortInjections.java
@@ -15,12 +15,10 @@
 import java.util.Set;
 import java.util.function.BiFunction;
 import java.util.stream.Collectors;
-import java.util.stream.IntStream;
 import org.kframework.Collections;
 import org.kframework.attributes.Att;
 import org.kframework.attributes.HasLocation;
 import org.kframework.builtin.Sorts;
-import org.kframework.definition.Context;
 import org.kframework.definition.Module;
 import org.kframework.definition.NonTerminal;
 import org.kframework.definition.Production;
@@ -40,7 +38,6 @@
 import org.kframework.parser.outer.Outer;
 import org.kframework.utils.errorsystem.KEMException;
 import scala.Option;
-import scala.Tuple2;
 
 public class AddSortInjections {
 
@@ -174,7 +171,6 @@ private K internalAddSortInjections(K term, Sort expectedSort) {
                   adjustedExpectedSort = k.att().get(Sort.class);
                 }
                 Production prod = production(k);
-                List<K> children = new ArrayList<>();
                 Production substituted =
                     substituteProd(
                         prod,
@@ -206,13 +202,6 @@ private K internalAddSortInjections(K term, Sort expectedSort) {
     }
   }
 
-  private Context addInjections(Context context) {
-    return new Context(
-        internalAddSortInjections(context.body(), Sorts.K()),
-        internalAddSortInjections(context.requires(), Sorts.Bool()),
-        context.att());
-  }
-
   private void initSortParams() {
     freshSortParamCounter = 0;
     sortParams.clear();
@@ -355,14 +344,6 @@ private void match(
     }
   }
 
-  private Set<Integer> getPositions(Sort param, Production prod) {
-    return IntStream.range(0, prod.nonterminals().size())
-        .mapToObj(i -> Tuple2.apply(prod.nonterminals().apply(i), i))
-        .filter(t -> t._1().sort().equals(param))
-        .map(t -> t._2())
-        .collect(Collectors.toSet());
-  }
-
   /**
    * Compute the sort of a term in a context where there is no expected sort, i.e., at the top of a
    * rule body.

diff --git a/kernel/src/main/java/org/kframework/compile/Backend.java b/kernel/src/main/java/org/kframework/compile/Backend.java
@@ -1,10 +1,8 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 package org.kframework.compile;
 
-import java.util.List;
 import java.util.Set;
 import java.util.function.Function;
-import javax.annotation.Nullable;
 import org.kframework.attributes.Att;
 import org.kframework.definition.Definition;
 import org.kframework.definition.Module;
@@ -26,9 +24,6 @@ public Holder(CompiledDefinition def) {
 
   Function<Definition, Definition> steps();
 
-  Function<Definition, Definition> proofDefinitionNonCachedSteps(
-      @Nullable List<String> extraConcreteRuleLabels);
-
   Function<Module, Module> specificationSteps(Definition def);
 
   Set<Att.Key> excludedModuleTags();

diff --git a/kernel/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java b/kernel/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java
@@ -6,7 +6,6 @@
 import edu.uci.ics.jung.graph.DirectedGraph;
 import edu.uci.ics.jung.graph.DirectedSparseGraph;
 import java.util.Collection;
-import java.util.Collections;
 import java.util.HashSet;
 import java.util.LinkedHashSet;
 import java.util.LinkedList;
@@ -99,10 +98,6 @@ private static <V> Set<V> ancestors(
     return visited;
   }
 
-  public Set<KLabel> ancestors(KLabel label) {
-    return ancestors(Collections.singleton(label), dependencies);
-  }
-
   public Set<KLabel> ancestors(Set<KLabel> labels) {
     return ancestors(labels, dependencies);
   }