diff options
Diffstat (limited to 'Chalice/src/main/scala/Parser.scala')
| -rw-r--r-- | Chalice/src/main/scala/Parser.scala | 645 |
1 files changed, 0 insertions, 645 deletions
diff --git a/Chalice/src/main/scala/Parser.scala b/Chalice/src/main/scala/Parser.scala deleted file mode 100644 index 9a4cd272..00000000 --- a/Chalice/src/main/scala/Parser.scala +++ /dev/null @@ -1,645 +0,0 @@ -//-----------------------------------------------------------------------------
-//
-// Copyright (C) Microsoft Corporation. All Rights Reserved.
-//
-//-----------------------------------------------------------------------------
-package chalice;
-import scala.util.parsing.combinator.syntactical.StandardTokenParsers
-import scala.util.parsing.combinator.lexical.StdLexical
-import scala.util.parsing.combinator._
-import scala.util.parsing.input.PagedSeqReader
-import scala.collection.immutable.PagedSeq
-import scala.util.parsing.input.Position
-import scala.util.parsing.input.Positional
-import scala.util.parsing.input.NoPosition
-import java.io.File
-
-class Parser extends StandardTokenParsers {
-
- def parseStdin = phrase(programUnit)(new lexical.Scanner(new PagedSeqReader(PagedSeq fromReader Console.in)))
- def parseFile(file: File) = phrase(programUnit)(new lexical.Scanner(new PagedSeqReader(PagedSeq fromFile file)))
-
- case class PositionedString(v: String) extends Positional
-
- // handle comments already in lexer
- override val lexical = new StdLexical {
- def rp: RegexParsers = new RegexParsers {}
- override val whitespace: Parser[Any] = rp.regex("""(\s|//.*|(?m)/\*(\*(?!/)|[^*])*\*/)*""".r).asInstanceOf[Parser[Any]]
- }
-
- lexical.reserved += ("class", "ghost", "var", "const", "method", "channel", "condition",
- "assert", "assume", "new", "this", "reorder",
- "between", "and", "above", "below", "share", "unshare", "acquire", "release", "downgrade",
- "lock", "fork", "join", "rd", "acc", "credit", "holds", "old", "assigned",
- "call", "if", "else", "while", "invariant", "lockchange",
- "returns", "requires", "ensures", "where", "static",
- "int", "bool", "false", "true", "null", "string", "waitlevel", "lockbottom",
- "module", "external",
- "predicate", "function", "free", "send", "receive",
- "ite", "fold", "unfold", "unfolding", "in", "forall", "exists",
- "seq", "nil", "result", "eval", "token",
- "wait", "signal", "unlimited",
- "refines", "transforms", "replaces", "by", "spec", "_", "*"
- )
- // todo: can we remove "nil"?
- lexical.delimiters += ("(", ")", "{", "}", "[[", "]]",
- "<==>", "==>", "&&", "||",
- "==", "!=", "<", "<=", ">=", ">", "<<", "in", "!in",
- "+", "-", "*", "/", "%", "!", ".", "..",
- ";", ":", ":=", ",", "?", "|", "[", "]", "++", "::"
- )
-
- def programUnit = (classDecl | channelDecl)*
- def Semi = ";" ?
- var currentLocalVariables = Set[String]() // used in the method context
- var assumeAllLocals = false;
- var insidePermission = false;
-
- /**
- * Top level declarations
- */
-
- def classDecl =
- positioned(("external" ?) ~ ("class" ~> ident) ~ opt("module" ~> ident) ~ opt("refines" ~> ident) ~
- ("{" ~> (memberDecl*) <~ "}") ^^ {
- case ext ~ id ~ module ~ refines ~ members =>
- val cl = Class(id, Nil, module.getOrElse("default"), members)
- if (ext.isDefined) cl.IsExternal = true
- if (refines.isDefined) {cl.IsRefinement = true; cl.refinesId = refines.get}
- cl
- })
- def channelDecl =
- positioned("channel" ~> ident ~ formalParameters(true) ~ ("where" ~> expression ?) <~ Semi ^^ {
- case id ~ ins ~ None => Channel(id, ins, BoolLiteral(true))
- case id ~ ins ~ Some(e) => Channel(id, ins, e)
- })
-
- /**
- * Member declarations
- */
-
- def memberDecl = {
- positioned(fieldDecl | invariantDecl | methodDecl | conditionDecl | predicateDecl | functionDecl | couplingDecl | transformDecl) // important that last one is transformDecl
- }
- def fieldDecl = {
- currentLocalVariables = Set[String]();
- ( "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id.v, t, false) }
- | "ghost" ~> "var" ~> idType <~ Semi ^^ { case (id,t) => Field(id.v, t, true) }
- )
- }
- def invariantDecl = {
- currentLocalVariables = Set[String]();
- "invariant" ~> expression <~ Semi ^^ MonitorInvariant
- }
- def methodDecl = {
- currentLocalVariables = Set[String]();
- "method" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~
- (methodSpec*) ~ blockStatement ^^ {
- case id ~ ins ~ outs ~ spec ~ body =>
- Method(id, ins, outs match {case None => Nil; case Some(outs) => outs}, spec, body)
- }
- }
- def predicateDecl: Parser[Predicate] = {
- currentLocalVariables = Set[String]();
- ("predicate" ~> ident) ~ ("{" ~> expression <~ "}") ^^ { case id ~ definition => Predicate(id, definition) }
- }
- def functionDecl = {
- currentLocalVariables = Set[String]();
- ("unlimited" ?) ~ ("static" ?) ~ ("function" ~> ident) ~ formalParameters(true) ~ (":" ~> typeDecl) ~ (methodSpec*) ~ opt("{" ~> expression <~ "}") ^^ {
- case u ~ s ~ id ~ ins ~ out ~ specs ~ body => {
- val f = Function(id, ins, out, specs, body);
- if (u.isDefined) f.isUnlimited = true;
- if (s.isDefined) f.isStatic = true;
- f
- }
- }
- }
- def conditionDecl = {
- currentLocalVariables = Set[String]();
- "condition" ~> ident ~ ("where" ~> expression ?) <~ Semi ^^ {
- case id ~ optE => Condition(id, optE) }
- }
- def transformDecl = {
- currentLocalVariables = Set[String]();
- ( "refines" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~ (methodSpec*) ~ blockStatement ^^ {
- case id ~ ins ~outs ~ spec ~ body =>
- MethodTransform(id, ins, outs match {case None => Nil; case Some(outs) => outs}, spec, ProgramPat(body)) }).|(
- "transforms" ~> ident ~ formalParameters(true) ~ ("returns" ~> formalParameters(false) ?) ~ (methodSpec*) into {case id ~ ins ~ outs ~ spec =>
- assumeAllLocals = true;
- "{" ~> transform <~ "}" ^^ {
- trans =>
- assumeAllLocals = false;
- MethodTransform(id, ins, outs match {case None => Nil; case Some(outs) => outs}, spec, AST.normalize(trans))
- }
- })
- }
- def couplingDecl = {
- currentLocalVariables = Set[String]();
- ("replaces" ~> rep1sep(ident, ",") <~ "by") ~ expression <~ Semi ^^ {case ids ~ e => CouplingInvariant(ids, e)}
- }
-
- def formalParameters(immutable: Boolean) =
- "(" ~> (formalList(immutable) ?) <~ ")" ^^ {
- case None => Nil
- case Some(ids) => ids }
- def formalList(immutable: Boolean) = repsep(formal(immutable), ",")
- def formal(immutable: Boolean): Parser[Variable] =
- idType ^^ {case (id,t) =>
- currentLocalVariables = currentLocalVariables + id.v;
- new Variable(id.v,t,false,immutable)
- }
- def Ident = positioned(ident ^^ PositionedString)
- def idType = idTypeOpt ^^ {
- case (id, None) => (id, Type("int", Nil)) // todo: this feature was once convenient to make some Chalice programs look cleaner, but now that Chalice has grown up a bit, it's a feature that is better removed (or replaced by some type inference)
- case (id, Some(t)) => (id, t) }
- def idTypeOpt =
- Ident ~ (":" ~> typeDecl ?) ^^ { case id ~ optT => (id, optT) }
- def typeDecl: Parser[Type] =
- positioned(("int" | "bool" | ident | "string" | "seq") ~ opt("<" ~> repsep(typeDecl, ",") <~ ">") ^^ { case t ~ parameters => Type(t, parameters.getOrElse(Nil)) }
- | ("token" ~ "<") ~> (typeDecl <~ ".") ~ ident <~ ">" ^^ { case c ~ m => TokenType(c, m) }
- )
-
- /**
- * Pre and post conditions
- */
-
- def methodSpec =
- positioned( "requires" ~> expression <~ Semi ^^ Precondition
- | "ensures" ~> expression <~ Semi ^^ Postcondition
- | "lockchange" ~> expressionList <~ Semi ^^ LockChange
- )
-
- /**
- * Statements
- */
-
- def blockStatement: Parser[List[Statement]] = "{" ~> blockStatementBody <~ "}"
- def blockStatementBody: Parser[List[Statement]] = {
- val prev = currentLocalVariables
- (statement*) ^^ {
- case x => currentLocalVariables = prev; x }
- }
- def statement: Parser[Statement] =
- positioned( "assert" ~> expression <~ Semi ^^ Assert
- | "assume" ~> expression <~ Semi ^^ Assume
- | blockStatement ^^ BlockStmt
- | "var" ~> localVarStmt(false, false)
- | "spec" ~> localVarStmt(false, false)
- | "const" ~> localVarStmt(true, false)
- | "ghost" ~> "const" ~> localVarStmt(true, true)
- | "ghost" ~> "var" ~> localVarStmt(false, true)
- | "call" ~> callStmt
- | "if" ~> ifStmtThen
- | "while" ~> "(" ~> expression ~ ")" ~ loopSpec ~ blockStatement ^^ {
- case guard ~ _ ~ lSpec ~ body =>
- lSpec match { case (invs,lkch) => WhileStmt(guard, invs, Nil, lkch, BlockStmt(body)) }}
- | "reorder" ~> expression ~ (installBounds ?) <~ Semi ^^ {
- case obj ~ None => Install(obj, List(), List())
- case obj ~ Some(bounds) => Install(obj, bounds._1, bounds._2) }
- | "share" ~> expression ~ (installBounds ?) <~ Semi ^^ {
- case obj ~ None => Share(obj, List(), List())
- case obj ~ Some(bounds) => Share(obj, bounds._1, bounds._2) }
- | "unshare" ~> expression <~ Semi ^^ Unshare
- | "acquire" ~> expression <~ Semi ^^ Acquire
- | "release" ~> expression <~ Semi ^^ Release
- | "lock" ~> "(" ~> expression ~ ")" ~ blockStatement ^^ {
- case e ~ _ ~ b => Lock(e, BlockStmt(b), false) }
- | "[[" ~> blockStatementBody <~ "]]" ^^ {
- case b => Lock(ExplicitThisExpr(), BlockStmt(b), false) }
- | "rd" ~>
- ( "lock" ~> "(" ~> expression ~ ")" ~ blockStatement ^^ {
- case e ~ _ ~ b => Lock(e, BlockStmt(b), true) }
- | "acquire" ~> expression <~ Semi ^^ RdAcquire
- | "release" ~> expression <~ Semi ^^ RdRelease
- )
- | "downgrade" ~> expression <~ Semi ^^ Downgrade
- | "free" ~> expression <~ Semi ^^ Free
- | Ident ~ ":=" ~ Rhs <~ Semi ^^ {
- case lhs ~ _ ~ rhs =>
- if ((currentLocalVariables contains lhs.v) || assumeAllLocals) {
- val varExpr = VariableExpr(lhs.v); varExpr.pos = lhs.pos;
- Assign(varExpr, rhs)
- } else {
- val implicitThis = ImplicitThisExpr();
- val select = MemberAccess(implicitThis, lhs.v);
- implicitThis.pos = lhs.pos;
- select.pos = lhs.pos;
- FieldUpdate(select, rhs)
- }}
- | selectExprFerSure ~ ":=" ~ Rhs <~ Semi ^^ {
- case lhs ~ _ ~ rhs => FieldUpdate(lhs, rhs) }
- | ("fold" ~> expression <~ Semi) ^? {
- case pred: MemberAccess => Fold(Access(pred, Full))
- case perm: Access => Fold(perm)
- }
- | ("unfold" ~> expression <~ Semi) ^? {
- case pred: MemberAccess => Unfold(Access(pred, Full))
- case perm: Access => Unfold(perm)
- }
- | ("fork") ~> callSignature ^? ({
- case None ~ target ~ args =>
- val (receiver, name) = target match {
- case VariableExpr(id) => (new ImplicitThisExpr, id)
- case MemberAccess(obj, id) => (obj, id)
- }
- CallAsync(false, null, receiver, name, args)
- case Some(List(tok)) ~ target ~ args =>
- val (receiver, name) = target match {
- case VariableExpr(id) => (new ImplicitThisExpr, id)
- case MemberAccess(obj, id) => (obj, id)
- }
- if (currentLocalVariables contains tok.id) {
- CallAsync(false, tok, receiver, name, args)
- } else {
- currentLocalVariables = currentLocalVariables + tok.id;
- CallAsync(true, tok, receiver, name, args)
- }
- }, t => "fork statement cannot take more than 1 left-hand side")
- | (("join") ~> ( identList <~ ":=" ?)) ~ expression <~ Semi ^^
- { case results ~ token => JoinAsync(ExtractList(results), token) }
- | "wait" ~> memberAccess <~ Semi ^^ {
- case MemberAccess(obj, id) => Wait(obj, id) }
- | "signal" ~> ("forall" ?) ~ memberAccess <~ Semi ^^ {
- case None ~ MemberAccess(obj, id) => Signal(obj, id, false)
- case _ ~ MemberAccess(obj, id) => Signal(obj, id, true) }
- | ("send" ~> suffixPlusExpr into { e => e match {
- case FunctionApplication(obj, name, args) => Semi ^^^ Send(MemberAccess(obj,name), args)
- case e => "(" ~> expressionList <~ ")" <~ Semi ^^ { case args => Send(e, args) }}})
- | ("send" ~> atom into { e => e match {
- case fa@FunctionApplication(ImplicitThisExpr(), name, args) => Semi ^^^ {val va = VariableExpr(name); va.pos = fa.pos; Send(va, args)}
- case e => "(" ~> expressionList <~ ")" <~ Semi ^^ { case args => Send(e, args) }}})
- | "receive" ~> (identList <~ ":=" ?) ~ expression <~ Semi ^^ {
- case outs ~ e =>
- val lhs = ExtractList(outs)
- Receive(declareImplicitLocals(lhs), e, lhs) }
- )
- // this could be slightly changed to make it LL(1)
- def localVarStmt(const: Boolean, ghost: Boolean) =
- ( (rep1sep(idType, ",") into {decls:List[(PositionedString,Type)] => {
- val locals = for ((id, t) <- decls; if (! currentLocalVariables.contains(id.v))) yield {
- currentLocalVariables = currentLocalVariables + id.v
- new Variable(id.v, t, ghost, const)
- }
- val lhs = for ((id, _) <- decls) yield {
- val v = VariableExpr(id.v); v.pos = id.pos; v
- }
- "[" ~> opt(expression <~ ",") ~ expression <~ "]" <~ Semi ^^ {
- case Some(pre) ~ post => SpecStmt(lhs, locals, pre, post)
- case None ~ post => SpecStmt(lhs, locals, BoolLiteral(true), post)
- };
- } })
- | idTypeOpt ~ (":=" ~> Rhs ?) <~ Semi ^^ {
- case (id,optT) ~ rhs =>
- currentLocalVariables = currentLocalVariables + id.v
- val v = Variable(id.v,
- optT match {
- case Some(t) => t
- case None =>
- // do a cheap (and hokey) type inference of the RHS
- rhs match {
- case Some(NewRhs(tid, _, _, _)) => Type(tid, Nil)
- case Some(BoolLiteral(b)) => Type("bool", Nil)
- case Some(StringLiteral(s)) => Type("string", Nil)
- case Some(x:BinaryExpr) if x.ResultType != null => new Type(x.ResultType);
- case Some(x:Contains) => Type("bool", Nil)
- case Some(x:Quantification) => Type("bool", Nil)
- case _ => Type("int", Nil)
- }
- }, ghost, const)
- LocalVar(v, rhs) }
- )
- def ifStmtThen: Parser[IfStmt] =
- "(" ~> expression ~ ")" ~ blockStatement ~ ("else" ~> ifStmtElse ?) ^^ {
- case guard ~ _ ~ thenClause ~ elseClause => IfStmt(guard, BlockStmt(thenClause), elseClause) }
- def ifStmtElse =
- ( "if" ~> ifStmtThen
- | statement
- )
- def loopSpec: Parser[(List[Expression], List[Expression])] =
- (loopSpecX *) ^^ {
- case pp => (pp :\ (List[Expression](), List[Expression]())) ( (p,list) =>
- (p,list) match {
- case ((null,ee),(e0,e1)) => (e0, ee ++ e1)
- case ((e,ee),(e0,e1)) => (e :: e0, ee ++ e1)
- })
- }
- def loopSpecX =
- ( "invariant" ~> expression <~ Semi ^^ { case e => (e,Nil) }
- | "lockchange" ~> expressionList <~ Semi ^^ { case ee => (null,ee) }
- )
- def declareImplicitLocals(lhs: List[VariableExpr]) =
- for (v <- lhs) yield
- if (currentLocalVariables contains v.id)
- false
- else {
- currentLocalVariables = currentLocalVariables + v.id
- true
- }
- def callStmt =
- callSignature ^? ({
- case outs ~ VariableExpr(id) ~ args =>
- val lhs = ExtractList(outs)
- Call(declareImplicitLocals(lhs), lhs, new ImplicitThisExpr, id, args)
- case outs ~ MemberAccess(obj,id) ~ args =>
- val lhs = ExtractList(outs)
- Call(declareImplicitLocals(lhs), lhs, obj, id, args)
- }, t => "bad call statement")
- def callSignature =
- (identList <~ ":=" ?) ~ callTarget ~ expressionList <~ ")" <~ Semi
- def callTarget = // returns a VariableExpr or a FieldSelect
- ( ident <~ "(" ^^ VariableExpr
- | selectExprFerSure <~ "("
- )
- def memberAccess = // returns a MemberAccess
- ( selectExprFerSure
- | ident ^^ { case id => MemberAccess(ImplicitThisExpr(), id) }
- )
- def ExtractList[T](a: Option[List[T]]): List[T] = a match {
- case None => Nil
- case Some(list) => list }
- def identList =
- ( Ident ^^ { case t => val v = VariableExpr(t.v); v.pos = t.pos; v }) ~
- (("," ~> Ident ^^ { case t => val v = VariableExpr(t.v); v.pos = t.pos; v }) *) ^^ { case e ~ ee => e::ee }
- def Rhs : Parser[RValue] =
- positioned(
- "new" ~> ident ~ opt("{" ~> repsep(FieldInit, ",") <~ "}") ~ opt(installBounds) ^^ {
- case id ~ None ~ None => NewRhs(id, Nil, Nil, Nil)
- case id ~ Some(inits) ~ None => NewRhs(id, inits, Nil, Nil)
- case id ~ None ~ Some(bounds) => NewRhs(id, Nil, bounds._1, bounds._2)
- case id ~ Some(inits) ~ Some(bounds) => NewRhs(id, inits, bounds._1, bounds._2)
- }
- | expression
- )
- def FieldInit: Parser[Init] =
- positioned( (ident <~ ":=") ~ expression ^^ { case id ~ e => Init(id, e) } )
- def installBounds: Parser[(List[Expression], List[Expression])] =
- ( "between" ~> expressionList ~ "and" ~ expressionList ^^ { case l ~ _ ~ u => (l,u) }
- | "below" ~> expressionList ~ ("above" ~> expressionList ?) ^^ {
- case u ~ None => (Nil,u)
- case u ~ Some(l) => (l,u) }
- | "above" ~> expressionList ~ ("below" ~> expressionList ?) ^^ {
- case l ~ None => (l,Nil)
- case l ~ Some(u) => (l,u) }
- )
-
- /**
- * Expressions
- */
-
- def expressionList =
- repsep(expression, ",")
- def expression = positioned(iteExpr)
-
- def partialExpressionList =
- repsep(expression | ("_" ^^^ VariableExpr("?")), ",")
-
- def iteExpr: Parser[Expression] =
- positioned(iffExpr ~ (("?" ~> iteExpr) ~ (":" ~> iteExpr) ?) ^^ {
- case e ~ None => e
- case e0 ~ Some(e1 ~ e2) => IfThenElse(e0,e1,e2) })
- def iffExpr: Parser[Expression] =
- positioned(implExpr ~ ("<==>" ~> iffExpr ?) ^^ {
- case e ~ None => e
- case e0 ~ Some(e1) => Iff(e0,e1) })
- def implExpr: Parser[Expression] =
- positioned(logicalExpr ~ ("==>" ~> implExpr ?) ^^ {
- case e ~ None => e
- case e0 ~ Some(e1) => Implies(e0,e1) })
- def logicalExpr =
- positioned(cmpExpr ~ (( ("&&" ~ cmpExpr +) | ("||" ~ cmpExpr +) )?) ^^ {
- case e ~ None => e
- case e0 ~ Some(rest) => (rest foldLeft e0) {
- case (a, "&&" ~ b) => And(a,b)
- case (a, "||" ~ b) => Or(a,b) }})
- def cmpExpr =
- positioned(concatExpr ~ ((CompareOp ~ concatExpr)?) ^^ {
- case e ~ None => e
- case e0 ~ Some("==" ~ e1) => Eq(e0,e1)
- case e0 ~ Some("!=" ~ e1) => Neq(e0,e1)
- case e0 ~ Some("<" ~ e1) => Less(e0,e1)
- case e0 ~ Some("<=" ~ e1) => AtMost(e0,e1)
- case e0 ~ Some(">=" ~ e1) => AtLeast(e0,e1)
- case e0 ~ Some(">" ~ e1) => Greater(e0,e1)
- case e0 ~ Some("<<" ~ e1) => LockBelow(e0,e1)
- case e0 ~ Some("in" ~ e1) => Contains(e0, e1)
- case e0 ~ Some("!in" ~ e1) => val c = Contains(e0, e1); c.pos = e0.pos; Not(c)
- })
- def CompareOp = "==" | "!=" | "<" | "<=" | ">=" | ">" | "<<" | "in" | "!in"
- def concatExpr =
- positioned(addExpr ~ ("++" ~> addExpr *) ^^ {
- case e0 ~ rest => (rest foldLeft e0) {
- case (a, b) => Append(a, b) }})
- def addExpr =
- positioned(multExpr ~ (AddOp ~ multExpr *) ^^ {
- case e0 ~ rest => (rest foldLeft e0) {
- case (a, "+" ~ b) => Plus(a,b)
- case (a, "-" ~ b) => Minus(a,b) }})
- def AddOp = "+" | "-"
- def multExpr: Parser[Expression] =
- unaryExpr ~ (MulOp ~ unaryExpr *) ^^ {
- case e0 ~ rest => (rest foldLeft e0) {
- case (a, "*" ~ b) => Times(a,b)
- case (a, "/" ~ b) => Div(a,b)
- case (a, "%" ~ b) => Mod(a,b) }}
- def MulOp = "*" | "/" | "%"
- def unaryExpr: Parser[Expression] =
- ( "!" ~> unaryExpr ^^ Not
- | "-" ~> unaryExpr ^^ { Minus(IntLiteral(0),_) }
- | suffixExpr
- )
- def suffixExpr =
- atom ~ (suffixThing *) ^^ {
- case e ~ sfxs => sfxs.foldLeft(e) { (t, a) => val result = a(t); result.pos = t.pos; result } }
- def suffixPlusExpr =
- atom ~ (suffixThing +) ^^ {
- case e ~ sfxs => sfxs.foldLeft(e) { (t, a) => val result = a(t); result.pos = t.pos; result } }
- def suffixThing: Parser[(Expression => Expression)] =
- ( "[" ~> expression <~ "]" ^^ { case e1 => { e0: Expression => At(e0, e1) }}
- | "[" ~> expression <~ (".." ~ "]") ^^ { case e1 => { e0: Expression => Drop(e0, e1)}}
- | "[" ~> ".." ~> expression <~ "]" ^^ { case e1 => { e0: Expression => Take(e0, e1)}}
- | "[" ~> (expression <~ "..") ~ expression <~ "]" ^^ {
- case e1 ~ e2 => {e0: Expression => val tak = Take(e0, e2); tak.pos = e0.pos; Drop(tak, e1)} }
- | "." ~> ident ~ opt("(" ~> expressionList <~ ")") ^^ {
- case name ~ None => { e0: Expression => MemberAccess(e0, name) }
- case name ~ Some(es) => { e0: Expression => FunctionApplication(e0, name, es) } }
- | "." ~> "acquire" ~> exprBody ^^ { case eb => { e0: Expression => Eval(AcquireState(e0), eb) }}
- | "." ~> "release" ~> exprBody ^^ { case eb => { e0: Expression => Eval(ReleaseState(e0), eb) }}
- | "." ~> "fork" ~> (callTarget ~ partialExpressionList <~ ")") ~ exprBody ^^ {
- case MemberAccess(obj,id) ~ args ~ eb => { e0: Expression => Eval(CallState(e0, obj, id, args), eb) }}
- )
- def exprBody =
- "{" ~> expression <~ "}"
-
- def selectExprFerSure: Parser[MemberAccess] =
- positioned(atom ~ "." ~ ident ~ ("." ~> ident *) ^^ {
- case e ~ _ ~ field ~ moreFields =>
- (moreFields foldLeft MemberAccess(e,field)) { (target, f) =>
- val result = MemberAccess(target, f); result.pos = target.pos; result }})
- def selectExprFerSureX: Parser[MemberAccess] =
- positioned(atom ~ identOrSpecial ~ ("." ~> ident *) ^^ {
- case e ~ field ~ moreFields =>
- (moreFields foldLeft MemberAccess(e,field)) { (target, f) =>
- val result = MemberAccess(target, f); result.pos = target.pos; result }})
- def identOrSpecial: Parser[String] =
- ( "." ~> ident ^^ { case s => s }
- | "." ~> "acquire" ^^^ "acquire"
- | "." ~> "release" ^^^ "release"
- | "." ~> "fork" ^^^ "fork"
- | "." ~> "*" ^^^ "*"
- | "["~"*"~"]"~"."~"*" ^^^ "[*].*"
- | "["~"*"~"]" ^^^ "[*]"
- )
-
- def atom : Parser[Expression] =
- positioned(
- numericLit ^^ { case n => IntLiteral(n.toInt) }
- | "false" ^^^ BoolLiteral(false)
- | "true" ^^^ BoolLiteral(true)
- | "null" ^^^ NullLiteral()
- | stringLit ^^ { case s => StringLiteral(s) }
- | "waitlevel" ^^^ MaxLockLiteral()
- | "lockbottom" ^^^ LockBottomLiteral()
- | "this" ^^^ ExplicitThisExpr()
- | "result" ^^^ Result()
- | positioned(Ident) ~ opt("(" ~> expressionList <~ ")") ^^ {
- case id ~ None =>
- val r =
- if ((currentLocalVariables contains id.v) || assumeAllLocals) {
- VariableExpr(id.v)
- } else {
- val implicitThis = ImplicitThisExpr(); implicitThis.pos = id.pos
- MemberAccess(implicitThis, id.v)
- }
- r.pos = id.pos; r
- case id ~ Some(args) =>
- val implicitThis = ImplicitThisExpr(); implicitThis.pos = id.pos
- val r = FunctionApplication(implicitThis, id.v, args)
- r.pos = id.pos; r
- }
- | "rd" ~> "(" ~>
- ( // note: depending on the context where rd occurs, we parse it wrongly (e.g. acc(x,rd(n)) is parsed to
- // Access(MemberAccess(ImplicitThisExpr(),x),Frac(Access(MemberAccess(ImplicitThisExpr(),n),Epsilon))) ).
- // This might seem completely wrong (and it is), but we correct this later, see the comment before
- // method ResolvePermissionExpr in the resolver.
- (( (Ident ^^ (e => { val result = MemberAccess(ImplicitThisExpr(),e.v); result.pos = e.pos; result})) ~ rdPermArg <~ ")"
- | selectExprFerSureX ~ rdPermArg <~ ")"
- ) ^^ {
- case MemberAccess(obj, "*") ~ p => AccessAll(obj, p);
- case MemberAccess(obj, "[*].*") ~ p => AccessSeq(obj, None, p);
- case MemberAccess(MemberAccess(obj, "[*]"), f) ~ p => AccessSeq(obj, Some(MemberAccess(At(obj, IntLiteral(0)), f)), p);
- case e ~ p => Access(e, p)
- })
- | expression <~ ")" ^^ {
- case e => val eps = Epsilons(e); eps.pos = e.pos; eps
- }
- | "*" ~> ")" ~ err("This syntax is not supported any longer. For the starred read permission, use rd*(o.f).") ^^^ Star
- )
- | "rd" ~> "*" ~> "(" ~>
- (
- (( (Ident ^^ (e => { val result = MemberAccess(ImplicitThisExpr(),e.v); result.pos = e.pos; result})) <~ ")"
- | selectExprFerSureX <~ ")"
- ) ^^ {
- case MemberAccess(obj, "*") => AccessAll(obj, Star);
- case MemberAccess(obj, "[*].*") => AccessSeq(obj, None, Star);
- case MemberAccess(MemberAccess(obj, "[*]"), f) => AccessSeq(obj, Some(MemberAccess(At(obj, IntLiteral(0)), f)), Star);
- case e => Access(e, Star)
- })
- )
- | "acc" ~> "(" ~>
- ( (Ident ^^ (e => { val result = MemberAccess(ImplicitThisExpr(),e.v); result.pos = e.pos; result} )) ~ accPermArg <~ ")"
- | selectExprFerSureX ~ accPermArg <~ ")"
- ) ^^ {
- case MemberAccess(obj, "*") ~ p => AccessAll(obj, p);
- case MemberAccess(obj, "[*].*") ~ p => AccessSeq(obj, None, p);
- case MemberAccess(MemberAccess(obj, "[*]"), f) ~ p => AccessSeq(obj, Some(MemberAccess(At(obj, IntLiteral(0)), f)), p);
- case e ~ p => Access(e, p)
- }
- | "credit" ~> "(" ~> expression ~ ("," ~> expression ?) <~ ")" ^^ {
- case ch ~ n => Credit(ch, n) }
- | "holds" ~> "(" ~> expression <~ ")" ^^ Holds
- | "rd" ~> "holds" ~> "(" ~> expression <~ ")" ^^ RdHolds
- | "rd" ^^ (_ => MethodEpsilon)
- | "assigned" ~> "(" ~> ident <~ ")" ^^ Assigned
- | "old" ~> "(" ~> expression <~ ")" ^^ Old
- | ("unfolding" ~> suffixExpr <~ "in") ~ expression ^? {
- case (pred: MemberAccess) ~ e => val acc = Access(pred, Full); acc.pos = pred.pos; Unfolding(acc, e)
- case (perm: Access) ~ e => Unfolding(perm, e)
- }
- | "|" ~> expression <~ "|" ^^ Length
- | ("eval" ~ "(") ~> (evalstate <~ ",") ~ (expression <~ ")") ^^ { case h ~ e => Eval(h, e) }
- | ("ite" ~> "(" ~> expression <~ ",") ~ (expression <~ ",") ~ (expression <~ ")") ^^ {
- case con ~ then ~ els => IfThenElse (con, then, els) }
- | "(" ~> expression <~ ")"
- | quantifierType
- | quantifierSeq
- | ("[" ~> expression) ~ (".." ~> expression <~ "]") ^^ { case from ~ to => Range(from, to) }
- | ("nil" ~> "<") ~> (typeDecl <~ ">") ^^ EmptySeq
- | ("[" ~> expressionList <~ "]") ^^ { case es => ExplicitSeq(es) }
- )
-
- def quantifierSeq: Parser[Quantification] =
- (quant ~ repsep(ident, ",")) into {case q ~ is => quantifierSeqBody(q, is)}
- def quantifierSeqBody(q: Quant, is: List[String]) : Parser[Quantification] =
- (("in" ~> expression <~ "::") ~ (exprWithLocals(is))) ^^
- { case seq ~ e =>
- currentLocalVariables = currentLocalVariables -- is;
- SeqQuantification(q, is, seq, e);
- }
- def quantifierType: Parser[Quantification] =
- (quant ~ repsep(ident, ",")) into {case q ~ is => quantifierTypeBody(q, is)}
- def quantifierTypeBody(q: Quant, is: List[String]) : Parser[Quantification] =
- ((":" ~> typeDecl <~ "::") ~ (exprWithLocals(is))) ^^
- { case t ~ e =>
- currentLocalVariables = currentLocalVariables -- is;
- new TypeQuantification(q, is, t, e);
- }
- def quant: Parser[Quant] =
- ( "forall" ^^^ Forall | "exists" ^^^ Exists)
-
- def exprWithLocals(i: List[String]) : Parser[Expression] = {
- currentLocalVariables = currentLocalVariables ++ i;
- val result = ((expression) ^^ { case e => e});
- result
- }
-
- def evalstate: Parser[EvalState] =
- (suffixExpr <~ ".") into { e =>
- ( "acquire" ^^^ AcquireState(e)
- | "release" ^^^ ReleaseState(e)
- | "fork" ~> callTarget ~ partialExpressionList <~ ")" ^^ {
- case MemberAccess(obj,id) ~ args => CallState(e, obj, id, args) }
- )}
-
- def rdPermArg : Parser[Permission] =
- opt( "," ~> "*" ~ err("This syntax is not supported any longer. For the starred read permission, use rd*(o.f).") ^^^ Star
- | "," ~> expression ^^ { case e => val eps = Epsilons(e); eps.pos = e.pos; eps }) ^^ { case None => Epsilon; case Some(p) => p}
-
- def accPermArg : Parser[Write] =
- opt( "," ~> expression ^^ { case e => val f: Frac = Frac(e); f.pos = e.pos; f }) ^^ { case None => Full; case Some(p) => p}
-
- /**
- * Transforms
- */
-
- def transform: Parser[Transform] = rep1(transformAtom) ^^ SeqPat
- def transformAtom: Parser[Transform] = positioned(
- "_" ~ Semi ^^^ BlockPat()
- | "*" ~ Semi ^^^ SkipPat()
- | "if" ~> ifTransform
- | "while" ~> rep("invariant" ~> expression <~ Semi) ~ ("{" ~> transform <~ "}") ^^ {case ee ~ body => WhilePat(ee, body)}
- | "replaces" ~> "*" ~> "by" ~> blockStatement ^^ ProgramPat
- | "replaces" ~> rep1sep(Ident,",") ~ ("by" ~> blockStatement) ^^ {
- case ids ~ code => NonDetPat(ids map {x => x.v}, code)
- }
- | rep1(statement) ^^ {case s => InsertPat(s)}
- )
- def ifTransform: Parser[IfPat] =
- ("{" ~> transform <~ "}") ~ ("else" ~> ifTransformElse ?) ^^ {
- case thn ~ els => IfPat(thn, els)
- }
- def ifTransformElse = (
- "if" ~> ifTransform
- | "{" ~> transform <~ "}"
- )
-
-}
|