/*****************************/
/* Christian Ohlsson         */
/* Logik för dataloger       */
/* Karlstad 990228           */
/* Laboration 2 i Logik      */
/*****************************/
/* Functions included        */
/* free_in                   */
/* rename_var                */
/*****************************/

:- op(200, fx, -).
:- op(400, xfy, #).
:- op(400, xfy, &).
:- op(700, xfy, ->).
:- op(700, xfy, <->).

exist(X, [H|T]) :- X = H, !, fail.
exist(X, [H|T]) :- Z =.. T, free_in(X, Z).

all(X, [H|T]) :- X = H, !, fail.
all(X, [H|T]) :- Z =.. T, free_in(X, Z).

operators(X, [H|T]) :- free_in(X, H), Z =.. T, free_in(X, Z).
falsum(X) :- true.

/* Del 1 - free_in */
/* free_in(+variabel, +TermOrFormula */
free_in(X, Y) :- Y =.. [H|T], T = [].

free_in(X, Y) :- Y =.. [H|T], member(H, [&, #, ->, <->]), operators(X, T).
free_in(X, Y) :- Y =.. [H|T], member(H, [all, exist]), call(H, X, T).
free_in(X, Y) :- Y =.. [H|T], member(H, [-]), falsum(X).
free_in(X, Y) :- Y =.. [H|T], member(H, [as, pr, fu, qu, rt]).

/* Del 2 - rename_var  */
/* rename_var(+Element, +TermOrFormula, +Nyttelement, -NyTermOrFormula) */
ersatt(E1, E2, [], []).
ersatt(E1, E2, [E1|R], [E2|S]) :- ersatt(E1, E2, R, S).
ersatt(E1, E2, [X|R], [X|S]) :- ersatt(E1, E2, R, S).


rv(E1, E2, [H|T], New) :- T = [], atom(H), ersatt(E1, E2, [H], New).
rv(E1, E2, [H|T], New) :- T = [], rename_var(E1, H, E2, Next), append([Next], [], New).
rv(E1, E2, [H|T], New) :- rv(E1, E2, T, N1), rv(E1, E2, [H], N2), append(N2,N1, New).
rename_var(E1, Old, E2, New) :- Old =.. [H|T], T = [], ersatt(E1, E2, [H], Z), New =.. Z. 
rename_var(E1, Old, E2, New) :- Old =.. [H|T], rv(E1, E2, T, Next), New =.. [H|Next].