Make interface nicer for overrides

epfl-lara · Feb 17, 2021 · d94cfd6 · d94cfd6
1 parent 6048f68
commit d94cfd6
Showing 1 changed file with 2 additions and 9 deletions.
diff --git a/src/main/scala/inox/ast/ExprOps.scala b/src/main/scala/inox/ast/ExprOps.scala
@@ -69,7 +69,7 @@ trait ExprOps extends GenTreeOps {
     * Note that we don't freshen choose ids as these are considered global
     * and used to lookup their images within models!
     */
-  class Freshener(freshenChooses: Boolean = false) extends SelfTransformer {
+  protected class Freshener(freshenChooses: Boolean) extends SelfTransformer {
     type Env = Map[Identifier, Identifier]
 
     override def transform(id: Identifier, env: Env): Identifier = {
@@ -97,9 +97,6 @@ trait ExprOps extends GenTreeOps {
         }
         Forall(sparams, transform(b, senv)).copiedFrom(e)
 
-      case Choose(vd, pred) if !freshenChooses =>
-        Choose(transform(vd, env), transform(pred, env)).copiedFrom(e)
-
       case Choose(vd, pred) if freshenChooses =>
         val freshVd = vd.freshen
         Choose(transform(freshVd, env), transform(pred, env.updated(vd.id, freshVd.id))).copiedFrom(e)
@@ -133,12 +130,8 @@ trait ExprOps extends GenTreeOps {
     }
   }
 
-  val freshenerNoChooses = new Freshener(false)
-  val freshenerWithChooses = new Freshener(true)
-
   def freshenLocals(expr: Expr, freshenChooses: Boolean = false): Expr = {
-    if (freshenChooses) freshenerWithChooses.transform(expr, Map.empty[Identifier, Identifier])
-    else freshenerNoChooses.transform(expr, Map.empty[Identifier, Identifier])
+    new Freshener(freshenChooses).transform(expr, Map.empty[Identifier, Identifier])
   }
 
   /** Returns true if the expression contains a function call */