Delete statically dead code (#3967)

As part of the cleanup discussed in #3891, this PR removes statically
dead code as identified by IntelliJ.

IntelliJ's analysis reports some false positives, e.g. with dependency
injection and usages in Scala code, so I had to manually review and
delete everything. It also seems to miss some dead Scala code.

The "Batch N" commits just delete dead code, while the following commits
perform some easy simplifications I noticed.

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");

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);
 

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();
-      }
     };
   }
 

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();

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;

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";
 }

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)

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;

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;

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.

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();

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);
   }