Skip to content

Commit

Permalink
Don't do concretization if no cells specified
Browse files Browse the repository at this point in the history
  • Loading branch information
radumereuta committed Nov 14, 2023
1 parent 2eeccd5 commit d3f7614
Show file tree
Hide file tree
Showing 2 changed files with 23 additions and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -66,7 +66,7 @@ private boolean skipSentence(Sentence s) {
// cell mentioned is the automatically-added <generatedCounter> cell.
private boolean shouldConsider(List<K> items, boolean isClaim) {
if (items.size() == 1) {
return true;
return !isClaim;
} else if (items.size() == 2 && isClaim) {
K second = items.get(1);
if (second instanceof KApply app) {
Expand Down
22 changes: 22 additions & 0 deletions kernel/src/main/java/org/kframework/compile/ConcretizeCells.java
Original file line number Diff line number Diff line change
@@ -1,8 +1,13 @@
// Copyright (c) K Team. All Rights Reserved.
package org.kframework.compile;

import org.kframework.attributes.Att;
import org.kframework.definition.*;
import org.kframework.definition.Module;
import org.kframework.kore.K;
import org.kframework.kore.KRewrite;

import java.util.stream.Stream;

/**
* Apply the configuration concretization process. The implicit {@code <k>} cell is added by another
Expand Down Expand Up @@ -60,6 +65,7 @@ public ConcretizeCells(
}

public Sentence concretize(Module m, Sentence s) {
if (s instanceof Claim c && !hasCells(c.body())) return s;
s = addRootCell.addImplicitCells(s, m);
s = addParentCells.concretize(s);
s = closeCells.close(s);
Expand All @@ -69,4 +75,20 @@ public Sentence concretize(Module m, Sentence s) {
s = sortCells.postprocess(s);
return s;
}

private static boolean hasCells(K item) {
if (IncompleteCellUtils.flattenCells(item).stream()
.anyMatch(k -> k.att().get(Production.class).att().contains(Att.CELL()))) {
return true;
}

if (item instanceof final KRewrite rew) {
return Stream.concat(
IncompleteCellUtils.flattenCells(rew.left()).stream(),
IncompleteCellUtils.flattenCells(rew.right()).stream())
.anyMatch(ConcretizeCells::hasCells);
}

return false;
}
}

0 comments on commit d3f7614

Please sign in to comment.