// #define LISP90 1
#define DEBUGGING 1

#ifdef LISP90
int test_program_append();
#include "lisp90.cpp"
#else
#define nonvar char*
#define read_atom(s) s
// #define to_string(s) s
#endif

#define C_TEXT( text ) ((char*)std::string( text ).c_str())
#undef C_TEXT
#define C_TEXT( text ) ((char*)text)

#define MKATOM(TEXT) new Atom(C_TEXT(TEXT))
#define FACT(TEXT) new Clause(TEXT)
#define RULE(HEAD,BODY...) new Clause(HEAD,BODY)

/*Psuedovars for source translation */
#define PSUEDOVAR(NAME)  Var* V(NAME) = new Var()
#define V(NAME) VAR_ ## NAME
#define TERMS Structure*


/* Create a Callable Compound*/
#define CC(TEXT...) new Structure(TEXT)
/* Create a List*/
#define LL(TEXT...) CC(ATOM_dot,TEXT)

#ifdef DEBUGGING
//#define DEBUG(mask,CPP) if ((mask & debugflags)!=0) CPP
#define DEBUG(mask,CPP) CPP
#else
#define DEBUG(mask,CPP)
#endif

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

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

class Trail; class Structure; class Var; class Prog1Pred;

class TermVarMapping
{
private:
  Var* *varvar;
  const char* *vartext;
  int size;
public:
  TermVarMapping(Var* vv[], const 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] << "\n";
    }
  }
};

class Term
{
public:
  virtual bool unify(Trail* ,Term* ) = 0;
  virtual bool unify2(Trail* , TERMS ) = 0;
  virtual Term* copy(Trail* ) = 0;
  virtual void reset() = 0;
  void debug() { cout<<this; }
  virtual ostream& operator<<(ostream& str) = 0;
};

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


class Atom
{ nonvar atomname;
public: Atom(char* s) :
    #ifdef LISP90
       atomname(read_atom(s)){}
    #else
       atomname(s){}
    #endif

  const char* c_str()
  {
    #ifdef LISP90
       return to_string(atomname).c_str();
    #else
       return atomname;
    #endif
  }

  ostream& operator<<(ostream& str)
  { return str <<  "atom(" << c_str() << ")"; }

  bool eqatom(Atom* t)
  { return(strcmp(c_str(),t->c_str()) == 0);
  }
};


Atom* ATOM_nil = MKATOM("[]");
Atom* ATOM_dot = MKATOM(".");

class Structure : public Term
{ int arity;
  Atom* fsym;
  Term** args;
public:
  Structure(const char* f): fsym(MKATOM(f)), arity(0), args(NULL){}
  Structure(Atom* f): fsym(f), arity(0), args(NULL){}
  Structure(Atom* f, Term* a1): fsym(f), arity(1), args(new Term*[1]){args[0]=a1;};
  Structure(Atom* f, Term* a1, Term* a2): fsym(f), arity(2), args(new Term*[2]){args[0]=a1, args[1]=a2;};
  Structure(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;}

  ostream& operator<<(ostream& str)
  {
    if(fsym==ATOM_dot)
    {
      str <<"[";
      for(int i = 0; i<arity;)
      {
        str << args[i++];
        if(args[i] == NULL) continue;
        if(i < arity) str << "|";
      }
      return str <<"]";
    }
    str << fsym;
    if(arity>0)
    {
      str <<"(";
      for(int i = 0; i<arity;)
      {
        str << args[i];
        if(++i < arity) str << ",";
      }
      str <<")";
    }
    return str;
  }
  bool unify(Trail* mach,Term* t)
  {
    return(t->unify2(mach,this));
  }
  Term* copy(Trail* mach)
  {
    return(copyNonvar(mach));
  }
  TERMS copyNonvar(Trail* mach)
  {
    return(CC(mach,this));
  }
  virtual void reset(){}
private:
  Structure(Trail* mach, TERMS 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(mach);
  }

  bool unify2(Trail* mach, TERMS t)
  {
    if(!(fsym->eqatom(t->fsym) && arity == t->arity))
      return(false);
    for(int i = 0; i<arity; i++)
      if(!args[i]->unify(mach,t->args[i])) return(false);
    return(true);
  }
};

class Var : public Term
{
private:
  Term* instance;
  int varno;
  static int timestamp;
public:
  Var() : instance(this), varno(++timestamp) {}
  ostream& operator<<(ostream& str)
  { if(instance!=this) return str << instance; else return str <<"_"<<varno;
  }
  virtual void reset() {instance = this;}
private:
  bool unify2(Trail* mach,TERMS t)
  {
    return(this->unify(mach,t));
  }
  bool unify(Trail* mach, Term* t)
  {
    if(instance!=this) return(instance->unify(mach,t));
    mach->Push(this); instance = t; return(true);
  }

  Term* copy(Trail* mach)
  {
    if(instance==this)
    {
      mach->Push(this); instance = new Var();
    }
    return(instance);
  }
};

int Var::timestamp = 0;


class Goal
{
private:
  TERMS car;
  Goal* cdr;
  Trail* mach;

public:
  Goal(TERMS h ) : car(h), cdr(NULL) {mach = new Trail();}
  Goal(TERMS h, Goal* t) : car(h), cdr(t) {mach = new Trail();}

  Goal* copy(Trail* mach) {
    return(new Goal(car->copyNonvar(mach),
                    cdr==NULL ? NULL : cdr->copy(mach)));
  }
  Goal* append(Goal* l)
  { return(new Goal(car,cdr==NULL ? NULL : cdr->append(l))); }

  ostream& operator<<(ostream& str)
  {  str << "GOAL: " << car;
     if (cdr != NULL) str << ", " << cdr;
     return str;
   }

  Prog1Pred* solve(Prog1Pred* p, int level, TermVarMapping* map);
};

class Clause
{
public:
  TERMS head;
  Goal* body;
  Clause(TERMS h, Goal* t) : head(h), body(t) {}
  Clause(TERMS h, TERMS t) : head(h), body(new Goal(t)) {}
  Clause(TERMS h) : head(h), body(NULL) {}

  Clause* copy(Trail* mach)
  { return(RULE(head->copyNonvar(mach),
                      body==NULL ? NULL : body->copy(mach)));
  }
  ostream& operator<<(ostream& str)
  { str << head << " :- ";
    if(body==NULL) str<<"true"; else str<<body;
    return str;
  }

  Clause* append(TERMS l)
  { if(body==NULL) {body = new Goal(l);}
    else {
       body = body->append(new Goal(l));
    }
    return this;
  }

};

class Prog1Pred
{
public:
  Clause* pcar;
  Prog1Pred* pcdr;
  Prog1Pred(Clause* h) : pcar(h), pcdr(NULL){}
  Prog1Pred(Clause* h, Prog1Pred* t) : pcar(h), pcdr(t){}
  Prog1Pred(Clause* h, Clause* t) : pcar(h), pcdr(new Prog1Pred(t)){}
  Prog1Pred(Clause* h, Clause* h2, Clause* t) : pcar(h), pcdr(new Prog1Pred(h2, t)){}

  /* returns the newly appended Prog1Pred*/
  Prog1Pred* append(Clause* l)
  { if(pcdr==NULL) {return pcdr = new Prog1Pred(l);}
    else {
       return pcdr->append(l);
    }
  }

  /* returns itself*/
  Prog1Pred* prepend(Clause* h)
  {
    pcdr = new Prog1Pred(pcar, pcdr);
    pcar = h;
    return this;
  }
};


TERMS NIL = CC(ATOM_nil);

TERMS CUT = CC(MKATOM("!"));
/* returns a new Goal if coroutining or null if cutted */
Prog1Pred* Goal::solve(Prog1Pred* p, int level, TermVarMapping* map)
{
  if(mach==NULL) mach = new Trail();

  Prog1Pred* retQ = p;

  DEBUG(SOLVE,{ indent(level); cout << "solve@"  << level << ": " << this << "\n";});

  for(Prog1Pred* q = p; q != NULL; q = q->pcdr)
  {
    Trail* t = mach->Note();
    Clause* next = q->pcar;
    /*
    if(next ==CUT)
    {
      //cutTo =
      // should succeed
      DEBUG(SOLVE,{ indent(level); str << "  cut: " <<  q << "\n";});
      return retQ;
    }
    */

    retQ = q;

    Clause* c = next->copy(mach);
    mach->Undo(t);
    DEBUG(SOLVE,{ indent(level); cout << "  try: " <<  c << "\n";});
    if(car->unify(mach,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
    {
      DEBUG(SOLVE,{
          indent(level); cout << "  nomatch.\n";});
      //break;
    }
    mach->Undo(t);
  }
}



int test_program_append()
{
/*Psuedovars for source translation */
PSUEDOVAR(X);
PSUEDOVAR(L);
PSUEDOVAR(M);
PSUEDOVAR(N);
PSUEDOVAR(I);
PSUEDOVAR(J);


  Atom* APPEND3 = MKATOM("append_3");




  /* append_3([],X,X). */
  Clause* c1 = FACT(CC(APPEND3, NIL, VAR_X, VAR_X));
  /*  append([X|LL],M,[X|N]):- append(LL,M,N). */
  Clause* c2 = RULE(CC(APPEND3, LL(VAR_X, VAR_L),VAR_M, LL(VAR_X,VAR_N)), CC(APPEND3, VAR_L, VAR_M, VAR_N));


  /*
     Test normally:

      append_3([],X,X).
      append([X|LL],M,[X|N]):- append(LL,M,N).
  */
  Prog1Pred* test_program_normally = new Prog1Pred(c1, c2);


  /*
    Test reversed:

      append([X|LL],M,[X|N]):- append(LL,M,N).
      append_3([],X,X).
  */
  Prog1Pred* test_program_reversed = new Prog1Pred(c2, c1);


  /*
     Test Cat:

      append_3([],X,X):- !.
      append([X|LL],M,[X|N]):- append(LL,M,N).
  */
  Clause* c3 = c1->copy(new Trail());
  c3->append(CUT);

  Prog1Pred* test_program_cut = new Prog1Pred(c3, c2);



  Var* varvar[] = {VAR_I,VAR_J};
  const char* varname[] = {"I", "J"};
  TermVarMapping* var_name_map = new TermVarMapping(varvar, varname, 2);

  /*
     ?- append_3(I,J,[1,2,3]).
  */
  Goal* g1 = new Goal(CC(APPEND3, VAR_I, VAR_J, LL( CC("1"),LL( CC("2"),LL( CC("3"), NIL)))));

  cout << "=======Append with normal clause order:\n";
  g1->solve(test_program_normally, 0, var_name_map);

  cout << "\n=======Append with reversed normal clause order:\n";
  g1->solve(test_program_reversed, 0, var_name_map);

  cout << "\n=======Append with a cut:\n";
  g1->solve(test_program_cut, 0, var_name_map);

  return(0);
}


#ifndef LISP90
int main(int argc, char* argv[]) {
   test_program_append();
}
#endif