Merge branch 'develop' into _update-deps/runtimeverification/llvm-bac…

…kend
runtimeverification · Aug 22, 2024 · ff79d7b · ff79d7b
2 parents 244f019 + 0e4c4ea
commit ff79d7b
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 3 deletions.
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
@@ -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/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

diff --git 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,

diff --git a/pyk/.gitignore b/pyk/.gitignore
@@ -10,3 +10,6 @@ __pycache__/
 
 .kprove*
 *.debug-log
+
+.idea/
+.DS_Store