Remove usages of K Source and Location

runtimeverification · Mar 1, 2024 · ec7ffce · ec7ffce
1 parent 9186ac2
commit ec7ffce
Show file tree

Hide file tree

Showing 6 changed files with 48 additions and 15 deletions.
diff --git a/matching/src/main/java/org/kframework/backend/llvm/matching/Location.java b/matching/src/main/java/org/kframework/backend/llvm/matching/Location.java
@@ -0,0 +1,31 @@
+package org.kframework.backend.llvm.matching;
+
+public class Location {
+    int startLine;
+    int endLine;
+    int startColumn;
+    int endColumn;
+
+    public Location(int startLine, int endLine, int startColumn, int endColumn) {
+        this.startLine = startLine;
+        this.endLine = endLine;
+        this.startColumn = startColumn;
+        this.endColumn = endColumn;
+    }
+
+    public int getStartLine() {
+        return startLine;
+    }
+
+    public int getEndLine() {
+        return endLine;
+    }
+
+    public int getStartColumn() {
+        return startColumn;
+    }
+
+    public int getEndColumn() {
+        return endColumn;
+    }
+}
diff --git a/matching/src/main/java/org/kframework/backend/llvm/matching/MatchingException.java b/matching/src/main/java/org/kframework/backend/llvm/matching/MatchingException.java
@@ -1,8 +1,5 @@
 package org.kframework.backend.llvm.matching;
 
-import org.kframework.attributes.Location;
-import org.kframework.attributes.Source;
-
 import java.util.Optional;
 
 public final class MatchingException extends Throwable {

diff --git a/matching/src/main/java/org/kframework/backend/llvm/matching/Source.java b/matching/src/main/java/org/kframework/backend/llvm/matching/Source.java
@@ -0,0 +1,13 @@
+package org.kframework.backend.llvm.matching;
+
+public class Source {
+    String source;
+
+    public Source(String source) {
+        this.source = source;
+    }
+
+    public String getSource() {
+        return source;
+    }
+}
diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala
@@ -3,9 +3,6 @@ package org.kframework.backend.llvm.matching
 import java.util
 import java.util.concurrent.ConcurrentHashMap
 import java.util.Optional
-import org.kframework.attributes.HasLocation
-import org.kframework.attributes.Location
-import org.kframework.attributes.Source
 import org.kframework.backend.llvm.matching.dt._
 import org.kframework.backend.llvm.matching.pattern._
 import org.kframework.kore.KORE.KApply
@@ -328,7 +325,7 @@ case class Action(
     source: Optional[Source],
     location: Optional[Location],
     nonlinear: Boolean
-) extends HasLocation {
+) {
   override lazy val hashCode: Int = scala.runtime.ScalaRunTime._hashCode(this)
 }
 

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
@@ -2,8 +2,6 @@ package org.kframework.backend.llvm.matching
 
 import java.util
 import java.util.Optional
-import org.kframework.attributes.Location
-import org.kframework.attributes.Source
 import org.kframework.parser.kore._
 import org.kframework.parser.kore.implementation.{ DefaultBuilders => B }
 import org.kframework.parser.kore.parser.KoreToK
@@ -161,7 +159,7 @@ object Parser {
   def source(att: Attributes): Optional[Source] =
     if (hasAtt(att, SOURCE)) {
       val sourceStr = getStringAtt(att, SOURCE).get
-      return Optional.of(Source(sourceStr.substring("Source(".length, sourceStr.length - 1)))
+      Optional.of(new Source(sourceStr.substring("Source(".length, sourceStr.length - 1)))
     } else {
       Optional.empty()
     }
@@ -170,8 +168,8 @@ object Parser {
     if (hasAtt(att, LOCATION)) {
       val locStr   = getStringAtt(att, LOCATION).get
       val splitted = locStr.split("[(,)]")
-      return Optional.of(
-        Location(splitted(1).toInt, splitted(2).toInt, splitted(3).toInt, splitted(4).toInt)
+      Optional.of(
+        new Location(splitted(1).toInt, splitted(2).toInt, splitted(3).toInt, splitted(4).toInt)
       )
     } else {
       Optional.empty()

diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/SortCategory.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/SortCategory.scala
@@ -1,9 +1,6 @@
 package org.kframework.backend.llvm.matching.pattern
 
 import java.util.regex.{ Pattern => Regex }
-import java.util.Optional
-import org.kframework.attributes.Location
-import org.kframework.attributes.Source
 import org.kframework.backend.llvm.matching._
 import org.kframework.backend.llvm.matching.dt._
 import org.kframework.backend.llvm.matching.MatchingException