Skip to content

Commit b149ceb

Browse files
committed
Fix macro issue and add support for macros as types
1 parent 348c2a5 commit b149ceb

4 files changed

Lines changed: 50 additions & 30 deletions

File tree

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

Lines changed: 29 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -595,10 +595,9 @@ class FastParser {
595595
case class MacroApp(name: String, arguments: Seq[PExp], node: PNode)
596596

597597
val matchOnMacroCall: PartialFunction[PNode, MacroApp] = {
598-
case app: PMacroRef => MacroApp(app.idnuse.name, Nil, app)
599-
case app@PAssign(_, call: PCall) if isMacro(call.func.name) => MacroApp(call.func.name, call.args, app)
600-
case app: PCall if isMacro(app.func.name) => MacroApp(app.func.name, app.args, app)
601-
case app: PIdnUse if isMacro(app.name) => MacroApp(app.name, Nil, app)
598+
case assign@PAssign(Seq(), app: PMacro) if isMacro(app.name) => MacroApp(app.name, app.args, assign)
599+
case app: PMacro if isMacro(app.name) => MacroApp(app.name, app.args, app)
600+
case app: PMacroType[_] => MacroApp(app.use.name, app.use.args, app)
602601
}
603602

604603
def detectCyclicMacros(start: PNode, seen: Set[String]): Unit = {
@@ -706,11 +705,21 @@ class FastParser {
706705
throw ParseException("Number of macro arguments does not match", call.pos._1)
707706

708707
(call, body) match {
709-
case (_: PStmt, _: PExp) =>
710-
throw ParseException("Expression macro used in statement position", call.pos._1)
711-
case (_: PExp, _: PStmt) =>
712-
throw ParseException("Statement macro used in expression position", call.pos._1)
708+
case (_: PStmt, _: PStmt) | (_: PExp, _: PExp) | (_: PType, _: PType) =>
713709
case _ =>
710+
val expandedType = body match {
711+
case _: PExp => "Expression"
712+
case _: PStmt => "Statement"
713+
case _: PType => "Type"
714+
case _ => "Unknown"
715+
}
716+
val callType = call match {
717+
case _: PExp => "expression"
718+
case _: PStmt => "statement"
719+
case _: PType => "type"
720+
case _ => "unknown"
721+
}
722+
throw ParseException(s"$expandedType macro used in $callType position", call.pos._1)
714723
}
715724

716725
/* TODO: The current unsupported position detection is probably not exhaustive.
@@ -778,7 +787,6 @@ class FastParser {
778787
* to construct invalid AST nodes.
779788
* Recursing into such PIdnUse nodes caused Silver issue #205.
780789
*/
781-
case PMacroRef(_) => Seq.empty
782790
case PCall(_, args, typeAnnotated) => Seq(args, typeAnnotated)
783791
}.repeat
784792

@@ -997,28 +1005,29 @@ class FastParser {
9971005

9981006
def formalArg[$: P]: P[PFormalArgDecl] = FP(idndef ~ ":" ~ typ).map { case (pos, (a, b)) => PFormalArgDecl(a, b)(pos) }
9991007

1000-
def typ[$: P]: P[PType] = P(primitiveTyp | domainTyp | seqType | setType | multisetType | mapType)
1001-
// Maps: lazy val typ: P[PType] = P(primitiveTyp | domainTyp | seqType | setType | multisetType | mapType)
1008+
def typ[$: P]: P[PType] = P(primitiveTyp | domainTyp | seqType | setType | multisetType | mapType | macroType)
10021009

10031010
def domainTyp[$: P]: P[PDomainType] = P(FP(idnuse ~ "[" ~ typ.rep(sep = ",") ~ "]").map { case (pos, (a, b)) => PDomainType(a, b)(pos) } |
10041011
// domain type without type arguments (might also be a type variable)
10051012
idnuse.map(name => {
10061013
PDomainType(name, Nil)(name.pos)
10071014
}))
10081015

1009-
def seqType[$: P]: P[PType] = FP(keyword("Seq") ~ "[" ~ typ ~ "]").map{ case (pos, t) => PSeqType(t)(pos)}
1016+
def seqType[$: P]: P[PSeqType] = FP(keyword("Seq") ~ "[" ~ typ ~ "]").map{ case (pos, t) => PSeqType(t)(pos)}
10101017

1011-
def setType[$: P]: P[PType] = FP(keyword("Set") ~ "[" ~ typ ~ "]").map{ case (pos, t) => PSetType(t)(pos)}
1018+
def setType[$: P]: P[PSetType] = FP(keyword("Set") ~ "[" ~ typ ~ "]").map{ case (pos, t) => PSetType(t)(pos)}
10121019

1013-
def multisetType[$: P]: P[PType] = FP(keyword("Multiset") ~ "[" ~ typ ~ "]").map{ case (pos, t) => PMultisetType(t)(pos)}
1020+
def multisetType[$: P]: P[PMultisetType] = FP(keyword("Multiset") ~ "[" ~ typ ~ "]").map{ case (pos, t) => PMultisetType(t)(pos)}
10141021

10151022
//def mapType[$: P]: P[PType] = FP(keyword("Map") ~ "[" ~ typ ~ "," ~ typ ~ "]").map{ case (pos, t) => PSeqType(t._3)(pos)}
10161023
// Maps:
1017-
def mapType[$: P] : P[PType] = FP(keyword("Map") ~ "[" ~ typ ~ "," ~ typ ~ "]").map {
1024+
def mapType[$: P] : P[PMapType] = FP(keyword("Map") ~ "[" ~ typ ~ "," ~ typ ~ "]").map {
10181025
case (pos, (keyType, valueType)) => PMapType(keyType, valueType)(pos)
10191026
}
10201027

1021-
def primitiveTyp[$: P]: P[PType] = P(FP(keyword("Rational")).map{ case (pos, _) => PPrimitiv("Perm")(pos)}
1028+
def macroType[$: P] : P[PMacroType[_]] = idnuse.map(PMacroType(_)) | fapp.map(PMacroType(_))
1029+
1030+
def primitiveTyp[$: P]: P[PPrimitiv] = P(FP(keyword("Rational")).map{ case (pos, _) => PPrimitiv("Perm")(pos)}
10221031
| FP((StringIn("Int", "Bool", "Perm", "Ref") ~~ !identContinues).!).map{ case (pos, name) => PPrimitiv(name)(pos)})
10231032
/* Maps:
10241033
lazy val primitiveTyp: P[PType] = P(keyword("Rational").map(_ => PPrimitiv("Perm"))
@@ -1101,18 +1110,16 @@ class FastParser {
11011110
case (pos, (func, args, typeGiven)) => PCall(func, args, Some(typeGiven))(pos)
11021111
}
11031112

1104-
def stmt(implicit ctx : P[_]) : P[PStmt] = P(ParserExtension.newStmtAtStart(ctx) | fold | unfold | exhale | assertP |
1113+
def stmt(implicit ctx : P[_]) : P[PStmt] = P(ParserExtension.newStmtAtStart(ctx) | assign | fold | unfold | exhale | assertP |
11051114
inhale | assume | ifthnels | whle | varDecl | defineDecl |
1106-
goto | lbl | packageWand | applyWand | assign | macroref | block |
1115+
goto | lbl | packageWand | applyWand | block |
11071116
quasihavoc | quasihavocall | ParserExtension.newStmtAtEnd(ctx))
11081117

1109-
def nodefinestmt(implicit ctx : P[_]) : P[PStmt] = P(ParserExtension.newStmtAtStart(ctx) | fold | unfold | exhale | assertP |
1118+
def nodefinestmt(implicit ctx : P[_]) : P[PStmt] = P(ParserExtension.newStmtAtStart(ctx) | assign | fold | unfold | exhale | assertP |
11101119
inhale | assume | ifthnels | whle | varDecl |
1111-
goto | lbl | packageWand | applyWand | assign | macroref | block |
1120+
goto | lbl | packageWand | applyWand | block |
11121121
quasihavoc | quasihavocall | ParserExtension.newStmtAtEnd(ctx))
11131122

1114-
def macroref[$: P]: P[PMacroRef] = FP(idnuse).map { case (pos, a) => PMacroRef(a)(pos) }
1115-
11161123
def assignTarget[$: P]: P[PAssignTarget] = P(fieldAcc | NoCut(fapp) | idnuse)
11171124

11181125
def assign[$: P]: P[PAssign] = FP((assignTarget.rep(min = 1, sep = ",") ~ ":=").? ~ exp).map { case (pos, (targets, rhs)) => PAssign(targets.getOrElse(Seq()), rhs)(pos) }

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

Lines changed: 21 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -149,8 +149,9 @@ trait PIdentifier {
149149

150150
case class PIdnDef(name: String)(val pos: (Position, Position)) extends PNode with PIdentifier
151151

152-
case class PIdnUse(name: String)(val pos: (Position, Position)) extends PExp with PIdentifier with PAssignTarget {
152+
case class PIdnUse(name: String)(val pos: (Position, Position)) extends PExp with PIdentifier with PAssignTarget with PMacro {
153153
var decl: PDeclaration = null
154+
override def args: Seq[PExp] = Seq()
154155
/* Should be set during resolving. Intended to preserve information
155156
* that is needed by the translator.
156157
*/
@@ -366,6 +367,16 @@ case class PMapType(keyType: PType, valueType: PType)(val pos: (Position, Positi
366367
override def withTypeArguments(s: Seq[PType]): PMapType = copy(keyType = s.head, valueType = s(1))(pos)
367368
}
368369

370+
case class PMacroType[T <: PMacro](use: T) extends PType {
371+
override val pos: (Position, Position) = use.pos
372+
373+
override def isValidOrUndeclared: Boolean = ???
374+
375+
override def substitute(ts: PTypeSubstitution): PType = ???
376+
377+
override def subNodes: Seq[PType] = ???
378+
}
379+
369380
/** Type used for internal nodes (e.g. typing predicate accesses) - should not be
370381
* the type of any expression whose value is meaningful in the translation.
371382
*/
@@ -569,9 +580,10 @@ object POpApp {
569580
def pRes = PTypeVar(pResS)
570581
}
571582

572-
case class PCall(func: PIdnUse, args: Seq[PExp], typeAnnotated: Option[PType] = None)(val pos: (Position, Position)) extends POpApp with PLocationAccess with PAssignTarget {
583+
case class PCall(func: PIdnUse, args: Seq[PExp], typeAnnotated: Option[PType] = None)(val pos: (Position, Position)) extends POpApp with PLocationAccess with PAssignTarget with PMacro {
573584
override val idnuse = func
574585
override val opName = func.name
586+
override def name = func.name
575587

576588
override def signatures = if (function != null && function.formalArgs.size == args.size) (function match {
577589
case _: PFunction => List(
@@ -1224,6 +1236,7 @@ case class PAssume(e: PExp)(val pos: (Position, Position)) extends PStmt
12241236

12251237
case class PInhale(e: PExp)(val pos: (Position, Position)) extends PStmt
12261238

1239+
/** Can also represent a method call or statement macro with no `:=` when `targets` is empty. */
12271240
case class PAssign(targets: Seq[PAssignTarget], rhs: PExp)(val pos: (Position, Position)) extends PStmt
12281241

12291242
case class PIf(cond: PExp, thn: PSeqn, els: PSeqn)(val pos: (Position, Position)) extends PStmt
@@ -1240,8 +1253,6 @@ case class PGoto(targets: PIdnUse)(val pos: (Position, Position)) extends PStmt
12401253

12411254
case class PTypeVarDecl(idndef: PIdnDef)(val pos: (Position, Position)) extends PLocalDeclaration
12421255

1243-
case class PMacroRef(idnuse: PIdnUse)(val pos: (Position, Position)) extends PStmt
1244-
12451256
case class PDefine(idndef: PIdnDef, parameters: Option[Seq[PIdnDef]], body: PNode)(val pos: (Position, Position)) extends PStmt with PLocalDeclaration
12461257

12471258
case class PSkip()(val pos: (Position, Position)) extends PStmt
@@ -1272,6 +1283,12 @@ object PScope {
12721283
}
12731284
}
12741285

1286+
// Macros
1287+
sealed trait PMacro extends PExp {
1288+
def name: String
1289+
def args: Seq[PExp]
1290+
}
1291+
12751292
// Assignments
12761293
sealed trait PAssignTarget extends PExp
12771294

@@ -1467,7 +1484,6 @@ object Nodes {
14671484
case PExplicitSet(elems) => elems
14681485
case PEmptyMultiset(t) => Seq(t)
14691486
case PExplicitMultiset(elems) => elems
1470-
case PMacroRef(_) => Nil
14711487
case PEmptyMap(k, v) => Seq(k, v)
14721488
case PExplicitMap(elems) => elems
14731489
case PMapRange(base) => Seq(base)

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

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -172,8 +172,6 @@ case class TypeChecker(names: NameAnalyser) {
172172

173173
def check(stmt: PStmt): Unit = {
174174
stmt match {
175-
case PMacroRef(id) =>
176-
messages ++= FastMessaging.message(stmt, "unknown macro used: " + id.name)
177175
case s@PSeqn(ss) =>
178176
checkMember(s) {
179177
ss foreach check

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,6 @@ object Transformer {
2222

2323
def recurse(parent: PNode): PNode = {
2424
val newNode = parent match {
25-
case p@PMacroRef(idnuse) => PMacroRef(go(idnuse))(p.pos)
2625
case _: PIdnDef => parent
2726
case _: PIdnUse => parent
2827
case p@PFormalArgDecl(idndef, typ) => PFormalArgDecl(go(idndef), go(typ))(p.pos)

0 commit comments

Comments
 (0)