Skip to content

Commit

Permalink
Inlining command can receive an target pred.
Browse files Browse the repository at this point in the history
  • Loading branch information
cedretaber committed Jul 21, 2024
1 parent 87090bf commit 3b380ef
Show file tree
Hide file tree
Showing 4 changed files with 47 additions and 6 deletions.
9 changes: 8 additions & 1 deletion bin/inlining.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 ->
Expand Down
7 changes: 7 additions & 0 deletions examples/inlining4.dl
Original file line number Diff line number Diff line change
@@ -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).
25 changes: 21 additions & 4 deletions src/inlining.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down Expand Up @@ -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 ->
Expand Down Expand Up @@ -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
Expand All @@ -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))
Expand Down
12 changes: 11 additions & 1 deletion test/inlining_test.ml
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@ open Expr
type test_case = {
title : string;
input : rule list;
mode : Inlining.inlining_mode;
expected : string;
}

Expand All @@ -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
Expand Down Expand Up @@ -64,6 +65,7 @@ let main () =
{
title = "inlining the empty program";
input = [];
mode = Inlining.All;
expected = "";
};
{
Expand All @@ -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).";
Expand All @@ -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).";
Expand All @@ -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).";
Expand All @@ -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).";
Expand All @@ -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.";
Expand All @@ -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).";
Expand All @@ -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.";
Expand All @@ -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'."
Expand Down

0 comments on commit 3b380ef

Please sign in to comment.