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