% Propositional TR syntax
% The predicate wff(+Term, -S) accepts as input a CTR term, "Term". 
% It returns in "S"  the correspondent function term.
% E.g.: ?- read(X), wff(X, S).
%       a # (b * c) # d.
%
%       X = a # (b * c) # d. 
%       S = conc([a,seq([b,c]),d]).
%       yes
%

:- export wff/2.

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

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

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).

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

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(_, '.') :- !.

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('*', seq(L1), seq(L2), seq([seq(L1), seq(L2)])) :- !. 
%mkTerm('#', conc(L1), conc(L2), conc([conc(L1), conc(L2)])) :- !. 
%mkTerm('\/', or(L1), or(L2), or([or(L1), or(L2)])) :- !. 

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)) :- !.

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