:- module(analyse,[ technique/3, schema/2,
		    recursive_case/4, predicate_clauses/3]).
:- use_module(normalform).

%=technique(?Argumentstelle,?Technique,+NormalisierteKlausel)
technique(N,becomes(X,Y),Head-Calls):-
	functor(Head,Functor,Arity),
	functor(Call,Functor,Arity),
	member(Call,Calls),
	arg(N,Head,X),
	arg(N,Call,Y).
technique(N,same(X),Clause):-
	technique(N,becomes(X,X),Clause).
technique(N,list_uncons(A,X),Clause):-
	technique(N,becomes([A|X],X),Clause).
technique(N,list_cons(A,X),Clause):-
	technique(N,becomes(X,[A|X]),Clause).

recursive_case(Head-NBody,Before,Call,After):-
	functor(Head,Functor,N),
	functor(Call,Functor,N),
	append(Before,[Call|After],NBody).
predicate_clauses(_,[],[]).
predicate_clauses(Functor/Arity,[Head-Body|Rest],[Head-Body|Rest1]):-
	functor(Head,Functor,Arity),
	predicate_clauses(Functor/Arity,Rest,Rest1).
predicate_clauses(Functor/Arity,[Head-_|Rest],Rest1):-
	predicate_clauses(Functor/Arity,Rest,Rest1),
	not(functor(Head,Functor,Arity)).
	

%=schema(?Schema,+NKM)
schema(basecase(X),Pred):-
	member(X-[],Pred).
schema(recursion(Head,Call),Pred):-
	member(Head-NBody,Pred),
	recursive_case(Head-NBody,_,Call,_).

schema(list_recursion(Rec),Pred):-
	schema(basecase(Base),Pred),
	arg(Rec,Base,[]),
	schema(recursion(Head,Call),Pred),
	arg(Rec,Head,[_|Rest]),
	arg(Rec,Call,Rest).

schema(accu(Accu,Return),Pred):-
	schema(recursion(Head0,Call0),Pred),
	arg(Return,Head0,RetVar0),
	arg(Return,Call0,RetVar0),
	schema(basecase(Base0),Pred),
	arg(Accu,Base0,AccuVar0),
	arg(Return,Base0,AccuVar0),
	Accu\=Return,
	forall(schema(basecase(BaseCase),Pred),
	       (arg(Accu,BaseCase,AccuVar),
		arg(Return,BaseCase,AccuVar))),
	forall(schema(recursion(Head,Call),Pred),
	       (arg(Return,Head,RetVar),
		arg(Return,Call,RetVar))).


test(1,[rev([],X,X)-[],
	rev([A|X],Y,Z)-[rev(Z,[A|Y],Z)]
       ]):-
	replaceVars(['A'=A,'X'=X,'Y'=Y,'Z'=Z]).