/*
 * Unify pred program copyright (C) 2009 - 2013 H.Niwa
 */

/*
 * This program is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2, or (at your option)
 * any later version.

 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.

 * You should have received a copy of the GNU General Public License
 * along with this program; if not, write to the Free Software
 * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA
 * 02110-1301, USA.
 */

#include "config.h"

#include <stdio.h>
#include <stdlib.h>
#include <errno.h>
#include <string.h>
#include <setjmp.h>

#include <string>
#include <complex>

#include "syserr.h"

#include "bin_node.h"
#include "gc.h"
#include "var.h"
#include "pred.h"
#include "context.h"
#include "builtin.h"
#include "sysmodule.h"
#include "module.h"
#include "unify.h"
#include "func.h"
#include "timeout.h"
#include "token.h"
#include "ncurlib.h"
#include "compiler.h"

/* base module list */
List *Module;

/* enable/disable trace flag */
int TraceFlag = 0;

/* enable/disable step trace flag */
int StepFlag = 0;

/* enable/disable display result flag */
int DResultFlag = 0;

/* break flag */
int BreakFlag = 0;

/* throw flag */
int ThrowFlag = 0;

int CheckInherit(Node* var, Context* cx)
{
	Node*	n = cx->inherit;
	int	num = 0;
	
	for ( ; n->kind() != ATOM; n=n->Cdr()) {
		if (n->Car()->Eq(var)) {
			num++;
			if (num > 10) {
				return 1;
			}
		}
	}
	return 0;
}

/* Push an Unify stack unit. store successful unification records */
void PushStack(Context* cx, Node* goals, Node* md,
	       Node* env)
{
    /* record an input position */
    long seekp = ftell(cx->ioin);

//printf("PushStack env %x \n", env);
//PrintNode("PushStack env val ", env);
    cx->env_stack = Cons(MkList(goals, md, mka((long long)seekp), env), 
    			cx->env_stack);

//PrintNode("PushStack goals ", goals);
}


/* Pop an Unify stack unit. take out unificaion recoreds */
int PopStack(Context * cx, Node* &goals, Node* &md, Node* &env)
{
    if (cx->env_stack->Car() == Nil) {
//PrintNode("PopStack 0 goals ", goals);
//PrintNode("PopStack 0 env_stack ", cx->env_stack);
	return 0;
    }

    goals = cx->env_stack->Car()->Car();
    md = cx->env_stack->Car()->Cdr()->Car();
    Node* 
    nseekp = cx->env_stack->Car()->Cdr()->Cdr()->Car();
    env = cx->env_stack->Car()->Cdr()->Cdr()->Cdr()->Car();
//PrintNode("PopStack new env ", env);

    /* return an input position to the old position */
    long long seekp;
    ((Atom*)nseekp)->toInt(seekp);
    
    if (seekp >= 0) {
	fseek(cx->ioin, (long)seekp, 0);
    }

    cx->env_stack = cx->env_stack->Cdr();

//PrintNode("PopStack 1 goals ", goals);
//PrintNode("PopStack 1 md ", md);

    return 1;
}

/* drop an Unify stack unit. */
int DropStack(Context * cx)
{
	Node* dummy_goals;
	Node* dummy_md;
	Node* dummy_env;
//printf("Dropstack call PopStack \n");

	int r = PopStack(cx, dummy_goals, dummy_md, dummy_env);

//printf("DropStack dummy_env %x \n", dummy_env);
//PrintNode("DropStack dummy_env ", dummy_env);
	if (r) {
		UnsetEnv(dummy_env);
	}

	return r;
}

/* find a cutmark in the Unify stack. */
int FindCutMark(Node* goals, Node* cut)
{
    Node* goalscar;
    Node* goalscdr;
    int level;
    for (; goals->kind() != ATOM; ) {
	level = 0;
	goalscar = GetLeftNode(goals, goalscdr, level);
//	goalscar = goals->Car();

	if (goalscar == cut) {
	    return 1;
	}
	
	goals = goalscdr;
//	goals = goals->Cdr();
    }
    return 0;
}

/* repeal Unify stack units to a cut operator. */
void CutStack(Context* cx, Node* cut)
{
    Node* goals;
    Node* md;
    Node* env;
    
    for (;;) {
//PrintNode("FindCutMark ", cx->env_stack->Car()->Car());
	if (!FindCutMark(cx->env_stack->Car()->Car(), cut)) {
//printf("CutStack trace 0 \n");
//printf("CutStack 1 call PopStack \n");
		PopStack(cx, goals, md, env);
		return;
	}
//printf("CutStack 2 call PopStack \n");
	if (!PopStack(cx, goals, md, env)) {
//printf("CutStack trace 1 \n");
		return;
	}
//printf("CutStack trace 2 \n");
    }
}

/* make a duplication of Node */
Node *Dup(Node* n)
{
    /*
      call Dup of each node after clearing all dupp flag.
    */
    (n)->DuppClr();
    return (n)->Dup();
}


/* set a variable environment */
void SetEnv(Node* env, Node* udef)
{
    if (env->kind() != LIST) {
	syserr("SetEnv : not LIST");
	return;
    }
    Node *np = new List(udef, ((Undef *) udef)->GetUndefValue());
    np = np->Cons(env->Car());
    ((List *) env)->SetCar(np);

}

/* unset all variable environments */
void UnsetEnv(Node* env)
{
    Node *np1;
    Node *np2;

//PrintNode("UnsetEnv env ", env);

    for (np1 = env->Car(); (np1 != Nil) && (np1->Car() != Nil); 
						np1 = np1->Cdr()) {
	np2 = np1->Car();
//PrintNode("Unsetenv ", np2->Car());

	((Undef *) (np2->Car()))->Set(np2->Cdr());
	((List *) env)->SetCar(env->Car()->Cdr());
    }
}


/* unify the elements of the list. */
int Unification(Node* pred1, Node* pred2, Node* env, Context* cx)
{
    Node *pr1 = pred1->Val();
    Node *pr2 = pred2->Val();

//printf("* Unification     "); pred1->print(); printf(" : "); pred2->print();  printf("\n");
//printf("* Unification Val "); pred1->Val()->print(); printf(" : "); pred2->Val()->print();  printf("\n");

    if (pr2->kind() == UNDEF) {
	if ((pr1 == pr2) ||
	    (((Undef*)pr1)->GetUndefValue() == pr2) ||
	    (pr1 == ((Undef*)pr2)->GetUndefValue())) {
		return 1;
	}
		
	SetEnv(env, pr2);
	((Undef *) pr2)->Set(pr1);
	return 1;
    }

    if (pr1->kind() == UNDEF) {
	if ((pr1 == pr2) ||
	    (((Undef*)pr1)->GetUndefValue() == pr2) ||
	    (pr1 == ((Undef*)pr2)->GetUndefValue())) {
		return 1;
	}

	SetEnv(env, pr1);
	((Undef *) pr1)->Set(pr2);
	return 1;
    }

    if (pr1->kind() != pr2->kind()) {
	if (!(pr1->kind() == LIST && pr2->kind() == PRED) &&
	    !(pr1->kind() == PRED && pr2->kind() == LIST)) {
	    return 0;
	}
    }

    switch (pr1->kind()) {
    case PRED: 
    case LIST:
    	return  Unification(pred1->Car(), pred2->Car(), env, cx)
    	       && Unification(pred1->Cdr(), pred2->Cdr(), env, cx);
	break;
    case ATOM:
    	{
	return pr1->Eq(pr2);
	}
	break;
    case VAR:
	// VAR needs not to be used.
	// The reason is because it is converted into set value or UNDEF
	syserr("Unification: pred1 is Var");
	return 0;
	break;
    default:
	syserr("Unification: pred1 is undefined kind");
	return 0;
	break;
    }

}

/* It is the Unify processing that does not have context in an argument. */
int Unify(Node* goals)
{
    Context *cx = new Context(Module, new Atom("WORLD"));

    int r = Unify(cx, goals);

    delete cx;
    cx = 0;

    return r;
}

/* It is the Unify processing that does not have module in an argument. */
int Unify(Context*& cx, Node* goals)
{
	return Unify(cx, goals, Module);
}

/* main processing to carry out Unify. */
int Unify(Context*& cx, Node* goals, List* module)
{
    Node *md  = Nil;
    Node *bd  = Nil;
    cx->env = Nil->Cons(Nil);

    int rval;

    Node *goalscar;
    Node *goalscdr;
    int  level = 0, newlevel = 0;

    /*
     * The origin is a function call. Unify() was recurcieve
     * called and executed. 
     * However, to decrease the overhead of the function call, 
     * it changed it into the 'goto' operation. There are no 
     * differences before it changes.
     * 'goto CALLUNIFY' is equivalent to 'Unify()' call. 
     * 'goto RETUNIFY' is equivalent to 'return rval'. 
     */
CALLUNIFY:
    extern int sigint_flag;
    if (sigint_flag) {
    	sigint_flag = 0;
    	EventThrow(mka("SIGINT"));
    }

    if (BreakFlag) {
    	return 1;
    }
    if (ThrowFlag) {
    	return 1;
    }
    
    // check timeout
    CheckTime();

    if (goals == Nil) {
//printf("Unify goals Nil \n");
        return 1;
    }

    /*
     * The head of LIST is taken out. 
     * In addition, when the head of LIST is LIST, the head in 
     * that is taken out.
     */
    level = 0;
    goalscar = GetLeftNode(goals, goalscdr, level);
    goalscar = goalscar->Val();

    ErrGoal = goalscar;
    
//PrintNode("GetLeftNode goals ", goals);
//PrintNode("GetLeftNode goalscar ", goalscar);
//PrintNode("GetLeftNode goalscdr ", goalscdr);
//printf("GetLeftNode level %d \n", level);

    // token Nil is ignored
    if (goalscar == Nil) {
	goals = goalscdr;
	goto CALLUNIFY;
    }

    // step for debug
    if (StepFlag) {
    	char c[2];

	fflush(stdin);
	PrintNode("goals : ", goals->Val());
	printf("step ! (s: step, c: continue) \n");
    	char* rsc = fgets(c, 2, stdin);
	fflush(stdin);
    	
	if (c[0] == 's') {
		StepFlag = 1;
	} else if (c[0] == 'c') {
		StepFlag = 0;
	}

    } else if (TraceFlag) {
//	PrintNode("goals : ", goals->Val());
    }


    // check pred
    if (goalscar->kind() == PRED) {
	// check sys module pred
#if 1
	if (CheckInherit(mka("sys"), cx)) {
		int r;
		int rt = sysmodule(cx, goalscar, goalscdr, goals, module, r);
		if (rt) {
			if (r>0) {
		    		if (TraceFlag) {
					PrintNode("sys module: ", goalscar->Val(), "...success");
				}
			    goals = goalscdr;
			    goto CALLUNIFY;
			} else {
			    rval = r;
			    if (TraceFlag) {
				if (rval == 0) {
					PrintNode("sys module: ", goalscar->Val(), "...false");
				} else {	// rval == -1
					PrintNode("sys module: ", goalscar->Val(), "...unknown");
				}
			    }
			    goto RETUNIFY;
			}
		}
	}
#endif

//PrintNode("goalscar trace 0 ", goalscar);

	std::string s;

	// check operator pred
	if ((goalscar->Car()->kind() == ATOM) 
	    		&& (goalscar->Cdr() == Nil)) {
	       ((Atom *)(goalscar->Car()))->toString(s);
	        if (s == CUTOP) {
//printf("cut !!\n");
		    CutStack(cx, goalscar);
		    goals = goalscdr;
		    goto CALLUNIFY;
	        } else if (s == TRUEOP) {
		    goals = goalscdr;
		    goto CALLUNIFY;
	        } else if (s == FALSEOP) {
//printf("false !!\n");
	            rval = 0;
		    goto RETUNIFY;
	        } else if (s == UNKNOWNOP) {
		    if (PopStack(cx, goals, md, cx->env)) {
			if (TraceFlag) {
				PrintNode("*** back track ***1 ", goals->Car());
			}
//PrintNode("backtrack 1 goals ", goals);
			if (goals->Car()->Eq(mka("x"))) {
				xex(cx, goals->Cdr(), module);
			}

		        level = 0;
		        goalscar = GetLeftNode(goals, goalscdr, level);
		        rval = -1;
		        goto RETUNIFY;
		    } else {
		        return -1;
		    }
	        } else if (s == BREAKOP) {
//printf("break !!\n");
		    if (TraceFlag) {
		    	printf("*** break ***\n");
		    }
	            rval = 1;
	            BreakFlag = 1;
		    goto RETUNIFY;
	        } else if (s == BRKOP) {
//printf("brk !!\n");
	    	    char c[1024];

		    PrintNode("brk ! (s: step, c: continue) \n", goals);
    	    	    char* rsc = fgets(c, 1023, stdin);
    	    	    c[1023] = 0;
		    for (int i=0; i < 1023; i++) {
			if ((c[i] == 's') || (c[i] == '\n')){
				StepFlag = 1;
				break;
			} else if (c[i] == 'c') {
				StepFlag = 0;
				break;
			}
		    }
		    goals = goalscdr;
		    goto CALLUNIFY;
	        }
	    } else if (goalscar->Car()->Eq(mka(WCARD))) {
//printf("unify wcard trace \n");
		    rval = tokenWildcard(cx, goalscar, goalscdr, goals);
		    if (rval >= 0) {
		    	goals = goalscar = goalscdr = Nil;
			goto CALLUNIFY;
		    } else {
			goto RETUNIFY;
		    }
	    }

	    int r;

//PrintNode("goalscar trace 1 ", goalscar);

//PrintNode("Unify Pred : ", goalscar->Val());
//	    cxpush(cx, bd);
            bd = Nil;
	    cxpush(cx, md);
	    cxpush(cx, goals);
	    cxpush(cx, goalscar);
	    cxpush(cx, goalscdr);
	    if (builtin(cx, goalscar, goalscdr, goals, module, r)) {
//	    	cxpop(cx);
	    	cxpop(cx);
	    	cxpop(cx);
	    	cxpop(cx);
	    	cxpop(cx);
//PrintNode("goalscar trace 1.1 ", goalscar);
		if (r>0) {
		    if (TraceFlag) {
		    	if (!goalscar->Car()->Eq(mka("obj")) &&
			    !goalscar->Car()->Eq(mka("unify"))) {
				PrintNode("builtin: ", goalscar->Val(), 
					"...success");
			}
		    }
		    goals = goalscdr;
//PrintNode("goalscar trace 1.2 ", goalscar);
		    goto CALLUNIFY;
		} else {
//PrintNode("goalscar trace 1.3 ", goalscar);
		    rval = r;
		    if (TraceFlag) {
		    	if (!goalscar->Car()->Eq(mka("obj")) &&
			    !goalscar->Car()->Eq(mka("unify"))) {
				if (rval == 0) {
					PrintNode("builtin: ", goalscar->Val(), 
							"...false");
				} else {	// rval == -1
					PrintNode("builtin: ", goalscar->Val(), 
							"...unknown");
				}
			}
		    }
//PrintNode("goalscar trace 1.4 ", goalscar);
		    goto RETUNIFY;
		}
	    } else {
//PrintNode("goalscar trace 1.5 ", goalscar);
//	    	cxpop(cx);
	    	cxpop(cx);
	    	cxpop(cx);
	    	cxpop(cx);
	    	cxpop(cx);
	    
	   }
//PrintNode("goalscar trace 1.6 ", goalscar);
    }

//PrintNode("goalscar trace 2 ", goalscar);

    // parse token
    if (goalscar->kind() == ATOM) {
    	std::string s;
    	((Atom*)goalscar)->toString(s);
//	syserr("not a predication but strings:%s appeared. \n", s.c_str());

	// token Node
	if (tokenCmpDirect(cx, goalscar, goalscdr, goals, md) == 1) {
	    if (TraceFlag) {
		PrintNode("token: [", goalscar->Val(), "]...success");
	    }

	    goals = goalscdr;
	    goto CALLUNIFY;
	} else {
#if 0
	    if (TraceFlag) {
		extern std::string RToken;

	    	int tlen = RToken.length()+20;
	    	char* tbuf = new char[tlen];
	    	strncpy(tbuf, "token: [", 9);
	    	strncat(tbuf, RToken.c_str(), RToken.length());
	    	strncat(tbuf, "] : [", 6);
		PrintNode(tbuf, goalscar->Val(), "]...fail");
	    }
#endif 

            rval = -1;
            goto RETUNIFY;
	}

    }


//PrintNode("goalscar trace 3 ", goalscar);

//printf("\nUnify     "); goals->print(); printf("\n");
//printf("Unify Val "); goals->Val()->print(); printf("\n");

    md = module->Car();
//printf("Unify md "); md->print(); printf("\n");

    int undeclareflag;
    for (undeclareflag=0;;undeclareflag++) {
//PrintNode("goalscar trace 4 ", goalscar); fflush(stdout);
	while (md->kind() == LIST) {
//PrintNode("goalscar trace 5 ", goalscar); fflush(stdout);
		// extend inherit module
		Node* name = md->Car()->Car()->Val();
		if ((name->kind() == ATOM) 
				&& (((Atom*)name)->EqStr("inherit"))) {

//PrintNode("inherit unify ", MkList(mka("unify"), md->Car()->Cdr()->Car(),goalscar));
//PrintNode("cx->inherit ", cx->inherit);
			if (CheckInherit(md->Car()->Cdr()->Car(), cx)) {
				std::string s, s2;
				((Atom*)md->Car()->Cdr()->Car())->toString(s);
				((Atom*)cx->modulename->Car())->toString(s2);
				syserr("inherit overlaps : %s in %s \n", 
						s.c_str(), s2.c_str());
				rval = 0;
				goto RETUNIFY;
			} else {
				cx->inherit = Cons(md->Car()->Cdr()->Car(), 
						cx->inherit);
//PrintNode("cx->inherit 2 ", cx->inherit);
				rval = DoInherit(cx, MkList(mka("unify"), 
						md->Car()->Cdr()->Car(),
						goalscar),
					(List*)Module);
				cx->inherit = cx->inherit->Cdr();
//PrintNode("cx->inherit 3 ", cx->inherit);
//printf("rval %d \n", rval);
				if (rval >= 0) {
					goto RETUNIFY;
				}
			}
//			md = md->Cdr();
		} else {
//PrintNode("name->Car() ", name->Car());
//PrintNode("goalscar->Car() ", goalscar->Car());
			if (ModuleCompare(name->Car(), goalscar->Car()) == 0) {
				break;
			}
		}
		md = md->Cdr();
	}

	if (md->kind() != LIST) {
#if 0
	    if (TraceFlag && (undeclareflag == 0)) {
	    	PrintNode("Undeclared predicate : ", goalscar);
	    }
#endif
//printf("Unify md==Nil call PopStack \n");
	    if (PopStack(cx, goals, md, cx->env)) {
		if (TraceFlag) {
			PrintNode("*** back track ***2 ", goals->Car());
		}
//PrintNode("backtrack 2 goals ", goals);
		if (goals->Car()->Eq(mka("x"))) {
			xex(cx, goals->Cdr(), module);
		}

		level = 0;
		goalscar = GetLeftNode(goals, goalscdr, level);
		rval = -1;	// unknown
		goto RETUNIFY;
	    } else {
		return -1;	// unknown
	    }
	}

	bd = Dup(md->Car());
	cx->env = Nil->Cons(Nil);

	level = 0;
	goalscar = GetLeftNode(goals, goalscdr, level);
	if (TraceFlag) {
		PrintNode("Unification: ", goalscar->Val());
		PrintNode("           : ", bd->Car()->Val());
	}
//PrintNode("unify goals ", goals);
//PrintNode("unify goalscar ", goalscar);
//PrintNode("unify goalscdr ", goalscdr);

	cxpush(cx, bd);
	cxpush(cx, goalscar);
	cxpush(cx, goalscdr);

	if (Unification(goalscar->Val(), bd->Car(), cx->env, cx)) {
	    if (TraceFlag) {
		PrintNode("Result     > ", bd->Car()->Val(), "...success");
	    }

	    cxpop(cx);
	    cxpop(cx);
	    cxpop(cx);

	    // Call Unify
	    PushStack(cx, goals, md, cx->env);
	    goals = Append(MkList(bd->Cdr()), goalscdr);

	    GC(goals);

	    goto CALLUNIFY;

	} else {
//PrintNode("           > ", bd->Val(), "...fail");
	    cxpop(cx);
	    cxpop(cx);
	    cxpop(cx);

	    // When Unification fails, it skips to SKIPRET. 
	    goto SKIPRET;
	}


RETUNIFY:
	if (rval>0) {
//printf("unify return rval %d\n", rval);
		PushStack(cx, Nil, Nil, cx->env);
		return rval;
	} else if (rval == 0) {
		return rval;
	}

SKIPRET:

//PrintNode("UnsetEnv(cx->env)1 ", cx->env);

	UnsetEnv(cx->env);

//PrintNode("UnsetEnv(cx->env)2 ", cx->env);

	md = md->Cdr();

	if (md->kind() != LIST) {

//printf("Unify md==Nil 2 call PopStack \n");
	    if (PopStack(cx, goals, md, cx->env)) {
		if (TraceFlag) {
			PrintNode("*** back track ***3 ", goals->Car());
		}
//PrintNode("backtrack 3 goals ", goals);
		if (goals->Car()->Eq(mka("x"))) {
			xex(cx, goals->Cdr(), module);
		}
		
		level = 0;
		goalscar = GetLeftNode(goals, goalscdr, level);
		rval = -1;	// unknown
		goto RETUNIFY;
	    } else {
		return -1;	// unknown
	    }
	}

    }

//printf("Unify False call PopStack \n");
    if (PopStack(cx, goals, md, cx->env)) {
	if (TraceFlag) {
		PrintNode("*** back track ***4 ", goals->Car());
	}
//PrintNode("backtrack 4 goals ", goals);
	if (goals->Car()->Eq(mka("x"))) {
		xex(cx, goals->Cdr(), module);
	}
	
	level = 0;
	goalscar = GetLeftNode(goals, goalscdr, level);
	rval = -1;
	goto RETUNIFY;
    } else {
	return -1;
    }

    {
	syserr("Not PRED ");
	goalscar->Val()->print();
	printf("\n");
	printf("kind %d \n", goalscar->Val()->kind());
	return 0;
    }
}

