From 965d5f0dde734db5dacf354676bb7422522f87de Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 15 Mar 2016 13:29:53 +0100
Subject: [PATCH] LeonOptions should use Option
---
src/main/scala/leon/GlobalOptions.scala | 15 ++---
src/main/scala/leon/LeonOption.scala | 63 ++++++++++---------
src/main/scala/leon/Main.scala | 19 +++---
.../scala/leon/laziness/LazinessUtil.scala | 9 +--
.../scala/leon/utils/FileOutputPhase.scala | 8 +--
5 files changed, 52 insertions(+), 62 deletions(-)
diff --git a/src/main/scala/leon/GlobalOptions.scala b/src/main/scala/leon/GlobalOptions.scala
index 63648ca33..9632926a6 100644
--- a/src/main/scala/leon/GlobalOptions.scala
+++ b/src/main/scala/leon/GlobalOptions.scala
@@ -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(
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index 642092d0f..d1f93981f 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -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
}
}
}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index c429165e8..02a21c508 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -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]())
)
diff --git a/src/main/scala/leon/laziness/LazinessUtil.scala b/src/main/scala/leon/laziness/LazinessUtil.scala
index f65c385ed..0a9f97035 100644
--- a/src/main/scala/leon/laziness/LazinessUtil.scala
+++ b/src/main/scala/leon/laziness/LazinessUtil.scala
@@ -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()
diff --git a/src/main/scala/leon/utils/FileOutputPhase.scala b/src/main/scala/leon/utils/FileOutputPhase.scala
index 6f2fc3753..140a863ac 100644
--- a/src/main/scala/leon/utils/FileOutputPhase.scala
+++ b/src/main/scala/leon/utils/FileOutputPhase.scala
@@ -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)
--
GitLab