diff --git a/util/appmacro/src/main/scala/sbt/appmacro/ContextUtil.scala b/util/appmacro/src/main/scala/sbt/appmacro/ContextUtil.scala index 381674e47..fe1baa696 100644 --- a/util/appmacro/src/main/scala/sbt/appmacro/ContextUtil.scala +++ b/util/appmacro/src/main/scala/sbt/appmacro/ContextUtil.scala @@ -32,12 +32,16 @@ object ContextUtil { def unexpectedTree[C <: Context](tree: C#Tree): Nothing = sys.error("Unexpected macro application tree (" + tree.getClass + "): " + tree) } +// TODO 2.11 Remove this after dropping 2.10.x support. +private object HasCompat { val compat = ??? }; import HasCompat._ + /** Utility methods for macros. Several methods assume that the context's universe is a full compiler (`scala.tools.nsc.Global`). * This is not thread safe due to the underlying Context and related data structures not being thread safe. * Use `ContextUtil[c.type](c)` to construct. */ final class ContextUtil[C <: Context](val ctx: C) { import ctx.universe.{Apply=>ApplyTree,_} + import compat._ val powerContext = ctx.asInstanceOf[reflect.macros.runtime.Context] val global: powerContext.universe.type = powerContext.universe @@ -222,17 +226,20 @@ final class ContextUtil[C <: Context](val ctx: C) object appTransformer extends Transformer { override def transform(tree: Tree): Tree = - tree match - { - case ApplyTree(TypeApply(Select(_, nme), targ :: Nil), qual :: Nil) => subWrapper(nme.decoded, targ.tpe, qual, tree) match { - case Converted.Success(t, finalTx) => finalTx(t) - case Converted.Failure(p,m) => ctx.abort(p, m) - case _: Converted.NotApplicable[_] => super.transform(tree) - } + tree match { + case ApplyTree(TypeApply(Select(_, nme), targ :: Nil), qual :: Nil) => + subWrapper(nme.decoded, targ.tpe, qual, tree) match { + case Converted.Success(t, finalTx) => + changeOwner(qual, currentOwner, initialOwner) // Fixes https://github.com/sbt/sbt/issues/1150 + finalTx(t) + case Converted.Failure(p,m) => ctx.abort(p, m) + case _: Converted.NotApplicable[_] => super.transform(tree) + } case _ => super.transform(tree) } } - - appTransformer.transform(t) + appTransformer.atOwner(initialOwner) { + appTransformer.transform(t) + } } -} \ No newline at end of file +} diff --git a/util/appmacro/src/main/scala/sbt/appmacro/Instance.scala b/util/appmacro/src/main/scala/sbt/appmacro/Instance.scala index 0de166b67..043ad8731 100644 --- a/util/appmacro/src/main/scala/sbt/appmacro/Instance.scala +++ b/util/appmacro/src/main/scala/sbt/appmacro/Instance.scala @@ -167,7 +167,7 @@ object Instance def addType(tpe: Type, qual: Tree, selection: Tree): Tree = { qual.foreach(checkQual) - val vd = util.freshValDef(tpe, qual.symbol.pos, functionSym) + val vd = util.freshValDef(tpe, qual.pos, functionSym) inputs ::= new Input(tpe, qual, vd) util.refVal(selection, vd) } diff --git a/util/appmacro/src/main/scala/sbt/appmacro/KListBuilder.scala b/util/appmacro/src/main/scala/sbt/appmacro/KListBuilder.scala index e9fb207d8..d9dbebe42 100644 --- a/util/appmacro/src/main/scala/sbt/appmacro/KListBuilder.scala +++ b/util/appmacro/src/main/scala/sbt/appmacro/KListBuilder.scala @@ -9,11 +9,15 @@ package appmacro /** A `TupleBuilder` that uses a KList as the tuple representation.*/ object KListBuilder extends TupleBuilder { + // TODO 2.11 Remove this after dropping 2.10.x support. + private object HasCompat { val compat = ??? }; import HasCompat._ + def make(c: Context)(mt: c.Type, inputs: Inputs[c.universe.type]): BuilderResult[c.type] = new BuilderResult[c.type] { val ctx: c.type = c val util = ContextUtil[c.type](c) import c.universe.{Apply=>ApplyTree,_} + import compat._ import util._ val knilType = c.typeOf[KNil] @@ -24,7 +28,7 @@ object KListBuilder extends TupleBuilder val kconsTC: Type = kconsTpe.typeConstructor /** This is the L in the type function [L[x]] ... */ - val tcVariable: TypeSymbol = newTCVariable(NoSymbol) + val tcVariable: TypeSymbol = newTCVariable(util.initialOwner) /** Instantiates KCons[h, t <: KList[L], L], where L is the type constructor variable */ def kconsType(h: Type, t: Type): Type = @@ -65,4 +69,4 @@ object KListBuilder extends TupleBuilder val alistInstance: ctx.universe.Tree = TypeApply(select(Ident(alist), "klist"), TypeTree(representationC) :: Nil) def extract(param: ValDef) = bindKList(param, Nil, inputs.map(_.local)) } -} \ No newline at end of file +} diff --git a/util/appmacro/src/main/scala/sbt/appmacro/TupleNBuilder.scala b/util/appmacro/src/main/scala/sbt/appmacro/TupleNBuilder.scala index 89fe31792..28fa581a4 100644 --- a/util/appmacro/src/main/scala/sbt/appmacro/TupleNBuilder.scala +++ b/util/appmacro/src/main/scala/sbt/appmacro/TupleNBuilder.scala @@ -14,10 +14,14 @@ object TupleNBuilder extends TupleBuilder final val MaxInputs = 11 final val TupleMethodName = "tuple" + // TODO 2.11 Remove this after dropping 2.10.x support. + private object HasCompat { val compat = ??? }; import HasCompat._ + def make(c: Context)(mt: c.Type, inputs: Inputs[c.universe.type]): BuilderResult[c.type] = new BuilderResult[c.type] { val util = ContextUtil[c.type](c) import c.universe.{Apply=>ApplyTree,_} + import compat._ import util._ val global: Global = c.universe.asInstanceOf[Global] @@ -25,7 +29,7 @@ object TupleNBuilder extends TupleBuilder val ctx: c.type = c val representationC: PolyType = { - val tcVariable: Symbol = newTCVariable(NoSymbol) + val tcVariable: Symbol = newTCVariable(util.initialOwner) val tupleTypeArgs = inputs.map(in => typeRef(NoPrefix, tcVariable, in.tpe :: Nil).asInstanceOf[global.Type]) val tuple = global.definitions.tupleType(tupleTypeArgs) PolyType(tcVariable :: Nil, tuple.asInstanceOf[Type] ) diff --git a/util/collection/src/main/scala/sbt/Dag.scala b/util/collection/src/main/scala/sbt/Dag.scala index 4250b0f10..f0594ed50 100644 --- a/util/collection/src/main/scala/sbt/Dag.scala +++ b/util/collection/src/main/scala/sbt/Dag.scala @@ -15,7 +15,7 @@ object Dag import JavaConverters.asScalaSetConverter def topologicalSort[T](root: T)(dependencies: T => Iterable[T]): List[T] = topologicalSort(root :: Nil)(dependencies) - + def topologicalSort[T](nodes: Iterable[T])(dependencies: T => Iterable[T]): List[T] = { val discovered = new mutable.HashSet[T] @@ -24,7 +24,7 @@ object Dag def visitAll(nodes: Iterable[T]) = nodes foreach visit def visit(node : T){ if (!discovered(node)) { - discovered(node) = true; + discovered(node) = true; try { visitAll(dependencies(node)); } catch { case c: Cyclic => throw node :: c } finished += node; } @@ -33,11 +33,13 @@ object Dag } visitAll(nodes); - + finished.toList; } // doesn't check for cycles - def topologicalSortUnchecked[T](node: T)(dependencies: T => Iterable[T]): List[T] = + def topologicalSortUnchecked[T](node: T)(dependencies: T => Iterable[T]): List[T] = topologicalSortUnchecked(node :: Nil)(dependencies) + + def topologicalSortUnchecked[T](nodes: Iterable[T])(dependencies: T => Iterable[T]): List[T] = { val discovered = new mutable.HashSet[T] var finished: List[T] = Nil @@ -45,23 +47,23 @@ object Dag def visitAll(nodes: Iterable[T]) = nodes foreach visit def visit(node : T){ if (!discovered(node)) { - discovered(node) = true; + discovered(node) = true; visitAll(dependencies(node)) finished ::= node; } } - visit(node); + visitAll(nodes); finished; } final class Cyclic(val value: Any, val all: List[Any], val complete: Boolean) extends Exception( "Cyclic reference involving " + - (if(complete) all.mkString("\n ", "\n ", "") else value) + (if(complete) all.mkString("\n ", "\n ", "") else value) ) { def this(value: Any) = this(value, value :: Nil, false) override def toString = getMessage - def ::(a: Any): Cyclic = + def ::(a: Any): Cyclic = if(complete) this else if(a == value) @@ -69,5 +71,62 @@ object Dag else new Cyclic(value, a :: all, false) } -} + /** A directed graph with edges labeled positive or negative. */ + private[sbt] trait DirectedSignedGraph[Node] + { + /** Directed edge type that tracks the sign and target (head) vertex. + * The sign can be obtained via [[isNegative]] and the target vertex via [[head]]. */ + type Arrow + /** List of initial nodes. */ + def nodes: List[Arrow] + /** Outgoing edges for `n`. */ + def dependencies(n: Node): List[Arrow] + /** `true` if the edge `a` is "negative", false if it is "positive". */ + def isNegative(a: Arrow): Boolean + /** The target of the directed edge `a`. */ + def head(a: Arrow): Node + } + + /** Traverses a directed graph defined by `graph` looking for a cycle that includes a "negative" edge. + * The directed edges are weighted by the caller as "positive" or "negative". + * If a cycle containing a "negative" edge is detected, its member edges are returned in order. + * Otherwise, the empty list is returned. */ + private[sbt] def findNegativeCycle[Node](graph: DirectedSignedGraph[Node]): List[graph.Arrow] = + { + import scala.annotation.tailrec + import graph._ + val finished = new mutable.HashSet[Node] + val visited = new mutable.HashSet[Node] + + def visit(edges: List[Arrow], stack: List[Arrow]): List[Arrow] = edges match { + case Nil => Nil + case edge :: tail => + val node = head(edge) + if(!visited(node)) + { + visited += node + visit(dependencies(node), edge :: stack) match { + case Nil => + finished += node + visit(tail, stack) + case cycle => cycle + } + } + else if(!finished(node)) + { + // cycle. If a negative edge is involved, it is an error. + val between = edge :: stack.takeWhile(f => head(f) != node) + if(between exists isNegative) + between + else + visit(tail, stack) + } + else + visit(tail, stack) + } + + visit(graph.nodes, Nil) + } + +} diff --git a/util/logic/src/main/scala/sbt/logic/Logic.scala b/util/logic/src/main/scala/sbt/logic/Logic.scala new file mode 100644 index 000000000..4eb8e64b1 --- /dev/null +++ b/util/logic/src/main/scala/sbt/logic/Logic.scala @@ -0,0 +1,325 @@ +package sbt +package logic + + import scala.annotation.tailrec + import Formula.{And, True} + +/* +Defines a propositional logic with negation as failure and only allows stratified rule sets (negation must be acyclic) in order to have a unique minimal model. + +For example, this is not allowed: + + p :- not q + + q :- not p +but this is: + + p :- q + + q :- p +as is this: + + p :- q + + q := not r + + + Some useful links: + + https://en.wikipedia.org/wiki/Nonmonotonic_logic + + https://en.wikipedia.org/wiki/Negation_as_failure + + https://en.wikipedia.org/wiki/Propositional_logic + + https://en.wikipedia.org/wiki/Stable_model_semantics + + http://www.w3.org/2005/rules/wg/wiki/negation +*/ + + +/** Disjunction (or) of the list of clauses. */ +final case class Clauses(clauses: List[Clause]) { + assert(clauses.nonEmpty, "At least one clause is required.") +} + +/** When the `body` Formula succeeds, atoms in `head` are true. */ +final case class Clause(body: Formula, head: Set[Atom]) + +/** A literal is an [[Atom]] or its [[negation|Negated]]. */ +sealed abstract class Literal extends Formula { + /** The underlying (positive) atom. */ + def atom: Atom + /** Negates this literal.*/ + def unary_! : Literal +} +/** A variable with name `label`. */ +final case class Atom(label: String) extends Literal { + def atom = this + def unary_! : Negated = Negated(this) +} +/** A negated atom, in the sense of negation as failure, not logical negation. +* That is, it is true if `atom` is not known/defined. */ +final case class Negated(atom: Atom) extends Literal { + def unary_! : Atom = atom +} + +/** A formula consists of variables, negation, and conjunction (and). +* (Disjunction is not currently included- it is modeled at the level of a sequence of clauses. +* This is less convenient when defining clauses, but is not less powerful.) */ +sealed abstract class Formula { + /** Constructs a clause that proves `atoms` when this formula is true. */ + def proves(atom: Atom, atoms: Atom*): Clause = Clause(this, (atom +: atoms).toSet) + + /** Constructs a formula that is true iff this formula and `f` are both true.*/ + def && (f: Formula): Formula = (this, f) match { + case (True, x) => x + case (x, True) => x + case (And(as), And(bs)) => And(as ++ bs) + case (And(as), b: Literal) => And(as + b) + case (a: Literal, And(bs)) => And(bs + a) + case (a: Literal, b: Literal) => And( Set(a,b) ) + } +} + + +object Formula { + /** A conjunction of literals. */ + final case class And(literals: Set[Literal]) extends Formula { + assert(literals.nonEmpty, "'And' requires at least one literal.") + } + final case object True extends Formula +} + +object Logic +{ + 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]): Either[LogicException, Matched] = + { + val (posSeq, negSeq) = separate(initialFacts.toSeq) + val (pos, neg) = (posSeq.toSet, negSeq.toSet) + + val problem = + checkContradictions(pos, neg) orElse + checkOverlap(clauses, pos) orElse + checkAcyclic(clauses) + + problem.toLeft( + reduce0(clauses, initialFacts, Matched.empty) + ) + } + + + /** Verifies `initialFacts` are not in the head of any `clauses`. + * 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. */ + private[this] def checkOverlap(clauses: Clauses, initialFacts: Set[Atom]): Option[InitialOverlap] = { + val as = atoms(clauses) + val initialOverlap = initialFacts.filter(as.inHead) + if(initialOverlap.nonEmpty) Some(new InitialOverlap(initialOverlap)) else None + } + + private[this] def checkContradictions(pos: Set[Atom], neg: Set[Atom]): Option[InitialContradictions] = { + val contradictions = pos intersect neg + if(contradictions.nonEmpty) Some(new InitialContradictions(contradictions)) else None + } + + private[this] def checkAcyclic(clauses: Clauses): Option[CyclicNegation] = { + val deps = dependencyMap(clauses) + val cycle = Dag.findNegativeCycle(graph(deps)) + if(cycle.nonEmpty) Some(new CyclicNegation(cycle)) else None + } + private[this] def graph(deps: Map[Atom, Set[Literal]]) = new Dag.DirectedSignedGraph[Atom] { + type Arrow = Literal + def nodes = deps.keys.toList + def dependencies(a: Atom) = deps.getOrElse(a, Set.empty).toList + def isNegative(b: Literal) = b match { + case Negated(_) => true + case Atom(_) => false + } + def head(b: Literal) = b.atom + } + + private[this] def dependencyMap(clauses: Clauses): Map[Atom, Set[Literal]] = + (Map.empty[Atom, Set[Literal]] /: clauses.clauses) { + case (m, Clause(formula, heads)) => + val deps = literals(formula) + (m /: heads) { (n, head) => n.updated(head, n.getOrElse(head, Set.empty) ++ deps) } + } + + 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]) { + def add(atoms: Set[Atom]): Matched = add(atoms.toList) + def add(atoms: List[Atom]): Matched = { + val newOnly = atoms.filterNot(provenSet) + new Matched(provenSet ++ newOnly, newOnly ::: reverseOrdered) + } + def ordered: List[Atom] = reverseOrdered.reverse + override def toString = ordered.map(_.label).mkString("Matched(", ",", ")") + } + object Matched { + val empty = new Matched(Set.empty, Nil) + } + + /** Separates a sequence of literals into `(pos, neg)` atom sequences. */ + private[this] def separate(lits: Seq[Literal]): (Seq[Atom], Seq[Atom]) = Util.separate(lits) { + case a: Atom => Left(a) + case Negated(n) => Right(n) + } + + /** Finds clauses that have no body and thus prove their head. + * Returns `(, )`. */ + private[this] def findProven(c: Clauses): (Set[Atom], List[Clause]) = + { + val (proven, unproven) = c.clauses.partition(_.body == True) + (proven.flatMap(_.head).toSet, unproven) + } + private[this] def keepPositive(lits: Set[Literal]): Set[Atom] = + lits.collect{ case a: Atom => a}.toSet + + // precondition: factsToProcess contains no contradictions + @tailrec + private[this] def reduce0(clauses: Clauses, factsToProcess: Set[Literal], state: Matched): Matched = + applyAll(clauses, factsToProcess) match { + case None => // all of the remaining clauses failed on the new facts + state + case Some(applied) => + val (proven, unprovenClauses) = findProven(applied) + val processedFacts = state add keepPositive(factsToProcess) + val newlyProven = proven -- processedFacts.provenSet + val newState = processedFacts add newlyProven + if(unprovenClauses.isEmpty) + newState // no remaining clauses, done. + else { + val unproven = Clauses(unprovenClauses) + val nextFacts: Set[Literal] = if(newlyProven.nonEmpty) newlyProven.toSet else inferFailure(unproven) + reduce0(unproven, nextFacts, newState) + } + } + + /** Finds negated atoms under the negation as failure rule and returns them. + * This should be called only after there are no more known atoms to be substituted. */ + private[this] def inferFailure(clauses: Clauses): Set[Literal] = + { + /* At this point, there is at least one clause and one of the following is the case as the result of the acyclic negation rule: + i. there is at least one variable that occurs in a clause body but not in the head of a clause + ii. there is at least one variable that occurs in the head of a clause and does not transitively depend on a negated variable + In either case, each such variable x cannot be proven true and therefore proves 'not x' (negation as failure, !x in the code). + */ + val allAtoms = atoms(clauses) + val newFacts: Set[Literal] = negated(allAtoms.triviallyFalse) + if(newFacts.nonEmpty) + newFacts + else { + val possiblyTrue = hasNegatedDependency(clauses.clauses, Relation.empty, Relation.empty) + val newlyFalse: Set[Literal] = negated(allAtoms.inHead -- possiblyTrue) + if(newlyFalse.nonEmpty) + newlyFalse + else // should never happen due to the acyclic negation rule + error(s"No progress:\n\tclauses: $clauses\n\tpossibly true: $possiblyTrue") + } + } + + private[this] def negated(atoms: Set[Atom]): Set[Literal] = atoms.map(a => Negated(a)) + + /** Computes the set of atoms in `clauses` that directly or transitively take a negated atom as input. + * For example, for the following clauses, this method would return `List(a, d)` : + * a :- b, not c + * d :- a + */ + @tailrec + def hasNegatedDependency(clauses: Seq[Clause], posDeps: Relation[Atom, Atom], negDeps: Relation[Atom, Atom]): List[Atom] = + clauses match { + case Seq() => + // because cycles between positive literals are allowed, this isn't strictly a topological sort + Dag.topologicalSortUnchecked(negDeps._1s)(posDeps.reverse) + case Clause(formula, head) +: tail => + // collect direct positive and negative literals and track them in separate graphs + val (pos, neg) = directDeps(formula) + val (newPos, newNeg) = ( (posDeps, negDeps) /: head) { case ( (pdeps, ndeps), d) => + (pdeps + (d, pos), ndeps + (d, neg) ) + } + hasNegatedDependency(tail, newPos, newNeg) + } + + /** Computes the `(positive, negative)` literals in `formula`. */ + private[this] def directDeps(formula: Formula): (Seq[Atom], Seq[Atom]) = + Util.separate(literals(formula).toSeq) { + case Negated(a) => Right(a) + case a: Atom => Left(a) + } + private[this] def literals(formula: Formula): Set[Literal] = formula match { + case And(lits) => lits + case l: Literal => Set(l) + case True => Set.empty + } + + /** Computes the atoms in the heads and bodies of the clauses in `clause`. */ + def atoms(cs: Clauses): Atoms = cs.clauses.map(c => Atoms(c.head, atoms(c.body))).reduce(_ ++ _) + + /** Computes the set of all atoms in `formula`. */ + def atoms(formula: Formula): Set[Atom] = formula match { + case And(lits) => lits.map(_.atom) + case Negated(lit) => Set(lit) + case a: Atom => Set(a) + case True => Set() + } + + /** Represents the set of atoms in the heads of clauses and in the bodies (formulas) of clauses. */ + final case class Atoms(val inHead: Set[Atom], val inFormula: Set[Atom]) { + /** Concatenates this with `as`. */ + def ++ (as: Atoms): Atoms = Atoms(inHead ++ as.inHead, inFormula ++ as.inFormula) + /** Atoms that cannot be true because they do not occur in a head. */ + def triviallyFalse: Set[Atom] = inFormula -- inHead + } + + /** Applies known facts to `clause`s, deriving a new, possibly empty list of clauses. + * 1. If a fact is in the body of a clause, the derived clause has that fact removed from the body. + * 2. If the negation of a fact is in a body of a clause, that clause fails and is removed. + * 3. If a fact or its negation is in the head of a clause, the derived clause has that fact (or its negation) removed from the head. + * 4. If a head is empty, the clause proves nothing and is removed. + * + * NOTE: empty bodies do not cause a clause to succeed yet. + * All known facts must be applied before this can be done in order to avoid inconsistencies. + * Precondition: no contradictions in `facts` + * Postcondition: no atom in `facts` is present in the result + * Postcondition: No clauses have an empty head + * */ + def applyAll(cs: Clauses, facts: Set[Literal]): Option[Clauses] = + { + val newClauses = + if(facts.isEmpty) + cs.clauses.filter(_.head.nonEmpty) // still need to drop clauses with an empty head + else + cs.clauses.map(c => applyAll(c, facts)).flatMap(_.toList) + if(newClauses.isEmpty) None else Some(Clauses(newClauses)) + } + + def applyAll(c: Clause, facts: Set[Literal]): Option[Clause] = + { + val atoms = facts.map(_.atom) + val newHead = c.head -- atoms // 3. + if(newHead.isEmpty) // 4. empty head + None + else + substitute(c.body, facts).map( f => Clause(f, newHead) ) // 1, 2 + } + + /** Derives the formula that results from substituting `facts` into `formula`. */ + @tailrec + def substitute(formula: Formula, facts: Set[Literal]): Option[Formula] = formula match { + case And(lits) => + def negated(lits: Set[Literal]): Set[Literal] = lits.map(a => !a) + if( lits.exists( negated(facts) ) ) // 2. + None + else { + val newLits = lits -- facts + val newF = if(newLits.isEmpty) True else And(newLits) + Some(newF) // 1. + } + case True => Some(True) + case lit: Literal => // define in terms of And + substitute(And(Set(lit)), facts) + } +} diff --git a/util/logic/src/test/scala/sbt/logic/Test.scala b/util/logic/src/test/scala/sbt/logic/Test.scala new file mode 100644 index 000000000..cf50ef9fd --- /dev/null +++ b/util/logic/src/test/scala/sbt/logic/Test.scala @@ -0,0 +1,117 @@ +package sbt +package logic + + import org.scalacheck._ + import Prop.secure + import Logic.{LogicException, Matched} + +object LogicTest extends Properties("Logic") +{ + import TestClauses._ + + property("Handles trivial resolution.") = secure( expect(trivial, Set(A) ) ) + property("Handles less trivial resolution.") = secure( expect(lessTrivial, Set(B,A,D)) ) + property("Handles cycles without negation") = secure( expect(cycles, Set(F,A,B)) ) + property("Handles basic exclusion.") = secure( expect(excludedPos, Set()) ) + property("Handles exclusion of head proved by negation.") = secure( expect(excludedNeg, Set()) ) + // TODO: actually check ordering, probably as part of a check that dependencies are satisifed + property("Properly orders results.") = secure( expect(ordering, Set(B,A,C,E,F))) + property("Detects cyclic negation") = secure( + Logic.reduceAll(badClauses, Set()) match { + case Right(res) => false + case Left(err: Logic.CyclicNegation) => true + case Left(err) => error(s"Expected cyclic error, got: $err") + } + ) + + def expect(result: Either[LogicException, Matched], expected: Set[Atom]) = result match { + case Left(err) => false + case Right(res) => + val actual = res.provenSet + (actual == expected) || error(s"Expected to prove $expected, but actually proved $actual") + } +} + +object TestClauses +{ + + val A = Atom("A") + val B = Atom("B") + val C = Atom("C") + val D = Atom("D") + val E = Atom("E") + val F = Atom("F") + val G = Atom("G") + + val clauses = + A.proves(B) :: + A.proves(F) :: + B.proves(F) :: + F.proves(A) :: + (!C).proves(F) :: + D.proves(C) :: + C.proves(D) :: + Nil + + val cycles = Logic.reduceAll(clauses, Set()) + + val badClauses = + A.proves(D) :: + clauses + + val excludedNeg = { + val cs = + (!A).proves(B) :: + Nil + val init = + (!A) :: + (!B) :: + Nil + Logic.reduceAll(cs, init.toSet) + } + + val excludedPos = { + val cs = + A.proves(B) :: + Nil + val init = + A :: + (!B) :: + Nil + Logic.reduceAll(cs, init.toSet) + } + + val trivial = { + val cs = + Formula.True.proves(A) :: + Nil + Logic.reduceAll(cs, Set.empty) + } + + val lessTrivial = { + val cs = + Formula.True.proves(A) :: + Formula.True.proves(B) :: + (A && B && (!C)).proves(D) :: + Nil + Logic.reduceAll(cs, Set()) + } + + val ordering = { + val cs = + E.proves(F) :: + (C && !D).proves(E) :: + (A && B).proves(C) :: + Nil + Logic.reduceAll(cs, Set(A,B)) + } + + def all { + println(s"Cycles: $cycles") + println(s"xNeg: $excludedNeg") + println(s"xPos: $excludedPos") + println(s"trivial: $trivial") + println(s"lessTrivial: $lessTrivial") + println(s"ordering: $ordering") + } +} diff --git a/util/relation/src/main/scala/sbt/Relation.scala b/util/relation/src/main/scala/sbt/Relation.scala index 725512d0b..77c0b70c2 100644 --- a/util/relation/src/main/scala/sbt/Relation.scala +++ b/util/relation/src/main/scala/sbt/Relation.scala @@ -40,7 +40,7 @@ object Relation private[sbt] def get[X,Y](map: M[X,Y], t: X): Set[Y] = map.getOrElse(t, Set.empty[Y]) - private[sbt] type M[X,Y] = Map[X, Set[Y]] + private[sbt] type M[X,Y] = Map[X, Set[Y]] } /** Binary relation between A and B. It is a set of pairs (_1, _2) for _1 in A, _2 in B. */ @@ -111,7 +111,7 @@ private final class MRelation[A,B](fwd: Map[A, Set[B]], rev: Map[B, Set[A]]) ext { def forwardMap = fwd def reverseMap = rev - + def forward(t: A) = get(fwd, t) def reverse(t: B) = get(rev, t) @@ -119,12 +119,12 @@ private final class MRelation[A,B](fwd: Map[A, Set[B]], rev: Map[B, Set[A]]) ext def _2s = rev.keySet def size = (fwd.valuesIterator map { _.size }).foldLeft(0)(_ + _) - + def all: Traversable[(A,B)] = fwd.iterator.flatMap { case (a, bs) => bs.iterator.map( b => (a,b) ) }.toTraversable def +(pair: (A,B)) = this + (pair._1, Set(pair._2)) def +(from: A, to: B) = this + (from, to :: Nil) - def +(from: A, to: Traversable[B]) = + def +(from: A, to: Traversable[B]) = if(to.isEmpty) this else new MRelation( add(fwd, from, to), (rev /: to) { (map, t) => add(map, t, from :: Nil) }) def ++(rs: Traversable[(A,B)]) = ((this: Relation[A,B]) /: rs) { _ + _ }