From a9bb6e0338d802df389c8f6e53976ac6f1c95bce Mon Sep 17 00:00:00 2001 From: Tibo De Peuter Date: Fri, 9 May 2025 16:50:20 +0200 Subject: [PATCH] Added loose operators --- src/interpreter/Preprocessor.kt | 10 +++- src/prolog/ast/terms/Functor.kt | 2 + src/prolog/builtins/analysisOperators.kt | 47 ++++++++------- src/prolog/builtins/verificationOperators.kt | 57 +++++++++++++++++++ src/prolog/logic/terms.kt | 19 ------- .../logic/TermAnalysisConstructionTest.kt | 7 ++- 6 files changed, 95 insertions(+), 47 deletions(-) create mode 100644 src/prolog/builtins/verificationOperators.kt diff --git a/src/interpreter/Preprocessor.kt b/src/interpreter/Preprocessor.kt index 7076dc8..5f9a8ae 100644 --- a/src/interpreter/Preprocessor.kt +++ b/src/interpreter/Preprocessor.kt @@ -64,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) @@ -172,6 +172,12 @@ 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/terms/Functor.kt b/src/prolog/ast/terms/Functor.kt index 98d764f..b7a4cc3 100644 --- a/src/prolog/ast/terms/Functor.kt +++ b/src/prolog/ast/terms/Functor.kt @@ -4,6 +4,8 @@ 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/builtins/analysisOperators.kt b/src/prolog/builtins/analysisOperators.kt index f905696..1de5b4c 100644 --- a/src/prolog/builtins/analysisOperators.kt +++ b/src/prolog/builtins/analysisOperators.kt @@ -1,5 +1,6 @@ package prolog.builtins +import com.sun.tools.javac.resources.CompilerProperties.Fragments.Anonymous import prolog.Answers import prolog.Substitutions import prolog.ast.Database.Program @@ -16,6 +17,8 @@ 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(Atom("functor"), listOf(term, functorName, functorArity)) { @@ -154,30 +157,6 @@ class ClauseOp(private val head: Head, private val body: Body) : ) } -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 { @@ -246,3 +225,23 @@ open class Univ(private val term: Term, private val list: Term) : Operator(Atom( list.applySubstitution(subs) ) } + +class NumberVars(private val term: Term, private val start: Integer, private val end: Term) : + Structure(Atom("numbervars"), listOf(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/verificationOperators.kt b/src/prolog/builtins/verificationOperators.kt new file mode 100644 index 0000000..76bf185 --- /dev/null +++ b/src/prolog/builtins/verificationOperators.kt @@ -0,0 +1,57 @@ +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 +import prolog.logic.atomic +import prolog.logic.compound +import prolog.logic.nonvariable +import prolog.logic.variable + +class Atomic(private val term: Term) : Operator(Atom("atomic"), null, 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(Atom("compound"), null, 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(Atom("nonvar"), null, 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(Atom("var"), null, 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 8c2b26f..459d58d 100644 --- a/src/prolog/logic/terms.kt +++ b/src/prolog/logic/terms.kt @@ -1,29 +1,10 @@ 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/prolog/logic/TermAnalysisConstructionTest.kt b/tests/prolog/logic/TermAnalysisConstructionTest.kt index c1033a9..47f58d0 100644 --- a/tests/prolog/logic/TermAnalysisConstructionTest.kt +++ b/tests/prolog/logic/TermAnalysisConstructionTest.kt @@ -1,10 +1,13 @@ package prolog.logic +import org.junit.jupiter.api.Assertions.assertEquals 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 +import prolog.ast.arithmetic.Integer /** * Based on [Predicates for analyzing/constructing terms](https://github.com/dtonhofer/prolog_notes/blob/master/swipl_notes/about_term_analysis_and_construction/term_analysis_construction.png) @@ -19,7 +22,7 @@ class TermAnalysisConstructionTest { assertTrue(atomic(atom)) assertFalse(compound(atom)) - assertTrue(functor(atom, Atom("foo"), 0)) + assertEquals(Functor("foo", 0), atom.functor) } @Test @@ -37,6 +40,6 @@ class TermAnalysisConstructionTest { assertFalse(atomic(structure)) assertTrue(compound(structure)) - assertTrue(functor(structure, Atom("foo"), 1)) + assertEquals(Functor("foo", 1), structure.functor) } } \ No newline at end of file