Checkpoint

pl/scratchpad.pl

@@ -1,4 +1,3 @@
-likes(mary, john).
-likes(john, mary).
-
-X :- likes(mary, X).
+a.
+f(a).
+f(X, _) :- X.

src/prolog/builtins/control.kt

@@ -1,11 +1,16 @@
 package prolog.builtins
 
+import prolog.components.expressions.Operand
+import prolog.components.expressions.Operator
 import prolog.components.terms.Atom
+import prolog.components.terms.Body
 
 /**
  * Always fail.
  */
-class Fail: Atom("fail")
+class Fail: Atom("fail"), Body {
+    override fun prove(): Boolean = false
+}
 
 /**
  * Same as fail, but the name has a more declarative connotation.
@@ -15,6 +20,32 @@ typealias False = Fail
 /**
  * Always succeed.
  */
-class True: Atom("true")
+class True: Atom("true"), Body {
+    override fun prove(): Boolean = true
+}
 
 // TODO Repeat/0
+
+// TODO !/0 (Cut)
+
+/**
+ * Conjunction (and). True if both Goal1 and Goal2 are true.
+ */
+class Conjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(","), leftOperand, rightOperand) {
+    override fun prove(): Boolean {
+        val left = leftOperand?.prove() ?: true
+        val right = rightOperand.prove()
+        return left && right
+    }
+}
+
+/**
+ * Disjunction (or). True if either Goal1 or Goal2 succeeds.
+ */
+class Disjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(";"), leftOperand, rightOperand) {
+    override fun prove(): Boolean {
+        val left = leftOperand?.prove() ?: false
+        val right = rightOperand.prove()
+        return left || right
+    }
+}

src/prolog/builtins/other.kt

@@ -0,0 +1,9 @@
+package prolog.builtins
+
+import prolog.components.expressions.Operand
+import prolog.components.expressions.Operator
+import prolog.components.terms.Atom
+
+class Query(rightOperand: Operand) : Operator(Atom("?-"), null, rightOperand) {
+    override fun prove(): Boolean = rightOperand.prove()
+}

src/prolog/builtins2/control/Conjunction.kt

@@ -1,10 +0,0 @@
-package prolog.builtins2.control
-
-import prolog.components.terms.Atom
-import prolog.components.Operand
-import prolog.components.Operator
-
-/**
- * Conjunction (and). True if both Goal1 and Goal2 are true.
- */
-class Conjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(","), leftOperand, rightOperand)

src/prolog/builtins2/control/Disjunction.kt

@@ -1,10 +0,0 @@
-package prolog.builtins2.control
-
-import prolog.components.terms.Atom
-import prolog.components.Operand
-import prolog.components.Operator
-
-/**
- * Disjunction (or). True if either Goal1 or Goal2 succeeds.
- */
-class Disjunction(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(";"), leftOperand, rightOperand)

src/prolog/components/Program.kt

@@ -10,16 +10,30 @@ import prolog.components.terms.Goal
 /**
  * Prolog Program or database.
  */
-object Program {
+object Program: Resolvent {
     private var predicates: Map<Functor, Predicate> = emptyMap()
 
     init {
+        setup()
+    }
+
+    private fun setup() {
         // Initialize the program with built-in predicates
         load(listOf(
             Fact(True())
         ))
     }
 
+    fun query(goal: Goal): Boolean {
+        val functor = goal.functor
+        // If the predicate does not exist, return false
+        val predicate = predicates[functor] ?: return false
+        // If the predicate exists, evaluate the goal against it
+        return predicate.solve(goal)
+    }
+
+    override fun solve(goal: Goal): Boolean = query(goal)
+
     /**
      * Loads a list of clauses into the program.
      */
@@ -51,13 +65,9 @@ object Program {
         }
     }
 
-    fun query(goal: Goal): Boolean {
-        val functor = goal.functor
-        val predicate = predicates[functor]
-            ?: // If the predicate does not exist, return false
-            return false
-        // If the predicate exists, evaluate the goal against it
-        return predicate.evaluate(goal)
+    fun clear() {
+        predicates = emptyMap()
+        setup()
     }
 }
 

src/prolog/components/Provable.kt

@@ -0,0 +1,5 @@
+package prolog.components
+
+interface Provable {
+    fun prove(): Boolean
+}

src/prolog/components/Resolvent.kt

@@ -0,0 +1,10 @@
+package prolog.components
+
+import prolog.components.terms.Goal
+
+/**
+ * Can be instructed to solve a goal.
+ */
+interface Resolvent {
+    fun solve(goal: Goal): Boolean
+}

src/prolog/components/expressions/Clause.kt

@@ -1,15 +1,9 @@
 package prolog.components.expressions
 
-import prolog.components.terms.Functor
-import prolog.components.terms.Goal
-import prolog.components.terms.Head
-import prolog.components.terms.Term
+import prolog.components.Resolvent
+import prolog.components.terms.*
 import prolog.unify
 
-// TODO Change this to the right type, supporting operators and normal Clauses
-//  Probably needs a new interface or abstract class (?)
-typealias Body = List<Term>
-
 /**
  * ‘Sentence’ of a Prolog program.
  *
@@ -18,18 +12,29 @@ typealias Body = List<Term>
  * @see [prolog.components.terms.Variable]
  * @see [Predicate]
  */
-abstract class Clause(val head: Head, val body: Body = emptyList()) : Expression {
+abstract class Clause(private val head: Head, private val body: Body? = null) : Resolvent {
     val functor: Functor = head.functor
-    override fun evaluate(goal: Goal): Boolean {
-        val result = unify(goal, head)
-        // TODO Evaluate the body
-        return result.isEmpty
+
+    override fun solve(goal: Goal): Boolean {
+        val unification = unify(goal, head)
+
+        if (unification.isEmpty) {
+            return false
+        }
+
+        val substitutions = unification.get()
+
+        val proven = body == null || body.prove()
+
+        substitutions.forEach { (variable, _) -> variable.unbind() }
+
+        return proven
     }
 
     override fun toString(): String {
         return when {
-            body.isEmpty() -> head.toString()
-            else -> "$head :- ${body.joinToString(", ")}"
+            body == null -> head.toString()
+            else -> "$head :- $body"
         }
     }
 }

src/prolog/components/expressions/Expression.kt

@@ -1,7 +0,0 @@
-package prolog.components.expressions
-
-import prolog.components.terms.Goal
-
-interface Expression {
-    fun evaluate(goal: Goal): Boolean
-}

src/prolog/components/expressions/Fact.kt

@@ -3,4 +3,4 @@ package prolog.components.expressions
 import prolog.builtins.True
 import prolog.components.terms.Head
 
-class Fact(head: Head) : Clause(head, listOf(True()))
+class Fact(head: Head) : Clause(head, True())

src/prolog/components/expressions/Operator.kt

@@ -1,13 +1,19 @@
-package prolog.components
+package prolog.components.expressions
 
-import prolog.components.terms.Argument
+import prolog.components.Provable
 import prolog.components.terms.Atom
+import prolog.components.terms.CompoundTerm
+import prolog.components.terms.Goal
 
-open class Operator(
+typealias Operand = Goal
+
+abstract class Operator(
     val symbol: Atom,
     val leftOperand: Operand? = null,
     val rightOperand: Operand
-) {
+) : CompoundTerm(symbol, listOfNotNull(leftOperand, rightOperand)), Provable {
+    abstract override fun prove(): Boolean
+
     override fun toString(): String {
         return when (leftOperand) {
             null -> "${symbol.name} $rightOperand"
@@ -15,5 +21,3 @@ open class Operator(
         }
     }
 }
-
-typealias Operand = Argument

src/prolog/components/expressions/Predicate.kt

@@ -1,5 +1,6 @@
 package prolog.components.expressions
 
+import prolog.components.Resolvent
 import prolog.components.terms.Functor
 import prolog.components.terms.Goal
 
@@ -9,7 +10,7 @@ import prolog.components.terms.Goal
  * If a goal is proved, the system looks for a predicate with the same functor, then uses indexing
  * to select candidate clauses and then tries these clauses one-by-one.
  */
-class Predicate : Expression {
+class Predicate : Resolvent {
     val functor: Functor
     val clauses: MutableList<Clause>
 
@@ -47,8 +48,8 @@ class Predicate : Expression {
         this.clauses.addAll(clauses)
     }
 
-    override fun evaluate(goal: Goal): Boolean {
+    override fun solve(goal: Goal): Boolean {
         require(goal.functor == functor) { "Goal functor does not match predicate functor" }
-        return clauses.any { it.evaluate(goal) }
+        return clauses.any { it.solve(goal) }
     }
 }

src/prolog/components/expressions/Rule.kt

@@ -1,5 +1,6 @@
 package prolog.components.expressions
 
+import prolog.components.terms.Body
 import prolog.components.terms.Head
 
 class Rule(head: Head, body: Body): Clause(head, body)

src/prolog/components/terms/Atom.kt

@@ -1,9 +1,27 @@
 package prolog.components.terms
 
-open class Atom(val name: String): Goal() {
+import prolog.components.Resolvent
+import prolog.unify
+
+open class Atom(val name: String) : Goal(), Head, Body, Resolvent {
     override val functor: Functor = "$name/_"
 
+    override fun solve(goal: Goal): Boolean = unify(goal, this).isEmpty
+
     override fun toString(): String {
         return name
     }
+
+    override fun equals(other: Any?): Boolean {
+        if (this === other) return true
+        if (other !is Atom) return false
+
+        if (name != other.name) return false
+
+        return true
+    }
+
+    override fun hashCode(): Int {
+        return javaClass.hashCode()
+    }
 }

src/prolog/components/terms/Body.kt

@@ -0,0 +1,5 @@
+package prolog.components.terms
+
+import prolog.components.Provable
+
+interface Body : Provable

src/prolog/components/terms/Goal.kt

@@ -1,16 +1,17 @@
 package prolog.components.terms
 
 import prolog.components.Program
+import prolog.components.Provable
 
 /**
- * Question stated to the Prolog engine.
+ * Ask the Prolog engine.
  *
- * A goal is either an [atom][prolog.components.terms.Atom] or a [compound term][prolog.components.terms.CompoundTerm].
+ * A goal is either an [Atom] or a [CompoundTerm].
  * A goal either [succeeds][prolog.builtins.True], in which case the variables in the compound terms have a binding,
  * or it fails if Prolog fails to prove it.
  */
-abstract class Goal : Head() {
-    fun prove(): Boolean {
-        return Program.query(this)
-    }
+abstract class Goal : Term, Provable {
+    abstract val functor: Functor
+
+    override fun prove(): Boolean = Program.query(this)
 }

src/prolog/components/terms/Head.kt

@@ -2,12 +2,9 @@ package prolog.components.terms
 
 /**
  * Part of a [Clause][prolog.components.expressions.Clause] before the [neck][prolog.terms.Neck] operator.
- *
- * @see [Atom]
- * @see [CompoundTerm]
  */
-abstract class Head: Term {
-    abstract val functor: Functor
+interface Head : Term {
+    val functor: Functor
 }
 
 typealias Functor = String

src/prolog/components/terms/Structure.kt

@@ -1,8 +1,17 @@
 package prolog.components.terms
 
-open class Structure(val name: Atom, val arguments: List<Argument>): Goal() {
+import prolog.components.Resolvent
+import prolog.unify
+
+typealias Argument = Term
+
+open class Structure(val name: Atom, val arguments: List<Argument>): Goal(), Head, Body, Resolvent {
     override val functor: Functor = "${name.name}/${arguments.size}"
 
+    override fun solve(goal: Goal): Boolean {
+        return unify(goal, this).isEmpty
+    }
+
     override fun toString(): String {
         return when {
             arguments.isEmpty() -> name.name

src/prolog/components/terms/Term.kt

@@ -8,8 +8,6 @@ package prolog.components.terms
  */
 interface Term
 
-typealias Argument = Term
-
 /*
 <program> ::= <clause list> <query> | <query>
 <clause list> ::= <clause> | <clause list> <clause>
@@ -22,11 +20,4 @@ typealias Argument = Term
 <query> ::= ?- <predicate list>.
 <small atom> ::= <lowercase letter> | <small atom> <character>
 <variable> ::= <uppercase letter> | <variable> <character>
-<lowercase letter> ::= a | b | c | ... | x | y | z
-<uppercase letter> ::= A | B | C | ... | X | Y | Z | _
-<numeral> ::= <digit> | <numeral> <digit>
-<digit> ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
-<character> ::= <lowercase letter> | <uppercase letter> | <digit> | <special>
-<special> ::= + | - | * | / | \ | ^ | ~ | : | . | ? |  | # | $ | &
-<string> ::= <character> | <string> <character>
 */

src/prolog/components/terms/Variable.kt

@@ -2,7 +2,7 @@ package prolog.components.terms
 
 import java.util.Optional
 
-data class Variable(val name: String): Term {
+data class Variable(val name: String) : Term {
     private var alias: Optional<Term> = Optional.empty()
 
     fun alias(): Optional<Term> {
@@ -27,4 +27,12 @@ data class Variable(val name: String): Term {
             else -> name
         }
     }
+
+    override fun equals(other: Any?): Boolean {
+        return if (alias.isPresent) {
+            alias.get() == other
+        } else {
+            name == other.toString()
+        }
+    }
 }

src/prolog/terms/operators.kt

@@ -1,9 +0,0 @@
-package prolog.terms
-
-import prolog.components.Operand
-import prolog.components.Operator
-import prolog.components.terms.Atom
-
-class Neck(leftOperand: Operand, rightOperand: Operand) : Operator(Atom(":-"), leftOperand, rightOperand)
-
-class Query(rightOperand: Operand): Operator(Atom("?-"), null, rightOperand)

src/prolog/unify.kt

@@ -74,9 +74,9 @@ fun unifyLazy(term1: Term, term2: Term, substitution: Substitution = emptyMap())
 
 fun unify(term1: Term, term2: Term): Optional<Substitution> {
     val substitutions = unifyLazy(term1, term2).toList()
-    return if (substitutions.isEmpty()) {
-        Optional.empty()
-    } else {
+    return if (substitutions.isNotEmpty()) {
         Optional.of(substitutions.first())
+    } else {
+        Optional.empty()
     }
 }

tests/prolog/EvaluationTest.kt

@@ -2,14 +2,24 @@ package prolog
 
 import org.junit.jupiter.api.Assertions.assertFalse
 import org.junit.jupiter.api.Assertions.assertTrue
+import org.junit.jupiter.api.BeforeEach
 import org.junit.jupiter.api.Test
+import prolog.builtins.Conjunction
+import prolog.builtins.Disjunction
 import prolog.components.Program
 import prolog.components.expressions.Fact
+import prolog.components.expressions.Rule
 import prolog.components.terms.Atom
+import prolog.components.terms.Structure
 
 class EvaluationTest {
+    @BeforeEach
+    fun setUp() {
+        Program.clear()
+    }
+
     @Test
-    fun successful_single_clause_program_query() {
+    fun successful_single_fact_query() {
         val fact = Fact(Atom("a"))
         Program.load(listOf(fact))
 
@@ -17,10 +27,137 @@ class EvaluationTest {
     }
 
     @Test
-    fun failing_single_clause_program_query() {
+    fun failing_single_fact_query() {
         val fact = Fact(Atom("a"))
         Program.load(listOf(fact))
 
-        assertFalse(Program.query(Atom("b")))
+        val result = Program.query(Atom("b"))
+
+        assertFalse(result)
+    }
+
+    @Test
+    fun multiple_fact_query() {
+        val fact1 = Fact(Atom("a"))
+        val fact2 = Fact(Atom("b"))
+        Program.load(listOf(fact1, fact2))
+
+        assertTrue(Program.query(Atom("a")))
+        assertTrue(Program.query(Atom("b")))
+        assertFalse(Program.query(Atom("c")))
+    }
+
+    @Test
+    fun single_compound_query() {
+        val structure = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))
+        Program.load(listOf(Fact(structure)))
+
+        assertTrue(Program.query(Structure(Atom("f"), listOf(Atom("a"), Atom("b")))))
+    }
+
+    @Test
+    fun multiple_compound_query() {
+        val structure1 = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))
+        val structure2 = Structure(Atom("g"), listOf(Atom("c"), Atom("d")))
+        Program.load(listOf(Fact(structure1), Fact(structure2)))
+
+        assertTrue(Program.query(Structure(Atom("f"), listOf(Atom("a"), Atom("b")))))
+        assertTrue(Program.query(Structure(Atom("g"), listOf(Atom("c"), Atom("d")))))
+        assertFalse(Program.query(Structure(Atom("h"), listOf(Atom("e")))))
+    }
+
+    /**
+     * John and Jane are Jimmy's parents.
+     */
+    @Test
+    fun parents_prolog_way() {
+        val father = Fact(Structure(Atom("father"), listOf(Atom("john"), Atom("jimmy"))))
+        val mother = Fact(Structure(Atom("mother"), listOf(Atom("jane"), Atom("jimmy"))))
+
+        val parent1 = Rule(
+            Structure(Atom("parent"), listOf(Atom("X"), Atom("Y"))),
+            /* :- */
+            Structure(Atom("father"), listOf(Atom("X"), Atom("Y")))
+        )
+        val parent2 = Rule(
+            Structure(Atom("parent"), listOf(Atom("X"), Atom("Y"))),
+            /* :- */
+            Structure(Atom("mother"), listOf(Atom("X"), Atom("Y")))
+        )
+
+        Program.load(listOf(father, mother, parent1, parent2))
+
+        assertTrue(Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jimmy")))))
+        assertTrue(Program.query(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy")))))
+    }
+
+    /**
+     * John and Jane are Jimmy's parents.
+     */
+    @Test
+    fun parents_disjunction_way() {
+        val father = Fact(Structure(Atom("father"), listOf(Atom("john"), Atom("jimmy"))))
+        val mother = Fact(Structure(Atom("mother"), listOf(Atom("jane"), Atom("jimmy"))))
+
+        val parent = Rule(
+            Structure(Atom("parent"), listOf(Atom("X"), Atom("Y"))),
+            /* :- */ Disjunction(
+            Structure(Atom("father"), listOf(Atom("X"), Atom("Y"))),
+            /* ; */
+            Structure(Atom("mother"), listOf(Atom("X"), Atom("Y")))
+            ))
+
+        Program.load(listOf(father, mother, parent))
+
+        assertTrue(Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jimmy")))))
+        assertTrue(Program.query(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy")))))
+
+        assertFalse(Program.query(Structure(Atom("parent"), listOf(Atom("john"), Atom("jane")))))
+        assertFalse(Program.query(Structure(Atom("father"), listOf(Atom("john"), Atom("jane")))))
+    }
+
+    /**
+     * John is Jimmy's father.
+     * Jane is Jimmy's mother.
+     */
+    @Test
+    fun father_or_mother() {
+        val male = Fact(Structure(Atom("male"), listOf(Atom("john"))))
+        val female = Fact(Structure(Atom("female"), listOf(Atom("jane"))))
+
+        val parent1 = Fact(Structure(Atom("parent"), listOf(Atom("john"), Atom("jimmy"))))
+        val parent2 = Fact(Structure(Atom("parent"), listOf(Atom("jane"), Atom("jimmy"))))
+
+        val isFather = Rule(
+            Structure(Atom("isFather"), listOf(Atom("X"), Atom("Y"))),
+            Conjunction(
+                Structure(Atom("parent"), listOf(Atom("X"), Atom("Y"))),
+                Structure(Atom("male"), listOf(Atom("X")))
+            )
+        )
+        val isMother = Rule(
+            Structure(Atom("isMother"), listOf(Atom("X"), Atom("Y"))),
+            Conjunction(
+                Structure(Atom("parent"), listOf(Atom("X"), Atom("Y"))),
+                Structure(Atom("female"), listOf(Atom("X")))
+            )
+        )
+
+        Program.load(listOf(male, female, parent1, parent2, isFather, isMother))
+
+        val result1 = Program.query(Structure(Atom("isFather"), listOf(Atom("john"), Atom("jimmy"))))
+        assertTrue(result1)
+
+        val result2 = Program.query(Structure(Atom("isMother"), listOf(Atom("jane"), Atom("jimmy"))))
+        assertTrue(result2)
+
+        val result3 = Program.query(Structure(Atom("isFather"), listOf(Atom("jane"), Atom("jimmy"))))
+        assertFalse(result3)
+
+        val result4 = Program.query(Structure(Atom("isMother"), listOf(Atom("john"), Atom("jimmy"))))
+        assertFalse(result4)
+
+        val result5 = Program.query(Structure(Atom("parent"), listOf(Atom("trudy"), Atom("jimmy"))))
+        assertFalse(result5)
     }
 }

tests/prolog/UnifyTest.kt

@@ -234,13 +234,4 @@ class UnifyTest {
 
         assertFalse(result.isPresent, "Atom with different arity should not unify")
     }
-
-    @Test
-    fun temp() {
-        val atom1 = Atom("a")
-        val atom2 = Atom("a")
-
-        val result = unify(atom1, atom2)
-        assertTrue(result.isPresent, "Identical atoms should unify")
-    }
 }