/* prolog.c: a simple Prolog interpreter written in C++,                */
/*           including an example test run as main().                   */
/* Copyright (c) Alan Mycroft, University of Cambridge, 2000.           */

#include <iostream>
using namespace std;
#include <string.h>

void indent(int n)
{   for (int i = 0; i<n; i++) cout << "    ";
}

class Atom {
    char *atomname;
public: Atom(char *s) : atomname(s) {}
    void print() { cout<<atomname; }
    bool eqatom(Atom *t) { return strcmp(atomname, t->atomname) == 0; }
};

class TermCons;

class Term {
public: virtual void print() = 0;
public: virtual bool unify(Term *) = 0;
public: virtual bool unify2(TermCons *) = 0;
public: virtual Term *copy() = 0;
};

class TermCons : public Term {
private:
    int arity;
    Atom *fsym;
    Term **args;
public:
    TermCons(Atom *f) : fsym(f), arity(0), args(NULL)
            { }
    TermCons(Atom *f, Term *a1) : fsym(f), arity(1), args(new Term*[1])
            { args[0]=a1; };
    TermCons(Atom *f, Term *a1, Term *a2)
            : fsym(f), arity(2), args(new Term*[2])
            { args[0]=a1, args[1]=a2; };
    TermCons(Atom *f, Term *a1, Term *a2, Term *a3)
            : fsym(f), arity(3), args(new Term*[3])
            { args[0]=a1, args[1]=a2, args[2]=a3; };
    void print() { fsym->print();
                   if (arity>0)
                   {   cout <<"(";
                       for (int i = 0; i<arity; )
                       {   args[i]->print();
                           if (++i < arity) cout << ",";
                       }
                       cout <<")";
                   }
                 }
    bool unify(Term *t) { return t->unify2(this); }
    Term *copy() { return copy2(); }
    TermCons *copy2() { return new TermCons(this); }
private:
    TermCons(TermCons *p)
            : fsym(p->fsym), arity(p->arity),
              args(p->arity==0 ? NULL : new Term*[p->arity])
            { for (int i=0; i<arity; i++) args[i] = p->args[i]->copy(); }
    bool unify2(TermCons *t) { 
      if (!(fsym->eqatom(t->fsym) && arity == t->arity))
          return false;
      for (int i = 0; i<arity; i++)
          if (!args[i]->unify(t->args[i])) return false;
      return true;
    }
};

class TermVar : public Term {
private:
    Term *instance;
    int varno;
    static int timestamp;
public:
    TermVar() : instance(this), varno(++timestamp) {}
    void print() { if (instance!=this) instance->print();
                   else cout<<"_"<<varno; };
    bool unify(Term *t);
    Term *copy();
    Term *reset() { instance = this; }
private:
    bool unify2(TermCons *t) { return this->unify(t); }
};

int TermVar::timestamp = 0;

class Program;
class TermVarMapping;

class Goal {
private:
    TermCons *car;
    Goal *cdr;
public:
    Goal(TermCons *h, Goal *t) : car(h), cdr(t) {}
    Goal *copy() { return new Goal(car->copy2(),
                                   cdr==NULL ? NULL : cdr->copy()); }
    Goal *append(Goal *l) { return new Goal(car,
                                   cdr==NULL ? NULL : cdr->append(l)); }
    void print() { car->print();
                   if (cdr != NULL) { cout << "; ", cdr->print(); }
                 }
    void solve(Program *p, int level, TermVarMapping *map);
};

class Clause {
public:
    TermCons *head;
    Goal *body;
    Clause(TermCons *h, Goal *t) : head(h), body(t) {}
    Clause *copy() { return new Clause(head->copy2(),
                                       body==NULL ? NULL : body->copy()); }
    void print() { head->print();
                   cout << " :- ";
                   if (body==NULL) cout << "true";
                   else body->print();
                 }
};

class Program {
public:
    Clause *pcar;
    Program *pcdr;
    Program(Clause *h, Program *t) : pcar(h), pcdr(t) {}
};

class Trail {
private:
    TermVar *tcar;
    Trail *tcdr;
    static Trail *sofar;
    Trail(TermVar *h, Trail *t) : tcar(h), tcdr(t) {}
public:
    static Trail *Note() { return sofar; }
    static void Push(TermVar *x) { sofar = new Trail(x, sofar); }
    static void Undo(Trail *whereto)
    {   for (; sofar != whereto; sofar = sofar->tcdr)
            sofar->tcar->reset();
    }
};
Trail *Trail::sofar = NULL;

bool TermVar::unify(Term *t) { 
                               if (instance!=this) return instance->unify(t);
                               Trail::Push(this); instance = t; return true; }
Term *TermVar::copy() {
                        if (instance==this)
                        {   Trail::Push(this); instance = new TermVar();
                        }
                        return instance;
                      }

class TermVarMapping {
private:
    TermVar **varvar;
    char **vartext;
    int size;
public:
    TermVarMapping(TermVar *vv[], char *vt[], int vs)
        :varvar(vv), vartext(vt), size(vs) {}
    void showanswer()
    {   if (size == 0) cout << "yes\n";
        else
        {   for (int i = 0; i < size; i++)
            {   cout << vartext[i] << " = "; varvar[i]->print(); cout << "\n";
            }
        }
    }
};

void Goal::solve(Program *p, int level, TermVarMapping *map)
{   indent(level); cout << "solve@"  << level << ": ";
                   this->print(); cout << "\n";
    for (Program *q = p; q != NULL; q = q->pcdr)
    {   Trail *t = Trail::Note();
        Clause *c = q->pcar->copy();
        Trail::Undo(t);
        indent(level); cout << "  try:"; c->print(); cout << "\n";
        if (car->unify(c->head))
        {   Goal *gdash = c->body==NULL ? cdr : c->body->append(cdr);
            if (gdash == NULL) map->showanswer();
            else gdash->solve(p, level+1, map);
        }
        else
        {   indent(level); cout << "  nomatch.\n";
        }
        Trail::Undo(t);
    }
}

/* A sample test program: append */

Atom *at_app = new Atom("app");
Atom *at_cons = new Atom("cons");
TermCons *f_nil = new TermCons(new Atom("nil"));
TermCons *f_1 = new TermCons(new Atom("1"));
TermCons *f_2 = new TermCons(new Atom("2"));
TermCons *f_3 = new TermCons(new Atom("3"));

Term *v_x = new TermVar();
TermCons *lhs1 = new TermCons(at_app, f_nil, v_x, v_x);
Clause *c1 = new Clause(lhs1, NULL);

Term *v_l = new TermVar();
Term *v_m = new TermVar();
Term *v_n = new TermVar();
TermCons *rhs2 = new TermCons(at_app, v_l, v_m, v_n);
TermCons *lhs2 = new TermCons(at_app, new TermCons(at_cons, v_x, v_l),
                                      v_m,
                                      new TermCons(at_cons, v_x, v_n));
Clause *c2 = new Clause(lhs2, new Goal(rhs2,NULL));

TermVar *v_i = new TermVar();
TermVar *v_j = new TermVar();
TermCons *rhs3 = new TermCons(at_app, v_i, v_j, 
                      new TermCons(at_cons, f_1,
                      new TermCons(at_cons, f_2,
                      new TermCons(at_cons, f_3, f_nil))));

Goal *g1 = new Goal(rhs3, NULL);

Program *test_p = new Program(c1, new Program(c2, NULL));
Program *test_p2 = new Program(c2, new Program(c1, NULL));

TermVar *varvar[] = {v_i, v_j};
char *varname[] =  {"I", "J"};
TermVarMapping *var_name_map = new TermVarMapping(varvar, varname, 2);

int main(int argc, char *argv[])
{
   cout << "=======Append with normal clause order:\n";
   g1->solve(test_p, 0, var_name_map);
   cout << "\n=======Append with reversed normal clause order:\n";
   g1->solve(test_p2, 0, var_name_map);
   return 0;
}

from http://www.cl.cam.ac.uk/~am21/research/funnel/prolog.c