From 6aae149b6f7bbeebdb949bcfa082c1464cb5f666 Mon Sep 17 00:00:00 2001
From: Scott Guest <scott.guest@runtimeverification.com>
Date: Wed, 21 Aug 2024 21:02:33 -0700
Subject: [PATCH 1/3] 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
---
 .../java/org/kframework/compile/checks/CheckAtt.java     | 9 +++++++++
 .../src/main/scala/org/kframework/attributes/Att.scala   | 2 ++
 2 files changed, 11 insertions(+)

diff --git a/k-frontend/src/main/java/org/kframework/compile/checks/CheckAtt.java b/k-frontend/src/main/java/org/kframework/compile/checks/CheckAtt.java
index 8268041cca9..45eea040134 100644
--- a/k-frontend/src/main/java/org/kframework/compile/checks/CheckAtt.java
+++ b/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;
diff --git a/k-frontend/src/main/scala/org/kframework/attributes/Att.scala b/k-frontend/src/main/scala/org/kframework/attributes/Att.scala
index 5be702cb370..e81750f1694 100644
--- a/k-frontend/src/main/scala/org/kframework/attributes/Att.scala
+++ b/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,

From 0055fe7c67e9b2637230a518d52f0fcfd3345aad Mon Sep 17 00:00:00 2001
From: Scott Guest <scott.guest@runtimeverification.com>
Date: Wed, 21 Aug 2024 22:02:39 -0700
Subject: [PATCH 2/3] Don't trim list separators (#4596)

Closes #4592

Previously, we trimmed list separators, presumably under the assumption
that `#Layout` deletes all whitespace and the user may end up including
redundant whitespace. This is hacky and a faulty assumption given that
we allow custom `#Layout`.

For now, we just remove the `trim()` call. This shouldn't cause issues
downstream - I've manually checked that all `List{...}` and
`NeList{...}` declarations in the EVM, C, and WASM semantics are already
correct. If anything was missed, it's an easy fix.

A proper solution is described in #4595

Co-authored-by: rv-jenkins <admin@runtimeverification.com>
---
 k-frontend/src/main/java/org/kframework/kil/UserList.java | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/k-frontend/src/main/java/org/kframework/kil/UserList.java b/k-frontend/src/main/java/org/kframework/kil/UserList.java
index 05f22b959cd..4c42c990daa 100644
--- a/k-frontend/src/main/java/org/kframework/kil/UserList.java
+++ b/k-frontend/src/main/java/org/kframework/kil/UserList.java
@@ -18,13 +18,13 @@ public class UserList extends ProductionItem {
 
   public UserList(Sort sort, String separator) {
     this.sort = sort;
-    this.separator = separator.trim();
+    this.separator = separator;
     this.listType = ZERO_OR_MORE;
   }
 
   public UserList(Sort sort, String separator, String listType) {
     this.sort = sort;
-    this.separator = separator.trim();
+    this.separator = separator;
     this.listType = listType;
   }
 
@@ -58,7 +58,7 @@ public String getSeparator() {
   }
 
   public void setSeparator(String separator) {
-    this.separator = separator.trim();
+    this.separator = separator;
   }
 
   @Override

From 0e4c4ea7286ef31ca0ee159a2af3e61f1b65232f Mon Sep 17 00:00:00 2001
From: JianHong Zhao <zhaojianhong96@gmail.com>
Date: Thu, 22 Aug 2024 14:38:55 +0800
Subject: [PATCH 3/3] Update .gitignore for MacOS and Pycharm (#4599)

Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com>
---
 pyk/.gitignore | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/pyk/.gitignore b/pyk/.gitignore
index 5a5bd829a48..e8fd5033e06 100644
--- a/pyk/.gitignore
+++ b/pyk/.gitignore
@@ -10,3 +10,6 @@ __pycache__/
 
 .kprove*
 *.debug-log
+
+.idea/
+.DS_Store
\ No newline at end of file