From 806e7bc4edd3fe3f9e8a23c0dbc4220265c33b77 Mon Sep 17 00:00:00 2001 From: Alexander Steen Date: Sun, 14 Oct 2018 14:54:37 +0200 Subject: [PATCH] clean-up a bit the Main method --- src/main/scala/leo/Configuration.scala | 9 ++-- src/main/scala/leo/Main.scala | 69 ++++++++++---------------- src/main/scala/leo/modules/Modes.scala | 26 ++++++++++ 3 files changed, 58 insertions(+), 46 deletions(-) diff --git a/src/main/scala/leo/Configuration.scala b/src/main/scala/leo/Configuration.scala index 942dd6217..8c395477c 100644 --- a/src/main/scala/leo/Configuration.scala +++ b/src/main/scala/leo/Configuration.scala @@ -1,9 +1,10 @@ package leo import java.util.logging.Level -import java.nio.file.{Path,Files} +import java.nio.file.{Files, Path} -import leo.modules.output.Output +import leo.modules.SZSException +import leo.modules.output.{Output, SZS_UsageError} import leo.modules.parsers.CLParameterParser /** @@ -111,7 +112,7 @@ object Configuration extends DefaultConfiguration { lazy val HELP: Boolean = isSet(PARAM_HELP) lazy val PROBLEMFILE: String = configMap.get(CLParameterParser.ARG0Name) match { - case None => throw new IllegalArgumentException("No problem file given. Aborting.") + case None => throw new SZSException(SZS_UsageError, "No problem file given. Aborting.") case Some(str :: Nil) => str case Some(_) => throw new IllegalArgumentException("This should not happen. Please call support hotline.") } @@ -366,7 +367,7 @@ object Configuration extends DefaultConfiguration { } sb.append(s"\n\t${entry._2._3}\n") } - sb.append("\n") +// sb.append("\n") sb.toString } def help(): Unit = Out.output(helptext) diff --git a/src/main/scala/leo/Main.scala b/src/main/scala/leo/Main.scala index a4292e38b..3f6e8f461 100644 --- a/src/main/scala/leo/Main.scala +++ b/src/main/scala/leo/Main.scala @@ -1,7 +1,8 @@ package leo -import leo.modules._ -import leo.modules.output.{SZS_Error, SZS_Forced, SZS_MemoryOut} +import leo.modules.Modes +import leo.modules.{SZSException, SZSResult, stackTraceAsString} +import leo.modules.output.{SZS_Error, SZS_Forced, SZS_MemoryOut, SZS_UsageError} import leo.modules.parsers.{CLParameterParser, Input} /** @@ -13,36 +14,32 @@ import leo.modules.parsers.{CLParameterParser, Input} */ object Main { private[this] var hook: scala.sys.ShutdownHookThread = _ + final private[this] val MSG_LEO3_STOPPED: String = "Leo-III stopped externally." + final private[this] val MSG_LEO3_GENERAL_ERROR: String = "OUT OF CHEESE ERROR +++ MELON MELON MELON +++ REDO FROM START" - def main(args : Array[String]){ + final def main(args: Array[String]): Unit = { try { val beginTime = System.currentTimeMillis() /** Hook is for returning an szs status if leo3 is killed forcefully. */ hook = sys.addShutdownHook({ Configuration.cleanup() - Out.output(SZSResult(SZS_Forced, Configuration.PROBLEMFILE, "Leo-III stopped externally.")) + Out.output(SZSResult(SZS_Forced, Configuration.PROBLEMFILE, MSG_LEO3_STOPPED)) }) /** Parameter stuff BEGIN */ - try { - Configuration.init(new CLParameterParser(args)) - } catch { - case e: IllegalArgumentException => - Out.severe(e.getMessage) - Configuration.help() - return - } - if (Configuration.PROBLEMFILE == "--caps") { // FIXME: Hacky, redo argument reading + // TODO: Hacky parameter stuff, redo argument processing + Configuration.init(new CLParameterParser(args)) + if (Configuration.PROBLEMFILE == "--caps") { println(Configuration.CAPS) return } - if (Configuration.PROBLEMFILE == s"--${Configuration.PARAM_VERSION}") { // FIXME: Hacky, redo argument reading + if (Configuration.PROBLEMFILE == s"--${Configuration.PARAM_VERSION}") { println(s"Leo-III ${Configuration.VERSION}") return } if (Configuration.HELP || Configuration.PROBLEMFILE == s"-${Configuration.PARAM_HELP}" || - Configuration.PROBLEMFILE == s"--${Configuration.PARAM_USAGE}") { // FIXME: Hacky, redo argument reading + Configuration.PROBLEMFILE == s"--${Configuration.PARAM_USAGE}") { Configuration.help() return } @@ -55,46 +52,34 @@ object Main { } else { // Functionality that need to parse the input file, do it now import leo.modules.parsers.{ModalPreprocessor => Modal, DDLPreprocessor => DDL} + // If "ddl" mode is set (dyadic deontic logic), parse with DDL pre-processor. val problem0 = if (Configuration.isSet("ddl")) DDL.apply(Configuration.PROBLEMFILE) else Input.parseProblemFile(Configuration.PROBLEMFILE) // If it is a logic embedding, call the embedding tool, else just use the problem itself val problem = if (Modal.canApply(problem0)) Modal.apply(problem0) else problem0 - // Functionality calls - if (Configuration.isSet("seq")) { - Modes.seqLoop(beginTime, Configuration.TIMEOUT, problem) - } else if (Configuration.isSet("scheduled")) { - Modes.scheduledSeq(beginTime, Configuration.TIMEOUT, problem) - } else if (Configuration.isSet("pure-ext")) { - Modes.runExternalProver(problem) - } else if (Configuration.isSet("rules")) { - Modes.agentRuleRun(beginTime, problem) - } else if (Configuration.isSet("par")) { - Modes.runParallel(beginTime, problem) - } else if (Configuration.isSet("scheduled-par")) { - Modes.runMultiSearch(beginTime, problem) - } else if (Configuration.isSet("processOnly")) { - Modes.normalizationOnly(problem) - } else if (Configuration.isSet("syntaxcheck")) { - Modes.syntaxCheck(problem) - } else if (Configuration.isSet("typecheck")) { - Modes.typeCheck(problem) - } else if (Configuration.isSet("toTHF")) { - Modes.toTHF(problem) - } else { - Modes.seqLoop(beginTime, Configuration.TIMEOUT, problem) - } + // Invoke concrete mode + Modes.apply(beginTime, problem) } /** Call concrete functionality END */ } catch { /** Handle all top-level errors BEGIN */ case e:Throwable => - Out.comment("OUT OF CHEESE ERROR +++ MELON MELON MELON +++ REDO FROM START") + Out.comment(MSG_LEO3_GENERAL_ERROR) e match { case e0: SZSException => - Out.output(SZSResult(e0.status, Configuration.PROBLEMFILE,e0.getMessage)) - Out.debug(e0.debugMessage) + e0.status match { + case SZS_UsageError => + // Happens only if no problem file was given. Syntax/semantics/input errors are + // handled separately + Out.output(SZSResult(e0.status, "" ,e0.getMessage)) + println() + Configuration.help() + case s => + Out.output(SZSResult(s, Configuration.PROBLEMFILE,e0.getMessage)) + Out.debug(e0.debugMessage) + } case e0: OutOfMemoryError => Out.output(SZSResult(SZS_MemoryOut, Configuration.PROBLEMFILE, e0.toString)) case _ => Out.output(SZSResult(SZS_Error, Configuration.PROBLEMFILE,e.toString)) diff --git a/src/main/scala/leo/modules/Modes.scala b/src/main/scala/leo/modules/Modes.scala index 662720dcb..a59c6a31b 100644 --- a/src/main/scala/leo/modules/Modes.scala +++ b/src/main/scala/leo/modules/Modes.scala @@ -7,6 +7,32 @@ import leo.modules.output._ import leo.modules.parsers.Input object Modes { + final def apply(beginTime: Long, parsedProblem: Seq[AnnotatedFormula]): Unit = { + val timeout = Configuration.TIMEOUT + if (Configuration.isSet("seq")) { + seqLoop(beginTime, timeout, parsedProblem) + } else if (Configuration.isSet("scheduled")) { + scheduledSeq(beginTime, timeout, parsedProblem) + } else if (Configuration.isSet("pure-ext")) { + runExternalProver(parsedProblem) + } else if (Configuration.isSet("rules")) { + agentRuleRun(beginTime, parsedProblem) + } else if (Configuration.isSet("par")) { + runParallel(beginTime, parsedProblem) + } else if (Configuration.isSet("scheduled-par")) { + runMultiSearch(beginTime, parsedProblem) + } else if (Configuration.isSet("processOnly")) { + normalizationOnly(parsedProblem) + } else if (Configuration.isSet("syntaxcheck")) { + syntaxCheck(parsedProblem) + } else if (Configuration.isSet("typecheck")) { + typeCheck(parsedProblem) + } else if (Configuration.isSet("toTHF")) { + toTHF(parsedProblem) + } else { + seqLoop(beginTime, timeout, parsedProblem) + } + } final def toTHF(parsedProblem: scala.Seq[AnnotatedFormula]): Unit = { implicit val sig: Signature = Signature.freshWithHOL()