:- include(library(pfc_header_3_0)).

% -*-Prolog-*-

skCheck(eq(_,_),[]) :- !.

skCheck(P,Rules) :-
  sk(P,L),
  bagof(Rule,
        S^(member(S,L),
           skNoticer(P,S,Rule)),
        Rules).
         
% L is a list of the skolem constants found in the term P.
sk(P,L) :- sk1(P,[],L).

sk1(P,L,[P|L]) :- 
  skolemConstant(P),
  !,
  \+member(P,L),
  !.

sk1(P,L,L) :- 
  skolemConstant(P),
  !.

sk1(P,L,L) :- atomic(P),!.

sk1([Head|Tail], Lin, Lout) :-
  !,
  sk1(Head,Lin,Ltemp),
  sk1(Tail,Ltemp,Lout).

sk1(P,Lin,Lout) :-
  P =.. Plist,
  sk1(Plist,Lin,Lout).

% a skolem constant is any term sk/1.
skolemConstant(sk(_)).


% make a Pfc rule to add new facts based on equality info about skolem terms.
skNoticer(P,Sk,(eq(Sk,X)==>P2)) :- termSubst(Sk,X,P,P2).
  

% list Lisp's subst, but for terms.

termSubst(Old,New,Old,New) :- !.

termSubst(_,_,Term,Term) :- atomic(Term),!.

termSubst(Old,New,[Head|Tail],[Head2|Tail2]) :- 
  !,
  termSubst(Old,New,Head,Head2),
  termSubst(Old,New,Tail,Tail2).

termSubst(Old,New,Term,Term2) :-
  Term =.. TermList,
  termSubst(Old,New,TermList,TermList2),
  Term2 =.. TermList2.

%:- add((P/(\+P=eq(_,_)) ==> {skCheck(P,Rules)}, Rules)).
:- add((P ==> {skCheck(P,Rules)}, Rules)).

:- add((eq(X,Y) <==> eq(Y,X))).