/**********************************************************************
% Copyright (C) 1997 Ullrich Hustadt
%                    Max-Planck-Institut fuer Informatik
%                    Im Stadtwald
%                    66123 Saarbruecken, Germany
% Version 1.3 of ftmodal.pl
%
% ftmodal.pl is free software; you can redistribute it and/or modify
% it under the terms of the GNU General Public License as published by
% the Free Software Foundation; either version 1, or (at your option)
% any later version.
%
% ftmodal.pl is distributed in the hope that it will be useful,
% but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
% GNU General Public License for more details.
%
%
% CHANGES
%
% Version 1.3
% Although Version 1.2 ensured the the Goedel number used in the
% skolemisation procedure is unique, the computation and the printing
% of the numbers took to long for some problems. Version 1.3 uses 
% a skolemisation procedure which relies on a history-lookup mechanism 
% to ensure that skolem functions are unique for equivalence classes
% of formulae.
%
% Version 1.2
% Corrected a problem in the skolemisation procedure concerning
% the calculation of Goedel numbers for `some' and `all' modal
% quantifiers.
%
% Version 1.1
% Corrected skolemisation procedure 
**********************************************************************/

:- use_module(library(lists)).

%---------------------------------------------------------------------------
% printTerm(alc2cnfres_fol,+WorldPath,+TERM)
% print term TERM using the functional translation to first-order logic.
% The syntax of the output conforms with the input syntax for first-order
% formulae of CNFRES.
%
printTerm(alc2cnfres_fol,WorldPath,some(R,C)) :-
	gensym(a,C,World),
	append(WorldPath,[[R,World]],NewWorldPath),
	length(WorldPath,WPLength),
	print('(and (nd'), print(R), print('_'), print(WPLength), 
	printTypes(alc2cnfres_fol,typed,WorldPath),
	print(' '),
	printArguments(alc2cnfres_fol,untyped,WorldPath),
	print(') '),
	nl,
	printTerm(alc2cnfres_fol,NewWorldPath,C),
	print(')').
printTerm(alc2cnfres_fol,WorldPath,all(R,C)) :-
	gensym(w,World),
	append(WorldPath,[[R,World]],NewWorldPath),
	length(WorldPath,WPLength),
	print('(all ('), print(World), print(') (impl (nd'),
	print(R), print('_'), print(WPLength), 
	printTypes(alc2cnfres_fol,typed,WorldPath),
	print(' '),
	printArguments(alc2cnfres_fol,untyped,WorldPath),
	print(') '),
	nl,
	printTerm(alc2cnfres_fol,NewWorldPath,C),
	print('))').
printTerm(alc2cnfres_fol,WP,and(L)) :-
	print('(and '),
	printTerms(alc2cnfres_fol,' ',WP,L),
	print(')').
printTerm(alc2cnfres_fol,WP,or(L)) :-
	print('(or '),
	printTerms(alc2cnfres_fol,' ',WP,L),
	print(')').
printTerm(alc2cnfres_fol,WP,not(A)) :-
	print('(not '),
	printTerm(alc2cnfres_fol,WP,A),
	print(')').
%printTerm(alc2cnfres_fol,WP,true) :-
%	print('(true)'),
%	!.
%printTerm(alc2cnfres_fol,WP,false) :-
%	print('(false)'),
%	!.
printTerm(alc2cnfres_fol,WP,A) :-
	atomic(A),
	length(WP,WPL),
	% Ausgabe von (A_WPL
	print('('), print(A), print('_'), print(WPL), 
	% Ausgabe der Typen der Argumente
	printTypes(alc2cnfres_fol,typed,WP), print(' '),
	% Ausgabe der Argumente
	printArguments(alc2cnfres_fol,untyped,WP),
	print(')').
printTerms(alc2cnfres_fol,_Op,WP,[T1]) :-
	printTerm(alc2cnfres_fol,WP,T1).
printTerms(alc2cnfres_fol,Op,WP,[T1,T2|TL]) :-
	printTerm(alc2cnfres_fol,WP,T1),
	print(Op),
	nl,
	printTerms(alc2cnfres_fol,Op,WP,[T2|TL]).
printTypes(alc2cnfres_fol,typed,_L) :-
	!.
printTypes(alc2cnfres_fol,untyped,[]) :-
	!.
printTypes(alc2cnfres_fol,untyped,[T1,T2|TL]) :-
	printTypes(alc2cnfres_fol,untyped,[T1]),
	printTypes(alc2cnfres_fol,untyped,[T2|TL]).
printTypes(alc2cnfres_fol,untyped,[[R,_T]]) :-
	print('_'), print(R),
	!.
printTypes(alc2cnfres_fol,untyped,[T]) :-
	atomic(T),
	print('_'), print(T).
printArguments(alc2cnfres_fol,_Type,[]) :-
	!.
printArguments(alc2cnfres_fol,Type,[[R,T]]) :-
	atomic(T),
	atom_chars(T,[119|_]),
	!,
	% T is a variable
	% Ausgabe als (R T)
	(Type = typed ->
	    print('('), print(R), print(' '), print(T), print(')')
	;
	    print(T)
	).
printArguments(alc2cnfres_fol,Type,[[R,T]]) :-
	atomic(T),
%	atom_chars(T,[97|_]),
	!,
	% T is a constant denoting a successor world
        % Ausgabe als (R (T))
	(Type = typed ->
	    print('('), print(R), print(' ('), print(T), print('))')
	;
	    print('('), print(T), print(')')
	).
printArguments(alc2cnfres_fol,_,[T]) :-
	atomic(T),
%	atom_chars(T,[97|_]),
	!,
	% T is the existentially quantified world a0
	% Ausgabe als (T)
	print('('), print(T), print(')').
printArguments(alc2cnfres_fol,Type,[T1,T2|TL]) :-
	printArguments(alc2cnfres_fol,Type,[T1]),
	print(' '),
	printArguments(alc2cnfres_fol,Type,[T2|TL]).

gensym(Prefix, V) :-
        var(V),
        atomic(Prefix),
        (   retract(gensym_counter(Prefix, M))
        ;   M = 0

        ),
        N is M+1,
        asserta(gensym_counter(Prefix, N)),
        name(Prefix,P1),
        name(N,N1),
        append(P1,N1,V1),
        name(V,V1),
        !.


gensym(Prefix,C1,V) :-
	ac_unique(C1,C2),
	(gensym_symbol(C2,V1) ->
	    V = V1
	;
	    gensym(Prefix,V),
	    assertz(gensym_symbol(C2,V))
	).


ac_unique(C,C) :-
	% If C has been simplified modulo AC, then
        % it is already unique up to AC.
	option(simplify,yes),
	option(ac,yes),
	!.
ac_unique(C1,C2) :-
	ac_unique1(C1,C2).

ac_unique1(C,C) :-
	atomic(C),
	!.
ac_unique1(and(L1),and(L3)) :-
	ac_unique1_list(L1,L2),
	list_to_ord_set(L2,L3),
	!.
ac_unique1(or(L1),or(L3)) :-
	ac_unique1_list(L1,L2),
	list_to_ord_set(L2,L3),
	!.
ac_unique1(all(R,C1),all(R,C2)) :-
	ac_unique1(C1,C2),
	!.
ac_unique1(not(C1),C2) :-
	ac_unique1(C1,C2),
	!.
ac_unique1(some(R,C1),some(R,C2)) :-
	ac_unique1(C1,C2),
	!.
ac_unique1_list([],[]).
ac_unique1_list([L1|LL1],[L2|LL2]) :-
	ac_unique1(L1,L2),
	ac_unique1_list(LL1,LL2),
	!.