Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Remove usages of K source and location classes #1002

Merged
merged 2 commits into from
Mar 1, 2024
Merged

Remove usages of K source and location classes #1002

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8fa81a3
Remove usages of K Source and Location
Baltoli Mar 1, 2024
485a682
Fix nulls on exhaustiveness check
Baltoli Mar 1, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 31 additions & 0 deletions matching/src/main/java/org/kframework/backend/llvm/matching/Location.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
}
}
3 changes: 0 additions & 3 deletions matching/src/main/java/org/kframework/backend/llvm/matching/MatchingException.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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 {
Expand Down
13 changes: 13 additions & 0 deletions matching/src/main/java/org/kframework/backend/llvm/matching/Source.java
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
}
}
9 changes: 3 additions & 6 deletions matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)
}

Expand Down Expand Up @@ -1087,8 +1084,8 @@ class Matrix private (
val k = fringe.zip(counterexample.get).map(t => t._2.toK(t._1))
val func = KApply(symlib.koreToK(name), KList(k))
val attributes = symlib.signatures(name)._3
val location = Parser.location(attributes).orElse(null)
val source = Parser.source(attributes).orElse(null)
val location = Parser.location(attributes)
val source = Parser.source(attributes)

kem(
new MatchingException(
Expand Down
8 changes: 3 additions & 5 deletions matching/src/main/scala/org/kframework/backend/llvm/matching/Parser.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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()
}
Expand All @@ -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()
Expand Down
3 changes: 0 additions & 3 deletions matching/src/main/scala/org/kframework/backend/llvm/matching/pattern/SortCategory.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
Loading