@@ -27,13 +27,26 @@ object FastParserCompanion {
2727 val whitespaceWithoutNewlineOrComments = {
2828 import NoWhitespace ._
2929 implicit ctx : ParsingRun [_] =>
30- NoTrace (( " " | " \t " ) .rep)
30+ NoTrace (space .rep)
3131 }
3232
33+ def blockComment [$ : P ] = {
34+ import NoWhitespace ._
35+ " /*" ~ (! StringIn (" */" ) ~ AnyChar ).rep ~ " */"
36+ }
37+
38+ def lineComment [$ : P ] = {
39+ import NoWhitespace ._
40+ " //" ~ CharsWhile (_ != '\n ' ).? ~ (" \n " | End )
41+ }
42+
43+ def space [$ : P ] = " " | " \t "
44+ def newline [$ : P ] = StringIn (" \r\n " ) | " \n " | " \r "
45+
3346 implicit val whitespace = {
3447 import NoWhitespace ._
3548 implicit ctx : ParsingRun [_] =>
36- NoTrace ((( " /* " ~ ( ! StringIn ( " */ " ) ~ AnyChar ).rep ~ " */ " ) | ( " // " ~ CharsWhile (_ != ' \n ' ). ? ~ ( " \n " | End )) | " " | " \t " | " \n " | " \r " ).rep)
49+ NoTrace ((blockComment | lineComment | space | newline ).rep)
3750 }
3851
3952 def identStarts [$ : P ] = CharIn (" A-Z" , " a-z" , " $_" )
@@ -95,15 +108,37 @@ object FastParserCompanion {
95108 .map { case (first, inner) => PDelimited (first, inner, None )(_) }
96109 ).pos
97110
98- def delimitedTrailing [$ : P , U ](sep : => P [U ], min : Int = 0 , max : Int = Int .MaxValue , exactly : Int = - 1 )(implicit lineCol : LineCol , _file : Path ): P [PDelimited [T , Option [ U ] ]] =
111+ def delimitedTrailing [$ : P , U , V ](sep : => P [U ], map : Option [ U ] => V = ( u : Option [ U ]) => u, min : Int = 0 , max : Int = Int .MaxValue , exactly : Int = - 1 )(implicit lineCol : LineCol , _file : Path ): P [PDelimited [T , V ]] =
99112 P ((p().lw ~~~ sep.lw.? ./ ).repX(min = min, max = max, exactly = exactly)
100113 .map(seq => {
101114 val (ts, us) = seq.unzip
102- PDelimited (ts.headOption, us.zip(ts.drop(1 )), us.lastOption)(_)
115+ val usm = us.map(map)
116+ PDelimited (ts.headOption, usm.zip(ts.drop(1 )), usm.lastOption)(_)
103117 })
104118 ).pos
105119 }
106120
121+ /* These special parser methods are only used in the reformatter
122+ to parse and interpret the whitespaces and comments between two AST nodes.
123+ */
124+ def pSpace [$ : P ]: P [PSpace ] = P (space map (_ => PSpace ()))
125+
126+ def pNewline [$ : P ]: P [PNewLine ] = P (newline map (_ => PNewLine ()))
127+
128+ def pLineComment [$ : P ]: P [PComment ] = P (lineComment.! .map { content =>
129+ PComment (content)
130+ })
131+
132+ def pBlockComment [$ : P ]: P [PComment ] = P (blockComment.! .map { content =>
133+ PComment (content)
134+ })
135+
136+ def pComment [$ : P ]: P [PComment ] = pLineComment | pBlockComment
137+
138+ def pTrivia [$ : P ]: P [Seq [PTrivia ]] = {
139+ P ((pSpace | pNewline | pComment).repX)
140+ }
141+
107142 /**
108143 * A parser which matches leading whitespaces. See `LeadingWhitespace.lw` for more info. Can only be operated on in
109144 * restricted ways (e.g. `?`, `rep`, `|` or `map`), requiring that it is eventually appended to a normal parser (of type `P[V]`).
@@ -167,7 +202,7 @@ object FastParserCompanion {
167202}
168203
169204class FastParser {
170- def parse (s : String , f : Path , plugins : Option [SilverPluginManager ] = None , loader : FileLoader = DiskLoader ) = {
205+ def parse (s : String , f : Path , plugins : Option [SilverPluginManager ] = None , loader : FileLoader = DiskLoader , expandMacros : Boolean = true ) = {
171206 // Strategy to handle imports
172207 // Idea: Import every import reference and merge imported methods, functions, imports, .. into current program
173208 // iterate until no new imports are present.
@@ -179,7 +214,11 @@ class FastParser {
179214 val file = f.toAbsolutePath().normalize()
180215 val data = ParserData (plugins, loader, mutable.HashSet (file))
181216 val program = RecParser (file, data, false ).parses(s)
182- MacroExpander .expandDefines(program)
217+ if (expandMacros) {
218+ MacroExpander .expandDefines(program)
219+ } else {
220+ program
221+ }
183222 }
184223
185224 case class ParserData (plugins : Option [SilverPluginManager ], loader : FileLoader , local : mutable.HashSet [Path ], std : mutable.HashSet [Path ] = mutable.HashSet .empty)
@@ -312,13 +351,13 @@ class FastParser {
312351 // ////////////////////////
313352
314353 import fastparse ._
315- import FastParserCompanion .{ExtendedParsing , identContinues , identStarts , LeadingWhitespace , Pos , PositionParsing , reservedKw , reservedSym }
354+ import FastParserCompanion .{ExtendedParsing , identContinues , identStarts , LeadingWhitespace , Pos , PositionParsing , reservedKw , reservedSym , blockComment , lineComment , newline , space }
316355
317356
318357 implicit val whitespace = {
319358 import NoWhitespace ._
320359 implicit ctx : ParsingRun [_] =>
321- NoTrace ((( " /* " ~ ( ! StringIn ( " */ " ) ~ AnyChar ).rep ~ " */ " ) | ( " // " ~ CharsWhile (_ != ' \n ' ). ? ~ ( " \n " | End )) | " " | " \t " | " \n " | " \r " ).rep)
360+ NoTrace ((blockComment | lineComment | space | newline ).rep)
322361 }
323362
324363 implicit val lineCol : LineCol = new LineCol (this )
@@ -357,7 +396,7 @@ class FastParser {
357396 def typeList [$ : P , T ](p : => P [T ]) = p.delimited(PSym .Comma ).brackets
358397
359398 /** ...`;`? ...`;`? ...`;`? */
360- def semiSeparated [$ : P , T ](p : => P [T ]) = p.delimitedTrailing(PSym .Semi )
399+ def semiSeparated [$ : P , T ](p : => P [T ]): P [ PDelimited [ T , PSym . OptionSemi ]] = p.delimitedTrailing(PSym .Semi , map = ND .apply )
361400
362401 def foldPExp [E <: PExp ](e : E , es : Seq [SuffixedExpressionGenerator [E ]]): E =
363402 es.foldLeft(e) { (t, a) => a(t) }
@@ -426,7 +465,7 @@ class FastParser {
426465
427466 def ident [$ : P ]: P [String ] = identifier.! .filter(a => ! keywords.contains(a)).opaque(" identifier" )
428467
429- def idnuse [$ : P ]: P [PIdnUseExp ] = P (ident map (PIdnUseExp .apply _)).pos
468+ def idnuse [$ : P ]: P [PIdnUseExp ] = P (idnref[$, PTypedVarDecl ] map (PIdnUseExp .apply _))
430469
431470 def idnref [$ : P , T <: PDeclarationInner ](implicit ctag : scala.reflect.ClassTag [T ]): P [PIdnRef [T ]] = P (ident map (PIdnRef .apply[T ] _)).pos
432471
@@ -640,7 +679,7 @@ class FastParser {
640679 def trigger [$ : P ]: P [PTrigger ] = P (exp.delimited(PSym .Comma ).braces map (PTrigger .apply _)).pos
641680
642681 def forperm [$ : P ]: P [PKw .Forperm => Pos => PExp ] = P (nonEmptyIdnTypeList(PLogicalVarDecl (_)) ~ resAcc.brackets ~ PSym .ColonColon ~ exp).map {
643- case (args, res, op, body) => PForPerm (_, args, res, op, body)
682+ case (args, res, op, body) => PForPerm (_, args, PPermTrigger ( res) , op, body)
644683 }
645684
646685 def unfolding [$ : P ]: P [PKwOp .Unfolding => Pos => PExp ] = P (predicateAccessAssertion ~ PKwOp .In ~ exp).map {
@@ -767,7 +806,7 @@ class FastParser {
767806 // delimited sequence of field access, function application or identifier)
768807 def assign [$ : P ]: P [PAssign ] = P (
769808 (assignTarget.delimited(PSym .Comma , min = 1 ) ~~~ (P (PSymOp .Assign ).map(Some (_)) ~ exp).lw.? )
770- filter (a => a._2.isDefined || (a._1.length == 1 && ( a._1.head.isInstanceOf [PIdnUse ] || a._1.head. isInstanceOf [ PCall ]) ))
809+ filter (a => a._2.isDefined || (a._1.length == 1 && ! a._1.head.isInstanceOf [PFieldAccess ] ))
771810 map (a => if (a._2.isDefined) PAssign (a._1, a._2.get._1, a._2.get._2) _ else PAssign (PDelimited .empty, None , a._1.head) _)
772811 ).pos
773812
@@ -812,7 +851,7 @@ class FastParser {
812851 P ((P (PKw .Else ) ~ stmtBlock()) map (PElse .apply _).tupled).pos
813852
814853 def whileStmt [$ : P ]: P [PKw .While => Pos => PWhile ] =
815- P ((parenthesizedExp ~~ semiSeparated (invariant) ~ stmtBlock()) map { case (cond, invs, body) => PWhile (_, cond, invs, body) })
854+ P ((parenthesizedExp ~~ specifications (invariant) ~ stmtBlock()) map { case (cond, invs, body) => PWhile (_, cond, invs, body) })
816855
817856 def invariant (implicit ctx : P [_]) : P [PSpecification [PKw .InvSpec ]] = P ((P (PKw .Invariant ) ~ exp).map((PSpecification .apply _).tupled).pos | ParserExtension .invSpecification(ctx))
818857
@@ -821,7 +860,7 @@ class FastParser {
821860
822861 def defineDecl [$ : P ]: P [PKw .Define => PAnnotationsPosition => PDefine ] =
823862 P ((idndef ~~~/ NoCut (argList((idndef map PDefineParam .apply).pos)).lw.? ~ (stmtBlock(false ) | exp)) map {
824- case (idn, args, body) => k => ap : PAnnotationsPosition => PDefine (ap.annotations, k, idn, args, body)(ap.pos)
863+ case (idn, args, body) => k => ap : PAnnotationsPosition => PDefine (ap.annotations, k, idn, args, PDefineInner ( body) )(ap.pos)
825864 })
826865
827866 def defineDeclStmt [$ : P ]: P [PKw .Define => Pos => PDefine ] = P (defineDecl.map { f => k => pos : Pos => f(k)(PAnnotationsPosition (Nil , pos)) })
@@ -859,7 +898,7 @@ class FastParser {
859898 P (programMember.rep map (members => {
860899 val warnings = _warnings
861900 _warnings = Seq ()
862- PProgram (Nil , members)(_, warnings)
901+ PProgram (Nil , members)(_, warnings, Nil , " " )
863902 })).pos
864903
865904 def preambleImport [$ : P ]: P [PKw .Import => PAnnotationsPosition => PImport ] = P (
@@ -879,28 +918,22 @@ class FastParser {
879918 P ((P (PKw .Interpretation ) ~ argList(domainInterp)) map (PDomainInterpretations .apply _).tupled).pos
880919
881920 def domainDecl [$ : P ]: P [PKw .Domain => PAnnotationsPosition => PDomain ] = P (idndef ~~~ typeList(domainTypeVarDecl).lw.? ~~~ domainInterps.lw.? ~
882- annotated(domainFunctionDecl | axiomDecl).rep.map( PDomainMembers1 .apply _).pos .braces).map {
921+ semiSeparated( annotated(domainFunctionDecl | axiomDecl)) .braces).map {
883922 case (name, typparams, interpretations, block) =>
884- val members = block.inner.members
885- val funcs1 = members collect { case m : PDomainFunction1 => m }
886- val axioms1 = members collect { case m : PAxiom1 => m }
887- 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))
888- val axioms = axioms1 map (a => (PAxiom (a.annotations, a.axiom, a.idndef, a.exp)(a.pos), a.s))
889- val allMembers = block.update(PDomainMembers (PDelimited (funcs)(NoPosition , NoPosition ), PDelimited (axioms)(NoPosition , NoPosition ))(block.pos))
890923 k => ap : PAnnotationsPosition => PDomain (
891924 ap.annotations,
892925 k,
893926 name,
894927 typparams,
895928 interpretations,
896- allMembers )(ap.pos)
929+ block )(ap.pos)
897930 }
898931
899932 def domainTypeVarDecl [$ : P ]: P [PTypeVarDecl ] = P (idndef map (PTypeVarDecl .apply _)).pos
900933
901934 def domainFunctionInterpretation [$ : P ]: P [PDomainFunctionInterpretation ] = P ((P (PKw .Interpretation ) ~ stringLiteral) map (PDomainFunctionInterpretation .apply _).tupled).pos
902- def domainFunctionDecl [$ : P ]: P [PAnnotationsPosition => PDomainFunction1 ] = P (P (PKw .Unique ).? ~ domainFunctionSignature ~ domainFunctionInterpretation. ? ~~~ P ( PSym . Semi ).lw .? ).map {
903- case (unique, (function, idn, args, c, typ), interpretation, s ) => ap : PAnnotationsPosition => PDomainFunction1 (ap.annotations, unique, function, idn, args, c, typ, interpretation, s )(ap.pos)
935+ def domainFunctionDecl [$ : P ]: P [PAnnotationsPosition => PDomainFunction ] = P (P (PKw .Unique ).? ~ domainFunctionSignature ~ domainFunctionInterpretation.? ).map {
936+ case (unique, (function, idn, args, c, typ), interpretation) => ap : PAnnotationsPosition => PDomainFunction (ap.annotations, unique, function, idn, args, c, typ, interpretation)(ap.pos)
904937 }
905938
906939 def domainFunctionSignature [$ : P ] = P (P (PKw .FunctionD ) ~ idndef ~ argList(domainFunctionArg) ~ PSym .Colon ~ typ)
@@ -911,20 +944,21 @@ class FastParser {
911944
912945 def bracedExp [$ : P ]: P [PBracedExp ] = P (exp.braces map (PBracedExp (_) _)).pos
913946
914- def axiomDecl [$ : P ]: P [PAnnotationsPosition => PAxiom1 ] = P (P (PKw .Axiom ) ~ idndef.? ~ bracedExp ~~~ P ( PSym . Semi ).lw. ? ). map { case (k, a, b, s ) =>
915- ap : PAnnotationsPosition => PAxiom1 (ap.annotations, k, a, b, s )(ap.pos)
947+ def axiomDecl [$ : P ]: P [PAnnotationsPosition => PAxiom ] = P (P (PKw .Axiom ) ~ idndef.? ~ bracedExp). map { case (k, a, b) =>
948+ ap : PAnnotationsPosition => PAxiom (ap.annotations, k, a, b)(ap.pos)
916949 }
917950
918951 def fieldDecl [$ : P ]: P [PKw .Field => PAnnotationsPosition => PFields ] = P ((nonEmptyIdnTypeList(PFieldDecl (_)) ~~~ P (PSym .Semi ).lw.? ) map {
919952 case (a, s) => k => ap : PAnnotationsPosition => PFields (ap.annotations, k, a, s)(ap.pos)
920953 })
921954
922955 def functionDecl [$ : P ]: P [PKw .Function => PAnnotationsPosition => PFunction ] = P ((idndef ~ argList(formalArg) ~ PSym .Colon ~ typ
923- ~~ semiSeparated (precondition) ~~ semiSeparated (postcondition) ~~~ bracedExp.lw.?
956+ ~~ specifications (precondition) ~~ specifications (postcondition) ~~~ bracedExp.lw.?
924957 ) map { case (idn, args, c, typ, d, e, f) => k =>
925958 ap : PAnnotationsPosition => PFunction (ap.annotations, k, idn, args, c, typ, d, e, f)(ap.pos)
926959 })
927960
961+ def specifications [$ : P , T <: PKw .Spec ](kw : => P [PSpecification [T ]]): P [PSpecs [T ]] = P (semiSeparated(kw) map (PSpecs .apply _)).pos
928962
929963 def precondition (implicit ctx : P [_]) : P [PSpecification [PKw .PreSpec ]] = P ((P (PKw .Requires ) ~ exp).map((PSpecification .apply _).tupled).pos | ParserExtension .preSpecification(ctx))
930964
@@ -936,7 +970,7 @@ class FastParser {
936970 }
937971
938972 def methodDecl [$ : P ]: P [PKw .Method => PAnnotationsPosition => PMethod ] =
939- P ((idndef ~ argList(formalArg) ~~~ methodReturns.lw.? ~~ semiSeparated (precondition) ~~ semiSeparated (postcondition) ~~~ stmtBlock().lw.? ) map {
973+ P ((idndef ~ argList(formalArg) ~~~ methodReturns.lw.? ~~ specifications (precondition) ~~ specifications (postcondition) ~~~ stmtBlock().lw.? ) map {
940974 case (idn, args, rets, pres, posts, body) => k =>
941975 ap : PAnnotationsPosition => PMethod (ap.annotations, k, idn, args, rets, pres, posts, body)(ap.pos)
942976 })
@@ -970,7 +1004,11 @@ class FastParser {
9701004
9711005 // Assume entire file is correct and try parsing it quickly
9721006 fastparse.parse(s, entireProgram(_)) match {
973- case Parsed .Success (value, _) => return value
1007+ case Parsed .Success (value, _) => {
1008+ value.offsets = _line_offset;
1009+ value.rawProgram = s;
1010+ return value;
1011+ }
9741012 case _ : Parsed .Failure =>
9751013 }
9761014 // There was a parsing error, parse member by member to get all errors
@@ -1018,7 +1056,7 @@ class FastParser {
10181056 val warnings = _warnings
10191057 _warnings = Nil
10201058 val pos = (FilePosition (lineCol.getPos(0 )), FilePosition (lineCol.getPos(res.get.index)))
1021- PProgram (Nil , members)(pos, errors ++ warnings)
1059+ PProgram (Nil , members)(pos, errors ++ warnings, Nil , " " );
10221060 }
10231061
10241062 object ParserExtension extends ParserPluginTemplate {
0 commit comments