simplification コマンドに --prepare オプションを追加した (#48)

* A view can be delta predicates with --prepare option.

* Add a sample code.

* Add some tests for simplification.

bin/dl2u.ml

@@ -11,7 +11,7 @@ let sort rules =
 
 let simplify rules sources =
   let open Result in
-  match Simplification.simplify rules sources with
+  match Simplification.simplify rules None sources with
   | Error err ->
       error @@ Simplification.string_of_error err
   | Result.Ok rules ->

bin/simplification.ml

@@ -1,5 +1,11 @@
 open Birds
 
+let build_view ast =
+  if Array.length Sys.argv >= 3 && Sys.argv.(2) = "--prepare" then
+    ast.Expr.view
+  else
+    None
+
 let _ =
   if Array.length Sys.argv < 2 then
     print_endline "Invalid arguments. File name must be passed."
@@ -10,11 +16,12 @@ let _ =
     let ast = Parser.main Lexer.token lexbuf in
     let rules = ast.rules in
     let sources = ast.sources in
+    let view = build_view ast in
     match Inlining.sort_rules rules with
     | Result.Error err ->
       print_endline @@ Inlining.string_of_error err
     | Result.Ok rules ->
-      match Simplification.simplify rules sources with
+      match Simplification.simplify rules view sources with
       | Result.Error err ->
         print_endline @@ Simplification.string_of_error err
       | Result.Ok rules ->

examples/simplification_prepare1.dl

@@ -0,0 +1,5 @@
+source x('A':int).
+view v('A':int).
+
++x(A) :- x(A), v(A), A <> 42.
+-x(A) :- +x(A), -v(A).

examples/simplification_prepare2.dl

@@ -0,0 +1,5 @@
+source x('A':int).
+view v('A':int).
+
++x(A) :- x(A), v(A), A <> 42.
+-x(A) :- +x(A), +v(A).

examples/simplification_prepare3.dl

@@ -0,0 +1,13 @@
+source b('B':int, 'C':int).
+source a('A':int, 'B':int).
+view v('A':int, 'B':int, 'C':int).
+-a(A, B) :- a(A, B) , not __updated__v(A, B, GENV1).
+-b(B, C) :- b(B, C) , a(GENV2, B) , b(B, GENV3) , not -v(GENV2, B, GENV3) , not __updated__v(GENV4, B, C).
+-b(B, C) :- b(B, C) , +v(GENV2, B, GENV3) , not __updated__v(GENV4, B, C).
++a(A, B) :- a(A, B) , b(B, GENV5) , not -v(A, B, GENV5) , not a(A, B).
++a(A, B) :- +v(A, B, GENV5) , not a(A, B).
++b(B, C) :- a(GENV6, B) , b(B, C) , not -v(GENV6, B, C) , not b(B, C).
++b(B, C) :- +v(GENV6, B, C) , not b(B, C).
+__updated__v(A, B, C) :- a(A, B) , b(B, C) , not -v(A, B, C).
+__updated__v(A, B, C) :- +v(A, B, C).
+v(A, B, C) :- a(A, B) , b(B, C).

examples/simplification_prepare4.dl

@@ -0,0 +1,10 @@
+source projs('A':int, 'B':string).
+view projv('A':int).
+-projs(A, B) :- projs(A, B) , -projv(A).
++projs(A, B) :- projs(A, GENV7) , not -projv(A) , not projs(A, GENV1) , not -projs(GENV2, GENV3) , B = 'a'.
++projs(A, B) :- projs(A, GENV8) , not -projv(A) , not projs(A, GENV4) , projs(GENV5, B) , -projv(GENV5).
++projs(A, B) :- +projv(A) , not projs(A, GENV1) , not -projs(GENV2, GENV3) , B = 'a'.
++projs(A, B) :- +projv(A) , not projs(A, GENV4) , projs(GENV5, B) , -projv(GENV5).
+__updated__projv(A) :- projs(A, GENV6) , not -projv(A).
+__updated__projv(A) :- +projv(A).
+projv(A) :- projs(A, B).

examples/simplification_prepare5.dl

@@ -0,0 +1,13 @@
+source uniona('NAME':string).
+source unionb('NAME':string).
+source uniono('NAME':string, 'TP':string).
+view unionview('NAME':string, 'TP':string).
+-uniona(N) :- uniona(N) , -unionview(N, T) , T = 'A'.
+-unionb(N) :- unionb(N) , -unionview(N, T) , T = 'B'.
+-uniono(N, T) :- uniono(N, T) , -unionview(N, T).
++uniona(N) :- +unionview(N, T) , not uniona(N) , T = 'A' , not uniono(N, T).
++unionb(N) :- +unionview(N, T) , not unionb(N) , T = 'B' , not uniono(N, T).
++uniono(N, T) :- +unionview(N, T) , not uniono(N, T) , not T = 'A' , not T = 'B'.
+unionview(N, T) :- uniona(N) , T = 'A'.
+unionview(N, T) :- unionb(N) , T = 'B'.
+unionview(N, T) :- uniono(N, T).

src/simplification.ml

@@ -585,7 +585,7 @@ let rec simplify_rule_recursively (imrule1 : intermediate_rule) : intermediate_r
     simplify_rule_recursively imrule2
 
 
-let resolve_undefined_predicates (imrules : intermediate_rule list) : intermediate_rule list =
+let resolve_undefined_predicates (view : PredicateSet.t) (imrules : intermediate_rule list) : intermediate_rule list =
   imrules
   |> List.fold_left (fun (preds_set, acc) imrule ->
     let { head_predicate; positive_terms; negative_terms; _ } = imrule in
@@ -620,15 +620,15 @@ let resolve_undefined_predicates (imrules : intermediate_rule list) : intermedia
         let preds_set = preds_set |> PredicateSet.add head_predicate in
         let imrule = { imrule with positive_terms; negative_terms } in
         (preds_set, imrule :: acc)
-  ) (PredicateSet.empty, [])
+  ) (view, [])
   |> snd
   |> List.rev
 
 
 module TableNameSet = Set.Make(String)
 
 
-let remove_unused_rules (sources : TableNameSet.t) (imrules : intermediate_rule list) : intermediate_rule list =
+let remove_unused_rules (sources : TableNameSet.t) (view : PredicateSet.t) (imrules : intermediate_rule list) : intermediate_rule list =
   List.fold_right (fun imrule (pred_set, acc) ->
     let { positive_terms; negative_terms; _ } = imrule in
     let terms = PredicateMap.union (fun _ x _ -> Some x) positive_terms negative_terms in
@@ -657,7 +657,7 @@ let remove_unused_rules (sources : TableNameSet.t) (imrules : intermediate_rule
         else
           (pred_set, acc)
 
-  ) imrules (PredicateSet.empty, [])
+  ) imrules (view, [])
   |> snd
 
 
@@ -781,7 +781,7 @@ let remove_duplicate_rules (rules : rule list) : rule list =
   with
   | (rules, _) -> rules
 
-let simplify (rules : rule list) (sources : source list) : (rule list, error) result =
+let simplify (rules : rule list) (view : view option) (sources : source list) : (rule list, error) result =
   let open ResultMonad in
 
   (* Converts each rule to an intermediate rule (with unsatisfiable ones removed): *)
@@ -794,8 +794,14 @@ let simplify (rules : rule list) (sources : source list) : (rule list, error) re
   (* Performs per-rule simplification: *)
   let imrules = imrules |> List.map simplify_rule_recursively in
 
+  let view =
+    match view with
+    | None      -> PredicateSet.empty
+    | Some (view, _) -> PredicateSet.of_list [ImDeltaInsert view; ImDeltaDelete view]
+  in
+
   (* Removes predicates that are not defined: *)
-  let imrules = imrules |> resolve_undefined_predicates in
+  let imrules = imrules |> resolve_undefined_predicates view in
 
   let sources =
     sources
@@ -804,7 +810,7 @@ let simplify (rules : rule list) (sources : source list) : (rule list, error) re
   in
 
   (* Removes rules that are not used: *)
-  let imrules = imrules |> remove_unused_rules sources in
+  let imrules = imrules |> remove_unused_rules sources view in
 
   (* Removes rules that have a contradicting body: *)
   let imrules = imrules |> List.filter (fun imrule -> not (has_contradicting_body imrule)) in

src/simplification.mli

@@ -3,6 +3,6 @@ open Expr
 
 type error
 
-val simplify : rule list -> source list -> (rule list, error) result
+val simplify : rule list -> view option -> source list -> (rule list, error) result
 
 val string_of_error : error -> string

test/ast2sql_operation_based_conversion_test.ml

@@ -210,7 +210,7 @@ let main () =
                   assert false
               | Ok rules ->
                 let sources = [ "a", []; "b", []; "v", [] ] in
-                match Simplification.simplify rules sources with
+                match Simplification.simplify rules None sources with
                 | Error err ->
                     Printf.printf "Error: %s\n" (Simplification.string_of_error err);
                     assert false