Remove Let/LetTuple madness, rely on constructors

src/main/scala/leon/synthesis/ConvertHoles.scala

@@ -8,6 +8,7 @@ import purescala.Trees._
 import purescala.TypeTrees._
 import purescala.TreeOps._
 import purescala.Definitions._
+import purescala.Constructors._
 
 object ConvertHoles extends LeonPhase[Program, Program] {
   val name        = "Convert Holes to Choose"
@@ -62,11 +63,7 @@ object ConvertHoles extends LeonPhase[Program, Program] {
               BooleanLiteral(true)
           }
 
-          val withChoose = if (holes.size > 1) {
-            LetTuple(holes, Choose(cids, pred), newBody)
-          } else {
-            Let(holes.head, Choose(cids, pred), newBody)
-          }
+          val withChoose = letTuple(holes, Choose(cids, pred), newBody)
 
           fd.body = Some(withChoose)
         }

src/main/scala/leon/synthesis/ConvertWithOracles.scala

@@ -7,6 +7,7 @@ import purescala.Common._
 import purescala.Trees._
 import purescala.TreeOps._
 import purescala.Definitions._
+import purescala.Constructors._
 
 object ConvertWithOracle extends LeonPhase[Program, Program] {
   val name        = "Convert WithOracle to Choose"
@@ -53,11 +54,7 @@ object ConvertWithOracle extends LeonPhase[Program, Program] {
                     BooleanLiteral(true)
                 }
 
-                if (chooseOs.size > 1) {
-                  Some(LetTuple(os, Choose(chooseOs, pred), b))
-                } else {
-                  Some(Let(os.head, Choose(chooseOs, pred), b))
-                }
+                Some(letTuple(os, Choose(chooseOs, pred), b))
               case None =>
                 None
             }

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

@@ -10,6 +10,7 @@ import purescala.Common._
 import purescala.TypeTrees._
 import purescala.TreeOps._
 import purescala.Extractors._
+import purescala.Constructors._
 
 case object DetupleOutput extends Rule("Detuple Out") {
 
@@ -39,13 +40,12 @@ case object DetupleOutput extends Rule("Detuple Out") {
       }.unzip
 
       val newOuts = subOuts.flatten
-      //sctx.reporter.warning("newOuts: " + newOuts.toString)
 
       val sub = Problem(p.as, p.pc, subProblem, newOuts)
 
       val onSuccess: List[Solution] => Option[Solution] = {
         case List(sol) =>
-          Some(Solution(sol.pre, sol.defs, LetTuple(newOuts, sol.term, Tuple(outerOuts))))
+          Some(Solution(sol.pre, sol.defs, letTuple(newOuts, sol.term, Tuple(outerOuts))))
         case _ =>
           None
       }

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

@@ -8,6 +8,7 @@ import purescala.Common._
 import purescala.Trees._
 import purescala.TreeOps._
 import purescala.Extractors._
+import purescala.Constructors._
 
 case object OnePoint extends NormalizingRule("One-point") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
@@ -32,14 +33,9 @@ case object OnePoint extends NormalizingRule("One-point") {
 
       val newProblem = Problem(p.as, p.pc, subst(x -> e, And(others)), oxs)
 
-      val onSuccess: List[Solution] => Option[Solution] = { 
+      val onSuccess: List[Solution] => Option[Solution] = {
         case List(Solution(pre, defs, term)) =>
-          if (oxs.isEmpty) {
-            Some(Solution(pre, defs, Tuple(e :: Nil)))
-          } else {
-            Some(Solution(pre, defs, LetTuple(oxs, term, subst(x -> e, Tuple(p.xs.map(Variable(_)))))))
-          }
-
+          Some(Solution(pre, defs, letTuple(oxs, term, subst(x -> e, Tuple(p.xs.map(Variable(_)))))))
         case _ =>
           None
       }

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

@@ -7,6 +7,7 @@ package rules
 import purescala.Trees._
 import purescala.TreeOps._
 import purescala.Extractors._
+import purescala.Constructors._
 
 case object UnconstrainedOutput extends NormalizingRule("Unconstr.Output") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
@@ -17,13 +18,8 @@ case object UnconstrainedOutput extends NormalizingRule("Unconstr.Output") {
 
       val onSuccess: List[Solution] => Option[Solution] = { 
         case List(s) =>
-          val term = if (sub.xs.size > 1) {
-            LetTuple(sub.xs, s.term, Tuple(p.xs.map(id => if (unconstr(id)) simplestValue(id.getType) else Variable(id))))
-          } else if (sub.xs.size == 1) {
-            Let(sub.xs.head, s.term, Tuple(p.xs.map(id => if (unconstr(id)) simplestValue(id.getType) else Variable(id))))
-          } else {
-            Tuple(p.xs.map(id => simplestValue(id.getType)))
-          }
+          val term = letTuple(sub.xs, s.term, Tuple(p.xs.map(id => if (unconstr(id)) simplestValue(id.getType) else Variable(id))))
+
           Some(Solution(s.pre, s.defs, term))
         case _ =>
           None