Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Apply Java migration: pattern variables #3750

Merged
merged 1 commit into from
Oct 24, 2023
Merged

Apply Java migration: pattern variables #3750

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 1 addition & 2 deletions kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading