home *** CD-ROM | disk | FTP | other *** search
/ ftp.cs.arizona.edu / ftp.cs.arizona.edu.tar / ftp.cs.arizona.edu / tsql / tsql2 / tl2tsql2.pl < prev   
Text File  |  1995-06-29  |  13KB  |  382 lines
  1. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  2. % Mapping between TL and TSQL2.                 %
  3. %                                               %
  4. % Runs with SICStus, Quintus, and SWI-Prolog.   % 
  5. %                                               %
  6. % To start, load this file into Prolog, e.g.,   %
  7. %   prolog                                      %
  8. %   [tl2tsql2].                                 %
  9. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  10.  
  11. :- op(900,yfx,[implies]).
  12. :- op(850,yfx,[or]).
  13. :- op(800,yfx,[and, since,until]).
  14. :- op(750,xfy,[:]).
  15. :- op(750,fy,[not,nx,pr,ef,ep,af,ap,exists,forall]).
  16. :- op(700,xfx,[<=,<>]).
  17.  
  18. is_atom(F) :- functor(F,N,_), \+current_op(_,_,N).
  19.  
  20. member(H,[H|_]).
  21. member(H,[_|T]) :- member(H,T).
  22.  
  23. nth([X|_],1,X) :- !.
  24. nth([_|T],N,X) :- N1 is N-1, nth(T,N1,X).
  25.  
  26. exclude(L1,L2,L) :- findall(X, (member(X,L1),\+member(X,L2)), L).
  27.  
  28. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  29. % normalization of temporal logic formulas %
  30. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  31.  
  32. :- op(950,xfx,'==>').
  33.  
  34. F1 implies F2         ==> not F1 or F2.
  35. forall VL: F          ==> not exists VL: (not F).
  36.  
  37. not (A and B)         ==> not A or not B.
  38. not (A or B)          ==> not A and not B.
  39. not not F             ==> F.
  40. not T1==T2            ==> T1<>T2.
  41. not T1<T2             ==> T1>=T2.
  42. not T1>T2             ==> T1<=T2.
  43. not T1<=T2            ==> T1>T2.
  44. not T1>=T2            ==> T1<T2.
  45. not T1<>T2            ==> T1==T2.
  46.  
  47. F1 and (F2 or F3)     ==> F1 and F2 or F1 and F3.
  48. (F1 or F2) and F3     ==> F1 and F3 or F2 and F3.
  49. exists VL: (F1 or F2) ==> exists VL: F1 or exists VL: F2.
  50. F1 since (F2 or F3)   ==> F1 since F2 or F1 since F3.
  51. F1 until (F2 or F3)   ==> F1 until F2 or F1 until F3.
  52. ep (F1 or F2)         ==> ep F1 or ep F2.
  53. ef (F1 or F2)         ==> ef F1 or ef F2.
  54. pr (F1 or F2)         ==> pr F1 or pr F2.
  55. nx (F1 or F2)         ==> nx F1 or nx F2.
  56.  
  57. %% try(+Form,+VarNr,-Form,-VarNr)
  58. try(var(N),N,var(N),N1) :- !, N1 is N+1.
  59. try(X,N,Y,N) :- X==>Y.
  60. try(X,N,Y,N1) :- X=..[F|Args], try_list(Args,N,NArgs,N1), Y=..[F|NArgs].
  61.  
  62. %% try_list(+FormList,+VarNr,-FormList,-VarNr)
  63. try_list([X|T],N,[Z|T],N1) :- try(X,N,Z,N1).
  64. try_list([X|T],N,[X|T1],N1) :- try_list(T,N,T1,N1).
  65.  
  66. %% normalize(+Form,+VarNr,-Form,-VarNr)
  67. normalize(X,N,Y,N2) :- try(X,N,Z,N1), !, normalize(Z,N1,Y,N2).
  68. normalize(X,_,X,_).
  69.  
  70. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  71. % allowedness of temporal logic formulas %
  72. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  73.  
  74. %% vars(+Formula,+VarList,?VarList)
  75. vars(var(N),V,V1)        :- !, (member(var(N),V) -> V1=V; V1=[var(N)|V]).
  76. vars(exists VL: A,V,V1)  :- !, vars(A,V,V2), exclude(V2,VL,V1).
  77. vars([H|T],V,V1)         :- !, vars(H,V,V2), vars(T,V2,V1).
  78. vars([],V,V1)            :- !, V=V1.
  79. vars(A,V,V1)             :- A=..[_|L], vars(L,V,V1).
  80.  
  81. %% alwd(+Formula,+SafeVarList)
  82. alwd(A and B,V)      :- !, alwd(A,V), vars(A,V,V1), alwd(B,V1).
  83. alwd(A or B,_)       :- !, alwd(A,[]), alwd(B,[]), vars(A,[],V), vars(B,[],V).
  84. alwd(not A,V)        :- !, alwd(A,V), vars(A,V,V).
  85. alwd(exists VL: A,V) :- !, exclude(V,VL,V1), alwd(A,V1).
  86. alwd(A since B,_)    :- !, alwd(A,[]), alwd(B,[]).
  87. alwd(A until B,_)    :- !, alwd(A,[]), alwd(B,[]).
  88. alwd(pr A,_)         :- !, alwd(A,[]).
  89. alwd(nx A,_)         :- !, alwd(A,[]).
  90. alwd(ep A,_)         :- !, alwd(A,[]).
  91. alwd(ef A,_)         :- !, alwd(A,[]).
  92. alwd(ap A,_)         :- !, alwd(A,[]).
  93. alwd(af A,_)         :- !, alwd(A,[]).
  94. alwd(T1<T2,V)        :- !, vars(T1,V,V), vars(T2,V,V).
  95. alwd(T1>T2,V)        :- !, vars(T1,V,V), vars(T2,V,V).
  96. alwd(T1<=T2,V)       :- !, vars(T1,V,V), vars(T2,V,V).
  97. alwd(T1>=T2,V)       :- !, vars(T1,V,V), vars(T2,V,V).
  98. alwd(T1<>T2,V)       :- !, vars(T1,V,V), vars(T2,V,V).
  99. alwd(T1==T2,V)       :- !, (vars(T1,V,V); vars(T2,V,V)).
  100. alwd(A,_)            :- is_atom(A), !.
  101.  
  102. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  103. % translation from temporal logic to TSQL2 %
  104. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  105.  
  106. or_free_part(A or B, OFP) :- !, (or_free_part(A, OFP) ; or_free_part(B, OFP)).
  107. or_free_part(OFP, OFP).
  108.  
  109. simplify(Q,Q1) :- simplify1(Q,Qx), !, simplify(Qx,Q1).
  110. simplify(Q,Q).
  111.  
  112. simplify1(vsel([],S,[union([vsel(V1,S1,F1,W1)])-_],[]),vsel(V1,S2,F1,W1)) :- !,
  113.   findall(X, (member(Y,S), (Y=_-(_-C) -> nth(S1,C,X); X=Y)), S2).
  114. simplify1(vsel(V,S,F,W),vsel(V,S,F1,W)) :-
  115.   simplify2(F,F1).
  116.  
  117. simplify2([R-A|T],[R1-A|T]) :- simplify1(R,R1).
  118. simplify2([R-A|T],[R-A|T1]) :- simplify2(T,T1).
  119.  
  120. remove(_,[],[]).
  121. remove(QV,[Var-_|S1],S2) :- member(Var,QV), !, remove(QV,S1,S2).
  122. remove(QV,[Var-V|S1],[Var-V|S2]) :- remove(QV,S1,S2).
  123.  
  124. unify(_-V,_-V,W,W) :- !.
  125. unify(_-V1,_-V2,W,[V2=V1|W]).
  126.  
  127. trans_expr(var(N),S,var(N)-V,S) :- member(var(N)-V,S), !.
  128. trans_expr(var(N),S,var(N)-V,[var(N)-V|S]) :- !.
  129. trans_expr(E,S,_-E,S).
  130.  
  131. trans_args([],_,_,S,W,S,W).
  132. trans_args([Arg|T],N,A,S,W,S2,W2) :-
  133.   N1 is N+1,
  134.   trans_args(T,N1,A,S,W,S1,W1),
  135.   trans_expr(Arg,S1,VV,S2),
  136.   unify(VV,_-(A-N),W1,W2).
  137.  
  138. %% trans_nested_query(+Form,+Alias,-SQL,-Alias,-Sel,-Where)
  139. trans_nested_query(Form,A,SQL,A2,S) :-
  140.   Form=..[Func|Args],
  141.   ((is_atom(Func), trans_args(Args,1,A,[],[],S,[])) ->
  142.      A2 is A+1,
  143.      SQL=Func;
  144.      A1 is A+1,
  145.      trans_query(Form,A1,SQL,A2),
  146.      SQL=union([vsel(_,S,_,_)|_])).
  147.  
  148. %% add_sel(+Select,+Alias,+ColNumber,+Select,+Where,-Select,-Where)
  149. add_sel([],_,_,S,W,S,W).
  150. add_sel([Var-_|T],A,N,S,W,S2,W2) :-
  151.   trans_expr(Var,S,VV,S1),
  152.   unify(VV,_-(A-N),W,W1),
  153.   N1 is N+1,
  154.   add_sel(T,A,N1,S1,W1,S2,W2).
  155.  
  156. %% trans_form(+Formula,+Alias&ValidSelectStmt,-Alias&ValidSelectStmt)
  157. trans_form(C since D,A-vsel(V,S,F,W),A5-vsel(V,Sz,
  158.            [union([vsel(VC,Sy,[SQL1-A,SQL2-A2],[C1,C2|Wy])])-A4|F],Wz)) :- !,
  159.   trans_nested_query(C,A,SQL1,A2,S1),
  160.   trans_nested_query(D,A2,SQL2,A4,S2),
  161.   VC=per(lst(bgn(vld(A)),succ(bgn(vld(A2)))),end(vld(A))),
  162.   C1=(lst(bgn(vld(A)),succ(bgn(vld(A2))))<end(vld(A))),
  163.   C2=(end(vld(A2))>=bgn(vld(A))),
  164.   add_sel(S1,A,1,[],[],Sx,Wx),
  165.   add_sel(S2,A2,1,Sx,Wx,Sy,Wy),
  166.   add_sel(Sy,A4,1,S,W,Sz,Wz),
  167.   A5 is A4+1.
  168. trans_form(C until D,A-vsel(V,S,F,W),A5-vsel(V,Sz,
  169.            [union([vsel(VC,Sy,[SQL1-A,SQL2-A2],[C1,C2|Wy])])-A4|F],Wz)) :- !,
  170.   trans_nested_query(C,A,SQL1,A2,S1),
  171.   trans_nested_query(D,A2,SQL2,A4,S2),
  172.   VC=per(bgn(vld(A)),fst(end(vld(A)),pred(end(vld(A2))))),
  173.   C1=(bgn(vld(A))<fst(end(vld(A)),pred(end(vld(A2))))),
  174.   C2=(end(vld(A))>=bgn(vld(A2))),
  175.   add_sel(S1,A,1,[],[],Sx,Wx),
  176.   add_sel(S2,A2,1,Sx,Wx,Sy,Wy),
  177.   add_sel(Sy,A4,1,S,W,Sz,Wz),
  178.   A5 is A4+1.
  179. trans_form(pr C,A-vsel(V,S,F,W),
  180.            A3-vsel(V,S5,[union([vsel(VC,S2,[SQL-A],[])])-A2|F],W5)) :- !,
  181.   trans_nested_query(C,A,SQL,A2,S1),
  182.   VC=succ(vld(A)),
  183.   add_sel(S1,A,1,[],[],S2,[]),
  184.   add_sel(S2,A2,1,S,W,S5,W5),
  185.   A3 is A2+1.
  186. trans_form(nx C,A-vsel(V,S,F,W),
  187.            A3-vsel(V,S5,[union([vsel(VC,S2,[SQL-A],[])])-A2|F],W5)) :- !,
  188.   trans_nested_query(C,A,SQL,A2,S1),
  189.   VC=pred(vld(A)),
  190.   add_sel(S1,A,1,[],[],S2,[]),
  191.   add_sel(S2,A2,1,S,W,S5,W5),
  192.   A3 is A2+1.
  193. trans_form(ep C,A-vsel(V,S,F,W),
  194.            A3-vsel(V,S5,[union([vsel(VC,S2,[SQL-A],[])])-A2|F],W5)) :- !,
  195.   trans_nested_query(C,A,SQL,A2,S1),
  196.   VC=per(succ(bgn(vld(A))),forever),
  197.   add_sel(S1,A,1,[],[],S2,[]),
  198.   add_sel(S2,A2,1,S,W,S5,W5),
  199.   A3 is A2+1.
  200. trans_form(ef C,A-vsel(V,S,F,W),
  201.            A3-vsel(V,S5,[union([vsel(VC,S2,[SQL-A],[])])-A2|F],W5)) :- !,
  202.   trans_nested_query(C,A,SQL,A2,S1),
  203.   VC=per(beginning,pred(end(vld(A)))),
  204.   add_sel(S1,A,1,[],[],S2,[]),
  205.   add_sel(S2,A2,1,S,W,S5,W5),
  206.   A3 is A2+1.
  207. trans_form(ap C,A-vsel(V,S,F,W),
  208.            A3-vsel(V,S5,[union([vsel(VC,S2,[SQL-A],[C1|[]])])-A2|F],W5)) :- !,
  209.   trans_nested_query(C,A,SQL,A2,S1),
  210.   VC=per(bgn(vld(A)),succ(end(vld(A)))),
  211.   C1=(bgn(vld(A))=beginning),
  212.   add_sel(S1,A,1,[],[],S2,[]),
  213.   add_sel(S2,A2,1,S,W,S5,W5),
  214.   A3 is A2+1.
  215. trans_form(af C,A-vsel(V,S,F,W),
  216.            A3-vsel(V,S5,[union([vsel(VC,S2,[SQL-A],[C1|[]])])-A2|F],W5)) :- !,
  217.   trans_nested_query(C,A,SQL,A2,S1),
  218.   VC=per(pred(bgn(vld(A)),end(vld(A)))),
  219.   C1=(end(vld(A))=forever),
  220.   add_sel(S1,A,1,[],[],S2,[]),
  221.   add_sel(S2,A2,1,S,W,S5,W5),
  222.   A3 is A2+1.
  223. trans_form(A and B,I,O) :- !,
  224.   trans_form(A,I,H),
  225.   trans_form(B,H,O).
  226. trans_form(not E,A-vsel(V,S,F,W),
  227.            A1-vsel(V,S1,F,[not(vsel(V1,[*],F1,W1))|W])) :- !,
  228.   trans_form(E,A-vsel([],S,[],[]),A1-vsel(V1,S1,F1,W1)).
  229. trans_form(exists QV: E,A-vsel(V1,S1,F1,W1),A1-vsel(V2,S2,F2,W2)) :- !,
  230.   trans_form(E,A-vsel(V1,S1,F1,W1),A1-vsel(V2,S3,F2,W2)),
  231.   remove(QV,S3,S2).
  232. trans_form(E1==E2,A-vsel(V,S,F,W),A-vsel(V,S2,F,W1)) :- !,
  233.   trans_expr(E1,S,VV1,S1),
  234.   trans_expr(E2,S1,VV2,S2),
  235.   unify(VV1,VV2,W,W1).
  236. trans_form(E1<E2,A-vsel(V,S,F,W),A-vsel(V,S2,F,[V1<V2|W])) :- !,
  237.   trans_expr(E1,S,_-V1,S1),
  238.   trans_expr(E2,S1,_-V2,S2).
  239. trans_form(E1>E2,A-vsel(V,S,F,W),A-vsel(V,S2,F,[V1>V2|W])) :- !,
  240.   trans_expr(E1,S,_-V1,S1),
  241.   trans_expr(E2,S1,_-V2,S2).
  242. trans_form(E1<>E2,A-vsel(V,S,F,W),A-vsel(V,S2,F,[V1<>V2|W])) :- !,
  243.   trans_expr(E1,S,_-V1,S1),
  244.   trans_expr(E2,S1,_-V2,S2).
  245. trans_form(E1<=E2,A-vsel(V,S,F,W),A-vsel(V,S2,F,[V1<=V2|W])) :- !,
  246.   trans_expr(E1,S,_-V1,S1),
  247.   trans_expr(E2,S1,_-V2,S2).
  248. trans_form(E1>=E2,A-vsel(V,S,F,W),A-vsel(V,S2,F,[V1>=V2|W])) :- !,
  249.   trans_expr(E1,S,_-V1,S1),
  250.   trans_expr(E2,S1,_-V2,S2).
  251. trans_form(P,A-vsel(V,S,F,W),A1-vsel(V,S1,[Func-A|F],W1)) :-
  252.   P=..[Func|Args],
  253.   A1 is A+1,
  254.   trans_args(Args,1,A,S,W,S1,W1).
  255.  
  256. trans_query(Form,A,union(SQLList),A1) :-
  257.   findall(OFF, or_free_part(Form,OFF), FL),
  258.   trans_query2(FL,A,SQLList,A1).
  259. trans_query2([],A,[],A).
  260. trans_query2([OFF|OFFList],A,[SQL1|SQLList],A1) :-
  261.   trans_form(OFF,A-vsel([],[],[],[]),A2-SQL),
  262.   simplify(SQL,SQL1),
  263.   trans_query2(OFFList,A2,SQLList,A1).
  264.  
  265. %%%%%%%%%%%%%%%%%%%%%%%%%%%%
  266. % displaying a TSQL2 query %
  267. %%%%%%%%%%%%%%%%%%%%%%%%%%%%
  268.  
  269. disp(union([H|T]),Tab) :- disp_and(H,Tab), disp2(T,Tab).
  270. disp2([],_).
  271. disp2([H|T],Tab) :- format("~n~sUNION~n",[Tab]), disp_and(H,Tab), disp2(T,Tab).
  272.  
  273. disp_and(vsel(V,S,F,W),Tab) :-
  274.   disp_valid(V,Tab,Tab1),
  275.   format("~sSELECT ",[Tab1]), disp_sel(S,'',1), nl,
  276.   format("~sFROM ",[Tab1]), disp_from(F,'',Tab1),
  277.   disp_where(W,'WHERE',Tab1).
  278.  
  279. disp_valid([],Tab,Tab) :- !.
  280. disp_valid(V,Tab,[0' ,0' |Tab]) :- format("~sVALID ",[Tab]), disp_expr(V), nl.
  281.  
  282. disp_expr(per(E1,E2)) :- !,
  283.   format("PERIOD(",[]),
  284.   disp_expr(E1),
  285.   format(",",[]),
  286.   disp_expr(E2),
  287.   format(")",[]).
  288. disp_expr(lst(E1,E2)) :- !,
  289.   format("LAST(",[]),
  290.   disp_expr(E1),
  291.   format(",",[]),
  292.   disp_expr(E2),
  293.   format(")",[]).
  294. disp_expr(fst(E1,E2)) :- !,
  295.   format("FIRST(",[]),
  296.   disp_expr(E1),
  297.   format(",",[]),
  298.   disp_expr(E2),
  299.   format(")",[]).
  300. disp_expr(vld(N))    :- !, format("VALID(a~d)",[N]).
  301. disp_expr(bgn(E))    :- !, format("BEGIN(",[]), disp_expr(E), format(")",[]).
  302. disp_expr(end(E))    :- !, format("END(",[]), disp_expr(E), format(")",[]).
  303. disp_expr(succ(E))   :- !, disp_expr(E), format("+INTERVAL'1'YEAR",[]).
  304. disp_expr(pred(E))   :- !, disp_expr(E), format("-INTERVAL'1'YEAR",[]).
  305. disp_expr(forever)   :- !, format("TIMESTAMP'forever'",[]).
  306. disp_expr(beginning) :- !, format("TIMESTAMP'beginning'",[]).
  307. disp_expr(A-C)       :- !, format("a~d.c~d",[A,C]).
  308. disp_expr(X)         :- !, (number(X) -> format("~w",[X]); format("'~w'",[X])).
  309.  
  310. disp_sel([],'',1) :- !, write('1 AS c1').
  311. disp_sel([*],_,_) :- !, write(*).
  312. disp_sel([],_,_).
  313. disp_sel([_-X|T],IS,N) :-
  314.   format("~w",[IS]),
  315.   disp_expr(X),
  316.   format(" AS c~d",[N]),
  317.   N1 is N+1,
  318.   disp_sel(T,',',N1).
  319.  
  320. disp_from([],'',Tab) :- !, format("dual",[Tab]).
  321. disp_from([],_,_).
  322. disp_from([union(SQLList)-A|T],IS,Tab) :- !,
  323.   Tab1=[0' ,0' ,0' ,0' ,0' |Tab],
  324.   format("~w~n~s(~n",[IS,Tab1]),
  325.   disp(union(SQLList),[0' ,0' |Tab1]), 
  326.   format("~n~s)(PERIOD) AS a~d",[Tab1,A]),
  327.   disp_from(T,',',Tab).
  328. disp_from([P-A|T],IS,Tab) :-
  329.   format("~w~w(PERIOD) AS a~d",[IS,P,A]),
  330.   disp_from(T,',',Tab).
  331.  
  332. disp_where([],'WHERE',_) :- !.
  333. disp_where([],'AND',_).
  334. disp_where([not(S)|T],IS,Tab) :- !,
  335.   format("~n~s~w NOT EXISTS (~n",[Tab,IS]),
  336.   disp_and(S,[0' ,0' |Tab]), 
  337.   format(")",[]),
  338.   disp_where(T,'AND',Tab).
  339. disp_where([Cmp|T],IS,Tab) :-
  340.   format("~n~s~w ",[Tab,IS]),
  341.   Cmp=..[Op,Arg1,Arg2],
  342.   disp_expr(Arg1), 
  343.   format("~w",[Op]),
  344.   disp_expr(Arg2), 
  345.   disp_where(T,'AND',Tab).
  346.  
  347. %%%%%%%%%%%%%%%%
  348. % main program %
  349. %%%%%%%%%%%%%%%%
  350.  
  351. go :-
  352.   repeat,
  353.     read(user_input,Query), nl,
  354.     (Query == quit ->
  355.        true;
  356.        normalize(Query,1,NQuery,_),
  357.        (alwd(NQuery,[]) -> true; write('formula is not allowed'), nl, nl, fail),
  358.        trans_query(NQuery,0,SQLList,_), 
  359.        format("(~n",[]), disp(SQLList,""), format("~n)(PERIOD)~n~n",[]),
  360.        fail).
  361.  
  362. :- format("~n~78c~nPurpose: Translation from temporal logic to TSQL2~n",[0'-]),
  363.    format("Author:  Michael Boehlen (boehlen@cs.arizona.edu)~2n",[]),
  364.    format("Connectives: and, or, implies, exists, forall, not,~n",[]),
  365.    format("             since, until, nx, pr, ep, ef, ap, af~n",[]),
  366.    format("Built-in predicates: <, >, ==, <>, <=, >=~n",[]),
  367.    format("Built-in functions: none~n",[]),
  368.    format("Error handling: none~n",[]),
  369.    format("Miscellaneous: quit. (to quit translator) ~n",[]),
  370.    format("               go. (to restart translator) ~2n",[]),
  371.    format("Examples:~n",[]),
  372.    format("  not (p(X) implies q(X)).~n",[]),
  373.    format("  p(X) or q(X).~n",[]),
  374.    format("  p(X) since q(X).~n",[]),
  375.    format("  ep p(X) and exists [Y]: (r(X,Y) and Y>8).~n",[]),
  376.    format("  ap (p(X) or q(X)).~2n",[]),
  377.    format("  exists [S]: (i('Poland',S) and not exists [S2]: i('Slovakia',S2)).~n",[]),
  378.    format("  (i('Poland',City) and City<>'Cracow') since i('Poland','Cracow').~n",[]),
  379.    format("  exists [S1,S2]: (ep i(X,S1) and ef i(X,S2) and ",[]),
  380.    format("forall [S]: not i(X,S)).~n~77c~2n",[0'-]),
  381.    go.
  382.