% Written Jan. 22nd 2005 by Markus Triska (triska@gmx.at)
% Public domain code.

/* - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
   structures used:

   variable:  var(V,I)   (V: name, I: index, facilitates renaming)
   term:      var(V,I) or term(F,Ts) (F: function symbol, Ts: list of subterms)
   substitution: list of (var(_,_),T) terms
   rewriting system: list of (L,R) terms
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - */

indomain(Var,Subst) :- memberchk((Var,_), Subst).

% apply subsitution to a variable

app([(Var,T)|Ss], V, S) :-
	(Var == V ->
		S = T
	;
		app(Ss,V,S)
	).

% homeomorphic extension to terms & substitutions

lift(Subst, var(V,I), R) :- !,
	( indomain(var(V,I), Subst) ->
		app(Subst, var(V,I), R)
	;
		R = var(V,I)
	).
lift(Subst, term(F,Ts), term(F,Rs)) :- !,
	maplist(lift(Subst), Ts, Rs).
lift(Subst, (A0,B0), (A,B)) :- !,
	lift(Subst, A0, A),
	lift(Subst, B0, B).


occurs(var(X,I), var(X,I)) :- !.
occurs(V, term(_F,Ts)) :-
	member(T, Ts),
	occurs(V, T).

zip([], [], []).
zip([A|As], [B|Bs], [(A,B)|Cs]) :-
	zip(As, Bs, Cs).

% compute MGU

solve([], Comp, Comp).
solve([(var(X,I),T)|Ss], Comp, Rs) :- !,
	( var(X,I) == T ->
		solve(Ss, Comp, Rs)
	;
		elim(var(X,I), T, Ss, Comp, Rs)
	).
solve([(T,var(X,I))|Ss], Comp, Rs) :- !,
	T = term(_,_),
	elim(var(X,I), T, Ss, Comp, Rs).
solve([(term(F,Ts),term(G,Us))|Ss], Comp, Rs) :- !,
	F == G,
	zip(Ts, Us, Zs),
	append(Zs, Ss, Ss1),
	solve(Ss1, Comp, Rs).

elim(X, T, Ss, Comp, Rs) :-
	(occurs(X, T) ->
		format("\noccurs-check!"),
		fail
	;
		Goal = lift([(X,T)]),
		maplist(Goal, Ss, Ss1),
		maplist(Goal, Comp, Comp1),
		solve(Ss1, [(X,T)|Comp1], Rs)
	).


unify(T1, T2, Subst) :-
	solve([(T1,T2)], [], Subst).


% matching

matchs([], Comp, Comp).
matchs([(var(X,I),T)|Ss], Comp, Rs) :- !,
	( indomain(var(X,I) ,Comp) ->
		app(Comp, var(X,I), T),
		matchs(Ss, Comp, Rs)
	;
		matchs(Ss, [(var(X,I),T)|Comp], Rs)
	).
matchs([(term(F,Ts),term(G,Us))|Ss], Comp, Rs) :- !,
	F == G,
	zip(Ts, Us, Zs),
	append(Zs, Ss, Ss1),
	matchs(Ss1, Comp, Rs).

match(Pat, Obj, Rs) :-
	matchs([(Pat,Obj)], [], Rs).

% perform one rewriting step using the first matching rule

rewrite([], T, norm(T)).
rewrite([(L,R)|Rs], T, Rewr) :-
	( match(L, T, Subst) ->
		lift(Subst, R, Rewr)
	;
		rewrite(Rs, T, Rewr)
	).

% reduce to normal form - may not terminate!
% for example R = { a -> a, f(x) -> b }, although f(a) does have a normal form!

norm(_, var(X,I), var(X,I)) :- !.
norm(R, term(F,Ts), N) :-
	maplist(norm(R), Ts, Ts1),
	U = term(F,Ts1),
	rewrite(R, U, Urewr),
	( Urewr = norm(_) ->
		Urewr = norm(N)
	;
		norm(R, Urewr, N)
	).


rename(N, var(X,I), var(X,I1)) :- !,
	I1 is I + N.
rename(N, term(F,Ts), term(F,Ts1)) :-
	maplist(rename(N), Ts, Ts1).



maxs(Is, M) :-
	maxs(Is, 0, M).

maxs([], M, M).
maxs([I|Is], M0, M) :-
	M1 is max(I, M0),
	maxs(Is, M1, M).


maxindex(var(_,I), I).
maxindex(term(_,Ts), M) :-
	maplist(maxindex, Ts, Ms),
	maxs(Ms, M).


% concat(map (CP C (T(f,ts),r)) R ) @ (innercps C (f,[],ts,r))


% compute critical pairs

cp(C, (T,R), (L2,R2), Ls) :-
	( unify(T, L2, Sigma) ->
		lift(Sigma, R, SigmaR),
		capply(C, R2, CR2),
		lift(Sigma, CR2, SigmaCR2),
		Ls = [(SigmaR,SigmaCR2)]
	;
		Ls = []
	).


cps(_, (var(_,_),_), _, []) :- !.
cps(C, (term(F,Ts),R), Rules, Ls) :-
	maplist(cp(C,(term(F,Ts),R)), Rules, Ls1),
	flatten(Ls1, Ls2),
	innercps(C, (F,[],Ts,R), Rules, Ls3),
	append(Ls2, Ls3, Ls).


% Cf s = C(T(f,ts0 @ [s] @ ts1))

capply(func(Head,Body,Result), Arg, R1) :-
	copy_term((Head,Body,Result), (H1,B1,R1)),
	Arg = H1,
	call(B1).


innercps(_, (_ ,_ , [], _), _Rules, []) :- !.
innercps(C, (F, Ts0, [T|Ts1], R), Rules, Ls) :-
	Cf = func(S, (append(Ts0,[S|Ts1],Ts01),capply(C,term(F,Ts01),CResult)), CResult),
	cps(Cf, (T,R), Rules, Ls0),
	append(Ts0, [T], NTs0),
	innercps(C, (F,NTs0,Ts1,R), Rules, Ls1),
	append(Ls0, Ls1, Ls).

tomaxindex((L,R), M) :-
	maxindex(L, ML),
	maxindex(R, MR),
	M is max(ML, MR).

cps(Rules, (L,R), CPs) :-
	maplist(tomaxindex, Rules, Maxindices),
	maxs(Maxindices, M0),
	M is M0 + 1,
	rename(M, L, RL),
	rename(M, R, RR),
	cps(func(S,true,S), (RL, RR), Rules, CPs).


criticalPairs2(R1, R2, CPs) :-
	maplist(cps(R1), R2, CPs1),
	flatten(CPs1, CPs).

criticalPairs(R, CPs) :-
	criticalPairs2(R, R, CPs).


% testing:
rules(Rules) :-
	L = term(f,[term(f,[var(x,1)])]),
	R = term(g,[var(x,1)]),
	Rules = [(L,R)].
rules(Rules) :-
	Ls = [term(f,[term(f,[var(x,1)])]), term(g,[term(g,[var(x,1)])])],
	Rs = [term(f,[var(x,1)]), term(f,[var(x,1)])],
	zip(Ls, Rs, Rules).

c(CPs) :-
	rules(Rules),
	criticalPairs(Rules, CPs).
% end testing


ord(_, F1, F1, eq) :- !.
ord(Ord, F1, F2, Stat) :-
	nth0(F1, Ord, N1),
	nth0(F2, Ord, N2),
	( N1 < N2 ->
		Stat = gr
	;
		Stat = nge
	).


% not finished
%lex(_,[],[],eq) :-
%lex(Ord,[X|Xs],[Y|Ys],O) :-
%	ord(Ord,X,Y,O1),
%	( O1 = eq ->
%		lex(Ord,Xs,Ys,O)
%	)