Add syntactic to whitelist (#4597)

Part of #4579

Adds the `syntactic` attribute to the whitelist, and checks that it is
only applied to simplification rules.

Notably, we still need to:
- Check that the arguments actually refer to existing clauses
- Tag the underlying clauses and re-construct the attribute at the end
of the compilation pipeline because the `requires` clauses may be
manipulated during compilation

k-frontend/src/main/java/org/kframework/compile/checks/CheckAtt.java

@@ -60,6 +60,7 @@ private void checkRule(Rule rule) {
  checkNonExecutable(rule);
  checkSimplification(rule);
  checkSymbolic(rule);
+ checkSyntactic(rule);
  }
 
  private void checkProduction(Production prod) {
@@ -151,6 +152,14 @@ private void checkSymbolic(Rule rule) {
  }
  }
 
+ private void checkSyntactic(Rule rule) {
+ if (rule.att().contains(Att.SYNTACTIC()) && !rule.att().contains(Att.SIMPLIFICATION())) {
+ errors.add(
+ KEMException.compilerError(
+ "syntactic attribute is only supported on simplification rules."));
+ }
+ }
+
  private void checkHookedSortConstructors(Production prod) {
  if (prod.sort().equals(Sorts.KItem())) {
  return;

k-frontend/src/main/scala/org/kframework/attributes/Att.scala

@@ -416,6 +416,8 @@ object Att {
  onlyon3[Module, Production, Rule],
  KeyRange.WholePipeline
  )
+ final val SYNTACTIC =
+ Key.builtin("syntactic", KeyParameter.Required, onlyon[Rule], KeyRange.WholePipeline)
  final val TOKEN = Key.builtin(
  "token",
  KeyParameter.Forbidden,