Skip to content

Commit ba9ea5a

Browse files
author
Malte Schwerhoff
committed
Merge branch 'master' of github.com:viperproject/silver
2 parents 2f0e6ed + 741a39d commit ba9ea5a

12 files changed

Lines changed: 175 additions & 149 deletions

File tree

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

Lines changed: 17 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -121,30 +121,37 @@ trait Node extends Iterable[Node] with Rewritable {
121121
/** @see [[viper.silver.ast.utility.ViperStrategy]] */
122122
def transform(pre: PartialFunction[Node, Node] = PartialFunction.empty,
123123
recurse: Traverse = Traverse.Innermost)
124-
: this.type =
124+
: this.type = {
125125

126-
StrategyBuilder.Slim[Node](pre, recurse) execute[this.type] (this)
126+
StrategyBuilder.Slim[Node](pre, recurse) execute[this.type] (this)
127+
}
127128

128129
def transformForceCopy(pre: PartialFunction[Node, Node] = PartialFunction.empty,
129-
recurse: Traverse = Traverse.Innermost)
130-
: this.type =
130+
recurse: Traverse = Traverse.Innermost)
131+
: this.type = {
131132

132133
StrategyBuilder.Slim[Node](pre, recurse).forceCopy() execute[this.type] (this)
134+
}
133135

134136
/**
135137
* Allows a transformation with a custom context threaded through
136138
*
137139
* @see [[viper.silver.ast.utility.ViperStrategy]] */
138140
def transformWithContext[C](transformation: PartialFunction[(Node,C), (Node, C)] = PartialFunction.empty,
139-
initialContext: C,
140-
recurse: Traverse = Traverse.Innermost)
141-
: this.type =
141+
initialContext: C,
142+
recurse: Traverse = Traverse.Innermost)
143+
: this.type = {
144+
142145
ViperStrategy.CustomContext[C](transformation, initialContext, recurse) execute[this.type] (this)
146+
}
143147

144148
def transformNodeAndContext[C](transformation: PartialFunction[(Node,C), (Node, C)],
145149
initialContext: C,
146-
recurse: Traverse = Traverse.Innermost) : this.type =
150+
recurse: Traverse = Traverse.Innermost)
151+
: this.type = {
152+
147153
StrategyBuilder.RewriteNodeAndContext[Node, C](transformation, initialContext, recurse).execute[this.type](this)
154+
}
148155

149156
def replace(original: Node, replacement: Node): this.type =
150157
this.transform { case `original` => replacement }
@@ -155,11 +162,11 @@ trait Node extends Iterable[Node] with Rewritable {
155162

156163
/** @see [[Visitor.deepCollect()]] */
157164
def deepCollect[A](f: PartialFunction[Node, A]): Seq[A] =
158-
Visitor.deepCollect(Seq(this), Nodes.subnodes)(f)
165+
Visitor.deepCollect(Seq(this), Nodes.subnodes)(f)
159166

160167
/** @see [[Visitor.shallowCollect()]] */
161168
def shallowCollect[R](f: PartialFunction[Node, R]): Seq[R] =
162-
Visitor.shallowCollect(Seq(this), Nodes.subnodes)(f)
169+
Visitor.shallowCollect(Seq(this), Nodes.subnodes)(f)
163170

164171
def contains(n: Node): Boolean = this.existsDefined {
165172
case `n` =>

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -55,6 +55,7 @@ object FastMessaging {
5555
*/
5656
def message (value : Any, msg : String, cond : Boolean = true, error : Boolean = true) : Messages =
5757
if (cond) {
58+
// Warning: Potential scala.MatchError here if position info is lost!
5859
val valuePos: SourcePosition = value.asInstanceOf[PNode].pos._1 match {
5960
case slc: FilePosition => {
6061
value.asInstanceOf[PNode].pos._2 match {

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

Lines changed: 37 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -145,7 +145,7 @@ object FastParser {
145145
j += 1
146146
}
147147
}
148-
PProgram(Seq(), macros, domains, fields, functions, predicates, methods, extensions, errors)()
148+
PProgram(Seq(), macros, domains, fields, functions, predicates, methods, extensions, errors)(p.pos)
149149
}
150150

151151

@@ -474,7 +474,7 @@ object FastParser {
474474
linearizeMethod(doExpandDefines(localMacros ++ globalMacros, methodWithoutMacros, p))
475475
})
476476

477-
PProgram(p.imports, p.macros, domains, p.fields, functions, predicates, methods, p.extensions, p.errors ++ warnings)()
477+
PProgram(p.imports, p.macros, domains, p.fields, functions, predicates, methods, p.extensions, p.errors ++ warnings)(p.pos)
478478
}
479479

480480

@@ -1017,43 +1017,51 @@ object FastParser {
10171017

10181018
def setTypedEmpty[_: P]: P[PExp] = collectionTypedEmpty("Set", (a, b) => PEmptySet(a)(b))
10191019

1020-
def explicitSetNonEmpty[_: P]: P[PExp] = P("Set" ~ "(" ~/ exp.rep(sep = ",", min = 1) ~ ")").map(PExplicitSet(_)())
1020+
def explicitSetNonEmpty[_: P]: P[PExp] = P(FP("Set" ~ "(" ~/ exp.rep(sep = ",", min = 1) ~ ")").map {
1021+
case (pos, exps) => PExplicitSet(exps)(pos)
1022+
})
10211023

1022-
def explicitMultisetNonEmpty[_: P]: P[PExp] = P("Multiset" ~ "(" ~/ exp.rep(min = 1, sep = ",") ~ ")").map(PExplicitMultiset(_)())
1024+
def explicitMultisetNonEmpty[_: P]: P[PExp] = P(FP("Multiset" ~ "(" ~/ exp.rep(min = 1, sep = ",") ~ ")").map {
1025+
case (pos, exps) => PExplicitMultiset(exps)(pos)
1026+
})
10231027

10241028
def multiSetTypedEmpty[_: P]: P[PExp] = collectionTypedEmpty("Multiset", (a, b) => PEmptyMultiset(a)(b))
10251029

10261030
def seqTypedEmpty[_: P]: P[PExp] = collectionTypedEmpty("Seq", (a, b) => PEmptySeq(a)(b))
10271031

1028-
//HEAD: def seqLength[_: P]: P[PExp] = P("|" ~ exp ~ "|").map(PSize(_)())
1029-
def size[_: P]: P[PExp] = P("|" ~ exp ~ "|").map(PSize(_)())
1030-
//MAP: lazy val size: P[PExp] = P("|" ~ exp ~ "|").map(PSize)
1032+
def size[_: P]: P[PExp] = P(FP("|" ~ exp ~ "|").map {
1033+
case (pos, e) => PSize(e)(pos)
1034+
})
10311035

1032-
def explicitSeqNonEmpty[_: P]: P[PExp] = P("Seq" ~ "(" ~/ exp.rep(min = 1, sep = ",") ~ ")").map(PExplicitSeq(_)())
1036+
def explicitSeqNonEmpty[_: P]: P[PExp] = P(FP("Seq" ~ "(" ~/ exp.rep(min = 1, sep = ",") ~ ")").map {
1037+
case (pos, exps) => PExplicitSeq(exps)(pos)
1038+
})
10331039

10341040
private def collectionTypedEmpty[_: P](name: String, typeConstructor: (PType, (Position, Position)) => PExp): P[PExp] =
10351041
FP(`name` ~ ("[" ~/ typ ~ "]").? ~ "(" ~ ")").map{ case (pos, typ) => typeConstructor(typ.getOrElse(PTypeVar("#E")), pos)}
10361042

10371043
def seqRange[_: P]: P[PExp] = FP("[" ~ exp ~ ".." ~ exp ~ ")").map { case (pos, (a, b)) => PRangeSeq(a, b)(pos) }
1038-
// MAPS: lazy val seqRange: P[PExp] = P("[" ~ exp ~ ".." ~ exp ~ ")").map { case (a, b) => PRangeSeq(a, b) }
10391044

1040-
def mapTypedEmpty[_: P] : P[PMapLiteral] = P("Map" ~ ("[" ~/ typ ~ "," ~ typ ~ "]").? ~ "(" ~ ")").map {
1041-
case Some((keyType, valueType)) => PEmptyMap(keyType, valueType)()
1042-
case None => PEmptyMap(PTypeVar("#K"), PTypeVar("#E"))()
1043-
}
1045+
def mapTypedEmpty[_: P] : P[PMapLiteral] = P(FP("Map" ~ ("[" ~/ typ ~ "," ~ typ ~ "]").? ~ "(" ~ ")").map {
1046+
case (pos, Some((keyType, valueType))) => PEmptyMap(keyType, valueType)(pos)
1047+
case (pos, None) => PEmptyMap(PTypeVar("#K"), PTypeVar("#E"))(pos)
1048+
})
10441049

1045-
def maplet[_: P]: P[PMaplet] = P(exp ~ ":=" ~ exp).map {
1046-
case (key, value) => PMaplet(key, value)()
1047-
}
1050+
def maplet[_: P]: P[PMaplet] = P(FP(exp ~ ":=" ~ exp).map {
1051+
case (pos, (key, value)) => PMaplet(key, value)(pos)
1052+
})
10481053

1049-
// MAPS: lazy val explicitMapNonEmpty : P[PMapLiteral] = P("Map" ~ "(" ~/ maplet.rep(min = 1, sep = ",") ~ ")").map(PExplicitMap)
1050-
def explicitMapNonEmpty[_: P]: P[PMapLiteral] = P("Map" ~ "(" ~/ maplet.rep(sep = ",", min = 1) ~ ")").map(PExplicitMap(_)())
1054+
def explicitMapNonEmpty[_: P]: P[PMapLiteral] = P(FP("Map" ~ "(" ~/ maplet.rep(sep = ",", min = 1) ~ ")").map {
1055+
case (pos, maplets) => PExplicitMap(maplets)(pos)
1056+
})
10511057

1052-
//lazy val mapDomain : P[PExp] = P("domain" ~ "(" ~ exp ~ ")").map(PMapDomain)
1053-
def mapDomain[_: P]: P[PExp] = P("domain" ~ "(" ~ exp ~ ")").map(PMapDomain(_)())
1054-
//def size[_: P]: P[PExp] = P("|" ~ exp ~ "|").map(PSize(_))
1058+
def mapDomain[_: P]: P[PExp] = P(FP("domain" ~ "(" ~ exp ~ ")").map {
1059+
case (pos, e) => PMapDomain(e)(pos)
1060+
})
10551061

1056-
def mapRange[_: P] : P[PExp] = P("range" ~ "(" ~ exp ~ ")").map(PMapRange(_)())
1062+
def mapRange[_: P] : P[PExp] = P(FP("range" ~ "(" ~ exp ~ ")").map {
1063+
case (pos, e) => PMapRange(e)(pos)
1064+
})
10571065

10581066
def fapp[_: P]: P[PCall] = FP(idnuse ~ parens(actualArgList)).map {
10591067
case (pos, (func, args)) =>
@@ -1105,9 +1113,9 @@ object FastParser {
11051113
case (pos, (cond, thn, ele)) => PSeqn(Seq(PIf(cond, thn, ele)(pos)))(pos)
11061114
}
11071115

1108-
def els[_: P]: LW[PSeqn] = ((keyword("else") ~/ block) | FP(Pass)).lw.map {
1109-
case block: PSeqn => block
1110-
case (pos, _) => PSeqn(Nil)() }
1116+
def els[_: P]: LW[PSeqn] = ((keyword("else") ~/ block) | FP(Pass).map {
1117+
case (pos, _) => PSeqn(Nil)(pos)
1118+
}).lw
11111119

11121120
def whle[_: P]: P[PWhile] = FP(keyword("while") ~/ "(" ~ exp ~ ")" ~ inv.rep ~ block).map {
11131121
case (pos, (cond, invs, body)) =>
@@ -1156,8 +1164,8 @@ object FastParser {
11561164

11571165
def applying[_: P]: P[PExp] = FP(keyword("applying") ~/ "(" ~ magicWandExp ~ ")" ~ "in" ~ exp).map { case (pos, (a, b)) => PApplying(a, b)(pos) }
11581166

1159-
def programDecl(implicit ctx : P[_]) : P[PProgram] = P((ParserExtension.newDeclAtStart(ctx) | preambleImport | defineDecl | domainDecl | fieldDecl | functionDecl | predicateDecl | methodDecl | ParserExtension.newDeclAtEnd(ctx)).rep).map {
1160-
decls => {
1167+
def programDecl(implicit ctx : P[_]) : P[PProgram] = P(FP((ParserExtension.newDeclAtStart(ctx) | preambleImport | defineDecl | domainDecl | fieldDecl | functionDecl | predicateDecl | methodDecl | ParserExtension.newDeclAtEnd(ctx)).rep).map {
1168+
case (pos, decls) => {
11611169
PProgram(
11621170
decls.collect { case i: PImport => i }, // Imports
11631171
decls.collect { case d: PDefine => d }, // Macros
@@ -1168,9 +1176,9 @@ object FastParser {
11681176
decls.collect { case m: PMethod => m }, // Methods
11691177
decls.collect { case e: PExtender => e }, // Extensions
11701178
Seq() // Parse Errors
1171-
)()
1179+
)(pos)
11721180
}
1173-
}
1181+
})
11741182

11751183
def preambleImport[_: P]: P[PImport] = FP(keyword("import") ~/ (
11761184
P(quoted(relativeFilePath.!)).map{ filename => pos: (Position, Position) => PLocalImport(filename)(pos) } |

0 commit comments

Comments
 (0)