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

Functor

Browse source
This commit is contained in:
Tibo De Peuter 2025-05-07 20:22:14 +02:00
parent dff53b4e68
commit 65c4d925d3
Signed by: tdpeuter
GPG key ID: 38297DE43F75FFE2
15 changed files with 270 additions and 83 deletions
Download patch file Download diff file Expand all files Collapse all files

58
src/interpreter/Preprocessor.kt
View file

@ -67,51 +67,51 @@ open class Preprocessor {
when {
// TODO Remove hardcoding by storing the functors as constants in operators?
term.functor == ":-/2" -> Rule( args[0] as Head, args[1] as Body )
term.functor == FunctorInfo.of(":-/2") -> Rule( args[0] as Head, args[1] as Body )
// Logic
term.functor == "=/2" -> Unify(args[0], args[1])
term.functor == "\\=/2" -> NotUnify(args[0], args[1])
term.functor == ",/2" -> Conjunction(args[0] as LogicOperand, args[1] as LogicOperand)
term.functor == ";/2" -> Disjunction(args[0] as LogicOperand, args[1] as LogicOperand)
term.functor == "\\+/1" -> Not(args[0] as Goal)
term.functor == "\\==/2" -> NotEquivalent(args[0], args[1])
term.functor == "==/2" -> Equivalent(args[0], args[1])
term.functor == FunctorInfo.of("=/2") -> Unify(args[0], args[1])
term.functor == FunctorInfo.of("\\=/2") -> NotUnify(args[0], args[1])
term.functor == FunctorInfo.of(",/2") -> Conjunction(args[0] as LogicOperand, args[1] as LogicOperand)
term.functor == FunctorInfo.of(";/2") -> Disjunction(args[0] as LogicOperand, args[1] as LogicOperand)
term.functor == FunctorInfo.of("\\+/1") -> Not(args[0] as Goal)
term.functor == FunctorInfo.of("\\==/2") -> NotEquivalent(args[0], args[1])
term.functor == FunctorInfo.of("==/2") -> Equivalent(args[0], args[1])
term.functor == "=\\=/2" && args.all { it is Expression } -> EvaluatesToDifferent(args[0] as Expression, args[1] as Expression)
term.functor == "=:=/2" && args.all { it is Expression } -> EvaluatesTo(args[0] as Expression, args[1] as Expression)
term.functor == "is/2" && args.all { it is Expression } -> Is(args[0] as Expression, args[1] as Expression)
term.functor == FunctorInfo.of("=\\=/2") && args.all { it is Expression } -> EvaluatesToDifferent(args[0] as Expression, args[1] as Expression)
term.functor == FunctorInfo.of("=:=/2") && args.all { it is Expression } -> EvaluatesTo(args[0] as Expression, args[1] as Expression)
term.functor == FunctorInfo.of("is/2") && args.all { it is Expression } -> Is(args[0] as Expression, args[1] as Expression)
// Arithmetic
term.functor == "-/1" && args.all { it is Expression } -> Negate(args[0] as Expression)
term.functor == "-/2" && args.all { it is Expression } -> Subtract(args[0] as Expression, args[1] as Expression)
term.functor == "+/1" && args.all { it is Expression } -> Positive(args[0] as Expression)
term.functor == "+/2" && args.all { it is Expression } -> Add(args[0] as Expression, args[1] as Expression)
term.functor == "*/2" && args.all { it is Expression } -> Multiply(args[0] as Expression, args[1] as Expression)
term.functor == "//2" && args.all { it is Expression } -> Divide(args[0] as Expression, args[1] as Expression)
term.functor == "between/3" && args.all { it is Expression } -> Between(args[0] as Expression, args[1] as Expression, args[2] as Expression)
term.functor == "succ/2" && args.all { it is Expression } -> Successor(args[0] as Expression, args[1] as Expression)
term.functor == FunctorInfo.of("-/1") && args.all { it is Expression } -> Negate(args[0] as Expression)
term.functor == FunctorInfo.of("-/2") && args.all { it is Expression } -> Subtract(args[0] as Expression, args[1] as Expression)
term.functor == FunctorInfo.of("+/1") && args.all { it is Expression } -> Positive(args[0] as Expression)
term.functor == FunctorInfo.of("+/2") && args.all { it is Expression } -> Add(args[0] as Expression, args[1] as Expression)
term.functor == FunctorInfo.of("*/2") && args.all { it is Expression } -> Multiply(args[0] as Expression, args[1] as Expression)
term.functor == FunctorInfo.of("//2") && args.all { it is Expression } -> Divide(args[0] as Expression, args[1] as Expression)
term.functor == FunctorInfo.of("between/3") && args.all { it is Expression } -> Between(args[0] as Expression, args[1] as Expression, args[2] as Expression)
term.functor == FunctorInfo.of("succ/2") && args.all { it is Expression } -> Successor(args[0] as Expression, args[1] as Expression)
// Database
term.functor == "dynamic/1" -> Dynamic((args[0] as Atom).name)
term.functor == "retract/1" -> Retract(args[0])
term.functor == "retractall/1" -> RetractAll(args[0])
term.functor == "assert/1" -> {
term.functor == FunctorInfo.of("dynamic/1") -> Dynamic(FunctorInfo.of((args[0] as Atom).name))
term.functor == FunctorInfo.of("retract/1") -> Retract(args[0])
term.functor == FunctorInfo.of("retractall/1") -> RetractAll(args[0])
term.functor == FunctorInfo.of("assert/1") -> {
if (args[0] is Rule) {
Assert(args[0] as Rule)
} else {
Assert(Fact(args[0] as Head))
}
}
term.functor == "asserta/1" -> {
term.functor == FunctorInfo.of("asserta/1") -> {
if (args[0] is Rule) {
AssertA(args[0] as Rule)
} else {
AssertA(Fact(args[0] as Head))
}
}
term.functor == "assertz/1" -> {
term.functor == FunctorInfo.of("assertz/1") -> {
if (args[0] is Rule) {
AssertZ(args[0] as Rule)
} else {
@ -120,10 +120,10 @@ open class Preprocessor {
}
// Other
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)
term.functor == FunctorInfo.of("write/1") -> Write(args[0])
term.functor == FunctorInfo.of("read/1") -> Read(args[0])
term.functor == FunctorInfo.of("initialization/1") -> Initialization(args[0] as Goal)
term.functor == FunctorInfo.of("forall/2") -> ForAll(args[0] as LogicOperand, args[1] as Goal)
else -> {
term.arguments = args

10
src/prolog/ast/Database.kt
View file

@ -6,14 +6,14 @@ import prolog.Substitutions
import prolog.ast.logic.Clause
import prolog.ast.logic.Predicate
import prolog.ast.logic.Resolvent
import prolog.ast.terms.Functor
import prolog.ast.terms.FunctorInfo
import prolog.ast.terms.Goal
/**
* Prolog Program or Database
*/
open class Database(val sourceFile: String) {
var predicates: Map<Functor, Predicate> = emptyMap()
var predicates: Map<FunctorInfo, Predicate> = emptyMap()
/**
* Initializes the database by running the initialization clauses of that database.
@ -23,14 +23,14 @@ open class Database(val sourceFile: String) {
if (sourceFile !== "") {
Logger.debug("Moving clauses from $sourceFile to main database")
predicates.filter { it.key != "/_" }
predicates.filter { it.key != FunctorInfo.of("/_") }
.forEach { (_, predicate) -> db.load(predicate, force = true) }
}
Logger.info("Initializing database from $sourceFile")
if (predicates.contains("/_")) {
if (predicates.contains(FunctorInfo.of("/_"))) {
Logger.debug("Loading clauses from /_ predicate")
predicates["/_"]?.clauses?.forEach {
predicates[FunctorInfo.of("/_")]?.clauses?.forEach {
Logger.debug("Loading clause $it")
val goal = it.body as Goal
goal.satisfy(emptyMap()).toList()

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

@ -1,8 +1,8 @@
package prolog.ast.logic
import prolog.Answers
import prolog.ast.Database.Program
import prolog.Substitutions
import prolog.ast.Database.Program
import prolog.ast.terms.*
import prolog.builtins.True
import prolog.flags.AppliedCut
@ -20,7 +20,7 @@ import prolog.logic.unifyLazy
* @see [Predicate]
*/
abstract class Clause(var head: Head, var body: Body) : Term, Resolvent {
val functor: Functor = head.functor
val functor: FunctorInfo = head.functor
override fun solve(goal: Goal, subs: Substitutions): Answers = sequence {
// If the clause is a rule, unify the goal with the head and then try to prove the body.
@ -45,7 +45,14 @@ abstract class Clause(var head: Head, var body: Body) : Term, Resolvent {
onSuccess = { bodySubs ->
// If the body can be proven, yield the (combined) substitutions
val goalToHeadResult = goalToHeadSubs.mapValues { applySubstitution(it.value, bodySubs) }
val headResult = headToGoalSubs.filterKeys { key -> goalToHeadSubs.any { occurs(key as Variable, it.value) } }
val headResult = headToGoalSubs.filterKeys { key ->
goalToHeadSubs.any {
occurs(
key as Variable,
it.value
)
}
}
yield(Result.success(goalToHeadResult + headResult))
},
onFailure = { error ->

8
src/prolog/ast/logic/Predicate.kt
View file

@ -2,25 +2,25 @@ package prolog.ast.logic
import prolog.Answers
import prolog.Substitutions
import prolog.ast.terms.Functor
import prolog.ast.terms.FunctorInfo
import prolog.ast.terms.Goal
import prolog.flags.AppliedCut
/**
* Collection of [Clause]s with the same [Functor].
* Collection of [Clause]s with the same [FunctorInfo].
*
* If a goal is proved, the system looks for a predicate with the same functor, then uses indexing
* to select candidate clauses and then tries these clauses one-by-one.
*/
class Predicate : Resolvent {
val functor: Functor
val functor: FunctorInfo
val clauses: MutableList<Clause>
var dynamic = false
/**
* Creates a predicate with the given functor and an empty list of clauses.
*/
constructor(functor: Functor, dynamic: Boolean = false) {
constructor(functor: FunctorInfo, dynamic: Boolean = false) {
this.functor = functor
this.clauses = mutableListOf()
this.dynamic = dynamic

3
src/prolog/ast/terms/Atom.kt
View file

@ -4,9 +4,10 @@ import prolog.Answers
import prolog.Substitutions
import prolog.ast.logic.Resolvent
import prolog.logic.unifyLazy
import prolog.ast.arithmetic.Integer
open class Atom(val name: String) : Goal(), Head, Body, Resolvent {
override val functor: Functor = "$name/_"
override val functor: FunctorInfo = FunctorInfo(this, Integer(0))
override fun solve(goal: Goal, subs: Substitutions): Answers = unifyLazy(goal, this, subs)

29
src/prolog/ast/terms/FunctorInfo.kt Normal file
View file

@ -0,0 +1,29 @@
package prolog.ast.terms
import prolog.Substitutions
import prolog.ast.arithmetic.Integer
data class FunctorInfo(val name: Atom, val arity: Integer) : Term {
companion object {
fun of(functor: String): FunctorInfo {
// Split the functor string into name and arity, by splitting the last "/"
val lastSlash = functor.lastIndexOf('/')
val name = Atom(functor.substring(0, lastSlash))
val arity = Integer(functor.substring(lastSlash + 1).toIntOrNull() ?: 0)
return FunctorInfo(name, arity)
}
}
override fun toString(): String = "${name.name}/$arity"
override fun applySubstitution(subs: Substitutions) : FunctorInfo = this
override fun equals(other: Any?): Boolean {
if (this === other) return true
if (other == null) return false
if (other !is FunctorInfo && other !is String) return false
if (other is FunctorInfo) {
return this.name.toString() == other.name.toString() && this.arity == other.arity
}
return this.toString() == other
}
}

4
src/prolog/ast/terms/Goal.kt
View file

@ -1,8 +1,8 @@
package prolog.ast.terms
import prolog.Answers
import prolog.ast.Database.Program
import prolog.Substitutions
import prolog.ast.Database.Program
import prolog.ast.logic.LogicOperand
/**
@ -13,7 +13,7 @@ import prolog.ast.logic.LogicOperand
* or it fails if Prolog fails to prove it.
*/
abstract class Goal : LogicOperand(), Term {
abstract val functor: Functor
abstract val functor: FunctorInfo
override fun satisfy(subs: Substitutions): Answers = Program.solve(this, subs)
}

4
src/prolog/ast/terms/Head.kt
View file

@ -4,7 +4,5 @@ package prolog.ast.terms
* Part of a [Clause][prolog.ast.logic.Clause] before the neck operator.
*/
interface Head : Term {
val functor: Functor
val functor: FunctorInfo
}
typealias Functor = String

3
src/prolog/ast/terms/Structure.kt
View file

@ -5,13 +5,14 @@ import prolog.Substitutions
import prolog.ast.logic.Resolvent
import prolog.logic.applySubstitution
import prolog.logic.unifyLazy
import prolog.ast.arithmetic.Integer
typealias Argument = Term
typealias CompoundTerm = Structure
open class Structure(val name: Atom, var arguments: List<Argument>) : Goal(), Head, Body, Resolvent {
override val functor: Functor = "${name.name}/${arguments.size}"
override val functor: FunctorInfo = FunctorInfo(name, Integer(arguments.size))
override fun solve(goal: Goal, subs: Substitutions): Answers {
return unifyLazy(goal, this, subs)

65
src/prolog/builtins/analysingAndConstructionOperators.kt Normal file
View file

@ -0,0 +1,65 @@
package prolog.builtins
import prolog.Answers
import prolog.Substitutions
import prolog.ast.arithmetic.Integer
import prolog.ast.terms.AnonymousVariable
import prolog.ast.terms.Atom
import prolog.ast.terms.Head
import prolog.ast.terms.Structure
import prolog.ast.terms.Term
import prolog.ast.terms.Variable
import prolog.logic.applySubstitution
import prolog.logic.atomic
import prolog.logic.nonvariable
import prolog.logic.unifyLazy
import prolog.logic.variable
class Functor(private val term: Term, private val functorName: Term, private val functorArity: Term) :
Structure(Atom("functor"), listOf(term, functorName, functorArity)) {
override fun satisfy(subs: Substitutions): Answers {
if (nonvariable(term, subs)) {
val t = applySubstitution(term, subs) as Head
return Conjunction(
Unify(t.functor.arity, functorArity),
Unify(t.functor.name, functorName)
).satisfy(subs)
}
if (variable(term, subs)) {
require(atomic(functorName, subs) && atomic(functorArity, subs)) {
"Arguments are not sufficiently instantiated"
}
val name = applySubstitution(functorName, subs) as Atom
val arity = applySubstitution(functorArity, subs) as Integer
val result = if (arity.value == 0) {
functorName
} else {
val argList = mutableListOf<Term>()
for (i in 1..arity.value) {
argList.add(AnonymousVariable.create())
}
Structure(name, argList)
}
if (nonvariable(term, subs)) {
return unifyLazy(term, result, subs)
}
return sequenceOf(Result.success(mapOf(term to result)))
}
throw IllegalStateException()
}
override fun applySubstitution(subs: Substitutions): Functor = Functor(
term.applySubstitution(subs),
functorName.applySubstitution(subs),
functorArity.applySubstitution(subs)
)
override fun toString(): String = "functor($term, $functorName, $functorArity)"
}

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

@ -3,26 +3,21 @@ package prolog.builtins
import io.Logger
import prolog.Answers
import prolog.Substitutions
import prolog.ast.logic.Clause
import prolog.ast.terms.Atom
import prolog.ast.terms.Structure
import prolog.ast.logic.Predicate
import prolog.ast.Database.Program
import prolog.ast.terms.Functor
import prolog.ast.terms.Term
import prolog.ast.logic.Fact
import prolog.ast.Database
import prolog.ast.terms.Body
import prolog.ast.terms.Goal
import prolog.ast.terms.Operator
import prolog.ast.Database.Program
import prolog.ast.arithmetic.Integer
import prolog.ast.logic.Clause
import prolog.ast.logic.Fact
import prolog.ast.logic.Predicate
import prolog.ast.terms.*
import prolog.logic.applySubstitution
import prolog.logic.unifyLazy
/**
* (Make) the [Predicate] with the corresponding [Functor] dynamic.
* (Make) the [Predicate] with the corresponding [FunctorInfo] dynamic.
*/
class Dynamic(private val dynamicFunctor: Functor): Goal(), Body {
override val functor: Functor = "dynamic/1"
class Dynamic(private val dynamicFunctor: FunctorInfo) : Goal(), Body {
override val functor = FunctorInfo(Atom("dynamic"), Integer(1))
override fun satisfy(subs: Substitutions): Answers {
val predicate = Program.db.predicates[dynamicFunctor]
@ -48,7 +43,7 @@ class Dynamic(private val dynamicFunctor: Functor): Goal(), Body {
}
class Assert(clause: Clause) : AssertZ(clause) {
override val functor: Functor = "assert/1"
override val functor = FunctorInfo(Atom("assert"), Integer(1))
}
/**