/* Copyright 2009-2014 EPFL, Lausanne */

package leon
package synthesis
package rules

import purescala.Expressions._
import purescala.Constructors._

case object InnerCaseSplit extends Rule("Inner-Case-Split"){
  def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
    p.phi match {
      case Or(_) =>
        // Inapplicable in this case, normal case-split has precedence here.
        Nil
      case _ =>
        var phi = p.phi
        phi match {
          case Not(And(es)) =>
            phi = orJoin(es.map(not))
            
          case Not(Or(es)) =>
            phi = andJoin(es.map(not))

          case _ =>
        }

        phi match {
          case Or(os) =>
            List(rules.CaseSplit.split(os, "Inner case-split"))

          case And(as) =>
            val optapp = for ((a, i) <- as.zipWithIndex) yield {
              a match {
                case Or(os) =>
                  Some(rules.CaseSplit.split(os.map(o => andJoin(as.updated(i, o))), "Inner case-split"))

                case _ =>
                  None
              }
            }

            optapp.flatten

          case e =>
            Nil
        }
    }
  }

}