Apply Java 17 automatic migration: records

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,9 +46,8 @@ public Boolean unit() {
 
             @Override
             public Boolean apply(KApply k) {
-                if (mod.attributesFor().get(k.klabel()).getOrElse(() -> Att.empty()).contains(Att.MAINCELL())) {
-                    if (k.items().get(0) instanceof KSequence) {
-                        KSequence seq = (KSequence) k.items().get(0);
+                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,24 +35,14 @@ 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;
         }
 
-        if (s instanceof RuleOrClaim) {
-            RuleOrClaim rule = (RuleOrClaim) s;
+        if (s instanceof RuleOrClaim rule) {
             return rule.newInstance(apply(rule.body(), m, rule instanceof Claim), rule.requires(), rule.ensures(), rule.att());
-        } else if (s instanceof Context) {
-            Context context = (Context) s;
+        } else if (s instanceof Context context) {
             return new Context(apply(context.body(), m, false), context.requires(), context.att());
         } else {
             return s;
@@ -74,8 +64,7 @@ private boolean shouldConsider(List<K> items, boolean isClaim) {
             return true;
         } else if (items.size() == 2 && isClaim) {
             K second = items.get(1);
-            if(second instanceof KApply) {
-                KApply app = (KApply) second;
+            if(second instanceof KApply app) {
                 return app.klabel() == KLabels.GENERATED_COUNTER_CELL;
             }
         }
@@ -88,8 +77,7 @@ private boolean canAddImplicitKCell(K item) {
             return false;
         }
 
-        if (item instanceof KRewrite) {
-            final KRewrite rew = (KRewrite) item;
+        if (item instanceof final KRewrite rew) {
             return Stream.concat(
                             IncompleteCellUtils.flattenCells(rew.left()).stream(),
                             IncompleteCellUtils.flattenCells(rew.right()).stream())

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;
 
@@ -92,8 +84,7 @@ protected K addRootCell(K term) {
         }
 
         // KRewrite instance
-        if (term instanceof KRewrite) {
-            KRewrite rew = (KRewrite) term;
+        if (term instanceof KRewrite rew) {
             K left = addRootCell(rew.left());
             if (left == rew.left()) {
                 return KRewrite(rew.left(), rew.right());

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

@@ -196,7 +196,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));
                 }
@@ -278,7 +278,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;
         }