Fix compiling pack of rules (#1036)

* 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). * 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. --------- Co-authored-by: Gabriel Hondet <gabriel.hondet@cominety.net>
Deducteam · Jan 30, 2024 · 2b8cfe4 · 2b8cfe4
1 parent b441123
commit 2b8cfe4
Show file tree

Hide file tree

Showing 5 changed files with 48 additions and 32 deletions.
diff --git 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
@@ -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
@@ -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;
diff --git 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
@@ -5,34 +5,34 @@
     <rules>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.boolean.bool_and</name><arg><var>1_0</var></arg><arg><funapp><name>tests.OK.boolean.false</name></funapp></arg></funapp>
+          <funapp><name>tests.OK.boolean.bool_and</name><arg><funapp><name>tests.OK.boolean.true</name></funapp></arg><arg><var>1_0</var></arg></funapp>
         </lhs>
         <rhs>
-          <funapp><name>tests.OK.boolean.false</name></funapp>
+          <var>1_0</var>
         </rhs>
       </rule>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.boolean.bool_and</name><arg><var>2_0</var></arg><arg><funapp><name>tests.OK.boolean.true</name></funapp></arg></funapp>
+          <funapp><name>tests.OK.boolean.bool_and</name><arg><funapp><name>tests.OK.boolean.false</name></funapp></arg><arg><var>2_0</var></arg></funapp>
         </lhs>
         <rhs>
-          <var>2_0</var>
+          <funapp><name>tests.OK.boolean.false</name></funapp>
         </rhs>
       </rule>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.boolean.bool_and</name><arg><funapp><name>tests.OK.boolean.false</name></funapp></arg><arg><var>3_0</var></arg></funapp>
+          <funapp><name>tests.OK.boolean.bool_and</name><arg><var>3_0</var></arg><arg><funapp><name>tests.OK.boolean.true</name></funapp></arg></funapp>
         </lhs>
         <rhs>
-          <funapp><name>tests.OK.boolean.false</name></funapp>
+          <var>3_0</var>
         </rhs>
       </rule>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.boolean.bool_and</name><arg><funapp><name>tests.OK.boolean.true</name></funapp></arg><arg><var>4_0</var></arg></funapp>
+          <funapp><name>tests.OK.boolean.bool_and</name><arg><var>4_0</var></arg><arg><funapp><name>tests.OK.boolean.false</name></funapp></arg></funapp>
         </lhs>
         <rhs>
-          <var>4_0</var>
+          <funapp><name>tests.OK.boolean.false</name></funapp>
         </rhs>
       </rule>
       <rule>
@@ -45,50 +45,50 @@
       </rule>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.boolean.bool_neg</name><arg><funapp><name>tests.OK.boolean.false</name></funapp></arg></funapp>
+          <funapp><name>tests.OK.boolean.bool_neg</name><arg><funapp><name>tests.OK.boolean.true</name></funapp></arg></funapp>
         </lhs>
         <rhs>
-          <funapp><name>tests.OK.boolean.true</name></funapp>
+          <funapp><name>tests.OK.boolean.false</name></funapp>
         </rhs>
       </rule>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.boolean.bool_neg</name><arg><funapp><name>tests.OK.boolean.true</name></funapp></arg></funapp>
+          <funapp><name>tests.OK.boolean.bool_neg</name><arg><funapp><name>tests.OK.boolean.false</name></funapp></arg></funapp>
         </lhs>
         <rhs>
-          <funapp><name>tests.OK.boolean.false</name></funapp>
+          <funapp><name>tests.OK.boolean.true</name></funapp>
         </rhs>
       </rule>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.boolean.bool_or</name><arg><var>7_0</var></arg><arg><funapp><name>tests.OK.boolean.false</name></funapp></arg></funapp>
+          <funapp><name>tests.OK.boolean.bool_or</name><arg><funapp><name>tests.OK.boolean.true</name></funapp></arg><arg><var>7_0</var></arg></funapp>
         </lhs>
         <rhs>
-          <var>7_0</var>
+          <funapp><name>tests.OK.boolean.true</name></funapp>
         </rhs>
       </rule>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.boolean.bool_or</name><arg><var>8_0</var></arg><arg><funapp><name>tests.OK.boolean.true</name></funapp></arg></funapp>
+          <funapp><name>tests.OK.boolean.bool_or</name><arg><funapp><name>tests.OK.boolean.false</name></funapp></arg><arg><var>8_0</var></arg></funapp>
         </lhs>
         <rhs>
-          <funapp><name>tests.OK.boolean.true</name></funapp>
+          <var>8_0</var>
         </rhs>
       </rule>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.boolean.bool_or</name><arg><funapp><name>tests.OK.boolean.false</name></funapp></arg><arg><var>9_0</var></arg></funapp>
+          <funapp><name>tests.OK.boolean.bool_or</name><arg><var>9_0</var></arg><arg><funapp><name>tests.OK.boolean.true</name></funapp></arg></funapp>
         </lhs>
         <rhs>
-          <var>9_0</var>
+          <funapp><name>tests.OK.boolean.true</name></funapp>
         </rhs>
       </rule>
       <rule>
         <lhs>
-          <funapp><name>tests.OK.boolean.bool_or</name><arg><funapp><name>tests.OK.boolean.true</name></funapp></arg><arg><var>10_0</var></arg></funapp>
+          <funapp><name>tests.OK.boolean.bool_or</name><arg><var>10_0</var></arg><arg><funapp><name>tests.OK.boolean.false</name></funapp></arg></funapp>
         </lhs>
         <rhs>
-          <funapp><name>tests.OK.boolean.true</name></funapp>
+          <var>10_0</var>
         </rhs>
       </rule>
       <rule>