Skip to content

Commit

Permalink
Apply Java migration: pattern variables (#3750)
Browse files Browse the repository at this point in the history 
This is a fully-mechanical PR that uses IntelliJ to migrate to using the
new Java feature for pattern variables in `instanceof` checks. For
example, this code:
```java
            if (left instanceof KApply) {
                KApply kapp = (KApply) left;
                Production prod = production(kapp);
```
becomes:
```java
            if (left instanceof KApply kapp) {
                Production prod = production(kapp);
```
which saves a lot of boilerplate code.

There are **no manual changes or decisions** in this PR; it's
push-button only.
  • Loading branch information
@Baltoli
Baltoli authored Oct 24, 2023
1 parent 18c190f commit 227b989
Show file tree
Hide file tree
Showing 66 changed files with 182 additions and 358 deletions.
3 changes: 1 addition & 2 deletions kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -201,8 +201,7 @@ public void convert(boolean heatCoolEq, String prelude, StringBuilder semantics,
SetMultimap<KLabel, Rule> 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);
Expand Down
3 changes: 1 addition & 2 deletions kernel/src/main/java/org/kframework/compile/AddCoolLikeAtt.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down
12 changes: 4 additions & 8 deletions kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -74,8 +72,7 @@ private boolean shouldConsider(List<K> items, boolean isClaim) {
return true;
} else if (items.size() == 2 && isClaim) {
K second = items.get(1);
if(second instanceof KApply) {
KApply app = (KApply) second;
if(second instanceof KApply app) {
return app.klabel() == KLabels.GENERATED_COUNTER_CELL;
}
}
Expand All @@ -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())
Expand Down
3 changes: 1 addition & 2 deletions kernel/src/main/java/org/kframework/compile/AddImplicitCounterCell.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
21 changes: 7 additions & 14 deletions kernel/src/main/java/org/kframework/compile/AddParentCells.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -181,8 +181,7 @@ Optional<Integer> getLevel(K k) {
}
}
return Optional.empty();
} else if (k instanceof KRewrite) {
KRewrite rew = (KRewrite) k;
} else if (k instanceof KRewrite rew) {
List<K> cells = IncompleteCellUtils.flattenCells(rew.left());
cells.addAll(IncompleteCellUtils.flattenCells(rew.right()));
Optional<Integer> level = Optional.empty();
Expand All @@ -205,8 +204,7 @@ Optional<Integer> getLevel(K k) {
}

Optional<KLabel> 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<K> items = app.klist().items();
if (items.isEmpty()) {
Expand Down Expand Up @@ -246,10 +244,9 @@ Optional<KLabel> 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;
Expand Down Expand Up @@ -291,17 +288,15 @@ 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())) {
return concretizeCell(newTerm);
} 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()
Expand All @@ -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;
Expand Down
21 changes: 7 additions & 14 deletions kernel/src/main/java/org/kframework/compile/AddSortInjections.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand All @@ -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;
Expand All @@ -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<K> children = new ArrayList<>();
for (int i = 0; i < kseq.size(); i++) {
K child = kseq.items().get(i);
Expand All @@ -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);
Expand Down Expand Up @@ -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);
}
Expand Down Expand Up @@ -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);
Expand All @@ -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);
Expand Down
3 changes: 1 addition & 2 deletions kernel/src/main/java/org/kframework/compile/AddTopCellToRules.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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());
Expand Down
3 changes: 1 addition & 2 deletions kernel/src/main/java/org/kframework/compile/CloseCells.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Expand Down
3 changes: 1 addition & 2 deletions kernel/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,8 +31,7 @@ public ComputeTransitiveFunctionDependencies(Module module) {
Set<KLabel> 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);
Expand Down
3 changes: 1 addition & 2 deletions kernel/src/main/java/org/kframework/compile/ConstantFolding.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
9 changes: 3 additions & 6 deletions kernel/src/main/java/org/kframework/compile/ConvertDataStructureToLookup.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -354,8 +354,7 @@ private K convertList(KApply k, KLabel collectionLabel, List<K> 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)))) {
Expand Down Expand Up @@ -444,10 +443,9 @@ private K convertMap(KApply k, KLabel collectionLabel, List<K> 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) {
Expand Down Expand Up @@ -520,8 +518,7 @@ private K convertSet(KApply k, KLabel collectionLabel, List<K> 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)
Expand Down
11 changes: 4 additions & 7 deletions kernel/src/main/java/org/kframework/compile/ExpandMacros.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -315,9 +315,8 @@ private Set<Sort> 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<Production> prods = new HashSet<>(mutable(mod.productionsFor().apply(kapp.klabel())));
Expand Down Expand Up @@ -364,10 +363,8 @@ private boolean match(Map<KVariable, K> 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())) {
Expand Down
24 changes: 8 additions & 16 deletions kernel/src/main/java/org/kframework/compile/GenerateSentencesFromConfigDecl.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -79,16 +79,14 @@ public static Set<Sentence> 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<Set<Sentence>, List<Sort>, 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);
Expand All @@ -115,8 +113,7 @@ private static Tuple4<Set<Sentence>, List<Sort>, 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));
Expand Down Expand Up @@ -166,10 +163,9 @@ private static Tuple4<Set<Sentence>, List<Sort>, K, Boolean> genInternal(K term,
Sort sort = kapp.att().get(Production.class).sort();
Tuple2<K, Set<Sentence>> 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<K, Set<Sentence>> 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) {
Expand Down Expand Up @@ -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));
Expand Down Expand Up @@ -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")) {
Expand All @@ -598,12 +592,10 @@ private static Att getCellPropertiesAsAtt(K k) {
}

private static Tuple2<Att.Key, String> 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(() ->
Expand Down
3 changes: 1 addition & 2 deletions kernel/src/main/java/org/kframework/compile/MarkExtraConcreteRules.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,7 @@ public static Definition mark(Definition def, @Nullable List<String> extraConcre
}
HashSet<String> 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
Expand Down
Loading

0 comments on commit 227b989

Please sign in to comment.