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.

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

Prohibit macro-like attributes on _all_ rules #3956

Merged
merged 5 commits into from
Feb 6, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
Original file line number Diff line number Diff line change
@@ -1,24 +1,24 @@
[Error] Compiler: Attributes macro|macro-rec|alias|alias-rec are not allowed on function rules.
[Error] Compiler: Rule cannot have the following attributes: [macro]
Source(checkFuncRuleAtt.k)
Location(11,10,11,18)
11 | rule foo => 0 [macro]
. ^~~~~~~~
[Error] Compiler: Attributes macro|macro-rec|alias|alias-rec are not allowed on function rules.
[Error] Compiler: Rule cannot have the following attributes: [macro-rec]
Source(checkFuncRuleAtt.k)
Location(12,10,12,18)
12 | rule foo => 1 [macro-rec]
. ^~~~~~~~
[Error] Compiler: Attributes macro|macro-rec|alias|alias-rec are not allowed on function rules.
[Error] Compiler: Rule cannot have the following attributes: [alias]
Source(checkFuncRuleAtt.k)
Location(13,10,13,18)
13 | rule foo => 2 [alias]
. ^~~~~~~~
[Error] Compiler: Attributes macro|macro-rec|alias|alias-rec are not allowed on function rules.
[Error] Compiler: Rule cannot have the following attributes: [alias-rec]
Source(checkFuncRuleAtt.k)
Location(14,10,14,18)
14 | rule foo => 3 [alias-rec]
. ^~~~~~~~
[Error] Compiler: Attributes macro|macro-rec|alias|alias-rec are not allowed on function rules.
[Error] Compiler: Rule cannot have the following attributes: [macro]
Source(checkFuncRuleAtt.k)
Location(17,10,18,26)
. v~~~~~~~~~~~~~
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -1673,14 +1673,15 @@ private Att addKoreAttributes(
// injective.
boolean isInjective = isConstructor;

boolean isMacro = false;
boolean isMacro = prod.isMacro();
boolean isAnywhere = overloads.contains(prod);

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

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

Expand Down
13 changes: 0 additions & 13 deletions kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,6 @@ private void checkSentence(Sentence sentence) {
}

private void checkRule(Rule rule) {
checkMacro(rule);
checkNonExecutable(rule);
checkSimplification(rule);
checkSymbolic(rule);
Expand Down Expand Up @@ -109,18 +108,6 @@ private void checkLabel(Sentence sentence) {
}
}

private void checkMacro(Rule rule) {
if (rule.isMacro()) {
kem.registerCompilerWarning(
ExceptionType.FUTURE_ERROR,
errors,
"The attribute ["
+ rule.att().getMacro().get()
+ "] has been deprecated on rules. Use this label on syntax declarations instead.",
rule);
}
}

private void checkNonExecutable(Rule rule) {
boolean isNonExecutable = rule.att().contains(Att.NON_EXECUTABLE());
boolean isFunction =
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@
import java.util.Set;
import org.kframework.attributes.Att;
import org.kframework.compile.RewriteAwareVisitor;
import org.kframework.definition.Claim;
import org.kframework.definition.Context;
import org.kframework.definition.ContextAlias;
import org.kframework.definition.Module;
Expand All @@ -21,63 +20,14 @@ public record CheckFunctions(Set<KEMException> errors, Module m) {
public void check(Sentence sentence) {
if (sentence instanceof Rule rl) {
checkFuncAtt(rl);
if (!rl.att().contains(Att.SIMPLIFICATION()))
if (!rl.att().contains(Att.SIMPLIFICATION())) {
// functions are allowed on the LHS of simplification rules
check(rl.body());
} else if (sentence instanceof Claim c) {
// functions are allowed on LHS of claims
if (c.att().contains(Att.MACRO())
|| c.att().contains(Att.MACRO_REC())
|| c.att().contains(Att.ALIAS())
|| c.att().contains(Att.ALIAS_REC()))
errors.add(
KEMException.compilerError(
"Attributes "
+ Att.MACRO()
+ "|"
+ Att.MACRO_REC()
+ "|"
+ Att.ALIAS()
+ "|"
+ Att.ALIAS_REC()
+ " are not allowed on claims.",
c));
}
} else if (sentence instanceof Context ctx) {
check(ctx.body());
if (ctx.att().contains(Att.MACRO())
|| ctx.att().contains(Att.MACRO_REC())
|| ctx.att().contains(Att.ALIAS())
|| ctx.att().contains(Att.ALIAS_REC()))
errors.add(
KEMException.compilerError(
"Attributes "
+ Att.MACRO()
+ "|"
+ Att.MACRO_REC()
+ "|"
+ Att.ALIAS()
+ "|"
+ Att.ALIAS_REC()
+ " are not allowed on contexts.",
ctx));
} else if (sentence instanceof ContextAlias ctx) {
check(ctx.body());
if (ctx.att().contains(Att.MACRO())
|| ctx.att().contains(Att.MACRO_REC())
|| ctx.att().contains(Att.ALIAS())
|| ctx.att().contains(Att.ALIAS_REC()))
errors.add(
KEMException.compilerError(
"Attributes "
+ Att.MACRO()
+ "|"
+ Att.MACRO_REC()
+ "|"
+ Att.ALIAS()
+ "|"
+ Att.ALIAS_REC()
+ " are not allowed on contexts.",
ctx));
}
}

Expand Down Expand Up @@ -140,31 +90,6 @@ public void checkFuncAtt(Rule r) {
public void apply(KApply k) {
if (k.klabel().name().equals("#withConfig")) {
super.apply(k);
return;
}
if ((isRHS() && !isLHS())
|| k.klabel() instanceof KVariable
|| !m.attributesFor().contains(k.klabel())) {
return;
}
Att attributes = m.attributesFor().apply(k.klabel());
if (attributes.contains(Att.FUNCTION())
&& (r.att().contains(Att.MACRO())
|| r.att().contains(Att.MACRO_REC())
|| r.att().contains(Att.ALIAS())
|| r.att().contains(Att.ALIAS_REC()))) {
errors.add(
KEMException.compilerError(
"Attributes "
+ Att.MACRO()
+ "|"
+ Att.MACRO_REC()
+ "|"
+ Att.ALIAS()
+ "|"
+ Att.ALIAS_REC()
+ " are not allowed on function rules.",
r));
}
}
}.apply(r.body());
Expand Down
28 changes: 14 additions & 14 deletions kore/src/main/scala/org/kframework/attributes/Att.scala
Original file line number Diff line number Diff line change
Expand Up @@ -241,10 +241,10 @@ object Att {
onlyon3[T1, T2, T3] ++ onlyon[T4]

/* Built-in attribute keys which can appear in user source code */
final val ALIAS = Key.builtin("alias", KeyParameter.Forbidden, onlyon2[Production, Rule])
final val ALIAS_REC = Key.builtin("alias-rec", KeyParameter.Forbidden, onlyon2[Production, Rule])
final val ALL_PATH = Key.builtin("all-path", KeyParameter.Forbidden, onlyon2[Claim, Module])
final val ANYWHERE = Key.builtin("anywhere", KeyParameter.Forbidden, onlyon[Rule])
final val ALIAS = Key.builtin("alias", KeyParameter.Forbidden, onlyon[Production])
final val ALIAS_REC = Key.builtin("alias-rec", KeyParameter.Forbidden, onlyon[Production])
final val ALL_PATH = Key.builtin("all-path", KeyParameter.Forbidden, onlyon2[Claim, Module])
final val ANYWHERE = Key.builtin("anywhere", KeyParameter.Forbidden, onlyon[Rule])
final val APPLY_PRIORITY = Key.builtin("applyPriority", KeyParameter.Required, onlyon[Production])
final val ASSOC = Key.builtin("assoc", KeyParameter.Forbidden, onlyon[Production])
final val AVOID = Key.builtin("avoid", KeyParameter.Forbidden, onlyon[Production])
Expand Down Expand Up @@ -288,16 +288,16 @@ object Att {
final val KLABEL = Key.builtin("klabel", KeyParameter.Required, onlyon[Production])
final val TERMINATOR_KLABEL =
Key.builtin("terminator-klabel", KeyParameter.Required, onlyon[Production])
final val LABEL = Key.builtin("label", KeyParameter.Required, onlyon[Sentence])
final val LATEX = Key.builtin("latex", KeyParameter.Required, onlyon[Production])
final val LEFT = Key.builtin("left", KeyParameter.Forbidden, onlyon[Production])
final val LOCATIONS = Key.builtin("locations", KeyParameter.Forbidden, onlyon[SyntaxSort])
final val MACRO = Key.builtin("macro", KeyParameter.Forbidden, onlyon2[Production, Rule])
final val MACRO_REC = Key.builtin("macro-rec", KeyParameter.Forbidden, onlyon2[Production, Rule])
final val MAINCELL = Key.builtin("maincell", KeyParameter.Forbidden, onlyon[Production])
final val MEMO = Key.builtin("memo", KeyParameter.Forbidden, onlyon[Production])
final val ML_BINDER = Key.builtin("mlBinder", KeyParameter.Forbidden, onlyon[Production])
final val ML_OP = Key.builtin("mlOp", KeyParameter.Forbidden, onlyon[Production])
final val LABEL = Key.builtin("label", KeyParameter.Required, onlyon[Sentence])
final val LATEX = Key.builtin("latex", KeyParameter.Required, onlyon[Production])
final val LEFT = Key.builtin("left", KeyParameter.Forbidden, onlyon[Production])
final val LOCATIONS = Key.builtin("locations", KeyParameter.Forbidden, onlyon[SyntaxSort])
final val MACRO = Key.builtin("macro", KeyParameter.Forbidden, onlyon[Production])
final val MACRO_REC = Key.builtin("macro-rec", KeyParameter.Forbidden, onlyon[Production])
final val MAINCELL = Key.builtin("maincell", KeyParameter.Forbidden, onlyon[Production])
final val MEMO = Key.builtin("memo", KeyParameter.Forbidden, onlyon[Production])
final val ML_BINDER = Key.builtin("mlBinder", KeyParameter.Forbidden, onlyon[Production])
final val ML_OP = Key.builtin("mlOp", KeyParameter.Forbidden, onlyon[Production])
final val MULTIPLICITY = Key.builtin("multiplicity", KeyParameter.Required, onlyon[Production])
final val NON_ASSOC = Key.builtin("non-assoc", KeyParameter.Forbidden, onlyon[Production])
final val NON_EXECUTABLE = Key.builtin("non-executable", KeyParameter.Forbidden, onlyon[Rule])
Expand Down
Loading