diff --git a/src/interpreter/Preprocessor.kt b/src/interpreter/Preprocessor.kt index 19d8f2b..7076dc8 100644 --- a/src/interpreter/Preprocessor.kt +++ b/src/interpreter/Preprocessor.kt @@ -3,6 +3,7 @@ package interpreter import io.Logger import prolog.ast.arithmetic.Expression import prolog.ast.arithmetic.Integer +import prolog.ast.lists.List as PList import prolog.ast.logic.Clause import prolog.ast.logic.Fact import prolog.ast.logic.LogicOperand @@ -63,9 +64,9 @@ open class Preprocessor { Functor.of("functor/3") -> FunctorOp(args[0], args[1], args[2]) Functor.of("arg/3") -> Arg(args[0], args[1], args[2]) Functor.of("clause/2") -> ClauseOp(args[0] as Head, args[1] as Body) + Functor.of("atomic/1") -> AtomicOp(args[0]) + Functor.of("compound/1") -> CompoundOp(args[0]) Functor.of("=../2") -> Univ(args[0], args[1]) - Functor.of("numbervars/1") -> NumberVars(args[0]) - Functor.of("numbervars/3") -> NumberVars(args[0], args[1] as Integer, args[2]) // Arithmetic Functor.of("inf/0") -> Integer(Int.MAX_VALUE) @@ -155,8 +156,7 @@ open class Preprocessor { Functor.of("read/1") -> Read(args[0]) // Lists - Functor.of("member/2") -> Member(args[0], args[1]) - Functor.of("append/3") -> Append(args[0], args[1], args[2]) + Functor.of("member/2") -> Member(args[0], args[1] as PList) // Meta Functor.of("call/1") -> Call(args[0]) @@ -172,12 +172,6 @@ open class Preprocessor { Functor.of("==/2") -> Equivalent(args[0], args[1]) Functor.of("\\==/2") -> NotEquivalent(args[0], args[1]) - // Verification - Functor.of("atomic/1") -> Atomic(args[0]) - Functor.of("compound/1") -> Compound(args[0]) - Functor.of("nonvar/1") -> NonVar(args[0]) - Functor.of("var/1") -> Var(args[0]) - Functor.of(":-/2") -> Rule(args[0] as Head, args[1] as Body) else -> { diff --git a/src/prolog/ast/arithmetic/ArithmeticOperator.kt b/src/prolog/ast/arithmetic/ArithmeticOperator.kt index d87c6e8..61550a9 100644 --- a/src/prolog/ast/arithmetic/ArithmeticOperator.kt +++ b/src/prolog/ast/arithmetic/ArithmeticOperator.kt @@ -4,7 +4,4 @@ import prolog.ast.terms.Atom import prolog.ast.terms.Operator abstract class ArithmeticOperator(symbol: Atom, leftOperand: Expression, rightOperand: Expression) : - Operator(symbol, leftOperand, rightOperand), Expression { - constructor(symbol: String, leftOperand: Expression, rightOperand: Expression) : - this(Atom(symbol), leftOperand, rightOperand) -} + Operator(symbol, leftOperand, rightOperand), Expression diff --git a/src/prolog/ast/lists/List.kt b/src/prolog/ast/lists/List.kt index cd5ee80..494aa08 100644 --- a/src/prolog/ast/lists/List.kt +++ b/src/prolog/ast/lists/List.kt @@ -6,18 +6,11 @@ import prolog.ast.arithmetic.Integer sealed class List : Term { abstract val head: Term - open val tail: Term? = null - - operator fun component1(): Term = head - operator fun component2(): Term? = tail - + open val tail: List? = null val size: Integer get() = when (this) { is Empty -> Integer(0) - is Cons -> { - val tailSize = if (tail is List) { (tail as List).size.value } else 0 - Integer(1 + tailSize) - } + is Cons -> Integer(1 + tail.size.value) } fun isEmpty(): Boolean = this is Empty @@ -31,7 +24,7 @@ sealed class List : Term { override fun toString(): String = "[]" } - class Cons(override val head: Term, override var tail: Term) : List() { + class Cons(override val head: Term, override var tail: List) : List() { override fun applySubstitution(subs: Substitutions): List { val newHead = head.applySubstitution(subs) val newTail = tail.applySubstitution(subs) as List @@ -40,12 +33,11 @@ sealed class List : Term { override fun toString(): String { val values = mutableListOf() - var current: Term? = this - while (current != null && current is Cons) { + var current: List? = this + while (current != null && current !is Empty) { values.add(current.head) current = current.tail } - if (current != null && current !is Empty) values.add(current) return "[${values.joinToString(", ")}]" } } diff --git a/src/prolog/ast/logic/LogicOperator.kt b/src/prolog/ast/logic/LogicOperator.kt index 8fb488f..5353f0d 100644 --- a/src/prolog/ast/logic/LogicOperator.kt +++ b/src/prolog/ast/logic/LogicOperator.kt @@ -10,8 +10,5 @@ abstract class LogicOperator( leftOperand: LogicOperand? = null, rightOperand: LogicOperand ) : Operator(symbol, leftOperand, rightOperand), Satisfiable { - constructor(symbol: String, leftOperand: LogicOperand? = null, rightOperand: LogicOperand) : - this(Atom(symbol), leftOperand, rightOperand) - abstract override fun satisfy(subs: Substitutions): Answers } diff --git a/src/prolog/ast/terms/Functor.kt b/src/prolog/ast/terms/Functor.kt index b7a4cc3..98d764f 100644 --- a/src/prolog/ast/terms/Functor.kt +++ b/src/prolog/ast/terms/Functor.kt @@ -4,8 +4,6 @@ import prolog.Substitutions import prolog.ast.arithmetic.Integer data class Functor(val name: Atom, val arity: Integer) : Term { - constructor(name: String, arity: Int) : this(Atom(name), Integer(arity)) - companion object { fun of(functor: String): Functor { // Split the functor string into name and arity, by splitting the last "/" diff --git a/src/prolog/ast/terms/Operator.kt b/src/prolog/ast/terms/Operator.kt index 136c423..cf43b24 100644 --- a/src/prolog/ast/terms/Operator.kt +++ b/src/prolog/ast/terms/Operator.kt @@ -7,9 +7,6 @@ abstract class Operator( private val leftOperand: Operand? = null, private val rightOperand: Operand ) : CompoundTerm(symbol, listOfNotNull(leftOperand, rightOperand)), Term { - constructor(symbol: String, leftOperand: Operand? = null, rightOperand: Operand) : - this(Atom(symbol), leftOperand, rightOperand) - override fun toString(): String { return when (leftOperand) { null -> "${symbol.name} $rightOperand" diff --git a/src/prolog/ast/terms/Structure.kt b/src/prolog/ast/terms/Structure.kt index 162dc61..b6d41fe 100644 --- a/src/prolog/ast/terms/Structure.kt +++ b/src/prolog/ast/terms/Structure.kt @@ -12,8 +12,6 @@ typealias Argument = Term typealias CompoundTerm = Structure open class Structure(val name: Atom, var arguments: List) : Goal(), Head, Body, Resolvent { - constructor(name: String, vararg arguments: Argument) : this(Atom(name), arguments.asList()) - override val functor: Functor = Functor(name, Integer(arguments.size)) override fun solve(goal: Goal, subs: Substitutions): Answers { diff --git a/src/prolog/builtins/analysisOperators.kt b/src/prolog/builtins/analysisOperators.kt index 7f83ab0..f905696 100644 --- a/src/prolog/builtins/analysisOperators.kt +++ b/src/prolog/builtins/analysisOperators.kt @@ -1,6 +1,5 @@ package prolog.builtins -import com.sun.tools.javac.resources.CompilerProperties.Fragments.Anonymous import prolog.Answers import prolog.Substitutions import prolog.ast.Database.Program @@ -17,11 +16,9 @@ import prolog.ast.lists.List.Cons * * If Term is a [Variable] it is unified with a new term whose arguments are all different variables. * If Term is [atomic], Arity will be unified with the integer 0, and Name will be unified with Term. - * - * Source: [SWI-Prolog Predicate functor/3](https://www.swi-prolog.org/pldoc/doc_for?object=functor/3) */ class FunctorOp(private val term: Term, private val functorName: Term, private val functorArity: Term) : - Structure("functor", term, functorName, functorArity) { + Structure(Atom("functor"), listOf(term, functorName, functorArity)) { override fun satisfy(subs: Substitutions): Answers { return when { nonvariable(term, subs) -> { @@ -57,7 +54,7 @@ class FunctorOp(private val term: Term, private val functorName: Term, private v } class Arg(private val arg: Term, private val term: Term, private val value: Term) : - Structure("arg", arg, term, value) { + Structure(Atom("arg"), listOf(arg, term, value)) { override fun satisfy(subs: Substitutions): Answers = sequence { require(nonvariable(term, subs)) { "Arguments are not sufficiently instantiated" } require(compound(term, subs)) { @@ -118,7 +115,7 @@ class Arg(private val arg: Term, private val term: Term, private val value: Term * [SWI-Prolog Operator clause/2](https://www.swi-prolog.org/pldoc/doc_for?object=clause/2) */ class ClauseOp(private val head: Head, private val body: Body) : - Structure("clause", head, body) { + Structure(Atom("clause"), listOf(head, body)) { override fun satisfy(subs: Substitutions): Answers = sequence { require(nonvariable(head, subs)) { "Arguments are not sufficiently instantiated" } @@ -157,7 +154,31 @@ class ClauseOp(private val head: Head, private val body: Body) : ) } -open class Univ(private val term: Term, private val list: Term) : Operator("=..", term, list) { +class AtomicOp(private val term: Term) : Operator(Atom("atomic"), null, term) { + override fun satisfy(subs: Substitutions): Answers { + return if (atomic(term, subs)) { + sequenceOf(Result.success(emptyMap())) + } else { + emptySequence() + } + } + + override fun applySubstitution(subs: Substitutions): AtomicOp = AtomicOp(term.applySubstitution(subs)) +} + +class CompoundOp(private val term: Term) : Operator(Atom("compound"), null, term) { + override fun satisfy(subs: Substitutions): Answers { + return if (compound(term, subs)) { + sequenceOf(Result.success(emptyMap())) + } else { + emptySequence() + } + } + + override fun applySubstitution(subs: Substitutions): CompoundOp = CompoundOp(term.applySubstitution(subs)) +} + +open class Univ(private val term: Term, private val list: Term) : Operator(Atom("=.."), term, list) { override fun satisfy(subs: Substitutions): Answers { return when { nonvariable(term, subs) && nonvariable(list, subs) -> { @@ -189,14 +210,11 @@ open class Univ(private val term: Term, private val list: Term) : Operator("=.." list.size.value > 1 -> { val head = list.head val arguments = mutableListOf() - var tail: Term? = list.tail - while (tail != null && tail is Cons) { + var tail: List? = list.tail + while (tail != null && tail !is Empty) { arguments.add(tail.head) tail = tail.tail } - if (tail != null && tail !is Empty) { - arguments.add(tail) - } Structure(head as Atom, arguments) } @@ -228,23 +246,3 @@ open class Univ(private val term: Term, private val list: Term) : Operator("=.." list.applySubstitution(subs) ) } - -class NumberVars(private val term: Term, private val start: Integer, private val end: Term) : - Structure("numbervars", term, start, end) { - private var yieldEnd: Boolean = true - - constructor(term: Term) : this(term, Integer(0), AnonymousVariable.create()) { - yieldEnd = false - } - - override fun satisfy(subs: Substitutions): Answers = sequence { - val (newEnd, newSubs) = numbervars(term, start.value, subs) - unifyLazy(end, Integer(newEnd), subs).forEach { endResult -> - endResult.map { endSubs -> - val result = if (yieldEnd) (newSubs + endSubs) else newSubs - yield(Result.success(result)) - } - - } - } -} diff --git a/src/prolog/builtins/arithmeticOperators.kt b/src/prolog/builtins/arithmeticOperators.kt index 2a3b1fd..963a2ca 100644 --- a/src/prolog/builtins/arithmeticOperators.kt +++ b/src/prolog/builtins/arithmeticOperators.kt @@ -22,7 +22,7 @@ import prolog.logic.* * True if expression Expr1 evaluates to a number non-equal to Expr2. */ class EvaluatesToDifferent(private val left: Expression, private val right: Expression) : - Operator("=\\=", left, right), Satisfiable { + Operator(Atom("=\\="), left, right), Satisfiable { override fun satisfy(subs: Substitutions): Answers { val t1 = left.simplify(subs) val t2 = right.simplify(subs) @@ -49,7 +49,7 @@ class EvaluatesToDifferent(private val left: Expression, private val right: Expr * True if Expr1 evaluates to a number equal to Expr2. */ class EvaluatesTo(private val left: Expression, private val right: Expression) : - Operator("=:=", left, right) { + Operator(Atom("=:="), left, right) { override fun satisfy(subs: Substitutions): Answers { val t1 = left.simplify(subs) val t2 = right.simplify(subs) @@ -72,7 +72,7 @@ class EvaluatesTo(private val left: Expression, private val right: Expression) : * True when Number is the value to which Expr evaluates. */ class Is(val number: Expression, val expr: Expression) : - Operator("is", number, expr), Satisfiable { + Operator(Atom("is"), number, expr), Satisfiable { override fun satisfy(subs: Substitutions): Answers { val t1 = number.simplify(subs) val t2 = expr.simplify(subs) @@ -108,7 +108,7 @@ class Positive(operand: Expression) : Add(Integer(0), operand) * Result = Expr1 + Expr2 */ open class Add(private val expr1: Expression, private val expr2: Expression) : - ArithmeticOperator("+", expr1, expr2) { + ArithmeticOperator(Atom("+"), expr1, expr2) { override fun simplify(subs: Substitutions): Simplification { val result = Variable("Result") val map = plus(expr1, expr2, result, subs) @@ -126,7 +126,7 @@ open class Add(private val expr1: Expression, private val expr2: Expression) : * Result = Expr1 - Expr2 */ open class Subtract(private val expr1: Expression, private val expr2: Expression) : - ArithmeticOperator("-", expr1, expr2) { + ArithmeticOperator(Atom("-"), expr1, expr2) { override fun simplify(subs: Substitutions): Simplification { val result = Variable("Result") val map = plus(expr2, result, expr1, subs) @@ -144,7 +144,7 @@ open class Subtract(private val expr1: Expression, private val expr2: Expression * Result = Expr1 * Expr2 */ class Multiply(val expr1: Expression, val expr2: Expression) : - ArithmeticOperator("*", expr1, expr2) { + ArithmeticOperator(Atom("*"), expr1, expr2) { override fun simplify(subs: Substitutions): Simplification { val result = Variable("Result") val map = mul(expr1, expr2, result, subs) @@ -159,7 +159,7 @@ class Multiply(val expr1: Expression, val expr2: Expression) : } class Divide(private val expr1: Expression, private val expr2: Expression) : - ArithmeticOperator("/", expr1, expr2) { + ArithmeticOperator(Atom("/"), expr1, expr2) { override fun simplify(subs: Substitutions): Simplification { val result = Variable("Result") val map = div(expr1, expr2, result, subs) @@ -178,7 +178,7 @@ class Divide(private val expr1: Expression, private val expr2: Expression) : // TODO Expr rem Expr class Between(private val expr1: Expression, private val expr2: Expression, private val expr3: Expression) : - CompoundTerm("between", expr1, expr2, expr3), Satisfiable { + CompoundTerm(Atom("between"), listOf(expr1, expr2, expr3)), Satisfiable { override fun satisfy(subs: Substitutions): Answers { val e1 = expr1.simplify(subs) val e2 = expr2.simplify(subs) @@ -210,6 +210,6 @@ class Between(private val expr1: Expression, private val expr2: Expression, priv } class Successor(private val expr1: Expression, private val expr2: Expression) : - CompoundTerm("succ", expr1, expr2), Satisfiable { + CompoundTerm(Atom("succ"), listOf(expr1, expr2)), Satisfiable { override fun satisfy(subs: Substitutions): Answers = succ(expr1, expr2, subs) } diff --git a/src/prolog/builtins/controlOperators.kt b/src/prolog/builtins/controlOperators.kt index 3d81786..c1376f9 100644 --- a/src/prolog/builtins/controlOperators.kt +++ b/src/prolog/builtins/controlOperators.kt @@ -48,7 +48,7 @@ class Cut() : Atom("!") { * Conjunction (and). True if both Goal1 and Goal2 are true. */ open class Conjunction(val left: LogicOperand, private val right: LogicOperand) : - LogicOperator(",", left, right) { + LogicOperator(Atom(","), left, right) { override fun satisfy(subs: Substitutions): Answers = sequence { fun satisfyRight(leftSubs: Substitutions): Answers = sequence { right.satisfy(subs + leftSubs).forEach { right -> @@ -123,7 +123,7 @@ open class Conjunction(val left: LogicOperand, private val right: LogicOperand) * Disjunction (or). True if either Goal1 or Goal2 succeeds. */ open class Disjunction(private val left: LogicOperand, private val right: LogicOperand) : - LogicOperator(";", left, right) { + LogicOperator(Atom(";"), left, right) { override fun satisfy(subs: Substitutions): Answers = sequence { left.satisfy(subs).forEach { left -> left.fold( @@ -158,7 +158,7 @@ class Bar(leftOperand: LogicOperand, rightOperand: LogicOperand) : Disjunction(l /** * True if 'Goal' cannot be proven. */ -open class Not(private val goal: Goal) : LogicOperator("\\+", rightOperand = goal) { +class Not(private val goal: Goal) : LogicOperator(Atom("\\+"), rightOperand = goal) { override fun satisfy(subs: Substitutions): Answers { // If the goal can be proven, return an empty sequence val goalResults = goal.satisfy(subs).iterator() diff --git a/src/prolog/builtins/databaseOperators.kt b/src/prolog/builtins/databaseOperators.kt index 922201f..ddfa471 100644 --- a/src/prolog/builtins/databaseOperators.kt +++ b/src/prolog/builtins/databaseOperators.kt @@ -49,7 +49,7 @@ class Assert(clause: Clause) : AssertZ(clause) { /** * Assert a [Clause] as a first clause of the [Predicate] into the [Program]. */ -class AssertA(val clause: Clause) : Operator("asserta", rightOperand = clause) { +class AssertA(val clause: Clause) : Operator(Atom("asserta"), null, clause) { override fun satisfy(subs: Substitutions): Answers { // Add clause to the program val evaluatedClause = applySubstitution(clause, subs) as Clause @@ -64,7 +64,7 @@ class AssertA(val clause: Clause) : Operator("asserta", rightOperand = clause) { /** * Assert a [Clause] as a last clause of the [Predicate] into the [Program]. */ -open class AssertZ(val clause: Clause) : Operator("assertz", rightOperand = clause) { +open class AssertZ(val clause: Clause) : Operator(Atom("assertz"), null, clause) { override fun satisfy(subs: Substitutions): Answers { // Add clause to the program val evaluatedClause = applySubstitution(clause, subs) as Clause @@ -82,7 +82,7 @@ open class AssertZ(val clause: Clause) : Operator("assertz", rightOperand = clau * * @see [SWI-Prolog Predicate retract/1](https://www.swi-prolog.org/pldoc/doc_for?object=retract/1) */ -open class Retract(val term: Term) : Operator("retract", rightOperand = term) { +open class Retract(val term: Term) : Operator(Atom("retract"), null, term) { override fun satisfy(subs: Substitutions): Answers = sequence { // Check that term is a structure or atom if (term !is Structure && term !is Atom) { diff --git a/src/prolog/builtins/delimitedContinuationsOperators.kt b/src/prolog/builtins/delimitedContinuationsOperators.kt index b6d18fa..5a01eb4 100644 --- a/src/prolog/builtins/delimitedContinuationsOperators.kt +++ b/src/prolog/builtins/delimitedContinuationsOperators.kt @@ -23,7 +23,7 @@ import prolog.logic.unifyLazy * return, unifying Cont with a Goal that represents the continuation after shift. */ class Reset(private val goal: Goal, private val ball: Term, private val cont: Term) : - Structure("reset", goal, ball, cont) { + Structure(Atom("reset"), listOf(goal, ball, cont)) { override fun satisfy(subs: Substitutions): Answers = sequence { goal.satisfy(subs).forEach { goalResult -> goalResult.fold( @@ -63,7 +63,7 @@ class Reset(private val goal: Goal, private val ball: Term, private val cont: Te /** * Variables that have been bound during the procedure called by reset/3 stay bound after a shift/1: */ -class Shift(private val ball: Term) : Structure("shift", ball) { +class Shift(private val ball: Term) : Structure(Atom("shift"), listOf(ball)) { override fun satisfy(subs: Substitutions): Answers = sequence { val shift = AppliedShift( subs = subs, diff --git a/src/prolog/builtins/ioOperators.kt b/src/prolog/builtins/ioOperators.kt index e841679..514690c 100644 --- a/src/prolog/builtins/ioOperators.kt +++ b/src/prolog/builtins/ioOperators.kt @@ -16,7 +16,7 @@ import prolog.logic.unifyLazy /** * Write [Term] to the current output, using brackets and operators where appropriate. */ -class Write(private val term: Term) : Operator("write", rightOperand = term), Satisfiable { +class Write(private val term: Term) : Operator(Atom("write"), null, term), Satisfiable { constructor(message: String) : this(Atom(message)) override fun satisfy(subs: Substitutions): Answers { diff --git a/src/prolog/builtins/listOperators.kt b/src/prolog/builtins/listOperators.kt index 9835c44..d1a1944 100644 --- a/src/prolog/builtins/listOperators.kt +++ b/src/prolog/builtins/listOperators.kt @@ -5,28 +5,18 @@ import prolog.Substitutions import prolog.ast.lists.List import prolog.ast.lists.List.Cons import prolog.ast.lists.List.Empty -import prolog.ast.terms.Body +import prolog.ast.terms.Atom import prolog.ast.terms.Operator -import prolog.ast.terms.Structure import prolog.ast.terms.Term -import prolog.ast.terms.Variable import prolog.logic.applySubstitution -import prolog.logic.unifyLazy -class Member(private val element: Term, private val list: Term) : Operator("member", element, list) { - private var solution: Body = when (list) { - is Empty -> Fail +class Member(private val element: Term, private val list: List) : Operator(Atom("member"), element, list) { + private var solution: Operator = when (list) { + is Empty -> Disjunction(Fail, Fail) is Cons -> Disjunction( Unify(element, list.head), Member(element, list.tail) ) - - else -> { - // Generate a sequence of lists that have anonymous variables in them. - // Place element at each index - // TODO Fix this - Unify(element, list) - } } override fun satisfy(subs: Substitutions): Answers = solution.satisfy(subs) @@ -38,41 +28,3 @@ class Member(private val element: Term, private val list: Term) : Operator("memb override fun toString(): String = "$element ∈ $list" } - -class Append(private val list1: Term, private val list2: Term, private val list3: Term) : - Structure("append", list1, list2, list3) { - override fun satisfy(subs: Substitutions): Answers = sequence { - val l1 = applySubstitution(list1, subs) - val l2 = applySubstitution(list2, subs) - val l3 = applySubstitution(list3, subs) - - if (l1 is Empty) { - yieldAll(unifyLazy(l2, l3, subs)) - } - - val head1 = if (l1 is Cons) l1.head else Variable("Head1") - val tail1 = if (l1 is Cons) l1.tail else Variable("Tail1") - val head3 = if (l3 is Cons) l3.head else Variable("Head3") - val tail3 = if (l3 is Cons) l3.tail else Variable("Tail3") - - unifyLazy(head1, head3, subs).forEach { headResult -> - headResult.map { headSubs -> - val newSubs = subs + headSubs - Append(tail1, list2, tail3).satisfy(newSubs).forEach { tailResult -> - tailResult.map { tailSubs -> - val result = headSubs + tailSubs - yield(Result.success(result)) - } - } - } - } - - TODO("This does not return the expected results, especially when using variables for the lists.") - } - - override fun applySubstitution(subs: Substitutions): Append = Append( - applySubstitution(list1, subs), - applySubstitution(list2, subs), - applySubstitution(list3, subs) - ) -} diff --git a/src/prolog/builtins/metaOperators.kt b/src/prolog/builtins/metaOperators.kt index 2477c26..047fa5f 100644 --- a/src/prolog/builtins/metaOperators.kt +++ b/src/prolog/builtins/metaOperators.kt @@ -9,7 +9,7 @@ import prolog.ast.terms.Term import prolog.flags.AppliedCut import prolog.logic.applySubstitution -class Call(private val goal: Term) : Operator("call", rightOperand = goal) { +class Call(private val goal: Term) : Operator(Atom("call"), null, goal) { override fun satisfy(subs: Substitutions): Answers { val appliedGoal = applySubstitution(goal, subs) as Goal return appliedGoal.satisfy(subs) @@ -19,7 +19,7 @@ class Call(private val goal: Term) : Operator("call", rightOperand = goal) { /** * Calls [Goal] once, but succeeds, regardless of whether Goal succeeded or not. */ -class Ignore(goal: Goal) : Operator("ignore", rightOperand = goal) { +class Ignore(goal: Goal) : Operator(Atom("ignore"), null, goal) { private val disjunction = Disjunction( Conjunction(Call(goal), Cut()), True diff --git a/src/prolog/builtins/other.kt b/src/prolog/builtins/other.kt index 3c5599c..56c99d1 100644 --- a/src/prolog/builtins/other.kt +++ b/src/prolog/builtins/other.kt @@ -3,15 +3,18 @@ package prolog.builtins import prolog.Answers 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(":-", rightOperand = goal) { +class Initialization(val goal: LogicOperand) : LogicOperator(Atom(":-"), null, goal) { override fun satisfy(subs: Substitutions): Answers = goal.satisfy(subs).take(1) override fun toString(): String = goal.toString() } -class Query(val query: LogicOperand) : LogicOperator("?-", rightOperand = query) { +class Query(val query: LogicOperand) : LogicOperator(Atom("?-"), null, query) { override fun satisfy(subs: Substitutions): Answers = query.satisfy(subs) } @@ -21,8 +24,7 @@ class Query(val query: LogicOperand) : LogicOperator("?-", rightOperand = query) * * @see [SWI-Prolog Predicate forall/2](https://www.swi-prolog.org/pldoc/doc_for?object=forall/2) */ -class ForAll(private val condition: LogicOperand, private val action: Goal) : - Not(Conjunction(condition, Not(action))) { - override fun toString() = "forall($condition, $action)" +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/src/prolog/builtins/unificationOperators.kt b/src/prolog/builtins/unificationOperators.kt index c00175d..5ebeed3 100644 --- a/src/prolog/builtins/unificationOperators.kt +++ b/src/prolog/builtins/unificationOperators.kt @@ -7,6 +7,7 @@ package prolog.builtins import prolog.Answers import prolog.Substitutions +import prolog.ast.terms.Atom import prolog.ast.terms.Operator import prolog.ast.terms.Term import prolog.logic.applySubstitution @@ -16,7 +17,7 @@ import prolog.logic.unifyLazy /** * Unify Term1 with Term2. True if the unification succeeds. */ -class Unify(private val term1: Term, private val term2: Term): Operator("=", term1, term2) { +class Unify(private val term1: Term, private val term2: Term): Operator(Atom("="), term1, term2) { override fun satisfy(subs: Substitutions): Answers = sequence { val t1 = applySubstitution(term1, subs) val t2 = applySubstitution(term2, subs) @@ -30,11 +31,16 @@ class Unify(private val term1: Term, private val term2: Term): Operator("=", ter ) } -class NotUnify(private val term1: Term, private val term2: Term) : Not(Unify(term1, term2)) { - override fun toString(): String = "($term1 \\= $term2)" +class NotUnify(private val term1: Term, private val term2: Term) : Operator(Atom("\\="), term1, term2) { + private val not = Not(Unify(term1, term2)) + override fun satisfy(subs: Substitutions): Answers = not.satisfy(subs) + override fun applySubstitution(subs: Substitutions): NotUnify = NotUnify( + applySubstitution(term1, subs), + applySubstitution(term2, subs) + ) } -class Equivalent(private val term1: Term, private val term2: Term) : Operator("==", term1, term2) { +class Equivalent(private val term1: Term, private val term2: Term) : Operator(Atom("=="), term1, term2) { override fun satisfy(subs: Substitutions): Answers = sequence { val t1 = applySubstitution(term1, subs) val t2 = applySubstitution(term2, subs) @@ -50,6 +56,11 @@ class Equivalent(private val term1: Term, private val term2: Term) : Operator("= ) } -class NotEquivalent(private val term1: Term, private val term2: Term) : Not(Equivalent(term1, term2)) { - override fun toString(): String = "($term1 \\== $term2)" +class NotEquivalent(private val term1: Term, private val term2: Term) : Operator(Atom("\\=="), term1, term2) { + private val not = Not(Equivalent(term1, term2)) + override fun satisfy(subs: Substitutions): Answers = not.satisfy(subs) + override fun applySubstitution(subs: Substitutions): NotEquivalent = NotEquivalent( + applySubstitution(term1, subs), + applySubstitution(term2, subs) + ) } diff --git a/src/prolog/builtins/verificationOperators.kt b/src/prolog/builtins/verificationOperators.kt deleted file mode 100644 index fc87091..0000000 --- a/src/prolog/builtins/verificationOperators.kt +++ /dev/null @@ -1,52 +0,0 @@ -package prolog.builtins - -import prolog.Answers -import prolog.Substitutions -import prolog.ast.terms.Operator -import prolog.ast.terms.Term -import prolog.logic.* - -class Atomic(private val term: Term) : Operator("atomic", rightOperand = term) { - override fun satisfy(subs: Substitutions): Answers { - if (atomic(term, subs)) { - return sequenceOf(Result.success(emptyMap())) - } - return emptySequence() - } - - override fun applySubstitution(subs: Substitutions): Atomic = Atomic(applySubstitution(term, subs)) -} - -class Compound(private val term: Term) : Operator("compound", rightOperand = term) { - override fun satisfy(subs: Substitutions): Answers { - if (compound(term, subs)) { - return sequenceOf(Result.success(emptyMap())) - } - return emptySequence() - } - - override fun applySubstitution(subs: Substitutions): Compound = Compound(applySubstitution(term, subs)) -} - -class NonVar(private val term: Term) : Operator("nonvar", rightOperand = term) { - override fun satisfy(subs: Substitutions): Answers { - if (nonvariable(term, subs)) { - return sequenceOf(Result.success(emptyMap())) - } - - return emptySequence() - } - - override fun applySubstitution(subs: Substitutions): NonVar = NonVar(applySubstitution(term, subs)) -} - -class Var(private val term: Term) : Operator("var", rightOperand = term) { - override fun satisfy(subs: Substitutions): Answers { - if (variable(term, subs)) { - return sequenceOf(Result.success(emptyMap())) - } - return emptySequence() - } - - override fun applySubstitution(subs: Substitutions): Var = Var(applySubstitution(term, subs)) -} diff --git a/src/prolog/logic/terms.kt b/src/prolog/logic/terms.kt index 459d58d..8c2b26f 100644 --- a/src/prolog/logic/terms.kt +++ b/src/prolog/logic/terms.kt @@ -1,10 +1,29 @@ package prolog.logic import prolog.Substitutions +import prolog.ast.terms.Atom import prolog.ast.terms.Structure import prolog.ast.terms.Term import prolog.ast.terms.Variable +/** + * True when Term is a term with functor Name/Arity. If Term is a variable it is unified with a new term whose + * arguments are all different variables (such a term is called a skeleton). If Term is atomic, Arity will be unified + * with the integer 0, and Name will be unified with Term. Raises instantiation_error() if Term is unbound and + * Name/Arity is insufficiently instantiated. + * + * SWI-Prolog also supports terms with arity 0, as in a() (see + * [section 5](https://www.swi-prolog.org/pldoc/man?section=extensions)). Such terms must be processed using functor/4 + * or compound_name_arity/3. The predicate functor/3 and =../2 raise a domain_error when faced with these terms. + * Without this precaution a round trip of a term with arity 0 over functor/3 would create an atom. + * + * Source: [SWI-Prolog Predicate functor/3](https://www.swi-prolog.org/pldoc/doc_for?object=functor/3) + */ +fun functor(term: Term, name: Atom, arity: Int): Boolean { + // TODO Implement + return true +} + /** * Unify the free variables in Term with a term $VAR(N), where N is the number of the variable. * Counting starts at Start. diff --git a/tests/interpreter/ParserPreprocessorIntegrationTests.kt b/tests/interpreter/ParserPreprocessorIntegrationTests.kt index cf1cd94..05df756 100644 --- a/tests/interpreter/ParserPreprocessorIntegrationTests.kt +++ b/tests/interpreter/ParserPreprocessorIntegrationTests.kt @@ -41,7 +41,10 @@ class ParserPreprocessorIntegrationTests { val parsed = parser.parseToEnd("X is $input") as Term assertEquals( - Structure("is", Variable("X"), Structure("-",number)), + Structure(Atom("is"), listOf( + Variable("X"), + Structure(Atom("-"), listOf(number)), + )), parsed ) @@ -71,7 +74,7 @@ class ParserPreprocessorIntegrationTests { val result = parser.parseToEnd(input) as Term assertEquals( - Structure("is", Variable("X"), Structure("-", Integer(1), Integer(2))), + Structure(Atom("is"), listOf(Variable("X"), Structure(Atom("-"), listOf(Integer(1), Integer(2))))), result ) diff --git a/tests/interpreter/PreprocessorTests.kt b/tests/interpreter/PreprocessorTests.kt index 60bcbf9..ace7862 100644 --- a/tests/interpreter/PreprocessorTests.kt +++ b/tests/interpreter/PreprocessorTests.kt @@ -37,7 +37,7 @@ class PreprocessorTests { @Test fun `multiple anonymous variables should be unique`() { - val input = CompoundTerm("foo", Variable("_"), Variable("_")) + val input = CompoundTerm(Atom("foo"), listOf(Variable("_"), Variable("_"))) val result = preprocessor.preprocess(input) @@ -68,7 +68,7 @@ class PreprocessorTests { for (argument in inner.arguments) { if ((argument as Variable).name != "Name") { assertTrue( - argument.name.matches("_\\d+".toRegex()), + (argument as Variable).name.matches("_\\d+".toRegex()), "Expected anonymous variable name, but got ${argument.name}" ) } @@ -83,13 +83,27 @@ class PreprocessorTests { test( mapOf( Atom("=\\=") to Atom("=\\="), - CompoundTerm("=\\=") to CompoundTerm("=\\="), + CompoundTerm(Atom("=\\="), emptyList()) to CompoundTerm(Atom("=\\="), emptyList()), Atom("EvaluatesToDifferent") to Atom("EvaluatesToDifferent"), - CompoundTerm("EvaluatesToDifferent") to CompoundTerm("EvaluatesToDifferent"), - CompoundTerm("=\\=", Atom("a")) to CompoundTerm("=\\=", Atom("a")), - CompoundTerm("=\\=", Integer(1)) to CompoundTerm("=\\=", Integer(1)), - CompoundTerm("=\\=", Atom("=\\=")) to CompoundTerm("=\\=", Atom("=\\=")), - CompoundTerm("=\\=", Integer(1), Integer(2)) to EvaluatesToDifferent(Integer(1), Integer(2)) + CompoundTerm(Atom("EvaluatesToDifferent"), emptyList()) to CompoundTerm( + Atom("EvaluatesToDifferent"), + emptyList() + ), + CompoundTerm(Atom("=\\="), listOf(Atom("a"))) to CompoundTerm( + Atom("=\\="), + listOf(Atom("a")) + ), + CompoundTerm(Atom("=\\="), listOf(Integer(1))) to CompoundTerm( + Atom("=\\="), + listOf(Integer(1)) + ), + CompoundTerm(Atom("=\\="), listOf(Atom("=\\="))) to CompoundTerm( + Atom("=\\="), + listOf(Atom("=\\=")) + ), + CompoundTerm(Atom("=\\="), listOf(Integer(1), Integer(2))) to EvaluatesToDifferent( + Integer(1), Integer(2) + ) ) ) } @@ -99,7 +113,7 @@ class PreprocessorTests { test( mapOf( Atom("=:=") to Atom("=:="), - CompoundTerm("=:=") to CompoundTerm("=:="), + CompoundTerm(Atom("=:="), emptyList()) to CompoundTerm(Atom("=:="), emptyList()), Atom("EvaluatesTo") to Atom("EvaluatesTo"), CompoundTerm(Atom("EvaluatesTo"), emptyList()) to CompoundTerm( Atom("EvaluatesTo"), diff --git a/tests/prolog/builtins/DelimitedContinuationsOperatorsTests.kt b/tests/prolog/builtins/DelimitedContinuationsOperatorsTests.kt index 7d461d0..994a992 100644 --- a/tests/prolog/builtins/DelimitedContinuationsOperatorsTests.kt +++ b/tests/prolog/builtins/DelimitedContinuationsOperatorsTests.kt @@ -12,6 +12,8 @@ import prolog.ast.logic.Rule import prolog.ast.terms.Atom import prolog.ast.terms.Structure import prolog.ast.terms.Variable +import java.io.ByteArrayOutputStream +import java.io.PrintStream class DelimitedContinuationsOperatorsTests { @BeforeEach diff --git a/tests/prolog/builtins/ListOperatorsTests.kt b/tests/prolog/builtins/ListOperatorsTests.kt index f6d0b71..d0c44c2 100644 --- a/tests/prolog/builtins/ListOperatorsTests.kt +++ b/tests/prolog/builtins/ListOperatorsTests.kt @@ -1,6 +1,5 @@ package prolog.builtins -import com.sun.source.tree.EmptyStatementTree import org.junit.jupiter.api.Assertions.assertEquals import org.junit.jupiter.api.Assertions.assertTrue import org.junit.jupiter.api.Disabled @@ -8,7 +7,6 @@ import org.junit.jupiter.api.Test import prolog.ast.lists.List.Cons import prolog.ast.lists.List.Empty import prolog.ast.terms.Atom -import prolog.ast.terms.Term import prolog.ast.terms.Variable class ListOperatorsTests { @@ -72,161 +70,4 @@ class ListOperatorsTests { assertTrue(result[0].isSuccess, "Expected success") assertEquals(atom, result[0].getOrNull()!![variable], "Expected variable to be unified with atom") } - - @Disabled("Not implemented yet") - @Test - fun `appended empty lists is an empty list`() { - val append = Append(Empty, Empty, Empty) - - val result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitution map") - } - - @Disabled("Not implemented yet") - @Test - fun `appending two empty lists gives an empty list`() { - val list1 = Empty - val list2 = Empty - val list12 = Variable("Result") - - val append = Append(list1, list2, list12) - - val result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - val subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected one substitution") - assertEquals(Empty, subs[list12], "Expected result to be empty list") - } - - @Disabled("Not implemented yet") - @Test - fun `appending an empty list to another list gives that list`() { - val nonempty = Cons(Atom("a"), Empty) - - var append = Append(nonempty, Empty, Empty) - var result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitution map") - - append = Append(Empty, nonempty, Empty) - result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitution map") - - val variable = Variable("List1AndList2") - - append = Append(Empty, nonempty, variable) - result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - var subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected one substitution") - assertEquals(nonempty, subs[variable], "Expected result to be nonempty list") - - append = Append(nonempty, Empty, variable) - result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected one substitution") - } - - @Disabled("Not implemented yet") - @Test - fun `appending two lists gives combined list`() { - val list1 = Cons(Atom("a"), Cons(Atom("b"), Empty)) - val list2 = Cons(Atom("c"), Cons(Atom("d"), Empty)) - val list3 = Cons(Atom("a"), Cons(Atom("b"), Cons(Atom("c"), Cons(Atom("d"), Empty)))) - val list4 = Cons(Atom("c"), Cons(Atom("d"), Cons(Atom("a"), Cons(Atom("b"), Empty)))) - - var append = Append(list1, list2, list3) - var result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitution map") - - val variable = Variable("List1AndList2") - - append = Append(list1, list2, variable) - result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - var subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected one substitution") - assertEquals(list3, subs[variable], "Expected result to be combined list") - - append = Append(list2, list1, variable) - result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected one substitution") - assertEquals(list4, subs[variable], "Expected result to be combined list") - } - - @Disabled("Not implemented yet") - @Test - fun `you can find the appended list`() { - val list1 = Cons(Atom("a"), Cons(Atom("b"), Empty)) - val list2: Term = Variable("List2") - val list3 = Cons(Atom("a"), Cons(Atom("b"), Cons(Atom("c"), Cons(Atom("d"), Empty)))) - - var append = Append(list1, list2, list1) - var result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - var subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected one substitution") - assertEquals(Empty, subs[list2], "Expected result to be empty list") - - append = Append(list1, list2, list3) - result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected one substitution") - assertEquals(Cons(Atom("c"), Cons(Atom("d"), Empty)), subs[list2], "Expected result to be list with c and d") - } - - @Disabled("Not implemented yet") - @Test - fun `you can find the prepended list`() { - val list1 = Variable("List1") - val list2 = Cons(Atom("c"), Cons(Atom("d"), Empty)) - val list3 = Cons(Atom("a"), Cons(Atom("b"), Cons(Atom("c"), Cons(Atom("d"), Empty)))) - - var append = Append(list1, list2, list2) - var result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - var subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected one substitution") - assertEquals(Empty, subs[list1], "Expected result to be empty list") - - append = Append(list1, list2, list3) - result = append.satisfy(emptyMap()).toList() - - assertEquals(1, result.size, "Expected one solution") - assertTrue(result[0].isSuccess, "Expected success") - subs = result[0].getOrNull()!! - assertEquals(1, subs.size, "Expected one substitution") - assertEquals(Cons(Atom("a"), Cons(Atom("b"), Empty)), subs[list1], "Expected result to be list with a and b") - } } \ No newline at end of file diff --git a/tests/prolog/logic/TermAnalysisConstructionTest.kt b/tests/prolog/logic/TermAnalysisConstructionTest.kt index 7000a49..c1033a9 100644 --- a/tests/prolog/logic/TermAnalysisConstructionTest.kt +++ b/tests/prolog/logic/TermAnalysisConstructionTest.kt @@ -1,9 +1,9 @@ package prolog.logic -import org.junit.jupiter.api.Assertions.* +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.Functor import prolog.ast.terms.Structure /** @@ -19,12 +19,12 @@ class TermAnalysisConstructionTest { assertTrue(atomic(atom)) assertFalse(compound(atom)) - assertEquals(Functor("foo", 0), atom.functor) + assertTrue(functor(atom, Atom("foo"), 0)) } @Test fun compound_arity_0_properties() { - val structure = Structure("foo") + val structure = Structure(Atom("foo"), emptyList()) assertFalse(atomic(structure)) assertTrue(compound(structure)) @@ -32,11 +32,11 @@ class TermAnalysisConstructionTest { @Test fun compound_arity_1_properties() { - val structure = Structure("foo", Atom("bar")) + val structure = Structure(Atom("foo"), listOf(Atom("bar"))) assertFalse(atomic(structure)) assertTrue(compound(structure)) - assertEquals(Functor("foo", 1), structure.functor) + assertTrue(functor(structure, Atom("foo"), 1)) } } \ No newline at end of file