Merge pull request #29 from cedretaber/cedretaber/add-or-condition-to…

…-sql-where SQL WHERE 内での OR 条件に対応
proof-ninja · Sep 17, 2023 · df8a4c4 · df8a4c4
2 parents 44fef03 + c0fbb73
commit df8a4c4
Show file tree

Hide file tree

Showing 7 changed files with 146 additions and 39 deletions.
diff --git a/examples/update_or.dl b/examples/update_or.dl
@@ -0,0 +1 @@
+view t('A':string, 'B':string, 'C':string, 'D':string, 'E':string).
diff --git a/examples/update_or.sql b/examples/update_or.sql
@@ -0,0 +1,3 @@
+UPDATE t
+SET A = 'a', B = 'b'
+WHERE C = 'x' AND D = 'y' OR E = 'z';
diff --git a/src/sql/ast.ml b/src/sql/ast.ml
@@ -4,7 +4,6 @@ type binary_operator =
   | Minus   (* - *)
   | Times   (* * *)
   | Divides (* / *)
-  | Lor     (* || *)
 
 type unary_operator =
   | Negate (* - *)
@@ -38,21 +37,20 @@ type vterm =
 type sql_constraint =
   | Constraint of vterm * operator * vterm
 
-type where_clause =
-  | Where of sql_constraint list
+type where_clause = sql_constraint list
 
 type insert_value = vterm list
 
+(** The WHERE clause combines multiple constraints joined by AND conditions with OR conditions. *)
 type statement =
   | InsertInto of table_name * insert_value list
-  | UpdateSet of table_name * (column * vterm) list * where_clause option
+  | UpdateSet of table_name * (column * vterm) list * where_clause list
 
 let string_of_binary_operator = function
   | Plus    -> "+"
   | Minus   -> "-"
   | Times   -> "*"
   | Divides -> "/"
-  | Lor     -> "||"
 
 let string_of_unary_operator = function
   | Negate -> "-"
@@ -120,12 +118,16 @@ let to_string = function
       |> List.map string_of_set
       |> String.concat "\n"
     ) ^
-    match where with
-    | None -> ""
-    | Some (Where cs) ->
+    if List.length where = 0 then
+      ""
+    else
       "\nWHERE\n" ^ (
-        cs
-        |> List.map (fun c -> "  " ^ string_of_constraint c)
-        |> String.concat "\n"
+        where
+        |> List.map (fun cs ->
+          cs
+          |> List.map (fun c -> "  " ^ string_of_constraint c)
+          |> String.concat " AND "
+        )
+        |> String.concat " OR\n"
       )
     ^ "\n;"
diff --git a/src/sql/lexer.mll b/src/sql/lexer.mll
@@ -30,6 +30,8 @@
         "SET", SET;
         "and", AND;
         "AND", AND;
+        "or", OR;
+        "OR", OR;
     ]
 }
 let digit = ['0'-'9']
@@ -56,7 +58,6 @@ rule token = parse
   | "NULL" | "null" { NULL }
   | '=' { EQUAL }
   | '*' { ASTERISK }
-  | "||" { CONCAT_OP }
   | '/' { NUM_DIV_OP }
   | "!=" | "<>" { NUM_NEQ_OP }
   | '+' { PLUS }

diff --git a/src/sql/parser.mly b/src/sql/parser.mly
@@ -2,10 +2,10 @@
 %token <string> IDENT TEXT
 %token <float> FLOAT
 %token LPAREN RPAREN COMMA EOF DOT NULL
-%token INSERT INTO VALUES UPDATE WHERE EQUAL ASTERISK SET AND CONCAT_OP
+%token INSERT INTO VALUES UPDATE WHERE EQUAL ASTERISK SET AND OR
 %token NUM_DIV_OP NUM_NEQ_OP PLUS MINUS
 
-%left CONCAT_OP
+%left OR
 %left AND
 %nonassoc EQUAL NUM_NEQ_OP
 %left PLUS MINUS
@@ -30,7 +30,7 @@
   ;
 
   update:
-  | UPDATE table=IDENT SET ss=commas(set_column) w=where? { Ast.UpdateSet (table, ss, w) }
+  | UPDATE table=IDENT SET ss=commas(set_column) ws=wheres? { Ast.UpdateSet (table, ss, Option.value ~default:[] ws) }
   ;
 
   set_column:
@@ -67,11 +67,14 @@
   | MINUS { Ast.Minus }
   | ASTERISK { Ast.Times }
   | NUM_DIV_OP { Ast.Divides }
-  | CONCAT_OP { Ast.Lor }
+  ;
+
+  wheres:
+  | WHERE ws=ors(where) { ws }
   ;
 
   where:
-  | WHERE cs=ands(sql_constraint) { Ast.Where cs }
+  | cs=ands(sql_constraint) { cs }
   ;
 
   sql_constraint:
@@ -85,4 +88,5 @@
   ;
 
 %inline commas(X): l=separated_nonempty_list(COMMA, X) { l }
+%inline ors(X): l=separated_nonempty_list(OR, X) { l }
 %inline ands(X): l=separated_nonempty_list(AND, X) { l }
diff --git a/src/sql2ast.ml b/src/sql2ast.ml
@@ -42,17 +42,16 @@ let rec ast_vterm_of_sql_vterm colvarmap = function
       let op = Sql.string_of_binary_operator op in
       ResultMonad.return (Expr.BinaryOp (op, left, right))
 
-let ast_terms_of_sql_where_clause colvarmap = function
-  | Sql.Where sql_constraints ->
-    let ast_term_of_sql_constraint = function
-      | Sql.Constraint (left, op, right) ->
-          let op = Sql.string_of_operator op in
-          ast_vterm_of_sql_vterm colvarmap left >>= fun left ->
-          ast_vterm_of_sql_vterm colvarmap right >>= fun right ->
-          ResultMonad.return (Expr.Equat (Expr.Equation (op, left, right))) in
-    ResultMonad.mapM
-      ast_term_of_sql_constraint
-      sql_constraints
+let ast_terms_of_sql_where_clause colvarmap sql_constraints =
+  let ast_term_of_sql_constraint = function
+    | Sql.Constraint (left, op, right) ->
+        let op = Sql.string_of_operator op in
+        ast_vterm_of_sql_vterm colvarmap left >>= fun left ->
+        ast_vterm_of_sql_vterm colvarmap right >>= fun right ->
+        ResultMonad.return (Expr.Equat (Expr.Equation (op, left, right))) in
+  ResultMonad.mapM
+    ast_term_of_sql_constraint
+    sql_constraints
 
 let build_effects colvarmap column_and_vterms =
   (*
@@ -69,17 +68,20 @@ let build_effects colvarmap column_and_vterms =
         >>= fun var ->
       ResultMonad.return (Expr.Equat (Expr.Equation ("<>", Expr.Var var, vterm))))
 
-let build_deletion_rule colvarmap where_clause table_name varlist effect_term =
+let build_deletion_rules colvarmap where_clause table_name varlist effect_term =
   (* Constraints corresponding to the WHERE clause. May be empty. *)
   where_clause
-    |> Option.map (ast_terms_of_sql_where_clause colvarmap)
-    |> Option.value ~default:(Ok([]))
-    >>= fun body ->
+    |> ResultMonad.mapM (ast_terms_of_sql_where_clause colvarmap)
+    >>= fun bodies ->
 
   (* Create a rule corresponding to the operation to delete the record to be updated. *)
   let delete_pred = Expr.Deltadelete (table_name, varlist) in
   let from = Expr.Pred (table_name, varlist) in
-  ResultMonad.return (delete_pred, (Expr.Rel from :: body @ [effect_term]))
+
+  ResultMonad.return (
+    bodies
+    |> List.map (fun body -> delete_pred, (Expr.Rel from :: body @ [effect_term]))
+  )
 
 let build_creation_rule colvarmap colvarmap' column_and_vterms table_name columns varlist =
   (* Create an expression equivalent to a SET clause in SQL. *)
@@ -191,7 +193,9 @@ let update_to_datalog table_name column_and_vterms where_clause (columns : Sql.c
 
   build_effects colvarmap column_and_vterms
   >>= fun effect_terms ->
-  ResultMonad.mapM (build_deletion_rule colvarmap where_clause table_name varlist) effect_terms
+  effect_terms
+  |> ResultMonad.mapM (build_deletion_rules colvarmap where_clause table_name varlist)
+  |> ResultMonad.map List.flatten
   >>= fun deletes ->
   build_creation_rule colvarmap colvarmap' column_and_vterms table_name columns varlist
   >>= fun insert ->

diff --git a/test/sql2ast_test.ml b/test/sql2ast_test.ml
@@ -73,13 +73,13 @@ let main () =
         Sql.UpdateSet (
           "ced",
           [(None, "dname"), Sql.Const (String "'R&D'")],
-          Some (Sql.Where ([
+          [[
             Sql.Constraint (
               Sql.Column (None, "dname"),
               Sql.RelEqual,
               Sql.Const (String "'Dev'")
             )
-          ]))
+          ]]
         ),
         ["ename"; "dname"]
       );
@@ -130,7 +130,7 @@ let main () =
             (None, "c3"), Sql.Const (String "'v3'");
             (None, "c5"), Sql.Const (String "'v5'")
           ],
-          Some (Sql.Where ([
+          [[
             Sql.Constraint (
               Sql.Column (None, "c2"),
               Sql.RelEqual,
@@ -141,7 +141,7 @@ let main () =
               Sql.RelEqual,
               Sql.Const (String "'v100'")
             )
-          ]))
+          ]]
         ),
         ["c1"; "c2"; "c3"; "c4"; "c5"; "c6"]
       );
@@ -207,7 +207,7 @@ let main () =
             (None, "c1"), Sql.Column (None, "c2");
             (None, "c2"), Sql.Column (None, "c3")
           ],
-          Some (Sql.Where ([]))
+          [[]]
         ),
         ["c1"; "c2"; "c3"; "c4"]
       );
@@ -236,6 +236,98 @@ let main () =
         )
       ]
     };
+    {
+      title = "Use OR condition.";
+      (*
+       * SQL:
+       *   UPDATE t
+       *   SET A = 'a', B = 'b'
+       *   WHERE C = 'x' AND D = 'y' OR E = 'z';
+       *
+       * datalog:
+       *   -t(GENV1, GENV2, GENV3, GENV4, GENV5) :- t(GENV1, GENV2, GENV3, GENV4, GENV5), GENV3 = 'x', GENV4 = 'y', GENV1 <> 'a'.
+       *   -t(GENV1, GENV2, GENV3, GENV4, GENV5) :- t(GENV1, GENV2, GENV3, GENV4, GENV5), GENV5 = 'z', GENV1 <> 'a'.
+       *   -t(GENV1, GENV2, GENV3, GENV4, GENV5) :- t(GENV1, GENV2, GENV3, GENV4, GENV5), GENV3 = 'x', GENV4 = 'y', GENV2 <> 'b'.
+       *   -t(GENV1, GENV2, GENV3, GENV4, GENV5) :- t(GENV1, GENV2, GENV3, GENV4, GENV5), GENV5 = 'z', GENV2 <> 'b'.
+       *   +t(GENV1, GENV2, GENV3, GENV4, GENV5) :- GENV1 = 'a', GENV2 = 'b', -t(GENV1_2, GENV2_2, GENV3, GENV4, GENV5)
+       *
+       *)
+      input = (
+        Sql.UpdateSet (
+          "t",
+          [
+            (None, "A"), Sql.Const (String "'a'");
+            (None, "B"), Sql.Const (String "'b'");
+          ],
+          [
+            [
+              Sql.Constraint (
+                Sql.Column (None, "C"),
+                Sql.RelEqual,
+                Sql.Const (String "'x'")
+              );
+              Sql.Constraint (
+                Sql.Column (None, "D"),
+                Sql.RelEqual,
+                Sql.Const (String "'y'")
+              )
+            ];
+            [
+              Sql.Constraint (
+                Sql.Column (None, "E"),
+                Sql.RelEqual,
+                Sql.Const (String "'z'")
+              )
+            ]
+          ]
+        ),
+        ["A"; "B"; "C"; "D"; "E"]
+      );
+      expected = [
+        (
+          Deltadelete ("t", [NamedVar "GENV1"; NamedVar "GENV2"; NamedVar "GENV3"; NamedVar "GENV4"; NamedVar "GENV5"]),
+          [
+            Rel (Pred ("t", [NamedVar "GENV1"; NamedVar "GENV2"; NamedVar "GENV3"; NamedVar "GENV4"; NamedVar "GENV5"]));
+            Equat (Equation ("=", (Var (NamedVar "GENV3")), (Var (ConstVar (String "'x'")))));
+            Equat (Equation ("=", (Var (NamedVar "GENV4")), (Var (ConstVar (String "'y'")))));
+            Equat (Equation ("<>", (Var (NamedVar "GENV1")), (Var (ConstVar (String "'a'")))))
+          ]
+        );
+        (
+          Deltadelete ("t", [NamedVar "GENV1"; NamedVar "GENV2"; NamedVar "GENV3"; NamedVar "GENV4"; NamedVar "GENV5"]),
+          [
+            Rel (Pred ("t", [NamedVar "GENV1"; NamedVar "GENV2"; NamedVar "GENV3"; NamedVar "GENV4"; NamedVar "GENV5"]));
+            Equat (Equation ("=", (Var (NamedVar "GENV5")), (Var (ConstVar (String "'z'")))));
+            Equat (Equation ("<>", (Var (NamedVar "GENV1")), (Var (ConstVar (String "'a'")))))
+          ]
+        );
+        (
+          Deltadelete ("t", [NamedVar "GENV1"; NamedVar "GENV2"; NamedVar "GENV3"; NamedVar "GENV4"; NamedVar "GENV5"]),
+          [
+            Rel (Pred ("t", [NamedVar "GENV1"; NamedVar "GENV2"; NamedVar "GENV3"; NamedVar "GENV4"; NamedVar "GENV5"]));
+            Equat (Equation ("=", (Var (NamedVar "GENV3")), (Var (ConstVar (String "'x'")))));
+            Equat (Equation ("=", (Var (NamedVar "GENV4")), (Var (ConstVar (String "'y'")))));
+            Equat (Equation ("<>", (Var (NamedVar "GENV2")), (Var (ConstVar (String "'b'")))))
+          ]
+        );
+        (
+          Deltadelete ("t", [NamedVar "GENV1"; NamedVar "GENV2"; NamedVar "GENV3"; NamedVar "GENV4"; NamedVar "GENV5"]),
+          [
+            Rel (Pred ("t", [NamedVar "GENV1"; NamedVar "GENV2"; NamedVar "GENV3"; NamedVar "GENV4"; NamedVar "GENV5"]));
+            Equat (Equation ("=", (Var (NamedVar "GENV5")), (Var (ConstVar (String "'z'")))));
+            Equat (Equation ("<>", (Var (NamedVar "GENV2")), (Var (ConstVar (String "'b'")))))
+          ]
+        );
+        (
+          Deltainsert ("t", [NamedVar "GENV1"; NamedVar "GENV2"; NamedVar "GENV3"; NamedVar "GENV4"; NamedVar "GENV5"]),
+          [
+            Equat (Equation ("=", (Var (NamedVar "GENV1")), (Var (ConstVar (String "'a'")))));
+            Equat (Equation ("=", (Var (NamedVar "GENV2")), (Var (ConstVar (String "'b'")))));
+            Rel (Deltadelete ("t", [NamedVar "GENV1_2"; NamedVar "GENV2_2"; NamedVar "GENV3"; NamedVar "GENV4"; NamedVar "GENV5"]));
+          ]
+        )
+      ]
+    };
     {
       title = "Basic INSERT";
       (*