Propagate expected types to onSuccess

This allows CostModels to estimate correctly the minimal cost of a
applying a rule.

With type information on the expected types of a solution
reconstruction, the cost model can provide dummy values of the correct
type, avoiding assertion errors when composing solutions.

src/main/scala/leon/purescala/TreeOps.scala

@@ -854,6 +854,7 @@ object TreeOps {
       CaseClass(ccd, fields.map(f => simplestValue(f.getType)))
     case SetType(baseType) => FiniteSet(Seq()).setType(tpe)
     case MapType(fromType, toType) => FiniteMap(Seq()).setType(tpe)
+    case TupleType(tpes) => Tuple(tpes.map(simplestValue))
     case _ => throw new Exception("I can't choose simplest value for type " + tpe)
   }
 

src/main/scala/leon/synthesis/CostModel.scala

@@ -12,7 +12,7 @@ abstract class CostModel(val name: String) {
   def problemCost(p: Problem): Cost
 
   def ruleAppCost(app: RuleInstantiation): Cost = new Cost {
-    val subSols = (1 to app.onSuccess.arity).map {i => Solution.simplest }.toList
+    val subSols = app.onSuccess.types.map {t => Solution.simplest(t) }.toList
     val simpleSol = app.onSuccess(subSols)
 
     val value = simpleSol match {

src/main/scala/leon/synthesis/Heuristics.scala

@@ -2,6 +2,7 @@ package leon
 package synthesis
 
 import purescala.Trees._
+import purescala.TypeTrees.TupleType
 
 import heuristics._
 
@@ -38,7 +39,9 @@ object HeuristicInstantiation {
   }
 
   def apply(problem: Problem, rule: Rule, subProblems: List[Problem], onSuccess: List[Solution] => Option[Solution]): RuleInstantiation = {
-    val builder = new SolutionBuilder(subProblems.size) {
+    val subTypes = subProblems.map(p => TupleType(p.xs.map(_.getType)))
+
+    val builder = new SolutionBuilder(subProblems.size, subTypes) {
       def apply(sols: List[Solution]) = {
         onSuccess(sols)
       }

src/main/scala/leon/synthesis/Rules.scala

@@ -3,6 +3,7 @@ package synthesis
 
 import purescala.Common._
 import purescala.Trees._
+import purescala.TypeTrees._
 import purescala.TreeOps._
 import rules._
 
@@ -27,11 +28,13 @@ object Rules {
   )
 }
 
-abstract class SolutionBuilder(val arity: Int) {
+abstract class SolutionBuilder(val arity: Int, val types: Seq[TypeTree]) {
   def apply(sols: List[Solution]): Option[Solution]
+
+  assert(types.size == arity)
 }
 
-class SolutionCombiner(arity: Int, f: List[Solution] => Option[Solution]) extends SolutionBuilder(arity) {
+class SolutionCombiner(arity: Int, types: Seq[TypeTree],  f: List[Solution] => Option[Solution]) extends SolutionBuilder(arity, types) {
   def apply(sols: List[Solution]) = {
     assert(sols.size == arity)
     f(sols)
@@ -39,7 +42,7 @@ class SolutionCombiner(arity: Int, f: List[Solution] => Option[Solution]) extend
 }
 
 object SolutionBuilder {
-  val none = new SolutionBuilder(0) {
+  val none = new SolutionBuilder(0, Seq()) {
     def apply(sols: List[Solution]) = None
   }
 }
@@ -48,14 +51,6 @@ abstract class RuleInstantiation(val problem: Problem, val rule: Rule, val onSuc
   def apply(sctx: SynthesisContext): RuleApplicationResult
 }
 
-//abstract class RuleApplication(val subProblemsCount: Int,
-//                               val onSuccess: List[Solution] => Solution) {
-//
-//  def apply(sctx: SynthesisContext): RuleApplicationResult
-//}
-//
-//abstract class RuleImmediateApplication extends RuleApplication(0, s => Solution.simplest)
-
 sealed abstract class RuleApplicationResult
 case class RuleSuccess(solution: Solution)    extends RuleApplicationResult
 case class RuleDecomposed(sub: List[Problem]) extends RuleApplicationResult
@@ -63,13 +58,15 @@ case object RuleApplicationImpossible         extends RuleApplicationResult
 
 object RuleInstantiation {
   def immediateDecomp(problem: Problem, rule: Rule, sub: List[Problem], onSuccess: List[Solution] => Option[Solution]) = {
-    new RuleInstantiation(problem, rule, new SolutionCombiner(sub.size, onSuccess)) {
+    val subTypes = sub.map(p => TupleType(p.xs.map(_.getType)))
+
+    new RuleInstantiation(problem, rule, new SolutionCombiner(sub.size, subTypes, onSuccess)) {
       def apply(sctx: SynthesisContext) = RuleDecomposed(sub)
     }
   }
 
   def immediateSuccess(problem: Problem, rule: Rule, solution: Solution) = {
-    new RuleInstantiation(problem, rule, new SolutionCombiner(0, ls => Some(solution))) {
+    new RuleInstantiation(problem, rule, new SolutionCombiner(0, Seq(), ls => Some(solution))) {
       def apply(sctx: SynthesisContext) = RuleSuccess(solution)
     }
   }

src/main/scala/leon/synthesis/Solution.scala

@@ -2,6 +2,7 @@ package leon
 package synthesis
 
 import leon.purescala.Trees._
+import leon.purescala.TypeTrees.TypeTree
 import leon.purescala.Definitions._
 import leon.purescala.TreeOps._
 import leon.xlang.Trees.LetDef
@@ -45,7 +46,7 @@ object Solution {
     new Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(id => simplestValue(id.getType))))
   }
 
-  def simplest: Solution = {
-    new Solution(BooleanLiteral(true), Set(), BooleanLiteral(true))
+  def simplest(t: TypeTree): Solution = {
+    new Solution(BooleanLiteral(true), Set(), simplestValue(t))
   }
 }