From 7468240773043d81ead16072c2386452d701a5bd Mon Sep 17 00:00:00 2001
From: Marco Eilers <eilers.marco@googlemail.com>
Date: Thu, 12 Sep 2024 16:56:12 +0200
Subject: [PATCH] Remove withPerm from interface of quantified chunks

---
 src/main/scala/interfaces/state/Chunks.scala | 4 +---
 src/main/scala/state/Chunks.scala            | 5 +----
 2 files changed, 2 insertions(+), 7 deletions(-)

diff --git a/src/main/scala/interfaces/state/Chunks.scala b/src/main/scala/interfaces/state/Chunks.scala
index 521ed7ac..6923efaa 100644
--- 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
 }
\ No newline at end of file
diff --git a/src/main/scala/state/Chunks.scala b/src/main/scala/state/Chunks.scala
index 53a65735..94b044ab 100644
--- 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"