%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% 
%% skolem functions sort annotation
%% -------------------------------------

%% Author: bernd thomas 
%% E-mail: bthomas@informatik.uni-koblenz.de
%% --------------------------------------------------
%% $Id: skolem.pl,v 1.1 1998/02/10 18:01:01 bthomas Exp $
%% $Log: skolem.pl,v $
%% Revision 1.1  1998/02/10 18:01:01  bthomas
%% Initial revision
%%




%% ==================================================
%% create_skolem_proto(+SkolemList)
%%
%% build skolem prototyps, these are no real
%% protos because sometimes skolemfunctions
%% are not sort annotated
%%

create_skolem_proto(skf([])) :- 
	retract_all(xx_skolem(_)),
	assert(xx_skolem([])), !.
	
create_skolem_proto(skf(SK)) :-
	retract_all(xx_skolem(_)),
	assert(xx_skolem([])),
	c_s_p(SK),!.

c_s_p([]) :- !.
c_s_p([F:S|MF]) :-
	var(S),
	xx_skolem(L),
	append(L,[F:S],NL),
	retract_all(xx_skolem(_)),	
	assert(xx_skolem(NL)),
	c_s_p(MF), !.

c_s_p([F:S|MF]) :-
	check_s_o_s(S,HS),       % expand sort to its full sorts-path
	xx_skolem(L),
	append(L,[F:HS],NL),
	retract_all(xx_skolem(_)),	
	assert(xx_skolem(NL)),
        c_s_p(MF), !.

% ==================================================
% max_close_skolems(+SkolemList,+TermList,-NewTermList)
%
% 1) first we have to find the maximum sort
% annotated skolem function.
% 
% 2) if the term contains skolem functions
% we have to prevent the skolem function to
% annotate a open sorts list. 
% ----------------------------------------

max_close_skolems(SK,Terms,NTerms) :-
	collect_max_skolems(SK,Terms),
	close_skolem_terms(SK,Terms,NTerms),
	!.


% ==================================================
% unify every skolem function contained in 
% the terms with the list of skolem functions
% derived so far. Unification gives us the most
% specified sort path for every skolem list.

collect_max_skolems([],_).
collect_max_skolems(_SK,[]).

% vars
collect_max_skolems(SK,[Term:_Sort|MT]) :-
	var(Term),
	collect_max_skolems(SK,MT).

% preds
collect_max_skolems(SK,[Term|MT]) :-
	nonvar(Term),
	\+ Term = (_F:_S),
	Term =.. [_Functor|Args],
	collect_max_skolems(SK,Args),
	collect_max_skolems(SK,MT).

% skolem
collect_max_skolems(SK,[Term:Sort|MT]) :-
	nonvar(Term),
	Term =.. [Functor|Args],
	member(Functor:Sort,SK),
	collect_max_skolems(SK,Args),
	collect_max_skolems(SK,MT).

% funcs
collect_max_skolems(SK,[Term:_Sort|MT]) :-
	nonvar(Term),
	Term =.. [_Functor|Args],
	collect_max_skolems(SK,Args),
	collect_max_skolems(SK,MT).


% ==================================================
% close_skolem_terms(+SkolemList,Terms,NTerms)
%
% looks like collect_max_skolems BUT works
% different obviuosly ... :-)
% so what the hell does it do? 
%  1) replaces the skolem_functions with none
%     max. sorts specification by the max sort annotation
%  2) closes all open sort-paths of skolem functions
%

close_skolem_terms([],Terms,Terms). %no skolems at all
close_skolem_terms(_,[],[]).        

close_skolem_terms(SK,[Term:Sort|MT],[Term:Sort|NT]) :-
	var(Term),
	close_skolem_terms(SK,MT,NT).

% preds
close_skolem_terms(SK,[Term|MT],[NewTerm|NTerms]) :-
	nonvar(Term),
	\+ Term = (_F:_S),
	Term =.. [Functor|Args],
	close_skolem_terms(SK,Args,NewArgs),
	NewTerm =.. [Functor|NewArgs],
	close_skolem_terms(SK,MT,NTerms).

% skolem
close_skolem_terms(SK,[Term:Sort|MT],[NewTerm:ClosedSort|NTerms]) :-
	nonvar(Term),
	Term =.. [Functor|Args],
	member(Functor:Sort,SK),
	close_list(Sort,ClosedSort),
	close_skolem_terms(SK,Args,NewArgs),
	NewTerm =.. [Functor|NewArgs],
	close_skolem_terms(SK,MT,NTerms).

% funcs
close_skolem_terms(SK,[Term:Sort|MT],[NewTerm:Sort|NTerms]) :-
	nonvar(Term),
	Term =.. [Functor|Args],
	close_skolem_terms(SK,Args,NewArgs),
	NewTerm =.. [Functor|NewArgs],
	close_skolem_terms(SK,MT,NTerms).


% ==================================================
% if the skolemfunc has been used before
% we collect the most specific skolemfunc
% by unification (member...)
calc_unique_skolem(SK) :-
	xx_mgu_sk(SKOLEMLIST),
	member(SK,SKOLEMLIST),
	retract_all(xx_mgu_sk(_)),
	assert(xx_mgu_sk(SKOLEMLIST)).

% first appearance of the skolemfunc
% then we append it to the list of skolemfuncs
calc_unique_skolem(SK) :-
	xx_mgu_sk(SKOLEMLIST),
	append(SKOLEMLIST,[SK],NSKOLEMLIST),
	retract(xx_mgu_sk(SKOLEMLIST)),
	assert(xx_mgu_sk(NSKOLEMLIST)).
   
% ==================================================
% skolem functions are not know by the specification
% so we have to treat them in a special way. We have
% to recognize a term as a skolemfunction and we have
% to check its right sort annotation and collect the
% sort annotations, that may have been generated by
% unification with prototyps during run time so far.
%

% A skolem function, that is extended sort annotated already
% e.g. sort list
check_skolem(Term:Sort,NTerm:Sort) :- 
  	nonvar(Term),
	Sort = [_|_],
	Term =.. [Functor|SArgs],
	xx_skolem(SKOLEM),
	member((Functor:_ProtoSort),SKOLEM), % now we know it's a skolem
	!,
        calc_unique_skolem(Functor:Sort),
	skolem_args(SArgs,NArgs),
	NTerm =.. [Functor|NArgs].

% A skolem function, with variable sort 
% e.g. Var 
check_skolem(Term:Sort,NTerm:ProtoSort) :- 
  	nonvar(Term),
	var(Sort),
	Term =.. [Functor|SArgs],
	xx_skolem(SKOLEM),
	member((Functor:ProtoSort),SKOLEM), % now we know it's a skolem
	!,
        calc_unique_skolem(Functor:ProtoSort),
	skolem_args(SArgs,NArgs),
	NTerm =.. [Functor|NArgs].

% A skolem function, with no sort 
% 
check_skolem(Term,NTerm:ProtoSort) :- 
  	nonvar(Term),
	\+ Term = (_F:_S),
	Term =.. [Functor|SArgs],
	xx_skolem(SKOLEM),
	member((Functor:ProtoSort),SKOLEM), % now we know it's a skolem
	!,
        calc_unique_skolem(Functor:ProtoSort),
	skolem_args(SArgs,NArgs),
	NTerm =.. [Functor|NArgs].

skolem_args([],[]).
skolem_args([A:S|MoreArgs],[A:Hierachy|SortedArgs]) :-
    check_s_o_s(S,Hierachy),
    skolem_args(MoreArgs,SortedArgs).