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 index cc95b117946..0c5c7e4a435 100644 --- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java +++ b/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 { - - 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 { @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 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); diff --git a/kernel/src/main/java/org/kframework/compile/AddCoolLikeAtt.java b/kernel/src/main/java/org/kframework/compile/AddCoolLikeAtt.java index 12c63782981..983aff86842 100644 --- a/kernel/src/main/java/org/kframework/compile/AddCoolLikeAtt.java +++ b/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; diff --git a/kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java b/kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java index 195f1a22053..78a23aea541 100644 --- a/kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java +++ b/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 } 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; diff --git a/kernel/src/main/java/org/kframework/compile/AddParentCells.java b/kernel/src/main/java/org/kframework/compile/AddParentCells.java index 7d206e1dbb9..3fd42ce8d18 100644 --- a/kernel/src/main/java/org/kframework/compile/AddParentCells.java +++ b/kernel/src/main/java/org/kframework/compile/AddParentCells.java @@ -175,7 +175,7 @@ Optional 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); } diff --git a/kernel/src/main/java/org/kframework/compile/AddTopCellToRules.java b/kernel/src/main/java/org/kframework/compile/AddTopCellToRules.java index 51d83c83165..5b8aff5f585 100644 --- a/kernel/src/main/java/org/kframework/compile/AddTopCellToRules.java +++ b/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; diff --git a/kernel/src/main/java/org/kframework/compile/CloseCells.java b/kernel/src/main/java/org/kframework/compile/CloseCells.java index 42c43928de6..a0d17fa2e7b 100644 --- a/kernel/src/main/java/org/kframework/compile/CloseCells.java +++ b/kernel/src/main/java/org/kframework/compile/CloseCells.java @@ -195,7 +195,7 @@ protected KApply closeCell(KApply cell) { List 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 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(); diff --git a/kernel/src/main/java/org/kframework/compile/ConcretizationInfo.java b/kernel/src/main/java/org/kframework/compile/ConcretizationInfo.java index 38d46082adc..696da3ca5c5 100644 --- a/kernel/src/main/java/org/kframework/compile/ConcretizationInfo.java +++ b/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) { diff --git a/kernel/src/main/java/org/kframework/compile/GenerateCoverage.java b/kernel/src/main/java/org/kframework/compile/GenerateCoverage.java index f4f951bfdb5..28c601891a9 100644 --- a/kernel/src/main/java/org/kframework/compile/GenerateCoverage.java +++ b/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); diff --git a/kernel/src/main/java/org/kframework/compile/PropagateMacro.java b/kernel/src/main/java/org/kframework/compile/PropagateMacro.java index 1fb4805e582..c41d1cccd6e 100644 --- a/kernel/src/main/java/org/kframework/compile/PropagateMacro.java +++ b/kernel/src/main/java/org/kframework/compile/PropagateMacro.java @@ -5,7 +5,6 @@ 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 @@ -13,12 +12,7 @@ * 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())) { diff --git a/kernel/src/main/java/org/kframework/compile/ResolveComm.java b/kernel/src/main/java/org/kframework/compile/ResolveComm.java index 08e9523a96e..d393b267e5b 100644 --- a/kernel/src/main/java/org/kframework/compile/ResolveComm.java +++ b/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) { diff --git a/kernel/src/main/java/org/kframework/compile/ResolveHeatCoolAttribute.java b/kernel/src/main/java/org/kframework/compile/ResolveHeatCoolAttribute.java index 1d817f61c40..7c26aa291f7 100644 --- a/kernel/src/main/java/org/kframework/compile/ResolveHeatCoolAttribute.java +++ b/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 unrestrictedRules; - - public ResolveHeatCoolAttribute(Set unrestrictedRules) { - this.unrestrictedRules = unrestrictedRules; - } +public record ResolveHeatCoolAttribute(Set 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; } diff --git a/kernel/src/main/java/org/kframework/compile/ResolveIOStreams.java b/kernel/src/main/java/org/kframework/compile/ResolveIOStreams.java index 5c6a5f78544..42f0908cf15 100644 --- a/kernel/src/main/java/org/kframework/compile/ResolveIOStreams.java +++ b/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)m.imports(). + return Module(m.name(), (Set) 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 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(); // java.util.List 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); diff --git a/kernel/src/main/java/org/kframework/compile/SortCells.java b/kernel/src/main/java/org/kframework/compile/SortCells.java index 31bd73ee1b3..a5f41346c40 100644 --- a/kernel/src/main/java/org/kframework/compile/SortCells.java +++ b/kernel/src/main/java/org/kframework/compile/SortCells.java @@ -141,7 +141,7 @@ void addOccurances(KLabel cell, KVariable var, List items) { } if (var.att().contains(Sort.class)) { Sort sort = var.att().get(Sort.class); - if (cfg.cfg.isCell(sort)) { + if (cfg.cfg().isCell(sort)) { remainingCells.removeIf(s -> !s.equals(sort)); } } @@ -174,7 +174,7 @@ K replacementTerm() { if (cfg.getMultiplicity(child) == Multiplicity.ONE) { arg = cfg.getCellAbsentTerm(child); } else { - arg = cfg.cfg.getUnit(child); + arg = cfg.cfg().getUnit(child); } } assert arg != null; @@ -277,7 +277,7 @@ private void processSide(KApply parentCell, boolean allowRhs, List items) { if (item instanceof KVariable var) { if (var.att().contains(Sort.class)) { Sort sort = var.att().get(Sort.class); - if (cfg.cfg.isCell(sort)) { + if (cfg.cfg().isCell(sort)) { if (!cellVariables.getOrDefault(var, sort).equals(sort)) { Sort prevSort = cellVariables.get(var); throw KEMException.compilerError("Variable "+var+" occurs annotated as multiple cell sorts, "+sort+" and "+prevSort, @@ -333,7 +333,7 @@ public void apply(KVariable k) { private Sort getPredicateSort(Sort s) { if (cfg.getMultiplicity(s) == Multiplicity.STAR) { - scala.collection.Set sorts = cfg.cfg.getCellBagSortsOfCell(s); + scala.collection.Set sorts = cfg.cfg().getCellBagSortsOfCell(s); if (sorts.size() != 1) { throw KEMException.compilerError("Expected exactly one cell collection sort for the sort " + s + "; found " + sorts); } @@ -407,7 +407,7 @@ public K apply(KApply k) { if (cfg.getMultiplicity(sort) == Multiplicity.ONE) { throw KEMException.compilerError("Missing cell of multiplicity=\"1\": " + sort, k); } else { - ordered.set(indexOf(order, sort, k), cfg.cfg.getUnit(sort)); + ordered.set(indexOf(order, sort, k), cfg.cfg().getUnit(sort)); } }); return KApply(k.klabel(), KList(ordered), k.att()); @@ -471,9 +471,9 @@ private K concatenateStarCells(Sort sort, List children) { + "into a cell collection.", children.iterator().next()); } if (children.size() == 0) { - return cfg.cfg.getUnit(sort); + return cfg.cfg().getUnit(sort); } - KLabel concat = cfg.cfg.getConcat(sort); + KLabel concat = cfg.cfg().getConcat(sort); int ix = children.size(); K result = children.get(--ix); while (ix > 0) { @@ -487,7 +487,7 @@ private void addDefaultCells(K item, Map splitLeft, Map splitR if (cfg.getMultiplicity(s) == Multiplicity.ONE) { throw KEMException.compilerError("Cannot rewrite a multiplicity=\"1\" cell to or from the cell unit.", item); } else { - splitRight.put(s, cfg.cfg.getUnit(s)); + splitRight.put(s, cfg.cfg().getUnit(s)); } } } @@ -583,7 +583,7 @@ public K apply(KApply k0) { if (cellFragmentSort.name().endsWith("Fragment")) { Sort cellSort = Sort(cellFragmentSort.name().substring(0,cellFragmentSort.name().indexOf("Fragment"))); - KLabel cellLabel = cfg.cfg.getCellLabel(cellSort); + KLabel cellLabel = cfg.cfg().getCellLabel(cellSort); List subcellSorts = cfg.getChildren(cellLabel); @@ -608,7 +608,7 @@ public K apply(KApply k0) { ArrayList klist = new ArrayList(Collections.nCopies(subcellSorts.size(), null)); for (K item : IncompleteCellUtils.flattenCells(k)) { // #cells(#cells(x,y),z) => [x,y,z] if (item instanceof KApply kapp) { - if (cfg.cfg.isCellLabel(kapp.klabel())) { + if (cfg.cfg().isCellLabel(kapp.klabel())) { Sort sort = cfg.getCellSort(kapp.klabel()); if (!subcellSorts.contains(sort)) { throw new IllegalArgumentException("No such sub-cell " + sort + " in the cell " + cellLabel); @@ -632,7 +632,7 @@ public K apply(KApply k0) { } if (var.att().contains(Sort.class)) { Sort sort = var.att().get(Sort.class); - if (cfg.cfg.isCell(sort)) { + if (cfg.cfg().isCell(sort)) { if (!subcellSorts.contains(sort)) { throw new IllegalArgumentException("No such sub-cell " + sort + " in the cell " + cellLabel); } @@ -641,7 +641,7 @@ public K apply(KApply k0) { // if the variable is not explicitly sort-casted, then its sort information should be found in other places if (varinfo != null && varinfo.remainingCells != null && varinfo.remainingCells.size() == 1) { Sort s = Iterables.getOnlyElement(varinfo.remainingCells); - if (cfg.cfg.isCell(s)) { + if (cfg.cfg().isCell(s)) { if (!subcellSorts.contains(s)) { throw new IllegalArgumentException("No such sub-cell " + s + " in the cell " + cellLabel); } @@ -669,7 +669,7 @@ public K apply(KApply k0) { if (cfg.getMultiplicity(subcellSorts.get(i)) == Multiplicity.ONE) { klist.set(i, cfg.getCellAbsentTerm(subcellSorts.get(i))); } else { // Multiplicity.OPTIONAL || Multiplicity.STAR - klist.set(i, cfg.cfg.getUnit(subcellSorts.get(i))); + klist.set(i, cfg.cfg().getUnit(subcellSorts.get(i))); } } @@ -743,7 +743,7 @@ public void apply(KApply k) { if (item instanceof KVariable var) { if (var.att().contains(Sort.class)) { Sort sort = var.att().get(Sort.class); - if (!cfg.cfg.isCell(sort)) { + if (!cfg.cfg().isCell(sort)) { if (!cellFragmentVars.containsKey(var)) { cellFragmentVars.put(var, new HashSet<>()); } @@ -818,7 +818,7 @@ public K apply(KApply k0) { } if (cellFragmentSort.name().endsWith("Fragment")) { Sort cellSort = Sort(cellFragmentSort.name().substring(0,cellFragmentSort.name().indexOf("Fragment"))); - KLabel cellLabel = cfg.cfg.getCellLabel(cellSort); + KLabel cellLabel = cfg.cfg().getCellLabel(cellSort); klist0.set(idx, KApply(cellLabel, KList(item0), Att().add(Att.DUMMY_CELL()))); } } diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckAssoc.java b/kernel/src/main/java/org/kframework/compile/checks/CheckAssoc.java index 6b763df6334..eea4f51f14e 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckAssoc.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckAssoc.java @@ -18,14 +18,7 @@ * - if right, then A <= B * - if non-assoc, then A <= B and A <= C */ -public class CheckAssoc { - private final Set errors; - private final Module module; - - public CheckAssoc(Set errors, Module module) { - this.errors = errors; - this.module = module; - } +public record CheckAssoc(Set errors, Module module) { public void check(Sentence s) { if (s instanceof Production p) { diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckFunctions.java b/kernel/src/main/java/org/kframework/compile/checks/CheckFunctions.java index 967bc92a781..8c727c51037 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckFunctions.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckFunctions.java @@ -19,14 +19,7 @@ /** * Check that functions are not used on LHS in places that should be performing matching. */ -public class CheckFunctions { - private final Set errors; - private final Module m; - - public CheckFunctions(Set errors, Module m) { - this.errors = errors; - this.m = m; - } +public record CheckFunctions(Set errors, Module m) { public void check(Sentence sentence) { if (sentence instanceof Rule rl) { diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckHOLE.java b/kernel/src/main/java/org/kframework/compile/checks/CheckHOLE.java index e1f55378e1c..ca443f43708 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckHOLE.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckHOLE.java @@ -20,14 +20,7 @@ import static org.kframework.kore.KORE.*; -public class CheckHOLE { - private final Set errors; - private final Module m; - - public CheckHOLE(Set errors, Module m) { - this.errors = errors; - this.m = m; - } +public record CheckHOLE(Set errors, Module m) { public void check(Sentence sentence) { if (sentence instanceof Production) { diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckK.java b/kernel/src/main/java/org/kframework/compile/checks/CheckK.java index 1de56a224ac..35d619a0bdf 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckK.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckK.java @@ -14,13 +14,7 @@ import java.util.Set; -public class CheckK { - - private final Set errors; - - public CheckK(Set errors) { - this.errors = errors; - } +public record CheckK(Set errors) { private void check(K k) { new VisitK() { diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckRewrite.java b/kernel/src/main/java/org/kframework/compile/checks/CheckRewrite.java index 56ced044fd8..a6e7536df6f 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckRewrite.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckRewrite.java @@ -18,14 +18,7 @@ /** * Created by dwightguth on 1/25/16. */ -public class CheckRewrite { - private final Set errors; - private final Module m; - - public CheckRewrite(Set errors, Module m) { - this.errors = errors; - this.m = m; - } +public record CheckRewrite(Set errors, Module m) { public void check(Sentence sentence) { if (sentence instanceof RuleOrClaim) { diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckSmtLemmas.java b/kernel/src/main/java/org/kframework/compile/checks/CheckSmtLemmas.java index a9690b86951..343a0454df8 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckSmtLemmas.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckSmtLemmas.java @@ -12,14 +12,7 @@ import java.util.Set; -public class CheckSmtLemmas { - private final Set errors; - private final Module m; - - public CheckSmtLemmas(Set errors, Module m) { - this.errors = errors; - this.m = m; - } +public record CheckSmtLemmas(Set errors, Module m) { public void check(Sentence sentence) { if ((sentence instanceof Rule) && sentence.att().contains(Att.SMT_LEMMA())) { @@ -37,7 +30,7 @@ public void apply(KApply k) { "Invalid term in smt-lemma detected. All terms in smt-lemma rules require smt-hook or smtlib labels", k)); } - k.klist().items().stream().forEach(ki -> super.apply(ki)); + k.klist().items().forEach(super::apply); } }.accept(rule.body()); } diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckSortTopUniqueness.java b/kernel/src/main/java/org/kframework/compile/checks/CheckSortTopUniqueness.java index 8a7527475dd..06f0150b345 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckSortTopUniqueness.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckSortTopUniqueness.java @@ -18,20 +18,7 @@ * syntax KList ::= A * syntax Bag ::= A */ -public class CheckSortTopUniqueness { - private final Set errors; - - private final Module module; - - /** - * Check that the given module has no sort that has multiple top sorts. - * @param errors to be updated when violations occur. Multiple violations will be accumulated in `errors`. - * @param module to be checked. - */ - public CheckSortTopUniqueness(Set errors, Module module) { - this.errors = errors; - this.module = module; - } +public record CheckSortTopUniqueness(Set errors, Module module) { public void check(Sentence s) { if (s instanceof Production) { diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckStreams.java b/kernel/src/main/java/org/kframework/compile/checks/CheckStreams.java index fd69a8973ce..239672df519 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckStreams.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckStreams.java @@ -18,15 +18,7 @@ /** * Checks that stream cells have contents of List sort. */ -public class CheckStreams { - private final Set errors; - - private final Module module; - - public CheckStreams(Set errors, Module module) { - this.errors = errors; - this.module = module; - } +public record CheckStreams(Set errors, Module module) { public void check(Sentence s) { if (s instanceof Production) { diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckSyntaxGroups.java b/kernel/src/main/java/org/kframework/compile/checks/CheckSyntaxGroups.java index 3361673327f..015cd8e03de 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckSyntaxGroups.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckSyntaxGroups.java @@ -14,22 +14,12 @@ import java.util.ArrayList; import java.util.Set; -public class CheckSyntaxGroups { - - private final Set errors; - private final KExceptionManager kem; - private final Module module; - - public CheckSyntaxGroups(Set errors, Module module, KExceptionManager kem) { - this.errors = errors; - this.kem = kem; - this.module = module; - } +public record CheckSyntaxGroups(Set errors, Module module, KExceptionManager kem) { public void check(Sentence s) { if(s instanceof SyntaxAssociativity) { Set tags = mutable(((SyntaxAssociativity) s).tags()); - List tagList = new ArrayList(tags); + List tagList = new ArrayList<>(tags); for(int i = 0; i < tagList.size(); ++i) { for(int j = i + 1; j < tagList.size(); ++j) { diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckTokens.java b/kernel/src/main/java/org/kframework/compile/checks/CheckTokens.java index 4d4fcbbe906..17d2546b5cd 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckTokens.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckTokens.java @@ -11,22 +11,14 @@ import java.util.Set; -public class CheckTokens { - private final Set errors; - private final Module m; +public record CheckTokens(Set errors, Module m) { private static final ImmutableSet ignoredSortNames = ImmutableSet.of("KBott", "KLabel"); private static final ImmutableSet allowedAtts = ImmutableSet.of(Att.FUNCTION(), Att.TOKEN(), Att.BRACKET()); - public CheckTokens(Set errors, Module m) { - this.errors = errors; - this.m = m; - } - public void check(Sentence sentence) { - if (sentence instanceof Production) { - check((Production) sentence); + if (sentence instanceof Production p) { + check(p); } - return; } // This check ensures that sorts containing token declarations only contain syntax declarations that are also tokens (or macros). diff --git a/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java b/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java index bfa4dab18b3..9134b70efe3 100644 --- a/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java +++ b/kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java @@ -347,7 +347,7 @@ private Definition resolveConfigBubbles(Definition def) { return m; Module configParserModule = gen.getConfigGrammar(m); ParseCache cache = loadCache(configParserModule); - try (ParseInModule parser = RuleGrammarGenerator.getCombinedGrammar(cache.getModule(), true, profileRules, files, options.debugTypeInference)) { + try (ParseInModule parser = RuleGrammarGenerator.getCombinedGrammar(cache.module(), true, profileRules, files, options.debugTypeInference)) { // each parser gets its own scanner because config labels can conflict with user tokens parser.getScanner(globalOptions); parser.initialize(); @@ -356,7 +356,7 @@ private Definition resolveConfigBubbles(Definition def) { .filter(s -> s instanceof Bubble && ((Bubble) s).sentenceType().equals(configuration)) .map(b -> (Bubble) b) .parallel() - .flatMap(b -> parseBubble(parser, cache.getCache(), b) + .flatMap(b -> parseBubble(parser, cache.cache(), b) .map(p -> upSentence(p, b.sentenceType()))) .collect(Collectors.toSet()); Set allSent = m.localSentences().$bar(immutable(parsedSet)).filter(s -> !(s instanceof Bubble && ((Bubble) s).sentenceType().equals(configuration))).seq(); @@ -407,7 +407,7 @@ private Definition resolveNonConfigBubbles(Definition defWithConfig, boolean ser RuleGrammarGenerator gen = new RuleGrammarGenerator(defWithCaches); Module ruleParserModule = gen.getRuleGrammar(defWithCaches.mainModule()); ParseCache cache = loadCache(ruleParserModule); - try (ParseInModule parser = RuleGrammarGenerator.getCombinedGrammar(cache.getModule(), true, profileRules, false, true, files, options.debugTypeInference, false)) { + try (ParseInModule parser = RuleGrammarGenerator.getCombinedGrammar(cache.module(), true, profileRules, false, true, files, options.debugTypeInference, false)) { Scanner scanner; if (deserializeScanner) { scanner = new Scanner(parser, globalOptions, files.resolveKompiled("scanner")); @@ -434,8 +434,8 @@ private Module resolveNonConfigBubbles(Module module, Scanner scanner, RuleGramm ParseCache cache = loadCache(ruleParserModule); try (ParseInModule parser = needNewScanner ? - RuleGrammarGenerator.getCombinedGrammar(cache.getModule(), true, profileRules, files, options.debugTypeInference) : - RuleGrammarGenerator.getCombinedGrammar(cache.getModule(), scanner, true, profileRules, false, files, options.debugTypeInference, false)) { + RuleGrammarGenerator.getCombinedGrammar(cache.module(), true, profileRules, files, options.debugTypeInference) : + RuleGrammarGenerator.getCombinedGrammar(cache.module(), scanner, true, profileRules, false, files, options.debugTypeInference, false)) { if (needNewScanner) parser.getScanner(globalOptions); parser.initialize(); @@ -444,7 +444,7 @@ private Module resolveNonConfigBubbles(Module module, Scanner scanner, RuleGramm .parallel() .filter(s -> s instanceof Bubble) .map(b -> (Bubble) b) - .flatMap(b -> parseBubble(parser, cache.getCache(), b) + .flatMap(b -> parseBubble(parser, cache.cache(), b) .map(p -> upSentence(p, b.sentenceType()))) .collect(Collections.toSet()); @@ -474,15 +474,15 @@ private Definition resolveCachedBubbles(Definition def, boolean isRule) { .filter(s -> s instanceof Bubble && (isRule || ((Bubble) s).sentenceType().equals(configuration))) .map(b -> (Bubble) b) .flatMap(b -> { - if (cache.getCache().containsKey(b.contents()) && cache.getCache().get(b.contents()).getParse() != null) { - ParsedSentence parse = updateLocation(cache.getCache().get(b.contents()), b); - Att termAtt = parse.getParse().att().remove(Source.class).remove(Location.class).remove(Production.class); + if (cache.cache().containsKey(b.contents()) && cache.cache().get(b.contents()).parse() != null) { + ParsedSentence parse = updateLocation(cache.cache().get(b.contents()), b); + Att termAtt = parse.parse().att().remove(Source.class).remove(Location.class).remove(Production.class); Att bubbleAtt = b.att().remove(Source.class).remove(Location.class).remove(Att.CONTENT_START_LINE(), Integer.class).remove(Att.CONTENT_START_COLUMN(), Integer.class); if (!termAtt.equals(bubbleAtt)) // invalidate cache if attributes changed return Stream.of(); cachedBubbles.getAndIncrement(); - registerWarnings(parse.getWarnings()); - KApply k = (KApply) new TreeNodesToKORE(Outer::parseSort, true).down(parse.getParse()); + registerWarnings(parse.warnings()); + KApply k = (KApply) new TreeNodesToKORE(Outer::parseSort, true).down(parse.parse()); return Stream.of(Pair.of(b, upSentence(k, b.sentenceType()))); } return Stream.of(); @@ -501,24 +501,24 @@ private Definition resolveCachedBubbles(Definition def, boolean isRule) { public static ParsedSentence updateLocation(ParsedSentence parse, Bubble b) { int newStartLine = b.att().get(Att.CONTENT_START_LINE(), Integer.class); int newStartColumn = b.att().get(Att.CONTENT_START_COLUMN(), Integer.class); - int oldStartLine = parse.getStartLine(); - int oldStartColumn = parse.getStartColumn(); - if (oldStartLine != newStartLine || oldStartColumn != newStartColumn || !parse.getSource().equals(b.source().get())) { + int oldStartLine = parse.startLine(); + int oldStartColumn = parse.startColumn(); + if (oldStartLine != newStartLine || oldStartColumn != newStartColumn || !parse.source().equals(b.source().get())) { int lineOffset = newStartLine - oldStartLine; int columnOffset = newStartColumn - oldStartColumn; - K k = parse.getParse() != null ? new AddAttRec(a -> { + K k = parse.parse() != null ? new AddAttRec(a -> { Location loc = a.get(Location.class); Location newLoc = updateLocation(oldStartLine, lineOffset, columnOffset, loc); return a.remove(Source.class).remove(Location.class).add(Location.class, newLoc) .add(Source.class, b.source().orElseThrow(() -> new AssertionError("Expecting bubble to have source location!"))); - }).apply(parse.getParse()) : null; - java.util.Set warnings = parse.getWarnings().stream().map(ex -> ex.withLocation(updateLocation(oldStartLine, lineOffset, columnOffset, ex.exception.getLocation()), + }).apply(parse.parse()) : null; + java.util.Set warnings = parse.warnings().stream().map(ex -> ex.withLocation(updateLocation(oldStartLine, lineOffset, columnOffset, ex.exception.getLocation()), b.source().orElseThrow(() -> new AssertionError("Expecting bubble to have source location!")))) .collect(Collectors.toSet()); - java.util.Set errors = parse.getErrors().stream().map(ex -> ex.withLocation(updateLocation(oldStartLine, lineOffset, columnOffset, ex.exception.getLocation()), + java.util.Set errors = parse.errors().stream().map(ex -> ex.withLocation(updateLocation(oldStartLine, lineOffset, columnOffset, ex.exception.getLocation()), b.source().orElseThrow(() -> new AssertionError("Expecting bubble to have source location!")))) .collect(Collectors.toSet()); - return new ParsedSentence(k, warnings, errors, newStartLine, newStartColumn, parse.getSource()); + return new ParsedSentence(k, warnings, errors, newStartLine, newStartColumn, parse.source()); } return parse; } @@ -629,7 +629,7 @@ private Configuration upConfiguration(K contents) { private ParseCache loadCache(Module parser) { ParseCache cachedParser = caches.get(parser.name()); - if (cachedParser == null || !equalsSyntax(cachedParser.getModule().signature(), parser.signature())) { + if (cachedParser == null || !equalsSyntax(cachedParser.module().signature(), parser.signature())) { cachedParser = new ParseCache(parser, true, java.util.Collections.synchronizedMap(new HashMap<>())); caches.put(parser.name(), cachedParser); } diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java index 8c279314223..f54868b20c6 100644 --- a/kernel/src/main/java/org/kframework/kompile/Kompile.java +++ b/kernel/src/main/java/org/kframework/kompile/Kompile.java @@ -263,11 +263,11 @@ private Definition postProcessJSON(Definition defn, String postProcess) { command.add(compiledJson.getAbsolutePath()); RunProcess.ProcessOutput output = RunProcess.execute(environment, files.getProcessBuilder(), command.toArray(new String[command.size()])); sw.printIntermediate("Post process JSON: " + String.join(" ", command)); - if (output.exitCode != 0) { + if (output.exitCode() != 0) { throw KEMException.criticalError("Post-processing returned a non-zero exit code: " - + output.exitCode + "\nStdout:\n" + new String(output.stdout) + "\nStderr:\n" + new String(output.stderr)); + + output.exitCode() + "\nStdout:\n" + new String(output.stdout()) + "\nStderr:\n" + new String(output.stderr())); } - return JsonParser.parseDefinition(new String(output.stdout)); + return JsonParser.parseDefinition(new String(output.stdout())); } private static String ruleSourceMap(Definition def) { diff --git a/kernel/src/main/java/org/kframework/kprove/KProve.java b/kernel/src/main/java/org/kframework/kprove/KProve.java index 07a471a6cfb..528b4ef23cb 100644 --- a/kernel/src/main/java/org/kframework/kprove/KProve.java +++ b/kernel/src/main/java/org/kframework/kprove/KProve.java @@ -18,43 +18,28 @@ import scala.Tuple2; import java.io.UnsupportedEncodingException; +import java.nio.charset.StandardCharsets; import java.util.Set; import java.util.function.Function; import java.util.stream.Collectors; import static org.kframework.Collections.*; -public class KProve { - - public static final String BOUNDARY_CELL_PREFIX = "BOUND_"; - +public record KProve( + KExceptionManager kem, + FileUtil files, + KPrint kprint, + KProveOptions kproveOptions, + CompiledDefinition compiledDefinition, + ProofDefinitionBuilder proofDefinitionBuilder, + Function rewriterGenerator, + Stopwatch sw +) { private static final int KPROVE_SUCCESS_EXIT_CODE = 0; private static final int KPROVE_MISMATCH_CONFIG_CODE = 1; - private final KExceptionManager kem; - private final FileUtil files; - private final KPrint kprint; - private final KProveOptions kproveOptions; - private final CompiledDefinition compiledDefinition; - private final BinaryLoader loader; - private final ProofDefinitionBuilder proofDefinitionBuilder; - private final Function rewriterGenerator; - private final Stopwatch sw; - @Inject - public KProve(KExceptionManager kem, FileUtil files, KPrint kprint, KProveOptions kproveOptions, - CompiledDefinition compiledDefinition, BinaryLoader loader, - ProofDefinitionBuilder proofDefinitionBuilder, Function rewriterGenerator, Stopwatch sw) { - this.kem = kem; - this.files = files; - this.kprint = kprint; - this.kproveOptions = kproveOptions; - this.compiledDefinition = compiledDefinition; - this.loader = loader; - this.proofDefinitionBuilder = proofDefinitionBuilder; - this.rewriterGenerator = rewriterGenerator; - this.sw = sw; - } + public KProve {} public int run() { if (!kproveOptions.specFile(files).exists()) { @@ -69,11 +54,7 @@ public int run() { Module specModule = compiled._2(); if (kproveOptions.emitJson) { - try { - files.saveToKompiled("prove-definition.json", new String(ToJson.apply(compiled._1()), "UTF-8")); - } catch (UnsupportedEncodingException e) { - throw KEMException.criticalError("Unsupported encoding `UTF-8` when saving JSON definition."); - } + files.saveToKompiled("prove-definition.json", new String(ToJson.apply(compiled._1()), StandardCharsets.UTF_8)); } if (kproveOptions.emitJsonSpec != null) { @@ -91,16 +72,15 @@ public int run() { int errCode = results.exitCode().orElse(0); switch (errCode) { - case KPROVE_SUCCESS_EXIT_CODE: - break; - case KPROVE_MISMATCH_CONFIG_CODE: - kem.addKException( new KException(KException.ExceptionType.ERROR, KException.KExceptionGroup.PROVER, - "backend terminated because the configuration cannot be rewritten further. See output for more details.")); - break; - default: - kem.addKException( new KException(KException.ExceptionType.ERROR, KException.KExceptionGroup.PROVER, - "backend crashed with exit code " + String.valueOf(errCode))); - break; + case KPROVE_SUCCESS_EXIT_CODE -> {} + case KPROVE_MISMATCH_CONFIG_CODE -> { + kem.addKException(new KException(KException.ExceptionType.ERROR, KException.KExceptionGroup.PROVER, + "backend terminated because the configuration cannot be rewritten further. See output for more details.")); + } + default -> { + kem.addKException(new KException(KException.ExceptionType.ERROR, KException.KExceptionGroup.PROVER, + "backend crashed with exit code " + errCode)); + } } return results.exitCode().orElse(KEMException.TERMINATED_WITH_ERRORS_EXIT_CODE); diff --git a/kernel/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java b/kernel/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java index 971f9415d81..2ff777a4a25 100644 --- a/kernel/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java +++ b/kernel/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java @@ -6,8 +6,8 @@ import org.apache.commons.io.FilenameUtils; import org.kframework.attributes.Att; import org.kframework.compile.Backend; -import org.kframework.definition.Module; import org.kframework.definition.*; +import org.kframework.definition.Module; import org.kframework.kompile.CompiledDefinition; import org.kframework.kompile.Kompile; import org.kframework.utils.Stopwatch; @@ -25,24 +25,13 @@ import static org.kframework.Collections.*; -public class ProofDefinitionBuilder { - - private final CompiledDefinition compiledDefinition; - private final Backend backend; - private final Kompile kompile; - private final KProveOptions proveOptions; - private final FileUtil files; - private final Stopwatch sw; +public record ProofDefinitionBuilder(CompiledDefinition compiledDefinition, + Backend backend, Kompile kompile, + KProveOptions proveOptions, + FileUtil files, Stopwatch sw) { @Inject - public ProofDefinitionBuilder(CompiledDefinition compiledDefinition, Backend backend, Kompile kompile, - KProveOptions proveOptions, FileUtil files, Stopwatch sw) { - this.compiledDefinition = compiledDefinition; - this.backend = backend; - this.kompile = kompile; - this.proveOptions = proveOptions; - this.files = files; - this.sw = sw; + public ProofDefinitionBuilder { } /** diff --git a/kernel/src/main/java/org/kframework/kserver/KServerFrontEnd.java b/kernel/src/main/java/org/kframework/kserver/KServerFrontEnd.java index 3b3017d8b5f..b1ea8a48939 100644 --- a/kernel/src/main/java/org/kframework/kserver/KServerFrontEnd.java +++ b/kernel/src/main/java/org/kframework/kserver/KServerFrontEnd.java @@ -147,10 +147,10 @@ public int run(String tool, String[] args, File workingDir, Map requestScope.enter(); Main.seedInjector(requestScope, tool, args, workingDir, env, startTime); TTYInfo tty = injector.getInstance(TTYInfo.class); - if (!tty.stdout) { + if (!tty.stdout()) { system_out.init(new PrintStream(system_out.getPrintStream())); } - if (!tty.stderr) { + if (!tty.stderr()) { system_err.init(new PrintStream(system_err.getPrintStream())); } diff --git a/kernel/src/main/java/org/kframework/lsp/TextDocumentSyncHandler.java b/kernel/src/main/java/org/kframework/lsp/TextDocumentSyncHandler.java index 07611f3c308..d204107e46a 100644 --- a/kernel/src/main/java/org/kframework/lsp/TextDocumentSyncHandler.java +++ b/kernel/src/main/java/org/kframework/lsp/TextDocumentSyncHandler.java @@ -75,7 +75,7 @@ public void loadCaches() { if (caches == null) caches = new HashMap<>(); caches.forEach((key, val) -> { - String uri = Path.of(val.getModule().att().get(org.kframework.attributes.Source.class).source()).toUri().toString(); + String uri = Path.of(val.module().att().get(org.kframework.attributes.Source.class).source()).toUri().toString(); // load into LSP all the files found in the caches, even if they are not open in the IDE. // this way we can find all the updated locations when finding references if (!files.containsKey(uri)) @@ -245,7 +245,7 @@ public CompletableFuture, List String suffix = ss.getType().equals(DefinitionParsing.configuration) ? "-" + RuleGrammarGenerator.CONFIG_CELLS : "-" + RuleGrammarGenerator.RULE_CELLS; Optional> ch = caches.entrySet().stream().filter(elm -> elm.getKey().startsWith(m.getName() + suffix)).findFirst(); if (ch.isPresent()) { - Map parsedSent = ch.get().getValue().getCache(); + Map parsedSent = ch.get().getValue().cache(); if (parsedSent.containsKey(ss.getContent())) { Bubble b = new Bubble(ss.getType(), ss.getContent(), ss.getAttributes() .add(org.kframework.attributes.Location.class, ss.getLocation()).add(Source.class, ss.getSource()) @@ -256,7 +256,7 @@ public CompletableFuture, List if (isPositionOverLocation(pos, t.location().get())) x.set(t); // find the deepest term that contains this position return t; - }, "Find def in rule").apply(parse.getParse()); + }, "Find def in rule").apply(parse.parse()); if (x.get() != null && x.get().att().get(org.kframework.definition.Production.class).source().isPresent()) { org.kframework.definition.Production prd = x.get().att().get(org.kframework.definition.Production.class); if (prd.source().isPresent()) // exclude generated productions like casts @@ -324,17 +324,17 @@ public CompletableFuture diagnostic(DocumentDiagnostic Optional> ch = caches.entrySet().stream().filter(elm -> elm.getKey().startsWith(m.getName() + suffix)).findFirst(); if (ch.isPresent()) { ParseCache parseCache = ch.get().getValue(); - Map parsedSent = parseCache.getCache(); + Map parsedSent = parseCache.cache(); if (parsedSent.containsKey(ss.getContent())) { Bubble b = new Bubble(ss.getType(), ss.getContent(), ss.getAttributes() .add(org.kframework.attributes.Location.class, ss.getLocation()).add(Source.class, ss.getSource()) .add(Att.CONTENT_START_LINE(), ss.getContentStartLine()).add(Att.CONTENT_START_COLUMN(), ss.getContentStartColumn())); ParseCache.ParsedSentence parse = DefinitionParsing.updateLocation(parsedSent.get(b.contents()), b); - parse.getErrors().forEach(err -> { + parse.errors().forEach(err -> { Diagnostic d = new Diagnostic(loc2range(err.exception.getLocation()), err.exception.getMessage(), DiagnosticSeverity.Error, "Inner Parser"); problems.add(d); }); - parse.getWarnings().forEach(err -> { + parse.warnings().forEach(err -> { Diagnostic d = new Diagnostic(loc2range(err.exception.getLocation()), err.exception.getMessage(), DiagnosticSeverity.Warning, "Inner Parser"); problems.add(d); }); @@ -399,16 +399,16 @@ public CompletableFuture> references(ReferenceParams pa // 1. for each cached sentence // 2. find if it still exists in the source file and get its updated location caches.forEach((mname, parseCache) -> { - String uri = Path.of(parseCache.getModule().att().get(org.kframework.attributes.Source.class).source()).toUri().toString(); + String uri = Path.of(parseCache.module().att().get(org.kframework.attributes.Source.class).source()).toUri().toString(); files.get(uri).dis.stream().filter(di2 -> di2 instanceof Module) .map(di2 -> (Module) di2) .filter(mm -> mname.startsWith((mm.getName()))) .forEach(mm -> mm.getItems().stream().filter(mi -> mi instanceof StringSentence) .map(mi -> (StringSentence) mi) .forEach(ss -> { - if (parseCache.getCache().containsKey(ss.getContent())) { - ParseCache.ParsedSentence ps = parseCache.getCache().get(ss.getContent()); - if (ps.getParse() != null) { + if (parseCache.cache().containsKey(ss.getContent())) { + ParseCache.ParsedSentence ps = parseCache.cache().get(ss.getContent()); + if (ps.parse() != null) { Bubble b = new Bubble(ss.getType(), ss.getContent(), ss.getAttributes() .add(org.kframework.attributes.Location.class, ss.getLocation()).add(Source.class, ss.getSource()) .add(Att.CONTENT_START_LINE(), ss.getContentStartLine()).add(Att.CONTENT_START_COLUMN(), ss.getContentStartColumn())); @@ -423,7 +423,7 @@ public CompletableFuture> references(ReferenceParams pa loc2range(t.location().get()))); } return t; - }, "Find ref in rule").apply(ps.getParse()); + }, "Find ref in rule").apply(ps.parse()); } } }) @@ -475,7 +475,7 @@ public CompletableFuture> selectionRange(SelectionRangePara Optional> ch = caches.entrySet().stream().filter(elm -> elm.getKey().startsWith(m.getName() + suffix)).findFirst(); AtomicReference x = new AtomicReference<>(sentsr); if (ch.isPresent()) { - Map parsedSent = ch.get().getValue().getCache(); + Map parsedSent = ch.get().getValue().cache(); if (parsedSent.containsKey(ss.getContent())) { Bubble b = new Bubble(ss.getType(), ss.getContent(), ss.getAttributes() .add(org.kframework.attributes.Location.class, ss.getLocation()).add(Source.class, ss.getSource()) @@ -487,7 +487,7 @@ public CompletableFuture> selectionRange(SelectionRangePara x.set(tsr); // find the deepest term that contains this position } return t; - }, "Find selectionRange in rule").apply(parse.getParse()); + }, "Find selectionRange in rule").apply(parse.parse()); } } lloc.add(x.get()); diff --git a/kernel/src/main/java/org/kframework/main/Main.java b/kernel/src/main/java/org/kframework/main/Main.java index 8f72f092a92..adbdb5b2f3a 100644 --- a/kernel/src/main/java/org/kframework/main/Main.java +++ b/kernel/src/main/java/org/kframework/main/Main.java @@ -35,7 +35,11 @@ import java.util.ServiceLoader; import java.util.concurrent.ExecutionException; -public class Main { +public record Main( + Provider kem, + Provider frontEnd, + @Named("requestScope") SimpleScope requestScope +) { /** * @param args @@ -91,19 +95,8 @@ public static void nailMain(NGContext context) { invalidJarArguments(); } - private final Provider kem; - private final Provider frontEnd; - private final SimpleScope requestScope; - @Inject - public Main( - Provider kem, - Provider frontEnd, - @Named("requestScope") SimpleScope requestScope) { - this.kem = kem; - this.frontEnd = frontEnd; - this.requestScope = requestScope; - } + public Main {} public SimpleScope getRequestScope() { return requestScope; @@ -123,8 +116,7 @@ public int runApplication() { KExceptionManager kem = this.kem.get(); kem.installForUncaughtExceptions(); try { - int retval = frontEnd.get().main(); - return retval; + return frontEnd.get().main(); } catch (ProvisionException e) { for (Message m : e.getErrorMessages()) { if (!(m.getCause() instanceof KEMException ex)) { @@ -207,8 +199,7 @@ public static Injector getInjector(String tool) { //boot error, we should have printed it already Main.exit(1); } - Injector injector = Guice.createInjector(modules); - return injector; + return Guice.createInjector(modules); } private static void invalidJarArguments() { diff --git a/kernel/src/main/java/org/kframework/parser/KRead.java b/kernel/src/main/java/org/kframework/parser/KRead.java index 58642dd00fb..63dbcab708e 100644 --- a/kernel/src/main/java/org/kframework/parser/KRead.java +++ b/kernel/src/main/java/org/kframework/parser/KRead.java @@ -32,24 +32,12 @@ import javax.json.JsonObject; import javax.json.JsonReader; -public class KRead { - - private final KExceptionManager kem; - private final FileUtil files; - private final InputModes input; - private final GlobalOptions globalOptions; - - public KRead( - KExceptionManager kem, - FileUtil files, - InputModes input, - GlobalOptions globalOptions - ) { - this.kem = kem; - this.files = files; - this.input = input; - this.globalOptions = globalOptions; - } +public record KRead( + KExceptionManager kem, + FileUtil files, + InputModes input, + GlobalOptions globalOptions +) { public String showTokens(Module mod, CompiledDefinition def, String stringToParse, Source source) { return def.showTokens(mod, files, stringToParse, source); @@ -96,16 +84,15 @@ public void createBisonParser(Module mod, Sort sort, File outputFile, boolean gl if (exit != 0) { throw KEMException.internalError("bison returned nonzero exit code: " + exit + "\n"); } - List command = new ArrayList<>(); - command.addAll(Arrays.asList( - Scanner.COMPILER, - "-DK_BISON_PARSER_SORT=" + sort.name(), - files.resolveKInclude("cparser/main.c").getAbsolutePath(), - files.resolveTemp("lex.yy.c").getAbsolutePath(), - files.resolveTemp("parser.tab.c").getAbsolutePath(), - "-iquote", files.resolveTemp(".").getAbsolutePath(), - "-iquote", files.resolveKInclude("cparser").getAbsolutePath(), - "-o", outputFile.getAbsolutePath())); + List command = new ArrayList<>(Arrays.asList( + Scanner.COMPILER, + "-DK_BISON_PARSER_SORT=" + sort.name(), + files.resolveKInclude("cparser/main.c").getAbsolutePath(), + files.resolveTemp("lex.yy.c").getAbsolutePath(), + files.resolveTemp("parser.tab.c").getAbsolutePath(), + "-iquote", files.resolveTemp(".").getAbsolutePath(), + "-iquote", files.resolveKInclude("cparser").getAbsolutePath(), + "-o", outputFile.getAbsolutePath())); if (library) { command.addAll(OS.current().getSharedLibraryCompilerFlags()); diff --git a/kernel/src/main/java/org/kframework/parser/inner/ParseCache.java b/kernel/src/main/java/org/kframework/parser/inner/ParseCache.java index f35340e028e..0c4fee0651f 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/ParseCache.java +++ b/kernel/src/main/java/org/kframework/parser/inner/ParseCache.java @@ -13,71 +13,11 @@ /** * Created by dwightguth on 4/20/15. */ -public class ParseCache implements Serializable { - private final Module module; - private final boolean strict; - private final Map cache; - - public ParseCache(Module module, boolean strict, Map cache) { - this.module = module; - this.strict = strict; - this.cache = cache; - } - - public Map getCache() { - return cache; - } - - public Module getModule() { - return module; - } - - public boolean isStrict() { - return strict; - } - - public static class ParsedSentence implements Serializable { - private K parse; - private final Set warnings; - - private final Set errors; - - private final int startLine; - private final int startColumn; - - private final Source source; - - public ParsedSentence(K parse, Set warnings, Set errors, int startLine, int startColumn, Source source) { - this.parse = parse; - this.warnings = warnings; - this.errors = errors; - this.startLine = startLine; - this.startColumn = startColumn; - this.source = source; - } - - public K getParse() { - return parse; - } - - public Set getWarnings() { - return warnings; - } - - public Set getErrors() { - return errors; - } - - public int getStartLine() { - return startLine; - } - - public int getStartColumn() { - return startColumn; - } - - public Source getSource() { - return source; - } +public record ParseCache(Module module, boolean strict, + Map cache) implements Serializable { + public record ParsedSentence(K parse, + Set warnings, + Set errors, int startLine, + int startColumn, Source source) implements Serializable { } } diff --git a/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java b/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java index e5704ef566e..b99c38a3be5 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java +++ b/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java @@ -52,9 +52,8 @@ * The instances of the non-terminal KItem is renamed in KItem#Top if found in the right * hand side of a production, and into KItem#Bottom if found in the left hand side. */ -public class RuleGrammarGenerator { +public record RuleGrammarGenerator(Definition baseK) { - private final Definition baseK; private static final Set kSorts = new HashSet<>(); static { @@ -70,6 +69,7 @@ public class RuleGrammarGenerator { private static Set kSorts() { return java.util.Collections.unmodifiableSet(kSorts); } + /// modules that have a meaning: public static final String DEFAULT_LAYOUT = "DEFAULT-LAYOUT"; public static final String RULE_CELLS = "RULE-CELLS"; @@ -94,11 +94,11 @@ private static Set kSorts() { /** * Initialize a grammar generator. + * * @param baseK A Definition containing a K module giving the syntax of K itself. * The default K syntax is defined in include/kast.k. */ - public RuleGrammarGenerator(Definition baseK) { - this.baseK = baseK; + public RuleGrammarGenerator { } private Set renameKItem2Bottom(Set def) { @@ -109,6 +109,7 @@ private Set renameKItem2Bottom(Set def) { /** * Creates the seed module that can be used to parse rules. * Imports module markers RULE-CELLS and K found in /include/kast.k. + * * @param mod The user defined module from which to start. * @return a new module which imports the original user module and a set of marker modules. */ @@ -118,17 +119,18 @@ public Module getRuleGrammar(Module mod) { private Module getGrammar(Module mod, String name) { // import RULE-CELLS in order to parse cells specific to rules - Module newM = new Module( mod.name() + "-" + name - , (scala.collection.Set) mod.imports().$bar(Set(Import(baseK.getModule(K).get(), true), Import(baseK.getModule(name).get(), true), Import(baseK.getModule(DEFAULT_LAYOUT).get(), true))) - , mod.localSentences() - , mod.att() - ); + Module newM = new Module(mod.name() + "-" + name + , (scala.collection.Set) mod.imports().$bar(Set(Import(baseK.getModule(K).get(), true), Import(baseK.getModule(name).get(), true), Import(baseK.getModule(DEFAULT_LAYOUT).get(), true))) + , mod.localSentences() + , mod.att() + ); return newM; } /** * Creates the seed module that can be used to parse configurations. * Imports module markers CONFIG-CELLS and K found in /include/kast.k. + * * @param mod The user defined module from which to start. * @return a new module which imports the original user module and a set of marker modules. */ @@ -139,12 +141,13 @@ public Module getConfigGrammar(Module mod) { /** * Creates the seed module that can be used to parse programs. * Imports module markers PROGRAM-LISTS found in /include/kast.k. + * * @param mod The user defined module from which to start. * @return a new module which imports the original user module and a set of marker modules. */ public Module getProgramsGrammar(Module mod) { - if(mod.name().endsWith(POSTFIX)) { + if (mod.name().endsWith(POSTFIX)) { return mod; } else { Module newMod = ModuleTransformer.from(oldMod -> { @@ -161,14 +164,14 @@ public Module getProgramsGrammar(Module mod) { Set modules = new HashSet(); for (Import m : iterable(newMod.imports())) { - modules.add(m); + modules.add(m); } // import PROGRAM-LISTS so user lists are modified to parse programs modules.add(Import(baseK.getModule(PROGRAM_LISTS).get(), true)); // check if `#Layout` has been declared, import `DEFAULT-LAYOUT` if not - if (! mod.allSorts().contains(Sorts.Layout())) { + if (!mod.allSorts().contains(Sorts.Layout())) { modules.add(Import(baseK.getModule(DEFAULT_LAYOUT).get(), true)); } @@ -182,7 +185,7 @@ public static boolean isParserSort(Sort s) { /* use this overload if you don't need to profile rule parse times. */ public static ParseInModule getCombinedGrammar(Module mod, boolean strict, FileUtil files) { - return getCombinedGrammar(mod, strict, false, false, false, files, null, false); + return getCombinedGrammar(mod, strict, false, false, false, files, null, false); } public static ParseInModule getCombinedGrammar(Module mod, boolean strict, FileUtil files, boolean partialParseDebug) { @@ -190,23 +193,23 @@ public static ParseInModule getCombinedGrammar(Module mod, boolean strict, FileU } public static ParseInModule getCombinedGrammar(Module mod, boolean strict, boolean timing, FileUtil files) { - return getCombinedGrammar(mod, strict, timing, false, false, files, null, false); + return getCombinedGrammar(mod, strict, timing, false, false, files, null, false); } public static ParseInModule getCombinedGrammar(Module mod, boolean strict, boolean timing, FileUtil files, String debugTypeInference) { - return getCombinedGrammar(mod, strict, timing, false, false, files, debugTypeInference, false); + return getCombinedGrammar(mod, strict, timing, false, false, files, debugTypeInference, false); } public static ParseInModule getCombinedGrammar(Module mod, boolean strict, boolean timing, boolean isBison, FileUtil files) { - return getCombinedGrammar(mod, strict, timing, isBison, false, files, null, false); + return getCombinedGrammar(mod, strict, timing, isBison, false, files, null, false); } public static ParseInModule getCombinedGrammar(Module mod, boolean strict, boolean timing, boolean isBison, boolean forGlobalScanner, FileUtil files) { - return getCombinedGrammar(mod, strict, timing, isBison, forGlobalScanner, files, null, false); + return getCombinedGrammar(mod, strict, timing, isBison, forGlobalScanner, files, null, false); } public static ParseInModule getCombinedGrammar(Module mod, Scanner scanner, boolean strict, boolean timing, boolean isBison, FileUtil files) { - return getCombinedGrammar(mod, scanner, strict, timing, isBison, files, null, false); + return getCombinedGrammar(mod, scanner, strict, timing, isBison, files, null, false); } // the forGlobalScanner flag tells the ParseInModule class not to exclude @@ -224,7 +227,7 @@ public static ParseInModule getCombinedGrammar(Module mod, Scanner scanner, bool * constructor. The new module contains syntax declaration for Casts and the diamond * which connects the user concrete syntax with K syntax. * - * @param mod module for which to create the parser. + * @param mod module for which to create the parser. * @param partialParseDebug * @return parser which applies disambiguation filters by default. */ @@ -244,16 +247,16 @@ public static Tuple3 getCombinedGrammarImpl(Module mod, Module origMod = mod; if (!forGlobalScanner) { - mod = mod.signature(); + mod = mod.signature(); } if (isBison) { - mod = ModuleTransformer.from(m -> { - if (m.att().contains(Att.NOT_LR1())) { - return Module(m.name(), m.imports(), Set(), m.att()); - } - return m; - }, "strip not-lr1 modules from bison grammar").apply(mod); + mod = ModuleTransformer.from(m -> { + if (m.att().contains(Att.NOT_LR1())) { + return Module(m.name(), m.imports(), Set(), m.att()); + } + return m; + }, "strip not-lr1 modules from bison grammar").apply(mod); } if (mod.importedModuleNames().contains(AUTO_CASTS)) { // create the diamond @@ -468,44 +471,44 @@ public static Tuple3 getCombinedGrammarImpl(Module mod, } // for each triple, generate a new pattern which works better for parsing lists in programs. prods3.addAll(parseProds.stream().collect(Collectors.toSet())); - java.util.Set res = new HashSet<>(); + Set res = new HashSet<>(); for (UserList ul : UserList.getLists(prods3)) { - org.kframework.definition.Production prod1, prod2, prod3 = null, prod4 = null, prod5 = null; + Production prod1, prod2, prod3 = null, prod4 = null, prod5 = null; Att newAtts = ul.attrs.remove(Att.USER_LIST()); if (ul.leftAssoc && ul.nonEmpty) { - prod1 = Production(ul.klabel, ul.sort, - Seq(NonTerminal(ul.sort), Terminal(ul.separator), NonTerminal(ul.childSort)), - newAtts.add(Att.ORIGINAL_PRD(), Production.class, ul.pList)); - prod2 = Production(Seq(), ul.sort, - Seq(NonTerminal(ul.childSort)), - newAtts.add(Att.ORIGINAL_PRD(), Production.class, ul.pList).add(Att.USER_LIST(), ul.klabel.name()).add(Att.USER_LIST_TERMINATOR(), ul.terminatorKLabel.name())); - prod3 = Production(ul.terminatorKLabel, Sort(ul.sort.name() + "#Terminator", ul.sort.params()), Seq(Terminal("")), - newAtts.remove(Att.FORMAT()).add(Att.ORIGINAL_PRD(), Production.class, ul.pTerminator)); + prod1 = Production(ul.klabel, ul.sort, + Seq(NonTerminal(ul.sort), Terminal(ul.separator), NonTerminal(ul.childSort)), + newAtts.add(Att.ORIGINAL_PRD(), Production.class, ul.pList)); + prod2 = Production(Seq(), ul.sort, + Seq(NonTerminal(ul.childSort)), + newAtts.add(Att.ORIGINAL_PRD(), Production.class, ul.pList).add(Att.USER_LIST(), ul.klabel.name()).add(Att.USER_LIST_TERMINATOR(), ul.terminatorKLabel.name())); + prod3 = Production(ul.terminatorKLabel, Sort(ul.sort.name() + "#Terminator", ul.sort.params()), Seq(Terminal("")), + newAtts.remove(Att.FORMAT()).add(Att.ORIGINAL_PRD(), Production.class, ul.pTerminator)); } else if (ul.leftAssoc) { - throw KEMException.compilerError("Cannot use List with --bison-lists", ul.pList); + throw KEMException.compilerError("Cannot use List with --bison-lists", ul.pList); } else { - // Es#Terminator ::= "" [klabel('.Es)] - prod1 = Production(ul.terminatorKLabel, Sort(ul.sort.name() + "#Terminator", ul.sort.params()), Seq(Terminal("")), - newAtts.remove(Att.FORMAT()).add(Att.ORIGINAL_PRD(), Production.class, ul.pTerminator)); - // Ne#Es ::= E "," Ne#Es [klabel('_,_)] - prod2 = Production(ul.klabel, Sort("Ne#" + ul.sort.name(), ul.sort.params()), - Seq(NonTerminal(ul.childSort), Terminal(ul.separator), NonTerminal(Sort("Ne#" + ul.sort.name(), ul.sort.params()))), - newAtts.add(Att.ORIGINAL_PRD(), Production.class, ul.pList)); - // Ne#Es ::= E "" Es#Terminator [klabel('_,_)] - prod3 = Production(ul.klabel, Sort("Ne#" + ul.sort.name(), ul.sort.params()), - Seq(NonTerminal(ul.childSort), Terminal(""), NonTerminal(Sort(ul.sort.name() + "#Terminator", ul.sort.params()))), - newAtts.add(Att.ORIGINAL_PRD(), Production.class, ul.pList)); - // Es ::= Ne#Es - prod4 = Production(Seq(), ul.sort, Seq(NonTerminal(Sort("Ne#" + ul.sort.name(), ul.sort.params()))), Att().add(Att.NOT_INJECTION())); - // Es ::= Es#Terminator // if the list is * - prod5 = Production(Seq(), ul.sort, Seq(NonTerminal(Sort(ul.sort.name() + "#Terminator", ul.sort.params()))), Att().add(Att.NOT_INJECTION())); + // Es#Terminator ::= "" [klabel('.Es)] + prod1 = Production(ul.terminatorKLabel, Sort(ul.sort.name() + "#Terminator", ul.sort.params()), Seq(Terminal("")), + newAtts.remove(Att.FORMAT()).add(Att.ORIGINAL_PRD(), Production.class, ul.pTerminator)); + // Ne#Es ::= E "," Ne#Es [klabel('_,_)] + prod2 = Production(ul.klabel, Sort("Ne#" + ul.sort.name(), ul.sort.params()), + Seq(NonTerminal(ul.childSort), Terminal(ul.separator), NonTerminal(Sort("Ne#" + ul.sort.name(), ul.sort.params()))), + newAtts.add(Att.ORIGINAL_PRD(), Production.class, ul.pList)); + // Ne#Es ::= E "" Es#Terminator [klabel('_,_)] + prod3 = Production(ul.klabel, Sort("Ne#" + ul.sort.name(), ul.sort.params()), + Seq(NonTerminal(ul.childSort), Terminal(""), NonTerminal(Sort(ul.sort.name() + "#Terminator", ul.sort.params()))), + newAtts.add(Att.ORIGINAL_PRD(), Production.class, ul.pList)); + // Es ::= Ne#Es + prod4 = Production(Seq(), ul.sort, Seq(NonTerminal(Sort("Ne#" + ul.sort.name(), ul.sort.params()))), Att().add(Att.NOT_INJECTION())); + // Es ::= Es#Terminator // if the list is * + prod5 = Production(Seq(), ul.sort, Seq(NonTerminal(Sort(ul.sort.name() + "#Terminator", ul.sort.params()))), Att().add(Att.NOT_INJECTION())); } res.add(prod1); res.add(prod2); res.add(prod3); - if(!ul.leftAssoc) { + if (!ul.leftAssoc) { res.add(prod4); res.add(SyntaxSort(Seq(), Sort(ul.sort.name() + "#Terminator", ul.sort.params()))); res.add(SyntaxSort(Seq(), Sort("Ne#" + ul.sort.name(), ul.sort.params()))); @@ -519,9 +522,9 @@ public static Tuple3 getCombinedGrammarImpl(Module mod, } if (mod.importedModuleNames().contains(RULE_LISTS)) { - java.util.Set res = new HashSet<>(); + Set res = new HashSet<>(); for (UserList ul : UserList.getLists(parseProds)) { - org.kframework.definition.Production prod1; + Production prod1; // Es ::= E prod1 = Production(Seq(), ul.sort, Seq(NonTerminal(ul.childSort))); res.add(prod1); @@ -535,7 +538,7 @@ public static Tuple3 getCombinedGrammarImpl(Module mod, Att att = mod.att(); List notLrModules = stream(mod.importedModules()).filter(m -> m.att().contains(Att.NOT_LR1())).map(Module::name).collect(Collectors.toList()); if (!notLrModules.isEmpty()) { - att = att.add(Att.NOT_LR1_MODULES(), notLrModules.toString()); + att = att.add(Att.NOT_LR1_MODULES(), notLrModules.toString()); } Module extensionM = new Module(mod.name() + "-EXTENSION", Set(Import(origMod, true)), immutable(extensionProds), att); Module disambM = new Module(mod.name() + "-DISAMB", Set(), immutable(disambProds), att); @@ -545,15 +548,16 @@ public static Tuple3 getCombinedGrammarImpl(Module mod, } private static final Pattern alphaNum = Pattern.compile("[A-Za-z][A-Za-z0-9\\-]*"); + private static void addCellNameProd(Set prods, Sentence prod) { if (prod instanceof Production) { - for (ProductionItem pi : iterable(((Production)prod).items())) { - if (pi instanceof Terminal t) { - if (alphaNum.matcher(t.value()).matches()) { - prods.add(Production(Seq(), Sorts.CellName(), Seq(t), Att().add(Att.TOKEN()))); - } + for (ProductionItem pi : iterable(((Production) prod).items())) { + if (pi instanceof Terminal t) { + if (alphaNum.matcher(t.value()).matches()) { + prods.add(Production(Seq(), Sorts.CellName(), Seq(t), Att().add(Att.TOKEN()))); + } + } } - } } } @@ -561,7 +565,7 @@ private static Set makeCasts(Sort outerSort, Sort innerSort, Sort cast Set prods = new HashSet<>(); Att attrs1 = Att().add(Sort.class, castSort); prods.add(Production(KLabel("#SyntacticCast"), castSort, Seq(NonTerminal(labelSort), Terminal("::" + castSort.toString())), attrs1.add(Att.FORMAT(), "%1%2"))); - prods.add(Production(KLabel("#SemanticCastTo" + labelSort.toString()), labelSort, Seq(NonTerminal(labelSort), Terminal(":" + castSort.toString())), attrs1.add(Att.FORMAT(), "%1%2"))); + prods.add(Production(KLabel("#SemanticCastTo" + labelSort.toString()), labelSort, Seq(NonTerminal(labelSort), Terminal(":" + castSort.toString())), attrs1.add(Att.FORMAT(), "%1%2"))); prods.add(Production(KLabel("#InnerCast"), castSort, Seq(Terminal("{"), NonTerminal(labelSort), Terminal("}"), Terminal("<:" + castSort.toString())), attrs1.add(Att.FORMAT(), "%1 %2 %3%4"))); prods.add(Production(KLabel("#OuterCast"), labelSort, Seq(Terminal("{"), NonTerminal(innerSort), Terminal("}"), Terminal(":>" + castSort.toString())), attrs1.add(Att.FORMAT(), "%1 %2 %3%4"))); return prods; diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/RemoveOverloads.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/RemoveOverloads.java index 7898b3cc6b6..7f0868b4faf 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/RemoveOverloads.java +++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/RemoveOverloads.java @@ -12,12 +12,7 @@ import java.util.Set; import java.util.stream.Collectors; -public class RemoveOverloads { - private final POSet overloads; - - public RemoveOverloads(POSet overloads) { - this.overloads = overloads; - } +public record RemoveOverloads(POSet overloads) { public Term apply(Ambiguity a) { Set productions = new HashSet<>(); @@ -29,7 +24,7 @@ public Term apply(Ambiguity a) { } } Set candidates = overloads.minimal(productions); - Ambiguity result = Ambiguity.apply(a.items().stream().filter(t -> candidates.contains(((ProductionReference)t).production())).collect(Collectors.toSet())); + Ambiguity result = Ambiguity.apply(a.items().stream().filter(t -> candidates.contains(((ProductionReference) t).production())).collect(Collectors.toSet())); if (result.items().size() == 1) { return result.items().iterator().next(); } diff --git a/kernel/src/main/java/org/kframework/parser/inner/kernel/EarleyParser.java b/kernel/src/main/java/org/kframework/parser/inner/kernel/EarleyParser.java index 8b24d81d73d..dd8995f655f 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/kernel/EarleyParser.java +++ b/kernel/src/main/java/org/kframework/parser/inner/kernel/EarleyParser.java @@ -78,15 +78,8 @@ private interface EarleyProductionItem { * * The sort is represented as an index within the `sorts` field. */ - private static final class EarleyNonTerminal implements EarleyProductionItem { - public EarleyNonTerminal(int sort, List sorts) { - this.sort = sort; - this.sorts = sorts; - } - - final int sort; - final List sorts; - + private record EarleyNonTerminal(int sort, List sorts) + implements EarleyProductionItem { public boolean isNonTerminal() { return true; } public boolean isNullable(BitSet nullable) { return nullable.get(sort); } @@ -101,15 +94,8 @@ public String toString() { * The terminal is represented by a particular token kind as informed by the provided {@link Scanner}. * Token 0 is always the EOF token, which should appear only in the production used by the start state of the parser. */ - private static final class EarleyTerminal implements EarleyProductionItem { - public EarleyTerminal(Scanner scanner, int kind) { - this.scanner = scanner; - this.kind = kind; - } - - private final Scanner scanner; - final int kind; - + private record EarleyTerminal(Scanner scanner, int kind) + implements EarleyProductionItem { public boolean isNonTerminal() { return false; } public boolean isNullable(BitSet ignored) { return false; } diff --git a/kernel/src/main/java/org/kframework/unparser/AddBrackets.java b/kernel/src/main/java/org/kframework/unparser/AddBrackets.java index a9f995f8b50..4e38384f5b3 100644 --- a/kernel/src/main/java/org/kframework/unparser/AddBrackets.java +++ b/kernel/src/main/java/org/kframework/unparser/AddBrackets.java @@ -29,12 +29,7 @@ * the same terminals in such a way as to cause ambiguities that cannot be resolved using priorities and associativities. * As such, we use this algorithm in krun in output --pretty, but it is insufficient for --output sound. */ -public class AddBrackets { - - private final Module m; - public AddBrackets(Module m) { - this.m = m; - } +public record AddBrackets(Module m) { public ProductionReference addBrackets(ProductionReference t) { return addBrackets(t, null, null); @@ -70,8 +65,7 @@ public ProductionReference addBrackets(ProductionReference inner, TermCons outer .filter(i -> i instanceof NonTerminal) .map(i -> (NonTerminal) i) .map(NonTerminal::sort) - .filter(s -> m.subsorts().lessThanEq(innerSort, s)) - .findAny().isPresent(); + .anyMatch(s -> m.subsorts().lessThanEq(innerSort, s)); if (isCorrectInnerSort) { return TermCons.apply(ConsPStack.singleton(inner), p); } @@ -118,24 +112,6 @@ boolean requiresBracketWithSimpleAlgorithm(ProductionReference outer, Production return false; } - private boolean isRightAssoc(ProductionReference outer, ProductionReference inner) { - Tag parentLabel = new Tag(outer.production().klabel().get().name()); - Tag localLabel = new Tag(inner.production().klabel().get().name()); - if (m.rightAssoc().contains(new Tuple2<>(parentLabel, localLabel))) { - return true; - } - return false; - } - - private boolean isLeftAssoc(ProductionReference outer, ProductionReference inner) { - Tag parentLabel = new Tag(outer.production().klabel().get().name()); - Tag localLabel = new Tag(inner.production().klabel().get().name()); - if (m.leftAssoc().contains(new Tuple2<>(parentLabel, localLabel))) { - return true; - } - return false; - } - private boolean isPriorityWrong(ProductionReference outer, ProductionReference inner, int position) { if (outer.production().klabel().isEmpty() || inner.production().klabel().isEmpty()) { return false; @@ -157,21 +133,6 @@ private boolean isPriorityWrong(ProductionReference outer, ProductionReference i return false; } - private boolean isPriorityWrong(ProductionReference outer, ProductionReference inner) { - Tag parentLabel = new Tag(outer.production().klabel().get().name()); - Tag localLabel = new Tag(inner.production().klabel().get().name()); - if (m.priorities().lessThan(parentLabel, localLabel)) { - return true; - } - if (m.leftAssoc().contains(new Tuple2<>(parentLabel, localLabel))) { - return true; - } - if (m.rightAssoc().contains(new Tuple2<>(parentLabel, localLabel))) { - return true; - } - return false; - } - private enum Fixity { BARE_LEFT, BARE_RIGHT diff --git a/kernel/src/main/java/org/kframework/unparser/KPrint.java b/kernel/src/main/java/org/kframework/unparser/KPrint.java index 098369d9c59..7c137c71e62 100644 --- a/kernel/src/main/java/org/kframework/unparser/KPrint.java +++ b/kernel/src/main/java/org/kframework/unparser/KPrint.java @@ -121,11 +121,11 @@ public void prettyPrint(Definition def, Module module, Consumer print, K } public void prettyPrint(Definition def, Module module, Consumer print, K result, Sort s) { - print.accept(prettyPrint(def, module, result, s, options.color(tty.stdout, files.getEnv()), options.output)); + print.accept(prettyPrint(def, module, result, s, options.color(tty.stdout(), files.getEnv()), options.output)); } public byte[] prettyPrint(Definition def, Module module, K result) { - return prettyPrint(def, module, result, Sorts.GeneratedTopCell(), options.color(tty.stdout, files.getEnv()), options.output); + return prettyPrint(def, module, result, Sorts.GeneratedTopCell(), options.color(tty.stdout(), files.getEnv()), options.output); } public byte[] prettyPrint(Definition def, Module module, K orig, Sort s, ColorSetting colorize, OutputModes outputMode) { @@ -176,7 +176,7 @@ public static byte[] serialize(K term, OutputModes outputMode) { } public String unparseTerm(K input, Module test) { - return unparseTerm(input, test, options.color(tty.stdout, files.getEnv())); + return unparseTerm(input, test, options.color(tty.stdout(), files.getEnv())); } public String unparseTerm(K input, Module test, ColorSetting colorize) { diff --git a/kernel/src/main/java/org/kframework/utils/InterrupterRunnable.java b/kernel/src/main/java/org/kframework/utils/InterrupterRunnable.java index 61028cde4e3..9e31a10780b 100644 --- a/kernel/src/main/java/org/kframework/utils/InterrupterRunnable.java +++ b/kernel/src/main/java/org/kframework/utils/InterrupterRunnable.java @@ -7,15 +7,7 @@ * @author Denis Bogdanas * Created on 24-Dec-18. */ -public class InterrupterRunnable implements Runnable { - - private final Thread thread; - private final long waitTimeMillis; - - public InterrupterRunnable(Thread thread, long waitTimeMillis) { - this.thread = thread; - this.waitTimeMillis = waitTimeMillis; - } +public record InterrupterRunnable(Thread thread, long waitTimeMillis) implements Runnable { @Override public void run() { diff --git a/kernel/src/main/java/org/kframework/utils/RunProcess.java b/kernel/src/main/java/org/kframework/utils/RunProcess.java index 9d71951c3b4..204d70fb350 100644 --- a/kernel/src/main/java/org/kframework/utils/RunProcess.java +++ b/kernel/src/main/java/org/kframework/utils/RunProcess.java @@ -10,7 +10,6 @@ import java.io.InputStream; import java.io.PrintStream; import java.util.Map; -import java.util.Scanner; import java.util.function.Supplier; // instantiate processes @@ -26,27 +25,16 @@ public static Thread getOutputStreamThread(Supplier in, PrintStream return new Thread(() -> { try { IOUtils.copy(in.get(), out); - } catch (IOException e) {} + } catch (IOException ignored) {} }); } - public static class ProcessOutput { - public final byte[] stdout; - public final byte[] stderr; - public final int exitCode; - - public ProcessOutput(byte[] stdout, byte[] stderr, int exitCode) { - this.stdout = stdout; - this.stderr = stderr; - this.exitCode = exitCode; - } + public record ProcessOutput(byte[] stdout, byte[] stderr, int exitCode) { } private RunProcess() {} public static ProcessOutput execute(Map environment, ProcessBuilder pb, String... commands) { - - try { if (commands.length <= 0) { throw KEMException.criticalError("Need command options to run"); diff --git a/kernel/src/main/java/org/kframework/utils/file/TTYInfo.java b/kernel/src/main/java/org/kframework/utils/file/TTYInfo.java index b88d0ccdb42..c0a9f6cc016 100644 --- a/kernel/src/main/java/org/kframework/utils/file/TTYInfo.java +++ b/kernel/src/main/java/org/kframework/utils/file/TTYInfo.java @@ -6,16 +6,7 @@ * connected to terminals. Essentially, each boolean in this class is * true if and only if the corresponding stream is one for which * ultimately the isatty function returns true. - * @author dwightguth * + * @author dwightguth */ -public class TTYInfo { - - public final boolean stdin, stdout, stderr; - - public TTYInfo(boolean stdin, boolean stdout, boolean stderr) { - this.stdin = stdin; - this.stdout = stdout; - this.stderr = stderr; - } -} +public record TTYInfo(boolean stdin, boolean stdout, boolean stderr) {} diff --git a/kernel/src/test/java/org/kframework/lsp/LSPTests.java b/kernel/src/test/java/org/kframework/lsp/LSPTests.java index f9e6f83c9ad..fd880e98e81 100644 --- a/kernel/src/test/java/org/kframework/lsp/LSPTests.java +++ b/kernel/src/test/java/org/kframework/lsp/LSPTests.java @@ -121,10 +121,10 @@ public void testKLSPathK() throws IOException { System.out.println(caches.size()); KPos pos = new KPos(10, 11); - Map ch = caches.entrySet().stream().filter(elm -> elm.getKey().startsWith("TEST-RULE-CELLS")).findFirst().get().getValue().getCache(); + Map ch = caches.entrySet().stream().filter(elm -> elm.getKey().startsWith("TEST-RULE-CELLS")).findFirst().get().getValue().cache(); ParseCache.ParsedSentence rl = ch.entrySet().stream().filter(r -> r.getKey().equals("1 => 2")).findFirst().get().getValue(); - K ast = rl.getParse(); + K ast = rl.parse(); AtomicReference x = new AtomicReference<>(); KViz.from(t -> { if (TextDocumentSyncHandler.isPositionOverLocation(pos, t.location().get())) {