The latest version of the interpreter can always be found at http://tribble.ilrt.bris.ac.uk/~cmjg/logic/prolog-latest - which should be used for external references.
The preliminary version is implemented using a recursive "tiny-prolog"-style interpreter. It doesn't support any of the extra-logical features of Prolog proper, nor any of the builtins.
The following sections outline how I see this progressing.
There is a simple method to implement many builtins. This involves including some of the code that implements a resolution step into each builtin; apart from that, the chore isn't too onerous, and can cover many of the standard functions, including some of the extra-logical ones.
There is quite a bit of scope here; for example, a builtin not/1 can include delaying until its arguments are ground with little extra effort.
Anyway, the implementation of Prolog with builtins is now online.
This is a little trickier. The way to do it is as follows: each term in the goal list carries with it a pointer to its parent subgoal. Backtracking over a builtin cut raises a flag on that parent subgoal which causes all other backtracking to fail.
renameVariables is given a third parameter to support this functionality. The cut/0 builtin flags a term's parent as having been cut when it is backtracked over.
Anyway, the changes (while profound), are minimal, and result in a recursive implementation of prolog with cut.
This is trickier still, and slightly changes the way that uiltins are implemented. A working version is available; it needs checking for bugs.
Each subgoal now additionally carries with it a result destination that determines what to do with successful results: they can be output (as before) or elements of the environment can be added to a list (as in the case of bagof). This technique has other, more general, applications.
The latest version allows a term in the body of a rule to be preceeded by a NOTTHIS qualifier.
This is interpreted as meaning: do not attempt to use the current rule in satisfying the named subgoal.
This is not very clever; it doesn't work deeply down an evaluation stack. The only place it is useful is in defining transitive functions in terms of themselves, as seen here.
Cheap hack, but handy on occasion. We can add hints to the definition of each predicate that indicate whether it expects its terms to be ground, bound, or free. The resolution step can shuffle a subgoal backwards in the queue if its terms are not sufficiently instantiated.
When you see a link from this section, it'll point to a tabling imlpementation that might even use a WAM variant. Yeah, right.