Trivial Prolog in Java

01: package ca.draisey.free.tprolog;
02:
03:
04:
05:
06:
07: // an instantiated formal variable -- usually only occurs in an instantiated rule
08: class VariTerm extends Term {
09:         VariTerm( final int i )
10:         {
11:                 index = i;
12:         }
13:         
14:         private static java.util.Random randomGenerator = new java.util.Random();
15:
16:         // for pretty output
17:         // -- don't return the binding itself -- just what it's linked to
18:         // -- if unbound just return the address of this object
19:         void listing( final int f, final Variables these, final java.io.PrintWriter p, final Monitor m )
20:         {
21:                 //System.out.print("v");
22:                 if( these.ruleBindings[ index ] == null ) {
23:                         if( ( f & -2 ) == 0 ) {
24:                                 p.print( "VariTerm( _" + these.hashCode() + "_" + index + " )" );
25:                         }
26:                         else {
27:                                 p.print( "_" + these.hashCode() + "_" + index );
28:                         }
29:                 }
30:                 else these.ruleBindings[ index ].listing( f, these.instanceBindings[ index ], p, m );
31:         }
32:
33:         // all terms inherit the ability to bind an unbound variable from Term
34:         // bindto can be only called when variable is unbound (i.e. binding == null)
35:         final void bindto( final Term that, final Variables these, final Variables those, final Successor success )
36:         {
37:                 // This is the heart of the unification engine -- all inference actually occurs here --
38:                 //System.out.print("V");
39:                 these.ruleBindings[ index ] = that;     // do the binding thus add to 
40:                 these.instanceBindings[ index ] = those;        // constraint structure on terms
41:                 success.succeed();
42:                 these.ruleBindings[ index ] = null;     // backtrack
43:                 these.instanceBindings[ index ] = null; // on failure
44:         }
45:
46:         // unifythrough -- by juggling terms unifythrough does dynamic dispatch on its Term argument --
47:         //      for bound variables the corresponding bound term is substituted immediately
48:         protected final void unifythrough( final Term that, final Variables these, final Variables those, final Successor success )
49:         {
50:                 if( these.ruleBindings[ index ] == null ) that.unifytoUnboundVariable( this, those, these, success );
51:                 else these.ruleBindings[ index ].unifythrough( that, these.instanceBindings[ index ], those, success );
52:         }
53:
54:         // the meat of class VariTerm
55:         //      for bound variables the corresponding bound term is substituted immediately
56:         protected final void unifytoAtom( final AtomTerm that, final Variables these, final Variables those, final Successor success )
57:         {
58:                 if( these.ruleBindings[ index ] == null ) bindto( that, these, those, success );
59:                 else these.ruleBindings[ index ].unifytoAtom( that, these.instanceBindings[ index ], those, success );
60:         }
61:         protected final void unifytoPair( final PairTerm that, final Variables these, final Variables those, final Successor success )
62:         {
63:                 if( these.ruleBindings[ index ] == null ) bindto( that, these, those, success );
64:                 else these.ruleBindings[ index ].unifytoPair( that, these.instanceBindings[ index ], those, success );
65:         }
66:         protected final void unifytoCons( final ConsTerm that, final Variables these, final Variables those, final Successor success )
67:         {
68:                 if( these.ruleBindings[ index ] == null ) bindto( that, these, those, success );
69:                 else these.ruleBindings[ index ].unifytoCons( that, these.instanceBindings[ index ], those, success );
70:         }
71:         protected final void unifytoUnboundVariable( final VariTerm that, final Variables these, final Variables those, final Successor success )
72:         {
73:                 if( these.ruleBindings[ index ] == null ) {
74:                         // don't try to unify already unified variables!
75:                         if( this == that && these == those ) success.succeed();
76:                         else {
77:                                 // what is best -- binding an unbound this to an unbound that
78:                                 //      -- or -- binding an unbound that to an unbound this
79:                                 // I don't know so I hedged my bets and let a random flip decide
80:                                 if( randomGenerator.nextBoolean() ) this.bindto( that, these, those, success );
81:                                 else that.bindto( this, those, these, success );
82:                         }
83:                 }
84:                 else these.ruleBindings[ index ].unifytoUnboundVariable( that, these.instanceBindings[ index ], those, success );
85:         }
86:
87:         // the VariTerm node structure
88:         protected final int index;
89: }
90:
91: // fin