@@ -8,6 +8,7 @@ import java.nio.file.Path
88
99import fastparse .parsers .Combinators .Rule
1010import fastparse .WhitespaceApi
11+ import fastparse .parsers .{Intrinsics , Terminals }
1112/* import fastparse.core.{Parsed, Parser}*/
1213import fastparse .parsers .Intrinsics
1314import viper .silver .verifier .{ParseError , ParseReport , ParseWarning }
@@ -36,11 +37,12 @@ package object Main {
3637
3738 val White = WhitespaceApi .Wrapper {
3839 import fastparse .all ._
39- NoTrace (" " .rep)
40+
41+ NoTrace ( ( (" /*" ~ (AnyChar ~ ! StringIn (" */" )).rep ~ AnyChar ~ " */" ) | (" //" ~ CharsWhile ( _ != '\n ' ) ~ " \n " ) | " " | " \n " ).rep )
4042 }
4143
4244 import fastparse .noApi ._
43- // import fastparse.all._
45+ // import fastparse.all._
4446 import White ._
4547
4648
@@ -140,7 +142,7 @@ package object Main {
140142 else None
141143 }
142144 /** The file we are currently parsing (for creating positions later). */
143- def file : Path
145+ def file : Path = null
144146
145147 def expandDefines [N <: PNode ](defines : Seq [PDefine ], node : N ): N =
146148 doExpandDefines(defines, node).getOrElse(node)
@@ -195,7 +197,7 @@ package object Main {
195197
196198 lazy val atom : P [PExp ] = P (integer| booltrue| boolfalse| nul| old| applyOld
197199 | keyword(" result" ).map{_ => PResultLit ()} | (CharIn (" -!+" ).! ~ sum).map{case (a,b) => PUnExp (a,b)}
198- | " (" ~/ exp ~ " )" | accessPred | inhaleExhale | perm | let | quant | forperm | unfolding | folding | applying
200+ | " (" ~ exp ~ " )" | accessPred | inhaleExhale | perm | let | quant | forperm | unfolding | folding | applying
199201 | packaging | setTypedEmpty | explicitSetNonEmpty | explicitMultisetNonEmpty | multiSetTypedEmpty | seqTypedEmpty
200202 | seqLength | explicitSeqNonEmpty | seqRange | fapp | typedFapp | idnuse )
201203
@@ -215,8 +217,8 @@ package object Main {
215217 // possible customize error code in rule ident
216218 lazy val idnuse : P [PIdnUse ] = P (ident ).map(PIdnUse )
217219
218- lazy val old : P [PExp ] = P ((StringIn (" old" ) ~/ parens(exp)).map(POld ) | (" [" ~ idnuse ~ " ]" ~ parens(exp)).map{case (a,b) => PLabelledOld (a,b)} )
219- lazy val applyOld : P [PExp ] = P ((StringIn (" lhs" ) ~/ parens(exp)).map(PApplyOld ) )
220+ lazy val old : P [PExp ] = P ((StringIn (" old" ) ~ parens(exp)).map(POld ) | (" [" ~ idnuse ~ " ]" ~ parens(exp)).map{case (a,b) => PLabelledOld (a,b)} )
221+ lazy val applyOld : P [PExp ] = P ((StringIn (" lhs" ) ~ parens(exp)).map(PApplyOld ) )
220222 lazy val magicWandExp : P [PExp ] = P (realMagicWandExp | orExp)
221223 lazy val realMagicWandExp : P [PExp ] = P ((orExp ~ " --*" .! ~ magicWandExp).map{case (a,b,c) => PBinExp (a,b,c)})
222224 lazy val implExp : P [PExp ] = P ((magicWandExp ~ " ==>" .! ~ implExp).map{case (a,b,c) => PBinExp (a,b,c)} | magicWandExp)
@@ -250,7 +252,7 @@ package object Main {
250252 lazy val andExp : P [PExp ] = P ((eqExp ~ " &&" .! ~ andExp).map{case (a,b,c) => PBinExp (a,b,c)} | eqExp)
251253 lazy val orExp : P [PExp ] = P ((andExp ~ " ||" .! ~ orExp).map{case (a,b,c) => PBinExp (a,b,c)} | andExp )
252254
253- lazy val accessPred : P [PAccPred ] = P (StringIn (" acc" ) ~/ parens(locAcc ~ (" ," ~ exp).? ).map{case (loc , perms) => PAccPred (loc, perms.getOrElse(PFullPerm ()))})
255+ lazy val accessPred : P [PAccPred ] = P (StringIn (" acc" ) ~ parens(locAcc ~ (" ," ~ exp).? ).map{case (loc , perms) => PAccPred (loc, perms.getOrElse(PFullPerm ()))})
254256 lazy val locAcc : P [PLocationAccess ] = P (fieldAcc | predAcc)
255257 // this rule is in doubt :D
256258 lazy val fieldAcc : P [PFieldAccess ] = P (realSuffixExpr.filter(getFieldAccess).map{case fa : PFieldAccess => fa}).opaque(" Field Expected" )
@@ -526,7 +528,7 @@ package object Main {
526528 PMethod (name, args, rets.getOrElse(Nil ), pres, posts, PSeqn (Seq (PInhale (PBoolLit (b = false )))))
527529 }
528530 lazy val methodSignature = P (" method" ~ idndef ~ " (" ~ formalArgList ~ " )" ~ (" returns" ~ " (" ~ formalArgList ~ " )" ).? )
529- lazy val parser : P [ PProgram ] = P (programDecl)
531+ lazy val parser = P (programDecl)
530532
531533
532534
@@ -566,6 +568,6 @@ package object Main {
566568
567569
568570def main (args : Array [String ]) {
569- println(forperm .parse(" forperm [ ] hello::2*2 " ))
571+ println(parser .parse(" method helper(a:Int, b: Int) \n { \n assert a+b == (a + b) //Verifies \n \n } " ))
570572 }
571573}
0 commit comments