Change reconstruction in DetupleInput

Use a LetPattern

Also reenable printing of LetPattern

src/main/scala/leon/purescala/PrettyPrinter.scala

@@ -392,11 +392,9 @@ class PrettyPrinter(opts: PrinterOptions,
               |}"""
         }
 
-      /*
       case LetPattern(p,s,rhs) =>
         p"""|val $p = $s
             |$rhs"""
-      */
 
       case MatchExpr(s, csc) =>
         optP {

src/main/scala/leon/synthesis/rules/DetupleInput.scala

@@ -8,8 +8,9 @@ import Witnesses.Hint
 import purescala.Expressions._
 import purescala.Common._
 import purescala.Types._
-import purescala.ExprOps._
+import purescala.ExprOps.simplePostTransform
 import purescala.Constructors._
+import purescala.Extractors.LetPattern
 
 /** Rule for detupling input variables, to be able to use their sub-expressions. For example, the input variable:
   * {{{d: Cons(head: Int, tail: List)}}}
@@ -31,28 +32,24 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
      * into a list of fresh typed identifiers, the tuple of these new identifiers,
      * and the mapping of those identifiers to their respective expressions.
      */
-    def decompose(id: Identifier): (List[Identifier], Expr, Map[Identifier, Expr], Expr => Seq[Expr]) = id.getType match {
+    def decompose(id: Identifier): (List[Identifier], Expr, Expr => Seq[Expr]) = id.getType match {
       case cct @ CaseClassType(ccd, _) if !ccd.isAbstract =>
         val newIds = cct.fields.map{ vd => FreshIdentifier(vd.id.name, vd.getType, true) }
 
-        val map = (ccd.fields zip newIds).map{ case (vd, nid) => nid -> caseClassSelector(cct, Variable(id), vd.id) }.toMap
-
         val tMap: (Expr => Seq[Expr]) = {
           case CaseClass(ccd, fields) => fields
         }
 
-        (newIds.toList, CaseClass(cct, newIds.map(Variable)), map, tMap)
+        (newIds.toList, CaseClass(cct, newIds.map(Variable)), tMap)
 
       case TupleType(ts) =>
         val newIds = ts.zipWithIndex.map{ case (t, i) => FreshIdentifier(id.name+"_"+(i+1), t, true) }
 
-        val map = newIds.zipWithIndex.map{ case (nid, i) => nid -> TupleSelect(Variable(id), i+1) }.toMap
-
         val tMap: (Expr => Seq[Expr]) = {
           case Tuple(fields) => fields
         }
 
-        (newIds.toList, tupleWrap(newIds.map(Variable)), map, tMap)
+        (newIds.toList, tupleWrap(newIds.map(Variable)), tMap)
 
       case _ => sys.error("woot")
     }
@@ -62,21 +59,32 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
       var subPc      = p.pc
       var subWs      = p.ws
       var hints: Seq[Expr] = Nil
-
-      var reverseMap = Map[Identifier, Expr]()
+      var patterns = List[(Identifier, Pattern)]()
+      var revMap = Map[Expr, Expr]().withDefault((e: Expr) => e)
 
       var ebMapInfo = Map[Identifier, Expr => Seq[Expr]]()
 
       val subAs = p.as.map { a =>
         if (isDecomposable(a)) {
-          val (newIds, expr, map, tMap) = decompose(a)
+          val (newIds, expr, tMap) = decompose(a)
 
           subProblem = subst(a -> expr, subProblem)
           subPc      = subst(a -> expr, subPc)
           subWs      = subst(a -> expr, subWs)
+          revMap     += expr -> Variable(a)
           hints      +:= Hint(expr)
 
-          reverseMap ++= map
+          val patts = newIds map (id => WildcardPattern(Some(id)))
+
+          patterns +:= ((
+            a,
+            a.getType match {
+              case TupleType(_) =>
+                TuplePattern(None, patts)
+              case cct: CaseClassType =>
+                CaseClassPattern(None, cct, patts)
+            }
+          ))
 
           ebMapInfo += a -> tMap
 
@@ -99,40 +107,19 @@ case object DetupleInput extends NormalizingRule("Detuple In") {
 
       val newAs = subAs.flatten
 
-      // Recompose CaseClasses and Tuples.
-      // E.g. Cons(l.head, l.tail) ~~> l
-      // (t._1, t._2, t._3) ~~> t
-      def recompose(e : Expr) : Expr = e match {
-        case CaseClass(ct, args) =>
-          val (cts, es) = args.zip(ct.fields).map { 
-            case (CaseClassSelector(ct, e, id), field) if field.id == id => (ct, e)
-            case _ =>
-              return e
-          }.unzip
-
-          if (cts.distinct.size == 1 && es.distinct.size == 1) {
-            es.head
-          } else {
-            e
-          }
-        case Tuple(args) =>
-          val es = args.zipWithIndex.map {
-            case (TupleSelect(e, i), index) if i == index + 1 => e
-            case _ => return e
-          }
-          if (es.distinct.size == 1) {
-            es.head
-          } else {
-            e
-          }
-        case other => other
-      }
-      
+      val (as, patts) = patterns.unzip
+
       val sub = Problem(newAs, subWs, subPc, subProblem, p.xs, eb).withWs(hints)
 
-      val s = (substAll(reverseMap, _:Expr)) andThen simplePostTransform(recompose)
+      val s = { (e: Expr) =>
+        LetPattern(
+          tuplePatternWrap(patts),
+          tupleWrap(as map Variable),
+          simplePostTransform(revMap)(e)
+        )
+      }
      
-      Some(decomp(List(sub), forwardMap(s), s"Detuple ${reverseMap.keySet.mkString(", ")}"))
+      Some(decomp(List(sub), forwardMap(s), s"Detuple ${as.mkString(", ")}"))
     } else {
       None
     }