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

#46 2-1の修正: ast2sqlでソースのカラム名を伝搬させず述語のカラム名をそのまま使うようにした #51

Merged
merged 4 commits into from
Oct 31, 2024

Conversation

hiroshi-cl
Copy link

@hiroshi-cl hiroshi-cl commented Oct 8, 2024

#46 (2-1) 同じ変数が複数の述語に現れると、エラー場合がある。の対応です

方針

これまでast2sqlはカラムのエイリアス名にソースのカラム名を伝搬させるルールになっていました。
しかしこのルールには以下の2点の考慮漏れがあり、SQLを生成できないDatalog式が多く存在しました。

  1. headに出てこない変数
  2. predicateに渡されていない変数

例えば tmp(A, B, C) :- a(A, G) , b(G, C) , B = 60 , G = 30. の場合、変数 G が(1)、変数 B が(2)に該当します。

そこで、このルールを削除し、素直に述語のカラム名をそのまま使用するように変更します。

入出力例1: #46 (2-1) のエラー例

入力 (dl2u_error.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) , tmp(A, B, C).
tmp(A, B, C) :- a(A, G) , b(G, C) , B = 60 , G = 30.

コマンド

dune exec dl2u examples/dl2u_error.dl

望ましい出力

エラーにならない

修正後の出力

エラーにならず以下が出力される

CREATE TEMPORARY TABLE tmp AS SELECT a_0.A AS A, 60 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 temp0 AS SELECT a_0.A AS A, a_0.B AS B FROM a AS a_0, tmp AS tmp_1 WHERE tmp_1.A = a_0.A AND tmp_1.B = a_0.B;
DELETE FROM a USING temp0 WHERE a.A = temp0.A AND a.B = temp0.B;

入出力例2: エイリアス名が変わる例

入力

source a('A':int, 'B':int).
view v('A':int, 'B':int, 'C':int).
-a(A, B) :- f(B, A).
f(C, D) :- a(D, C).

コマンド

dune exec dl2u examples/dl2u_name.dl

修正前の出力

テンポラリテーブル f のエイリアス名にソース aB, A が使われている。

CREATE TEMPORARY TABLE f AS SELECT a_0.B AS B, a_0.A AS A FROM a AS a_0;
CREATE TEMPORARY TABLE temp0 AS SELECT f_0.A AS A, f_0.B AS B FROM f AS f_0;
DELETE FROM a USING temp0 WHERE a.A = temp0.A AND a.B = temp0.B;

修正後の出力

テンポラリテーブル f のエイリアス名に述語 f 自体のカラム名 C, D が使われている。

CREATE TEMPORARY TABLE f AS SELECT a_0.B AS C, a_0.A AS D FROM a AS a_0;
CREATE TEMPORARY TABLE temp0 AS SELECT f_0.D AS A, f_0.C AS B FROM f AS f_0;
DELETE FROM a USING temp0 WHERE a.A = temp0.A AND a.B = temp0.B;

@hiroshi-cl hiroshi-cl requested a review from cedretaber October 8, 2024 15:14
@hiroshi-cl hiroshi-cl self-assigned this Oct 8, 2024
@hiroshi-cl hiroshi-cl force-pushed the fix/dl2u_tmp_error branch 3 times, most recently from fab3eb9 to b443514 Compare October 8, 2024 15:17
@hiroshi-cl hiroshi-cl changed the title [WIP] #46 2-1の修正 #46 2-1の修正: ast2sqlでソースのカラム名を伝搬させず述語のカラム名をそのまま使うようにした Oct 20, 2024
Comment on lines +230 to +237
"CREATE TEMPORARY TABLE v AS SELECT a_0.AA AS A, a_0.BB AS B, b_1.CC AS C FROM a AS a_0, b AS b_1 WHERE b_1.BB = a_0.BB;";
"CREATE TEMPORARY TABLE temp0 AS SELECT v_0.A AS A, v_0.B AS B, 3 AS C FROM v AS v_0 WHERE v_0.C = 3 AND v_0.A <> 4;";
"CREATE TEMPORARY TABLE temp1 AS SELECT 4 AS A, temp0.B AS B, temp0.C AS C FROM temp0 AS temp0;";
"CREATE TEMPORARY TABLE uv AS SELECT v_0.A AS A, v_0.B AS B, v_0.C AS C FROM v AS v_0 WHERE NOT EXISTS ( SELECT * FROM temp0 AS t WHERE t.A = v_0.A AND t.B = v_0.B AND t.C = v_0.C ) UNION SELECT temp1.A AS A, temp1.B AS B, temp1.C AS C FROM temp1 AS temp1;";
"CREATE TEMPORARY TABLE temp2 AS SELECT uv_0.B AS BB, uv_0.C AS CC FROM uv AS uv_0 WHERE NOT EXISTS ( SELECT * FROM b AS t WHERE t.BB = uv_0.B AND t.CC = uv_0.C );";
"CREATE TEMPORARY TABLE temp3 AS SELECT uv_0.A AS AA, uv_0.B AS BB FROM uv AS uv_0 WHERE NOT EXISTS ( SELECT * FROM a AS t WHERE t.AA = uv_0.A AND t.BB = uv_0.B );";
"CREATE TEMPORARY TABLE temp4 AS SELECT b_0.BB AS BB, b_0.CC AS CC FROM b AS b_0, uv AS uv_1 WHERE uv_1.B = b_0.BB AND NOT EXISTS ( SELECT * FROM uv AS t WHERE t.B = b_0.BB AND t.C = b_0.CC );";
"CREATE TEMPORARY TABLE temp5 AS SELECT a_0.AA AS AA, a_0.BB AS BB FROM a AS a_0 WHERE NOT EXISTS ( SELECT * FROM uv AS t WHERE t.A = a_0.AA AND t.B = a_0.BB );";
Copy link
Author

Choose a reason for hiding this comment

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

エイリアス名のルールを変更したのでテストも修正

Comment on lines -2330 to -2361
) ([], ArgMap.empty) >>= fun (colmns, arg_map) ->
body |> foldM (fun arg_map term ->
match term with
| Rel (Pred (target, args))
| Rel (Deltainsert (target, args))
| Rel (Deltadelete (target, args)) ->
begin match TableEnv.find_opt target table_env with
| None ->
err @@ UnknownTable { table = target; error_detail = InRule (head, body) }
| Some cols ->
List.combine cols args |> foldM (fun arg_map (col, arg) ->
match arg with
| NamedVar x ->
begin match arg_map |> ArgMap.find_opt x with
| None -> err @@ InvalidArgInBody { var = arg; error_detail = InRule (head, body) }
| Some None -> return (arg_map |> ArgMap.add x (Some col))
| Some (Some col0) when col = col0 -> return arg_map
| Some (Some _) -> err @@ InvalidArgInBody { var = arg; error_detail = InRule (head, body) }
end

| _ ->
err @@ InvalidArgInBody { var = arg; error_detail = InRule (head, body) }
) arg_map
end

| _ -> return arg_map
) arg_map >>= fun arg_map ->
colmns |> List.rev |> foldM (fun columns col ->
match arg_map |> ArgMap.find_opt col with
| None -> err @@ HeadVariableDoesNotOccurInBody col
| Some None -> err @@ HeadVariableDoesNotOccurInBody col
| Some Some col -> return (col :: columns)
Copy link
Author

Choose a reason for hiding this comment

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

ざっくり削除してしまう

@hiroshi-cl hiroshi-cl marked this pull request as ready for review October 20, 2024 15:06
@hiroshi-cl
Copy link
Author

修正が完了したのでreadyにしました

src/ast2sql.ml Outdated Show resolved Hide resolved
@cedretaber
Copy link
Collaborator

module ArgMap = Map.Make(String)

この module 定義も不要になってしまいましたね。

@cedretaber
Copy link
Collaborator

📝
同名の述語が複数あって、中で使われている変数名が異なる場合、 SQL では UNION で表現されるが、最初に出てきた方の述語の変数名に統一される。

source a('A':int, 'B':int).
source b('X':int, 'Y':int).
f(C, D) :- a(D, C), C <> 1.
f(E, F) :- b(E, F), E <> 2.
+a(A, B) :- f(B, A).
-b(X, Y) :- f(Y, X).
CREATE TEMPORARY TABLE f AS SELECT a_0.B AS C, a_0.A AS D FROM a AS a_0 WHERE a_0.B <> 1 UNION SELECT b_0.X AS C, b_0.Y AS D FROM b AS b_0 WHERE b_0.X <> 2;
CREATE TEMPORARY TABLE temp0 AS SELECT f_0.D AS A, f_0.C AS B FROM f AS f_0;
CREATE TEMPORARY TABLE temp1 AS SELECT f_0.D AS X, f_0.C AS Y FROM f AS f_0;
INSERT INTO a SELECT * FROM temp0;
DELETE FROM b USING temp1 WHERE b.X = temp1.X AND b.Y = temp1.Y;

Copy link
Collaborator

@cedretaber cedretaber left a comment

Choose a reason for hiding this comment

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

ありがとうございます 🙏

@hiroshi-cl
Copy link
Author

#51 (comment)
これ気付いていなかったのですがたしかに

Copy link
Collaborator

@hiroyukikato hiroyukikato left a comment

Choose a reason for hiding this comment

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

Thanks.

@hiroshi-cl
Copy link
Author

🙆‍♂️

@hiroshi-cl hiroshi-cl merged commit a67ac06 into proof-ninja:master Oct 31, 2024
2 checks passed
@hiroshi-cl hiroshi-cl deleted the fix/dl2u_tmp_error branch October 31, 2024 14:59
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