/*************************************************************************

         name: cllsLib.pl
      version: March 13, 2002
  description: Additional predicates for working with clls USRs
      authors: Stephan Walter, Aljoscha Burchardt
 
*************************************************************************/

:- module(cllsLib,[mergeUSR/2,usr2LambdaList/2,idom/3,root/2,hasCycle/1,reachable/3]).
		
:- ensure_loaded(comsemOperators).

:- use_module(comsemLib,[compose/3]).
:- use_module(signature,[newvar/1]).

/*========================================================================
   Merge for Underspecified Semantic Representations
========================================================================*/

mergeUSR(usr(N,L,D,B),usr(N,L,D,B)).

mergeUSR(merge(U1,U2),usr(N3,L3,D3,B3)):-
   mergeUSR(U1,usr(N1,L1,D1,B1)),
   mergeUSR(U2,usr(N2,L2,D2,B2)),
   append(N1,N2,N3),
   append(L1,L2,L3),
   append(D1,D2,D3),
   append(B1,B2,B3).


/*========================================================================
   Constraint Tree Predicats
========================================================================*/

%% The root node

% a root node has no incoming edges 
% (is not dominated by anyone)
root(Root,Usr) :-
	Usr = usr(Ns,_,_,_),
	member(Root,Ns),
	\+ dom(_,Root,Usr).

%% Dominance

% X immediately dominates Y via a dominance constraint
cdom(X,Y,Usr) :-
	Usr =  usr(_,_,DCs,_),
	member(dom(X,Y),DCs).

% X is Ys father
idom(X,Y,Usr) :-
	Usr = usr(_,LCs,_,_),
	member(X:Label,LCs),
	compose(Label,_,Args),
	member(Y,Args).

% X dominates Y by a constraint or is Y's father
dom(X,Y,Usr) :- cdom(X,Y,Usr).
dom(X,Y,Usr) :- idom(X,Y,Usr).

%% Reachability

% N1 is reachable from N2 if N2 dominates N1 or
reachable(N1,N2,Usr) :- 
	dom(N2,N1,Usr),!.

% if there is a node N3 that is dominates N1 and 
% N3 can be reached from N2
reachable(N1,N2,Usr) :-
	dom(N3,N1,Usr),
	reachable(N3,N2,Usr).


%% Test for Cycles

% if there are nodes, but there is no root node,
% there must be a cycle
hasCycle(Usr) :-
	Usr = usr(Ns,_,_,_),
	length(Ns,Length),
	Length > 0,
	\+ root(_,Usr).

% if there is a root node,
% look for cycles from the root node upwards
hasCycle(Usr) :-
	root(Root,Usr),
	hasCycleRec(Root,[],Usr).

% if a node is reached the second time, the Usr has a cycle
hasCycleRec(N,SoFar,_) :-
	member(N,SoFar). 

hasCycleRec(N,SoFar,Usr) :-	
	reachable(N2,N,Usr),
	hasCycleRec(N2,[N|SoFar],Usr).


/*========================================================================
  Translation of Solved Underspecified Representations to Lambda Terms
========================================================================*/

usr2LambdaList([],_).

usr2LambdaList([Usr|Usrs],[LT1|LTs]) :-
	usr2Lambda(Usr,LT1),
	usr2LambdaList(Usrs,LTs).

% translate from from root node upwards	
usr2Lambda(Usr,LT) :-
	root(Root,Usr),
	translate(Root,LT,[],Usr).


% binary operators: @, & ,v,>,< >: recursive translation of both children
translate(N,OutTerm,Bindings,Usr) :-
	Usr = usr(_,LCs,_,_),
	member(N:Term,LCs),
	compose(Term,Functor,[N1,N2]),
	member(Functor,['@','&','v','>','< >']),
	translate(N1,LT1,Bindings,Usr),
	translate(N2,LT2,Bindings,Usr),
	compose(OutTerm,Functor,[LT1,LT2]).


% N is labled Binder(N1), introduce new Var,
% add the binding N:Var to Bindings
% continue translation at node N1
translate(N,OutTerm,Bindings,Usr) :-
	Usr = usr(_,LCs,_,_),
	member(N:Term,LCs),
	compose(Term,Functor,[N1]),
	member(Functor,[lambda,exists,forall]),
	newvar(NewVar),
	translate(N1,LT,[N:NewVar|Bindings],Usr),
	compose(OutTerm,Functor,[NewVar,LT]). 


% var translates to a variable according to Bindings
translate(N,Var,Bindings,Usr) :-
	Usr = usr(_,LCs,_,BCs),
	member(N:var,LCs),
	member(bind(N,BinderNode),BCs),
	member(BinderNode:Var,Bindings).


% dom(N1,N2): continue translation at N2
translate(N1,LT,Bindings,Usr) :-
	Usr = usr(_,_,DCs,_),
	member(dom(N1,N2),DCs),
	translate(N2,LT,Bindings,Usr).
	

% basic case: labled nodes translate to the label
translate(N,Label,_,Usr) :-
	Usr = usr(_,LCs,_,_),
	member(N:Label,LCs).