From 5751f6c8b5ea5ff53cf3298182ca0e6285adcc71 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Wed, 10 Aug 2016 22:38:38 +0200
Subject: [PATCH] Operator follows same abstraction principle as NAryType

---
 src/main/scala/inox/ast/ExprOps.scala    |  2 +-
 src/main/scala/inox/ast/Extractors.scala | 20 ++++++++++++++++----
 src/main/scala/inox/ast/Types.scala      |  4 ++++
 src/main/scala/inox/package.scala        |  9 ++++++---
 4 files changed, 27 insertions(+), 8 deletions(-)

diff --git a/src/main/scala/inox/ast/ExprOps.scala b/src/main/scala/inox/ast/ExprOps.scala
index 0eb453a06..4f3bf2a7d 100644
--- a/src/main/scala/inox/ast/ExprOps.scala
+++ b/src/main/scala/inox/ast/ExprOps.scala
@@ -32,7 +32,7 @@ trait ExprOps extends GenTreeOps {
   type Source = Expr
   type Target = Expr
 
-  val Deconstructor = Operator
+  lazy val Deconstructor = Operator
 
   /** Replaces bottom-up variables by looking up for them in a map */
   def replaceFromSymbols[V <: VariableSymbol](substs: Map[V, Expr], expr: Expr)(implicit ev: VariableConverter[V]): Expr = {
diff --git a/src/main/scala/inox/ast/Extractors.scala b/src/main/scala/inox/ast/Extractors.scala
index d2af32ea8..9a235fa84 100644
--- a/src/main/scala/inox/ast/Extractors.scala
+++ b/src/main/scala/inox/ast/Extractors.scala
@@ -239,11 +239,23 @@ trait Extractors { self: Trees =>
     * tools for performing tree transformations that are very predictable, if
     * one need to simplify the tree, it is easy to write/call a simplification
     * function that would simply apply the corresponding constructor for each node.
+    *
+    * XXX: ideally, we would want [[Operator]] to be defined as
+    * {{{
+    *   val Operator: ExprDeconstructor {
+    *     val s: self.type
+    *     val t: self.type
+    *   }
+    * }}}
+    * however the Scala compiler seems to have some bug with this and reports
+    * wrong errors when we define it this way...
+    * @see https://issues.scala-lang.org/browse/SI-9247
     */
-
-  object Operator extends ExprDeconstructor {
-    val s: self.type = self
-    val t: self.type = self
+  val Operator: TreeExtractor {
+    val s: self.type
+    val t: self.type
+    type Source = self.Expr
+    type Target = self.Expr
   }
 
   object TopLevelOrs { // expr1 OR (expr2 OR (expr3 OR ..)) => List(expr1, expr2, expr3)
diff --git a/src/main/scala/inox/ast/Types.scala b/src/main/scala/inox/ast/Types.scala
index 1de21b0c0..a8767c3ae 100644
--- a/src/main/scala/inox/ast/Types.scala
+++ b/src/main/scala/inox/ast/Types.scala
@@ -85,6 +85,10 @@ trait Types { self: Trees =>
     def tcd(implicit s: Symbols): TypedClassDef = s.getClass(id, tps)
   }
 
+  /** NAryType extractor to extract any Type in a consistent way.
+    *
+    * @see [[Extractors.Operator]] about why we can't have nice(r) things
+    */
   val NAryType: TreeExtractor {
     val s: self.type
     val t: self.type
diff --git a/src/main/scala/inox/package.scala b/src/main/scala/inox/package.scala
index 3fec7b228..6f67768b0 100644
--- a/src/main/scala/inox/package.scala
+++ b/src/main/scala/inox/package.scala
@@ -1,7 +1,5 @@
 /* Copyright 2009-2016 EPFL, Lausanne */
 
-import inox.ast.TypeDeconstructor
-
 /** Core package of the Inox solving interface
   *
   * == Structure ==
@@ -45,10 +43,15 @@ package object inox {
 
   object trees extends ast.Trees {
 
+    object Operator extends {
+      protected val s: trees.type = trees
+      protected val t: trees.type = trees
+    } with ast.ExprDeconstructor
+
     object NAryType extends {
       protected val s: trees.type = trees
       protected val t: trees.type = trees
-    } with TypeDeconstructor
+    } with ast.TypeDeconstructor
 
     class Symbols(
       val functions: Map[Identifier, FunDef],
-- 
GitLab