package leon
package plugin

import scala.tools.nsc
import scala.tools.nsc.{Global,Phase}
import scala.tools.nsc.plugins.{Plugin,PluginComponent}
import purescala.Definitions.Program

/** This class is the entry point for the plugin. */
class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=>Unit] = None) extends Plugin {
  import global._

  val name = "leon"
  val description = "The Leon static analyzer"

  var stopAfterAnalysis: Boolean = true
  var stopAfterExtraction: Boolean = false
  var silentlyTolerateNonPureBodies: Boolean = false

  /** The help message displaying the options for that plugin. */
  override val optionsHelp: Option[String] = Some(
    "  --uniqid             When pretty-printing purescala trees, show identifiers IDs" + "\n" +
    "  --with-code          Allows the compiler to keep running after the static analysis" + "\n" +
    "  --parse              Checks only whether the program is valid PureScala" + "\n" +
    "  --extensions=ex1:... Specifies a list of qualified class names of extensions to be loaded" + "\n" +
    "  --nodefaults         Runs only the analyses provided by the extensions" + "\n" +
    "  --functions=fun1:... Only generates verification conditions for the specified functions" + "\n" +
    "  --unrolling=[0,1,2]  Unrolling depth for recursive functions" + "\n" + 
    "  --axioms             Generate simple forall axioms for recursive functions when possible" + "\n" + 
    "  --tolerant           Silently extracts non-pure function bodies as ''unknown''" + "\n" +
    "  --bapa               Use BAPA Z3 extension (incompatible with many other things)" + "\n" +
    "  --impure             Generate testcases only for impure functions" + "\n" +
    "  --testcases=[1,2]    Number of testcases to generate per function" + "\n" +
    "  --testbounds=l:u     Lower and upper bounds for integers in recursive datatypes" + "\n" +
    "  --timeout=N          Sets a timeout of N seconds" + "\n" +
    "  --XP                 Enable weird transformations and other bug-producing features" + "\n" +
    "  --BV                 Use bit-vectors for integers" + "\n" +
    "  --prune              Use additional SMT queries to rule out some unrollings" + "\n" +
    "  --cores              Use UNSAT cores in the unrolling/refinement step" + "\n" +
    "  --quickcheck         Use QuickCheck-like random search" + "\n" +
    "  --parallel           Run all solvers in parallel" + "\n" +
    "  --noLuckyTests       Do not perform additional tests to potentially find models early" + "\n" +
    "  --verbose            Print debugging informations"
  )

  /** Processes the command-line options. */
  private def splitList(lst: String) : Seq[String] = lst.split(':').map(_.trim).filter(!_.isEmpty)
  override def processOptions(options: List[String], error: String => Unit) {
    for(option <- options) {
      option match {
        case "with-code"  =>                     stopAfterAnalysis = false
        case "uniqid"     =>                     leon.Settings.showIDs = true
        case "parse"      =>                     stopAfterExtraction = true
        case "tolerant"   =>                     silentlyTolerateNonPureBodies = true
        case "nodefaults" =>                     leon.Settings.runDefaultExtensions = false
        case "axioms"     =>                     leon.Settings.noForallAxioms = false
        case "bapa"       =>                     leon.Settings.useBAPA = true
        case "impure"     =>                     leon.Settings.impureTestcases = true
        case "XP"         =>                     leon.Settings.experimental = true
        case "BV"         =>                     leon.Settings.bitvectorBitwidth = Some(32)
        case "prune"      =>                     leon.Settings.pruneBranches = true
        case "cores"      =>                     leon.Settings.useCores = true
        case "quickcheck" =>                     leon.Settings.useQuickCheck = true
        case "parallel"   =>                     leon.Settings.useParallel = true
        case "noLuckyTests" =>                   leon.Settings.luckyTest = false
        case "verbose"    =>                     leon.Settings.verbose = true
        case s if s.startsWith("unrolling=") =>  leon.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
        case s if s.startsWith("functions=") =>  leon.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
        case s if s.startsWith("extensions=") => leon.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))
        case s if s.startsWith("testbounds=") => leon.Settings.testBounds = try { val l = splitList(s.substring("testBounds=".length, s.length)).map(_.toInt); if (l.size != 2) (0, 3) else (l(0), l(1)) } catch { case _ => (0, 3) }
        case s if s.startsWith("timeout=") => leon.Settings.solverTimeout = try { Some(s.substring("timeout=".length, s.length).toInt) } catch { case _ => None }
        case s if s.startsWith("testcases=") =>  leon.Settings.nbTestcases = try { s.substring("testcases=".length, s.length).toInt } catch { case _ => 1 }
        case _ => error("Invalid option: " + option + "\nValid options are:\n" + optionsHelp.get)
      }
    }
  }

  val components = List[PluginComponent](new AnalysisComponent(global, this))
  val descriptions = List[String]("leon analyses")
}