Skip to content

Commit

Permalink
Add total to #let-bindings where LHS is a variable (#3798)
Browse files Browse the repository at this point in the history 
This PR addresses an issue whereby the Booster reverts to the old
Haskell backend when it encounters a rule written using `#let` bindings.
The reason for this is that the de-sugared form of `#let` is expressed
in terms of an intermediate `#lambda` function that is not marked as
being `total`.

To address the issue, this PR adds the `total` attribute to the
desugared intermediate lambda function for let-bindings and anonymous
functions when the left-hand side of the original binding is a variable.

Points to consider when reviewing this PR:
* ~~Is the identification of when the LHS a variable correct in its
handling of semantic casts and sorting? My presumption is that it is
given that the "first child of `#SemanticCastTo` `KApply`" logic is
replicated elsewhere.~~
*
#3798 (comment)
* Is there a way to integration-test this change other than "it doesn't
break the rest of the test suite"? At the moment I'm not sure there is
an obvious way to do so, but I'm open to suggestions.

Fixes #3715

---------

Co-authored-by: rv-jenkins <[email protected]>
  • Loading branch information
@Baltoli @rv-jenkins
Baltoli and rv-jenkins authored Nov 14, 2023
1 parent 0bad2c3 commit fb08dee
Showing 1 changed file with 59 additions and 21 deletions.
80 changes: 59 additions & 21 deletions kernel/src/main/java/org/kframework/compile/ResolveFun.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
import java.util.ArrayList;
import java.util.HashSet;
import java.util.List;
import java.util.Optional;
import java.util.Set;
import java.util.function.UnaryOperator;
import java.util.stream.Collectors;
Expand All @@ -29,6 +30,7 @@
import org.kframework.kore.KApply;
import org.kframework.kore.KAs;
import org.kframework.kore.KLabel;
import org.kframework.kore.KRewrite;
import org.kframework.kore.KSequence;
import org.kframework.kore.KToken;
import org.kframework.kore.KVariable;
Expand All @@ -42,7 +44,11 @@
* <p>The rule Ctx[#fun(Pattern)(Expression)] is equivalent to the following sentences assuming some
* completely unique KLabel #lambda1 not used in any token:
*
* <p>rule Ctx[#lambda1(Expression)] syntax K ::= #lambda1(K) [function] rule #lambda1(LHS) => RHS
* <pre>
* rule Ctx[#lambda1(Expression)]
* syntax K ::= #lambda1(K) [function]
* rule #lambda1(LHS) => RHS
* </pre>
*
* <p>Where LHS is the LHS of Pattern and RHS is the RHS of Pattern.
*
Expand Down Expand Up @@ -101,15 +107,14 @@ public K apply(KApply k) {
body = k.items().get(0);
arg = k.items().get(1);
}
if (arg instanceof KVariable) {
nameHint1 = ((KVariable) arg).name();
} else if (arg instanceof KApply
&& ((KApply) arg).klabel().name().startsWith("#SemanticCastTo")
&& ((KApply) arg).items().get(0) instanceof KVariable) {
nameHint1 = ((KVariable) ((KApply) arg).items().get(0)).name();

Optional<KVariable> underlying = underlyingVariable(arg);
if (underlying.isPresent()) {
nameHint1 = underlying.get().name();
}
if (body instanceof KApply) {
nameHint2 = ((KApply) body).klabel().name();

if (body instanceof KApply app) {
nameHint2 = app.klabel().name();
}
KLabel fun = getUniqueLambdaLabel(nameHint1, nameHint2);
Sort lhsSort = sort(RewriteToTop.toLeft(body));
Expand All @@ -118,7 +123,9 @@ public K apply(KApply k) {
if (lbl.name().equals("#fun3")
|| lbl.name().equals("#fun2")
|| lbl.name().equals("#let")) {
funProds.add(funProd(fun, body, lubSort));
boolean total =
body instanceof KRewrite rew && underlyingVariable(rew.left()).isPresent();
funProds.add(funProd(fun, body, lubSort, total));
funRules.add(funRule(fun, body, k.att()));
} else {
funProds.add(predProd(fun, body, lubSort));
Expand All @@ -139,6 +146,32 @@ public K apply(KApply k) {
}.apply(body);
}

/**
* Get the underlying variable from a (possibly nested) set of semantic casts. For example, in
* each of the following terms the variable X is returned:
*
* <pre>
* X
* ((X))
* X:Sort
* (X:SortA):SortB
* </pre>
*
* The {@link KRewrite} induced by a {@code #let} or {@code #fun} binding is considered to be
* total if its left-hand side has an underlying variable.
*/
private Optional<KVariable> underlyingVariable(K term) {
if (term instanceof KVariable var) {
return Optional.of(var);
} else if (term instanceof KApply app
&& app.klabel().name().startsWith("#SemanticCastTo")
&& app.items().size() == 1) {
return underlyingVariable(app.items().get(0));
}

return Optional.empty();
}

private Rule funRule(KLabel fun, K k, Att att) {
return lambdaRule(fun, k, k, att, RewriteToTop::toRight);
}
Expand Down Expand Up @@ -184,15 +217,20 @@ private List<KVariable> closure(K k) {
return result;
}

private Production funProd(KLabel fun, K k, Sort arg) {
return lambdaProd(fun, k, arg, sort(RewriteToTop.toRight(k)));
private Production funProd(KLabel fun, K k, Sort arg, boolean total) {
Att att = total ? Att().add(Att.TOTAL()) : Att();
return lambdaProd(fun, k, arg, sort(RewriteToTop.toRight(k)), att);
}

private Production predProd(KLabel fun, K k, Sort arg) {
return lambdaProd(fun, k, arg, Sorts.Bool());
}

private Production lambdaProd(KLabel fun, K k, Sort arg, Sort rhs) {
return lambdaProd(fun, k, arg, rhs, Att());
}

private Production lambdaProd(KLabel fun, K k, Sort arg, Sort rhs, Att att) {
List<ProductionItem> pis = new ArrayList<>();
pis.add(Terminal(fun.name()));
pis.add(Terminal("("));
Expand All @@ -202,14 +240,14 @@ private Production lambdaProd(KLabel fun, K k, Sort arg, Sort rhs) {
pis.add(NonTerminal(var.att().getOptional(Sort.class).orElse(Sorts.K())));
}
pis.add(Terminal(")"));
return Production(fun, rhs, immutable(pis), Att().add(Att.FUNCTION()));
return Production(fun, rhs, immutable(pis), att.add(Att.FUNCTION()));
}

private Sort sort(K k) {
if (k instanceof KSequence) return Sorts.K();
if (k instanceof KAs) return sort(((KAs) k).pattern());
if (k instanceof KAs as) return sort(as.pattern());
if (k instanceof InjectedKLabel) return Sorts.KItem();
if (k instanceof KToken) return ((KToken) k).sort();
if (k instanceof KToken token) return token.sort();
if (k instanceof KApply) {
return inj.sort(k, Sorts.K());
}
Expand All @@ -227,12 +265,12 @@ private ContextAlias resolve(ContextAlias context) {
}

public Sentence resolve(Sentence s) {
if (s instanceof Rule) {
return resolve((Rule) s);
} else if (s instanceof Context) {
return resolve((Context) s);
} else if (s instanceof ContextAlias) {
return resolve((ContextAlias) s);
if (s instanceof Rule r) {
return resolve(r);
} else if (s instanceof Context c) {
return resolve(c);
} else if (s instanceof ContextAlias ca) {
return resolve(ca);
} else {
return s;
}
Expand Down

0 comments on commit fb08dee

Please sign in to comment.