/*************************************************************************
based on:
         name: comsemLib.pl
      version: July 13, 2001
  description: Term Manipulation, Unification, Printing
      authors: Patrick Blackburn & Johan Bos

deletions and additions:

      version: July, 2002
  description: Helpers
      authors: Stephan Walter, Aljoscha Burchardt
      

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

:- module(comsemLib,
	[compose/3,
	substitute/4,
	printRepresentations/1,
	naonly/2,
	toconj/2,
	hbaseList/2]).

:- ensure_loaded(signature).
:- ensure_loaded(comsemOperators).

/*========================================================================
   Compose predicate argument structure
========================================================================*/

compose(Term,Symbol,ArgList):-
    Term =.. [Symbol|ArgList].


/*========================================================================
   Substitution Predicates
========================================================================*/

substitute(Term,Var,Exp,Result):- 
   Exp==Var, !, Result=Term.
substitute(_Term,_Var,Exp,Result):- 
   \+ compound(Exp), !, Result=Exp.
substitute(Term,Var,Formula,Result):-
   compose(Formula,Functor,[Exp,F]),
   member(Functor,[lambda,forall,exists]), !, 
   (
    Exp==Var, !, 
    Result=Formula
   ; 
    substitute(Term,Var,F,R),
    compose(Result,Functor,[Exp,R])
   ).
substitute(Term,Var,Formula,Result):-
   compose(Formula,Functor,ArgList),
   substituteList(Term,Var,ArgList,ResultList),
   compose(Result,Functor,ResultList).

substituteList(_Term,_Var,[],[]).
substituteList(Term,Var,[Exp|Others],[Result|ResultOthers]):-
   substitute(Term,Var,Exp,Result),
   substituteList(Term,Var,Others,ResultOthers).


/*========================================================================
   Printing a set of representations
========================================================================*/

printRepresentations(Readings):-
   printRep(Readings,0).

printRep([],_):- nl.
printRep([Reading|OtherReadings],M):-
   N is M + 1, nl, write(N), tab(2), 
   \+ \+ (numbervars(Reading,0,_), write(Reading)),
   printRep(OtherReadings,N).


/*========================================================================
   Formula Conversion from full FOL to ~,&,forall 
========================================================================*/
naonly(true(X),true(Z)) :- 
	!,naonly(X,Z).
naonly(false(X),false(Z)) :- 
	!,naonly(false(X),false(Z)).
naonly(~(X),~(Z)) :- 
	!,naonly(X,Z).
naonly(X & Y, Z & W) :- 
	!,naonly(X,Z), 
	naonly(Y,W).
naonly(X v Y,~(~(Z) & ~(W))) :- 
	!,naonly(X,Z), 
	naonly(Y,W).
naonly(X > Y,~(Z & ~(W))) :- 
	!,naonly(X,Z), 
	naonly(Y,W).

naonly(exists(X,S), ~forall(X,~C)) :- 
	!,naonly(S,C).
naonly(forall(X,S), forall(X,C)) :- 
	!,naonly(S,C).
naonly(X,X) :- !.

/*========================================================================
   Make a conjunction out of a list of formulae
========================================================================*/

toconj([X],X).

toconj([X|L],Y&C) :- 
        naonly(X,Y),
        toconj(L,C).


/*========================================================================
   Generate the Herbrand base out of a (signed) model
========================================================================*/

hbaseList(Formulas, HBaseSet) :-
	hbaseListRec(Formulas,HBaseList), 
	list_to_set(HBaseList,HBaseSet),
	length(HBaseSet,L),
	L > 0,!.

% Hbase may not be empty
hbaseList(_,['*']).

hbaseListRec([],[]).

hbaseListRec([Formula|Formulas], HBase) :-
	hbase(Formula, HBase1),
	append(HBase1,HBase2,HBase),
	hbaseListRec(Formulas,HBase2).

hbase(true(A),HBase) :-
	!,hbase(A,HBase).

hbase(false(A),HBase) :-
	!,hbase(A,HBase).

hbase(A&B,HBase) :-
	!,hbase(A,HBase1),
	append(HBase1,HBase2,HBase),
	hbase(B,HBase2).

hbase(~A,HBase) :-
	!,hbase(A,HBase).

hbase(exists(_,S),HBase) :-
	!,hbase(S,HBase).

hbase(forall(_,S),HBase) :-
	!,hbase(S,HBase).

hbase(A,HBase) :-
	A =.. [_|R],
	withoutvars(R,HBase).

withoutvars([],[]).

withoutvars([V|Rest],Rest):-
	fovar(V),!.

withoutvars([V|Rest],[V|WOVRest]):-
	withoutvars(Rest,WOVRest).


/*========================================================================
   Debugging
========================================================================*/

debug(List) :-
	makeFormatString(List,"~n",FS),
	format(FS,List).

makeFormatString([],FS,FS).

makeFormatString([_|T],FS,FSOut) :-
	append(FS,"~w",FSRec),
	makeFormatString(T,FSRec,FSOut).