diff --git a/k-distribution/tests/regression-new/checks/checkFuncRuleAtt.k.out b/k-distribution/tests/regression-new/checks/checkFuncRuleAtt.k.out index 489d1e92387..02ad205fcdf 100644 --- a/k-distribution/tests/regression-new/checks/checkFuncRuleAtt.k.out +++ b/k-distribution/tests/regression-new/checks/checkFuncRuleAtt.k.out @@ -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~~~~~~~~~~~~~ diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java index 2109e325648..dea3fe22171 100644 --- a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java +++ b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java @@ -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; diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java b/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java index 3e3efa53aa8..bc38572625e 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckAtt.java @@ -57,7 +57,6 @@ private void checkSentence(Sentence sentence) { } private void checkRule(Rule rule) { - checkMacro(rule); checkNonExecutable(rule); checkSimplification(rule); checkSymbolic(rule); @@ -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 = diff --git a/kernel/src/main/java/org/kframework/compile/checks/CheckFunctions.java b/kernel/src/main/java/org/kframework/compile/checks/CheckFunctions.java index c699bbdc40e..94f7aa07c9f 100644 --- a/kernel/src/main/java/org/kframework/compile/checks/CheckFunctions.java +++ b/kernel/src/main/java/org/kframework/compile/checks/CheckFunctions.java @@ -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; @@ -21,63 +20,14 @@ public record CheckFunctions(Set 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)); } } @@ -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()); diff --git a/kore/src/main/scala/org/kframework/attributes/Att.scala b/kore/src/main/scala/org/kframework/attributes/Att.scala index 3aa891b7c3b..552d3e39bc7 100644 --- a/kore/src/main/scala/org/kframework/attributes/Att.scala +++ b/kore/src/main/scala/org/kframework/attributes/Att.scala @@ -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]) @@ -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])