/*
 Copyright (C) 1988,2005, Shinji Kono 
 Everyone is permitted to copy and distribute verbatim copies
 of this license, but changing it is not allowed.  You can also
 use this wording to make the terms for other programs.

 send your comments to kono@ie.u-ryukyu.ac.jp
*/

 
/* 
	temporal unifier
					Tue Oct 15 11:36:12 JST 1985
*/

unifyAll(V,V) :- !.				% variable case
unifyAll('$t'(Now,Nxt),'$t'(Now,Nxt1)) :-!,
	unifyAll(Nxt,Nxt1).
unifyAll('$t'(Now,Nxt),D):-!,
	unifyNowNext(D,Now,Nxt1),
	unifyAll(Nxt,Nxt1).
unifyAll(D,'$t'(Now,Nxt)):-!,
	unifyNowNext(D,Now,Nxt1),
	unifyAll(Nxt,Nxt1).
unifyAll([H|L],[H1|L1]) :- !,
	unifyAll(H,H1),unifyAll(L,L1).
unifyAll(Sa,Sb):-
	functor(Sa,H,N),functor(Sb,H,N),
	unify_arg(N,N,Sa,Sb).

unify_arg(0,_N,_,_):-!.
unify_arg(M,N,Sa,Sb):-
	arg(M,Sa,Aa),arg(M,Sb,Ab),
	unifyAll(Aa,Ab),M1 is M-1,!,
	unify_arg(M1,N,Sa,Sb).

unifyNowNext('$t'(Now,Next),Now1,Next1):-!,Now=Now1,Next=Next1.
unifyNowNext(X,X1,X1):-atomic(X),!,X=X1.	
unifyNowNext([H|L],[Hn|Ln],[Hnn|Lnn]):-!,
	unifyNowNext(H,Hn,Hnn),
	unifyNowNext(L,Ln,Lnn).
unifyNowNext(S,Sn,Snn):-
	functor(S,H,N),functor(Sn,H,N),functor(Snn,H,N),
	unifyNowNextArg(N,N,S,Sn,Snn).

unifyNowNextArg(0,_,_,_,_).
unifyNowNextArg(M,N,Sa,Sb,Sc):-
	arg(M,Sa,Aa),arg(M,Sb,Ab),arg(M,Sc,Ac),
	unifyNowNext(Aa,Ab,Ac),M1 is M-1,!,
	unifyNowNextArg(M1,N,Sa,Sb,Sc).

unifyNow(X,X1):-atomic(X),!,X=X1.	
unifyNow('$t'(Now,_),Now1):-!,Now=Now1.
unifyNow([H|L],[Hn|Ln]):-!,
	unifyNow(H,Hn),
	unifyNow(L,Ln).
unifyNow(S,Sn):-
	functor(S,H,N),functor(Sn,H,N),
	unifyNowArg(N,N,S,Sn).

unifyNowArg(0,_,_,_).
unifyNowArg(M,N,Sa,Sb):-
	arg(M,Sa,Aa),arg(M,Sb,Ab),
	unifyNow(Aa,Ab),M1 is M-1,!,
	unifyNowArg(M1,N,Sa,Sb).


unifyNext(X,X):-atomic(X),!.
unifyNext('$t'(_,Next),Next1):-!,Next=Next1.
unifyNext([H|L],[Hn|Ln]):-!,
	unifyNext(H,Hn),
	unifyNext(L,Ln).
unifyNext(S,Sn):-
	functor(S,H,N),functor(Sn,H,N),
	unifyNextArg(N,N,S,Sn).

unifyNextArg(0,_,_,_).
unifyNextArg(M,N,Sa,Sb):-
	arg(M,Sa,Aa),arg(M,Sb,Ab),
	unifyNext(Aa,Ab),M1 is M-1,!,
	unifyNextArg(M1,N,Sa,Sb).


% ATOMIC 
% uatom(X, Atom) 
uatom(X, X) :- !. 
uatom('$t'(Atom,Next), Atom) :- uatom(Next, Atom).
 
uconst(X, X) :- var(X),!. 
uconst('$t'(Atom,Next), Atom) :- uatom(Next, Atom).
uconst(X, Y) :- nonvar(X),!,X=Y. 
 
% unil(X) : Hacked version of uatom. 
unil([]) :- !. 
unil('$t'([],Next)) :- unil(Next).
 
 
% COMPOUND TERM 
% uskel(X, Skeleton) 
uskel(X,X) :- !. 
uskel('$t'(X,Next),S) :- 
    functor(S,H,N),functor(X,H,N),functor(Sn,H,N),
    uskelArg(N,N,S,X,Sn),
    uskel(Next,Sn).
 
uskelArg(0, _, _, _, _) :- !.
uskelArg(M, N, S, X, Sn) :-
    arg(M, S, '$t'(Now, Next)),
    arg(M, X, Now),
    arg(M, Sn, Next),
    M1 is M-1,
    uskelArg(M1, N, S, X, Sn).

% ulist(X, Car, Cdr) : Hacked version of uskel. 
ulist([H|T], H, T) :- !. 
ulist('$t'([H|T],Next), '$t'(H,NH), '$t'(T,NT)) :- !, ulist(Next, NH, NT).


% readonly unify


r_unifyAll(G,D):-
	(var(G) ; var(D)),!,G==D.
r_unifyAll(Fl,D):-functor(Fl,'$t',2),!,
	r_unify_flt(Fl,D).
r_unifyAll(D,Fl):-functor(Fl,'$t',2),!,
	r_unify_flt(Fl,D).
r_unifyAll(Sa,Sb):-
	functor(Sa,H,N),functor(Sb,H,N),
	r_unify_arg(N,N,Sa,Sb).

r_unify_arg(0,_N,_,_):-!.
r_unify_arg(M,N,Sa,Sb):-
	arg(M,Sa,Aa),arg(M,Sb,Ab),
	r_unifyAll(Aa,Ab),M1 is M-1,!,
	r_unify_arg(M1,N,Sa,Sb).

r_unify_flt('$t'(Now,Nxt),'$t'(Now1,Nxt1)) :-!,Now==Now1,
	r_unifyAll(Nxt,Nxt1).
r_unify_flt('$t'(Now,Nxt),S) :- nonvar(Now),nonvar(Nxt),
	r_unifyNowNext(S,Now,Nxt1),
	r_unifyAll(Nxt,Nxt1).

r_unifyNowNext(V,_,_) :- var(V),!,fail.
r_unifyNowNext('$t'(Now,Next),Now1,Next1):-!,Now==Now1,Next==Next1.
r_unifyNowNext(X,X1,X2):-atomic(X),!,X==X1,X==X2.	
r_unifyNowNext(S,Sn,Snn):-
	functor(S,H,N),functor(Sn,H,N),functor(Snn,H,N),
	r_unifyNowNext(N,N,S,Sn,Snn).

r_unifyNowNextArg(0,_,_,_,_).
r_unifyNowNextArg(M,N,Sa,Sb,Sc):-
	arg(M,Sa,Aa),arg(M,Sb,Ab),arg(M,Sc,Ac),
	r_unifyNowNext(Aa,Ab,Ac),M1 is M-1,!,
	r_unifyNowNextArg(M1,N,Sa,Sb,Sc).

 
/* end of unifier */