diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java index ac85673bfba..e9b27b88f53 100644 --- a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java +++ b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java @@ -201,8 +201,7 @@ public void convert(boolean heatCoolEq, String prelude, StringBuilder semantics, SetMultimap functionRules = HashMultimap.create(); for (Rule rule : sortedRules) { K left = RewriteToTop.toLeft(rule.body()); - if (left instanceof KApply) { - KApply kapp = (KApply) left; + if (left instanceof KApply kapp) { Production prod = production(kapp); if (prod.att().contains(Att.FUNCTION()) || rule.att().contains(Att.ANYWHERE()) || ExpandMacros.isMacro(rule)) { functionRules.put(kapp.klabel(), rule); diff --git a/kernel/src/main/java/org/kframework/compile/AddCoolLikeAtt.java b/kernel/src/main/java/org/kframework/compile/AddCoolLikeAtt.java index a519df7b0cc..12c63782981 100644 --- a/kernel/src/main/java/org/kframework/compile/AddCoolLikeAtt.java +++ b/kernel/src/main/java/org/kframework/compile/AddCoolLikeAtt.java @@ -53,8 +53,7 @@ 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 (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 b97cf28b056..195f1a22053 100644 --- a/kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java +++ b/kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java @@ -48,11 +48,9 @@ public Sentence apply(Module m, Sentence 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 +72,7 @@ private boolean shouldConsider(List 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 +85,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()) diff --git a/kernel/src/main/java/org/kframework/compile/AddImplicitCounterCell.java b/kernel/src/main/java/org/kframework/compile/AddImplicitCounterCell.java index 2ef876d6050..8fc7fb045b8 100644 --- a/kernel/src/main/java/org/kframework/compile/AddImplicitCounterCell.java +++ b/kernel/src/main/java/org/kframework/compile/AddImplicitCounterCell.java @@ -21,8 +21,7 @@ public class AddImplicitCounterCell { public AddImplicitCounterCell() {} public Sentence apply(Module m, Sentence s) { - if(s instanceof Claim) { - Claim claim = (Claim) s; + if(s instanceof Claim claim) { return claim.newInstance(apply(claim.body(), m), claim.requires(), claim.ensures(), claim.att()); } 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 4b9ee81bbdb..7d206e1dbb9 100644 --- a/kernel/src/main/java/org/kframework/compile/AddParentCells.java +++ b/kernel/src/main/java/org/kframework/compile/AddParentCells.java @@ -181,8 +181,7 @@ Optional getLevel(K k) { } } return Optional.empty(); - } else if (k instanceof KRewrite) { - KRewrite rew = (KRewrite) k; + } else if (k instanceof KRewrite rew) { List cells = IncompleteCellUtils.flattenCells(rew.left()); cells.addAll(IncompleteCellUtils.flattenCells(rew.right())); Optional level = Optional.empty(); @@ -205,8 +204,7 @@ Optional getLevel(K k) { } Optional getParent(K k) { - if (k instanceof KApply) { - final KApply app = (KApply) k; + if (k instanceof final KApply app) { if (KLabels.CELLS.equals(app.klabel())) { List items = app.klist().items(); if (items.isEmpty()) { @@ -246,10 +244,9 @@ Optional getParent(K k) { } K concretizeCell(K k) { - if (!(k instanceof KApply)) { + if (!(k instanceof KApply app)) { return k; } else { - KApply app = (KApply) k; KLabel target = app.klabel(); if (cfg.isLeafCell(target)) { return k; @@ -291,8 +288,7 @@ K concretizeCell(K k) { } K concretize(K term) { - if (term instanceof KApply) { - KApply app = (KApply) term; + if (term instanceof KApply app) { KApply newTerm = KApply(app.klabel(), KList(app.klist().stream() .map(this::concretize).collect(Collectors.toList())), app.att()); if (cfg.isParentCell(newTerm.klabel())) { @@ -300,8 +296,7 @@ K concretize(K term) { } else { return newTerm; } - } else if (term instanceof KRewrite) { - KRewrite rew = (KRewrite) term; + } else if (term instanceof KRewrite rew) { return KRewrite(concretize(rew.left()), concretize(rew.right())); } else if (term instanceof KSequence) { return KSequence(((KSequence) term).stream() @@ -314,11 +309,9 @@ K concretize(K term) { } public Sentence concretize(Sentence m) { - if (m instanceof RuleOrClaim) { - RuleOrClaim r = (RuleOrClaim) m; + if (m instanceof RuleOrClaim r) { return r.newInstance(concretize(r.body()), r.requires(), r.ensures(), r.att()); - } else if (m instanceof Context) { - Context c = (Context) m; + } else if (m instanceof Context c) { return new Context(concretize(c.body()), c.requires(), c.att()); } else { return m; diff --git a/kernel/src/main/java/org/kframework/compile/AddSortInjections.java b/kernel/src/main/java/org/kframework/compile/AddSortInjections.java index a4bfddabbe7..3cb2a329ca1 100644 --- a/kernel/src/main/java/org/kframework/compile/AddSortInjections.java +++ b/kernel/src/main/java/org/kframework/compile/AddSortInjections.java @@ -186,8 +186,7 @@ private K visitChildren(K term, Sort actualSort, Sort expectedSort) { if (actualSort.name().equals(SORTPARAM_NAME)) { sortParams.add(actualSort.params().head().name()); } - if (term instanceof KApply) { - KApply kapp = (KApply)term; + if (term instanceof KApply kapp) { if (kapp.klabel().name().equals("inj")) { return term; } @@ -208,8 +207,7 @@ private K visitChildren(K term, Sort actualSort, Sort expectedSort) { children.add(internalAddSortInjections(child, expectedSortOfChild)); } return KApply(substituted.klabel().get(), KList(children), att); - } else if (term instanceof KRewrite) { - KRewrite rew = (KRewrite) term; + } else if (term instanceof KRewrite rew) { isLHS = true; K lhs = internalAddSortInjections(rew.left(), actualSort); isLHS = false; @@ -220,8 +218,7 @@ private K visitChildren(K term, Sort actualSort, Sort expectedSort) { return KToken(((KToken) term).s(), ((KToken) term).sort(), att); } else if (term instanceof InjectedKLabel) { return InjectedKLabel(((InjectedKLabel) term).klabel(), att); - } else if (term instanceof KSequence) { - KSequence kseq = (KSequence)term; + } else if (term instanceof KSequence kseq) { List children = new ArrayList<>(); for (int i = 0; i < kseq.size(); i++) { K child = kseq.items().get(i); @@ -233,8 +230,7 @@ private K visitChildren(K term, Sort actualSort, Sort expectedSort) { } } return KSequence(children, att); - } else if (term instanceof KAs) { - KAs kas = (KAs)term; + } else if (term instanceof KAs kas) { return KAs(internalAddSortInjections(kas.pattern(), actualSort), kas.alias(), att); } else { throw KEMException.internalError("Invalid category of k found.", term); @@ -323,8 +319,7 @@ public Sort topSort(K term) { * Compute the sort of a term with a particular expected sort. */ public Sort sort(K term, Sort expectedSort) { - if (term instanceof KApply) { - KApply kapp = (KApply)term; + if (term instanceof KApply kapp) { if (kapp.klabel().name().equals("inj")) { return kapp.klabel().params().apply(1); } @@ -381,8 +376,7 @@ public Sort sort(K term, Sort expectedSort) { substituted = prod.substitute(immutable(args)); } return substituted.sort(); - } else if (term instanceof KRewrite) { - KRewrite rew = (KRewrite)term; + } else if (term instanceof KRewrite rew) { Sort leftSort = sort(rew.left(), expectedSort); Sort rightSort = sort(rew.right(), expectedSort); return lubSort(leftSort, rightSort, expectedSort, term, mod); @@ -394,8 +388,7 @@ public Sort sort(K term, Sort expectedSort) { return Sorts.K(); } else if (term instanceof InjectedKLabel) { return Sorts.KItem(); - } else if (term instanceof KAs) { - KAs as = (KAs) term; + } else if (term instanceof KAs as) { Sort patternSort = sort(as.pattern(), expectedSort); Sort rightSort = sort(as.alias(), expectedSort); return lubSort(patternSort, rightSort, expectedSort, term, mod); diff --git a/kernel/src/main/java/org/kframework/compile/AddTopCellToRules.java b/kernel/src/main/java/org/kframework/compile/AddTopCellToRules.java index 61381c3cdad..51d83c83165 100644 --- a/kernel/src/main/java/org/kframework/compile/AddTopCellToRules.java +++ b/kernel/src/main/java/org/kframework/compile/AddTopCellToRules.java @@ -92,8 +92,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()); diff --git a/kernel/src/main/java/org/kframework/compile/CloseCells.java b/kernel/src/main/java/org/kframework/compile/CloseCells.java index fd5fee249ba..42c43928de6 100644 --- a/kernel/src/main/java/org/kframework/compile/CloseCells.java +++ b/kernel/src/main/java/org/kframework/compile/CloseCells.java @@ -154,8 +154,7 @@ protected KApply closeCell(KApply cell) { } requiredRight = new HashSet<>(requiredLeft); for (K item : contents) { - if (item instanceof KRewrite) { - KRewrite rw = (KRewrite) item; + if (item instanceof KRewrite rw) { for (K leftItem : IncompleteCellUtils.flattenCells(rw.left())) { filterRequired(requiredLeft, leftItem); } diff --git a/kernel/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java b/kernel/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java index 3c4b4d160f0..ba0b95868f1 100644 --- a/kernel/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java +++ b/kernel/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java @@ -31,8 +31,7 @@ public ComputeTransitiveFunctionDependencies(Module module) { Set anywhereKLabels = new HashSet<>(); stream(module.rules()).filter(r -> !ExpandMacros.isMacro(r)).forEach(r -> { K left = RewriteToTop.toLeft(r.body()); - if (left instanceof KApply) { - KApply kapp = (KApply) left; + if (left instanceof KApply kapp) { if (r.att().contains(Att.ANYWHERE())) { if (kapp.klabel().name().equals(KLabels.INJ)) { K k = kapp.items().get(0); diff --git a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java index 1fb51489e3b..c0efd55e332 100644 --- a/kernel/src/main/java/org/kframework/compile/ConstantFolding.java +++ b/kernel/src/main/java/org/kframework/compile/ConstantFolding.java @@ -41,8 +41,7 @@ void setLoc(K loc) { } public Sentence fold(Module module, Sentence sentence) { - if (sentence instanceof Rule) { - Rule r = (Rule)sentence; + if (sentence instanceof Rule r) { return Rule(fold(module, r.body(), true), fold(module, r.requires(), false), fold(module, r.ensures(), false), r.att()); } return sentence; diff --git a/kernel/src/main/java/org/kframework/compile/ConvertDataStructureToLookup.java b/kernel/src/main/java/org/kframework/compile/ConvertDataStructureToLookup.java index be789f69eda..6f0759b24a3 100644 --- a/kernel/src/main/java/org/kframework/compile/ConvertDataStructureToLookup.java +++ b/kernel/src/main/java/org/kframework/compile/ConvertDataStructureToLookup.java @@ -354,8 +354,7 @@ private K convertList(KApply k, KLabel collectionLabel, List components) { } frame = (KVariable) component; isRight = true; - } else if (component instanceof KApply) { - KApply kapp = (KApply) component; + } else if (component instanceof KApply kapp) { boolean needsWrapper = false; if (kapp.klabel().equals(elementLabel) || (needsWrapper = kapp.klabel().equals(getWrapElement(collectionLabel)))) { @@ -444,10 +443,9 @@ private K convertMap(KApply k, KLabel collectionLabel, List components, Multi throw KEMException.internalError("Unsupported associative matching on Map. Found variables " + component + " and " + frame, k); } frame = (KVariable) component; - } else if (component instanceof KApply) { + } else if (component instanceof KApply kapp) { boolean needsWrapper = false; - KApply kapp = (KApply) component; if (kapp.klabel().equals(KLabel(m.attributesFor().apply(collectionLabel).get(Att.ELEMENT()))) || (needsWrapper = kapp.klabel().equals(getWrapElement(collectionLabel)))) { if (kapp.klist().size() != 2 && !needsWrapper) { @@ -520,8 +518,7 @@ private K convertSet(KApply k, KLabel collectionLabel, List components) { throw KEMException.internalError("Unsupported associative matching on Set. Found variables " + component + " and " + frame, k); } frame = (KVariable) component; - } else if (component instanceof KApply) { - KApply kapp = (KApply) component; + } else if (component instanceof KApply kapp) { boolean needsWrapper = false; if (kapp.klabel().equals(elementLabel) diff --git a/kernel/src/main/java/org/kframework/compile/ExpandMacros.java b/kernel/src/main/java/org/kframework/compile/ExpandMacros.java index 0e6978b69c2..f4f39e35f5c 100644 --- a/kernel/src/main/java/org/kframework/compile/ExpandMacros.java +++ b/kernel/src/main/java/org/kframework/compile/ExpandMacros.java @@ -315,9 +315,8 @@ private Set sort(K k, RuleOrClaim r) { return Collections.singleton(k.att().getOptional(Sort.class).orElse(null)); } else if (k instanceof KToken) { return Collections.singleton(((KToken)k).sort()); - } else if (k instanceof KApply) { - KApply kapp = (KApply)k; - if (kapp.klabel() instanceof KVariable) { + } else if (k instanceof KApply kapp) { + if (kapp.klabel() instanceof KVariable) { throw KEMException.compilerError("Cannot compute macros with klabel variables.", r); } Set prods = new HashSet<>(mutable(mod.productionsFor().apply(kapp.klabel()))); @@ -364,10 +363,8 @@ private boolean match(Map subst, K pattern, K subject, RuleOrClaim } } } - if (pattern instanceof KApply && subject instanceof KApply) { - KApply p = (KApply)pattern; - KApply s = (KApply)subject; - if (p.klabel() instanceof KVariable || s.klabel() instanceof KVariable) { + if (pattern instanceof KApply p && subject instanceof KApply s) { + if (p.klabel() instanceof KVariable || s.klabel() instanceof KVariable) { throw KEMException.compilerError("Cannot compute macros with klabel variables.", r); } if (!p.klabel().name().equals(s.klabel().name())) { diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java b/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java index 502fec251af..2f40bc08d47 100644 --- a/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java +++ b/kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java @@ -79,16 +79,14 @@ public static Set gen(K body, K ensures, Att att, Module m) { * @return A tuple of the sentences generated, a list of the sorts of the children of the cell, and the body of the initializer. */ private static Tuple4, List, K, Boolean> genInternal(K term, K ensures, Att cfgAtt, Module m) { - if (term instanceof KApply) { - KApply kapp = (KApply) term; + if (term instanceof KApply kapp) { if (kapp.klabel().name().equals("#configCell")) { // is a single cell if (kapp.klist().size() == 4) { K startLabel = kapp.klist().items().get(0); K endLabel = kapp.klist().items().get(3); if (startLabel.equals(endLabel)) { - if (startLabel instanceof KToken) { - KToken label = (KToken) startLabel; + if (startLabel instanceof KToken label) { if (label.sort().equals(Sort("#CellName"))) { String cellName = label.s(); Att cellProperties = getCellPropertiesAsAtt(kapp.klist().items().get(1), cellName, ensures); @@ -115,8 +113,7 @@ private static Tuple4, List, K, Boolean> genInternal(K term, } else if (kapp.klabel().name().equals("#externalCell")) { if (kapp.klist().size() == 1) { K startLabel = kapp.klist().items().get(0); - if (startLabel instanceof KToken) { - KToken label = (KToken) startLabel; + if (startLabel instanceof KToken label) { if (label.sort().equals(Sort("#CellName"))) { String cellName = label.s(); Sort sort = Sort(getSortOfCell(cellName)); @@ -166,10 +163,9 @@ private static Tuple4, List, K, Boolean> genInternal(K term, Sort sort = kapp.att().get(Production.class).sort(); Tuple2> res = getLeafInitializer(term, m); return Tuple4.apply(res._2(), Lists.newArrayList(sort), res._1(), true); - } else if (term instanceof KToken) { + } else if (term instanceof KToken ktoken) { // child of a leaf cell. Generate no productions, but inform parent that it has a child of a particular sort. // A leaf cell initializes to the value specified in the configuration declaration. - KToken ktoken = (KToken) term; Tuple2> res = getLeafInitializer(term, m); return Tuple4.apply(res._2(), Lists.newArrayList(ktoken.sort()), res._1(), true); } else if (term instanceof KSequence || term instanceof KVariable || term instanceof InjectedKLabel) { @@ -217,8 +213,7 @@ public void apply(KApply kapp) { if (kapp.klabel().name().equals("#externalCell")) { if (kapp.klist().size() == 1) { K startLabel = kapp.klist().items().get(0); - if (startLabel instanceof KToken) { - KToken label = (KToken) startLabel; + if (startLabel instanceof KToken label) { if (label.sort().equals(Sort("#CellName"))) { String cellName = label.s(); Sort sort = Sort(getSortOfCell(cellName)); @@ -580,8 +575,7 @@ private static Att getCellPropertiesAsAtt(K k, String cellName, K ensures) { } private static Att getCellPropertiesAsAtt(K k) { - if (k instanceof KApply) { - KApply kapp = (KApply) k; + if (k instanceof KApply kapp) { if (kapp.klabel().name().equals("#cellPropertyListTerminator")) { return Att(); } else if (kapp.klabel().name().equals("#cellPropertyList")) { @@ -598,12 +592,10 @@ private static Att getCellPropertiesAsAtt(K k) { } private static Tuple2 getCellProperty(K k) { - if (k instanceof KApply) { - KApply kapp = (KApply) k; + if (k instanceof KApply kapp) { if (kapp.klabel().name().equals("#cellProperty")) { if (kapp.klist().size() == 2) { - if (kapp.klist().items().get(0) instanceof KToken) { - KToken keyToken = (KToken) kapp.klist().items().get(0); + if (kapp.klist().items().get(0) instanceof KToken keyToken) { if (keyToken.sort().equals(Sort("#CellName"))) { Att.Key key = Att.getBuiltinKeyOptional(keyToken.s()) .orElseThrow(() -> diff --git a/kernel/src/main/java/org/kframework/compile/MarkExtraConcreteRules.java b/kernel/src/main/java/org/kframework/compile/MarkExtraConcreteRules.java index b3e6393b144..1ec0c8c2607 100644 --- a/kernel/src/main/java/org/kframework/compile/MarkExtraConcreteRules.java +++ b/kernel/src/main/java/org/kframework/compile/MarkExtraConcreteRules.java @@ -22,8 +22,7 @@ public static Definition mark(Definition def, @Nullable List extraConcre } HashSet concreteLabelsSet = new HashSet<>(extraConcreteRuleLabels); Definition result = DefinitionTransformer.fromSentenceTransformer((mod, s) -> { - if (s instanceof Rule) { - Rule r = (Rule) s; + if (s instanceof Rule r) { String label = r.att().getOption(Att.LABEL()).getOrElse(() -> null); if (label != null && concreteLabelsSet.contains(label)) { // rule labels must be unique, so it's safe to remove from the set as we iterate diff --git a/kernel/src/main/java/org/kframework/compile/RemoveUnit.java b/kernel/src/main/java/org/kframework/compile/RemoveUnit.java index 8b969b0598f..4a9c3e96caa 100644 --- a/kernel/src/main/java/org/kframework/compile/RemoveUnit.java +++ b/kernel/src/main/java/org/kframework/compile/RemoveUnit.java @@ -29,10 +29,9 @@ public Module apply(Module module) { } private Stream gen(Sentence s) { - if (!(s instanceof Rule)) { + if (!(s instanceof Rule r)) { return Stream.of(s); } - Rule r = (Rule)s; K body = flattenLists(r.body()); K requires = flattenLists(r.requires()); K ensures = flattenLists(r.ensures()); diff --git a/kernel/src/main/java/org/kframework/compile/ResolveContexts.java b/kernel/src/main/java/org/kframework/compile/ResolveContexts.java index 8e1715c9e64..3c5ade584ba 100644 --- a/kernel/src/main/java/org/kframework/compile/ResolveContexts.java +++ b/kernel/src/main/java/org/kframework/compile/ResolveContexts.java @@ -184,8 +184,7 @@ public void apply(KApply k) { // TODO(dwightguth): generate freezers better for pretty-printing purposes List items = new ArrayList<>(); KLabel freezerLabel; - if (cooled instanceof KApply) { - KApply kApply = (KApply)cooled; + if (cooled instanceof KApply kApply) { String name = kApply.klabel().name(); if (name.equals("#SemanticCastToK")) { K firstArg = kApply.klist().items().get(0); @@ -309,8 +308,7 @@ public void apply(KRewrite k) { // return true when k is either HOLE or #SemanticCastToX(HOLE) private boolean isHOLE(K k) { - if (k instanceof KApply) { - KApply kapp = (KApply) k; + if (k instanceof KApply kapp) { return kapp.klabel().name().startsWith("#SemanticCastTo") && kapp.klist().size() == 1 && isHOLEVar(kapp.klist().items().get(0)); diff --git a/kernel/src/main/java/org/kframework/compile/ResolveFreshConfigConstants.java b/kernel/src/main/java/org/kframework/compile/ResolveFreshConfigConstants.java index dd21c8c875c..b722627a9d4 100644 --- a/kernel/src/main/java/org/kframework/compile/ResolveFreshConfigConstants.java +++ b/kernel/src/main/java/org/kframework/compile/ResolveFreshConfigConstants.java @@ -37,11 +37,10 @@ public class ResolveFreshConfigConstants { * fresh constant */ private K transform(RuleOrClaim r, K body) { - if (!(r instanceof Rule)) { + if (!(r instanceof Rule rule)) { return body; } - Rule rule = (Rule) r; if (!rule.att().contains(Att.INITIALIZER())) { return body; } diff --git a/kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java b/kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java index fdf468a2217..3c96a020dd1 100644 --- a/kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java +++ b/kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java @@ -72,8 +72,7 @@ private Rule resolve(Rule rule) { rule.att()); if (rule.att().contains(Att.INITIALIZER())) { K left = RewriteToTop.toLeft(withFresh.body()); - if (left instanceof KApply) { - KApply kapp = (KApply) left; + if (left instanceof KApply kapp) { if (kapp.klabel().equals(KLabels.INIT_GENERATED_TOP_CELL)) { KApply right = (KApply)RewriteToTop.toRight(withFresh.body()); KApply cells = (KApply)right.items().get(1); @@ -91,8 +90,7 @@ private Rule resolve(Rule rule) { } } K left = RewriteToTop.toLeft(rule.body()); - if (left instanceof KApply) { - KApply kapp = (KApply)left; + if (left instanceof KApply kapp) { if (kapp.klabel().name().equals("#withConfig")) { left = kapp.items().get(0); } @@ -255,8 +253,7 @@ private static Production fixFormat(Production prod) { List cellPositions = new ArrayList(); int i = 1; for (ProductionItem p: JavaConverters.seqAsJavaList(prod.items())) { - if (p instanceof NonTerminal) { - NonTerminal nt = (NonTerminal) p; + if (p instanceof NonTerminal nt) { if (! nt.sort().equals(Sorts.GeneratedCounterCell())) { cellPositions.add(i); } diff --git a/kernel/src/main/java/org/kframework/compile/ResolveFunctionWithConfig.java b/kernel/src/main/java/org/kframework/compile/ResolveFunctionWithConfig.java index 5221572e610..aa832c24f59 100644 --- a/kernel/src/main/java/org/kframework/compile/ResolveFunctionWithConfig.java +++ b/kernel/src/main/java/org/kframework/compile/ResolveFunctionWithConfig.java @@ -122,9 +122,8 @@ public K apply(KApply kapp) { } private K resolve(K body, Module module) { - if (body instanceof KApply) { - KApply kapp = (KApply) body; - if (kapp.klabel().name().equals("#withConfig")) { + if (body instanceof KApply kapp) { + if (kapp.klabel().name().equals("#withConfig")) { K fun = kapp.items().get(0); K cell = kapp.items().get(1); K rhs = null; @@ -134,18 +133,16 @@ private K resolve(K body, Module module) { fun = rew.left(); rhs = rew.right(); } - if (!(fun instanceof KApply)) { + if (!(fun instanceof KApply funKApp)) { throw KEMException.compilerError("Found term that is not a cell or a function at the top of a rule.", fun); } - KApply funKApp = (KApply)fun; - if (!module.attributesFor().apply(funKApp.klabel()).contains(Att.FUNCTION())) { + if (!module.attributesFor().apply(funKApp.klabel()).contains(Att.FUNCTION())) { throw KEMException.compilerError("Found term that is not a cell or a function at the top of a rule.", fun); } - if (!(cell instanceof KApply)) { + if (!(cell instanceof KApply cellKApp)) { throw KEMException.compilerError("Found term that is not a cell in the context of a function rule.", cell); } - KApply cellKApp = (KApply)cell; - K secondChild; + K secondChild; if (cellKApp.klabel().equals(topCellLabel)) { secondChild = cell; } else { @@ -213,9 +210,8 @@ public Boolean merge(Boolean a, Boolean b) { } public Sentence resolveConfigVar(Sentence s) { - if (s instanceof RuleOrClaim) { - RuleOrClaim r = (RuleOrClaim)s; - return r.newInstance(resolveConfigVar(r.body(), r.requires(), r.ensures()), r.requires(), r.ensures(), r.att()); + if (s instanceof RuleOrClaim r) { + return r.newInstance(resolveConfigVar(r.body(), r.requires(), r.ensures()), r.requires(), r.ensures(), r.att()); } 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 ec76d94562d..5c6a5f78544 100644 --- a/kernel/src/main/java/org/kframework/compile/ResolveIOStreams.java +++ b/kernel/src/main/java/org/kframework/compile/ResolveIOStreams.java @@ -94,8 +94,7 @@ public Module resolve(Module m) { private java.util.Set getStreamProductions(Set sentences) { java.util.Set productions = new HashSet<>(); for (Sentence s : mutable(sentences)) { - if (s instanceof Production) { - Production p = (Production) s; + if (s instanceof Production p) { if (p.att().getOption(Att.STREAM()).isDefined()) { checkStreamName(p.att().get(Att.STREAM())); productions.add(p); @@ -187,8 +186,7 @@ private java.util.Set getStreamModuleSentences(Production streamProduc java.util.Set sentences = new HashSet<>(); for (Sentence s : mutable(getStreamModule(streamName).localSentences())) { - if (s instanceof Rule) { - Rule rule = (Rule) s; + if (s instanceof Rule rule) { if (rule.att().contains(Att.STREAM())) { // Update cell names K body = new TransformK() { @@ -212,8 +210,7 @@ private KLabel apply(KLabel klabel) { } else if (rule.att().contains(Att.PROJECTION())) { sentences.add(rule); } - } else if (s instanceof Production) { - Production production = (Production) s; + } else if (s instanceof Production production) { if (production.sort().toString().equals("Stream") || production.att().contains(Att.PROJECTION())) { sentences.add(production); } @@ -257,8 +254,7 @@ private java.util.Set getStdinStreamUnblockingRules(Production streamP // find rules with currently supported matching patterns java.util.Set> rules = new HashSet<>(); for (Sentence s : sentences) { - if (s instanceof Rule) { - Rule rule = (Rule) s; + if (s instanceof Rule rule) { java.util.List sorts = isSupportingRulePatternAndGetSortNameOfCast(streamProduction, rule); assert sorts.size() <= 1; if (sorts.size() == 1) { @@ -402,8 +398,7 @@ private K getUnblockRuleBody(Production streamProduction, String sort) { public K apply(KApply k) { if (k.klabel().name().equals("#SemanticCastToString") && k.klist().size() == 1) { K i = k.klist().items().get(0); - if (i instanceof KVariable) { - KVariable x = (KVariable) i; + if (i instanceof KVariable x) { switch (x.name()) { case "?Sort": return KToken("\"" + sort + "\"", Sorts.String()); diff --git a/kernel/src/main/java/org/kframework/compile/ResolveSemanticCasts.java b/kernel/src/main/java/org/kframework/compile/ResolveSemanticCasts.java index 6a4100fffbb..fc066d02f86 100644 --- a/kernel/src/main/java/org/kframework/compile/ResolveSemanticCasts.java +++ b/kernel/src/main/java/org/kframework/compile/ResolveSemanticCasts.java @@ -105,8 +105,7 @@ public void apply(KApply v) { if (v.klabel().name().startsWith("#SemanticCastTo")) { casts.add(v); K child = v.klist().items().get(0); - if (child instanceof KVariable) { - KVariable var = (KVariable) child; + if (child instanceof KVariable var) { varToTypedVar.put(var, KVariable(var.name(), var.att().contains(Sort.class) ? var.att() : var.att().add(Sort.class, Outer.parseSort(getSortNameOfCast(v))))); } } diff --git a/kernel/src/main/java/org/kframework/compile/SortCells.java b/kernel/src/main/java/org/kframework/compile/SortCells.java index ac58989c4c3..31bd73ee1b3 100644 --- a/kernel/src/main/java/org/kframework/compile/SortCells.java +++ b/kernel/src/main/java/org/kframework/compile/SortCells.java @@ -146,8 +146,7 @@ void addOccurances(KLabel cell, KVariable var, List items) { } } for (K item : items) { - if (item instanceof KApply) { - KApply kApply = (KApply) item; + if (item instanceof KApply kApply) { Sort s = cfg.getCellSort(kApply.klabel()); if (s != null && cfg.getMultiplicity(s) != Multiplicity.STAR) { remainingCells.remove(s); @@ -275,8 +274,7 @@ public void apply(KApply k) { private void processSide(KApply parentCell, boolean allowRhs, List items) { List bagVars = new ArrayList<>(); for (K item : items) { - if (item instanceof KVariable) { - KVariable var = (KVariable) item; + if (item instanceof KVariable var) { if (var.att().contains(Sort.class)) { Sort sort = var.att().get(Sort.class); if (cfg.cfg.isCell(sort)) { @@ -382,8 +380,7 @@ public K apply(KApply k) { .reduce(BooleanUtils.TRUE, BooleanUtils::and); } else if(k.klabel().name().equals("isBag") && k.klist().size() == 1 - && k.klist().items().get(0) instanceof KVariable) { - KVariable var = (KVariable)k.klist().items().get(0); + && k.klist().items().get(0) instanceof KVariable var) { VarInfo info = variables.get(var); if (info != null) { return info.getSplit(var).entrySet().stream() @@ -454,8 +451,7 @@ private Map getSplit(K item) { return concatenateStarCells(e.getKey(), e.getValue()); } })); - } else if (item instanceof KRewrite) { - KRewrite rw = (KRewrite) item; + } else if (item instanceof KRewrite rw) { Map splitLeft = new HashMap<>(getSplit(rw.left())); Map splitRight = new HashMap<>(getSplit(rw.right())); addDefaultCells(item, splitLeft, splitRight); @@ -573,8 +569,7 @@ public K apply(KApply k0) { for (int idx = 0; idx < k0.klist().size(); idx++) { K item0 = k0.klist().items().get(idx); klist0.set(idx, item0); - if (item0 instanceof KApply) { - KApply k = (KApply) item0; + if (item0 instanceof KApply k) { // incomplete cells remain as #cells(...) after processVars if (k.klabel().name().equals("#cells")) { @@ -612,8 +607,7 @@ public K apply(KApply k0) { KApply cellFragment = null; 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) { - KApply kapp = (KApply) item; + if (item instanceof KApply kapp) { if (cfg.cfg.isCellLabel(kapp.klabel())) { Sort sort = cfg.getCellSort(kapp.klabel()); if (!subcellSorts.contains(sort)) { @@ -627,8 +621,7 @@ public K apply(KApply k0) { } else { throw KEMException.compilerError("Unsupported cell fragment element.", item); } - } else if (item instanceof KVariable) { - KVariable var = (KVariable) item; + } else if (item instanceof KVariable var) { VarInfo varinfo = null; if (variables.containsKey(var)) { varinfo = variables.get(var); @@ -747,8 +740,7 @@ public void apply(KApply k) { if (k.klabel().name().equals("#cells")) { for (int i = 0; i < k.klist().size(); i++) { K item = k.klist().items().get(i); - if (item instanceof KVariable) { - KVariable var = (KVariable) item; + if (item instanceof KVariable var) { if (var.att().contains(Sort.class)) { Sort sort = var.att().get(Sort.class); if (!cfg.cfg.isCell(sort)) { @@ -817,8 +809,7 @@ public K apply(KApply k0) { for (int idx = 0; idx < k0.klist().size(); idx++) { K item0 = k0.klist().items().get(idx); klist0.set(idx, item0); - if (item0 instanceof KApply) { - KApply k = (KApply) item0; + if (item0 instanceof KApply k) { if (k.klabel().name().equals("#cells")) { if (cellFragmentVarsCell.contains(k)) { Sort cellFragmentSort = nthArgSort(k0.klabel(), idx); diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckAnonymous.java b/kernel/src/main/java/org/kframework/compile/checks/CheckAnonymous.java index f6a4b086b02..0cf1e94e395 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckAnonymous.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckAnonymous.java @@ -75,17 +75,14 @@ public void check(Sentence s) { return; } resetVars(); - if (s instanceof RuleOrClaim) { - RuleOrClaim r = (RuleOrClaim) s; + if (s instanceof RuleOrClaim r) { gatherVars(r.body()); gatherVars(r.requires()); gatherVars(r.ensures()); - } else if (s instanceof Context) { - Context c = (Context)s; + } else if (s instanceof Context c) { gatherVars(c.body()); gatherVars(c.requires()); - } else if (s instanceof ContextAlias) { - ContextAlias c = (ContextAlias)s; + } else if (s instanceof ContextAlias c) { gatherVars(c.body()); gatherVars(c.requires()); } 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 bdcebfee8a8..6b763df6334 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckAssoc.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckAssoc.java @@ -28,8 +28,7 @@ public CheckAssoc(Set errors, Module module) { } public void check(Sentence s) { - if (s instanceof Production) { - Production p = (Production) s; + if (s instanceof Production p) { if (p.arity() != 2) { return; } diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckBracket.java b/kernel/src/main/java/org/kframework/compile/checks/CheckBracket.java index 0d68a3acad8..9b826a49aa2 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckBracket.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckBracket.java @@ -21,8 +21,7 @@ public static void check(Module m) { } private static void check(ModuleItem i) { - if (i instanceof Syntax) { - Syntax s = (Syntax) i; + if (i instanceof Syntax s) { for (PriorityBlock b : s.getPriorityBlocks()) { for (Production p : b.getProductions()) { if (p.containsAttribute(Att.BRACKET())) { 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 6384cfdd7da..967bc92a781 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckFunctions.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckFunctions.java @@ -29,30 +29,26 @@ public CheckFunctions(Set errors, Module m) { } public void check(Sentence sentence) { - if (sentence instanceof Rule) { - Rule rl = (Rule) sentence; + if (sentence instanceof Rule rl) { checkFuncAtt(rl); if (!rl.att().contains(Att.SIMPLIFICATION())) // functions are allowed on the LHS of simplification rules check(rl.body()); - } else if (sentence instanceof Claim) { + } else if (sentence instanceof Claim c) { // functions are allowed on LHS of claims - Claim c = (Claim) sentence; if (c.att().contains(Att.MACRO()) || c.att().contains(Att.MACRO_REC()) || c.att().contains(Att.ALIAS()) || c.att().contains(Att.ALIAS_REC())) errors.add(KEMException.compilerError( "Attributes " + Att.MACRO() + "|" + Att.MACRO_REC() + "|" + Att.ALIAS() + "|" + Att.ALIAS_REC() + " are not allowed on claims.", c)); - } else if (sentence instanceof Context) { - Context ctx = (Context) sentence; + } else if (sentence instanceof Context ctx) { check(ctx.body()); if (ctx.att().contains(Att.MACRO()) || ctx.att().contains(Att.MACRO_REC()) || ctx.att().contains(Att.ALIAS()) || ctx.att().contains(Att.ALIAS_REC())) errors.add(KEMException.compilerError( "Attributes " + Att.MACRO() + "|" + Att.MACRO_REC() + "|" + Att.ALIAS() + "|" + Att.ALIAS_REC() + " are not allowed on contexts.", ctx)); - } else if (sentence instanceof ContextAlias) { - ContextAlias ctx = (ContextAlias) sentence; + } else if (sentence instanceof ContextAlias ctx) { check(ctx.body()); if (ctx.att().contains(Att.MACRO()) || ctx.att().contains(Att.MACRO_REC()) || ctx.att().contains(Att.ALIAS()) || ctx.att().contains(Att.ALIAS_REC())) 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 5cb323c2192..1de56a224ac 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckK.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckK.java @@ -29,8 +29,7 @@ public void apply(KAs as) { boolean error = false; if (!(as.alias() instanceof KVariable)) { error = true; - if (as.alias() instanceof KApply) { - KApply app = (KApply)as.alias(); + if (as.alias() instanceof KApply app) { if (app.klabel().name().startsWith("#SemanticCastTo") && app.items().size() == 1 && app.items().get(0) instanceof KVariable) { error = false; } @@ -45,17 +44,14 @@ public void apply(KAs as) { } public void check(Sentence s) { - if (s instanceof RuleOrClaim) { - RuleOrClaim r = (RuleOrClaim)s; + if (s instanceof RuleOrClaim r) { check(r.body()); check(r.requires()); check(r.ensures()); - } else if (s instanceof Context) { - Context c = (Context)s; + } else if (s instanceof Context c) { check(c.body()); check(c.requires()); - } else if (s instanceof ContextAlias) { - ContextAlias c = (ContextAlias)s; + } else if (s instanceof ContextAlias c) { check(c.body()); check(c.requires()); } diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckKLabels.java b/kernel/src/main/java/org/kframework/compile/checks/CheckKLabels.java index c9eaabec5a9..a7947a43dbc 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckKLabels.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckKLabels.java @@ -87,21 +87,17 @@ private void apply(KLabel klabel, K k) { } } }; - if (sentence instanceof Rule) { - Rule rl = (Rule) sentence; + if (sentence instanceof Rule rl) { checkKLabels.apply(rl.body()); checkKLabels.apply(rl.requires()); checkKLabels.apply(rl.ensures()); - } else if (sentence instanceof Context) { - Context ctx = (Context) sentence; + } else if (sentence instanceof Context ctx) { checkKLabels.apply(ctx.body()); checkKLabels.apply(ctx.requires()); - } else if (sentence instanceof ContextAlias) { - ContextAlias ctx = (ContextAlias) sentence; + } else if (sentence instanceof ContextAlias ctx) { checkKLabels.apply(ctx.body()); checkKLabels.apply(ctx.requires()); - } else if (sentence instanceof Production) { - Production prod = (Production) sentence; + } else if (sentence instanceof Production prod) { if (prod.klabel().isDefined()) { KLabel klabel = prod.klabel().get(); if (klabelProds.containsKey(klabel.name()) && !internalDuplicates.contains(klabel.name())) { diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckListDecl.java b/kernel/src/main/java/org/kframework/compile/checks/CheckListDecl.java index e4f82b263f0..f8a6744abf7 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckListDecl.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckListDecl.java @@ -37,8 +37,7 @@ private static boolean isBaseSort(Sort sort) { private static void check(ModuleItem i) { - if (i instanceof Syntax) { - Syntax s = (Syntax) i; + if (i instanceof Syntax s) { for (PriorityBlock b : s.getPriorityBlocks()) { for (Production p : b.getProductions()) { if (p.getItems().size() == 1 && p.getItems().get(0) instanceof UserList) { // Syntax Es ::= List{E,""} diff --git a/kernel/src/main/java/org/kframework/kil/Lexical.java b/kernel/src/main/java/org/kframework/kil/Lexical.java index 5cab825026e..1e444c401a3 100644 --- a/kernel/src/main/java/org/kframework/kil/Lexical.java +++ b/kernel/src/main/java/org/kframework/kil/Lexical.java @@ -27,11 +27,9 @@ public boolean equals(Object obj) { return false; if (obj == this) return true; - if (!(obj instanceof Lexical)) + if (!(obj instanceof Lexical trm)) return false; - Lexical trm = (Lexical) obj; - if (!trm.lexicalRule.equals(this.lexicalRule)) return false; return true; diff --git a/kernel/src/main/java/org/kframework/kil/NonTerminal.java b/kernel/src/main/java/org/kframework/kil/NonTerminal.java index a29c205debb..e8d4c2bef17 100644 --- a/kernel/src/main/java/org/kframework/kil/NonTerminal.java +++ b/kernel/src/main/java/org/kframework/kil/NonTerminal.java @@ -52,11 +52,9 @@ public boolean equals(Object obj) { return false; if (obj == this) return true; - if (!(obj instanceof NonTerminal)) + if (!(obj instanceof NonTerminal nt)) return false; - NonTerminal nt = (NonTerminal) obj; - if (!sort.equals(nt.sort)) return false; return true; diff --git a/kernel/src/main/java/org/kframework/kil/PriorityBlock.java b/kernel/src/main/java/org/kframework/kil/PriorityBlock.java index 6ab3096a010..776ed5c7721 100644 --- a/kernel/src/main/java/org/kframework/kil/PriorityBlock.java +++ b/kernel/src/main/java/org/kframework/kil/PriorityBlock.java @@ -66,9 +66,8 @@ public boolean equals(Object obj) { return false; if (this == obj) return true; - if (!(obj instanceof PriorityBlock)) + if (!(obj instanceof PriorityBlock pb)) return false; - PriorityBlock pb = (PriorityBlock) obj; if (!pb.getAssoc().equals(this.assoc)) return false; diff --git a/kernel/src/main/java/org/kframework/kil/PriorityBlockExtended.java b/kernel/src/main/java/org/kframework/kil/PriorityBlockExtended.java index 420381ccc58..ffccf40a51b 100644 --- a/kernel/src/main/java/org/kframework/kil/PriorityBlockExtended.java +++ b/kernel/src/main/java/org/kframework/kil/PriorityBlockExtended.java @@ -38,9 +38,8 @@ public boolean equals(Object obj) { return false; if (this == obj) return true; - if (!(obj instanceof PriorityBlockExtended)) + if (!(obj instanceof PriorityBlockExtended pb)) return false; - PriorityBlockExtended pb = (PriorityBlockExtended) obj; if (pb.productions.size() != productions.size()) return false; diff --git a/kernel/src/main/java/org/kframework/kil/PriorityExtended.java b/kernel/src/main/java/org/kframework/kil/PriorityExtended.java index c30594e6da2..c65e5e79fba 100644 --- a/kernel/src/main/java/org/kframework/kil/PriorityExtended.java +++ b/kernel/src/main/java/org/kframework/kil/PriorityExtended.java @@ -36,9 +36,8 @@ public boolean equals(Object obj) { return false; if (this == obj) return true; - if (!(obj instanceof PriorityExtended)) + if (!(obj instanceof PriorityExtended syn)) return false; - PriorityExtended syn = (PriorityExtended) obj; if (syn.priorityBlocks.size() != priorityBlocks.size()) return false; diff --git a/kernel/src/main/java/org/kframework/kil/PriorityExtendedAssoc.java b/kernel/src/main/java/org/kframework/kil/PriorityExtendedAssoc.java index 2371bd840ab..6dce9bdcfe6 100644 --- a/kernel/src/main/java/org/kframework/kil/PriorityExtendedAssoc.java +++ b/kernel/src/main/java/org/kframework/kil/PriorityExtendedAssoc.java @@ -49,9 +49,8 @@ public boolean equals(Object obj) { return false; if (this == obj) return true; - if (!(obj instanceof PriorityExtendedAssoc)) + if (!(obj instanceof PriorityExtendedAssoc syn)) return false; - PriorityExtendedAssoc syn = (PriorityExtendedAssoc) obj; if (syn.tags.size() != tags.size()) return false; diff --git a/kernel/src/main/java/org/kframework/kil/Syntax.java b/kernel/src/main/java/org/kframework/kil/Syntax.java index cd0d0af5c8e..a88dda8191c 100644 --- a/kernel/src/main/java/org/kframework/kil/Syntax.java +++ b/kernel/src/main/java/org/kframework/kil/Syntax.java @@ -82,9 +82,8 @@ public boolean equals(Object obj) { return false; if (this == obj) return true; - if (!(obj instanceof Syntax)) + if (!(obj instanceof Syntax syn)) return false; - Syntax syn = (Syntax) obj; if (!syn.getDeclaredSort().equals(this.sort)) return false; diff --git a/kernel/src/main/java/org/kframework/kil/Terminal.java b/kernel/src/main/java/org/kframework/kil/Terminal.java index 9ddf619cbf3..e3c6783a961 100644 --- a/kernel/src/main/java/org/kframework/kil/Terminal.java +++ b/kernel/src/main/java/org/kframework/kil/Terminal.java @@ -32,11 +32,9 @@ public boolean equals(Object obj) { return false; if (obj == this) return true; - if (!(obj instanceof Terminal)) + if (!(obj instanceof Terminal trm)) return false; - Terminal trm = (Terminal) obj; - if (!trm.terminal.equals(this.terminal)) return false; return true; diff --git a/kernel/src/main/java/org/kframework/kil/UserList.java b/kernel/src/main/java/org/kframework/kil/UserList.java index aaa5f42722a..162c0ccf7e7 100644 --- a/kernel/src/main/java/org/kframework/kil/UserList.java +++ b/kernel/src/main/java/org/kframework/kil/UserList.java @@ -58,11 +58,9 @@ public boolean equals(Object obj) { return false; if (obj == this) return true; - if (!(obj instanceof UserList)) + if (!(obj instanceof UserList srt)) return false; - UserList srt = (UserList) obj; - if (!sort.equals(srt.getSort())) return false; if (!separator.equals(srt.getSeparator())) diff --git a/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java b/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java index 9ce8a08456d..3201c8b9a48 100644 --- a/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java +++ b/kernel/src/main/java/org/kframework/kompile/CompiledDefinition.java @@ -100,11 +100,9 @@ private void initializeConfigurationVariableDefaultSorts(FileUtil files) { @Override public void apply(KApply k) { if (k.klabel().name().startsWith("project:") - && k.items().size() == 1 && k.items().get(0) instanceof KApply) { - KApply theMapLookup = (KApply) k.items().get(0); + && k.items().size() == 1 && k.items().get(0) instanceof KApply theMapLookup) { if (KLabels.MAP_LOOKUP.equals(theMapLookup.klabel()) - && theMapLookup.size() == 2 && theMapLookup.items().get(1) instanceof KToken) { - KToken t = (KToken) theMapLookup.items().get(1); + && theMapLookup.size() == 2 && theMapLookup.items().get(1) instanceof KToken t) { if (t.sort().equals(Sorts.KConfigVar())) { Sort sort = Outer.parseSort(k.klabel().name().substring("project:".length())); configurationVariableDefaultSorts.put(t.s(), sort); diff --git a/kernel/src/main/java/org/kframework/kompile/Kompile.java b/kernel/src/main/java/org/kframework/kompile/Kompile.java index 6c0f56f698b..8c279314223 100644 --- a/kernel/src/main/java/org/kframework/kompile/Kompile.java +++ b/kernel/src/main/java/org/kframework/kompile/Kompile.java @@ -338,9 +338,8 @@ public static Function1 excludeModulesByTag(Set } public static Sentence removePolyKLabels(Sentence s) { - if (s instanceof Production) { - Production p = (Production)s; - if (!p.isSyntacticSubsort() && p.params().nonEmpty()) { + if (s instanceof Production p) { + if (!p.isSyntacticSubsort() && p.params().nonEmpty()) { p = p.substitute(immutable(Collections.nCopies(p.params().size(), Sorts.K()))); return Production(p.klabel().map(KLabel::head), Seq(), p.sort(), p.items(), p.att()); } diff --git a/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java b/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java index af7e7bbaa2c..d68fa14ef4d 100644 --- a/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java +++ b/kernel/src/main/java/org/kframework/kore/convertors/KILtoKORE.java @@ -205,8 +205,7 @@ public Set apply(Syntax s) { } else { List items = new ArrayList<>(); for (org.kframework.kil.ProductionItem it : p.getItems()) { - if (it instanceof NonTerminal) { - NonTerminal nt = (NonTerminal)it; + if (it instanceof NonTerminal nt) { items.add(NonTerminal(nt.getSort(), nt.getName())); } else if (it instanceof UserList) { throw new AssertionError("Lists should have applied before."); diff --git a/kernel/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java b/kernel/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java index 5e97f01e495..971f9415d81 100644 --- a/kernel/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java +++ b/kernel/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java @@ -92,9 +92,8 @@ private Module filter(Module specModule) { } specModule = new ModuleTransformer((m -> { Set filtered = stream(m.localSentences()).flatMap(s -> { - if (s instanceof Claim && s.att().getOptional(Att.LABEL()).isPresent()) { + if (s instanceof Claim c && s.att().getOptional(Att.LABEL()).isPresent()) { String label = s.att().getOptional(Att.LABEL()).get(); - Claim c = (Claim) s; if (proveOptions.trusted != null && proveOptions.trusted.contains(label)) { s = c.newInstance(c.body(), c.requires(), c.ensures(), c.att().add(Att.TRUSTED())); unused.remove(label); diff --git a/kernel/src/main/java/org/kframework/lsp/TextDocumentSyncHandler.java b/kernel/src/main/java/org/kframework/lsp/TextDocumentSyncHandler.java index f79b7318780..07611f3c308 100644 --- a/kernel/src/main/java/org/kframework/lsp/TextDocumentSyncHandler.java +++ b/kernel/src/main/java/org/kframework/lsp/TextDocumentSyncHandler.java @@ -228,13 +228,11 @@ public CompletableFuture, List loc2range(loc))); break; } - } else if (di instanceof Module) { - Module m = (Module) di; + } else if (di instanceof Module m) { for (ModuleItem mi : m.getItems()) { org.kframework.attributes.Location loc = getSafeLoc(mi); if (isPositionOverLocation(pos, loc)) { - if (mi instanceof Import) { // goto module definition - Import imp = (Import) mi; + if (mi instanceof Import imp) { // goto module definition List allDi = slurp(params.getTextDocument().getUri()); allDi.stream().filter(ddi -> ddi instanceof Module) .map(ddi -> ((Module) ddi)) @@ -243,8 +241,7 @@ public CompletableFuture, List loc2range(getSafeLoc(m3)), loc2range(getSafeLoc(m3)), loc2range(getSafeLoc(imp))))); - } else if (mi instanceof StringSentence) { // goto syntax of term inside rule - StringSentence ss = (StringSentence) mi; + } else if (mi instanceof StringSentence ss) { // goto syntax of term inside rule 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()) { @@ -461,22 +458,19 @@ public CompletableFuture> selectionRange(SelectionRangePara KPos pos = new KPos(ppos); for (DefinitionItem di : dis) { if (isPositionOverLocation(pos, getSafeLoc(di))) { - if (di instanceof Module) { - Module m = (Module) di; + if (di instanceof Module m) { SelectionRange msr = new SelectionRange(loc2range(m.getLocation()), topsr); for (ModuleItem mi : m.getItems()) { if (isPositionOverLocation(pos, getSafeLoc(mi))) { SelectionRange sentsr = new SelectionRange(loc2range(getSafeLoc(mi)), msr); - if (mi instanceof org.kframework.kil.Syntax) { - Syntax stx = (org.kframework.kil.Syntax) mi; + if (mi instanceof Syntax stx) { for (PriorityBlock pb : stx.getPriorityBlocks()) { SelectionRange pbsr = new SelectionRange(loc2range(getSafeLoc(pb)), sentsr); for (Production prd : pb.getProductions()) if (isPositionOverLocation(pos, getSafeLoc(prd))) lloc.add(new SelectionRange(loc2range(getSafeLoc(prd)), pbsr)); } - } else if (mi instanceof StringSentence) { // if we have caches, find the deepest term - StringSentence ss = (StringSentence) mi; + } else if (mi instanceof StringSentence ss) { // if we have caches, find the deepest term 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(); AtomicReference x = new AtomicReference<>(sentsr); diff --git a/kernel/src/main/java/org/kframework/main/Main.java b/kernel/src/main/java/org/kframework/main/Main.java index 18708fcfe6c..8f72f092a92 100644 --- a/kernel/src/main/java/org/kframework/main/Main.java +++ b/kernel/src/main/java/org/kframework/main/Main.java @@ -127,10 +127,9 @@ public int runApplication() { return retval; } catch (ProvisionException e) { for (Message m : e.getErrorMessages()) { - if (!(m.getCause() instanceof KEMException)) { + if (!(m.getCause() instanceof KEMException ex)) { throw e; } else { - KEMException ex = (KEMException) m.getCause(); kem.registerThrown(ex); } } diff --git a/kernel/src/main/java/org/kframework/parser/inner/ApplySynonyms.java b/kernel/src/main/java/org/kframework/parser/inner/ApplySynonyms.java index 582b6829072..18211cff8fa 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/ApplySynonyms.java +++ b/kernel/src/main/java/org/kframework/parser/inner/ApplySynonyms.java @@ -20,9 +20,8 @@ public Production apply(Module m, Production p) { Sort returnSort = m.sortSynonymMap().applyOrElse(p.sort(), s -> p.sort()); List pis = new ArrayList<>(); for (ProductionItem pi : iterable(p.items())) { - if (pi instanceof NonTerminal) { - NonTerminal nt = (NonTerminal)pi; - pis.add(NonTerminal(m.sortSynonymMap().applyOrElse(nt.sort(), s -> nt.sort()), nt.name())); + if (pi instanceof NonTerminal nt) { + pis.add(NonTerminal(m.sortSynonymMap().applyOrElse(nt.sort(), s -> nt.sort()), nt.name())); } else { pis.add(pi); } 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 7c4e0303e47..e5704ef566e 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java +++ b/kernel/src/main/java/org/kframework/parser/inner/RuleGrammarGenerator.java @@ -395,8 +395,7 @@ public static Tuple3 getCombinedGrammarImpl(Module mod, if (s instanceof Production && s.att().contains(Att.CELL_COLLECTION())) { return Stream.empty(); } - if (s instanceof Production && (s.att().contains(Att.CELL()))) { - Production p = (Production) s; + if (s instanceof Production p && (s.att().contains(Att.CELL()))) { // assuming that productions tagged with 'cell' start and end with terminals, and only have non-terminals in the middle assert p.items().head() instanceof Terminal || p.items().head() instanceof RegexTerminal; assert p.items().last() instanceof Terminal || p.items().last() instanceof RegexTerminal; @@ -412,8 +411,7 @@ public static Tuple3 getCombinedGrammarImpl(Module mod, Production p2 = Production(Seq(), Sorts.Cell(), Seq(NonTerminal(p.sort()))); return Stream.of(p1, p2); } - if (s instanceof Production && (s.att().contains(Att.CELL_FRAGMENT(), Sort.class))) { - Production p = (Production) s; + if (s instanceof Production p && (s.att().contains(Att.CELL_FRAGMENT(), Sort.class))) { Production p1 = Production(Seq(), Sorts.Cell(), Seq(NonTerminal(p.sort()))); return Stream.of(p, p1); } @@ -442,8 +440,7 @@ public static Tuple3 getCombinedGrammarImpl(Module mod, if (i instanceof Terminal) terminals.put(((Terminal) i).value(), PRESENT); })); parseProds = parseProds.stream().map(s -> { - if (s instanceof Production) { - Production p = (Production) s; + if (s instanceof Production p) { if (p.sort().name().startsWith("#")) return p; // don't do anything for such productions since they are advanced features // rewrite productions to contain follow restrictions for prefix terminals @@ -551,9 +548,8 @@ public static Tuple3 getCombinedGrammarImpl(Module mod, private static void addCellNameProd(Set prods, Sentence prod) { if (prod instanceof Production) { for (ProductionItem pi : iterable(((Production)prod).items())) { - if (pi instanceof Terminal) { - Terminal t = (Terminal)pi; - if (alphaNum.matcher(t.value()).matches()) { + if (pi instanceof Terminal t) { + if (alphaNum.matcher(t.value()).matches()) { prods.add(Production(Seq(), Sorts.CellName(), Seq(t), Att().add(Att.TOKEN()))); } } diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AddEmptyLists.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AddEmptyLists.java index b3dd9f1faad..f03c0439400 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AddEmptyLists.java +++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AddEmptyLists.java @@ -222,8 +222,7 @@ private Optional greatest(Iterable sorts) { } private Optional klabelFromTerm(Term labelTerm) { - if (labelTerm instanceof Constant) { - Constant labelCon = (Constant) labelTerm; + if (labelTerm instanceof Constant labelCon) { if (labelCon.production().sort().equals(Sorts.KLabel())) { String labelVal = labelCon.value(); if (labelVal.charAt(0) == '`') { @@ -243,8 +242,7 @@ private List lowerKList(Term listTerm) { } private void lowerKListAcc(Term term, List items) { - if (term instanceof TermCons) { - TermCons cons = (TermCons) term; + if (term instanceof TermCons cons) { if (cons.production().klabel().isDefined()) { String labelName = cons.production().klabel().get().name(); if (labelName.equals("#KList")) { diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AmbFilter.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AmbFilter.java index 52f4e49b8eb..a934b9bca59 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AmbFilter.java +++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AmbFilter.java @@ -52,8 +52,7 @@ public Tuple2, Term>, Set> apply(Ambiguit for (int i = 0; i < amb.items().size(); i++) { msg += "\n" + (i + 1) + ": "; Term elem = (Term) amb.items().toArray()[i]; - if (elem instanceof ProductionReference) { - ProductionReference tc = (ProductionReference) elem; + if (elem instanceof ProductionReference tc) { msg += tc.production().toString(); } // TODO: use the unparser diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AmbFilterError.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AmbFilterError.java index 2d411bff580..2d09a1612c3 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AmbFilterError.java +++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/AmbFilterError.java @@ -55,8 +55,7 @@ public Either, Term> apply(Ambiguity amb) { for (int i = 0; i < amb.items().size(); i++) { msg += "\n" + (i + 1) + ": "; Term elem = (Term) amb.items().toArray()[i]; - if (elem instanceof ProductionReference) { - ProductionReference tc = (ProductionReference) elem; + if (elem instanceof ProductionReference tc) { msg += tc.production().toString(); } // TODO: use the unparser diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/KAppToTermConsVisitor.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/KAppToTermConsVisitor.java index 4669a3228ff..fc09bb686f9 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/KAppToTermConsVisitor.java +++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/KAppToTermConsVisitor.java @@ -50,10 +50,9 @@ public KAppToTermConsVisitor(Module mod) { public Either, Term> apply(TermCons tc) { assert tc.production() != null : this.getClass() + ":" + " production not found." + tc; if (tc.production().klabel().isDefined() && tc.production().klabel().get().equals(KLabels.KAPP)) { - if (!(tc.get(0) instanceof Constant) || !((Constant) tc.get(0)).production().sort().equals(Sorts.KLabel())) + if (!(tc.get(0) instanceof Constant kl) || !((Constant) tc.get(0)).production().sort().equals(Sorts.KLabel())) // TODO: remove check once the java backend is no longer supported. return super.apply(tc); // don't do anything if the label is not a token KLabel (in case of variable or casted variable) - Constant kl = (Constant) tc.get(0); String klvalue = kl.value(); try { klvalue = StringUtil.unescapeKoreKLabel(kl.value()); } catch (IllegalArgumentException e) { /* ignore */ } // if possible, unescape Set prods = mutable(mod.productionsFor().get(KLabel(klvalue)) @@ -85,8 +84,7 @@ private static PStack flattenKList(Term t) { assert false : KAppToTermConsVisitor.class + " expected all ambiguities to already be pushed to the top:\n" + " Source: " + ((Ambiguity) t).items().iterator().next().source().orElse(null) + "\n" + " Location: " + ((Ambiguity) t).items().iterator().next().location().orElse(null); - } else if (t instanceof TermCons) { - TermCons tc = (TermCons) t; + } else if (t instanceof TermCons tc) { if (tc.production().klabel().isDefined() && tc.production().klabel().get().equals(KLabels.KLIST)) return flattenKList(tc.get(0)).plusAll(Lists.reverse(Lists.newArrayList(flattenKList(tc.get(1))))); else if (tc.production().klabel().isDefined() && tc.production().klabel().get().equals(KLabels.EMPTYKLIST)) diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/PushAmbiguitiesDownAndPreferAvoid.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/PushAmbiguitiesDownAndPreferAvoid.java index 33824b9f0fe..9782997580e 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/PushAmbiguitiesDownAndPreferAvoid.java +++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/PushAmbiguitiesDownAndPreferAvoid.java @@ -84,10 +84,9 @@ public Term apply(Ambiguity a) { a = (Ambiguity)super.apply(a); for (Term t : a.items()) { - if (!(t instanceof ProductionReference)) { + if (!(t instanceof ProductionReference ref)) { return a; } - ProductionReference ref = (ProductionReference)t; if (prod == null) { prod = ref.production(); if (ref instanceof TermCons) { diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/PushTopAmbiguityUp.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/PushTopAmbiguityUp.java index 139fbd0de89..c75479b4690 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/PushTopAmbiguityUp.java +++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/PushTopAmbiguityUp.java @@ -16,8 +16,7 @@ public class PushTopAmbiguityUp extends SafeTransformer { public Term apply(TermCons tc) { if (tc.production().sort().equals(Sorts.RuleContent())) { Term t = new PushTopAmbiguityUp2().apply(tc.get(0)); - if (t instanceof Ambiguity) { - Ambiguity old = (Ambiguity)t; + if (t instanceof Ambiguity old) { Set newTerms = new HashSet<>(); for (Term child : old.items()) { Term newTerm = tc.with(0, child); @@ -34,8 +33,7 @@ private class PushTopAmbiguityUp2 extends SafeTransformer { public Term apply(TermCons tc) { if (tc.production().klabel().isDefined() && tc.production().klabel().get().head().equals(KLabels.KREWRITE)) { Term t = tc.get(0); - if (t instanceof Ambiguity) { - Ambiguity old = (Ambiguity)t; + if (t instanceof Ambiguity old) { Set newTerms = new HashSet<>(); for (Term child : old.items()) { Term newTerm = tc.with(0, child); 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 239898a8382..7898b3cc6b6 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 @@ -22,8 +22,7 @@ public RemoveOverloads(POSet overloads) { public Term apply(Ambiguity a) { Set productions = new HashSet<>(); for (Term t : a.items()) { - if (t instanceof TermCons) { - TermCons tc = (TermCons)t; + if (t instanceof TermCons tc) { productions.add(tc.production()); } else { return a; diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TreeCleanerVisitor.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TreeCleanerVisitor.java index 17d97f272a6..040260b987c 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TreeCleanerVisitor.java +++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TreeCleanerVisitor.java @@ -13,8 +13,7 @@ public class TreeCleanerVisitor extends SafeTransformer { @Override public Term apply(Ambiguity amb) { Term newTerm = super.apply(amb); - if (newTerm instanceof Ambiguity) { - Ambiguity newAmb = (Ambiguity)newTerm; + if (newTerm instanceof Ambiguity newAmb) { if (newAmb.items().size() == 1) { return newAmb.items().iterator().next(); } diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java index bb8dc27508d..6af78b0bef0 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java +++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferenceVisitor.java @@ -208,8 +208,7 @@ private Either, Term> typeError(ProductionReference pr, Sort e @Override public Either, Term> apply(Term term) { - if (term instanceof Ambiguity) { - Ambiguity amb = (Ambiguity)term; + if (term instanceof Ambiguity amb) { return super.apply(amb); } ProductionReference pr = (ProductionReference)term; @@ -233,8 +232,7 @@ public Either, Term> apply(Term term) { return typeError(pr, expectedSort, actualSort); } // check types of children - if (pr instanceof TermCons) { - TermCons tc = (TermCons)pr; + if (pr instanceof TermCons tc) { for (int i = 0, j = 0; i < substituted.items().size(); i++) { if (substituted.items().apply(i) instanceof NonTerminal) { // save prior value of variables diff --git a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java index 362fc8429ee..e9325d9c7f3 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java +++ b/kernel/src/main/java/org/kframework/parser/inner/disambiguation/TypeInferencer.java @@ -354,10 +354,9 @@ public void push(Term t, Sort topSort, boolean isAnywhere) { * @return */ private static Optional getFunction(Term t) { - if (!(t instanceof ProductionReference)) { + if (!(t instanceof ProductionReference child)) { return Optional.empty(); } - ProductionReference child = (ProductionReference)t; while (child.production().att().contains(Att.BRACKET())) { if (((TermCons)child).get(0) instanceof Ambiguity) { return Optional.empty(); @@ -514,8 +513,7 @@ public class ExpectedSortsVisitor { * this term. */ public String apply(Term t) { - if (t instanceof Ambiguity) { - Ambiguity amb = (Ambiguity)t; + if (t instanceof Ambiguity amb) { if (isIncremental) { // we are error checking an ill typed term, so we pick just one branch of the ambiguity and explain why it is // ill typed. @@ -567,15 +565,13 @@ public String apply(Term t) { // get cached id id = pr.id().get(); } - if (pr instanceof TermCons) { + if (pr instanceof TermCons tc) { boolean wasStrict = isStrictEquality; Sort oldExpectedSort = expectedSort; Optional oldExpectedParams = expectedParams; - TermCons tc = (TermCons)pr; // traverse children for (int i = 0, j = 0; i < tc.production().items().size(); i++) { - if (tc.production().items().apply(i) instanceof NonTerminal) { - NonTerminal nt = (NonTerminal)tc.production().items().apply(i); + if (tc.production().items().apply(i) instanceof NonTerminal nt) { expectedParams = Optional.of(tc); isStrictEquality = false; // compute expected sort and whether this is a cast @@ -586,8 +582,7 @@ public String apply(Term t) { expectedSort = getSortOfCast(tc); isStrictEquality = tc.production().klabel().get().name().equals("#SyntacticCast") || tc.production().klabel().get().name().equals("#InnerCast"); - if (tc.get(0) instanceof Constant) { - Constant child = (Constant)tc.get(0); + if (tc.get(0) instanceof Constant child) { if (child.production().sort().equals(Sorts.KVariable()) || child.production().sort().equals(Sorts.KConfigVar())) { isStrictEquality = true; } @@ -619,8 +614,7 @@ public String apply(Term t) { if (isIncremental || !shared || !cached) { // if we are in incremental mode or this is the first time reaching this term under this expected sort, // compute the local constraints of this term and add them to the current constraint. - if (pr instanceof Constant && (pr.production().sort().equals(Sorts.KVariable()) || pr.production().sort().equals(Sorts.KConfigVar()))) { - Constant c = (Constant) pr; + if (pr instanceof Constant c && (pr.production().sort().equals(Sorts.KVariable()) || pr.production().sort().equals(Sorts.KConfigVar()))) { String name; boolean oldStrictEquality = isStrictEquality; if (!shared) { 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 8ea406e5ee5..8b24d81d73d 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 @@ -658,8 +658,7 @@ private List getProductions(Module m, Scanner scanner, Sort st } List items = new ArrayList<>(prod.items().size()); for (ProductionItem item : iterable(prod.items())) { - if (item instanceof Terminal) { - Terminal t = (Terminal) item; + if (item instanceof Terminal t) { if (t.value().isEmpty()) { continue; } diff --git a/kernel/src/main/java/org/kframework/parser/inner/kernel/KSyntax2Bison.java b/kernel/src/main/java/org/kframework/parser/inner/kernel/KSyntax2Bison.java index a1690ef0b85..c341eedb048 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/kernel/KSyntax2Bison.java +++ b/kernel/src/main/java/org/kframework/parser/inner/kernel/KSyntax2Bison.java @@ -79,8 +79,7 @@ public static Module transformByPriorityAndAssociativity(Module module) { Set sentences = new HashSet<>(); Set>> nts = new HashSet<>(); for (Sentence s : iterable(module.sentences())) { - if (s instanceof Production) { - Production prod = (Production)s; + if (s instanceof Production prod) { if (prod.klabel().isDefined() && prod.params().isEmpty()) { List items = new ArrayList<>(mutable(prod.items())); if (items.get(0) instanceof NonTerminal) { @@ -332,8 +331,7 @@ private static void processProduction(Production prod, Module module, Module dis int i = 1; List nts = new ArrayList<>(); for (ProductionItem item : iterable(prod.items())) { - if (item instanceof NonTerminal) { - NonTerminal nt = (NonTerminal)item; + if (item instanceof NonTerminal nt) { encode(nt.sort(), bison); bison.append(" "); nts.add(i); diff --git a/kernel/src/main/java/org/kframework/parser/inner/kernel/Scanner.java b/kernel/src/main/java/org/kframework/parser/inner/kernel/Scanner.java index b71d0c44c16..5ff062ab00f 100644 --- a/kernel/src/main/java/org/kframework/parser/inner/kernel/Scanner.java +++ b/kernel/src/main/java/org/kframework/parser/inner/kernel/Scanner.java @@ -59,8 +59,7 @@ public static Map> getTokens(Module modul Set terminals = new HashSet<>(); for (Production p : iterable(module.productions())) { for (ProductionItem pi : iterable(p.items())) { - if (pi instanceof TerminalLike) { - TerminalLike lx = (TerminalLike) pi; + if (pi instanceof TerminalLike lx) { if (tokens.containsKey(lx)) { int prec; if (p.att().contains(Att.PREC())) { @@ -151,8 +150,7 @@ public void appendScanner(StringBuilder flex, BiConsumer ordered = tokens.keySet().stream().sorted((t1, t2) -> tokens.get(t2)._2() - tokens.get(t1)._2()).collect(Collectors.toList()); for (TerminalLike key : ordered) { - if (key instanceof Terminal) { - Terminal t = (Terminal) key; + if (key instanceof Terminal t) { flex.append(StringUtil.enquoteCString(t.value())); } else { RegexTerminal t = (RegexTerminal) key; @@ -191,11 +189,10 @@ public void writeStandaloneScanner(File path) { flex.append("%%\n\n"); if (module.productionsForSort().contains(Sorts.LineMarker().head())) { stream(module.productionsForSort().apply(Sorts.LineMarker().head())).forEach(prod -> { - if (prod.items().size() != 1 || !(prod.items().apply(0) instanceof RegexTerminal)) { + if (prod.items().size() != 1 || !(prod.items().apply(0) instanceof RegexTerminal terminal)) { throw KEMException.compilerError("Productions of sort `#LineMarker` must be exactly one `RegexTerminal`.", prod); } - RegexTerminal terminal = (RegexTerminal)prod.items().apply(0); - String regex = terminal.regex(); + String regex = terminal.regex(); flex.append(regex).append(" line_marker(yytext, yyscanner);\n"); }); } diff --git a/kernel/src/main/java/org/kframework/unparser/Formatter.java b/kernel/src/main/java/org/kframework/unparser/Formatter.java index 38a497d2b50..8b65a020851 100644 --- a/kernel/src/main/java/org/kframework/unparser/Formatter.java +++ b/kernel/src/main/java/org/kframework/unparser/Formatter.java @@ -33,13 +33,11 @@ public static String format(Term term, ColorSetting colorize) { public static void format(Term term, Indenter indenter, ColorSetting colorize) { int indent = 0; int localColor = 0; - if (term instanceof Constant) { - Constant c = (Constant) term; + if (term instanceof Constant c) { color(indenter, c.production(), 0, colorize); indenter.append(c.value()); resetColor(indenter, c.production(), colorize); - } else if (term instanceof TermCons) { - TermCons tc = (TermCons) term; + } else if (term instanceof TermCons tc) { String format = tc.production().att().getOptional(Att.FORMAT()).orElse(defaultFormat(tc.production().items().size())); for (int i = 0; i < format.length(); i++) { char c = format.charAt(i); @@ -84,8 +82,7 @@ public static void format(Term term, Indenter indenter, ColorSetting colorize) { assert tc.production().nonterminal(nt) == item; Term inner = tc.get(nt); boolean assoc = false; - if (inner instanceof TermCons) { - TermCons innerTc = (TermCons) inner; + if (inner instanceof TermCons innerTc) { Production origProd = tc.production().att().getOptional(Att.ORIGINAL_PRD(), Production.class).orElse(tc.production()); Production innerOrigProd = innerTc.production().att().getOptional(Att.ORIGINAL_PRD(), Production.class).orElse(innerTc.production()); if (innerOrigProd.equals(origProd) && origProd.att().contains(Att.ASSOC())) { diff --git a/kernel/src/main/java/org/kframework/unparser/KPrint.java b/kernel/src/main/java/org/kframework/unparser/KPrint.java index 62303a0daa1..098369d9c59 100644 --- a/kernel/src/main/java/org/kframework/unparser/KPrint.java +++ b/kernel/src/main/java/org/kframework/unparser/KPrint.java @@ -221,11 +221,10 @@ public void apply(KVariable var) { } private K filterSubst(K term, Module mod) { - if (!(term instanceof KApply)) { + if (!(term instanceof KApply kapp)) { return term; } - KApply kapp = (KApply)term; - if (kapp.klabel().head().equals(KLabels.ML_AND)) { + if (kapp.klabel().head().equals(KLabels.ML_AND)) { return filterConjunction(kapp, mod); } else if (kapp.klabel().head().equals(KLabels.ML_OR)) { KLabel unit = KLabel(KLabels.ML_FALSE.name(), kapp.klabel().params().apply(0)); @@ -244,11 +243,10 @@ private K filterSubst(K term, Module mod) { } private K filterConjunction(K term, Module mod) { - if (!(term instanceof KApply)) { + if (!(term instanceof KApply kapp)) { return term; } - KApply kapp = (KApply)term; - if (kapp.klabel().head().equals(KLabels.ML_AND)) { + if (kapp.klabel().head().equals(KLabels.ML_AND)) { KLabel unit = KLabel(KLabels.ML_TRUE.name(), kapp.klabel().params().apply(0)); List conjuncts = Assoc.flatten(kapp.klabel(), kapp.items(), unit); return conjuncts.stream() @@ -266,11 +264,10 @@ private K filterConjunction(K term, Module mod) { } public Optional filterEquality(K term, Multiset vars, Module mod) { - if (!(term instanceof KApply)) { + if (!(term instanceof KApply kapp)) { return Optional.of(term); } - KApply kapp = (KApply)term; - if (kapp.klabel().head().equals(KLabels.ML_EQUALS)) { + if (kapp.klabel().head().equals(KLabels.ML_EQUALS)) { if (!(kapp.items().get(0) instanceof KVariable) && (!(kapp.items().get(0) instanceof KApply) || !mod.attributesFor().apply(((KApply)kapp.items().get(0)).klabel()).contains(Att.FUNCTION()))) { @@ -391,10 +388,9 @@ private K flattenTerms(Module mod, K input) { @Override public K apply(KApply orig) { K newK = super.apply(orig); - if (! (newK instanceof KApply)) { + if (! (newK instanceof KApply kapp)) { return newK; } - KApply kapp = (KApply) newK; String name = orig.klabel().name(); return options.flattenedKLabels.contains(name) ? flattenTerm(mod, kapp) : kapp ; diff --git a/kernel/src/main/java/org/kframework/unparser/ToBinary.java b/kernel/src/main/java/org/kframework/unparser/ToBinary.java index 40a17971209..7682b23b0cf 100644 --- a/kernel/src/main/java/org/kframework/unparser/ToBinary.java +++ b/kernel/src/main/java/org/kframework/unparser/ToBinary.java @@ -64,16 +64,14 @@ private void traverse(K k) throws IOException { add_intern(k); return; } - if (k instanceof KToken) { - KToken tok = (KToken) k; + if (k instanceof KToken tok) { data.writeByte(BinaryParser.KTOKEN); add_intern(k); writeString(tok.s()); writeString(tok.sort().toString()); - } else if (k instanceof KApply) { - KApply app = (KApply) k; + } else if (k instanceof KApply app) { for (K item : app.asIterable()) { traverse(item); @@ -84,8 +82,7 @@ private void traverse(K k) throws IOException { data.writeBoolean(app.klabel() instanceof KVariable); data.writeInt(app.size()); - } else if (k instanceof KSequence) { - KSequence seq = (KSequence) k; + } else if (k instanceof KSequence seq) { for (K item : seq.asIterable()) { traverse(item); @@ -94,23 +91,20 @@ private void traverse(K k) throws IOException { add_intern(k); data.writeInt(seq.size()); - } else if (k instanceof KVariable) { - KVariable var = (KVariable) k; + } else if (k instanceof KVariable var) { data.writeByte(BinaryParser.KVARIABLE); add_intern(k); writeString(var.name()); - } else if (k instanceof KRewrite) { - KRewrite rew = (KRewrite) k; + } else if (k instanceof KRewrite rew) { traverse(rew.left()); traverse(rew.right()); data.writeByte(BinaryParser.KREWRITE); add_intern(k); - } else if (k instanceof InjectedKLabel) { - InjectedKLabel inj = (InjectedKLabel) k; + } else if (k instanceof InjectedKLabel inj) { data.writeByte(BinaryParser.INJECTEDKLABEL); add_intern(k); diff --git a/kernel/src/main/java/org/kframework/unparser/ToJson.java b/kernel/src/main/java/org/kframework/unparser/ToJson.java index d60ee110f37..86fa96bd331 100644 --- a/kernel/src/main/java/org/kframework/unparser/ToJson.java +++ b/kernel/src/main/java/org/kframework/unparser/ToJson.java @@ -369,21 +369,18 @@ public static JsonStructure toJson(Production pro) { public static JsonObject toJson(ProductionItem prod) { JsonObjectBuilder jsonProduction = factory.createObjectBuilder(); - if (prod instanceof NonTerminal) { - NonTerminal t = (NonTerminal) prod; + if (prod instanceof NonTerminal t) { jsonProduction.add("node", JsonParser.KNONTERMINAL); jsonProduction.add("sort", toJson(t.sort())); Option name = t.name(); if (! name.isEmpty()) jsonProduction.add("name", name.get()); - } else if (prod instanceof RegexTerminal) { - RegexTerminal t = (RegexTerminal) prod; + } else if (prod instanceof RegexTerminal t) { jsonProduction.add("node", JsonParser.KREGEXTERMINAL); jsonProduction.add("precedeRegex", t.precedeRegex()); jsonProduction.add("regex", t.regex()); jsonProduction.add("followRegex", t.followRegex()); - } else if (prod instanceof Terminal) { - Terminal t = (Terminal) prod; + } else if (prod instanceof Terminal t) { jsonProduction.add("node", JsonParser.KTERMINAL); jsonProduction.add("value", t.value()); } @@ -431,15 +428,13 @@ public static byte[] apply(K k) { public static JsonStructure toJson(K k) { JsonObjectBuilder knode = factory.createObjectBuilder(); - if (k instanceof KToken) { - KToken tok = (KToken) k; + if (k instanceof KToken tok) { knode.add("node", JsonParser.KTOKEN); knode.add("sort", toJson(tok.sort())); knode.add("token", tok.s()); - } else if (k instanceof KApply) { - KApply app = (KApply) k; + } else if (k instanceof KApply app) { knode.add("node", JsonParser.KAPPLY); knode.add("label", toJson(((KApply) k).klabel())); @@ -452,8 +447,7 @@ public static JsonStructure toJson(K k) { knode.add("arity", app.klist().size()); knode.add("args", args.build()); - } else if (k instanceof KSequence) { - KSequence seq = (KSequence) k; + } else if (k instanceof KSequence seq) { knode.add("node", JsonParser.KSEQUENCE); @@ -465,8 +459,7 @@ public static JsonStructure toJson(K k) { knode.add("arity", seq.size()); knode.add("items", items.build()); - } else if (k instanceof KVariable) { - KVariable var = (KVariable) k; + } else if (k instanceof KVariable var) { knode.add("node", JsonParser.KVARIABLE); knode.add("name", var.name()); @@ -474,22 +467,19 @@ public static JsonStructure toJson(K k) { knode.add("sort", toJson(k.att().get(Sort.class))); } - } else if (k instanceof KRewrite) { - KRewrite rew = (KRewrite) k; + } else if (k instanceof KRewrite rew) { knode.add("node", JsonParser.KREWRITE); knode.add("lhs", toJson(rew.left())); knode.add("rhs", toJson(rew.right())); - } else if (k instanceof KAs) { - KAs alias = (KAs) k; + } else if (k instanceof KAs alias) { knode.add("node", JsonParser.KAS); knode.add("pattern", toJson(alias.pattern())); knode.add("alias", toJson(alias.alias())); - } else if (k instanceof InjectedKLabel) { - InjectedKLabel inj = (InjectedKLabel) k; + } else if (k instanceof InjectedKLabel inj) { knode.add("node", JsonParser.INJECTEDKLABEL); knode.add("label", toJson(inj.klabel())); diff --git a/kernel/src/main/java/org/kframework/unparser/ToLatex.java b/kernel/src/main/java/org/kframework/unparser/ToLatex.java index d02b77a38ef..67436d15531 100644 --- a/kernel/src/main/java/org/kframework/unparser/ToLatex.java +++ b/kernel/src/main/java/org/kframework/unparser/ToLatex.java @@ -71,13 +71,11 @@ public static void apply(DataOutputStream out, Att att) throws IOException { } public static void apply(DataOutputStream out, K k) throws IOException { - if (k instanceof KToken) { - KToken tok = (KToken) k; + if (k instanceof KToken tok) { writeString(out, ("\\texttt{ " + tok.s() + " }")); - } else if (k instanceof KApply) { - KApply app = (KApply) k; + } else if (k instanceof KApply app) { writeString(out, ("\\" + latexedKLabel(app.klabel().name()))); @@ -87,8 +85,7 @@ public static void apply(DataOutputStream out, K k) throws IOException { writeString(out, "}"); } - } else if (k instanceof KSequence) { - KSequence kseq = (KSequence) k; + } else if (k instanceof KSequence kseq) { writeString(out, "\\kseq{"); @@ -99,8 +96,7 @@ public static void apply(DataOutputStream out, K k) throws IOException { writeString(out, "}{\\dotk{}}"); - } else if (k instanceof KVariable) { - KVariable var = (KVariable) k; + } else if (k instanceof KVariable var) { Optional origName = var.att().getOptional(Att.ORIGINAL_NAME()); if (origName.isPresent()) { @@ -109,8 +105,7 @@ public static void apply(DataOutputStream out, K k) throws IOException { writeString(out, var.name()); } - } else if (k instanceof KRewrite) { - KRewrite rew = (KRewrite) k; + } else if (k instanceof KRewrite rew) { writeString(out, "\\krewrites{"); apply(out, rew.left()); @@ -120,8 +115,7 @@ public static void apply(DataOutputStream out, K k) throws IOException { apply(out, rew.att()); writeString(out, "}"); - } else if (k instanceof KAs) { - KAs alias = (KAs) k; + } else if (k instanceof KAs alias) { writeString(out, "\\kas{"); apply(out, alias.pattern()); @@ -131,8 +125,7 @@ public static void apply(DataOutputStream out, K k) throws IOException { apply(out, alias.att()); writeString(out, "}"); - } else if (k instanceof InjectedKLabel) { - InjectedKLabel inj = (InjectedKLabel) k; + } else if (k instanceof InjectedKLabel inj) { writeString(out, "\\injectedklabel{"); writeString(out, inj.klabel().name()); diff --git a/kernel/src/main/java/org/kframework/utils/inject/Annotations.java b/kernel/src/main/java/org/kframework/utils/inject/Annotations.java index bb755221471..585dfa0012b 100644 --- a/kernel/src/main/java/org/kframework/utils/inject/Annotations.java +++ b/kernel/src/main/java/org/kframework/utils/inject/Annotations.java @@ -24,10 +24,9 @@ public int hashCode() { } public boolean equals(Object o) { - if (!(o instanceof Main)) { + if (!(o instanceof Main other)) { return false; } - Main other = (Main) o; return annotation.equals(other.value()); } @@ -53,10 +52,9 @@ public int hashCode() { } public boolean equals(Object o) { - if (!(o instanceof Spec1)) { + if (!(o instanceof Spec1 other)) { return false; } - Spec1 other = (Spec1) o; return annotation.equals(other.value()); } @@ -82,10 +80,9 @@ public int hashCode() { } public boolean equals(Object o) { - if (!(o instanceof Spec2)) { + if (!(o instanceof Spec2 other)) { return false; } - Spec2 other = (Spec2) o; return annotation.equals(other.value()); } diff --git a/kore/src/main/java/org/kframework/kore/AttCompare.java b/kore/src/main/java/org/kframework/kore/AttCompare.java index 5690202cf77..425b3c66b30 100644 --- a/kore/src/main/java/org/kframework/kore/AttCompare.java +++ b/kore/src/main/java/org/kframework/kore/AttCompare.java @@ -39,15 +39,11 @@ private boolean attEquals(K thisK, K thatK) { || (thisK instanceof KVariable && thatK instanceof KVariable) || (thisK instanceof InjectedKLabel && thatK instanceof InjectedKLabel)) { return thisK.equals(thatK); - } else if (thisK instanceof KApply && thatK instanceof KApply) { - KApply thisKItem = (KApply) thisK; - KApply thatKItem = (KApply) thatK; + } else if (thisK instanceof KApply thisKItem && thatK instanceof KApply thatKItem) { return thisKItem.klabel().equals(thatKItem.klabel()) && attEquals(thisKItem.klist().items(), thatKItem.klist().items()); } else if (thisK instanceof KSequence && thatK instanceof KSequence) { return attEquals(((KSequence) thisK).items(), ((KSequence) thatK).items()); - } else if (thisK instanceof KRewrite && thatK instanceof KRewrite) { - KRewrite thisKR = (KRewrite) thisK; - KRewrite thatKR = (KRewrite) thatK; + } else if (thisK instanceof KRewrite thisKR && thatK instanceof KRewrite thatKR) { return attEquals(thisKR.left(), thatKR.left()) && attEquals(thisKR.right(), thatKR.right()); } else { return false;