Added loose operators
This commit is contained in:
parent
717e5e0954
commit
a9bb6e0338
6 changed files with 95 additions and 47 deletions
|
@ -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 -> {
|
||||
|
|
|
@ -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 "/"
|
||||
|
|
|
@ -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))
|
||||
}
|
||||
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
57
src/prolog/builtins/verificationOperators.kt
Normal file
57
src/prolog/builtins/verificationOperators.kt
Normal file
|
@ -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))
|
||||
}
|
|
@ -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.
|
||||
|
|
|
@ -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)
|
||||
}
|
||||
}
|
Reference in a new issue