mirror of https://github.com/sbt/sbt.git
Logic system supporting auto plugins and initial outline of AutoPlugin and Natures types.
* Not integrated into project loading * Doesn't yet check that negation is acyclic before execution
This commit is contained in:
Mark Harrah
parent
1d627797d7
commit
322f6de655
|
|
@ -0,0 +1,128 @@
|
|||
package sbt
|
||||
|
||||
import logic.{Atom, Clause, Clauses, Formula, Literal, Logic}
|
||||
import Def.Setting
|
||||
import Natures._
|
||||
|
||||
/**
|
||||
An AutoPlugin defines a group of settings and the conditions that the settings are automatically added to a build (called "activation").
|
||||
The `select` method defines the conditions,
|
||||
`provides` defines an identifier for the AutoPlugin,
|
||||
and the a method like `projectSettings` defines the settings to add.
|
||||
|
||||
Steps for plugin authors:
|
||||
1. Determine the natures that, when present (or absent), activate the AutoPlugin.
|
||||
2. Determine the settings/configurations to automatically inject when activated.
|
||||
3. Define a new, unique identifying [[Nature]] (which is a wrapper around a String ID).
|
||||
|
||||
For example, the following will automatically add the settings in `projectSettings`
|
||||
to a project that has both the `Web` and `Javascript` natures enabled. It will itself
|
||||
define the `MyStuff` nature. This nature can be explicitly disabled by the user to
|
||||
prevent the plugin from activating.
|
||||
|
||||
object MyPlugin extends AutoPlugin {
|
||||
def select = Web && Javascript
|
||||
def provides = MyStuff
|
||||
def projectSettings = Seq(...)
|
||||
}
|
||||
|
||||
Steps for users:
|
||||
1. add dependencies on plugins as usual with addSbtPlugin
|
||||
2. add Natures to Projects, which will automatically select the plugin settings to add for those Projects.
|
||||
|
||||
For example, given natures Web and Javascript (perhaps provided by plugins added with addSbtPlugin),
|
||||
|
||||
<Project>.natures( Web && Javascript )
|
||||
|
||||
will activate `MyPlugin` defined above and have its settings automatically added. If the user instead defines
|
||||
|
||||
<Project>.natures( Web && Javascript && !MyStuff)
|
||||
|
||||
then the `MyPlugin` settings (and anything that activates when `MyStuff` is activated) will not be added.
|
||||
*/
|
||||
abstract class AutoPlugin
|
||||
{
|
||||
/** This AutoPlugin will be activated for a project when the [[Natures]] matcher returned by this method matches that project's natures
|
||||
* AND the user does not explicitly exclude the Nature returned by `provides`.
|
||||
*
|
||||
* For example, if this method returns `Web && Javascript`, this plugin instance will only be added
|
||||
* if the `Web` and `Javascript` natures are enabled. */
|
||||
def select: Natures
|
||||
|
||||
/** The unique [[Nature]] for this AutoPlugin instance. This has two purposes:
|
||||
* 1. The user can explicitly disable this AutoPlugin.
|
||||
* 2. Other plugins can activate based on whether this AutoPlugin was activated.
|
||||
*/
|
||||
def provides: Nature
|
||||
|
||||
/** The [[Configuration]]s to add to each project that activates this AutoPlugin.*/
|
||||
def projectConfigurations: Seq[Configuration] = Nil
|
||||
|
||||
/** The [[Setting]]s to add in the scope of each project that activates this AutoPlugin. */
|
||||
def projectSettings: Seq[Setting[_]] = Nil
|
||||
|
||||
/** The [[Setting]]s to add to the build scope for each project that activates this AutoPlugin.
|
||||
* The settings returned here are guaranteed to be added to a given build scope only once
|
||||
* regardless of how many projects for that build activate this AutoPlugin. */
|
||||
def buildSettings: Seq[Setting[_]] = Nil
|
||||
|
||||
/** The [[Setting]]s to add to the global scope exactly once if any project activates this AutoPlugin. */
|
||||
def globalSettings: Seq[Setting[_]] = Nil
|
||||
|
||||
// TODO?: def commands: Seq[Command]
|
||||
}
|
||||
|
||||
/** An expression that matches `Nature`s. */
|
||||
sealed trait Natures {
|
||||
def && (o: Basic): Natures
|
||||
}
|
||||
|
||||
/** Represents a feature or conceptual group of settings.
|
||||
* `label` is the unique ID for this nature. */
|
||||
final case class Nature(label: String) extends Basic {
|
||||
/** Constructs a Natures matcher that excludes this Nature. */
|
||||
def unary_! : Basic = Exclude(this)
|
||||
}
|
||||
|
||||
object Natures
|
||||
{
|
||||
// TODO: allow multiple AutoPlugins to provide the same Nature?
|
||||
// TODO: translate error messages
|
||||
/** Select the AutoPlugins to include according to the user-specified natures in `requested` and all discovered AutoPlugins in `defined`.*/
|
||||
def evaluate(requested: Natures, defined: List[AutoPlugin]): Seq[AutoPlugin] =
|
||||
{
|
||||
val byAtom = defined.map(x => (Atom(x.provides.label), x)).toMap
|
||||
val clauses = Clauses( defined.map(d => asClause(d)) )
|
||||
val results = Logic.reduce(clauses, flatten(requested).toSet)
|
||||
results.ordered.map(byAtom)
|
||||
}
|
||||
|
||||
/** An included or excluded Nature. TODO: better name than Basic. */
|
||||
sealed abstract class Basic extends Natures {
|
||||
def &&(o: Basic): Natures = And(this :: o :: Nil)
|
||||
}
|
||||
private[sbt] final case class Exclude(n: Nature) extends Basic {
|
||||
def unary_! : Nature = n
|
||||
}
|
||||
private[sbt] final case class And(natures: List[Basic]) extends Natures {
|
||||
def &&(o: Basic): Natures = And(o :: natures)
|
||||
}
|
||||
|
||||
private[sbt] def asClause(ap: AutoPlugin): Clause =
|
||||
Clause( convert(ap.select), Set(Atom(ap.provides.label)) )
|
||||
|
||||
private[this] def flatten(n: Natures): Seq[Literal] = n match {
|
||||
case And(ns) => convertAll(ns)
|
||||
case b: Basic => convertBasic(b) :: Nil
|
||||
}
|
||||
|
||||
private[this] def convert(n: Natures): Formula = n match {
|
||||
case And(ns) => convertAll(ns).reduce[Formula](_ && _)
|
||||
case b: Basic => convertBasic(b)
|
||||
}
|
||||
private[this] def convertBasic(b: Basic): Literal = b match {
|
||||
case Exclude(n) => !convertBasic(n)
|
||||
case Nature(s) => Atom(s)
|
||||
}
|
||||
private[this] def convertAll(ns: Seq[Basic]): Seq[Literal] = ns map convertBasic
|
||||
}
|
||||
|
|
@ -73,6 +73,8 @@ object Sbt extends Build
|
|||
lazy val datatypeSub = baseProject(utilPath /"datatype", "Datatype Generator") dependsOn(ioSub)
|
||||
// cross versioning
|
||||
lazy val crossSub = baseProject(utilPath / "cross", "Cross") settings(inConfig(Compile)(Transform.crossGenSettings): _*)
|
||||
// A monotonic logic that includes restricted negation as failure
|
||||
lazy val logicSub = baseProject(utilPath / "logic", "Logic").dependsOn(collectionSub, relationSub)
|
||||
|
||||
/* **** Intermediate-level Modules **** */
|
||||
|
||||
|
|
@ -130,7 +132,7 @@ object Sbt extends Build
|
|||
completeSub, classpathSub, stdTaskSub, processSub) settings( sbinary )
|
||||
|
||||
// The main integration project for sbt. It brings all of the subsystems together, configures them, and provides for overriding conventions.
|
||||
lazy val mainSub = testedBaseProject(mainPath, "Main") dependsOn(actionsSub, mainSettingsSub, interfaceSub, ioSub, ivySub, launchInterfaceSub, logSub, processSub, runSub, commandSub) settings(scalaXml)
|
||||
lazy val mainSub = testedBaseProject(mainPath, "Main") dependsOn(actionsSub, mainSettingsSub, interfaceSub, ioSub, ivySub, launchInterfaceSub, logSub, logicSub, processSub, runSub, commandSub) settings(scalaXml)
|
||||
|
||||
// Strictly for bringing implicits and aliases from subsystems into the top-level sbt namespace through a single package object
|
||||
// technically, we need a dependency on all of mainSub's dependencies, but we don't do that since this is strictly an integration project
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -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 `(<proven atoms>, <remaining unproven clauses>)`. */
|
||||
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)
|
||||
}
|
||||
}
|
||||
|
|
@ -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")
|
||||
}
|
||||
}
|
||||
|
|
@ -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) { _ + _ }
|
||||
|
|
|
|||
Loading…
Reference in New Issue