diff --git a/util/collection/src/main/scala/sbt/Dag.scala b/util/collection/src/main/scala/sbt/Dag.scala index 4250b0f10..ef8f9cec1 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) @@ -70,4 +72,3 @@ object Dag new Cyclic(value, a :: all, false) } } - 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..8d02b2ab9 --- /dev/null +++ b/util/logic/src/main/scala/sbt/logic/Logic.scala @@ -0,0 +1,297 @@ +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]): 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 = + { + val (posSeq, negSeq) = separate(initialFacts.toSeq) + val (pos, neg) = (posSeq.toSet, negSeq.toSet) + + checkContradictions(pos, neg) + checkOverlap(clauses, pos) + checkAcyclic(clauses) + + 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. */ + def checkOverlap(clauses: Clauses, initialFacts: Set[Atom]) { + val as = atoms(clauses) + val initialOverlap = initialFacts.filter(as.inHead) + if(initialOverlap.nonEmpty) throw new InitialOverlap(initialOverlap) + } + + private[this] def checkContradictions(pos: Set[Atom], neg: Set[Atom]) { + val contradictions = pos intersect neg + if(contradictions.nonEmpty) throw new InitialContradictions(contradictions) + } + + def checkAcyclic(clauses: Clauses) { + // TODO + } + + 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[Atom]) extends RuntimeException("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]) = formula match { + case And(lits) => separate(lits.toSeq) + case Negated(a) => (Nil, a :: Nil) + case a: Atom => (a :: Nil, Nil) + case True => (Nil, Nil) + } + + /** 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..49836998a --- /dev/null +++ b/util/logic/src/test/scala/sbt/logic/Test.scala @@ -0,0 +1,84 @@ +package sbt +package logic + +object Test { + 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) { _ + _ }