Add formatter for the parse AST

src/main/scala/viper/silver/ast/pretty/PrettyPrinter.scala

@@ -346,8 +346,7 @@ trait FastPrettyPrinterBase extends PrettyPrintPrimitives {
   def parens (d : Cont) : Cont =
     char ('(') <> d <> char (')')
 
-
-
+
   def brackets (d : Cont) : Cont =
     char ('[') <> d <> char (']')
 

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

@@ -35,7 +35,7 @@ object CfgTest {
   }
 
   private def parse(input: String, file: Path): Option[PProgram] = {
-    val program = new FastParser().parse(input, file)
+    val program = new FastParser().parse(input, file, false)
     if (program.errors.forall(_.isInstanceOf[ParseWarning])) Some(program)
     else None
   }

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

@@ -0,0 +1,26 @@
+// This Source Code Form is subject to the terms of the Mozilla Public
+// License, v. 2.0. If a copy of the MPL was not distributed with this
+// file, You can obtain one at http://mozilla.org/MPL/2.0/.
+//
+// Copyright (c) 2011-2024 ETH Zurich.
+
+package viper.silver.frontend
+import viper.silver.parser.PProgram
+import viper.silver.reporter.Reporter
+import viper.silver.verifier.{Failure, Success, VerificationResult}
+
+class ReformatterAstProvider(override val reporter: Reporter) extends ViperAstProvider(reporter) {
+  override val phases: Seq[Phase] = Seq(Parsing)
+
+  override def doParsing(input: String): Result[PProgram] = parsingInner(input, false)
+
+  override def result: VerificationResult = {
+    if (_errors.isEmpty) {
+      require(state >= DefaultStates.Parsing)
+      Success
+    }
+    else {
+      Failure(_errors)
+    }
+  }
+}

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

@@ -310,11 +310,11 @@ trait SilFrontend extends DefaultFrontend {
     _config = configureVerifier(args)
   }
 
-  override def doParsing(input: String): Result[PProgram] = {
+  def parsingInner(input: String, expandMacros: Boolean): Result[PProgram] = {
     val file = _inputFile.get
     plugins.beforeParse(input, isImported = false) match {
       case Some(inputPlugin) =>
-        val result = fp.parse(inputPlugin, file, Some(plugins), _loader)
+        val result = fp.parse(inputPlugin, file, expandMacros, Some(plugins), _loader)
         if (result.errors.forall(p => p.isInstanceOf[ParseWarning])) {
           reporter report WarningsDuringParsing(result.errors)
           Succ({
@@ -327,6 +327,8 @@ trait SilFrontend extends DefaultFrontend {
     }
   }
 
+  override def doParsing(input: String): Result[PProgram] = parsingInner(input, true)
+
   override def doSemanticAnalysis(input: PProgram): Result[PProgram] = {
     plugins.beforeResolve(input) match {
       case Some(inputPlugin) =>

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

@@ -104,6 +104,26 @@ object FastParserCompanion {
       ).pos
   }
 
+  def space[$: P]: P[PSpace] = P(("\t" | " ") map (_ => PSpace()))
+
+  def newline[$: P]: P[PNewLine] = P((StringIn("\n\r") | "\n" | "\r") map (_ => PNewLine()))
+
+  def lineComment[$: P]: P[PComment] = {
+    P(("//" ~~ CharsWhile(_ != '\n').?.!).map { content =>
+      PComment(content, false)
+    })
+  }
+
+  def blockComment[$: P]: P[PComment] = P(("/*" ~~ (!StringIn("*/") ~~ AnyChar).repX.! ~~ "*/").map { content =>
+    PComment(content, true)
+  })
+
+  def comment[$: P]: P[PComment] = lineComment | blockComment
+
+  def trivia[$: P]: P[Seq[PTrivia]] = {
+    P((space | newline | comment).repX)
+  }
+
   /**
     * A parser which matches leading whitespaces. See `LeadingWhitespace.lw` for more info. Can only be operated on in
     * restricted ways (e.g. `?`, `rep`, `|` or `map`), requiring that it is eventually appended to a normal parser (of type `P[V]`).
@@ -167,7 +187,7 @@ object FastParserCompanion {
 }
 
 class FastParser {
-  def parse(s: String, f: Path, plugins: Option[SilverPluginManager] = None, loader: FileLoader = DiskLoader) = {
+  def parse(s: String, f: Path, expandMacros: Boolean, plugins: Option[SilverPluginManager] = None, loader: FileLoader = DiskLoader) = {
     // Strategy to handle imports
     // Idea: Import every import reference and merge imported methods, functions, imports, .. into current program
     //       iterate until no new imports are present.
@@ -179,7 +199,11 @@ class FastParser {
     val file = f.toAbsolutePath().normalize()
     val data = ParserData(plugins, loader, mutable.HashSet(file))
     val program = RecParser(file, data, false).parses(s)
-    MacroExpander.expandDefines(program)
+    if (expandMacros) {
+      MacroExpander.expandDefines(program)
+    } else  {
+      program
+    }
   }
 
   case class ParserData(plugins: Option[SilverPluginManager], loader: FileLoader, local: mutable.HashSet[Path], std: mutable.HashSet[Path] = mutable.HashSet.empty)
@@ -859,7 +883,7 @@ class FastParser {
     P(programMember.rep map (members => {
       val warnings = _warnings
       _warnings = Seq()
-      PProgram(Nil, members)(_, warnings)
+      PProgram(Nil, members)(_, warnings, Nil, "")
     })).pos
 
   def preambleImport[$: P]: P[PKw.Import => PAnnotationsPosition => PImport] = P(
@@ -886,7 +910,7 @@ class FastParser {
       val axioms1 = members collect { case m: PAxiom1 => m }
       val funcs = funcs1 map (f => (PDomainFunction(f.annotations, f.unique, f.function, f.idndef, f.args, f.c, f.typ, f.interpretation)(f.pos), f.s))
       val axioms = axioms1 map (a => (PAxiom(a.annotations, a.axiom, a.idndef, a.exp)(a.pos), a.s))
-      val allMembers = block.update(PDomainMembers(PDelimited(funcs)(NoPosition, NoPosition), PDelimited(axioms)(NoPosition, NoPosition))(block.pos))
+      val allMembers = block.update(PDomainMembers(PDelimited(funcs)(NoPosition, NoPosition), PDelimited(axioms)(NoPosition, NoPosition))(block.pos, block.inner))
       k => ap: PAnnotationsPosition => PDomain(
         ap.annotations,
         k,
@@ -970,9 +994,14 @@ class FastParser {
 
     // Assume entire file is correct and try parsing it quickly
     fastparse.parse(s, entireProgram(_)) match {
-      case Parsed.Success(value, _) => return value
+      case Parsed.Success(value, _) => {
+        value.offsets = _line_offset;
+        value.rawProgram = s;
+        return value;
+      }
       case _: Parsed.Failure =>
     }
+
     // There was a parsing error, parse member by member to get all errors
     var startIndex = 0
     var members: Seq[PMember] = Nil
@@ -1018,7 +1047,7 @@ class FastParser {
     val warnings = _warnings
     _warnings = Nil
     val pos = (FilePosition(lineCol.getPos(0)), FilePosition(lineCol.getPos(res.get.index)))
-    PProgram(Nil, members)(pos, errors ++ warnings)
+    PProgram(Nil, members)(pos, errors ++ warnings, Nil, "");
   }
 
   object ParserExtension extends ParserPluginTemplate {

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

@@ -156,9 +156,9 @@ object MacroExpander {
                 pos._1
             }
           }
-          return PProgram(newImported, program.members)(program.pos, program.localErrors ++ reports :+ ParseError(msg, location))
+          return PProgram(newImported, program.members)(program.pos, program.localErrors ++ reports :+ ParseError(msg, location), program.offsets, program.rawProgram)
       }
-      PProgram(newImported, newMembers)(program.pos, program.localErrors ++ reports)
+      PProgram(newImported, newMembers)(program.pos, program.localErrors ++ reports, program.offsets, program.rawProgram)
     }
 
     doExpandDefinesAll(p, reports)