Merge pull request #39 from hiroshi-cl/feat/incrementalization_step2

Effect-basedへの変換 Step2

bin/dune

@@ -33,3 +33,10 @@
  (name parse)
  (modules parse)
  (libraries birds sql))
+
+(executable
+  (public_name s2e)
+  (name s2e)
+  (modules s2e)
+  (libraries birds))
+

bin/s2e.ml

@@ -0,0 +1,17 @@
+open Birds
+
+let _ =
+  if Array.length Sys.argv < 2 then
+    print_endline "Invalid arguments. File name must be passed."
+  else begin
+    let filename = Sys.argv.(1) in
+    let chan = open_in filename in
+    let lexbuf = Lexing.from_channel chan in
+    let ast = Parser.main Lexer.token lexbuf in
+    match Incrementalization.incrementalization_ast ast with
+    | Result.Error err ->
+      print_endline @@ Incrementalization.string_of_error err
+    | Result.Ok rules ->
+      let ast = Expr.{ ast with rules } in
+      print_endline @@ Expr.to_string ast
+  end

examples/incrementalization1.dl

@@ -0,0 +1,9 @@
+source ed('EMP_NAME':string,'DEPT_NAME':string).
+source eed('EMP_NAME':string,'DEPT_NAME':string).
+view ced('EMP_NAME':string, 'DEPT_NAME':string).
+
+ced(E,D) :- ed(E,D), not eed(E,D).
+
++ed(E, D) :- ced(E, D), NOT ed(E, D).
+-eed(E, D) :- ced(E, D), eed(E, D).
++eed(E, D) :- ed(E, D), NOT ced(E, D), NOT eed(E, D).

examples/incrementalization1_random.dl

@@ -0,0 +1,8 @@
+source ed('EMP_NAME':string,'DEPT_NAME':string).
+source eed('EMP_NAME':string,'DEPT_NAME':string).
+view ced('EMP_NAME':string, 'DEPT_NAME':string).
+
+-eed(E, D) :- ced(E, D), eed(E, D).
++eed(E, D) :- ed(E, D), NOT ced(E, D), NOT eed(E, D).
++ed(E, D) :- ced(E, D), NOT ed(E, D).
+ced(E,D) :- ed(E,D), not eed(E,D).

examples/incrementalization2.dl

@@ -0,0 +1,9 @@
+source s('A':int, 'B':string).
+view v('A':int).
+
+%view definition
+v(A) :- s(A,B).
+
+-s(A,B) :- s(A,B), not v(A).
++s(A,B) :- v(A), not s(A,_), not -s(_,_), B='a'.
++s(A,B) :- v(A), not s(A,_), -s(_,B).

examples/incrementalization2_without_anonymous.dl

@@ -0,0 +1,9 @@
+source s('A':int, 'B':string).
+view v('A':int).
+
+%view definition
+v(A) :- s(A,B).
+
+-s(A,B) :- s(A,B), not v(A).
++s(A,B) :- v(A), not s(A,B), not -s(A,B), B='a'.
++s(A,B) :- v(A), not s(A,B), -s(A,B).

examples/incrementalization2_without_anonymous_a.dl

@@ -0,0 +1,7 @@
+source s('A':int, 'B':string).
+view v('A':int).
+
+%view definition
+v(A) :- s(A,B).
+
+-s(A,B) :- s(A,B), not v(A).

examples/incrementalization2_without_anonymous_b.dl

@@ -0,0 +1,8 @@
+source s('A':int, 'B':string).
+view v('A':int).
+
+%view definition
+v(A) :- s(A,B).
+
+-s(A,B) :- s(A,B), not v(A).
++s(A,B) :- v(A), not s(A,B), not -s(A,B), B='a'.

examples/incrementalization2_without_anonymous_c.dl

@@ -0,0 +1,8 @@
+source s('A':int, 'B':string).
+view v('A':int).
+
+%view definition
+v(A) :- s(A,B).
+
+-s(A,B) :- s(A,B), not v(A).
++s(A,B) :- v(A), not s(A,B), -s(A,B).

examples/incrementalization3.dl

@@ -0,0 +1,21 @@
+source b('B':string, 'C':real).
+source a('A':real, 'B':string).
+view v('A':real, 'B':string, 'C':real).
+
+% primary key
+% A -> B on view v
+_|_ :- v(A, B1, _), v(A, B2, _), B1 <> B2.
+% B -> C on view v
+_|_ :- v(_, B, C1), v(_, B, C2), C1 <> C2.
+
+% foreign key
+_|_ :- a(_, B), not b(B, _).
+
+% view definition
+v(A, B, C) :- a(A, B), b(B, C).
+
+% update strategy
+-a(A, B) :- a(A, B), not v(A, B, _).
+-b(B, C) :- b(B, C), v(_, B, _), not v(_, B, C).
++a(A, B) :- v(A, B, _), not a(A, B).
++b(B, C) :- v(_, B, C), not b(B, C).

src/incrementalization.ml

@@ -0,0 +1,126 @@
+
+open Expr
+open Utils
+open Rule_abstraction
+open Sorted_rules
+
+(** The prefix used for variables generated during incrementalization. *)
+let updated_variable_prefix = "__updated__"
+
+type error = Rule_abstraction.error
+
+let string_of_intermediate_predicate = function
+  | ImPred table        -> Printf.sprintf "%s" table
+  | ImDeltaInsert table -> Printf.sprintf "+%s" table
+  | ImDeltaDelete table -> Printf.sprintf "-%s" table
+
+let string_of_error = function
+  | UnexpectedHeadVarForm var ->
+      Printf.sprintf "unexpected head var form: %s" (string_of_var var)
+  | UnexpectedBodyVarForm var ->
+      Printf.sprintf "unexpected body var form: %s" (string_of_var var)
+  | NoViewVariable ->
+      "There is no view in this program."
+  | CyclicDependency defs ->
+    let s =
+      defs |>
+      List.map (fun (impred, _) -> string_of_intermediate_predicate impred) |>
+      String.concat ", "
+    in
+    Printf.sprintf "cyclic dependency found among %s" s
+
+let incrementalization_ast (ast: expr): (rule list, error) result =
+  let open ResultMonad in
+
+  match ast.view with
+    | Some (view_name, params) ->
+      let updated_view_name = updated_variable_prefix ^ view_name  in
+
+      let intermediate_rules =
+        let param_vars = params |> List.map(fun (var_name, _) -> NamedVar(var_name)) in
+
+        let delete_rule = Pred (updated_view_name, param_vars), Rel (Pred (view_name, param_vars)) :: Not (Deltadelete (view_name, param_vars)) :: [] in
+
+        let insert_rule = Pred (updated_view_name, param_vars), Rel (Deltainsert (view_name, param_vars)) :: [] in
+
+        delete_rule :: insert_rule :: []
+      in
+
+      let convert_not_linear_rule_abstraction (ruleabs: rule_abstraction): rule_abstraction =
+        let replace_name (name: string): string =
+          if name = view_name then updated_view_name else name 
+        in
+
+        let convert_intermediate_predicate: intermediate_predicate -> intermediate_predicate = function
+          | ImPred table_name -> ImPred (replace_name table_name)
+          | ImDeltaInsert table_name -> ImDeltaInsert (replace_name table_name)
+          | ImDeltaDelete table_name -> ImDeltaDelete (replace_name table_name)
+        in
+
+        let convert_intermediate_clause: intermediate_clause -> intermediate_clause = function
+          | ImPositive (pred, vars) -> ImPositive (convert_intermediate_predicate pred, vars)
+          | ImNegative (pred, vars) -> ImNegative (convert_intermediate_predicate pred, vars)
+          | ImEquation  eterm -> ImEquation  eterm
+          | ImNonequation eterm -> ImNonequation eterm
+          | ImConstTerm bool -> ImConstTerm bool
+        in
+
+        { binder = ruleabs.binder; body = ruleabs.body |> List.map convert_intermediate_clause; }
+      in
+
+      let convert_linear_rule_abstraction (ruleabs: rule_abstraction): rule_abstraction =
+        let convert_intermediate_clause: intermediate_clause -> intermediate_clause = function
+          | ImPositive (ImPred table_name, vars) ->
+            if table_name = view_name then ImPositive (ImDeltaInsert table_name, vars) else ImPositive (ImPred table_name, vars)
+          | ImNegative (ImPred table_name, vars) ->
+            if table_name = view_name then ImPositive (ImDeltaDelete table_name, vars) else ImNegative (ImPred table_name, vars)
+          | ImPositive (intermediate_predicate, vars) -> ImPositive (intermediate_predicate, vars)
+          | ImNegative (intermediate_predicate, vars) -> ImNegative (intermediate_predicate, vars)
+          | ImEquation  eterm -> ImEquation  eterm
+          | ImNonequation eterm -> ImNonequation eterm
+          | ImConstTerm bool -> ImConstTerm bool
+        in
+
+        { binder = ruleabs.binder; body = ruleabs.body |> List.map convert_intermediate_clause; }
+      in
+
+      sort_rules ast.rules >>= fun sorted_predicate_definitions ->
+
+      let (infos, converted_rules) =
+        List.fold_left (fun acc predicate_definition ->
+
+          let (acc_infos, acc_rules) = acc in
+          let (impred, ruleabs_set) = predicate_definition in
+
+          let (results, rules) =
+            ruleabs_set |>
+            RuleAbstractionSet.to_list |>
+            List.map (fun ruleabs ->
+              let result = Lvgn.linear_view_result_of_rule_abstraction view_name acc_infos ruleabs in
+
+              let converted_ruleabs =
+                if Result.is_error result then
+                  convert_not_linear_rule_abstraction ruleabs
+                else
+                  convert_linear_rule_abstraction ruleabs
+              in
+
+              (result, Rule_abstraction.inject_rule impred converted_ruleabs)
+            ) |>
+            List.split
+          in
+
+          (PredicateMap.add impred (Lvgn.merge_linear_view_result_for_predicate_definition results) acc_infos, rules :: acc_rules)
+
+        ) (PredicateMap.empty, []) sorted_predicate_definitions
+      in
+
+      return (
+        if (PredicateMap.exists (fun _ -> Result.is_error) infos) then
+          List.flatten (intermediate_rules :: List.rev converted_rules)
+        else
+          List.flatten (List.rev converted_rules)
+      )
+
+    | None -> err NoViewVariable
+

src/incrementalization.mli

@@ -0,0 +1,8 @@
+
+open Expr
+
+type error
+
+val string_of_error : error -> string
+
+val incrementalization_ast : expr -> (rule list, error) result

src/lvgn.ml

@@ -0,0 +1,142 @@
+open Rule_abstraction
+open Utils.ResultMonad
+
+type linear_view_info = {
+  view_parameters: bool list;
+  poc: int;
+  soc: int;
+}
+
+type linear_view_result = (linear_view_info, unit) result
+
+type predicate_definition_linear_view_infos = linear_view_result PredicateMap.t
+
+let swap_result_list (list: ('a, 'e) result list): ('a list, 'e) result =
+  List.fold_left (fun a b -> match (a, b) with
+    | _, Result.Error e -> Result.error e
+    | Result.Error e, _ -> Result.error e
+    | Result.Ok xs, Result.Ok y -> Result.ok (y :: xs)
+  ) (Result.ok []) list
+
+let linear_view_result_of_rule_abstraction (view_name: string) (infos: predicate_definition_linear_view_infos) (rule: rule_abstraction): linear_view_result =
+  let is_view_predicate = function
+    | ImPred name -> name = view_name
+    | ImDeltaInsert _ -> false
+    | ImDeltaDelete _ -> false
+  in
+
+  let merge_view_parameter_list (list: bool list list): bool list =
+    List.fold_left (List.map2(||)) (List.hd list) (List.tl list)
+  in
+
+  let merge_view_parameter_result_list (list: (bool list, unit) result list): (bool list, unit) result =
+    list |>
+    swap_result_list |>
+    Result.map merge_view_parameter_list
+  in
+
+  let process_bound_predicate (binder: named_var list) (predicate: intermediate_predicate) (arguments: intermediate_argument list): (bool list, unit) result  =
+    (
+      if is_view_predicate predicate then
+        arguments |> List.map(fun a -> (a, true)) |> Result.ok
+      else
+        match PredicateMap.find_opt predicate infos with
+          | Some (Result.Ok info) -> List.combine arguments info.view_parameters |> Result.ok
+          | Some (Result.Error _) -> Result.error ()
+          | None -> arguments |> List.map(fun a -> (a, false)) |> Result.ok (* source or built-in predicate *)
+    ) >>= fun bound_pair ->
+
+    let has_anonymous_view_patermeters =
+      bound_pair |> 
+      List.exists (function
+        | ImAnonVarArg, true -> true
+        | _ -> false
+      )
+    in
+
+    let view_argument_names =
+      bound_pair |> 
+      List.filter_map (function
+        | ImNamedVarArg named_var, true -> Some named_var
+        | _ -> None
+      )
+    in
+
+    if has_anonymous_view_patermeters then
+      Result.error ()
+    else
+      binder |> List.map(fun v -> List.mem v view_argument_names) |> Result.ok
+  in
+
+  let process_intermediate_clause (binder: named_var list) (clause: intermediate_clause): (bool list, unit) result =
+    match clause with
+      | ImPositive (predicate, arguments) -> process_bound_predicate binder predicate arguments
+      | ImNegative (predicate, arguments) -> process_bound_predicate binder predicate arguments
+      | ImEquation    _ -> binder |> List.map(fun _ -> false) |> Result.ok
+      | ImNonequation _ -> binder |> List.map(fun _ -> false) |> Result.ok
+      | ImConstTerm   _ -> binder |> List.map(fun _ -> false) |> Result.ok
+  in
+
+  (
+    rule.body |>
+    List.map (process_intermediate_clause rule.binder) |>
+    merge_view_parameter_result_list
+  ) >>= fun parameters_of_rule_abstraction ->
+
+  let poc_of_predicate (predicate: intermediate_predicate): (int, unit) result =
+    if is_view_predicate predicate then
+      Result.ok 1
+    else
+      match PredicateMap.find_opt predicate infos with
+        | Some(Result.Ok info) -> Result.ok info.poc
+        | Some(Result.Error _) -> Result.error ()
+        | None -> Result.ok 0
+  in
+
+  let poc_of_intermediate_clause (clause: intermediate_clause): (int, unit) result =
+    match clause with
+      | ImPositive (predicate, _) -> poc_of_predicate predicate
+      | ImNegative (predicate, _) -> poc_of_predicate predicate |> Result.map (min 1)
+      | ImEquation    _ -> Result.ok 0
+      | ImNonequation _ -> Result.ok 0
+      | ImConstTerm   _ -> Result.ok 0
+  in
+
+  (
+    rule.body |>
+    List.map poc_of_intermediate_clause |>
+    swap_result_list |>
+    Result.map (List.fold_left max 0)
+  ) >>= fun poc_of_rule_abstraction ->
+
+  let soc_of_intermediate_clause (clause: intermediate_clause): (int, unit) result =
+    match clause with
+      | ImPositive (predicate, _) -> poc_of_predicate predicate |> Result.map (min 1)
+      | ImNegative (predicate, _) -> poc_of_predicate predicate
+      | ImEquation    _ -> Result.ok 0
+      | ImNonequation _ -> Result.ok 0
+      | ImConstTerm   _ -> Result.ok 0
+  in
+
+  (
+    rule.body |>
+    List.map soc_of_intermediate_clause |>
+    swap_result_list |>
+    Result.map (List.fold_left (+) 0)
+  ) >>= fun soc_of_rule_abstraction ->
+
+  if soc_of_rule_abstraction <= 1 then
+    Result.ok { view_parameters = parameters_of_rule_abstraction; poc = poc_of_rule_abstraction; soc = soc_of_rule_abstraction; }
+  else
+    Result.error ()
+
+let merge_linear_view_result_for_predicate_definition (list: linear_view_result list): linear_view_result =
+  List.fold_left (fun r s -> match (r, s) with
+      | Result.Ok i, Result.Ok j -> 
+        Result.ok {
+          view_parameters = List.map2 (||) i.view_parameters j.view_parameters;
+          poc = i.poc + j.poc;
+          soc = max i.soc j.soc;
+        }
+      | _, _ -> Result.error ()
+    ) (List.hd list) (List.tl list)