01: package ca.draisey.free.tprolog; 02: 03: 04: 05: 06: 07: // recursive term elements give predicates, formal functions, formal constants and formal variables 08: // pair, atom and variable terms are sufficient to generate tham all 09: // the binding of variable terms is sufficient to create constraint space of predicate logic 10: // unification is just a recursive descent of matching terms 11: // -- following bound variables to satisfy given constraints 12: // -- binding unbound variables as necessary to generate new contraints 13: // -- failing at mismatched terms 14: // -- succeeding otherwise with newfound constraints added to environment 15: // this unification algorithm can create circular references -- equivalent to circular reasoning 16: // in logic -- so called occurance loops -- such is prolog -- these circular references 17: // never occur in normal prolog programming 18: abstract class Term extends Clause { 19: // part of the instantiation process for stripping unwanted qualifiers 20: final Term dequantifyTerm() { return this; } 21: 22: // glue between clauses and terms 23: final void queryClause( final Term goal, final Variables these, final Variables goals, final Successor success ) 24: { 25: unifythrough( goal, these, goals, success ); 26: } 27: 28: // unifythrough -- by juggling terms unifythrough does dynamic dispatch on its Term argument -- 29: // Java can only dispatch dynamically on "this" -- we do so through "unifythrough" 30: // and on a per class basis swap "this" and "that" and then dispatch to the 31: // specialized "unifytoPair", "unifytoAtom", and "unifytoUnboundVariable" -- note 32: // that for bound variables the corresponding bound term is substituted immediately 33: protected abstract void unifythrough( final Term that, final Variables these, final Variables those, final Successor success ); 34: 35: // the meat of any Term 36: // unifytoPair and unifytoAtom fail by default -- overriden as necessary -- 37: protected void unifytoPair( final PairTerm that, final Variables these, final Variables those, final Successor success ) {}; 38: protected void unifytoCons( final ConsTerm that, final Variables these, final Variables those, final Successor success ) {}; 39: protected void unifytoAtom( final AtomTerm that, final Variables these, final Variables those, final Successor success ) {}; 40: // all terms inherit the ability to bind an unbound variable from Term -- always succeeds -- 41: protected void unifytoUnboundVariable( final VariTerm that, final Variables these, final Variables those, final Successor success ) 42: { 43: that.bindto( this, those, these, success ); 44: } 45: } 46: 47: // fin