add some data about attributes to AxiomInfo

runtimeverification · Jul 18, 2023 · 1284c9f · 1284c9f
1 parent e3ed1bf
commit 1284c9f
Showing 1 changed file with 7 additions and 3 deletions.
diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Parser.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Parser.scala
@@ -7,7 +7,7 @@ import org.kframework.parser.kore.implementation.{DefaultBuilders => B}
 import java.util
 import java.util.Optional
 
-case class AxiomInfo(priority: Int, ordinal: Int, rewrite: GeneralizedRewrite, sideCondition: Option[Pattern], source: Optional[Source], location: Optional[Location]) {}
+case class AxiomInfo(priority: Int, ordinal: Int, rewrite: GeneralizedRewrite, sideCondition: Option[Pattern], source: Optional[Source], location: Optional[Location], att: Attributes) {}
 
 object Parser {
 
@@ -20,7 +20,11 @@ object Parser {
   }
 
   def getAtt(axiom: AxiomDeclaration, att: String): Option[Pattern] = {
-    axiom.att.patterns.find(isAtt(att, _))
+    getAtt(axiom.att, att)
+  }
+
+  def getAtt(att: Attributes, att: String): Option[Pattern] = {
+    att.patterns.find(isAtt(att, _))
   }
 
   def getStringAtt(att: Attributes, attName: String): Option[String] = {
@@ -143,7 +147,7 @@ object Parser {
       if (hasAtt(s, "comm") || hasAtt(s, "assoc") || hasAtt(s, "idem") || hasAtt(s, "unit") || hasAtt(s, "non-executable") || (hasAtt(s, "simplification") && !simplification)) {
         Seq()
       } else {
-        Seq((splitted.get._1, AxiomInfo(rulePriority(s, search), axiom._2, splitted.get._2, splitted.get._3, source(s), location(s))))
+        Seq((splitted.get._1, AxiomInfo(rulePriority(s, search), axiom._2, splitted.get._2, splitted.get._3, source(s), location(s), s.att)))
       }
     } else {
       Seq()