tdpeuter/2025LogProg-project-GhentProlog
tdpeuter/2025LogProg-project-GhentProlog
Archived
1
Fork 0
Code Issues Releases Activity Actions

Sync

Browse source
This commit is contained in:
Tibo De Peuter 2025-05-05 18:04:37 +02:00
parent a937b1bc44
commit fc8b83fca3
8 changed files with 117 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/prolog/ast/logic/Clause.kt
View file

@ -27,27 +27,21 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent {
// Only if the body can be proven, the substitutions should be returned.
// Do this in a lazy way.
val preHead = applySubstitution(head, subs)
val preGoal = applySubstitution(goal, subs)
val (headEnd, headRenaming) = numbervars(preHead, Program.variableRenamingStart, subs)
val headReverse = headRenaming.entries.associate { (a, b) -> b to a }
val (headEnd, headRenaming) = numbervars(head, Program.variableRenamingStart, subs)
Program.variableRenamingStart = headEnd
val renamedHead = applySubstitution(head, headRenaming)
unifyLazy(preGoal, renamedHead, subs).forEach { headAnswer ->
unifyLazy(goal, renamedHead, subs).forEach { headAnswer ->
headAnswer.map { headSubs ->
// If the body can be proven, yield the (combined) substitutions
val preBody = applySubstitution(body, headRenaming + headSubs) as Body
preBody.satisfy(subs).forEach { bodyAnswer ->
bodyAnswer.fold(
onSuccess = { bodySubs ->
var result = (headSubs + bodySubs)
.mapKeys { applySubstitution(it.key, headReverse) }
.mapValues { applySubstitution(it.value, headReverse) }
result = result.map { it.key to applySubstitution(it.value, result) }
.toMap()
.filterNot { it.key in headRenaming.keys && !occurs(it.key as Variable, goal, emptyMap())}
val newSubs = headSubs + bodySubs
val result = newSubs
.mapValues { applySubstitution(it.value, newSubs) }
.filter { it.key !is AnonymousVariable && occurs(it.key as Variable, goal, emptyMap()) }
yield(Result.success(result))
},
onFailure = { error ->

1
src/prolog/ast/terms/Term.kt
View file

@ -15,5 +15,4 @@ import prolog.ast.arithmetic.Float
interface Term : Comparable<Term>, Cloneable {
override fun compareTo(other: Term): Int = compare(this, other, emptyMap())
fun applySubstitution(subs: Substitutions): Term
public override fun clone(): Term
}

40
src/prolog/builtins/arithmeticOperators.kt
View file

@ -39,6 +39,10 @@ class EvaluatesToDifferent(private val left: Expression, private val right: Expr
}
}
override fun applySubstitution(subs: Substitutions): EvaluatesToDifferent = EvaluatesToDifferent(
left.applySubstitution(subs) as Expression,
right.applySubstitution(subs) as Expression
)
}
/**
@ -57,6 +61,11 @@ class EvaluatesTo(private val left: Expression, private val right: Expression) :
return if (equivalent(t1.to, t2.to, subs)) sequenceOf(Result.success(emptyMap())) else emptySequence()
}
override fun applySubstitution(subs: Substitutions): EvaluatesTo = EvaluatesTo(
left.applySubstitution(subs) as Expression,
right.applySubstitution(subs) as Expression
)
}
/**
@ -78,6 +87,11 @@ class Is(val number: Expression, val expr: Expression) :
return unifyLazy(t1.to, t2.to, subs)
}
override fun applySubstitution(subs: Substitutions): Is = Is(
number.applySubstitution(subs) as Expression,
expr.applySubstitution(subs) as Expression
)
}
/**
@ -101,6 +115,11 @@ open class Add(private val expr1: Expression, private val expr2: Expression) :
val simplification = result.simplify(map.first().getOrThrow())
return Simplification(this, simplification.to)
}
override fun applySubstitution(subs: Substitutions): Add = Add(
expr1.applySubstitution(subs) as Expression,
expr2.applySubstitution(subs) as Expression
)
}
/**
@ -114,6 +133,11 @@ open class Subtract(private val expr1: Expression, private val expr2: Expression
val simplification = result.simplify(map.first().getOrThrow())
return Simplification(this, simplification.to)
}
override fun applySubstitution(subs: Substitutions): Subtract = Subtract(
expr1.applySubstitution(subs) as Expression,
expr2.applySubstitution(subs) as Expression
)
}
/**
@ -127,6 +151,11 @@ class Multiply(val expr1: Expression, val expr2: Expression) :
val simplification = result.simplify(map.first().getOrThrow())
return Simplification(this, simplification.to)
}
override fun applySubstitution(subs: Substitutions): Multiply = Multiply(
expr1.applySubstitution(subs) as Expression,
expr2.applySubstitution(subs) as Expression
)
}
class Divide(private val expr1: Expression, private val expr2: Expression) :
@ -137,6 +166,11 @@ class Divide(private val expr1: Expression, private val expr2: Expression) :
val simplification = result.simplify(map.first().getOrThrow())
return Simplification(this, simplification.to)
}
override fun applySubstitution(subs: Substitutions): Divide = Divide(
expr1.applySubstitution(subs) as Expression,
expr2.applySubstitution(subs) as Expression
)
}
// TODO Expr mod Expr
@ -166,5 +200,11 @@ class Between(private val expr1: Expression, private val expr2: Expression, priv
}
}
override fun applySubstitution(subs: Substitutions): Between = Between(
expr1.applySubstitution(subs) as Expression,
expr2.applySubstitution(subs) as Expression,
expr3.applySubstitution(subs) as Expression
)
override fun toString(): String = "$expr1..$expr3..$expr2"
}

14
src/prolog/builtins/controlOperators.kt
View file

@ -9,12 +9,14 @@ import prolog.ast.terms.Body
import prolog.ast.terms.Goal
import prolog.ast.terms.Structure
import prolog.flags.AppliedCut
import prolog.logic.applySubstitution
/**
* Always fail.
*/
object Fail : Atom("fail"), Body {
override fun satisfy(subs: Substitutions): Answers = emptySequence()
override fun applySubstitution(subs: Substitutions): Fail = Fail
}
/**
@ -27,6 +29,7 @@ typealias False = Fail
*/
object True : Atom("true"), Body {
override fun satisfy(subs: Substitutions): Answers = sequenceOf(Result.success(emptyMap()))
override fun applySubstitution(subs: Substitutions): True = True
}
// TODO Repeat/0
@ -99,8 +102,8 @@ class Conjunction(val left: LogicOperand, private val right: LogicOperand) :
}
override fun applySubstitution(subs: Substitutions): Conjunction = Conjunction(
left.applySubstitution(subs) as LogicOperand,
right.applySubstitution(subs) as LogicOperand
applySubstitution(left, subs) as LogicOperand,
applySubstitution(right, subs) as LogicOperand
)
}
@ -114,10 +117,9 @@ open class Disjunction(private val left: LogicOperand, private val right: LogicO
yieldAll(right.satisfy(subs))
}
override fun clone(): Disjunction = Disjunction(left.clone() as LogicOperand, right.clone() as LogicOperand)
override fun applySubstitution(subs: Substitutions): Disjunction = Disjunction(
left.applySubstitution(subs) as LogicOperand,
right.applySubstitution(subs) as LogicOperand
applySubstitution(left, subs) as LogicOperand,
applySubstitution(right, subs) as LogicOperand
)
}
@ -141,4 +143,6 @@ class Not(private val goal: Goal) : LogicOperator(Atom("\\+"), rightOperand = go
// If the goal cannot be proven, return a sequence with an empty map
return sequenceOf(Result.success(emptyMap()))
}
override fun applySubstitution(subs: Substitutions): Not = Not(applySubstitution(goal, subs) as Goal)
}

6
src/prolog/builtins/databaseOperators.kt
View file

@ -62,6 +62,8 @@ class AssertA(val clause: Clause) : Operator(Atom("asserta"), null, clause) {
return sequenceOf(Result.success(emptyMap()))
}
override fun applySubstitution(subs: Substitutions): AssertA = AssertA(applySubstitution(clause, subs) as Clause)
}
/**
@ -75,6 +77,8 @@ open class AssertZ(val clause: Clause) : Operator(Atom("assertz"), null, clause)
return sequenceOf(Result.success(emptyMap()))
}
override fun applySubstitution(subs: Substitutions): AssertZ = AssertZ(applySubstitution(clause, subs) as Clause)
}
/**
@ -113,4 +117,6 @@ class Retract(val term: Term) : Operator(Atom("retract"), null, term) {
}
}
}
override fun applySubstitution(subs: Substitutions): Retract = Retract(applySubstitution(term, subs))
}

6
src/prolog/builtins/ioOperators.kt
View file

@ -27,6 +27,8 @@ class Write(private val term: Term) : Operator(Atom("write"), null, term), Satis
return sequenceOf(Result.success(emptyMap()))
}
override fun applySubstitution(subs: Substitutions): Write = Write(applySubstitution(term, subs))
override fun toString(): String = "write($term)"
}
@ -39,6 +41,8 @@ object Nl : Atom("nl"), Satisfiable {
Program.storeNewLine = false
return sequenceOf(Result.success(emptyMap()))
}
override fun applySubstitution(subs: Substitutions): Nl = this
}
/**
@ -72,4 +76,6 @@ class Read(private val term: Term) : Operator(Atom("read"), null, term), Satisfi
yieldAll(unifyLazy(t1, t2, subs))
}
override fun applySubstitution(subs: Substitutions): Read = Read(applySubstitution(term, subs))
}

16
src/prolog/builtins/unificationOperators.kt
View file

@ -24,11 +24,20 @@ class Unify(private val term1: Term, private val term2: Term): Operator(Atom("="
yieldAll(unifyLazy(t1, t2, subs))
}
override fun applySubstitution(subs: Substitutions): Unify = Unify(
applySubstitution(term1, subs),
applySubstitution(term2, subs)
)
}
class NotUnify(term1: Term, term2: Term) : Operator(Atom("\\="), 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(Atom("=="), term1, term2) {
@ -40,4 +49,9 @@ class Equivalent(private val term1: Term, private val term2: Term) : Operator(At
yield(Result.success(emptyMap()))
}
}
override fun applySubstitution(subs: Substitutions): Equivalent = Equivalent(
applySubstitution(term1, subs),
applySubstitution(term2, subs)
)
}

35
tests/prolog/EvaluationTests.kt
View file

@ -14,6 +14,8 @@ import prolog.ast.terms.Atom
import prolog.ast.terms.Structure
import prolog.ast.terms.Variable
import prolog.ast.Database.Program
import prolog.ast.arithmetic.Integer
import prolog.ast.terms.AnonymousVariable
class EvaluationTests {
@BeforeEach
@ -418,4 +420,37 @@ class EvaluationTests {
assertEquals(Atom("bob"), subs5[Variable("Person")], "Expected bob")
}
}
@Test
fun `leq Peano`() {
val fact = Fact(Structure(Atom("leq"), listOf(Integer(0), AnonymousVariable.create())))
val rule = Rule(
Structure(Atom("leq"), listOf(Structure(Atom("s"), listOf(Variable("X"))), Structure(Atom("s"), listOf(Variable("Y"))))),
Structure(Atom("leq"), listOf(Variable("X"), Variable("Y"))),
)
Program.db.load(listOf(fact, rule))
val result1 = Program.query(Structure(Atom("leq"), listOf(Variable("X"), Integer(0)))).toList()
assertEquals(1, result1.size, "Expected 1 result")
assertTrue(result1[0].isSuccess, "Expected success")
val subs = result1[0].getOrNull()!!
assertEquals(1, subs.size, "Expected 1 substitution")
assertEquals(Integer(0), subs[Variable("X")], "Expected X to be 0")
val result2 = Program.query(Structure(Atom("leq"), listOf(Variable("X"), Structure(Atom("s"), listOf(Integer(0)))))).toList()
assertEquals(2, result2.size, "Expected 2 results")
assertTrue(result2[0].isSuccess, "Expected success")
val subs2a = result2[0].getOrNull()!!
assertEquals(1, subs2a.size, "Expected 1 substitution")
assertEquals(Integer(0), subs2a[Variable("X")], "Expected X to be 0")
assertTrue(result2[1].isSuccess, "Expected success")
val subs2b = result2[1].getOrNull()!!
assertEquals(1, subs2b.size, "Expected 1 substitution")
assertEquals(Structure(Atom("s"), listOf(Integer(0))), subs2b[Variable("X")], "Expected X to be s(0)")
}
}