Improve language flexibility (#685)

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

@@ -85,7 +85,7 @@ case class MethodCall(methodName: String, args: Seq[Exp], targets: Seq[LocalVar]
     if(!Consistency.noResult(this))
       s :+= ConsistencyError("Result variables are only allowed in postconditions of functions.", pos)
     if (!Consistency.noDuplicates(targets))
-      s :+= ConsistencyError("Targets are not allowed to have duplicates", targets.head.pos)
+      s :+= ConsistencyError("Targets are not allowed to have duplicates", pos)
     s ++= args.flatMap(Consistency.checkPure)
     s
   }

src/main/scala/viper/silver/ast/utility/rewriter/Rewritable.scala

@@ -6,7 +6,7 @@
 
 package viper.silver.ast.utility.rewriter
 
-import viper.silver.parser.{PDomain, PDomainFunction, PField, PFunction, PMethod, PPredicate}
+import viper.silver.parser.{PDomain, PDomainFunction, PFields, PFunction, PMethod, PPredicate}
 import viper.silver.parser.Transformer.ParseTreeDuplicationError
 import viper.silver.ast.{AtomicType, BackendFuncApp, DomainFuncApp, ErrorTrafo, FuncApp, Info, Node, Position}
 
@@ -56,7 +56,7 @@ trait Rewritable extends Product {
           case pm: PMethod => secondArgList = Seq(pos.getOrElse(pm.pos), pm.annotations)
           case pp: PPredicate => secondArgList = Seq(pos.getOrElse(pp.pos), pp.annotations)
           case pf: PFunction => secondArgList = Seq(pos.getOrElse(pf.pos), pf.annotations)
-          case pf: PField => secondArgList = Seq(pos.getOrElse(pf.pos), pf.annotations)
+          case pf: PFields => secondArgList = Seq(pos.getOrElse(pf.pos), pf.annotations)
           case pn: PNode => secondArgList = Seq(pos.getOrElse(pn.pos))
           case _ =>
         }

src/main/scala/viper/silver/cfg/CfgTest.scala

@@ -8,7 +8,6 @@ package viper.silver.cfg
 
 import java.nio.file.{Files, Path, Paths}
 
-import fastparse._
 import viper.silver.parser.{FastParser, PProgram, Resolver, Translator}
 import viper.silver.verifier.ParseWarning
 
@@ -36,12 +35,8 @@ object CfgTest {
   }
 
   private def parse(input: String, file: Path): Option[PProgram] = {
-    val result = new FastParser().parse(input, file)
-    result match {
-      case Parsed.Success(program@PProgram(_, _, _, _, _, _, _,_, errors), _) =>
-        if (errors.isEmpty || errors.forall(_.isInstanceOf[ParseWarning])) Some(program)
-        else None
-      case _ => None
-    }
+    val program = new FastParser().parse(input, file)
+    if (program.errors.forall(_.isInstanceOf[ParseWarning])) Some(program)
+    else None
   }
 }

src/main/scala/viper/silver/frontend/SilFrontend.scala

@@ -7,13 +7,12 @@
 package viper.silver.frontend
 
 import viper.silver.ast.utility.Consistency
-import viper.silver.ast.{SourcePosition, _}
+import viper.silver.ast._
 import viper.silver.parser._
 import viper.silver.plugin.SilverPluginManager
 import viper.silver.plugin.SilverPluginManager.PluginException
 import viper.silver.reporter._
 import viper.silver.verifier._
-import fastparse.Parsed
 import java.nio.file.{Path, Paths}
 import viper.silver.FastMessaging
 
@@ -247,7 +246,8 @@ trait SilFrontend extends DefaultFrontend {
   }
 
   def finish(): Unit = {
-    val res = plugins.beforeFinish(result)
+    val tRes = result.transformedResult()
+    val res = plugins.beforeFinish(tRes)
     _verificationResult = Some(res)
     res match {
       case Success =>
@@ -266,22 +266,11 @@ trait SilFrontend extends DefaultFrontend {
     plugins.beforeParse(input, isImported = false) match {
       case Some(inputPlugin) =>
         val result = fp.parse(inputPlugin, file, Some(plugins))
-          result match {
-            case Parsed.Success(e@ PProgram(_, _, _, _, _, _, _, _, err_list), _) =>
-              if (err_list.isEmpty || err_list.forall(p => p.isInstanceOf[ParseWarning])) {
-                reporter report WarningsDuringParsing(err_list)
-                Succ({e.initProperties(); e})
-              }
-              else Fail(err_list)
-            case fail @ Parsed.Failure(_, index, _) =>
-              val msg = fail.trace().aggregateMsg
-              val (line, col) = fp.lineCol.getPos(index)
-              Fail(List(ParseError(msg, SourcePosition(file, line, col))))
-            //? val pos = extra.input.prettyIndex(index).split(":").map(_.toInt)
-              //? Fail(List(ParseError(s"Expected $msg", SourcePosition(file, pos(0), pos(1)))))
-            case error: ParseError => Fail(List(error))
-          }
-
+        if (result.errors.forall(p => p.isInstanceOf[ParseWarning])) {
+          reporter report WarningsDuringParsing(result.errors)
+          Succ({result.initProperties(); result})
+        }
+        else Fail(result.errors)
       case None => Fail(plugins.errors)
     }
   }

src/main/scala/viper/silver/parser/FastMessage.scala

@@ -53,12 +53,12 @@ object FastMessaging {
    /**
     * Makes a message list if cond is true. Stored with the position of the value
     */
-  def message (value : Any, msg : String, cond : Boolean = true, error : Boolean = true) : Messages =
+  def message (value : PNode, msg : String, cond : Boolean = true, error : Boolean = true) : Messages =
     if (cond) {
       // Warning: Potential scala.MatchError here if position info is lost!
-      val valuePos: SourcePosition = value.asInstanceOf[PNode].pos._1 match {
+      val valuePos: SourcePosition = value.pos._1 match {
         case slc: FilePosition => {
-          value.asInstanceOf[PNode].pos._2 match {
+          value.pos._2 match {
             case flc: HasLineColumn => {
               SourcePosition(slc.file, slc, flc)
             }