Skip to content
Snippets Groups Projects
Commit 965d5f0d authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

LeonOptions should use Option

parent 5ed87d42
No related branches found
No related tags found
No related merge requests found
......@@ -51,19 +51,16 @@ object GlobalOptions extends LeonComponent {
}
val default = Set[DebugSection]()
val usageRhs = "d1,d2,..."
val debugParser: OptionParser[Set[DebugSection]] = s => {
private val debugParser: OptionParser[Set[DebugSection]] = s => {
if (s == "all") {
DebugSections.all
Some(DebugSections.all)
} else {
DebugSections.all.find(_.name == s) match {
case Some(rs) =>
Set(rs)
case None =>
throw new IllegalArgumentException
}
DebugSections.all.find(_.name == s).map(Set(_))
}
}
val parser: String => Set[DebugSection] = setParser[Set[DebugSection]](debugParser)(_).flatten
val parser: String => Option[Set[DebugSection]] = {
setParser[Set[DebugSection]](debugParser)(_).map(_.flatten)
}
}
val optTimeout = LeonLongOptionDef(
......
......@@ -7,6 +7,8 @@ import OptionParsers._
import purescala.Definitions._
import purescala.DefOps.fullName
import scala.util.Try
abstract class LeonOptionDef[+A] {
val name: String
val description: String
......@@ -22,14 +24,12 @@ abstract class LeonOptionDef[+A] {
}
private def parseValue(s: String)(implicit reporter: Reporter): A = {
try { parser(s) }
catch {
case _ : IllegalArgumentException =>
reporter.fatalError(
s"Invalid option usage: --$name\n" +
"Try 'leon --help' for more information."
)
}
parser(s).getOrElse(
reporter.fatalError(
s"Invalid option usage: --$name\n" +
"Try 'leon --help' for more information."
)
)
}
def parse(s: String)(implicit reporter: Reporter): LeonOption[A] =
......@@ -67,7 +67,7 @@ class LeonOption[+A] private (val optionDef: LeonOptionDef[A], val value: A) {
optionDef.name == this.optionDef.name && value == this.value
case _ => false
}
override def hashCode = optionDef.hashCode
override def hashCode = optionDef.hashCode + value.hashCode
}
object LeonOption {
......@@ -78,20 +78,28 @@ object LeonOption {
}
object OptionParsers {
type OptionParser[A] = String => A
val longParser: OptionParser[Long] = _.toLong
val stringParser: OptionParser[String] = x => x
def booleanParser: OptionParser[Boolean] = {
case "on" | "true" | "yes" | "" => true
case "off" | "false" | "no" => false
case _ => throw new IllegalArgumentException
type OptionParser[A] = String => Option[A]
val longParser: OptionParser[Long] = { s =>
Try(s.toLong).toOption
}
val stringParser: OptionParser[String] = Some(_)
val booleanParser: OptionParser[Boolean] = {
case "on" | "true" | "yes" | "" => Some(true)
case "off" | "false" | "no" => Some(false)
case _ => None
}
def seqParser[A](base: OptionParser[A]): OptionParser[Seq[A]] = s => {
s.split(",").filter(_.nonEmpty).map(base)
@inline def foo: Option[Seq[A]] = Some(
s.split(",")
.filter(_.nonEmpty)
.map(base andThen (_.getOrElse(return None)))
)
foo
}
def setParser[A](base: OptionParser[A]): OptionParser[Set[A]] = s => {
s.split(",").filter(_.nonEmpty).map(base).toSet
def setParser[A](base: OptionParser[A]): OptionParser[Set[A]] = {
seqParser(base)(_).map(_.toSet)
}
}
......@@ -103,9 +111,9 @@ object OptionsHelpers {
private val matcherWithout = s"--(.*)".r
def nameValue(s: String) = s match {
case matcher(name, value) => (name, value)
case matcherWithout(name) => (name, "")
case _ => throw new IllegalArgumentException
case matcher(name, value) => Some(name, value)
case matcherWithout(name) => Some(name, "")
case _ => None
}
// helper for options that include patterns
......@@ -131,7 +139,7 @@ object OptionsHelpers {
Pattern.compile("(.+\\.)?"+p)
}
{ (name: String) => regexPatterns.exists(p => p.matcher(name).matches()) }
(name: String) => regexPatterns.exists(p => p.matcher(name).matches())
}
def fdMatcher(pgm: Program)(patterns: Traversable[String]): FunDef => Boolean = {
......@@ -144,11 +152,8 @@ object OptionsHelpers {
i
case None =>
excluded match {
case Some(f) =>
{ (t: T) => !f(t) }
case None =>
{ (t: T) => true }
case Some(f) => (t: T) => !f(t)
case None => (t: T) => true
}
}
}
......
......@@ -57,7 +57,7 @@ object Main {
val optHelp = LeonFlagOptionDef("help", "Show help message", false)
val optInstrument = LeonFlagOptionDef("instrument", "Instrument the code for inferring time/depth/stack bounds", false)
val optInferInv = LeonFlagOptionDef("inferInv", "Infer invariants from (instrumented) the code", false)
val optLazyEval = LeonFlagOptionDef("lazy", "Handles programs that may use the lazy construct", false)
val optLazyEval = LeonFlagOptionDef("lazy", "Handles programs that may use the 'lazy' construct", false)
val optGenc = LeonFlagOptionDef("genc", "Generate C code", false)
override val definedOptions: Set[LeonOptionDef[Any]] =
......@@ -109,15 +109,13 @@ object Main {
val files = args.filterNot(_.startsWith("-")).map(new java.io.File(_))
val leonOptions: Seq[LeonOption[Any]] = options.map { opt =>
val (name, value) = try {
OptionsHelpers.nameValue(opt)
} catch {
case _: IllegalArgumentException =>
initReporter.fatalError(
s"Malformed option $opt. Options should have the form --name or --name=value")
}
val (name, value) = OptionsHelpers.nameValue(opt).getOrElse(
initReporter.fatalError(
s"Malformed option $opt. Options should have the form --name or --name=value"
)
)
// Find respective LeonOptionDef, or report an unknown option
val df = allOptions.find(_. name == name).getOrElse{
val df = allOptions.find(_.name == name).getOrElse{
initReporter.fatalError(
s"Unknown option: $name\n" +
"Try 'leon --help' for more information."
......@@ -128,7 +126,8 @@ object Main {
val reporter = new DefaultReporter(
leonOptions.collectFirst {
case LeonOption(GlobalOptions.optDebug, sections) => sections.asInstanceOf[Set[DebugSection]]
case LeonOption(GlobalOptions.optDebug, sections) =>
sections.asInstanceOf[Set[DebugSection]]
}.getOrElse(Set[DebugSection]())
)
......
......@@ -11,6 +11,7 @@ import java.io.File
import java.io.FileWriter
import java.io.BufferedWriter
import scala.util.matching.Regex
import utils.FileOutputPhase
object LazinessUtil {
......@@ -19,13 +20,7 @@ object LazinessUtil {
}
def prettyPrintProgramToFile(p: Program, ctx: LeonContext, suffix: String, uniqueIds: Boolean = false) {
val optOutputDirectory = new LeonOptionDef[String] {
val name = "o"
val description = "Output directory"
val default = "leon.out"
val usageRhs = "dir"
val parser = (x: String) => x
}
val optOutputDirectory = FileOutputPhase.optOutputDirectory
val outputFolder = ctx.findOptionOrDefault(optOutputDirectory)
try {
new File(outputFolder).mkdir()
......
......@@ -11,13 +11,7 @@ object FileOutputPhase extends UnitPhase[Program] {
val name = "File output"
val description = "Output parsed/generated program to the specified directory (default: leon.out)"
val optOutputDirectory = new LeonOptionDef[String] {
val name = "o"
val description = "Output directory"
val default = "leon.out"
val usageRhs = "dir"
val parser = (x: String) => x
}
val optOutputDirectory = LeonStringOptionDef("o", "Output directory", "leon.out", "dir")
override val definedOptions: Set[LeonOptionDef[Any]] = Set(optOutputDirectory)
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment