Remove withPerm from interface of quantified chunks

viperproject · Sep 12, 2024 · 7468240 · 7468240
1 parent 69cc8aa
commit 7468240
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 7 deletions.
diff --git a/src/main/scala/interfaces/state/Chunks.scala b/src/main/scala/interfaces/state/Chunks.scala
@@ -20,7 +20,6 @@ trait GeneralChunk extends Chunk {
   def applyCondition(newCond: Term): GeneralChunk
   def permMinus(perm: Term): GeneralChunk
   def permPlus(perm: Term): GeneralChunk
-  def withPerm(perm: Term): GeneralChunk
 }
 
 trait NonQuantifiedChunk extends GeneralChunk {
@@ -29,7 +28,7 @@ trait NonQuantifiedChunk extends GeneralChunk {
   override def applyCondition(newCond: Term): NonQuantifiedChunk
   override def permMinus(perm: Term): NonQuantifiedChunk
   override def permPlus(perm: Term): NonQuantifiedChunk
-  override def withPerm(perm: Term): NonQuantifiedChunk
+  def withPerm(perm: Term): NonQuantifiedChunk
   def withSnap(snap: Term): NonQuantifiedChunk
 }
 
@@ -40,6 +39,5 @@ trait QuantifiedChunk extends GeneralChunk {
   override def applyCondition(newCond: Term): QuantifiedChunk
   override def permMinus(perm: Term): QuantifiedChunk
   override def permPlus(perm: Term): QuantifiedChunk
-  override def withPerm(perm: Term): QuantifiedChunk
   def withSnapshotMap(snap: Term): QuantifiedChunk
 }
diff --git a/src/main/scala/state/Chunks.scala b/src/main/scala/state/Chunks.scala
@@ -57,7 +57,6 @@ sealed trait QuantifiedBasicChunk extends QuantifiedChunk {
   override def applyCondition(newCond: Term): QuantifiedBasicChunk
   override def permMinus(perm: Term): QuantifiedBasicChunk
   override def permPlus(perm: Term): QuantifiedBasicChunk
-  override def withPerm(perm: Term): QuantifiedBasicChunk
   override def withSnapshotMap(snap: Term): QuantifiedBasicChunk
   def singletonArguments: Option[Seq[Term]]
   def hints: Seq[Term]
@@ -99,7 +98,6 @@ case class QuantifiedFieldChunk(id: BasicChunkIdentifier,
   override def applyCondition(newCond: Term) = QuantifiedFieldChunk(id, fvf, terms.And(newCond, condition), permValue, invs, singletonRcvr, hints)
   override def permMinus(newPerm: Term) = QuantifiedFieldChunk(id, fvf, condition, PermMinus(permValue, newPerm), invs, singletonRcvr, hints)
   override def permPlus(newPerm: Term) = QuantifiedFieldChunk(id, fvf, condition, PermPlus(permValue, newPerm), invs, singletonRcvr, hints)
-  override def withPerm(newPerm: Term) = throw new RuntimeException("Should not be used with quantified field chunks")
   override def withSnapshotMap(newFvf: Term) = QuantifiedFieldChunk(id, newFvf, condition, permValue, invs, singletonRcvr, hints)
 
   override lazy val toString = s"${terms.Forall} ${`?r`} :: ${`?r`}.$id -> $fvf # $perm"
@@ -129,7 +127,6 @@ case class QuantifiedPredicateChunk(id: BasicChunkIdentifier,
   override def applyCondition(newCond: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, terms.And(newCond, condition), permValue, invs, singletonArgs, hints)
   override def permMinus(newPerm: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, condition, PermMinus(permValue, newPerm), invs, singletonArgs, hints)
   override def permPlus(newPerm: Term) = QuantifiedPredicateChunk(id, quantifiedVars, psf, condition, PermPlus(permValue, newPerm), invs, singletonArgs, hints)
-  override def withPerm(newPerm: Term) = throw new RuntimeException("Should not be used with quantified predicate chunks")
   override def withSnapshotMap(newPsf: Term) = QuantifiedPredicateChunk(id, quantifiedVars, newPsf, condition, permValue, invs, singletonArgs, hints)
 
   override lazy val toString = s"${terms.Forall} ${quantifiedVars.mkString(",")} :: $id(${quantifiedVars.mkString(",")}) -> $psf # $perm"
@@ -157,7 +154,7 @@ case class QuantifiedMagicWandChunk(id: MagicWandIdentifier,
   override def applyCondition(newCond: Term) = withPerm(Ite(newCond, perm, NoPerm))
   override def permMinus(newPerm: Term) = withPerm(PermMinus(perm, newPerm))
   override def permPlus(newPerm: Term) = withPerm(PermPlus(perm, newPerm))
-  override def withPerm(newPerm: Term) = QuantifiedMagicWandChunk(id, quantifiedVars, wsf, newPerm, invs, singletonArgs, hints)
+  def withPerm(newPerm: Term) = QuantifiedMagicWandChunk(id, quantifiedVars, wsf, newPerm, invs, singletonArgs, hints)
   override def withSnapshotMap(newWsf: Term) = QuantifiedMagicWandChunk(id, quantifiedVars, newWsf, perm, invs, singletonArgs, hints)
 
   override lazy val toString = s"${terms.Forall} ${quantifiedVars.mkString(",")} :: $id(${quantifiedVars.mkString(",")}) -> $wsf # $perm"