:- module(substitute,[subst/3,free/2,assignment/3]).
:- use_module(signature,[fovar/1,newvar/1,newconst/1]). %const/1
:- [comsemOperators].

assignment([],_Constants,[]).

assignment([V|Vars],Constants,[V:C|RestAssignment]) :-
	member(C,Constants),
	assignment(Vars,Constants,RestAssignment).

subst(Ass,true(A),true(B)) :- 
	!,subst(Ass,A,B).

subst(Ass,false(A),false(B)) :- 
	!,subst(Ass,A,B).

subst(Ass,~A,~B) :- 
	!,subst(Ass,A,B).

subst(Ass,A&B,C&D) :- 
	!,subst(Ass,A,C),
	subst(Ass,B,D).


%% exists(X,P):
%% 1. First, check if X is assigned a value. If so remove respective assignment.
%% 2. Then check, if some variable is assigned the value X. Rename accordingly.
%% 3. Substitute on scope.
%%
%% After checking (1), (2) may still be the case. Therefore, we have to go on with
%% exists(X,Scope) in clause one and can only remove the exists in clause two.

subst(Assignment,exists(X,Scope),Out) :-
	member(X:C,Assignment),
	!,delete(Assignment,X:C,NewAssignment),
        subst(NewAssignment,exists(X,Scope),Out).

subst(Assignment,exists(X,Scope),exists(Y,OutScope)) :-
        captures(Assignment,X),
        !,gensym(fovar,Y),
        subst([Y:X],Scope,RenamedScope),
        subst(Assignment,RenamedScope,OutScope).


% only reached if none of the above conditions holds.
subst(Ass,exists(X,Scope), exists(X,OutScope)) :-
        !,subst(Ass,Scope,OutScope).
	

subst(Assignment,forall(X,Scope),Out) :-
	member(X:C,Assignment),
	!,delete(Assignment,X:C,NewAssignment),
        subst(NewAssignment,forall(X,Scope),Out).

subst(Assignment,exists(X,Scope),forall(Y,OutScope)) :-
        captures(Assignment,X),
        !,gensym(fovar,Y),
        subst([Y:X],Scope,RenamedScope),
        subst(Assignment,RenamedScope,OutScope).

% only reached if none of the above conditions holds.
subst(Ass,forall(X,Scope), forall(X,OutScope)) :-
        !,subst(Ass,Scope,OutScope).


subst(Ass,X,C) :- 
	member(X:C,Ass),!.   % free variable in Dom(Ass)


subst(Ass,In,Out) :-                 % atom or constant/unassigned variable (Args = [])
	In =.. [F|Args],
        substargs(Ass,Args,OutArgs),
        Out =.. [F|OutArgs].



% substargs/3 maps subst/3 over a list.

substargs(_Ass,[],[]).
substargs(Ass,[H1|R1],[H2|R2]) :-
        subst(Ass,H1,H2),
        substargs(Ass,R1,R2).


/* was (less general, doesn't allow for complex terms as substitutes):
substargs(_Ass,[],[]).

substargs(Ass,[A1|R1],[A2|R2]) :-
	member(A1:A2, Ass),!,
        substargs(Ass,R1,R2).

substargs(Ass,[A1|R1],[A1|R2]) :-
        substargs(Ass,R1,R2).
*/

free(Formula,Vars) :-
	findall(V,(fovar(V),freein(V,Formula)),Vs),
	list_to_set(Vs,Vars).


captures([X:C|_],X) :- freein(X,C).
captures([_|R],X) :- captures(R,X).


freein(X,true(A)) :- !,freein(X,A).
freein(X,false(A)) :- !,freein(X,A).
freein(X,~A) :- !,freein(X,A).
freein(X,A&B) :- !,(freein(X,A);freein(X,B)).
freein(X,exists(X,_)) :- !,fail.
freein(X,exists(_,A)) :- !,freein(X,A). % X=Y already covered above.
freein(X,forall(X,_)) :- !,fail.
freein(X,forall(_,A)) :- !,freein(X,A).
% freein(X,A) :- \+ const(X), A =.. [_F|Args], member(X,Args). \+ can't be used for generating
freein(X,A) :- fovar(X), A =.. [_F|Args], member(X,Args).
freein(X,X) :- fovar(X).