LogicProgrammingScopeWithTheories

Adds theory/clause-database-building sugar to LogicProgrammingScopeWithUnificator: implements TheoryFactory itself (forwarding to theoryFactory, e.g. via TheoryFactory by theoryFactory as LogicProgrammingScopeImpl does) so a it.unibo.tuprolog.theory.Theory/MutableTheory can be built directly from this scope, and adds theory/mutableTheory overloads accepting one DSL lambda per clause (rather than an already-built Clause) plus theoryOf/mutableTheoryOf overloads that concatenate several Iterable/Sequences of clauses into one:

logicProgramming {
val db =
theory(
{ factOf(structOf("parent", atomOf("tom"), atomOf("bob"))) },
{ ruleOf(structOf("grandparent", varOf("X"), varOf("Z")), structOf("parent", varOf("X"), varOf("Z"))) },
)
}

Each S.() -> Any lambda passed to theory/mutableTheory runs against a fresh newScope (exactly like it.unibo.tuprolog.dsl.MinimalLogicProgrammingScope.fact/it.unibo.tuprolog.dsl.MinimalLogicProgrammingScope.rule do), so variables of the same name in two different lambdas denote distinct, unrelated it.unibo.tuprolog.core.Vars — as they would be in two separate clauses of a real Prolog theory.

Type Parameters

S

the concrete, self-referential scope type (see it.unibo.tuprolog.dsl.BaseLogicProgrammingScope).

Inheritors

Properties

Link copied to clipboard
open val _: Var
Link copied to clipboard
abstract val context: Substitution
Link copied to clipboard
abstract val emptyBlock: EmptyBlock
Link copied to clipboard
Link copied to clipboard
abstract val fail: Truth
Link copied to clipboard
Link copied to clipboard

The TheoryFactory this scope's TheoryFactory implementation (and theory/mutableTheory) forward to.

Link copied to clipboard
abstract val unificator: Unificator
Link copied to clipboard
abstract val variables: Map<String, Var>

Functions

Link copied to clipboard
abstract fun anonymous(): Var
Link copied to clipboard
abstract fun atomOf(value: Char): Atom
abstract fun atomOf(value: String): Atom
Link copied to clipboard
abstract fun blockOf(terms: Iterable<Term>): Block
abstract fun blockOf(terms: Sequence<Term>): Block
abstract fun blockOf(vararg terms: Term): Block
Link copied to clipboard
abstract fun clauseOf(head: Struct?, vararg body: Term): Clause
Link copied to clipboard
abstract fun consOf(head: Term, tail: Term): Cons
Link copied to clipboard
abstract operator fun contains(variable: Var): Boolean
abstract operator fun contains(variable: String): Boolean
Link copied to clipboard
abstract fun copy(unificator: Unificator): S
Link copied to clipboard
abstract fun directiveOf(body1: Term, vararg body: Term): Directive
Link copied to clipboard
Link copied to clipboard
open fun emptyTheory(): Theory
abstract fun emptyTheory(unificator: Unificator): Theory
Link copied to clipboard
abstract fun factOf(head: Struct): Fact
Link copied to clipboard
abstract operator fun get(variable: String): Var?
Link copied to clipboard
abstract fun indicatorOf(name: Term, arity: Term): Indicator
abstract fun indicatorOf(name: String, arity: Int): Indicator
Link copied to clipboard
abstract fun intOf(value: Byte): Integer
abstract fun intOf(value: Int): Integer
abstract fun intOf(value: Long): Integer
abstract fun intOf(value: Short): Integer
abstract fun intOf(value: String): Integer
abstract fun intOf(value: BigInteger): Integer
abstract fun intOf(value: String, radix: Int): Integer
Link copied to clipboard
abstract fun logicListFrom(terms: Iterable<Term>, last: Term?): List
abstract fun logicListFrom(terms: Sequence<Term>, last: Term?): List
abstract fun logicListFrom(vararg terms: Term, last: Term?): List
Link copied to clipboard
abstract fun logicListOf(terms: Iterable<Term>): List
abstract fun logicListOf(terms: Sequence<Term>): List
abstract fun logicListOf(vararg terms: Term): List
Link copied to clipboard
open fun match(term1: Term, term2: Term): Boolean
open fun match(term1: Term, term2: Term, occurCheckEnabled: Boolean): Boolean
Link copied to clipboard
open fun merge(substitution1: Substitution, substitution2: Substitution): Substitution
abstract fun merge(substitution1: Substitution, substitution2: Substitution, occurCheckEnabled: Boolean): Substitution
Link copied to clipboard
open fun mgu(term1: Term, term2: Term): Substitution
abstract fun mgu(term1: Term, term2: Term, occurCheckEnabled: Boolean): Substitution
Link copied to clipboard
open fun mutableTheory(vararg clauseFunctions: S.() -> Any): MutableTheory

Builds a MutableTheory out of clauseFunctions, one per clause. Otherwise identical to theory, down to how each lambda is run and its result converted via toClause; delegates to TheoryFactory.mutableTheoryOf (via theoryFactory).

Link copied to clipboard
open fun mutableTheoryOf(clauses: Iterable<Clause>, vararg otherClauses: Iterable<Clause>): MutableTheory
open fun mutableTheoryOf(clauses: Sequence<Clause>, vararg otherClauses: Sequence<Clause>): MutableTheory

Overload of TheoryFactory.mutableTheoryOf concatenating clauses and otherClauses into one MutableTheory.

open fun mutableTheoryOf(vararg clauses: Clause): MutableTheory
abstract fun mutableTheoryOf(unificator: Unificator, vararg clauses: Clause): MutableTheory
abstract fun mutableTheoryOf(clauses: Iterable<Clause>, unificator: Unificator): MutableTheory
abstract fun mutableTheoryOf(clauses: Sequence<Clause>, unificator: Unificator): MutableTheory
Link copied to clipboard
abstract fun newScope(): S
Link copied to clipboard
abstract fun numOf(value: Byte): Integer
abstract fun numOf(value: Double): Real
abstract fun numOf(value: Float): Real
abstract fun numOf(value: Int): Integer
abstract fun numOf(value: Long): Integer
abstract fun numOf(value: Number): Numeric
abstract fun numOf(value: Short): Integer
abstract fun numOf(value: String): Numeric
abstract fun numOf(value: BigDecimal): Real
abstract fun numOf(value: BigInteger): Integer
Link copied to clipboard
abstract fun realOf(value: Double): Real
abstract fun realOf(value: Float): Real
abstract fun realOf(value: String): Real
abstract fun realOf(value: BigDecimal): Real
Link copied to clipboard
abstract fun ruleOf(head: Struct, body1: Term, vararg body: Term): Rule
Link copied to clipboard
abstract fun structOf(functor: String, args: Iterable<Term>): Struct
abstract fun structOf(functor: String, args: List<Term>): Struct
abstract fun structOf(functor: String, args: Sequence<Term>): Struct
abstract fun structOf(functor: String, vararg args: Term): Struct
Link copied to clipboard
abstract fun substitutionOf(assignments: Iterable<Pair<Var, Term>>): Substitution
abstract fun substitutionOf(assignments: Sequence<Pair<Var, Term>>): Substitution
abstract fun substitutionOf(vararg assignments: Pair<String, Term>): Substitution
Link copied to clipboard
open fun theory(vararg clauseFunctions: S.() -> Any): Theory

Builds a Theory out of clauseFunctions, one per clause: each lambda runs with a fresh newScope as its receiver, and its result is coerced into a Clause via toClause — so it may return an already-built Clause (from it.unibo.tuprolog.core.Scope.factOf/it.unibo.tuprolog.core.Scope.ruleOf/ it.unibo.tuprolog.core.Scope.directiveOf) or a plain it.unibo.tuprolog.core.Struct, as shown in this interface's example. Delegates to TheoryFactory.theoryOf (via theoryFactory) for the actual construction.

Link copied to clipboard
open fun theoryOf(clauses: Iterable<Clause>, vararg otherClauses: Iterable<Clause>): Theory
open fun theoryOf(clauses: Sequence<Clause>, vararg otherClauses: Sequence<Clause>): Theory

Overload of TheoryFactory.theoryOf concatenating clauses and otherClauses into a single Theory.

open fun theoryOf(clauses: Iterable<Clause>): Theory
open fun theoryOf(clauses: Sequence<Clause>): Theory
open fun theoryOf(vararg clauses: Clause): Theory
abstract fun theoryOf(unificator: Unificator, vararg clauses: Clause): Theory
abstract fun theoryOf(clauses: Iterable<Clause>, unificator: Unificator): Theory
abstract fun theoryOf(clauses: Sequence<Clause>, unificator: Unificator): Theory
Link copied to clipboard
open fun <T : Term> Any.toSpecificSubTypeOfTerm(type: KClass<T>, converter: (Struct) -> T): T
Link copied to clipboard
open fun Any.toTerm(): Term
Link copied to clipboard
abstract fun truthOf(value: Boolean): Truth
Link copied to clipboard
abstract fun tupleOf(terms: Iterable<Term>): Tuple
abstract fun tupleOf(terms: Sequence<Term>): Tuple
abstract fun tupleOf(vararg terms: Term): Tuple
Link copied to clipboard
abstract fun unifierOf(assignments: Iterable<Pair<Var, Term>>): Substitution.Unifier
abstract fun unifierOf(assignments: Sequence<Pair<Var, Term>>): Substitution.Unifier
abstract fun unifierOf(vararg assignments: Pair<String, Term>): Substitution.Unifier
Link copied to clipboard
open fun unify(term1: Term, term2: Term): Term?
open fun unify(term1: Term, term2: Term, occurCheckEnabled: Boolean): Term?
Link copied to clipboard
abstract fun varOf(name: Char): Var
abstract fun varOf(name: String): Var
Link copied to clipboard
abstract fun whatever(): Var
Link copied to clipboard
abstract fun where(lambda: Scope.() -> Unit): Scope
Link copied to clipboard
abstract fun <R> with(lambda: Scope.() -> R): R