From e2ad4f1cd26d4ff876a71368bbfba1c9de89370a Mon Sep 17 00:00:00 2001 From: Gabriel Hondet Date: Sat, 27 Jan 2024 13:57:42 +0100 Subject: [PATCH 1/2] Fix compiling pack of rules Rules declared in group appeared to be reverted when handled, causing the "sequential" strategy to not behave as intended (the rule with highest priority was the last to appear in the source file). --- src/core/tree.ml | 4 +++- src/handle/command.ml | 9 +++++++-- tests/OK/1033.lp | 9 +++++++++ 3 files changed, 19 insertions(+), 3 deletions(-) create mode 100644 tests/OK/1033.lp diff --git a/src/core/tree.ml b/src/core/tree.ml index 1e96ae00a..e94d8cbf7 100644 --- a/src/core/tree.ml +++ b/src/core/tree.ml @@ -240,7 +240,9 @@ module CM = struct (** Type of clause matrices. *) type t = { clauses : clause list - (** The rules. *) + (** The rewrite rules. The order is significant when the {!Sequen} + strategy is used: the rewrite rules are ordered by decreasing + priority. *) ; slot : int (** Index of next slot to use in [vars] array to store variables. *) ; positions : arg list diff --git a/src/handle/command.ml b/src/handle/command.ml index f99821097..25bb420bb 100644 --- a/src/handle/command.ml +++ b/src/handle/command.ml @@ -218,12 +218,17 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output = (* Scope rules, and check that they preserve typing. Return the list of rules [srs] and also a map [map] mapping every symbol defined by a rule of [srs] to its defining rules. *) - let handle_rule (srs, map) r = + let handle_rule r (srs, map) = let (s,r) as sr = check_rule ss r in let h = function Some rs -> Some(r::rs) | None -> Some[r] in sr::srs, SymMap.update s h map in - let srs, map = List.fold_left handle_rule ([], SymMap.empty) rs in + (* The order of rules must be kept between [rs] and [srs]. + That is, the following assertion should hold + [assert (srs = List.map (check_rule ss) rs);] if we could compare + functional values. Failure to keep that invariant breaks some + evaluation strategies. *) + let srs, map = List.fold_right handle_rule rs ([], SymMap.empty) in (* /!\ Update decision trees without adding the rules themselves. It is important for local confluence checking. *) SymMap.iter Tree.update_dtree map; diff --git a/tests/OK/1033.lp b/tests/OK/1033.lp new file mode 100644 index 000000000..e2b4c5e82 --- /dev/null +++ b/tests/OK/1033.lp @@ -0,0 +1,9 @@ +// Test on the sequential reduction strategy +constant symbol I: TYPE; +constant symbol i: I; +constant symbol j: I; +sequential symbol k: I → I; +rule k i ↪ i +with k i ↪ j; + +assert ⊢ k i ≡ i; From ae43dc87126c1260af44b0dae2f29f2eb6eacbf1 Mon Sep 17 00:00:00 2001 From: Gabriel Hondet Date: Sat, 27 Jan 2024 14:21:18 +0100 Subject: [PATCH 2/2] Fix tests One can see that in hrs.expected, the order of the exported rewrite rules now match the order the rules are declared in. Look for instance at the rules of bool_neg in boolean.lp. --- tests/regressions/hrs.expected | 18 +++++++-------- tests/regressions/xtc.expected | 40 +++++++++++++++++----------------- 2 files changed, 29 insertions(+), 29 deletions(-) diff --git a/tests/regressions/hrs.expected b/tests/regressions/hrs.expected index f3dc68acd..9de812644 100644 --- a/tests/regressions/hrs.expected +++ b/tests/regressions/hrs.expected @@ -34,16 +34,16 @@ $10_0 : t (RULES A(L($x,$y),$z) -> $y($z), B($x,$z,$y) -> $y($z), -A(A(tests_OK_boolean_bool_and,$1_0),tests_OK_boolean_false) -> tests_OK_boolean_false, -A(A(tests_OK_boolean_bool_and,$2_0),tests_OK_boolean_true) -> $2_0, -A(A(tests_OK_boolean_bool_and,tests_OK_boolean_false),$3_0) -> tests_OK_boolean_false, -A(A(tests_OK_boolean_bool_and,tests_OK_boolean_true),$4_0) -> $4_0, +A(A(tests_OK_boolean_bool_and,tests_OK_boolean_true),$1_0) -> $1_0, +A(A(tests_OK_boolean_bool_and,tests_OK_boolean_false),$2_0) -> tests_OK_boolean_false, +A(A(tests_OK_boolean_bool_and,$3_0),tests_OK_boolean_true) -> $3_0, +A(A(tests_OK_boolean_bool_and,$4_0),tests_OK_boolean_false) -> tests_OK_boolean_false, tests_OK_boolean_bool_impl -> L(tests_OK_boolean_B,\82.L(tests_OK_boolean_B,\83.A(A(tests_OK_boolean_bool_or,83),A(tests_OK_boolean_bool_neg,82)))), -A(tests_OK_boolean_bool_neg,tests_OK_boolean_false) -> tests_OK_boolean_true, A(tests_OK_boolean_bool_neg,tests_OK_boolean_true) -> tests_OK_boolean_false, -A(A(tests_OK_boolean_bool_or,$7_0),tests_OK_boolean_false) -> $7_0, -A(A(tests_OK_boolean_bool_or,$8_0),tests_OK_boolean_true) -> tests_OK_boolean_true, -A(A(tests_OK_boolean_bool_or,tests_OK_boolean_false),$9_0) -> $9_0, -A(A(tests_OK_boolean_bool_or,tests_OK_boolean_true),$10_0) -> tests_OK_boolean_true, +A(tests_OK_boolean_bool_neg,tests_OK_boolean_false) -> tests_OK_boolean_true, +A(A(tests_OK_boolean_bool_or,tests_OK_boolean_true),$7_0) -> tests_OK_boolean_true, +A(A(tests_OK_boolean_bool_or,tests_OK_boolean_false),$8_0) -> $8_0, +A(A(tests_OK_boolean_bool_or,$9_0),tests_OK_boolean_true) -> tests_OK_boolean_true, +A(A(tests_OK_boolean_bool_or,$10_0),tests_OK_boolean_false) -> $10_0, tests_OK_boolean_bool_xor -> L(tests_OK_boolean_B,\84.L(tests_OK_boolean_B,\85.B(tests_OK_boolean_B,A(A(tests_OK_boolean_bool_and,84),A(tests_OK_boolean_bool_neg,85)),\86.B(tests_OK_boolean_B,A(A(tests_OK_boolean_bool_and,85),A(tests_OK_boolean_bool_neg,84)),\87.A(A(tests_OK_boolean_bool_or,86),87))))) ) diff --git a/tests/regressions/xtc.expected b/tests/regressions/xtc.expected index 94f5c4035..7510feae8 100644 --- a/tests/regressions/xtc.expected +++ b/tests/regressions/xtc.expected @@ -5,34 +5,34 @@ - tests.OK.boolean.bool_and1_0tests.OK.boolean.false + tests.OK.boolean.bool_andtests.OK.boolean.true1_0 - tests.OK.boolean.false + 1_0 - tests.OK.boolean.bool_and2_0tests.OK.boolean.true + tests.OK.boolean.bool_andtests.OK.boolean.false2_0 - 2_0 + tests.OK.boolean.false - tests.OK.boolean.bool_andtests.OK.boolean.false3_0 + tests.OK.boolean.bool_and3_0tests.OK.boolean.true - tests.OK.boolean.false + 3_0 - tests.OK.boolean.bool_andtests.OK.boolean.true4_0 + tests.OK.boolean.bool_and4_0tests.OK.boolean.false - 4_0 + tests.OK.boolean.false @@ -45,50 +45,50 @@ - tests.OK.boolean.bool_negtests.OK.boolean.false + tests.OK.boolean.bool_negtests.OK.boolean.true - tests.OK.boolean.true + tests.OK.boolean.false - tests.OK.boolean.bool_negtests.OK.boolean.true + tests.OK.boolean.bool_negtests.OK.boolean.false - tests.OK.boolean.false + tests.OK.boolean.true - tests.OK.boolean.bool_or7_0tests.OK.boolean.false + tests.OK.boolean.bool_ortests.OK.boolean.true7_0 - 7_0 + tests.OK.boolean.true - tests.OK.boolean.bool_or8_0tests.OK.boolean.true + tests.OK.boolean.bool_ortests.OK.boolean.false8_0 - tests.OK.boolean.true + 8_0 - tests.OK.boolean.bool_ortests.OK.boolean.false9_0 + tests.OK.boolean.bool_or9_0tests.OK.boolean.true - 9_0 + tests.OK.boolean.true - tests.OK.boolean.bool_ortests.OK.boolean.true10_0 + tests.OK.boolean.bool_or10_0tests.OK.boolean.false - tests.OK.boolean.true + 10_0