Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

ast2sqlでviewのΔに対してinsert/deleteを出力しない #49

Merged
merged 4 commits into from
Oct 25, 2024

Conversation

hiroshi-cl
Copy link

概要

#46 (2-2)

ビューに対するΔ述語が残っているルールをdl2uする場合、ビューに対するΔ述語は通常の述語を同様な扱いにしてほしい。

を実現するパッチです

方針

通常 dl2u コマンド (ast2sql.ml) では、 -a のようなΔ述語のDatalog式に対して以下のような2行のSQLを出力する

CREATE TEMPORARY TABLE temp2 AS SELECT ...;
DELETE FROM a USING temp2 WHERE ...;

ここで、ビューに対するΔ述語のときはDELETEを出力したくないが、テンポラリテーブルの方は変わらず参照が必要とのことであった。
そこで、今回の対応では単純にΔ述語がビューに対するものかどうか判定して、ビューに対するもののときはDELETEの出力だけ抑制するようにする。
また + および INSERT についても同様に出力抑制の対応を行う。

没にした方針

  • head_spec, grouping_state, rule_group にビューに対するΔ述語のパターンを追加して状態を引き回す
  • 没にした理由
    • 引き回しにより変更行数が大きくなるため
    • より簡単な方針が見つかったため
    • 大改修するならrule abstractionなどを使うように書き直した方がいいと思われるため

#46 に示されている例を使う

入力 (dl2u_2-2.dl)

source a('A':int, 'B':int).
source b('B':int, 'C':int).
view v('A':int, 'B':int, 'C':int).
-a(A, B) :- a(A, B) , not __updated__v(A, B, _).
-b(B, C) :- a(GENV2, B) , b(B, C) , b(B, GENV3) , not -v(GENV2, B, GENV3) , not __updated__v(_, B, C).
__updated__v(A, B, C) :- a(A, B) , b(B, C) , not -v(A, B, C).
-v(GENV1, GENV2, GENV3) :- a(GENV1, GENV2) , b(GENV2, GENV3) , GENV2 = 30.

実行コマンド

dune exec dl2u examples/dl2u_2-2.dl

望ましい出力例

CREATE TEMPORARY TABLE mv AS SELECT a_0.A AS A, 30 AS B, b_1.C AS C FROM a AS a_0, b AS b_1 WHERE a_0.B = 30 AND b_1.B = 30;
CREATE TEMPORARY TABLE __updated__v AS SELECT a_0.A AS A, a_0.B AS B, b_1.C AS C FROM a AS a_0, b AS b_1 WHERE b_1.B = a_0.B AND NOT EXISTS ( SELECT * FROM mv AS t WHERE t.A = a_0.A AND t.B = a_0.B AND t.C = b_1.C );
CREATE TEMPORARY TABLE temp0 AS SELECT a_0.B AS B, b_1.C AS C FROM a AS a_0, b AS b_1, b AS b_2 WHERE b_1.B = a_0.B AND b_2.B = a_0.B AND NOT EXISTS ( SELECT * FROM __updated__v AS t WHERE t.B = a_0.B AND t.C = b_1.C ) AND NOT EXISTS ( SELECT * FROM mv AS t WHERE t.A = a_0.A AND t.B = a_0.B AND t.C = b_2.C );
CREATE TEMPORARY TABLE temp1 AS SELECT a_0.A AS A, a_0.B AS B FROM a AS a_0 WHERE NOT EXISTS ( SELECT * FROM __updated__v AS t WHERE t.A = a_0.A AND t.B = a_0.B );
DELETE FROM b USING temp0 WHERE b.B = temp0.B AND b.C = temp0.C;
DELETE FROM a USING temp1 WHERE a.A = temp1.A AND a.B = temp1.B;

出力

CREATE TEMPORARY TABLE temp0 AS SELECT a_0.A AS A, 30 AS B, b_1.C AS C FROM a AS a_0, b AS b_1 WHERE a_0.B = 30 AND b_1.B = 30;
CREATE TEMPORARY TABLE __updated__v AS SELECT a_0.A AS A, a_0.B AS B, b_1.C AS C FROM a AS a_0, b AS b_1 WHERE b_1.B = a_0.B AND NOT EXISTS ( SELECT * FROM temp0 AS t WHERE t.A = a_0.A AND t.B = a_0.B AND t.C = b_1.C );
CREATE TEMPORARY TABLE temp1 AS SELECT a_0.B AS B, b_1.C AS C FROM a AS a_0, b AS b_1, b AS b_2 WHERE b_1.B = a_0.B AND b_2.B = a_0.B AND NOT EXISTS ( SELECT * FROM temp0 AS t WHERE t.A = a_0.A AND t.B = a_0.B AND t.C = b_2.C ) AND NOT EXISTS ( SELECT * FROM __updated__v AS t WHERE t.B = a_0.B AND t.C = b_1.C );
CREATE TEMPORARY TABLE temp2 AS SELECT a_0.A AS A, a_0.B AS B FROM a AS a_0 WHERE NOT EXISTS ( SELECT * FROM __updated__v AS t WHERE t.A = a_0.A AND t.B = a_0.B );
DELETE FROM b USING temp1 WHERE b.B = temp1.B AND b.C = temp1.C;
DELETE FROM a USING temp2 WHERE a.A = temp2.A AND a.B = temp2.B;

望ましい例では temp0 -> mv, temp1 -> temp0, temp2 -> temp1 とリネームされていたが、改修前と同じテンポラリテーブル名をそのまま使っている

@hiroshi-cl hiroshi-cl self-assigned this Sep 18, 2024
src/ast2sql.ml Outdated Show resolved Hide resolved
src/ast2sql.ml Outdated Show resolved Hide resolved
src/ast2sql.ml Outdated Show resolved Hide resolved
src/ast2sql.ml Outdated
@@ -2505,6 +2505,7 @@ let convert_expr_to_operation_based_sql (expr : expr) : (sql_operation list, err
table_env |> TableEnv.add table cols
) TableEnv.empty
in
let (view_name, _) = get_view expr in
Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

view_nameを取得

src/ast2sql.ml Outdated Show resolved Hide resolved
@hiroshi-cl hiroshi-cl marked this pull request as draft September 18, 2024 11:03
@@ -2559,7 +2560,7 @@ let convert_expr_to_operation_based_sql (expr : expr) : (sql_operation list, err
get_column_names_from_table ~error_detail:(InGroup delta_key) table_env table >>= fun cols ->
let delta_env = delta_env |> DeltaEnv.add delta_key (temporary_table, cols) in
let creation = SqlCreateTemporaryTable (temporary_table, sql_query) in
if TableSet.mem table existent_tables then
if Option.fold ~none:true ~some:((<>) table) view_name && TableSet.mem table existent_tables then
Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

viewに対するΔ述語だったら除外

@@ -2505,6 +2505,7 @@ let convert_expr_to_operation_based_sql (expr : expr) : (sql_operation list, err
table_env |> TableEnv.add table cols
) TableEnv.empty
in
let view_name = expr.view |> Option.map (fun (view_name, _) -> view_name) in
Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

option

@hiroshi-cl hiroshi-cl marked this pull request as ready for review September 18, 2024 12:34
@yoshihiro503
Copy link
Member

yoshihiro503 commented Sep 26, 2024

@hiroshi-cl
加藤さんからご指摘いただきました。

dl2uの修正(2-2)のPR49についてですが、少し複雑な例で試してみたところ、正しくなさそうな変換をしているようです。
以下の例を実行してみました。
dune exec dl2u inlining_j.dl > inlining_j_new.sql
inlining_j.dlには+bをheadとするルールが二つあるにも関わらず
変換後のinlining_j.sqlにはINSERT bがありません。
また、inlining_j.dlには、+aをheadとするルールが二つありますが一つ目のルールしか対応していないようです。
それと、+vに関するルール
+v(GENV1, GENV2, GENV3) :- GENV1 = 4 , a(GENV1_2, GENV2) , b(GENV2, GENV3) , GENV3 = 3 , GENV1_2 <> 4.
は、まさに昨日の例
tmp(A, B, C) :- a(A, G) , b(G, C) , B = 60 , G = 30.
と同様のルールで、適切にSQLに変換されていることを確認しました。

inlining_j_new.sql.txt
inlining_j.dl.txt

@hiroshi-cl
Copy link
Author

inlining_j.dlには+bをheadとするルールが二つあるにも関わらず
変換後のinlining_j.sqlにはINSERT bがありません。
また、inlining_j.dlには、+aをheadとするルールが二つありますが一つ目のルールしか対応していないようです。

こちらの1, 2番目の指摘事項なのですが、HEADでも起きていることなのでこのPRによるものではなさそうです。
HEADでdl2uを実行すると以下のようになりました。
別PRでの調査・修正対応とさせていただけるとありがたいです。

CREATE TEMPORARY TABLE temp0 AS SELECT a_0.A AS A, a_0.B AS B, 3 AS C FROM a AS a_0, b AS b_1 WHERE b_1.B = a_0.B AND b_1.C = 3 AND a_0.A <> 4;
CREATE TEMPORARY TABLE __updated__v AS SELECT a_0.A AS A, a_0.B AS B, b_1.C AS C FROM a AS a_0, b AS b_1 WHERE b_1.B = a_0.B AND NOT EXISTS ( SELECT * FROM temp0 AS t WHERE t.A = a_0.A AND t.B = a_0.B AND t.C = b_1.C ) UNION SELECT 4 AS A, a_0.B AS B, 3 AS C FROM a AS a_0, b AS b_1 WHERE b_1.B = a_0.B AND b_1.C = 3 AND a_0.A <> 4;
CREATE TEMPORARY TABLE temp1 AS SELECT 4 AS A, a_0.B AS B FROM a AS a_0, b AS b_1 WHERE b_1.B = a_0.B AND b_1.C = 3 AND a_0.A <> 4 AND NOT EXISTS ( SELECT * FROM a AS t WHERE t.A = 4 AND t.B = a_0.B );
CREATE TEMPORARY TABLE temp2 AS SELECT a_0.B AS B, b_1.C AS C FROM a AS a_0, b AS b_1, b AS b_2 WHERE b_1.B = a_0.B AND b_2.B = a_0.B AND NOT EXISTS ( SELECT * FROM temp0 AS t WHERE t.A = a_0.A AND t.B = a_0.B AND t.C = b_2.C ) AND NOT EXISTS ( SELECT * FROM __updated__v AS t WHERE t.B = a_0.B AND t.C = b_1.C ) UNION SELECT a_0.B AS B, b_1.C AS C FROM a AS a_0, b AS b_1, b AS b_2 WHERE b_1.B = a_0.B AND b_2.B = a_0.B AND b_2.C = 3 AND a_0.A <> 4 AND NOT EXISTS ( SELECT * FROM __updated__v AS t WHERE t.B = a_0.B AND t.C = b_1.C );
CREATE TEMPORARY TABLE temp3 AS SELECT a_0.A AS A, a_0.B AS B FROM a AS a_0 WHERE NOT EXISTS ( SELECT * FROM __updated__v AS t WHERE t.A = a_0.A AND t.B = a_0.B );
DELETE FROM v USING temp0 WHERE v.A = temp0.A AND v.B = temp0.B AND v.C = temp0.C;
INSERT INTO a SELECT * FROM temp1;
DELETE FROM b USING temp2 WHERE b.B = temp2.B AND b.C = temp2.C;
DELETE FROM a USING temp3 WHERE a.A = temp3.A AND a.B = temp3.B;

@hiroyukikato
Copy link
Collaborator

別PRでのご対応とのこと、よろしくお願いいたします。

@cedretaber cedretaber mentioned this pull request Oct 2, 2024
@hiroshi-cl
Copy link
Author

+CREATE TEMPORARY TABLE temp1 AS SELECT 4 AS A, a_0.B AS B, 3 AS C FROM a AS a_0, b AS b_1 WHERE b_1.B = a_0.B AND b_1.C = 3 AND a_0.A <> 4;

意図しない差分があったので調査していたのですが、 #47 が未反映だったためでした

@hiroshi-cl
Copy link
Author

HEADを取り込んだ後の差分

 CREATE TEMPORARY TABLE temp1 AS SELECT 4 AS A, a_0.B AS B FROM a AS a_0, b AS b_1 WHERE b_1.B = a_0.B AND b_1.C = 3 AND a_0.A <> 4 AND NOT EXISTS ( SELECT * FROM a AS t WHERE t.A = 4 AND t.B = a_0.B );
 CREATE TEMPORARY TABLE temp2 AS SELECT a_0.B AS B, b_1.C AS C FROM a AS a_0, b AS b_1, b AS b_2 WHERE b_1.B = a_0.B AND b_2.B = a_0.B AND NOT EXISTS ( SELECT * FROM temp0 AS t WHERE t.A = a_0.A AND t.B = a_0.B AND t.C = b_2.C ) AND NOT EXISTS ( SELECT * FROM __updated__v AS t WHERE t.B = a_0.B AND t.C = b_1.C ) UNION SELECT a_0.B AS B, b_1.C AS C FROM a AS a_0, b AS b_1, b AS b_2 WHERE b_1.B = a_0.B AND b_2.B = a_0.B AND b_2.C = 3 AND a_0.A <> 4 AND NOT EXISTS ( SELECT * FROM __updated__v AS t WHERE t.B = a_0.B AND t.C = b_1.C );
 CREATE TEMPORARY TABLE temp3 AS SELECT a_0.A AS A, a_0.B AS B FROM a AS a_0 WHERE NOT EXISTS ( SELECT * FROM __updated__v AS t WHERE t.A = a_0.A AND t.B = a_0.B );
-DELETE FROM v USING temp0 WHERE v.A = temp0.A AND v.B = temp0.B AND v.C = temp0.C;
 INSERT INTO a SELECT * FROM temp1;
 DELETE FROM b USING temp2 WHERE b.B = temp2.B AND b.C = temp2.C;
 DELETE FROM a USING temp3 WHERE a.A = temp3.A AND a.B = temp3.B;

@hiroyukikato
Copy link
Collaborator

Thanks! LGTM

@hiroshi-cl hiroshi-cl merged commit ec0e384 into proof-ninja:master Oct 25, 2024
2 checks passed
@hiroshi-cl hiroshi-cl deleted the feat/dl2u_del2 branch October 25, 2024 00:07
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants