Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 79a6f69

Browse files
committedApr 4, 2025·
Gave new utility method a proper signature
1 parent b4baa4b commit 79a6f69

File tree

4 files changed

+9
-8
lines changed

4 files changed

+9
-8
lines changed
 

‎src/main/scala/viper/silver/ast/utility/Consistency.scala

+2-2
Original file line numberDiff line numberDiff line change
@@ -270,8 +270,8 @@ object Consistency {
270270
case Old(nested) => validTrigger(nested, program) // case corresponds to OldTrigger node
271271
case LabelledOld(nested, _) => validTrigger(nested, program)
272272
case ee: ExtensionExp => ee.extensionIsValidTrigger()
273-
case wand: MagicWand => wand.subexpressionsToEvaluate(program).forall(e => !e.existsDefined(Expressions.isForbiddenInTrigger))
274-
case _ : PossibleTrigger | _: FieldAccess | _: PredicateAccess => !e.existsDefined(Expressions.isForbiddenInTrigger)
273+
case wand: MagicWand => wand.subexpressionsToEvaluate(program).forall(e => !e.exists(Expressions.isForbiddenInTrigger))
274+
case _ : PossibleTrigger | _: FieldAccess | _: PredicateAccess => !e.exists(Expressions.isForbiddenInTrigger)
275275
case _ => false
276276
}
277277
}

‎src/main/scala/viper/silver/ast/utility/Expressions.scala

+4-3
Original file line numberDiff line numberDiff line change
@@ -295,9 +295,10 @@ object Expressions {
295295
leftConds ++ guardedRightConds
296296
}
297297

298-
def isForbiddenInTrigger: PartialFunction[Node, Unit] = {
299-
case _: ForbiddenInTrigger =>
300-
case ee: ExtensionExp if ee.extensionIsForbiddenInTrigger() =>
298+
def isForbiddenInTrigger(n: Node): Boolean = n match {
299+
case _: ForbiddenInTrigger => true
300+
case ee: ExtensionExp => ee.extensionIsForbiddenInTrigger()
301+
case _ => false
301302
}
302303

303304
/** See [[viper.silver.ast.utility.Triggers.TriggerGeneration.generateTriggerSetGroups]] */

‎src/main/scala/viper/silver/ast/utility/Triggers.scala

+1-1
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ object Triggers {
3939
/* Note: If Add and Sub were type arguments of GenericTriggerGenerator, the latter
4040
* could implement isForbiddenInTrigger already */
4141
def isForbiddenInTrigger(e: Exp) = (customIsForbiddenInTrigger orElse {
42-
case e if Expressions.isForbiddenInTrigger.isDefinedAt(e) => true
42+
case e if Expressions.isForbiddenInTrigger(e) => true
4343
case _ => false
4444
}: PartialFunction[Exp, Boolean])(e)
4545

‎src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala

+2-2
Original file line numberDiff line numberDiff line change
@@ -207,7 +207,7 @@ case class AdtConstructorApp(name: String, args: Seq[Exp], typVarMap: Map[TypeVa
207207
}
208208
}
209209

210-
override def extensionIsValidTrigger(): Boolean = args.forall(a => !a.existsDefined(Expressions.isForbiddenInTrigger))
210+
override def extensionIsValidTrigger(): Boolean = args.forall(a => !a.exists(Expressions.isForbiddenInTrigger))
211211

212212
override def extensionIsForbiddenInTrigger(): Boolean = false
213213
}
@@ -258,7 +258,7 @@ case class AdtDestructorApp(name: String, rcv: Exp, typVarMap: Map[TypeVar, Type
258258
}
259259
}
260260

261-
override def extensionIsValidTrigger(): Boolean = !rcv.existsDefined(Expressions.isForbiddenInTrigger)
261+
override def extensionIsValidTrigger(): Boolean = !rcv.exists(Expressions.isForbiddenInTrigger)
262262

263263
override def extensionIsForbiddenInTrigger(): Boolean = false
264264
}

0 commit comments

Comments
 (0)
Please sign in to comment.