%
%     This file contains the source code that parses the CTR 
%      terms and translates them into Prolog formulas.
%

:- export wff/2.

 
% The CTR operators are defined with their corresponding
% precedence classes and position specifiers.
%

:- op(610, xfy, '#').
:- op(605, xfy, '*').
:- op(600, fx, 'o').
:- op(600, fx, 'o1').


% The initial term is translated into a list that
% is processed recursively based on its operator type.
%

wff(Term, S) :-
   Term =.. L,
   t_wff(t, L, S).

 
% The predicate "t_wff" is called recursively to translate
% the list. It decomposes the list to the lowest level
% possible, when its argument is an atomic term. Next, the
% predicate "mkterm" is called to rebuild the translated formula.
%
% The predicate "t_wff" is defined for binary operators,
% such as * and #.
%

t_wff(F, [Op, I1, I2], Term) :-
   op(F, Op), !,
   I1=..NI1,
   (not(NI1 = [OI1,_,_])
    ;
    NI1 = [OI1,_,_],
    not(Op = OI1)),
   (is_list(I1), !,
    t_wff(F, I1, O1)
    ;
    t_wff(F, NI1, O1)),
   I2=..NI2,
   (is_list(I2),! ,
    t_wff(F, I2, O2)
    ;
    t_wff(F, NI2, O2)),
   mkTerm(Op, O1, O2, Term).

 
% To translate terms containing unary operators, the following
% definition of "t_wff" is executed.
%

t_wff(F, [Op, I], Term) :-
   op(F, Op), !,
   I=..NI,
   t_wff(F, NI, O),
   mkTerm(Op, O, Term).

 
% The predicate t_wff is also defined for atomic terms.
%

t_wff(_, A, A) :- atomic(A), !.
t_wff(_, [A], A) :- atomic(A), !.
t_wff(_, [A], LS) :- !,
                     A =..A1,
                     t_wff(t, A1, B),
                     LS = [B].
t_wff(_, [L|X], F) :- F =.. [L|X], !.
t_wff(_, [., I1, []], ff(O1)) :- !,
   I1=..NI1,
   t_wff(b, NI1, O1).

op(_, '#') :- !.
op(_, '*') :- !.
op(_, '\/') :- !.
op(_, 'o') :- !.
op(_, 'o1') :- !.
op(_, '.') :- !.

 
% The predicate "mkterm" is defined recursively to create
% the translated Prolog formula based on the CTR operator.
%

mkTerm('*', [L1], [L2], seq([L1, L2])) :- !.
mkTerm('#', [L1], [L2], conc([L1, L2])) :- !.
mkTerm('\/', [L1], [L2], or([L1, L2])) :- !.

mkTerm('*', [O1], seq(L), seq([O1|L])) :- !.
mkTerm('#', [O1], conc(L), conc([O1|L])) :- !.
mkTerm('\/', [O1], or(L), or([O1|L])) :- !.

mkTerm('*', O1, [L], seq(L1)) :- !, not(is_list(O1)),
                                    append([O1], [L], L1).
mkTerm('#', O1, [L], conc(L1)) :- !, not(is_list(O1)),
                                    append([O1], [L], L1).
mkTerm('\/', O1, [L], or(L1)) :- !, not(is_list(O1)),
                                   append([O1], [L], L1).

mkTerm('*', O1, seq(L), seq([O1|L])) :- !, not(is_list(O1)).
mkTerm('#', O1, conc(L), conc([O1|L])) :- !, not(is_list(O1)).
mkTerm('\/', O1, or(L), or([O1|L])) :- !, not(is_list(O1)).

mkTerm('*', [O1], O2, seq([O1,O2])) :- !,
                                        not(is_list(O2)).
mkTerm('#', [O1], O2, conc([O1,O2])) :- !,
                                        not(is_list(O2)).
mkTerm('\/', [O1], O2, or([O1,O2])) :- !,
                                        not(is_list(O2)).

mkTerm('*', O1, [O2], seq([O1,O2])) :- !,
                                        not(is_list(O1)).
mkTerm('#', O1, [O2], conc([O1,O2])) :- !,
                                        not(is_list(O1)).
mkTerm('\/', O1, [O2], or([O1,O2])) :- !,
                                        not(is_list(O1)).

mkTerm('*', O1, O2, seq([O1,O2])) :- !, not(is_list(O1)),
                                        not(is_list(O2)).
mkTerm('#', O1, O2, conc([O1,O2])) :- !, not(is_list(O1)),
                                        not(is_list(O2)).
mkTerm('\/', O1, O2, or([O1,O2])) :- !, not(is_list(O1)),
                                        not(is_list(O2)).

mkTerm('.', O1, [], O1) :- !.
mkTerm('.', O1, O2, [O1, O2]) :- !.

mkTerm('o', O, isolate(O)) :- !.
mkTerm('o1', O, isolate1(O)) :- !.

 
% To concatenate lists, the predicate "append" is defined in this
% module and it is also called by the other CTR module.
%

append([],L,L).
append([X|L1],L2,[X|L3]) :- append(L1,L2,L3).