LetIn0Ex splitter

informalsystems · Aug 22, 2019 · 3244b15 · 3244b15
1 parent ab81f04
commit 3244b15
Show file tree

Hide file tree

Showing 2 changed files with 126 additions and 0 deletions.
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/SplitLetIn0.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/SplitLetIn0.scala
@@ -0,0 +1,74 @@
+package at.forsyte.apalache.tla.lir.transformations.standard
+
+import at.forsyte.apalache.tla.lir.{LetIn0Ex, OperEx}
+import at.forsyte.apalache.tla.lir.oper.LetInOper
+import at.forsyte.apalache.tla.lir.transformations.{TlaExTransformation, TransformationTracker}
+
+object SplitLetIn0 {
+  private def splitLetIn( tracker : TransformationTracker ) : TlaExTransformation = tracker.track {
+    case OperEx( oper : LetInOper, body ) =>
+
+      val (arity0, arityGt0) = oper.defs.partition( _.formalParams.isEmpty )
+
+      /** Let-in may be nested */
+      val splitInBody = apply( tracker )( body )
+
+      /** We assume that the operators are parser-ordered correctly, so that
+        *
+        * LET A1 == ...
+        *     ...
+        *     An == ...
+        * IN X
+        *
+        * is equivalent to
+        *
+        * LET A1 == ...
+        * IN (LET A2 == ... IN (... LET An == ... IN X))
+        */
+      val zeroForm = arity0.foldRight( splitInBody ){
+        case (decl, b) => LetIn0Ex( decl.name, decl.body, b )
+      }
+
+      if ( arityGt0.isEmpty )
+        zeroForm
+      else {
+        val newOper = new LetInOper( arityGt0 )
+        OperEx( newOper, zeroForm )
+      }
+    case ex => ex
+  }
+
+  /**
+    * Returns a transformation which replaces all 0-arity LET-IN defined expressions with
+    * the LetIn0Ex syntax.
+    *
+    * Example:
+    * LET X(a) == a + x
+    * Y == 1
+    * IN X(0) > Y
+    * -->
+    * LET X(a) == a + x
+    * IN LetIn0Ex( "Y", 1, X(0) > Y)
+    */
+  def apply( tracker : TransformationTracker ) : TlaExTransformation = tracker.track { ex =>
+    val tr = splitLetIn( tracker )
+    lazy val self = apply( tracker )
+    ex match {
+      case OperEx( op : LetInOper, _ ) =>
+        tr( ex )
+      case LetIn0Ex( name, operBody, exprBody ) =>
+        val newOperBody = self(operBody)
+        val newExprBody = self(exprBody)
+        val newEx =
+          if ( newOperBody == operBody && newExprBody == exprBody ) ex
+          else LetIn0Ex(name, newOperBody, newExprBody)
+        tr( newEx )
+      case ex@OperEx( op, args@_* ) =>
+        val newArgs = args map self
+        val retEx = if ( args == newArgs ) ex else OperEx( op, newArgs : _* )
+        tr( retEx )
+      case _ => tr( ex )
+    }
+  }
+}
+
diff --git a/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTransformations.scala b/tlair/src/test/scala/at/forsyte/apalache/tla/lir/TestTransformations.scala
@@ -347,4 +347,56 @@ class TestTransformations extends FunSuite with TestingPredefs {
     }
   }
 
+  test( "Test SplitLetIn0" ){
+    val transformation = SplitLetIn0( Trackers.NoTracker )
+
+    val pa1 =
+      and( n_x, and( n_y, n_z ) ) ->
+        and( n_x, and( n_y, n_z ) )
+    val pa2 =
+      LetIn0Ex( "X", n_x, appOp( NameEx( "X" ) ) ) ->
+        LetIn0Ex( "X", n_x, appOp( NameEx( "X" ) ) )
+    val pa3 =
+      letIn( appOp( NameEx( "X" ) ), declOp( "X", n_x ) ) ->
+        LetIn0Ex( "X", n_x, appOp( NameEx( "X" ) ) )
+
+    val pa4 =
+      letIn( appOp( NameEx( "X" ), int( 1 ) ), declOp( "X", n_t, "t" ) ) ->
+        letIn( appOp( NameEx( "X" ), int( 1 ) ), declOp( "X", n_t, "t" ) )
+
+    val pa5 =
+      letIn(
+        plus( appOp( NameEx( "X" ) ), appOp( NameEx( "Y" ), int( 1 ) ) ),
+        declOp( "X", n_x ),
+        declOp( "Y", n_t, "t" )
+      ) ->
+        letIn(
+          LetIn0Ex( "X", n_x, plus( appOp( NameEx( "X" ) ), appOp( NameEx( "Y" ), int( 1 ) ) ) ),
+          declOp( "Y", n_t, "t" )
+        )
+
+    val pa6 =
+      letIn(
+        plus( appOp( NameEx( "X" ) ), appOp( NameEx( "Y" ) ) ),
+        declOp( "X", n_x ),
+        declOp( "Y", n_y )
+      ) ->
+        LetIn0Ex(
+          "X",
+          n_x,
+          LetIn0Ex( "Y", n_y, plus( appOp( NameEx( "X" ) ), appOp( NameEx( "Y" ) ) ) )
+        )
+
+    val expected = Seq(
+      pa1, pa2, pa3, pa4, pa5, pa6
+    )
+    val cmp = expected map { case (k, v) =>
+      (v, transformation( k ))
+    }
+    cmp foreach { case (ex, act) =>
+      assert( ex == act )
+    }
+
+  }
+
 }