Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/develop'
Browse files Browse the repository at this point in the history
  • Loading branch information
devops committed Sep 11, 2024
2 parents 8914fd6 + c17a0ee commit 26a6c93
Show file tree
Hide file tree
Showing 3 changed files with 52 additions and 17 deletions.
57 changes: 45 additions & 12 deletions k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@
import org.kframework.builtin.KLabels;
import org.kframework.builtin.Sorts;
import org.kframework.compile.AddSortInjections;
import org.kframework.compile.ComputeTransitiveFunctionDependencies;
import org.kframework.compile.ExpandMacros;
import org.kframework.compile.RefreshRules;
import org.kframework.compile.RewriteToTop;
Expand Down Expand Up @@ -107,6 +108,7 @@ public enum SentenceType {
public static final String ONE_PATH_OP = KLabels.RL_wEF.name();
public static final String ALL_PATH_OP = KLabels.RL_wAF.name();
private final Module module;
private final Set<String> impureFunctions = new HashSet<>();
private final AddSortInjections addSortInjections;
private final KLabel topCellInitializer;
private final Set<String> mlBinders = new HashSet<>();
Expand Down Expand Up @@ -232,6 +234,14 @@ public void convert(
}
}
}
ComputeTransitiveFunctionDependencies deps = new ComputeTransitiveFunctionDependencies(module);
Set<KLabel> impurities =
stream(module.sortedProductions())
.filter(prod -> prod.klabel().isDefined() && prod.att().contains(Att.IMPURE()))
.filter(prod -> prod.att().contains(Att.IMPURE()))
.map(prod -> prod.klabel().get())
.collect(Collectors.toSet());
impurities.addAll(deps.ancestors(impurities));

semantics.append("\n// symbols\n");
Set<Production> overloads = new HashSet<>();
Expand All @@ -240,8 +250,8 @@ public void convert(
}

syntax.append(semantics);
translateSymbols(attributes, functionRules, overloads, semantics, false);
translateSymbols(attributes, functionRules, overloads, syntax, true);
translateSymbols(attributes, functionRules, impurities, overloads, semantics, false);
translateSymbols(attributes, functionRules, impurities, overloads, syntax, true);

// print syntax definition
for (Tuple2<Sort, scala.collection.immutable.List<Production>> sort :
Expand All @@ -250,6 +260,7 @@ public void convert(
translateSymbol(
attributes,
functionRules,
impurities,
overloads,
prod.att().get(Att.BRACKET_LABEL(), KLabel.class),
prod,
Expand Down Expand Up @@ -303,8 +314,8 @@ public void convert(
if (isFunctional(prod)) {
genFunctionalAxiom(prod, semantics);
}
if (isConstructor(prod, functionRules)) {
genNoConfusionAxioms(prod, noConfusion, functionRules, semantics);
if (isConstructor(prod, functionRules, impurities)) {
genNoConfusionAxioms(prod, noConfusion, functionRules, impurities, semantics);
}
}

Expand Down Expand Up @@ -439,6 +450,7 @@ private void translateSorts(
private void translateSymbols(
Map<Att.Key, Boolean> attributes,
SetMultimap<KLabel, Rule> functionRules,
Set<KLabel> impurities,
Set<Production> overloads,
StringBuilder sb,
boolean withSyntaxAtts) {
Expand All @@ -449,14 +461,25 @@ private void translateSymbols(
if (prod.klabel().isEmpty()) {
continue;
}
if (impurities.contains(prod.klabel().get())) {
impureFunctions.add(prod.klabel().get().name());
}
translateSymbol(
attributes, functionRules, overloads, prod.klabel().get(), prod, sb, withSyntaxAtts);
attributes,
functionRules,
impurities,
overloads,
prod.klabel().get(),
prod,
sb,
withSyntaxAtts);
}
}

private void translateSymbol(
Map<Att.Key, Boolean> attributes,
SetMultimap<KLabel, Rule> functionRules,
Set<KLabel> impurities,
Set<Production> overloads,
KLabel label,
Production prod,
Expand All @@ -480,7 +503,7 @@ private void translateSymbol(
sb.append(") : ");
convert(prod.sort(), prod, sb);
sb.append(" ");
Att koreAtt = koreAttributes(prod, functionRules, overloads, withSyntaxAtts);
Att koreAtt = koreAttributes(prod, functionRules, impurities, overloads, withSyntaxAtts);
convert(attributes, koreAtt, sb, null, null);
sb.append("\n");
}
Expand Down Expand Up @@ -714,6 +737,7 @@ private void genNoConfusionAxioms(
Production prod,
Set<Tuple2<Production, Production>> noConfusion,
SetMultimap<KLabel, Rule> functionRulesMap,
Set<KLabel> impurities,
StringBuilder sb) {
// c(x1,x2,...) /\ c(y1,y2,...) -> c(x1/\y2,x2/\y2,...)
if (prod.arity() > 0) {
Expand Down Expand Up @@ -753,7 +777,7 @@ private void genNoConfusionAxioms(
if (prod2.klabel().isEmpty()
|| noConfusion.contains(Tuple2.apply(prod, prod2))
|| prod.equals(prod2)
|| !isConstructor(prod2, functionRulesMap)
|| !isConstructor(prod2, functionRulesMap, impurities)
|| isBuiltinProduction(prod2)) {
// TODO (traiansf): add no confusion axioms for constructor vs inj.
continue;
Expand Down Expand Up @@ -1615,8 +1639,9 @@ private void convertParams(Option<KLabel> maybeKLabel, boolean hasR, StringBuild
sb.append("}");
}

private boolean isConstructor(Production prod, SetMultimap<KLabel, Rule> functionRules) {
Att att = semanticAttributes(prod, functionRules, java.util.Collections.emptySet());
private boolean isConstructor(
Production prod, SetMultimap<KLabel, Rule> functionRules, Set<KLabel> impurities) {
Att att = semanticAttributes(prod, functionRules, impurities, java.util.Collections.emptySet());
return att.contains(Att.CONSTRUCTOR());
}

Expand Down Expand Up @@ -1652,6 +1677,7 @@ private boolean isGeneratedInKeysOp(Production prod) {
private Att koreAttributes(
Production prod,
SetMultimap<KLabel, Rule> functionRules,
Set<KLabel> impurities,
Set<Production> overloads,
boolean withSyntaxAtts) {
Att att = prod.att();
Expand All @@ -1669,15 +1695,18 @@ private Att koreAttributes(
for (Att.Key key : attsToRemove) {
att = att.remove(key);
}
att = att.addAll(semanticAttributes(prod, functionRules, overloads));
att = att.addAll(semanticAttributes(prod, functionRules, impurities, overloads));
if (withSyntaxAtts) {
att = att.addAll(syntaxAttributes(prod));
}
return att;
}

private Att semanticAttributes(
Production prod, SetMultimap<KLabel, Rule> functionRules, Set<Production> overloads) {
Production prod,
SetMultimap<KLabel, Rule> functionRules,
Set<KLabel> impurities,
Set<Production> overloads) {
boolean isConstructor = !isFunction(prod);
isConstructor &= !prod.att().contains(Att.ASSOC());
isConstructor &= !prod.att().contains(Att.COMM());
Expand All @@ -1692,16 +1721,20 @@ private Att semanticAttributes(
boolean isMacro = prod.isMacro();
boolean isAnywhere = overloads.contains(prod);

Att att = Att.empty();

if (prod.klabel().isDefined()) {
for (Rule r : functionRules.get(prod.klabel().get())) {
isAnywhere |= r.att().contains(Att.ANYWHERE());
}
if (impurities.contains(prod.klabel().get())) {
att = att.add(Att.IMPURE());
}
}

isConstructor &= !isMacro;
isConstructor &= !isAnywhere;

Att att = Att.empty();
if (isHook(prod)) {
att = att.add(Att.HOOK(), prod.att().get(att.HOOK()));
}
Expand Down
10 changes: 6 additions & 4 deletions k-frontend/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -88,10 +88,12 @@ private static <V> Set<V> ancestors(
while (!queue.isEmpty()) {
V v = queue.poll();
Collection<V> neighbors = graph.getPredecessors(v);
for (V n : neighbors) {
if (!visited.contains(n)) {
queue.offer(n);
visited.add(n);
if (neighbors != null) {
for (V n : neighbors) {
if (!visited.contains(n)) {
queue.offer(n);
visited.add(n);
}
}
}
}
Expand Down
2 changes: 1 addition & 1 deletion k-frontend/src/main/scala/org/kframework/attributes/Att.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -289,7 +289,7 @@ object Att {
final val IDEM =
Key.builtin("idem", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline)
final val IMPURE =
Key.builtin("impure", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly)
Key.builtin("impure", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline)
final val INDEX =
Key.builtin("index", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly)
final val INITIAL =
Expand Down

0 comments on commit 26a6c93

Please sign in to comment.