%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Mapping between TL and TSQL2.                 %
%                                               %
% Runs with SICStus, Quintus, and SWI-Prolog.   % 
%                                               %
% To start, load this file into Prolog, e.g.,   %
%   prolog                                      %
%   [tl2tsql2].                                 %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- op(900,yfx,[implies]).
:- op(850,yfx,[or]).
:- op(800,yfx,[and, since,until]).
:- op(750,xfy,[:]).
:- op(750,fy,[not,nx,pr,ef,ep,af,ap,exists,forall]).
:- op(700,xfx,[<=,<>]).

is_atom(F) :- functor(F,N,_), \+current_op(_,_,N).

member(H,[H|_]).
member(H,[_|T]) :- member(H,T).

nth([X|_],1,X) :- !.
nth([_|T],N,X) :- N1 is N-1, nth(T,N1,X).

exclude(L1,L2,L) :- findall(X, (member(X,L1),\+member(X,L2)), L).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% normalization of temporal logic formulas %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- op(950,xfx,'==>').

F1 implies F2         ==> not F1 or F2.
forall VL: F          ==> not exists VL: (not F).

not (A and B)         ==> not A or not B.
not (A or B)          ==> not A and not B.
not not F             ==> F.
not T1==T2            ==> T1<>T2.
not T1<T2             ==> T1>=T2.
not T1>T2             ==> T1<=T2.
not T1<=T2            ==> T1>T2.
not T1>=T2            ==> T1<T2.
not T1<>T2            ==> T1==T2.

F1 and (F2 or F3)     ==> F1 and F2 or F1 and F3.
(F1 or F2) and F3     ==> F1 and F3 or F2 and F3.
exists VL: (F1 or F2) ==> exists VL: F1 or exists VL: F2.
F1 since (F2 or F3)   ==> F1 since F2 or F1 since F3.
F1 until (F2 or F3)   ==> F1 until F2 or F1 until F3.
ep (F1 or F2)         ==> ep F1 or ep F2.
ef (F1 or F2)         ==> ef F1 or ef F2.
pr (F1 or F2)         ==> pr F1 or pr F2.
nx (F1 or F2)         ==> nx F1 or nx F2.

%% try(+Form,+VarNr,-Form,-VarNr)
try(var(N),N,var(N),N1) :- !, N1 is N+1.
try(X,N,Y,N) :- X==>Y.
try(X,N,Y,N1) :- X=..[F|Args], try_list(Args,N,NArgs,N1), Y=..[F|NArgs].

%% try_list(+FormList,+VarNr,-FormList,-VarNr)
try_list([X|T],N,[Z|T],N1) :- try(X,N,Z,N1).
try_list([X|T],N,[X|T1],N1) :- try_list(T,N,T1,N1).

%% normalize(+Form,+VarNr,-Form,-VarNr)
normalize(X,N,Y,N2) :- try(X,N,Z,N1), !, normalize(Z,N1,Y,N2).
normalize(X,_,X,_).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% allowedness of temporal logic formulas %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% vars(+Formula,+VarList,?VarList)
vars(var(N),V,V1)        :- !, (member(var(N),V) -> V1=V; V1=[var(N)|V]).
vars(exists VL: A,V,V1)  :- !, vars(A,V,V2), exclude(V2,VL,V1).
vars([H|T],V,V1)         :- !, vars(H,V,V2), vars(T,V2,V1).
vars([],V,V1)            :- !, V=V1.
vars(A,V,V1)             :- A=..[_|L], vars(L,V,V1).

%% alwd(+Formula,+SafeVarList)
alwd(A and B,V)      :- !, alwd(A,V), vars(A,V,V1), alwd(B,V1).
alwd(A or B,_)       :- !, alwd(A,[]), alwd(B,[]), vars(A,[],V), vars(B,[],V).
alwd(not A,V)        :- !, alwd(A,V), vars(A,V,V).
alwd(exists VL: A,V) :- !, exclude(V,VL,V1), alwd(A,V1).
alwd(A since B,_)    :- !, alwd(A,[]), alwd(B,[]).
alwd(A until B,_)    :- !, alwd(A,[]), alwd(B,[]).
alwd(pr A,_)         :- !, alwd(A,[]).
alwd(nx A,_)         :- !, alwd(A,[]).
alwd(ep A,_)         :- !, alwd(A,[]).
alwd(ef A,_)         :- !, alwd(A,[]).
alwd(ap A,_)         :- !, alwd(A,[]).
alwd(af A,_)         :- !, alwd(A,[]).
alwd(T1<T2,V)        :- !, vars(T1,V,V), vars(T2,V,V).
alwd(T1>T2,V)        :- !, vars(T1,V,V), vars(T2,V,V).
alwd(T1<=T2,V)       :- !, vars(T1,V,V), vars(T2,V,V).
alwd(T1>=T2,V)       :- !, vars(T1,V,V), vars(T2,V,V).
alwd(T1<>T2,V)       :- !, vars(T1,V,V), vars(T2,V,V).
alwd(T1==T2,V)       :- !, (vars(T1,V,V); vars(T2,V,V)).
alwd(A,_)            :- is_atom(A), !.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% translation from temporal logic to TSQL2 %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

or_free_part(A or B, OFP) :- !, (or_free_part(A, OFP) ; or_free_part(B, OFP)).
or_free_part(OFP, OFP).

simplify(Q,Q1) :- simplify1(Q,Qx), !, simplify(Qx,Q1).
simplify(Q,Q).

simplify1(vsel([],S,[union([vsel(V1,S1,F1,W1)])-_],[]),vsel(V1,S2,F1,W1)) :- !,
  findall(X, (member(Y,S), (Y=_-(_-C) -> nth(S1,C,X); X=Y)), S2).
simplify1(vsel(V,S,F,W),vsel(V,S,F1,W)) :-
  simplify2(F,F1).

simplify2([R-A|T],[R1-A|T]) :- simplify1(R,R1).
simplify2([R-A|T],[R-A|T1]) :- simplify2(T,T1).

remove(_,[],[]).
remove(QV,[Var-_|S1],S2) :- member(Var,QV), !, remove(QV,S1,S2).
remove(QV,[Var-V|S1],[Var-V|S2]) :- remove(QV,S1,S2).

unify(_-V,_-V,W,W) :- !.
unify(_-V1,_-V2,W,[V2=V1|W]).

trans_expr(var(N),S,var(N)-V,S) :- member(var(N)-V,S), !.
trans_expr(var(N),S,var(N)-V,[var(N)-V|S]) :- !.
trans_expr(E,S,_-E,S).

trans_args([],_,_,S,W,S,W).
trans_args([Arg|T],N,A,S,W,S2,W2) :-
  N1 is N+1,
  trans_args(T,N1,A,S,W,S1,W1),
  trans_expr(Arg,S1,VV,S2),
  unify(VV,_-(A-N),W1,W2).

%% trans_nested_query(+Form,+Alias,-SQL,-Alias,-Sel,-Where)
trans_nested_query(Form,A,SQL,A2,S) :-
  Form=..[Func|Args],
  ((is_atom(Func), trans_args(Args,1,A,[],[],S,[])) ->
     A2 is A+1,
     SQL=Func;
     A1 is A+1,
     trans_query(Form,A1,SQL,A2),
     SQL=union([vsel(_,S,_,_)|_])).

%% add_sel(+Select,+Alias,+ColNumber,+Select,+Where,-Select,-Where)
add_sel([],_,_,S,W,S,W).
add_sel([Var-_|T],A,N,S,W,S2,W2) :-
  trans_expr(Var,S,VV,S1),
  unify(VV,_-(A-N),W,W1),
  N1 is N+1,
  add_sel(T,A,N1,S1,W1,S2,W2).

%% trans_form(+Formula,+Alias&ValidSelectStmt,-Alias&ValidSelectStmt)
trans_form(C since D,A-vsel(V,S,F,W),A5-vsel(V,Sz,
           [union([vsel(VC,Sy,[SQL1-A,SQL2-A2],[C1,C2|Wy])])-A4|F],Wz)) :- !,
  trans_nested_query(C,A,SQL1,A2,S1),
  trans_nested_query(D,A2,SQL2,A4,S2),
  VC=per(lst(bgn(vld(A)),succ(bgn(vld(A2)))),end(vld(A))),
  C1=(lst(bgn(vld(A)),succ(bgn(vld(A2))))<end(vld(A))),
  C2=(end(vld(A2))>=bgn(vld(A))),
  add_sel(S1,A,1,[],[],Sx,Wx),
  add_sel(S2,A2,1,Sx,Wx,Sy,Wy),
  add_sel(Sy,A4,1,S,W,Sz,Wz),
  A5 is A4+1.
trans_form(C until D,A-vsel(V,S,F,W),A5-vsel(V,Sz,
           [union([vsel(VC,Sy,[SQL1-A,SQL2-A2],[C1,C2|Wy])])-A4|F],Wz)) :- !,
  trans_nested_query(C,A,SQL1,A2,S1),
  trans_nested_query(D,A2,SQL2,A4,S2),
  VC=per(bgn(vld(A)),fst(end(vld(A)),pred(end(vld(A2))))),
  C1=(bgn(vld(A))<fst(end(vld(A)),pred(end(vld(A2))))),
  C2=(end(vld(A))>=bgn(vld(A2))),
  add_sel(S1,A,1,[],[],Sx,Wx),
  add_sel(S2,A2,1,Sx,Wx,Sy,Wy),
  add_sel(Sy,A4,1,S,W,Sz,Wz),
  A5 is A4+1.
trans_form(pr C,A-vsel(V,S,F,W),
           A3-vsel(V,S5,[union([vsel(VC,S2,[SQL-A],[])])-A2|F],W5)) :- !,
  trans_nested_query(C,A,SQL,A2,S1),
  VC=succ(vld(A)),
  add_sel(S1,A,1,[],[],S2,[]),
  add_sel(S2,A2,1,S,W,S5,W5),
  A3 is A2+1.
trans_form(nx C,A-vsel(V,S,F,W),
           A3-vsel(V,S5,[union([vsel(VC,S2,[SQL-A],[])])-A2|F],W5)) :- !,
  trans_nested_query(C,A,SQL,A2,S1),
  VC=pred(vld(A)),
  add_sel(S1,A,1,[],[],S2,[]),
  add_sel(S2,A2,1,S,W,S5,W5),
  A3 is A2+1.
trans_form(ep C,A-vsel(V,S,F,W),
           A3-vsel(V,S5,[union([vsel(VC,S2,[SQL-A],[])])-A2|F],W5)) :- !,
  trans_nested_query(C,A,SQL,A2,S1),
  VC=per(succ(bgn(vld(A))),forever),
  add_sel(S1,A,1,[],[],S2,[]),
  add_sel(S2,A2,1,S,W,S5,W5),
  A3 is A2+1.
trans_form(ef C,A-vsel(V,S,F,W),
           A3-vsel(V,S5,[union([vsel(VC,S2,[SQL-A],[])])-A2|F],W5)) :- !,
  trans_nested_query(C,A,SQL,A2,S1),
  VC=per(beginning,pred(end(vld(A)))),
  add_sel(S1,A,1,[],[],S2,[]),
  add_sel(S2,A2,1,S,W,S5,W5),
  A3 is A2+1.
trans_form(ap C,A-vsel(V,S,F,W),
           A3-vsel(V,S5,[union([vsel(VC,S2,[SQL-A],[C1|[]])])-A2|F],W5)) :- !,
  trans_nested_query(C,A,SQL,A2,S1),
  VC=per(bgn(vld(A)),succ(end(vld(A)))),
  C1=(bgn(vld(A))=beginning),
  add_sel(S1,A,1,[],[],S2,[]),
  add_sel(S2,A2,1,S,W,S5,W5),
  A3 is A2+1.
trans_form(af C,A-vsel(V,S,F,W),
           A3-vsel(V,S5,[union([vsel(VC,S2,[SQL-A],[C1|[]])])-A2|F],W5)) :- !,
  trans_nested_query(C,A,SQL,A2,S1),
  VC=per(pred(bgn(vld(A)),end(vld(A)))),
  C1=(end(vld(A))=forever),
  add_sel(S1,A,1,[],[],S2,[]),
  add_sel(S2,A2,1,S,W,S5,W5),
  A3 is A2+1.
trans_form(A and B,I,O) :- !,
  trans_form(A,I,H),
  trans_form(B,H,O).
trans_form(not E,A-vsel(V,S,F,W),
           A1-vsel(V,S1,F,[not(vsel(V1,[*],F1,W1))|W])) :- !,
  trans_form(E,A-vsel([],S,[],[]),A1-vsel(V1,S1,F1,W1)).
trans_form(exists QV: E,A-vsel(V1,S1,F1,W1),A1-vsel(V2,S2,F2,W2)) :- !,
  trans_form(E,A-vsel(V1,S1,F1,W1),A1-vsel(V2,S3,F2,W2)),
  remove(QV,S3,S2).
trans_form(E1==E2,A-vsel(V,S,F,W),A-vsel(V,S2,F,W1)) :- !,
  trans_expr(E1,S,VV1,S1),
  trans_expr(E2,S1,VV2,S2),
  unify(VV1,VV2,W,W1).
trans_form(E1<E2,A-vsel(V,S,F,W),A-vsel(V,S2,F,[V1<V2|W])) :- !,
  trans_expr(E1,S,_-V1,S1),
  trans_expr(E2,S1,_-V2,S2).
trans_form(E1>E2,A-vsel(V,S,F,W),A-vsel(V,S2,F,[V1>V2|W])) :- !,
  trans_expr(E1,S,_-V1,S1),
  trans_expr(E2,S1,_-V2,S2).
trans_form(E1<>E2,A-vsel(V,S,F,W),A-vsel(V,S2,F,[V1<>V2|W])) :- !,
  trans_expr(E1,S,_-V1,S1),
  trans_expr(E2,S1,_-V2,S2).
trans_form(E1<=E2,A-vsel(V,S,F,W),A-vsel(V,S2,F,[V1<=V2|W])) :- !,
  trans_expr(E1,S,_-V1,S1),
  trans_expr(E2,S1,_-V2,S2).
trans_form(E1>=E2,A-vsel(V,S,F,W),A-vsel(V,S2,F,[V1>=V2|W])) :- !,
  trans_expr(E1,S,_-V1,S1),
  trans_expr(E2,S1,_-V2,S2).
trans_form(P,A-vsel(V,S,F,W),A1-vsel(V,S1,[Func-A|F],W1)) :-
  P=..[Func|Args],
  A1 is A+1,
  trans_args(Args,1,A,S,W,S1,W1).

trans_query(Form,A,union(SQLList),A1) :-
  findall(OFF, or_free_part(Form,OFF), FL),
  trans_query2(FL,A,SQLList,A1).
trans_query2([],A,[],A).
trans_query2([OFF|OFFList],A,[SQL1|SQLList],A1) :-
  trans_form(OFF,A-vsel([],[],[],[]),A2-SQL),
  simplify(SQL,SQL1),
  trans_query2(OFFList,A2,SQLList,A1).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% displaying a TSQL2 query %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%

disp(union([H|T]),Tab) :- disp_and(H,Tab), disp2(T,Tab).
disp2([],_).
disp2([H|T],Tab) :- format("~n~sUNION~n",[Tab]), disp_and(H,Tab), disp2(T,Tab).

disp_and(vsel(V,S,F,W),Tab) :-
  disp_valid(V,Tab,Tab1),
  format("~sSELECT ",[Tab1]), disp_sel(S,'',1), nl,
  format("~sFROM ",[Tab1]), disp_from(F,'',Tab1),
  disp_where(W,'WHERE',Tab1).

disp_valid([],Tab,Tab) :- !.
disp_valid(V,Tab,[0' ,0' |Tab]) :- format("~sVALID ",[Tab]), disp_expr(V), nl.

disp_expr(per(E1,E2)) :- !,
  format("PERIOD(",[]),
  disp_expr(E1),
  format(",",[]),
  disp_expr(E2),
  format(")",[]).
disp_expr(lst(E1,E2)) :- !,
  format("LAST(",[]),
  disp_expr(E1),
  format(",",[]),
  disp_expr(E2),
  format(")",[]).
disp_expr(fst(E1,E2)) :- !,
  format("FIRST(",[]),
  disp_expr(E1),
  format(",",[]),
  disp_expr(E2),
  format(")",[]).
disp_expr(vld(N))    :- !, format("VALID(a~d)",[N]).
disp_expr(bgn(E))    :- !, format("BEGIN(",[]), disp_expr(E), format(")",[]).
disp_expr(end(E))    :- !, format("END(",[]), disp_expr(E), format(")",[]).
disp_expr(succ(E))   :- !, disp_expr(E), format("+INTERVAL'1'YEAR",[]).
disp_expr(pred(E))   :- !, disp_expr(E), format("-INTERVAL'1'YEAR",[]).
disp_expr(forever)   :- !, format("TIMESTAMP'forever'",[]).
disp_expr(beginning) :- !, format("TIMESTAMP'beginning'",[]).
disp_expr(A-C)       :- !, format("a~d.c~d",[A,C]).
disp_expr(X)         :- !, (number(X) -> format("~w",[X]); format("'~w'",[X])).

disp_sel([],'',1) :- !, write('1 AS c1').
disp_sel([*],_,_) :- !, write(*).
disp_sel([],_,_).
disp_sel([_-X|T],IS,N) :-
  format("~w",[IS]),
  disp_expr(X),
  format(" AS c~d",[N]),
  N1 is N+1,
  disp_sel(T,',',N1).

disp_from([],'',Tab) :- !, format("dual",[Tab]).
disp_from([],_,_).
disp_from([union(SQLList)-A|T],IS,Tab) :- !,
  Tab1=[0' ,0' ,0' ,0' ,0' |Tab],
  format("~w~n~s(~n",[IS,Tab1]),
  disp(union(SQLList),[0' ,0' |Tab1]), 
  format("~n~s)(PERIOD) AS a~d",[Tab1,A]),
  disp_from(T,',',Tab).
disp_from([P-A|T],IS,Tab) :-
  format("~w~w(PERIOD) AS a~d",[IS,P,A]),
  disp_from(T,',',Tab).

disp_where([],'WHERE',_) :- !.
disp_where([],'AND',_).
disp_where([not(S)|T],IS,Tab) :- !,
  format("~n~s~w NOT EXISTS (~n",[Tab,IS]),
  disp_and(S,[0' ,0' |Tab]), 
  format(")",[]),
  disp_where(T,'AND',Tab).
disp_where([Cmp|T],IS,Tab) :-
  format("~n~s~w ",[Tab,IS]),
  Cmp=..[Op,Arg1,Arg2],
  disp_expr(Arg1), 
  format("~w",[Op]),
  disp_expr(Arg2), 
  disp_where(T,'AND',Tab).

%%%%%%%%%%%%%%%%
% main program %
%%%%%%%%%%%%%%%%

go :-
  repeat,
    read(user_input,Query), nl,
    (Query == quit ->
       true;
       normalize(Query,1,NQuery,_),
       (alwd(NQuery,[]) -> true; write('formula is not allowed'), nl, nl, fail),
       trans_query(NQuery,0,SQLList,_), 
       format("(~n",[]), disp(SQLList,""), format("~n)(PERIOD)~n~n",[]),
       fail).

:- format("~n~78c~nPurpose: Translation from temporal logic to TSQL2~n",[0'-]),
   format("Author:  Michael Boehlen (boehlen@cs.arizona.edu)~2n",[]),
   format("Connectives: and, or, implies, exists, forall, not,~n",[]),
   format("             since, until, nx, pr, ep, ef, ap, af~n",[]),
   format("Built-in predicates: <, >, ==, <>, <=, >=~n",[]),
   format("Built-in functions: none~n",[]),
   format("Error handling: none~n",[]),
   format("Miscellaneous: quit. (to quit translator) ~n",[]),
   format("               go. (to restart translator) ~2n",[]),
   format("Examples:~n",[]),
   format("  not (p(X) implies q(X)).~n",[]),
   format("  p(X) or q(X).~n",[]),
   format("  p(X) since q(X).~n",[]),
   format("  ep p(X) and exists [Y]: (r(X,Y) and Y>8).~n",[]),
   format("  ap (p(X) or q(X)).~2n",[]),
   format("  exists [S]: (i('Poland',S) and not exists [S2]: i('Slovakia',S2)).~n",[]),
   format("  (i('Poland',City) and City<>'Cracow') since i('Poland','Cracow').~n",[]),
   format("  exists [S1,S2]: (ep i(X,S1) and ef i(X,S2) and ",[]),
   format("forall [S]: not i(X,S)).~n~77c~2n",[0'-]),
   go.
