diff --git a/bin/inlining.ml b/bin/inlining.ml index c8a3dce..06b4f5f 100644 --- a/bin/inlining.ml +++ b/bin/inlining.ml @@ -9,7 +9,14 @@ let _ = let lexbuf = Lexing.from_channel chan in let ast = Parser.main Lexer.token lexbuf in let rules = ast.rules in - match Inlining.inline_rules rules with + let mode = + if Array.length Sys.argv < 3 then + Inlining.All + else + let target = Inlining.TableNameSet.singleton Sys.argv.(2) in + Inlining.Just target + in + match Inlining.inline_rules mode rules with | Result.Error err -> print_endline @@ Inlining.string_of_error err | Result.Ok rules -> diff --git a/examples/inlining4.dl b/examples/inlining4.dl new file mode 100644 index 0000000..ab71656 --- /dev/null +++ b/examples/inlining4.dl @@ -0,0 +1,7 @@ +a(X) :- X = 1. +a(X) :- X = 2. + +b(X) :- X = 1. +b(X) :- X = 2. + +f(X) :- a(X), NOT b(X). diff --git a/src/inlining.ml b/src/inlining.ml index c553d72..5089748 100644 --- a/src/inlining.ml +++ b/src/inlining.ml @@ -2,6 +2,13 @@ open Expr open Utils +module TableNameSet = Set.Make(String) + +(** Select whether all predicates should be inlining or only certain predicates should be inlining. *) +type inlining_mode = + | All + | Just of TableNameSet.t + (** The prefix used for variables generated during inlining. *) let generated_variable_prefix = "GENV" @@ -438,14 +445,24 @@ let negate_rule_abstractions (state : state) (ruleabss : rule_abstraction list) |> List.map (fun body -> { binder; body }) ) +let is_inlined (mode : inlining_mode) (pred : intermediate_predicate) : bool = + match mode with + | All -> true + | Just tables -> tables |> TableNameSet.mem ( + match pred with + | ImPred table -> table + | ImDeltaInsert table -> table + | ImDeltaDelete table -> table + ) + (** `inline_rule_abstraction state improg_inlined ruleabs` performs inlining of `ruleabs` by using `improg_inlined`, which consists of "already inlined" definitions. *) -let inline_rule_abstraction (state : state) (improg_inlined : intermediate_program) (ruleabs : rule_abstraction) : (state * rule_abstraction list, error) result = +let inline_rule_abstraction (state : state) (mode : inlining_mode) (improg_inlined : intermediate_program) (ruleabs : rule_abstraction) : (state * rule_abstraction list, error) result = let open ResultMonad in let { binder; body } = ruleabs in body |> foldM (fun ((state, accs) : state * (intermediate_clause list) list) (clause : intermediate_clause) -> match clause with - | ImPositive (impred, imargs) -> + | ImPositive (impred, imargs) when is_inlined mode impred -> begin match improg_inlined |> PredicateMap.find_opt impred with | Some ruleabsset -> @@ -501,7 +518,7 @@ let inject_rule (impred : intermediate_predicate) (ruleabs : rule_abstraction) : let terms = body |> List.map inject_clause in (rterm, terms) -let inline_rules (rules : rule list) : (rule list, error) result = +let inline_rules (mode : inlining_mode) (rules : rule list) : (rule list, error) result = let open ResultMonad in (* Converts rules into intermediate ones @@ -519,7 +536,7 @@ let inline_rules (rules : rule list) : (rule list, error) result = sorted_rules |> foldM (fun (state, improg_inlined) (impred, ruleabsset) -> let ruleabss = RuleAbstractionSet.elements ruleabsset in ruleabss |> foldM (fun (state, ruleabss_inlined) ruleabs -> - ruleabs |> inline_rule_abstraction state improg_inlined >>= fun (state, ruleabss_inlined_new) -> + ruleabs |> inline_rule_abstraction state mode improg_inlined >>= fun (state, ruleabss_inlined_new) -> return (state, List.append ruleabss_inlined ruleabss_inlined_new) ) (state, []) >>= fun (state, ruleabss_inlined) -> return (state, improg_inlined |> PredicateMap.add impred (RuleAbstractionSet.of_list ruleabss_inlined)) diff --git a/test/inlining_test.ml b/test/inlining_test.ml index 8d9e1e2..3187efa 100644 --- a/test/inlining_test.ml +++ b/test/inlining_test.ml @@ -6,6 +6,7 @@ open Expr type test_case = { title : string; input : rule list; + mode : Inlining.inlining_mode; expected : string; } @@ -18,7 +19,7 @@ let run_test (test_case : test_case) : (test_result, Inlining.error) result = let open ResultMonad in let expected = test_case.expected in - Inlining.inline_rules test_case.input >>= fun rules_output -> + Inlining.inline_rules test_case.mode test_case.input >>= fun rules_output -> let got = rules_output |> List.map string_of_rule |> String.concat "" in if String.equal got test_case.expected then @@ -64,6 +65,7 @@ let main () = { title = "inlining the empty program"; input = []; + mode = Inlining.All; expected = ""; }; { @@ -75,6 +77,7 @@ let main () = (* Input: +foo(X) :- bar(X). bar(Y) :- qux(Y). *) + mode = Inlining.All; expected = make_lines [ "+foo(X) :- qux(X)."; @@ -90,6 +93,7 @@ let main () = (* Input: +foo(X) :- bar(X, _). bar(A, B) :- qux(A, B, _). *) + mode = Inlining.All; expected = make_lines [ "+foo(X) :- qux(X, GENV1, GENV3)."; @@ -108,6 +112,7 @@ let main () = (* Input: +foo(X, Y) :- bar(X, _), bar(Y, _). bar(A, B) :- qux(A, B, _). *) + mode = Inlining.All; expected = make_lines [ "+foo(X, Y) :- qux(X, GENV1, GENV4) , qux(Y, GENV2, GENV5)."; @@ -125,6 +130,7 @@ let main () = +foo(X) :- bar(X). bar(A) :- qux(A, _). bar(B) :- thud(_, B). *) + mode = Inlining.All; expected = make_lines [ "+foo(X) :- qux(X, GENV3)."; @@ -145,6 +151,7 @@ let main () = (* Input: +foo(X) :- bar(X). bar(B) :- qux(A, B), A = 42. *) + mode = Inlining.All; expected = make_lines [ "+foo(X) :- qux(GENV1, X) , GENV1 = 42."; @@ -160,6 +167,7 @@ let main () = (* Input: +foo(X) :- bar(X, 42). bar(A, B) :- qux(A, B, 57). *) + mode = Inlining.All; expected = make_lines [ "+foo(X) :- qux(X, 42, 57)."; @@ -179,6 +187,7 @@ let main () = * +f(X) :- g(X). * g(Y) :- Y = 42, true. *) + mode = Inlining.All; expected = make_lines [ "+f(X) :- X = 42 , true."; @@ -204,6 +213,7 @@ let main () = * cp_v() :- +v(N,T), T <> 'A', T <> 'B'. * +a(N) :- +v(N,T), not a(N), T='A', not cp_v(). *) + mode = Inlining.All; expected = make_lines [ "+a(N) :- +v(N, T) , not a(N) , T = 'A' , not cp_v()."; "cp_v() :- +v(N, T) , T <> 'A' , T <> 'B'."