ForAll

src/interpreter/Preprocessor.kt

@@ -123,6 +123,7 @@ open class Preprocessor {
                     term.functor == "write/1" -> Write(args[0])
                     term.functor == "read/1" -> Read(args[0])
                     term.functor == "initialization/1" -> Initialization(args[0] as Goal)
+                    term.functor == "forall/2" -> ForAll(args[0] as LogicOperand, args[1] as Goal)
 
                     else -> {
                         term.arguments = args

src/prolog/builtins/other.kt

@@ -5,6 +5,9 @@ import prolog.Substitutions
 import prolog.ast.logic.LogicOperand
 import prolog.ast.terms.Atom
 import prolog.ast.logic.LogicOperator
+import prolog.ast.terms.Goal
+import prolog.ast.terms.Operand
+import prolog.ast.terms.Operator
 
 class Initialization(val goal: LogicOperand) : LogicOperator(Atom(":-"), null, goal) {
     override fun satisfy(subs: Substitutions): Answers = goal.satisfy(subs).take(1)
@@ -14,3 +17,14 @@ class Initialization(val goal: LogicOperand) : LogicOperator(Atom(":-"), null, g
 class Query(val query: LogicOperand) : LogicOperator(Atom("?-"), null, query) {
     override fun satisfy(subs: Substitutions): Answers = query.satisfy(subs)
 }
+
+/**
+ * For all alternative bindings of Cond, Action can be proven.
+ * It does not say which is wrong if one proves wrong.
+ *
+ * @see [SWI-Prolog Predicate forall/2](https://www.swi-prolog.org/pldoc/doc_for?object=forall/2)
+ */
+class ForAll(condition: LogicOperand, action: Goal) : Operator(Atom("forall"), condition, action) {
+    private val not = Not(Conjunction(condition, Not(action)))
+    override fun satisfy(subs: Substitutions): Answers = not.satisfy(subs)
+}

tests/prolog/builtins/OtherOperatorsTests.kt

@@ -0,0 +1,54 @@
+package prolog.builtins
+
+import org.junit.jupiter.api.Assertions.assertEquals
+import org.junit.jupiter.api.Assertions.assertTrue
+import org.junit.jupiter.api.Test
+import prolog.ast.Database.Program
+import prolog.ast.arithmetic.Integer
+import prolog.ast.logic.Rule
+import prolog.ast.terms.Atom
+import prolog.ast.terms.CompoundTerm
+import prolog.ast.terms.Variable
+import java.io.ByteArrayOutputStream
+import java.io.PrintStream
+
+class OtherOperatorsTests {
+    @Test
+    fun `forall(X is 1, X == 1)`() {
+        val forall = ForAll(Is(Variable("X"), Integer(1)), EvaluatesTo(Variable("X"), Integer(1)))
+
+        val result = forall.satisfy(emptyMap()).toList()
+
+        assertEquals(1, result.size)
+    }
+
+    /**
+     * @see [Forall instead of failure-driven loops](https://riptutorial.com/prolog/example/19554/forall-instead-of-failure-driven-loops#example)
+     */
+    @Test
+    fun `forall printer`() {
+        val printer = Rule(
+            CompoundTerm(Atom("print"), listOf(Variable("X"))),
+            ForAll(
+                Between(Integer(1), Variable("X"), Variable("Y")),
+                Write(Variable("Y"))
+            )
+        )
+        Program.load(listOf(printer))
+
+        // Set output
+        val outStream = ByteArrayOutputStream()
+        System.setOut(PrintStream(outStream))
+
+        var expected = ""
+        for (i in 1..5) {
+            val result = CompoundTerm(Atom("print"), listOf(Integer(i))).satisfy(emptyMap()).toList()
+            assertEquals(1, result.size)
+            assertTrue(result[0].isSuccess)
+
+            expected += "$i"
+            assertEquals(expected, outStream.toString())
+            outStream.reset()
+        }
+    }
+}

tests/prolog/logic/TermAnalysisConstructionTest.kt

@@ -1,13 +1,10 @@
-package prolog.builtins
+package prolog.logic
 
 import org.junit.jupiter.api.Assertions.assertFalse
 import org.junit.jupiter.api.Assertions.assertTrue
 import org.junit.jupiter.api.Test
 import prolog.ast.terms.Atom
 import prolog.ast.terms.Structure
-import prolog.logic.atomic
-import prolog.logic.compound
-import prolog.logic.functor
 
 /**
  * Based on [Predicates for analyzing/constructing terms](https://github.com/dtonhofer/prolog_notes/blob/master/swipl_notes/about_term_analysis_and_construction/term_analysis_construction.png)