Add information required for LSP features to Parse AST

src/main/scala/viper/silver/ast/Position.scala

@@ -12,10 +12,13 @@ import java.nio.file.Path
 import viper.silver.parser.FastParser
 
 /** A trait describing the position of occurrence of an AST node. */
-sealed trait Position
+sealed trait Position {
+  def deltaColumn(delta: Int): Position
+}
 
 /** Describes ''no location'' for cases where a `Position` is expected, but not available. */
 case object NoPosition extends Position {
+  override def deltaColumn(delta: Int): Position = this
   override def toString = "<no position>"
 }
 
@@ -25,6 +28,7 @@ trait HasLineColumn extends Position {
 
   def column: Int
 
+  def deltaColumn(delta: Int): HasLineColumn
   override def toString = s"$line.$column"
 }
 
@@ -35,7 +39,9 @@ trait HasIdentifier extends HasLineColumn {
   def id: String
 }
 
-case class LineColumnPosition(line: Int, column: Int) extends HasLineColumn
+case class LineColumnPosition(line: Int, column: Int) extends HasLineColumn {
+  override def deltaColumn(delta: Int): HasLineColumn = LineColumnPosition(line, column + delta)
+}
 
 /** Represents a source code position by referencing a file, a line and a column.
   * Optionally, an additional end position can be specified.
@@ -57,6 +63,7 @@ trait AbstractSourcePosition extends HasLineColumn {
   private def lineColComponent(lc_pos: HasLineColumn) =
     s"${lc_pos.line}.${lc_pos.column}"
 
+  override def deltaColumn(delta: Int): AbstractSourcePosition
   override def toString: String = end match {
     case None =>
       s"$fileComponent${lineColComponent(start)}"
@@ -79,12 +86,16 @@ object AbstractSourcePosition {
 class SourcePosition(val file: Path, val start: HasLineColumn, val end: Option[HasLineColumn])
   extends AbstractSourcePosition with StructuralEquality {
 
+  override def deltaColumn(delta: Int): SourcePosition =
+    new SourcePosition(file, start.deltaColumn(delta), end.map(_.deltaColumn(delta)))
   protected val equalityDefiningMembers: Seq[Object] =
     file :: start :: end :: Nil
 }
 
 class IdentifierPosition(val file: Path, val start: HasLineColumn, val end: Option[HasLineColumn], val id: String)
   extends AbstractSourcePosition with StructuralEquality with HasIdentifier {
+  override def deltaColumn(delta: Int): IdentifierPosition =
+    new IdentifierPosition(file, start.deltaColumn(delta), end.map(_.deltaColumn(delta)), id)
   protected val equalityDefiningMembers: Seq[Object] =
     file :: start :: end :: id :: Nil
 }
@@ -122,13 +133,16 @@ case class TranslatedPosition(pos: AbstractSourcePosition) extends AbstractSourc
   val file: Path = pos.file
   val start: HasLineColumn = pos.start
   val end: Option[HasLineColumn] = pos.end
+  override def deltaColumn(delta: Int): TranslatedPosition =
+    new TranslatedPosition(pos.deltaColumn(delta))
 }
 
 case class FilePosition(file: Path, vline: Int, col: Int) extends util.parsing.input.Position with HasLineColumn {
   override lazy val line: Int = vline
   override lazy val column: Int = col
   override lazy val lineContents: String = toString
   override lazy val toString: String = s"${file.getFileName}@$vline.$col"
+  override def deltaColumn(delta: Int): FilePosition = FilePosition(file, vline, col + delta)
 }
 
 /**
@@ -138,4 +152,5 @@ case class FilePosition(file: Path, vline: Int, col: Int) extends util.parsing.i
   */
 case class VirtualPosition(identifier: String) extends Position {
   override def toString: String = identifier
+  override def deltaColumn(delta: Int): VirtualPosition = this
 }

src/main/scala/viper/silver/ast/Program.scala

@@ -268,7 +268,7 @@ case class Program(domains: Seq[Domain], fields: Seq[Field], functions: Seq[Func
 
   lazy val groundTypeInstances = DomainInstances.findNecessaryTypeInstances(this)
 
-  lazy val members: Seq[Member with Serializable] = domains ++ fields ++ functions ++ predicates ++ methods
+  val members: Seq[Member with Serializable] = domains ++ fields ++ functions ++ predicates ++ methods ++ extensions
 
   def findFieldOptionally(name: String): Option[Field] = this.fieldsByName.get(name)
 
@@ -826,7 +826,7 @@ object BackendFunc {
 /**
   * The Extension Member trait provides the way to expand the Ast to include new Top Level declarations
   */
-trait ExtensionMember extends Member{
+trait ExtensionMember extends Member with Serializable {
   def extensionSubnodes: Seq[Node]
   def prettyPrint: PrettyPrintPrimitives#Cont
 }

src/main/scala/viper/silver/ast/utility/Consistency.scala

@@ -165,13 +165,15 @@ object Consistency {
     val argVars = args.map(_.localVar).toSet
     var s = Seq.empty[ConsistencyError]
 
-    for (a@LocalVarAssign(l, _) <- b if argVars.contains(l)) {
+    // Suppressing "pattern var a in value $anonfun is never used: use a wildcard `_` or suppress this warning with `a@_`" warning using `(true || a == a)`
+    for (a@LocalVarAssign(l, _) <- b if argVars.contains(l) && (true || a == a)) {
       s :+= ConsistencyError(s"$a is a reassignment of formal argument $l.", a.pos)
     }
     for (c@MethodCall(_, _, targets) <- b; t <- targets if argVars.contains(t)) {
       s :+= ConsistencyError(s"$c is a reassignment of formal argument $t.", c.pos)
     }
-    for (n@NewStmt(l, _) <- b if argVars.contains(l)){
+    // Suppressing "pattern var n in value $anonfun is never used: use a wildcard `_` or suppress this warning with `n@_`" warning using `(true || n == n)`
+    for (n@NewStmt(l, _) <- b if argVars.contains(l) && (true || n == n)) {
       s :+= ConsistencyError(s"$n is a reassignment of formal argument $l.", n.pos)
     }
     s

src/main/scala/viper/silver/ast/utility/Expressions.scala

@@ -41,6 +41,8 @@ object Expressions {
          | _: MultisetExp
          | _: MapExp
          | _: ForPerm
+         | _: Exists
+         | _: Forall
       => true
   }
 

src/main/scala/viper/silver/ast/utility/FileLoader.scala

@@ -0,0 +1,17 @@
+package viper.silver.ast.utility
+
+import java.nio.file.Path
+import scala.io.Source
+import scala.util.{Using, Try}
+
+trait FileLoader {
+  def loadContent(path: Path): Try[String]
+}
+
+trait DiskLoader extends FileLoader {
+  override def loadContent(path: Path): Try[String] = {
+    Using(Source.fromFile(path.toFile()))(_.mkString)
+  }
+}
+
+object DiskLoader extends DiskLoader