From fecfef7f5b46b1c4b7e1484ea4b0a9cb470b47ae Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Sun, 23 Oct 2016 22:04:46 +0200
Subject: [PATCH] Better TreeDeconstructor instantiation system
---
src/main/scala/inox/ast/Extractors.scala | 11 ++++++++---
src/main/scala/inox/ast/TreeOps.scala | 17 ++---------------
2 files changed, 10 insertions(+), 18 deletions(-)
diff --git a/src/main/scala/inox/ast/Extractors.scala b/src/main/scala/inox/ast/Extractors.scala
index 4582f9cb0..f7e261e88 100644
--- a/src/main/scala/inox/ast/Extractors.scala
+++ b/src/main/scala/inox/ast/Extractors.scala
@@ -231,14 +231,19 @@ trait TreeDeconstructor {
* [[TreeDeconstructor]] instance. */
trait Extractors { self: Trees =>
- val deconstructor: TreeDeconstructor {
+ def getDeconstructor(that: Trees): TreeDeconstructor {
val s: self.type
- val t: self.type
+ val t: that.type
} = new TreeDeconstructor {
protected val s: self.type = self
- protected val t: self.type = self
+ protected val t: that.type = that
}
+ val deconstructor: TreeDeconstructor {
+ val s: self.type
+ val t: self.type
+ } = getDeconstructor(self)
+
/** Operator Extractor to extract any Expression in a consistent way.
*
* You can match on any Inox Expr, and then get both a Seq[Expr] of
diff --git a/src/main/scala/inox/ast/TreeOps.scala b/src/main/scala/inox/ast/TreeOps.scala
index 5aeeef5aa..7116a0ee9 100644
--- a/src/main/scala/inox/ast/TreeOps.scala
+++ b/src/main/scala/inox/ast/TreeOps.scala
@@ -12,11 +12,6 @@ trait TreeOps { self: Trees =>
trait SelfTreeTransformer extends TreeTransformer {
val s: self.type = self
val t: self.type = self
-
- lazy val deconstructor: TreeDeconstructor {
- val s: self.type
- val t: self.type
- } = self.deconstructor
}
trait IdentityTreeTransformer extends SelfTreeTransformer {
@@ -57,10 +52,10 @@ trait TreeTransformer {
val s: Trees
val t: Trees
- val deconstructor: TreeDeconstructor {
+ lazy val deconstructor: TreeDeconstructor {
val s: TreeTransformer.this.s.type
val t: TreeTransformer.this.t.type
- }
+ } = s.getDeconstructor(t)
def transform(id: Identifier, tpe: s.Type): (Identifier, t.Type) = (id, transform(tpe))
@@ -231,14 +226,6 @@ trait TreeTransformer {
} = new TreeTransformerComposition {
val t1: TreeTransformer.this.type = TreeTransformer.this
val t2: that.type = that
-
- lazy val deconstructor: TreeDeconstructor {
- val s: TreeTransformer.this.s.type
- val t: that.t.type
- } = new TreeDeconstructor {
- protected val s: TreeTransformer.this.s.type = TreeTransformer.this.s
- protected val t: that.t.type = that.t
- }
}
}
--
GitLab