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 00:18:38 +02:00
parent a85169dced
commit a937b1bc44
Signed by: tdpeuter
GPG key ID: 38297DE43F75FFE2
15 changed files with 93 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -27,27 +27,27 @@ 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.
// Since we are only interested in substitutions in the goal (as opposed to the head of this clause),
// we can use variable renaming and filter out the substitutions that are not in the goal.
val (end, renamed: Substitutions) = numbervars(head, Program.variableRenamingStart, subs)
val preHead = applySubstitution(head, subs)
val preGoal = applySubstitution(goal, subs)
val reverse = renamed.entries.associate { (a, b) -> b to a }
Program.variableRenamingStart = end
val (headEnd, headRenaming) = numbervars(preHead, Program.variableRenamingStart, subs)
val headReverse = headRenaming.entries.associate { (a, b) -> b to a }
Program.variableRenamingStart = headEnd
var newSubs: Substitutions = subs + renamed
unifyLazy(applySubstitution(goal, subs), head, newSubs).forEach { headAnswer ->
val renamedHead = applySubstitution(head, headRenaming)
unifyLazy(preGoal, renamedHead, subs).forEach { headAnswer ->
headAnswer.map { headSubs ->
// If the body can be proven, yield the (combined) substitutions
newSubs = subs + renamed + headSubs
body.satisfy(newSubs).forEach { bodyAnswer ->
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, reverse)}
.mapValues { applySubstitution(it.value, reverse) }
.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 renamed.keys && !occurs(it.key as Variable, goal, emptyMap())}
.filterNot { it.key in headRenaming.keys && !occurs(it.key as Variable, goal, emptyMap())}
yield(Result.success(result))
},
onFailure = { error ->