Apply Java 17 automatic migration: records (#3746)

This PR applies automatic fixes suggested by IntelliJ to refactor Java
`class`es into `record`s, which reduces boilerplate code in a lot of
different places.

The changes made are large, but I have split the changes up so that each
commit deals only with a single class at a time, along with any
downstream changes required by making that class a record. In some
cases, I have applied small fix-its suggested by IntelliJ as well as the
record transformation.

I'm happy to bikeshed whether any of these cases should remain a class
rather than a record, and the commit history means that reverting an
individual case is easy should we decide to do so.

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

@@ -55,45 +55,22 @@
 import static org.kframework.builtin.BooleanUtils.*;
 
 @RequestScoped
-public class HaskellRewriter implements Function<Definition, Rewriter> {
-
-    private final GlobalOptions globalOptions;
-    private final SMTOptions smtOptions;
-    private final KompileOptions kompileOptions;
-    private final KProveOptions kProveOptions;
-    private final HaskellKRunOptions haskellKRunOptions;
-    private final BackendOptions backendOptions;
-    private final FileUtil files;
-    private final CompiledDefinition def;
-    private final KExceptionManager kem;
-    private final KPrint kprint;
-    private final Tool tool;
+public record HaskellRewriter(
+     GlobalOptions globalOptions,
+     SMTOptions smtOptions,
+     KompileOptions kompileOptions,
+     KProveOptions kProveOptions,
+     HaskellKRunOptions haskellKRunOptions,
+     BackendOptions backendOptions,
+     FileUtil files,
+     CompiledDefinition def,
+     KExceptionManager kem,
+     KPrint kprint,
+     Tool tool
+) implements Function<Definition, Rewriter> {
 
     @Inject
-    public HaskellRewriter(
-            GlobalOptions globalOptions,
-            SMTOptions smtOptions,
-            KompileOptions kompileOptions,
-            KProveOptions kProveOptions,
-            HaskellKRunOptions haskellKRunOptions,
-            BackendOptions backendOptions,
-            FileUtil files,
-            CompiledDefinition def,
-            KExceptionManager kem,
-            KPrint kprint,
-            Tool tool) {
-        this.globalOptions = globalOptions;
-        this.smtOptions = smtOptions;
-        this.haskellKRunOptions = haskellKRunOptions;
-        this.backendOptions = backendOptions;
-        this.kompileOptions = kompileOptions;
-        this.kProveOptions = kProveOptions;
-        this.files = files;
-        this.def = def;
-        this.kem = kem;
-        this.kprint = kprint;
-        this.tool = tool;
-    }
+    public HaskellRewriter {}
 
     @Override
     public Rewriter apply(Definition definition) {
@@ -294,8 +271,7 @@ private String saveKoreSpecToTemp(ModuleToKORE converter, Module rules) {
                 String koreOutput = converter.convertSpecificationModule(module, rules,
                         haskellKRunOptions.defaultClaimType, sb);
                 files.saveToTemp("spec.kore", koreOutput);
-                String specPath = files.resolveTemp("spec.kore").getAbsolutePath();
-                return specPath;
+                return files.resolveTemp("spec.kore").getAbsolutePath();
             }
 
             private List<String> buildCommonProvingCommand(String defPath, String specPath, String outPath,
@@ -393,8 +369,7 @@ public RewriterResult prove(Module rules, Boolean reuseDef) {
                     System.err.println("Executing " + args);
                 }
 
-                RewriterResult result = executeKoreCommands(rules, koreCommand, koreDirectory, koreOutputFile);
-                return result;
+                return executeKoreCommands(rules, koreCommand, koreDirectory, koreOutputFile);
             }
 
             @Override
@@ -456,7 +431,7 @@ private int executeCommandBasic(File workingDir, String... command) throws IOExc
                         p2.getOutputStream().write(buffer, 0, count);
                         p2.getOutputStream().flush();
                     }
-                } catch (IOException e) {}
+                } catch (IOException ignored) {}
             });
             Thread out = RunProcess.getOutputStreamThread(p2::getInputStream, System.out);
             Thread err = RunProcess.getOutputStreamThread(p2::getErrorStream, System.err);

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

@@ -13,13 +13,7 @@
 import org.kframework.kore.KVariable;
 import org.kframework.kore.FoldK;
 
-public class AddCoolLikeAtt {
-
-    private final Module mod;
-
-    public AddCoolLikeAtt(Module mod) {
-      this.mod = mod;
-    }
+public record AddCoolLikeAtt(Module mod) {
 
     private Rule add(Rule rule) {
         return new Rule(
@@ -52,7 +46,7 @@ public Boolean unit() {
 
             @Override
             public Boolean apply(KApply k) {
-                if (mod.attributesFor().get(k.klabel()).getOrElse(() -> Att.empty()).contains(Att.MAINCELL())) {
+                if (mod.attributesFor().get(k.klabel()).getOrElse(Att::empty).contains(Att.MAINCELL())) {
                     if (k.items().get(0) instanceof KSequence seq) {
                         if (seq.items().size() > 1 && seq.items().get(0) instanceof KVariable) {
                             return true;

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

@@ -17,7 +17,7 @@
  *  If a SemanticSentence (Rule or Context) has a body that is not wrapped in any cell,
  *  wrap it in a {@code <k>} cell
  */
-public class AddImplicitComputationCell {
+public record AddImplicitComputationCell(ConfigurationInfo cfg, LabelInfo labelInfo) {
 
     public static Definition transformDefinition(Definition input) {
         ConfigurationInfoFromModule configInfo = new ConfigurationInfoFromModule(input.mainModule());
@@ -35,14 +35,6 @@ public static Module transformModule(Module mod) {
                 "concretizing configuration").apply(mod);
     }
 
-    private final ConfigurationInfo cfg;
-    private final LabelInfo labelInfo;
-
-    public AddImplicitComputationCell(ConfigurationInfo cfg, LabelInfo labelInfo) {
-        this.cfg = cfg;
-        this.labelInfo = labelInfo;
-    }
-
     public Sentence apply(Module m, Sentence s) {
         if (skipSentence(s)) {
             return s;

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

@@ -175,7 +175,7 @@ Optional<Integer> getLevel(K k) {
         } else if (k instanceof KVariable) {
             if (k.att().contains(Sort.class)) {
                 Sort sort = k.att().get(Sort.class);
-                int level = cfg.cfg.getLevel(sort);
+                int level = cfg.cfg().getLevel(sort);
                 if (level >= 0) {
                     return Optional.of(level);
                 }

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

@@ -31,22 +31,14 @@
  * Rules with the anywhere attribute are not modified.
  */
 // TODO: rules defining functions shouldn't be wrapped
-public class AddTopCellToRules {
-
-    private final ConfigurationInfo cfg;
-    private final LabelInfo labelInfo;
-
-    public AddTopCellToRules(ConfigurationInfo cfg, LabelInfo labelInfo) {
-        this.cfg = cfg;
-        this.labelInfo = labelInfo;
-    }
+public record AddTopCellToRules(ConfigurationInfo cfg, LabelInfo labelInfo) {
 
     public K addImplicitCells(K term, Module m) {
         if (m.isFunction(term)) return term;
         return addRootCell(term);
     }
 
-    protected K addRootCell(K term) {
+    private K addRootCell(K term) {
         KLabel root;
         root = KLabels.GENERATED_TOP_CELL;
 

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

@@ -195,7 +195,7 @@ protected KApply closeCell(KApply cell) {
                 List<K> newContents = new ArrayList<>(contents.size() + requiredLeft.size());
                 newContents.addAll(contents);
                 for (Sort reqChild : requiredLeft) {
-                    if (!cfg.cfg.isConstantInitializer(reqChild))
+                    if (!cfg.cfg().isConstantInitializer(reqChild))
                         throw KEMException.compilerError("Cannot close cell on right hand side because the initializer for " + reqChild.toString() + " requires configuration variables.");
                     newContents.add(cfg.getDefaultCell(reqChild));
                 }
@@ -277,7 +277,7 @@ private void filterRequired(Set<Sort> required, K item) {
         } else if (item instanceof KVariable) {
             if (item.att().contains(Sort.class)) {
                 Sort sort = item.att().get(Sort.class);
-                if (cfg.cfg.isCell(sort)) {
+                if (cfg.cfg().isCell(sort)) {
                     required.remove(sort);
                 } else {
                     required.clear();

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

@@ -15,15 +15,7 @@
 /**
  * Created by brandon on 3/31/15.
  */
-public class ConcretizationInfo {
-    public final ConfigurationInfo cfg;
-    private final LabelInfo labels;
-
-    public ConcretizationInfo(ConfigurationInfo cfg, LabelInfo labels) {
-        this.cfg = cfg;
-        this.labels = labels;
-    }
-
+public record ConcretizationInfo(ConfigurationInfo cfg, LabelInfo labels) {
 
     public Sort getCellSort(K k) {
         if (k instanceof KApply) {

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

@@ -11,19 +11,14 @@
 import org.kframework.utils.StringUtil;
 import org.kframework.utils.file.FileUtil;
 
-import static org.kframework.kore.KORE.*;
+import java.io.File;
 
-public class GenerateCoverage {
-    private final boolean cover;
-    private final FileUtil files;
+import static org.kframework.kore.KORE.*;
 
-    public GenerateCoverage(boolean cover, FileUtil files) {
-        this.cover = cover;
-        this.files = files;
-    }
+public record GenerateCoverage(boolean cover, FileUtil files) {
 
     public K gen(RuleOrClaim r, K body, Module mod) {
-        if (!cover || !r.att().getOptional(Source.class).isPresent()) {
+        if (!cover || r.att().getOptional(Source.class).isEmpty()) {
             return body;
         }
         K left = RewriteToTop.toLeft(body);

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

@@ -5,20 +5,14 @@
 import org.kframework.definition.Module;
 import org.kframework.definition.Rule;
 import org.kframework.definition.Sentence;
-import org.kframework.kore.KLabel;
 
 /**
  * Propagate macro, macro-rec, alias, and alias-rec labels from productions to rules that only contain that klabel on the LHS
  * This prepares rules for macro expansion in ExpandMacros.
  * There is one exception: simplification rules are meant to be used for the haskell backend and macros should not be propagated
  * to these rules.
  */
-public class PropagateMacro {
-    private final Module m;
-
-    public PropagateMacro(Module m) {
-        this.m = m;
-    }
+public record PropagateMacro(Module m) {
 
     public Sentence propagate(Sentence s) {
         if (s instanceof Rule && m.ruleLhsHasMacroKLabel((Rule) s) && !((Rule) s).att().contains(Att.SIMPLIFICATION())) {

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

@@ -23,15 +23,7 @@
 import static org.kframework.Collections.stream;
 import static org.kframework.definition.Constructors.Module;
 
-public class ResolveComm {
-
-
-    private final KExceptionManager kem;
-
-
-    public ResolveComm(KExceptionManager kem) {
-        this.kem = kem;
-    }
+public record ResolveComm(KExceptionManager kem) {
 
 
     public Module resolve(Module m) {

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

@@ -2,7 +2,6 @@
 package org.kframework.compile;
 
 import org.kframework.attributes.Att;
-import org.kframework.attributes.Att.Key;
 import org.kframework.builtin.BooleanUtils;
 import org.kframework.definition.Context;
 import org.kframework.definition.Module;
@@ -20,13 +19,7 @@
 import static org.kframework.definition.Constructors.*;
 import static org.kframework.kore.KORE.*;
 
-public class ResolveHeatCoolAttribute {
-
-    private final Set<String> unrestrictedRules;
-
-    public ResolveHeatCoolAttribute(Set<String> unrestrictedRules) {
-        this.unrestrictedRules = unrestrictedRules;
-    }
+public record ResolveHeatCoolAttribute(Set<String> unrestrictedRules) {
 
     private Rule resolve(Module m, Rule rule) {
         return Rule(
@@ -70,10 +63,10 @@ public Sentence resolve(Module m, Sentence s) {
         if (!s.att().contains(Att.HEAT()) && !s.att().contains(Att.COOL())) {
             return s;
         }
-        if (s instanceof Rule) {
-            return resolve(m, (Rule) s);
-        } else if (s instanceof Context) {
-            return resolve(m, (Context) s);
+        if (s instanceof Rule r) {
+            return resolve(m, r);
+        } else if (s instanceof Context c) {
+            return resolve(m, c);
         } else {
             return s;
         }

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

@@ -37,16 +37,8 @@
 /**
  * Created by daejunpark on 9/6/15.
  */
-public class ResolveIOStreams {
-
-    private final Definition definition;
-
-    private final KExceptionManager kem;
-
-    public ResolveIOStreams(Definition definition, KExceptionManager kem) {
-        this.definition = definition;
-        this.kem = kem;
-    }
+public record ResolveIOStreams(Definition definition,
+                               KExceptionManager kem) {
 
     /**
      * Update modules that declare stream cells in configuration,
@@ -83,7 +75,7 @@ public Module resolve(Module m) {
                     sentences.addAll(getStreamModuleSentences(p));
                 }
             }
-            return Module(m.name(), (Set<Import>)m.imports().
+            return Module(m.name(), (Set<Import>) m.imports().
                             $bar(Set(Import(definition.getModule("K-IO").get(), true))).
                             $bar(Set(Import(definition.getModule("K-REFLECTION").get(), true))),
                     immutable(sentences), m.att());
@@ -164,8 +156,7 @@ private KList getContentsOfInitRule(Production streamProduction) {
 
         java.util.List<Sentence> initRules =
                 stream(getStreamModule(streamName).localSentences())
-                        .filter(s -> isInitRule(initLabel, cellLabel, s))
-                        .collect(Collectors.toList());
+                        .filter(s -> isInitRule(initLabel, cellLabel, s)).toList();
         assert initRules.size() == 1;
         Sentence initRule = initRules.get(0);
 
@@ -388,8 +379,7 @@ private K getUnblockRuleBody(Production streamProduction, String sort) {
         KLabel userCellLabel = streamProduction.klabel().get(); // <in>
 
         java.util.List<Sentence> unblockRules = stream(getStreamModule(streamName).localSentences())
-                .filter(s -> s instanceof Rule && s.att().getOptional(Att.LABEL()).map(lbl -> lbl.equals("STDIN-STREAM.stdinUnblock")).orElse(false))
-                .collect(Collectors.toList());
+                .filter(s -> s instanceof Rule && s.att().getOptional(Att.LABEL()).map(lbl -> lbl.equals("STDIN-STREAM.stdinUnblock")).orElse(false)).toList();
         assert unblockRules.size() == 1;
         Rule unblockRule = (Rule) unblockRules.get(0);