diff --git a/carbon b/carbon index bd453cb..4761f90 160000 --- a/carbon +++ b/carbon @@ -1 +1 @@ -Subproject commit bd453cb0c156b1307caa43a1273a7fae6f9265e7 +Subproject commit 4761f900b66fc7b395c628f0b5c20a5fb1389cbd diff --git a/silicon b/silicon index cec06e4..cfc2397 160000 --- a/silicon +++ b/silicon @@ -1 +1 @@ -Subproject commit cec06e4952245cd7d1c67b45728ce1872ad0c7da +Subproject commit cfc23979faad76058da633f76313633456674866 diff --git a/src/main/scala/viper/server/core/ViperCache.scala b/src/main/scala/viper/server/core/ViperCache.scala index 4679f42..482aec1 100644 --- a/src/main/scala/viper/server/core/ViperCache.scala +++ b/src/main/scala/viper/server/core/ViperCache.scala @@ -13,12 +13,14 @@ import net.liftweb.json.JsonAST.JObject import viper.server.core.ViperCache.logger import viper.server.vsi._ import viper.silver.{ast => vpr} -import viper.silver.ast.{Add, And, AnonymousDomainAxiom, AnySetCardinality, AnySetContains, AnySetIntersection, AnySetMinus, AnySetSubset, AnySetUnion, Apply, Applying, Assert, Cached, CondExp, ConsInfo, CurrentPerm, Div, Domain, DomainFunc, DomainFuncApp, EmptyMultiset, EmptySeq, EmptySet, EpsilonPerm, EqCmp, Exhale, Exists, ExplicitMultiset, ExplicitSeq, ExplicitSet, FalseLit, Field, FieldAccess, FieldAccessPredicate, FieldAssign, Fold, ForPerm, Forall, FractionalPerm, FullPerm, FuncApp, Function, GeCmp, Goto, GtCmp, Hashable, If, Implies, Inhale, InhaleExhaleExp, IntLit, IntPermMul, Label, LabelledOld, LeCmp, Let, LocalVar, LocalVarAssign, LocalVarDecl, LocalVarDeclStmt, LtCmp, MagicWand, Method, MethodCall, Minus, Mod, Mul, NamedDomainAxiom, NeCmp, NewStmt, NoPerm, Node, Not, NullLit, Old, Or, Package, PermAdd, PermDiv, PermGeCmp, PermGtCmp, PermLeCmp, PermLtCmp, PermMinus, PermMul, PermSub, Position, Predicate, PredicateAccess, PredicateAccessPredicate, Program, RangeSeq, SeqAppend, SeqContains, SeqDrop, SeqIndex, SeqLength, SeqTake, SeqUpdate, Seqn, Sub, Trigger, TrueLit, Unfold, Unfolding, While, WildcardPerm} +import viper.silver.ast.{Add, And, AnonymousDomainAxiom, AnySetCardinality, AnySetContains, AnySetIntersection, AnySetMinus, AnySetSubset, AnySetUnion, Apply, Applying, Assert, Cached, CondExp, ConsInfo, CurrentPerm, Div, Domain, DomainFunc, DomainFuncApp, EmptyMultiset, EmptySeq, EmptySet, EpsilonPerm, EqCmp, Exhale, Exists, ExplicitMultiset, ExplicitSeq, ExplicitSet, FalseLit, Field, FieldAccess, FieldAccessPredicate, FieldAssign, FilePosition, Fold, ForPerm, Forall, FractionalPerm, FullPerm, FuncApp, Function, GeCmp, Goto, GtCmp, Hashable, IdentifierPosition, If, Implies, Inhale, InhaleExhaleExp, IntLit, IntPermMul, Label, LabelledOld, LeCmp, Let, LineColumnPosition, LocalVar, LocalVarAssign, LocalVarDecl, LocalVarDeclStmt, LtCmp, MagicWand, Method, MethodCall, Minus, Mod, Mul, NamedDomainAxiom, NeCmp, NewStmt, NoPerm, Node, Not, NullLit, Old, Or, Package, PermAdd, PermDiv, PermGeCmp, PermGtCmp, PermLeCmp, PermLtCmp, PermMinus, PermMul, PermSub, Position, Predicate, PredicateAccess, PredicateAccessPredicate, Program, RangeSeq, SeqAppend, SeqContains, SeqDrop, SeqIndex, SeqLength, SeqTake, SeqUpdate, Seqn, SourcePosition, Sub, TranslatedPosition, Trigger, TrueLit, Unfold, Unfolding, While, WildcardPerm} import viper.silver.utility.CacheHelper import viper.silver.verifier.errors.{ApplyFailed, CallFailed, ContractNotWellformed, FoldFailed, HeuristicsFailed, IfFailed, InhaleFailed, Internal, LetWandFailed, UnfoldFailed, _} -import viper.silver.verifier.{AbstractVerificationError, VerificationError, errors} +import viper.silver.verifier.{AbstractVerificationError, FailureContext, VerificationError, errors} import net.liftweb.json.Serialization.{read, write} import net.liftweb.json.{DefaultFormats, Formats, JArray, JField, JInt, JString, MappingException, ShortTypeHints} +import viper.silicon.interfaces.SiliconAbductionFailureContext +import viper.silver.ast.utility.lsp.RangePosition import viper.silver.verifier.reasons.{AssertionFalse, DivisionByZero, EpsilonAsParam, FeatureUnsupported, InsufficientPermission, InternalReason, InvalidPermMultiplication, LabelledStateNotReached, MagicWandChunkNotFound, MapKeyNotContained, NegativePermission, QPAssertionNotInjective, ReceiverNull, SeqIndexExceedsLength, SeqIndexNegative, UnexpectedNode} import java.nio.charset.StandardCharsets @@ -83,7 +85,11 @@ object ViperCache extends Cache { val content = read[ViperCacheContent](ce.content.asInstanceOf[SerializedViperCacheContent].content) logger.trace(s"Got a cache hit for method ${concerning_method.name} and backend $backendName") // set cached flag: - val cachedErrors = content.errors.map(setCached) + val cachedErrors = content.errors.map(e => { + val ce = setCached(e._1) + ce.failureContexts = e._2 + ce + }) CacheResult(concerning_method, cachedErrors) } catch { case e: Throwable => @@ -307,7 +313,7 @@ object ViperCache extends Cache { val key: String = getKey(file = file, backendName = backendName) implicit val formats: Formats = DefaultFormats.withHints(ViperCacheHelper.errorNodeHints(p, key)) - SerializedViperCacheContent(write(ViperCacheContent(errors))) + SerializedViperCacheContent(write(ViperCacheContent(errors.map(e => (e, e.failureContexts.filter(c => c.isInstanceOf[SiliconAbductionFailureContext])))))) } } @@ -521,7 +527,9 @@ object ViperCacheHelper { classOf[InternalReason], classOf[FeatureUnsupported], classOf[UnexpectedNode], classOf[AssertionFalse], classOf[EpsilonAsParam], classOf[ReceiverNull], classOf[DivisionByZero], classOf[NegativePermission], classOf[InsufficientPermission], classOf[InvalidPermMultiplication], classOf[MagicWandChunkNotFound], classOf[QPAssertionNotInjective], classOf[LabelledStateNotReached], classOf[SeqIndexNegative], - classOf[SeqIndexExceedsLength], classOf[MapKeyNotContained] + classOf[SeqIndexExceedsLength], classOf[MapKeyNotContained], classOf[SiliconAbductionFailureContext], classOf[LineColumnPosition], + classOf[FilePosition], classOf[RangePosition], classOf[IdentifierPosition], classOf[SourcePosition], classOf[TranslatedPosition], + classOf[IdentifierPosition] )) { override def serialize: PartialFunction[Any, JObject] = { @@ -556,7 +564,7 @@ case class SerializedViperCacheContent(content: String) extends CacheContent /** Class containing the verification results of a viper verification run * */ -case class ViperCacheContent(errors: List[AbstractVerificationError]) +case class ViperCacheContent(errors: List[(AbstractVerificationError, Seq[FailureContext])]) /** An access path holds a List of Numbers * diff --git a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala index b3d59ad..831e582 100644 --- a/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala +++ b/src/main/scala/viper/server/frontends/lsp/ClientCoordinator.scala @@ -209,6 +209,14 @@ class ClientCoordinator(val server: ViperServerService)(implicit executor: Verif } } + def sendInferenceResults(irs: InferenceResultParams): Unit = { + try{ + client.get.notifyInferenceResults(irs) + } catch { + case e: Throwable => logger.debug(s"Error while sending inference results: $e") + } + } + def refreshEndings(): Future[Array[String]] = { client.map{_.requestVprFileEndings().asScala.map(response => { _vprFileEndings = Some(response.fileEndings) diff --git a/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala b/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala index e67e5a3..e5d759c 100644 --- a/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala +++ b/src/main/scala/viper/server/frontends/lsp/CommandProtocol.scala @@ -32,6 +32,7 @@ object S2C_Commands { final val Log = "Log" final val Hint = "Hint" final val VerificationNotStarted = "VerificationNotStarted" + final val InferenceResults = "InferenceResults" // final val StopDebugging = "StopDebugging" // final val StepsAsDecorationOptions = "StepsAsDecorationOptions" // final val HeapGraph = "HeapGraph" diff --git a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala index cd3c385..5c4a423 100644 --- a/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala +++ b/src/main/scala/viper/server/frontends/lsp/DataProtocol.scala @@ -178,6 +178,17 @@ case class StateChangeParams( stage: String = null, error: String = null) +case class InferenceResultParams( + inferenceResults: Array[InferenceResult]) + +case class InferenceResult( + start_line: Int, + start_col: Int, + end_line: Int, + end_col: Int, + edit: String, + file_uri: String) + case class UnhandledViperServerMessageTypeParams(msgType: String, msg: String, logLevel: Int) /** diff --git a/src/main/scala/viper/server/frontends/lsp/IdeLanguageClient.scala b/src/main/scala/viper/server/frontends/lsp/IdeLanguageClient.scala index 0b614f3..600ba56 100644 --- a/src/main/scala/viper/server/frontends/lsp/IdeLanguageClient.scala +++ b/src/main/scala/viper/server/frontends/lsp/IdeLanguageClient.scala @@ -41,4 +41,7 @@ trait IdeLanguageClient extends LanguageClient { @JsonNotification(S2C_Commands.StateChange) def notifyStateChanged(params: StateChangeParams): Unit + + @JsonNotification(S2C_Commands.InferenceResults) + def notifyInferenceResults(irs: InferenceResultParams): Unit } diff --git a/src/main/scala/viper/server/frontends/lsp/Receiver.scala b/src/main/scala/viper/server/frontends/lsp/Receiver.scala index 810994c..be50d94 100644 --- a/src/main/scala/viper/server/frontends/lsp/Receiver.scala +++ b/src/main/scala/viper/server/frontends/lsp/Receiver.scala @@ -312,8 +312,12 @@ trait TextDocumentReceiver extends StandardReceiver with TextDocumentService { } override def codeAction(params: CodeActionParams) = { - // TODO - CompletableFuture.completedFuture(Nil.asJava) + coordinator.logger.trace(s"[Req: textDocument/codeAction] ${params.toString()}") + val uri = params.getTextDocument.getUri + val ctxt = params.getContext + var diags = Seq.empty[Diagnostic] + ctxt.getDiagnostics.asScala.foreach(diag => diags = diags :+ diag) + coordinator.getRoot(uri).getCodeAction(uri, diags).map(cacts => cacts.map(cact => Either.forRight[Command, CodeAction](cact)).asJava).asJava.toCompletableFuture } override def formatting(params: DocumentFormattingParams) = { diff --git a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeLens.scala b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeLens.scala index a9df937..83faf45 100644 --- a/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeLens.scala +++ b/src/main/scala/viper/server/frontends/lsp/ast/utility/CodeLens.scala @@ -13,8 +13,12 @@ trait HasCodeLens { case class CodeLens( /** The range in which this code lens is valid. Should only span a single line. */ range: RangePosition, + /** The text this code lens displays. */ + title: String, /** The command this code lens represents. */ - command: String, + command: Option[String] = None, + /** The command this code lens represents. */ + args: Option[Seq[AnyRef]] = None ) extends HasRangePositions with BelongsToFile { override def rangePositions: Seq[RangePosition] = Seq(range) override def file = range.file diff --git a/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala b/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala index 2b6d7b1..cb9427d 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/FileManager.scala @@ -40,6 +40,7 @@ trait ManagesLeaf { def resetDiagnostics(first: Boolean): Unit def resetContainers(first: Boolean): Unit def addDiagnostic(first: Boolean)(vs: Seq[Diagnostic]): Unit + def addCodeAction(first: Boolean)(vs: Seq[CodeAction]): Unit def getInFuture[T](f: => T): Future[T] } diff --git a/src/main/scala/viper/server/frontends/lsp/file/Manager.scala b/src/main/scala/viper/server/frontends/lsp/file/Manager.scala index bf017d4..84b36d8 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Manager.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Manager.scala @@ -18,12 +18,27 @@ import viper.server.frontends.lsp.Lsp4jSemanticHighlight import org.eclipse.lsp4j import viper.silver.ast.utility.lsp import viper.server.frontends.lsp.Common +import viper.silicon.biabduction.ProgramEdit 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) override def file: Path = position.file } +case class CodeAction(backendClassName: Option[String], + title: String, + kind: String, + diags: Seq[Diagnostic], + command: Option[(String, String)], + edit: Option[Seq[ProgramEdit]], + diagkey: Option[lsp4j.Diagnostic], + fileinfo: PathInfo + ) extends lsp.HasRangePositions with lsp.BelongsToFile with utility.HasKey[lsp4j.Diagnostic] { + override def rangePositions: Seq[lsp.RangePosition] = diags.map(_.position) + override def file: Path = fileinfo.path + override val key: lsp4j.Diagnostic = diagkey.orNull +} + trait Manager { val file: PathInfo val content: FileContent @@ -33,6 +48,9 @@ trait Manager { def addContainer(c: utility.LspContainer[_, _, _, _, _]): Unit def resetContainers(first: Boolean): Unit + def getCodeAction(diag: lsp4j.Diagnostic): Seq[lsp4j.CodeAction] + def addCodeAction(first: Boolean)(vs: Seq[CodeAction]): Unit + def getCodeLens(): Seq[lsp4j.CodeLens] def addCodeLens(first: Boolean)(vs: Seq[lsp.CodeLens]): Unit @@ -71,6 +89,7 @@ trait Manager { } /** Stores and handles all aspects relating the the lsp features: + * - CodeAction * - CodeLens * - Diagnostic * - DocumentSymbol @@ -103,6 +122,20 @@ trait StandardManager extends Manager { } + // CodeAction + type CodeActionContainer = utility.StageMapContainer.MapContainer[CodeAction, lsp4j.Diagnostic, lsp4j.CodeAction] + val codeActionContainer: CodeActionContainer = utility.LspContainer(utility.CodeActionTranslator, () => {}) + private def initCodeActionKey(codeAction: CodeAction): Seq[CodeAction] = { + var cas: Seq[CodeAction] = Seq.empty + codeAction.diags.foreach(diag => { + cas = cas :+ new CodeAction(codeAction.backendClassName, codeAction.title, codeAction.kind, Seq(diag), codeAction.command, codeAction.edit, Some(diagnosticContainer.translator.translate(diag)()), codeAction.fileinfo) + }) + cas + } + containers.addOne(codeActionContainer) + def getCodeAction(diag: lsp4j.Diagnostic): Seq[lsp4j.CodeAction] = codeActionContainer.get(diag) + def addCodeAction(first: Boolean)(vs: Seq[CodeAction]): Unit = add(codeActionContainer, first, vs.map(v => initCodeActionKey(v)).flatten) + // CodeLens type CodeLensContainer = utility.StageArrayContainer.ArrayContainer[lsp.CodeLens, lsp4j.CodeLens] val codeLensContainer: CodeLensContainer = utility.LspContainer(utility.CodeLensTranslator, if (coordinator.client.isDefined) coordinator.client.get.refreshCodeLenses else () => {}) diff --git a/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala b/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala index 18d9fc9..001266b 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/ProjectManager.scala @@ -141,6 +141,8 @@ trait ProjectManager extends ProjectAware { }) grouped foreach (g => toC(g._1)(g._2)) } + override def addCodeAction(first: Boolean)(vs: Seq[CodeAction]): Unit = + addBtf(uri => getInProject(uri).addCodeAction(first), vs) def addCodeLens(first: Boolean)(vs: Seq[lsp.CodeLens]): Unit = addBtf(uri => getInProject(uri).addCodeLens(first), vs) @@ -236,6 +238,8 @@ trait ProjectManager extends ProjectAware { } } + def getCodeAction(uri: String, diags: Seq[lsp4j.Diagnostic]): Future[Seq[lsp4j.CodeAction]] = + Future.successful(diags.map(diag => getInProject(uri).getCodeAction(diag)).flatten) // Can force a refresh in the future if we get new ones, so return immediately def getCodeLens(uri: String): Future[Seq[lsp4j.CodeLens]] = Future.successful(getInProject(uri).getCodeLens()) diff --git a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala index 4b3bc89..796077a 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/Verification.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/Verification.scala @@ -8,23 +8,27 @@ package viper.server.frontends.lsp.file import ch.qos.logback.classic.Logger import viper.server.frontends.lsp + import scala.concurrent.Future import viper.server.core.ViperBackendConfig import viper.server.vsi.{AstJobId, VerJobId} + import scala.concurrent.ExecutionContext import akka.actor.Props - import viper.server.frontends.lsp.VerificationSuccess._ import viper.server.frontends.lsp.VerificationState._ - import viper.silver.verifier.AbstractError + import scala.collection.mutable.HashSet import viper.silver.ast.AbstractSourcePosition import org.eclipse.lsp4j.Range import org.eclipse.lsp4j +import viper.server.frontends.lsp.{InferenceResult, InferenceResultParams} import viper.silver.ast.utility.lsp.RangePosition import viper.silver.ast.HasLineColumn import viper.silver.ast.LineColumnPosition +import viper.silicon.interfaces._ +import viper.silver.verifier._ case class VerificationHandler(server: lsp.ViperServerService, logger: Logger) { private var waitingOn: Option[Either[AstJobId, VerJobId]] = None @@ -123,6 +127,7 @@ trait VerificationManager extends ManagesLeaf { //other var lastSuccess: VerificationSuccess = NA var internalErrorMessage: String = "" + var inferenceMode: Boolean = false //state specific to one verification var is_aborting: Boolean = false @@ -212,6 +217,7 @@ trait VerificationManager extends ManagesLeaf { def startVerification(backendClassName: String, customArgs: String, loader: FileContent, mt: Boolean): Future[Boolean] = { lastBackendClassName = Some(backendClassName) lastCustomArgs = Some(customArgs) + inferenceMode = customArgs.contains("--inferenceMode=full") val backend = ViperBackendConfig(backendClassName, customArgs) coordinator.logger.info(s"verify $filename ($backendClassName $customArgs)") @@ -279,6 +285,8 @@ trait VerificationManager extends ManagesLeaf { def processErrors(backendClassName: Option[String], errors: Seq[AbstractError], errorMsgPrefix: Option[String] = None): Unit = { val errMsgPrefixWithWhitespace = errorMsgPrefix.map(s => s"$s ").getOrElse("") val files = HashSet[String]() + var cas: Seq[CodeAction] = Seq.empty + var lsp_irs: Array[InferenceResult] = Array.empty val diags = errors.map(err => { coordinator.logger.info(s"Handling error ${err.toString()}") @@ -327,12 +335,49 @@ trait VerificationManager extends ManagesLeaf { val cachFlag: String = if(err.cached) " (cached)" else "" val message = s"$errMsgPrefixWithWhitespace${err.readableMessage}$cachFlag" - (phase, Diagnostic(backendClassName, rp, message, severity, err.cached, errorMsgPrefix)) + val diagnostic = Diagnostic(backendClassName, rp, message, severity, err.cached, errorMsgPrefix) + //If error contains inference results and inference mode is on error, create code action for inference results + if (errorType == "Verification error"){ + err match { + case g: VerificationError => + g.failureContexts.foreach { + case h1: SiliconAbductionFailureContext => + h1.fix match { + case Some(irs) => + irs.foreach(ir => + lsp_irs = lsp_irs :+ InferenceResult( + start_line = ir.start.line, + start_col = ir.start.column, + end_line = ir.end.line, + end_col = ir.end.column, + edit = ir.newText, + file_uri = this.file.file_uri) + ) + cas = cas :+ CodeAction(backendClassName, irs.map(ir => + if (ir.newText.equals("")) + "remove: Line " + ir.start.line + ", Col " + ir.start.column + " to Line " + ir.end.line + ", Col " + ir.end.column + else + "insert: " + ir.newText).foldLeft("")((cur: String, next: String) => if (cur == "") next else cur + ", " + next), "quickfix", Seq(diagnostic), None, Some(irs), None, this.file) + case None => () + } + case _ => () + } + case _ => () + } + } + (phase, diagnostic) }) + + if(inferenceMode){ + coordinator.sendInferenceResults(InferenceResultParams(inferenceResults = lsp_irs)) + return + } + diagnosticCount += errors.size errorCount += diags.count(_._2.severity == lsp4j.DiagnosticSeverity.Error) diags.groupBy(d => d._1).foreach { case (phase, diags) => this.addDiagnostic(phase.order <= VerificationPhase.TypeckEnd.order)(diags.map(_._2)) } + this.addCodeAction(true)(cas) } } diff --git a/src/main/scala/viper/server/frontends/lsp/file/utility/Containers.scala b/src/main/scala/viper/server/frontends/lsp/file/utility/Containers.scala index d37028f..d6ac3b3 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/utility/Containers.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/utility/Containers.scala @@ -17,6 +17,10 @@ import viper.silver.ast.utility.lsp import viper.silver.ast.utility.lsp.SelectionBoundScopeTrait import viper.silver.ast.utility.lsp.SelectionBoundKeywordTrait +trait HasKey[K] { + val key: K +} + trait StageContainer[K, V, I] { var resetCount: Int = 0 def reset(): Unit = { @@ -54,6 +58,33 @@ object StageArrayContainer { implicit def default[V]: () => StageArrayContainer[V] = () => StageArrayContainer() } +case class StageMapContainer[K, V <: HasKey[K]]() extends StageContainer[K, V, K]{ + private val map: HashMap[K, Seq[V]] = HashMap() + + override protected def innerReset(): Unit = map.clear() + override protected def innerAdd(v: V): K = { + map.put(v.key, map.getOrElse(v.key, Seq.empty) :+ v) + v.key + } + override def get(k: K): Seq[V] = { + map.getOrElse(k, Seq.empty) + } + override protected def innerUpdate(i: K, f: V => V): Boolean = { + if (!map.contains(i)) { + false + } else { + map.put(i, map(i).map(v => f(v))) + true + } + } + override def all(): Iterator[V] = map.values.flatten.iterator + override def filterInPlace(p: V => Boolean): Unit = map.values.map(vs => vs.filter(p)) +} +object StageMapContainer { + type MapContainer[V <: HasRangePositions with BelongsToFile with HasKey[K], K, U] = LspContainer[StageMapContainer[K, V], K, V, K, U] + implicit def default[K, V <: HasKey[K]]: () => StageMapContainer[K, V] = () => StageMapContainer() +} + 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() diff --git a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala index ece3667..5727316 100644 --- a/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala +++ b/src/main/scala/viper/server/frontends/lsp/file/utility/Conversions.scala @@ -10,8 +10,10 @@ import org.eclipse.lsp4j import org.eclipse.lsp4j.jsonrpc.messages.Either import viper.silver.ast.utility.lsp import viper.server.frontends.lsp.{Common, Lsp4jSemanticHighlight} -import viper.server.frontends.lsp.file.{Diagnostic, FindReferences} +import viper.server.frontends.lsp.file.{CodeAction, Diagnostic, FindReferences} import ch.qos.logback.classic.Logger +import org.eclipse.lsp4j.Command +import org.eclipse.lsp4j.WorkspaceEdit import scala.jdk.CollectionConverters._ import scala.collection.mutable.ArrayBuffer @@ -21,11 +23,42 @@ trait Translates[-T, +U, I] { def translate(t: Seq[T])(i: I)(implicit @annotation.unused log: Logger): Seq[U] = t.map(translate(_)(i)) } +object TranslationHelper { + def toWorkspaceEdit(uri: String, edits: Seq[viper.silicon.biabduction.ProgramEdit]): WorkspaceEdit = { + new WorkspaceEdit((Map(uri -> edits.map(edit => + new lsp4j.TextEdit( + new lsp4j.Range( + Common.toPosition(edit.start), + Common.toPosition(edit.end)), + edit.newText) + ).asJava)).asJava) + } +} + +case object CodeActionTranslator extends Translates[CodeAction, lsp4j.CodeAction, lsp4j.Diagnostic] { + override def translate(cact: CodeAction)(i: lsp4j.Diagnostic): lsp4j.CodeAction = { + val lspca = new lsp4j.CodeAction(cact.title) + lspca.setKind(cact.kind) + lspca.setDiagnostics(Seq(cact.key).asJava) + lspca.setEdit( + cact.edit match { + case Some(e) => TranslationHelper.toWorkspaceEdit(cact.fileinfo.file_uri, e) + case None => null + }) + lspca.setCommand(cact.command match { + case Some(e) => new Command(e._1, e._2) + case None => null + }) + lspca + } +} + case object CodeLensTranslator extends Translates[lsp.CodeLens, lsp4j.CodeLens, Unit] { override def translate(lens: lsp.CodeLens)(i: Unit): lsp4j.CodeLens = { val range = Common.toRange(lens.range) - val command = new lsp4j.Command(lens.command, "") - new lsp4j.CodeLens(range, command, null) + val command = new lsp4j.Command(lens.title, lens.command.getOrElse(""), lens.args.getOrElse(Seq.empty).asJava) + val data = lens.args.orNull + new lsp4j.CodeLens(range, command, data) } }