/* Copyright 2009-2013 EPFL, Lausanne */ package leon package synthesis package rules import purescala.Trees._ import purescala.Definitions._ import purescala.Common._ import purescala.TypeTrees._ import purescala.TreeOps._ import purescala.Extractors._ case object DetupleOutput extends Rule("Detuple Out") { def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = { def isDecomposable(id: Identifier) = id.getType match { case CaseClassType(t) if !t.isAbstract => true case _ => false } if (p.xs.exists(isDecomposable)) { var subProblem = p.phi val (subOuts, outerOuts) = p.xs.map { x => if (isDecomposable(x)) { val CaseClassType(ccd @ CaseClassDef(name, _, fields)) = x.getType val newIds = fields.map(vd => FreshIdentifier(vd.id.name, true).setType(vd.getType)) val newCC = CaseClass(ccd, newIds.map(Variable(_))) subProblem = subst(x -> newCC, subProblem) (newIds, newCC) } else { (List(x), Variable(x)) } }.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)))) case _ => None } Some(RuleInstantiation.immediateDecomp(p, this, List(sub), onSuccess, this.name)) } else { Nil } } }