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

fix: Mib

Browse source
This commit is contained in:
Tibo De Peuter 2025-05-08 18:58:33 +02:00
parent 7daae860fc
commit 1feb3893c5
Signed by: tdpeuter
GPG key ID: 38297DE43F75FFE2
4 changed files with 45 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -48,16 +48,17 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent {
onSuccess = { bodySubs ->
// If the body can be proven, yield the (combined) substitutions
val goalResult = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) }
yield(Result.success(goalResult + headResult))
val bodyResult = bodySubs.filterKeys { occurs(it as Variable, simplifiedGoal) }
yield(Result.success(goalResult + headResult + bodyResult))
},
onFailure = { error ->
if (error is AppliedCut) {
// Find single solution and return immediately
if (error.subs != null) {
val goalResult = goalToHeadSubs.mapValues {
applySubstitution(it.value, error.subs)
}
yield(Result.failure(AppliedCut(goalResult + headResult)))
val bodySubs = error.subs
val goalResult = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) }
val bodyResult = bodySubs.filterKeys { occurs(it as Variable, simplifiedGoal) }
yield(Result.failure(AppliedCut(goalResult + headResult + bodyResult)))
} else {
yield(Result.failure(AppliedCut()))
}

3
src/prolog/builtins/analysisOperators.kt
View file

@ -35,10 +35,11 @@ class FunctorOp(private val term: Term, private val functorName: Term, private v
"Arguments are not sufficiently instantiated"
}
val t = applySubstitution(term, subs)
val name = applySubstitution(functorName, subs) as Atom
val arity = applySubstitution(functorArity, subs) as Integer
val result = Structure(name, List(arity.value) { AnonymousVariable.create() })
sequenceOf(Result.success(mapOf(term to result)))
sequenceOf(Result.success(mapOf(t to result)))
}
else -> throw IllegalStateException()

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

@ -2,14 +2,15 @@ package prolog.builtins
import prolog.Answers
import prolog.Substitutions
import prolog.ast.Database.Program
import prolog.ast.logic.LogicOperand
import prolog.ast.logic.LogicOperator
import prolog.ast.terms.Atom
import prolog.ast.terms.Body
import prolog.ast.terms.Goal
import prolog.ast.terms.Structure
import prolog.flags.AppliedCut
import prolog.logic.applySubstitution
import prolog.logic.numbervars
/**
* Always fail.
@ -53,8 +54,8 @@ class Conjunction(val left: LogicOperand, private val right: LogicOperand) :
left.fold(
// If it succeeds, satisfy the right part with the updated substitutions and return all results
onSuccess = { leftSubs ->
right.satisfy(subs + leftSubs).forEach {
it.fold(
right.satisfy(subs + leftSubs).forEach { right ->
right.fold(
// If the right part succeeds, yield the result with the left substitutions
onSuccess = { rightSubs ->
yield(Result.success(leftSubs + rightSubs))

51
src/prolog/logic/unification.kt
View file

@ -12,10 +12,7 @@ import prolog.ast.lists.List.Cons
import prolog.ast.lists.List.Empty
import prolog.ast.logic.Fact
import prolog.ast.logic.LogicOperator
import prolog.ast.terms.Atom
import prolog.ast.terms.Structure
import prolog.ast.terms.Term
import prolog.ast.terms.Variable
import prolog.ast.terms.*
// Apply substitutions to a term
fun applySubstitution(term: Term, subs: Substitutions): Term = when {
@ -62,7 +59,10 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence
val t2 = applySubstitution(term2, subs)
when {
equivalent(t1, t2, subs) -> yield(Result.success(emptyMap()))
equivalent(t1, t2, subs) -> {
yield(Result.success(emptyMap()))
}
variable(t1, subs) -> {
val variable = t1 as Variable
if (!occurs(variable, t2, subs)) {
@ -85,19 +85,7 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence
val args1 = structure1.arguments
val args2 = structure2.arguments
if (args1.size == args2.size) {
// Keep track of the substitutions so far
val results = args1.zip(args2).map { (arg1, arg2) ->
unifyLazy(arg1, arg2, subs)
}
// Combine the results of all unifications
val combinedResults = results.reduce { acc, result ->
acc.flatMap { a ->
result.map { b ->
if (a.isSuccess && b.isSuccess) a.getOrThrow() + b.getOrThrow() else emptyMap()
}
}.map { Result.success(it) }
}
yieldAll(combinedResults)
yieldAll(unifyArgs(args1, args2, subs))
}
}
}
@ -131,6 +119,32 @@ fun unifyLazy(term1: Term, term2: Term, subs: Substitutions): Answers = sequence
}
}
private fun unifyArgs(
args1: kotlin.collections.List<Argument>,
args2: kotlin.collections.List<Argument>,
subs: Substitutions
): Answers = sequence {
// Using the current subs, unify the first argument of each list
val arg1 = applySubstitution(args1[0], subs)
val arg2 = applySubstitution(args2[0], subs)
unifyLazy(arg1, arg2, subs).forEach { headResult ->
// Use the resulting substitutions to unify the rest of the arguments
headResult.map { headSubs ->
val rest1 = args1.drop(1).map { applySubstitution(it, headSubs) }
val rest2 = args2.drop(1).map { applySubstitution(it, headSubs) }
if (rest1.isEmpty() && rest2.isEmpty()) {
yield(Result.success(headSubs))
} else if (rest1.isNotEmpty() && rest2.isNotEmpty()) {
unifyArgs(rest1, rest2, subs).forEach { tailResult ->
tailResult.map { tailSubs ->
yield(Result.success(headSubs + tailSubs))
}
}
}
}
}
}
fun unify(term1: Term, term2: Term): Answer {
val substitutions = unifyLazy(term1, term2, emptyMap()).iterator()
return if (substitutions.hasNext()) {
@ -151,6 +165,7 @@ fun equivalent(term1: Term, term2: Term, subs: Substitutions): Boolean {
equivalent(arg1, arg2, subs)
}
}
term1 is Integer && term2 is Integer -> compare(term1, term2, subs) == 0
term1 is Number && term2 is Number -> compare(term1, term2, subs) == 0
term1 is Variable && term2 is Variable -> term1 == term2