From 161be27f422e2c6d1970018486f127a5a5704ca1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 15 Apr 2016 02:16:57 +0200
Subject: [PATCH] use preMapWithContext to implement preMap
---
.../scala/leon/purescala/GenTreeOps.scala | 19 ++-----------------
1 file changed, 2 insertions(+), 17 deletions(-)
diff --git a/src/main/scala/leon/purescala/GenTreeOps.scala b/src/main/scala/leon/purescala/GenTreeOps.scala
index 2b9f1fcc5..08404ae15 100644
--- a/src/main/scala/leon/purescala/GenTreeOps.scala
+++ b/src/main/scala/leon/purescala/GenTreeOps.scala
@@ -133,23 +133,8 @@ trait GenTreeOps[SubTree <: Tree] {
* @note The mode with applyRec true can diverge if f is not well formed
*/
def preMap(f: SubTree => Option[SubTree], applyRec : Boolean = false)(e: SubTree): SubTree = {
- val rec = preMap(f, applyRec) _
-
- val newV = if (applyRec) {
- // Apply f as long as it returns Some()
- fixpoint { e : SubTree => f(e) getOrElse e } (e)
- } else {
- f(e) getOrElse e
- }
-
- val Deconstructor(es, builder) = newV
- val newEs = es.map(rec)
-
- if ((newEs zip es).exists { case (bef, aft) => aft ne bef }) {
- builder(newEs).copiedFrom(newV)
- } else {
- newV
- }
+ def g(t: SubTree, u: Unit): (Option[SubTree], Unit) = (f(t), ())
+ preMapWithContext[Unit](g, applyRec)(e, ())
}
--
GitLab