Skip to content

Commit

Permalink
Merge branch 'sem-highlight' of https://github.com/viperproject/viper…
Browse files Browse the repository at this point in the history 
…server into sem-highlight
  • Loading branch information
@marcoeilers
marcoeilers committed Feb 12, 2024
2 parents ca46f01 + bf2bc9f commit 16ec8d5
Show file tree
Hide file tree
Showing 4 changed files with 3 additions and 259 deletions.
15 changes: 0 additions & 15 deletions src/main/scala/viper/server/frontends/lsp/file/FileContent.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,25 +30,12 @@ case class FileContent(path: Path) extends DiskLoader {
}

val fileContent = new ArrayBuffer[String]
// val lineToChar = new ArrayBuffer[Int]

def set(newContent: String): Unit = {
fileContent.clear()
fileContent.addAll(newContent.split("\n", -1))
// var idx = 0
// fileContent.foreach(line => {
// lineToChar.addOne(idx)
// idx += line.length + 1
// })
}

// def rpToCharRange(rp: RangePosition): CharRange = {
// CharRange(
// lineToChar(rp.start.line) + rp.start.column,
// lineToChar(rp._end.line) + rp._end.column,
// )
// }

override def loadContent(path: Path): Try[String] =
if (this.path == path) Success(fileContent.mkString("\n")) else super.loadContent(path)

Expand Down Expand Up @@ -95,13 +82,11 @@ case class FileContent(path: Path) extends DiskLoader {
normalize(pos).flatMap(nPos => {
val start = iterBackward(nPos).drop(1).takeWhile { case (c, _) => Common.isIdentChar(c) }.length
val startPos = new Position(nPos.getLine, nPos.getCharacter - start)
// println("startPos: " + startPos.toString() + " " + nPos.toString())
if (!Common.isIdentStartChar(getCharAt(startPos))) return None
val end = iterForward(nPos).takeWhile { case (c, _) => Common.isIdentChar(c) }.length
val endPos = new Position(nPos.getLine, nPos.getCharacter + end)
if (start == 0 && end == 0 || inComment(nPos)) None else {
val ident = fileContent(nPos.getLine).slice(startPos.getCharacter, endPos.getCharacter)
// println("got: " + ident)
Some((ident, new Range(startPos, endPos)))
}
})
Expand Down
26 changes: 3 additions & 23 deletions src/main/scala/viper/server/frontends/lsp/file/Manager.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,39 +6,19 @@

package viper.server.frontends.lsp.file

import java.net.URI
import java.nio.file.{Path, Paths}
import akka.actor.{Actor, Props, Status}
import org.eclipse.lsp4j.{Diagnostic, DiagnosticSeverity, DocumentSymbol, FoldingRange, Position, PublishDiagnosticsParams, Range, SymbolKind}
import viper.server.core.VerificationExecutionContext
import java.nio.file.Path
import org.eclipse.lsp4j.{PublishDiagnosticsParams, Range}
import viper.server.frontends.lsp.ClientCoordinator
import viper.server.frontends.lsp.VerificationState._
import viper.server.frontends.lsp.VerificationSuccess._
import viper.server.vsi.VerJobId
import viper.silver.ast
import viper.silver.ast.{AbstractSourcePosition, HasLineColumn}
import viper.silver.reporter._
import viper.silver.verifier.{AbortedExceptionally, AbstractError, ErrorMessage}

import scala.jdk.CollectionConverters._
import scala.collection.mutable.{ArrayBuffer, HashMap}
import scala.concurrent.Future
import org.eclipse.lsp4j.ParameterInformation
import org.eclipse.lsp4j.jsonrpc.messages.Tuple.Two
import viper.server.vsi.AstJobId
import scala.collection.mutable.ArrayBuffer
import viper.server.frontends.lsp.file.FileContent
import viper.server.frontends.lsp.file.ProgressCoordinator
import viper.server.frontends.lsp.Lsp4jSemanticHighlight
import VerificationPhase._

import org.eclipse.lsp4j
import viper.silver.ast.utility.lsp
import viper.server.frontends.lsp.file.utility.LspContainer
import ch.qos.logback.classic.Logger
import viper.server.frontends.lsp.file.utility.StageContainer
import viper.silver.ast.utility.lsp.GotoDefinition
import viper.server.frontends.lsp.Common
import viper.silver.ast.utility.lsp.DocumentSymbol

case class Diagnostic(backendClassName: Option[String], position: lsp.RangePosition, message: String, severity: lsp4j.DiagnosticSeverity, cached: Boolean, errorMsgPrefix: Option[String]) extends lsp.HasRangePositions with lsp.BelongsToFile {
override def rangePositions: Seq[lsp.RangePosition] = Seq(position)
Expand Down
220 changes: 0 additions & 220 deletions src/main/scala/viper/server/frontends/lsp/file/utility/Containers.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,12 +15,7 @@ import ch.qos.logback.classic.Logger
import scala.collection.mutable.HashMap
import viper.silver.ast.utility.lsp
import viper.silver.ast.utility.lsp.SelectionBoundScopeTrait
import viper.silver.ast.utility.lsp.SelectionBoundScope
import viper.silver.ast.utility.lsp.SelectionBoundBoth
import viper.silver.ast.utility.lsp.SelectionBoundKeyword
import viper.silver.ast.utility.lsp.SelectionBound
import viper.silver.ast.utility.lsp.SelectionBoundKeywordTrait
import viper.server.frontends.lsp.file.VerificationPhase._

trait StageContainer[K, V, I] {
var resetCount: Int = 0
Expand All @@ -38,9 +33,6 @@ trait StageContainer[K, V, I] {
def all(): Iterator[V]
def filterInPlace(p: V => Boolean): Unit
}
// trait StageProjectContainer[K, V] extends StageContainer[K, V] {
// def get(uri: String, k: K): Seq[V]
// }

case class StageArrayContainer[V]() extends StageContainer[Unit, V, Int] {
private val array: ArrayBuffer[V] = ArrayBuffer()
Expand All @@ -57,25 +49,11 @@ case class StageArrayContainer[V]() extends StageContainer[Unit, V, Int] {
override def all(): Iterator[V] = array.iterator
def filterInPlace(p: V => Boolean): Unit = array.filterInPlace(p)
}
// case class StageArrayContainer[V]() extends StageArrayContainerTrait[V]
object StageArrayContainer {
type ArrayContainer[V <: HasRangePositions with BelongsToFile, U] = LspContainer[StageArrayContainer[V], Unit, V, Int, U]
implicit def default[V]: () => StageArrayContainer[V] = () => StageArrayContainer()
}

// case class StageArrayProjectContainer[V <: BelongsToFile](uriToStage: String => StageArrayContainer[V])(implicit root: String) extends StageArrayContainerTrait[V] {
// override def add(v: V): Unit = {
// val uri = v.file.toUri().toString()
// if (uri == root) super.add(v) else uriToStage(uri).add(v)
// }
// override def get(uri: String, k: Unit): Seq[V] = if (uri == root) super.get(uri, k) else uriToStage(uri).get(uri, k)
// }
// object StageArrayProjectContainer {
// type ArrayProjectContainer[V <: HasRangePositions with BelongsToFile, U, T <: Translates[V, U, Unit]] = LspProjectContainer[StageArrayProjectContainer[V], Unit, V, U, T]

// def default[V <: BelongsToFile](uriToStage: String => StageArrayContainer[V])(implicit root: String): StageArrayProjectContainer[V] = StageArrayProjectContainer[V](uriToStage)
// }

case class StageRangeContainer[V <: SelectableInBound]() extends StageContainer[(Option[lsp4j.Position], Option[(String, lsp4j.Range)], Boolean), V, (Option[String], Int)] {
// Has a `scope` bound
val localKeyword: HashMap[String, ArrayBuffer[V]] = HashMap()
Expand Down Expand Up @@ -129,7 +107,6 @@ case class StageRangeContainer[V <: SelectableInBound]() extends StageContainer[
localKeyword.filterInPlace((_, g) => g.nonEmpty)
}
}
// case class StageRangeContainer[V <: SelectableInBound[_, SelectionBoundScopeTrait]]() extends StageRangeContainerTrait[V]
object StageRangeContainer {
type RangeContainer[V <: HasRangePositions with SelectableInBound, U] = LspContainer[StageRangeContainer[V], (Option[lsp4j.Position], Option[(String, lsp4j.Range)], Boolean), V, (Option[String], Int), U]
implicit def default[V <: SelectableInBound]: () => StageRangeContainer[V] = () => StageRangeContainer()
Expand Down Expand Up @@ -192,73 +169,11 @@ case class StageSuggestableContainer[V <: lsp.SuggestableInBound]() extends Stag
perScope.filterInPlace((_, g) => g.nonEmpty)
}
}
// case class StageRangeContainer[V <: SelectableInBound[_, SelectionBoundScopeTrait]]() extends StageRangeContainerTrait[V]
object StageSuggestableContainer {
type SuggestableContainer[V <: HasRangePositions with lsp.SuggestableInBound, U] = LspContainer[StageSuggestableContainer[V], (lsp.SuggestionScope, Option[lsp4j.Position], Char), V, Map[Option[lsp.SuggestionScope], Int], U]
implicit def default[V <: lsp.SuggestableInBound]: () => StageSuggestableContainer[V] = () => StageSuggestableContainer()
}

// case class StageRangeProjectContainer[V <: SelectableInBound[V, SelectionBoundTrait]](uriToStage: String => StageRangeContainer[SelectableInBound[V, SelectionBoundScopeTrait]])(implicit root: String) extends StageRangeContainerTrait[SelectableInBound[V, SelectionBoundScopeTrait]] {
// // No `scope` bound
// val globalKeyword: HashMap[String, ArrayBuffer[V]] = HashMap()
// val global: ArrayBuffer[V] = ArrayBuffer()

// override def reset(): Unit = {
// super.reset()
// globalKeyword.clear()
// global.clear()
// }
// override def add(v: V): Unit = v.selectableInScope match {
// case Some(u) => {
// val uri = u.bound.scope.file.toUri().toString()
// if (uri == root) super.add(u) else uriToStage(uri).add(u)
// }
// case None => v.bound match {
// case bound: SelectionBoundKeywordTrait =>
// globalKeyword.getOrElseUpdate(bound.keyword, ArrayBuffer()).addOne(v)
// case _ => global.addOne(v)
// }
// }
// override def get(k: (Option[lsp4j.Position], Option[(String, lsp4j.Range)])): Seq[V] = {
// val local = if (uri == root) super.get(uri, k) else uriToStage(uri).get(uri, k)
// global.toSeq ++ globalKeyword.get(k._1).toSeq.flatten ++ local.map(_.get)
// }
// override def all(): Iterator[V] =
// super.all().map(_.get) ++ global.iterator ++ globalKeyword.values.flatten
// override def filterInPlace(p: V => Boolean): Unit = {
// super.filterInPlace(v => p(v.get))
// global.filterInPlace(p)
// globalKeyword.values.foreach(_.filterInPlace(p))
// globalKeyword.filterInPlace((_, g) => g.nonEmpty)
// }
// }
// object StageRangeProjectContainer {
// type RangeProjectContainer[V <: HasRangePositions with SelectableInBound[V, SelectionBoundTrait], U] = LspContainer[StageRangeProjectContainer[V], (Option[lsp4j.Position], Option[(String, lsp4j.Range)]), V, U]

// def default[V <: SelectableInBound[V, SelectionBoundTrait]](uriToStage: String => StageRangeContainer[SelectableInBound[V, SelectionBoundScopeTrait]])(implicit root: String): StageRangeProjectContainer[V] = StageRangeProjectContainer[V](uriToStage)
// }

// case class RangeSelector[T <: SelectableInBound](
// localKeyword: HashMap[String, ArrayBuffer[T]] = HashMap[String, ArrayBuffer[T]](),
// localPosition: ArrayBuffer[T] = ArrayBuffer[T](),
// globalKeyword: HashMap[String, ArrayBuffer[T]] = HashMap[String, ArrayBuffer[T]](),
// ) {
// def getGlobal(ident: String): Seq[T] = {
// globalKeyword.get(ident).toSeq.flatMap(_.toSeq)
// }
// def getLocalForPos(ident: String, pos: lsp4j.Position): Seq[T] = {
// // println("Checking for local pos: " + pos.toString() + " in " + localPosition.toString())
// localKeyword.get(ident).toSeq.flatMap(_.filter(inLocalPos(pos)).toSeq) ++
// localPosition.filter(inLocalPos(pos)).toSeq
// }
// def inLocalPos(pos: lsp4j.Position)(h: T): Boolean = {
// val range = Common.toRange(h.bound.scope.get)
// Common.comparePosition(range.getStart(), pos) <= 0 &&
// Common.comparePosition(range.getEnd(), pos) >= 0
// }
// // def setLocal
// }

case class LspContainer[+C <: StageContainer[K, V, I], K, V <: HasRangePositions, I, U]
(translator: Translates[V, U, K], onUpdate: () => Unit = () => {}, expandOnBorder: Boolean = false)(implicit initial: () => C) {
private val parseTypeck: C = initial()
Expand Down Expand Up @@ -316,15 +231,12 @@ case class LspContainer[+C <: StageContainer[K, V, I], K, V <: HasRangePositions
}

for (buffer <- Seq(parseTypeck, verify)) buffer.filterInPlace(v => {
// println("Updating pos for " + v.toString)
val positions = v.rangePositions
var overlapped = false
for (pos <- positions if !pos.modified && !overlapped) {
pos.modified = true
val pRange = Common.toRange(pos)
val cmp = Common.compareRange(pRange, range)
// println("PRange: " + pRange.toString() + " Range: " + range.toString())
// println("Cmp: " + cmp)
cmp match {
case -4 =>
case -3 | -2 =>
Expand All @@ -347,139 +259,7 @@ case class LspContainer[+C <: StageContainer[K, V, I], K, V <: HasRangePositions
case _ =>
}
}
// if (overlapped) println("overlapped: " + v.toString())
!overlapped
})
}
}

// case class LspProjectContainer[C <: StageProjectContainer[K, V], K, V <: HasRangePositions, U, T <: Translates[V, U, K]]
// (containerInFile: String => LspContainer[C, K, V], onUpdate: () => Unit = () => {})
// (implicit initial: (String => StageContainer[K, V]) => C, implicit val translator: T) extends LspContainerTrait[C, K, V] {
// override val parse: C = initial(containerInFile(_).parse)
// override val typeck: C = initial(containerInFile(_).typeck)
// override val verify: C = initial(containerInFile(_).verify)

// def resetAll() = {
// resetParse(false)
// resetTypeck(false)
// resetVerify(false)
// onUpdate()
// }
// def resetParse(doUpdate: Boolean = true) = {
// parse.reset()
// if (doUpdate) onUpdate()
// }
// def resetTypeck(doUpdate: Boolean = true) = {
// typeck.reset()
// if (doUpdate) onUpdate()
// }
// def resetVerify(doUpdate: Boolean = true) = {
// verify.reset()
// if (doUpdate) onUpdate()
// }

// // private def addToFile[N <: V with BelongsToFile](v: N, uriToStage: String => StageContainer[K, V]) = {
// // val uri = v.file.toUri().toString()
// // uriToStage(uri).add(v)
// // }

// def receiveParse(ps: Seq[V], doUpdate: Boolean = true): Unit = {
// ps.foreach(receiveParse(_, false))
// if (doUpdate) onUpdate()
// }
// def receiveTypeck(ps: Seq[V], doUpdate: Boolean = true): Unit = {
// ps.foreach(receiveTypeck(_, false))
// if (doUpdate) onUpdate()
// }
// def receiveVerify(ps: Seq[V], doUpdate: Boolean = true): Unit = {
// ps.foreach(receiveVerify(_, false))
// if (doUpdate) onUpdate()
// }

// def receiveParse(p: V, doUpdate: Boolean): Unit = {
// this.parse.add(p)
// if (doUpdate) onUpdate()
// }
// def receiveTypeck(t: V, doUpdate: Boolean): Unit = {
// this.typeck.add(t)
// if (doUpdate) onUpdate()
// }
// def receiveVerify(v: V, doUpdate: Boolean): Unit = {
// this.verify.add(v)
// if (doUpdate) onUpdate()
// }

// def get(uri: String, k: K)(implicit log: Logger): Seq[U] = translator.translate(Seq(parse.get(uri, k), typeck.get(uri, k), verify.get(uri, k)).flatten)(k)

// /** If a range position is aliased, we do not want to update it twice */
// def resetModifiedFlag(): Unit = {
// parse.all().foreach(_.rangePositions.foreach(_.modified = false))
// typeck.all().foreach(_.rangePositions.foreach(_.modified = false))
// verify.all().foreach(_.rangePositions.foreach(_.modified = false))
// }
// /**
// * Update the positions of semantic tokens after a change in the file
// *
// * @param range Replaced (deleted) range
// * @param text Newly inserted (added) text
// */
// def updatePositions(range: lsp4j.Range, text: String): Unit = {
// val lines = text.split("\n", -1)
// val deltaLines = lines.length - 1 + range.getStart.getLine - range.getEnd.getLine
// val startCharacter = if (lines.length == 1) range.getStart.getCharacter else 0
// val deltaChars = startCharacter + lines.last.length - range.getEnd.getCharacter
// val endLine = range.getEnd.getLine

// // TODO:
// // If the change cannot ruin the meaning of a semantic token at the start,
// // adjust the range start to avoid overlaps with adjacent tokens
// // if (text.isEmpty || !text.head.isLetterOrDigit) {
// // range.getStart.setCharacter(range.getStart.getCharacter + 1)
// // }
// // If the change cannot ruin the meaning of a semantic token at the end,
// // adjust the range end to avoid overlaps with adjacent tokens
// // if (text.isEmpty || !text.last.isLetterOrDigit) {
// // range.getEnd.setCharacter(range.getEnd.getCharacter - 1)
// // }
// // Remove overlapping semantic tokens and update positions of those after change
// def shiftEnd(pos: RangePosition, end: lsp4j.Position): Unit = {
// if (end.getLine == endLine) pos.shiftEnd(deltaLines, deltaChars)
// else pos.shiftEnd(deltaLines, 0)
// }
// def shiftStart(pos: RangePosition, start: lsp4j.Position): Unit = {
// if (start.getLine == endLine) pos.shiftStart(deltaLines, deltaChars)
// else pos.shiftStart(deltaLines, 0)
// }

// for (buffer <- Seq(parse, typeck, verify)) buffer.filterInPlace(v => {
// val positions = v.rangePositions
// var overlapped = false
// for (pos <- positions if !pos.modified && !overlapped) {
// pos.modified = true
// val start = Common.toPosition(pos.start)
// val end = Common.toPosition(pos._end)
// Common.containsPos(range, start) match {
// // `start` < `range.start`
// case neg if neg < 0 => Common.containsPos(range, end) match {
// // `end` < `range.start`
// case neg if neg < 0 => {}
// // `end` within `range`
// case 0 => overlapped = true
// // `end` > `range.end`
// case _ => shiftEnd(pos, end)
// }
// // `start` within `range`
// case 0 => overlapped = true
// // `start` > `range.end`
// case _ => {
// shiftStart(pos, start)
// shiftEnd(pos, end)
// }
// }
// }
// if (overlapped) println("overlapped: " + v.toString())
// !overlapped
// })
// }
// }
1 change: 0 additions & 1 deletion src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,6 @@ import ch.qos.logback.classic.Logger

import scala.jdk.CollectionConverters._
import scala.collection.mutable.ArrayBuffer
import viper.silver.ast.utility.lsp.DocumentSymbol

trait Translates[-T, +U, I] {
def translate(t: T)(i: I): U
Expand Down

0 comments on commit 16ec8d5

Please sign in to comment.