tarau.jinni
Class Clause

java.lang.Object
  |
  +--tarau.jinni.Term
        |
        +--tarau.jinni.Nonvar
              |
              +--tarau.jinni.Const
                    |
                    +--tarau.jinni.Fun
                          |
                          +--tarau.jinni.Clause

public class Clause

extends Fun

Datatype for a Prolog clause (H:-B) having a head H and a body b

Field Summary

int	begins_at
(package private) HashDict	dict Variable dictionary
int	ends_at
java.lang.String	fname File name and line where sources start and end (if applicable)
(package private) boolean	ground Remembers if a clause is ground.

Fields inherited from class tarau.jinni.Fun

args

Fields inherited from class tarau.jinni.Const

aFail, anEof, aNil, aNo, aTrue, aYes, sym

Fields inherited from class tarau.jinni.Term

CONST, INT, JAVA, REAL, VAR

Constructor Summary

Clause(java.lang.String s)
Constructs a clause by parsing its string representation.

Clause(Term head, Term body)
Builds a clause given ith head and its body

Method Summary

(package private) static Term	appendConj(Term x, Term y) Concatenates 2 Conjunctions
(package private) Clause	ccopy() Creates a copy of the clause with variables standardized apart, i.e.
(package private) void	checkIfGround() Detects that a clause is ground (i.e.
private java.lang.String	Clause2String(Clause c) Prints out a clause as Head:-Body
static Clause	clauseFromString(java.lang.String s) Extracts a clause from its String representation.
Clause	cnumbervars(boolean replaceAnonymous) Replaces varibles with nice looking upper case constants for printing purposes
Term	getBody() Extracts the body of a clause
(package private) Term	getFirst() Gets the leftmost (first) goal in the body of a clause, i.e.
Term	getHead() Extracts the head of a clause (a Term).
java.lang.String	getKey() Returns a key based on the principal functor of the head of the clause and its arity.
(package private) Term	getRest() Gets all but the leftmost goal in the body of a clause, i.e.
static Clause	goalFromString(java.lang.String line)
(package private) boolean	isClause()
java.lang.String	pprint() Pretty prints a clause after replacing ugly variable names
java.lang.String	pprint(boolean replaceAnonymous) Pretty prints a clause after replacing ugly variable names
(package private) boolean	provenGround() Checks if a Clause has been proven ground after beeing read in or created.
void	setFile(java.lang.String fname, int begins_at, int ends_at)
Clause	toClause() Clause to Term converter: the joy of strong typing:-)
Clause	toGoal() Reads a goal as a clause containing a dummy header with all veriables in it
Term	toTerm() Converts a clause to a term.
(package private) Clause	unfold_with_goal(Clause goal, Trail trail)
(package private) Clause	unfold(Clause that, Trail trail) Algebraic composition operation of 2 Clauses, doing the basic resolution step Jinni is based on.
(package private) Clause	unfoldedCopy(Clause that, Trail trail)

Methods inherited from class tarau.jinni.Fun

bind_to, funClone, funToString, getArg, getArity, getIntArg, init, initializedClone, listify, putArg, reaction, setArg, show_args, toBuiltin, token, toString, unify_to, unInitializedClone, watchNull

Methods inherited from class tarau.jinni.Const

eq, name, qname, the, toUnquoted

Methods inherited from class tarau.jinni.Term

action, charsToString, copy, exec, exec, fromString, isBuiltin, matches, matching_copy, numbervars, ref, stringToChars, toChars, toObject, undo, unify, varsOf

Methods inherited from class java.lang.Object

, clone, equals, finalize, getClass, hashCode, notify, notifyAll, registerNatives, wait, wait, wait

Field Detail

dict

HashDict dict

Variable dictionary

ground

boolean ground

Remembers if a clause is ground.

fname

public java.lang.String fname

File name and line where sources start and end (if applicable)

begins_at

public int begins_at

ends_at

public int ends_at

Constructor Detail

Clause

public Clause(Term head,
              Term body)

Builds a clause given ith head and its body

Clause

public Clause(java.lang.String s)

Constructs a clause by parsing its string representation. Note the building of a dictionary of variables, allowing listing of the clause with its original variable names.

Method Detail

clauseFromString

public static Clause clauseFromString(java.lang.String s)

Extracts a clause from its String representation.

toGoal

public Clause toGoal()

Reads a goal as a clause containing a dummy header with all veriables in it

goalFromString

public static Clause goalFromString(java.lang.String line)

checkIfGround

final void checkIfGround()

Detects that a clause is ground (i.e. has no variables)

setFile

public void setFile(java.lang.String fname,
                    int begins_at,
                    int ends_at)

provenGround

final boolean provenGround()

Checks if a Clause has been proven ground after beeing read in or created.

Clause2String

private java.lang.String Clause2String(Clause c)

Prints out a clause as Head:-Body

pprint

public java.lang.String pprint()

Pretty prints a clause after replacing ugly variable names

Overrides:

pprint in class Term

pprint

public java.lang.String pprint(boolean replaceAnonymous)

Pretty prints a clause after replacing ugly variable names

Overrides:

pprint in class Term

toClause

public Clause toClause()

Clause to Term converter: the joy of strong typing:-)

Overrides:

toClause in class Term

cnumbervars

public Clause cnumbervars(boolean replaceAnonymous)

Replaces varibles with nice looking upper case constants for printing purposes

toTerm

public Term toTerm()

Converts a clause to a term. Note that Head:-true will convert to the term Head.

Overrides:

toTerm in class Term

ccopy

final Clause ccopy()

Creates a copy of the clause with variables standardized apart, i.e. something like f(s(X),Y,X) becomes f(s(X1),Y1,X1)) with X1,Y1 variables garantted not to occurring in the the current resolvant.

getHead

public final Term getHead()

Extracts the head of a clause (a Term).

getBody

public final Term getBody()

Extracts the body of a clause

getFirst

final Term getFirst()

Gets the leftmost (first) goal in the body of a clause, i.e. from H:-B1,B2,...,Bn it will extract B1.

getRest

final Term getRest()

Gets all but the leftmost goal in the body of a clause, i.e. from H:-B1,B2,...,Bn it will extract B2,...,Bn. Note that the returned Term is either Conj or True, the last one meaning an empty body.

See Also:

True, Conj

appendConj

static final Term appendConj(Term x,
                             Term y)

Concatenates 2 Conjunctions

See Also:

unfold(tarau.jinni.Clause, tarau.jinni.Trail)

unfold

Clause unfold(Clause that,
              Trail trail)

Algebraic composition operation of 2 Clauses, doing the basic resolution step Jinni is based on. From A0:-A1,A2...An and B0:-B1...Bm it builds (A0:-B1,..Bm,A2,...An) mgu(A1,B0). Note that it returns null if A1 and B0 do not unify.

See Also:

Term#unify()

unfold_with_goal

final Clause unfold_with_goal(Clause goal,
                              Trail trail)

unfoldedCopy

Clause unfoldedCopy(Clause that,
                    Trail trail)

getKey

public java.lang.String getKey()

Returns a key based on the principal functor of the head of the clause and its arity.

Overrides:

getKey in class Const

isClause

final boolean isClause()

Overrides:

isClause in class Fun