Translate errors from logic system to Natures system.

This commit is contained in:
Mark Harrah 2014-01-24 14:19:18 -05:00
parent 5add7306c2
commit 1afd1931c4
4 changed files with 51 additions and 27 deletions

View File

@ -1,6 +1,7 @@
package sbt
import logic.{Atom, Clause, Clauses, Formula, Literal, Logic}
import logic.{Atom, Clause, Clauses, Formula, Literal, Logic, Negated}
import Logic.{CyclicNegation, InitialContradictions, InitialOverlap, LogicException}
import Def.Setting
import Natures._
@ -75,6 +76,11 @@ abstract class AutoPlugin
// TODO?: def commands: Seq[Command]
}
final class AutoPluginException(val origin: LogicException, prefix: String) extends RuntimeException(prefix + Natures.translateMessage(origin)) {
def withPrefix(p: String) = new AutoPluginException(origin, p)
}
/** An expression that matches `Nature`s. */
sealed trait Natures {
def && (o: Basic): Natures
@ -101,14 +107,24 @@ object Natures
{
val byAtom = defined.map(x => (Atom(x.provides.label), x)).toMap
val clauses = Clauses( defined.map(d => asClause(d)) )
requestedNatures => {
val results = Logic.reduce(clauses, flatten(requestedNatures).toSet)
// results includes the originally requested (positive) atoms,
// which won't have a corresponding AutoPlugin to map back to
results.ordered.flatMap(a => byAtom.get(a).toList)
}
requestedNatures =>
Logic.reduce(clauses, flatten(requestedNatures).toSet) match {
case Left(problem) => throw new AutoPluginException(problem, "")
case Right(results) =>
// results includes the originally requested (positive) atoms,
// which won't have a corresponding AutoPlugin to map back to
results.ordered.flatMap(a => byAtom.get(a).toList)
}
}
private[sbt] def translateMessage(e: LogicException) = e match {
case ic: InitialContradictions => s"Contradiction in selected natures. These natures were both included and excluded: ${literalsString(ic.literals.toSeq)}"
case io: InitialOverlap => s"Cannot directly enable plugins. Plugins are enabled when their required natures are satisifed. The directly selected plugins were: ${literalsString(io.literals.toSeq)}"
case cn: CyclicNegation => s"Cycles in plugin requirements cannot involve excludes. The problematic cycle is: ${literalsString(cn.cycle)}"
}
private[this] def literalsString(lits: Seq[Literal]): String =
lits map { case Atom(l) => l; case Negated(Atom(l)) => l } mkString(", ")
/** [[Natures]] instance that doesn't require any [[Nature]]s. */
def empty: Natures = Empty
private[sbt] final object Empty extends Natures {

View File

@ -6,11 +6,10 @@ package sbt
import java.io.File
import java.net.{URI,URL}
import compiler.{Eval,EvalImports}
import xsbti.compile.CompileOrder
import classpath.ClasspathUtilities
import scala.annotation.tailrec
import collection.mutable
import Compiler.{Compilers,Inputs}
import Compiler.Compilers
import inc.{FileValueCache, Locate}
import Project.{inScope,makeSettings}
import Def.{isDummy, ScopedKey, ScopeLocal, Setting}
@ -463,7 +462,9 @@ object Load
def loadSbtFiles(auto: AddSettings, base: File, autoPlugins: Seq[AutoPlugin]): LoadedSbtFile =
loadSettings(auto, base, plugins, eval, injectSettings, memoSettings, autoPlugins)
def loadForProjects = newProjects map { project =>
val autoPlugins = plugins.detected.compileNatures(project.natures)
val autoPlugins =
try plugins.detected.compileNatures(project.natures)
catch { case e: AutoPluginException => throw translateAutoPluginException(e, project) }
val autoConfigs = autoPlugins.flatMap(_.projectConfigurations)
val loadedSbtFiles = loadSbtFiles(project.auto, project.base, autoPlugins)
val newSettings = (project.settings: Seq[Setting[_]]) ++ loadedSbtFiles.settings
@ -485,6 +486,8 @@ object Load
else
loadTransitive(nextProjects, buildBase, plugins, eval, injectSettings, loadedProjects, memoSettings)
}
private[this] def translateAutoPluginException(e: AutoPluginException, project: Project): AutoPluginException =
e.withPrefix(s"Error determining plugins for project '${project.id}' in ${project.base}:\n")
private[this] def loadSettings(auto: AddSettings, projectBase: File, loadedPlugins: sbt.LoadedPlugins, eval: ()=>Eval, injectSettings: InjectSettings, memoSettings: mutable.Map[File, LoadedSbtFile], autoPlugins: Seq[AutoPlugin]): LoadedSbtFile =
{

View File

@ -88,6 +88,7 @@ object Dag
def visit(nodes: List[B], stack: List[B]): List[B] = nodes match {
case Nil => Nil
case node :: tail =>
def indent = "\t" * stack.size
val atom = toA(node)
if(!visited(atom))
{
@ -102,7 +103,7 @@ object Dag
else if(!finished(atom))
{
// cycle. If negation is involved, it is an error.
val between = stack.takeWhile(f => toA(f) != atom)
val between = node :: stack.takeWhile(f => toA(f) != atom)
if(between exists isNegated)
between
else

View File

@ -82,22 +82,26 @@ object Formula {
object Logic
{
def reduceAll(clauses: List[Clause], initialFacts: Set[Literal]): Matched = reduce(Clauses(clauses), initialFacts)
def reduceAll(clauses: List[Clause], initialFacts: Set[Literal]): Either[LogicException, Matched] =
reduce(Clauses(clauses), initialFacts)
/** Computes the variables in the unique stable model for the program represented by `clauses` and `initialFacts`.
* `clause` may not have any negative feedback (that is, negation is acyclic)
* and `initialFacts` cannot be in the head of any clauses in `clause`.
* These restrictions ensure that the logic program has a unique minimal model. */
def reduce(clauses: Clauses, initialFacts: Set[Literal]): Matched =
def reduce(clauses: Clauses, initialFacts: Set[Literal]): Either[LogicException, Matched] =
{
val (posSeq, negSeq) = separate(initialFacts.toSeq)
val (pos, neg) = (posSeq.toSet, negSeq.toSet)
checkContradictions(pos, neg)
checkOverlap(clauses, pos)
checkAcyclic(clauses)
val problem =
checkContradictions(pos, neg) orElse
checkOverlap(clauses, pos) orElse
checkAcyclic(clauses)
reduce0(clauses, initialFacts, Matched.empty)
problem.toLeft(
reduce0(clauses, initialFacts, Matched.empty)
)
}
@ -105,22 +109,21 @@ object Logic
* This avoids the situation where an atom is proved but no clauses prove it.
* This isn't necessarily a problem, but the main sbt use cases expects
* a proven atom to have at least one clause satisfied. */
def checkOverlap(clauses: Clauses, initialFacts: Set[Atom]) {
private[this] def checkOverlap(clauses: Clauses, initialFacts: Set[Atom]): Option[InitialOverlap] = {
val as = atoms(clauses)
val initialOverlap = initialFacts.filter(as.inHead)
if(initialOverlap.nonEmpty) throw new InitialOverlap(initialOverlap)
if(initialOverlap.nonEmpty) Some(new InitialOverlap(initialOverlap)) else None
}
private[this] def checkContradictions(pos: Set[Atom], neg: Set[Atom]) {
private[this] def checkContradictions(pos: Set[Atom], neg: Set[Atom]): Option[InitialContradictions] = {
val contradictions = pos intersect neg
if(contradictions.nonEmpty) throw new InitialContradictions(contradictions)
if(contradictions.nonEmpty) Some(new InitialContradictions(contradictions)) else None
}
def checkAcyclic(clauses: Clauses) {
private[this] def checkAcyclic(clauses: Clauses): Option[CyclicNegation] = {
val deps = dependencyMap(clauses)
val cycle = Dag.findNegativeCycle(system(deps))(deps.keys.toList)
if(cycle.nonEmpty)
throw new CyclicNegation(cycle)
if(cycle.nonEmpty) Some(new CyclicNegation(cycle)) else None
}
private[this] def system(deps: Map[Atom, Set[Literal]]) = new Dag.System[Atom] {
type B = Literal
@ -139,9 +142,10 @@ object Logic
(m /: heads) { (n, head) => n.updated(head, n.getOrElse(head, Set.empty) ++ deps) }
}
final class InitialContradictions(val literals: Set[Atom]) extends RuntimeException("Initial facts cannot be both true and false:\n\t" + literals.mkString("\n\t"))
final class InitialOverlap(val literals: Set[Atom]) extends RuntimeException("Initial positive facts cannot be implied by any clauses:\n\t" + literals.mkString("\n\t"))
final class CyclicNegation(val cycle: List[Literal]) extends RuntimeException("Negation may not be involved in a cycle:\n\t" + cycle.mkString("\n\t"))
sealed abstract class LogicException(override val toString: String)
final class InitialContradictions(val literals: Set[Atom]) extends LogicException("Initial facts cannot be both true and false:\n\t" + literals.mkString("\n\t"))
final class InitialOverlap(val literals: Set[Atom]) extends LogicException("Initial positive facts cannot be implied by any clauses:\n\t" + literals.mkString("\n\t"))
final class CyclicNegation(val cycle: List[Literal]) extends LogicException("Negation may not be involved in a cycle:\n\t" + cycle.mkString("\n\t"))
/** Tracks proven atoms in the reverse order they were proved. */
final class Matched private(val provenSet: Set[Atom], reverseOrdered: List[Atom]) {