Prolog implementation of McCarthy's metacircular lisp interpreter, following pg's explication

smolisp.pl

:- use_module(library(reif)).

axiom([quote, X], X).

axiom([atom, X], R) :-
  axiom(X, XR),
  ((atomic(XR),   R = t, !) ;
   (compound(XR), R = [])).

axiom([eq, X, Y], R) :-
  axiom(X, XR),
  axiom(Y, YR),
  if_((XR = YR), R = t, R = []).

axiom([car, X], R) :-
  axiom(X, [R|_]).

axiom([cdr, X], R) :-
  axiom(X, [_|R]).

axiom([cons, X, More], R) :-
  axiom(X, XR),
  axiom(More, MoreR),
  R = [XR|MoreR].

axiom([cond, [Test, Expr] | More], R) :-
  axiom(Test, TestR),
  if_((TestR = t),
    axiom(Expr, R),
    axiom([cond | More], R)).

/* These are the base forms! Now we move on to derived ones. */

/* Null testing */
axiom([null, X], R) :-
  axiom([eq, X, [quote, []]], R).

/* Boolean logic */
axiom([and, X, Y], R) :-
  axiom([cond, [X, [cond, [Y, [quote, t]],
                          [[quote, t], [quote, []]]]],
               [[quote, t], [quote, []]]],
        R).

axiom([not, X], R) :-
  axiom([cond, [X,          [quote, []]],
               [[quote, t], [quote, t]]],
        R).

/* List construction */
axiom([list, X, Y], R) :-
  axiom([cons, X, [cons, Y, [quote, []]]], R).

/* List concat */
axiom([append, X, Y], R) :-
  axiom([cond, [[null, X],  Y],
               [[quote, t], [cons, [car, X], [append, [cdr, X], Y]]]],
        R).

/* Zip together lists of as and lists of bs into [[a1 b1] [a2 b2] ...] */
axiom([pair, Xs, Ys], R) :-
  axiom([cond, [[and, [null, Xs], [null, Ys]], [quote, []]],
               [[and, [not, [atom, Xs]], [not, [atom, Ys]]],
                [cons, [list, [car, Xs], [car, Ys]],
                       [pair, [cdr, Xs], [cdr, Ys]]]]],
        R).

/* Look up an element in a pair list */
axiom([assoc, K, Pairs], R) :-
  axiom([cond, [[eq, K, [car, [car, Pairs]]], [car, [cdr, [car, Pairs]]]],
               [[quote, t],                   [assoc, K, [cdr, Pairs]]]],
        R).

/* Cond evaluator */
axiom([evcon, Cond, Env], R) :-
  axiom([cond, [[eval, [car, [car, Cond]], Env],
                [eval, [car, [cdr, [car, Cond]]], Env]],
               /* Recur */
               [[quote, t], [evcon, [cdr, Cond], Env]]],
        R).

/* Evaluate each element of a list in the context of an environment*/
axiom([evlis, M, Env], R) :-
  axiom([cond, [[null, M],  [quote, []]],
               [[quote, t], [cons, [eval, [car, M], Env],
                                   [evlis, [cdr, M], Env]]]],
        R).

/* Debugger */
axiom([log, X], R) :-
  axiom(X, R),
  print(R).

/* :- set_prolog_flag(toplevel_print_options,
 [quoted(true), portrayed(true), max_depth(0)]). */

/* E V A L U A T O R */
axiom([eval, Expr, Env], R) :-
  axiom(
    [cond,
      /* Symbol dereference in environment */
      [[atom, Expr], [assoc, Expr, Env]],

      /* (quote expr), (atom expr), etc */
      [[atom, [car, Expr]],
       [cond,
         [[eq, [car, Expr], [quote, quote]], [car, [cdr, Expr]]],

         [[eq, [car, Expr], [quote, log]],
          [log, [eval, [car, [cdr, Expr]], Env]]],

         [[eq, [car, Expr], [quote, atom]],
          [atom, [eval, [car, [cdr, Expr]], Env]]],

         [[eq, [car, Expr], [quote, eq]],
          [eq, [eval, [car, [cdr, Expr]],        Env],
               [eval, [car, [cdr, [cdr, Expr]]], Env]]],

         [[eq, [car, Expr], [quote, car]],
          [car, [eval, [car, [cdr, Expr]], Env]]],

         [[eq, [car, Expr], [quote, cdr]],
          [cdr, [eval, [car, [cdr, Expr]], Env]]],

         [[eq, [car, Expr], [quote, cons]],
          [cons, [eval, [car, [cdr, Expr]],        Env],
                 [eval, [car, [cdr, [cdr, Expr]]], Env]]],

         [[eq, [car, Expr], [quote, cond]], [evcon, [cdr, Expr], Env]],

         /* Look up term in environment and recur */
         [[quote, t], [eval, [cons, [assoc, [car, Expr], Env],
                                    [cdr, Expr]],
                             Env]]]],

      /* (label var body) */
      [[eq, [car, [car, Expr]], [quote, label]],
       /* Evaluate body... */
       [eval, [cons, [car, [cdr, [cdr, [car, Expr]]]], [cdr, Expr]],
              /* With var bound to the fn form */
              [cons, [list, [car, [cdr, [car, Expr]]], [car, Expr]], Env]]],

      /* (lambda (x y) body) */
      [[eq, [car, [car, Expr]], [quote, lambda]],
       /* Evaluate body ... */
       [eval, [car, [cdr, [cdr, [car, Expr]]]],
              /* With an environment plus additional bindings of the argument
               list to... */
               [append, [pair, [car, [cdr, [car, Expr]]],
               [evlis, [cdr, Expr], Env]],
               Env]]],

      [[quote, t], [quote, "no match"]]],
    R).

prologue([

[test, [lambda, [], [quote, test-success]]],

[do2, [lambda, [a, b], b]],
[do3, [lambda, [a, b, c], c]],

[rectest, [label, rectest, [lambda, [x],
  [cond, [[atom, x],  x],
         [[quote, t], [rectest, [car, x]]]]]]]

]).

lisp(Expr, R) :-
  prologue(P),
  axiom([eval, [quote, Expr], [quote, P]], R).