Translate substitute

src/main/scala/shine/DPIA/Phrases/Phrase.scala

@@ -139,7 +139,7 @@ object Phrase {
                                                      `for`: Phrase[T1],
                                                      in: Phrase[T2]): Phrase[T2] = {
     var substCounter = 0
-    object Visitor extends VisitAndRebuild.Visitor {
+    object Visitor extends PureTraversal {
       def renaming[X <: PhraseType](p: Phrase[X]): Phrase[X] = {
         case class Renaming(idMap: Map[String, String]) extends VisitAndRebuild.Visitor {
           override def phrase[T <: PhraseType](p: Phrase[T]): Result[Phrase[T]] = p match {
@@ -169,33 +169,33 @@ object Phrase {
         }
         VisitAndRebuild(p, Renaming(Map()))
       }
-      override def phrase[T <: PhraseType](p: Phrase[T]): Result[Phrase[T]] = {
-        p match {
-          case `for` =>
-            val newPh = if (substCounter == 0) ph else renaming(ph)
-            substCounter += 1
-            Stop(newPh.asInstanceOf[Phrase[T]])
-          case Natural(n) =>
-            val v = NatIdentifier(`for` match {
-              case Identifier(name, _) => name
-              case _ => throw new Exception("This should never happen")
-            })
-
-            ph.t match {
-              case ExpType(NatType, _) =>
-                Stop(Natural(Nat.substitute(
-                  Internal.transientNatFromExpr(ph.asInstanceOf[Phrase[ExpType]]).n, v, n)).asInstanceOf[Phrase[T]])
-              case ExpType(IndexType(_), _) =>
-                Stop(Natural(Nat.substitute(
-                  Internal.transientNatFromExpr(ph.asInstanceOf[Phrase[ExpType]]).n, v, n)).asInstanceOf[Phrase[T]])
-              case _ => Continue(p, this)
-            }
-          case _ => Continue(p, this)
-        }
+
+      // override def phrase[T <: PhraseType](p: Phrase[T]): Result[Phrase[T]] = {
+      override def phrase[T <: PhraseType]: Phrase[T] => Pure[Phrase[T]] = p => p match {
+        case `for` =>
+          val newPh = if (substCounter == 0) ph else renaming(ph)
+          substCounter += 1
+          return_(newPh.asInstanceOf[Phrase[T]])
+        case Natural(n) =>
+          val v = NatIdentifier(`for` match {
+            case Identifier(name, _) => name
+            case _ => throw new Exception("This should never happen")
+          })
+
+          ph.t match {
+            case ExpType(NatType, _) =>
+              return_(Natural(Nat.substitute(
+                Internal.transientNatFromExpr(ph.asInstanceOf[Phrase[ExpType]]).n, v, n)).asInstanceOf[Phrase[T]])
+            case ExpType(IndexType(_), _) =>
+              return_(Natural(Nat.substitute(
+                Internal.transientNatFromExpr(ph.asInstanceOf[Phrase[ExpType]]).n, v, n)).asInstanceOf[Phrase[T]])
+            case _ => super.phrase(p)
+          }
+        case _ => super.phrase(p)
       }
     }
 
-    VisitAndRebuild(in, Visitor)
+    Visitor.phrase(in).unwrap
   }
 
   def substitute[T2 <: PhraseType](substitutionMap: Map[Phrase[_], Phrase[_]],