diff --git a/src/interpreter/Preprocessor.kt b/src/interpreter/Preprocessor.kt index 3bd5fa9..4b36614 100644 --- a/src/interpreter/Preprocessor.kt +++ b/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 diff --git a/src/prolog/builtins/other.kt b/src/prolog/builtins/other.kt index 4cc582f..56c99d1 100644 --- a/src/prolog/builtins/other.kt +++ b/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) +} diff --git a/tests/prolog/builtins/OtherOperatorsTests.kt b/tests/prolog/builtins/OtherOperatorsTests.kt new file mode 100644 index 0000000..e9341d6 --- /dev/null +++ b/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() + } + } +} diff --git a/tests/prolog/builtins/TermAnalysisConstructionTest.kt b/tests/prolog/logic/TermAnalysisConstructionTest.kt similarity index 91% rename from tests/prolog/builtins/TermAnalysisConstructionTest.kt rename to tests/prolog/logic/TermAnalysisConstructionTest.kt index a137fca..c1033a9 100644 --- a/tests/prolog/builtins/TermAnalysisConstructionTest.kt +++ b/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)