mutual recursion admitted under lexicographic measures

1 files changed, 44 insertions, 4 deletions

diff --git a/test/test_vm.ml b/test/test_vm.ml
index 0ae62e1..ad58720 100644
--- a/test/test_vm.ml
+++ b/test/test_vm.ml
@@ -113,6 +113,42 @@ let test_deep_recursion () =
         items)
     "R=1000"
 
+(* Mutual recursion under a shared measure. *)
+
+let even_odd =
+  {|
+  Rule name: "even nil" head: [Even list: #()] body: [True]
+  Rule name: "even step" head: [Even list: #(H | T)] body: [Odd list: T]
+  Rule name: "odd step" head: [Odd list: #(H | T)] body: [Even list: T]
+  |}
+
+let count_solutions source =
+  match run source with
+  | [ solutions ] -> List.length solutions
+  | _ -> Alcotest.fail "expected one query"
+
+let test_mutual_recursion_admitted () =
+  Alcotest.(check int)
+    "four elements are even" 1
+    (count_solutions (even_odd ^ {| Query expression: [Even list: #(1 2 3 4)] |}));
+  Alcotest.(check int)
+    "three elements are not even" 0
+    (count_solutions (even_odd ^ {| Query expression: [Even list: #(1 2 3)] |}))
+
+let test_lexicographic_measure () =
+  (* One rule decreases b keeping a equal; the other decreases a
+     while b grows back. Only the order (a, b) covers both calls. *)
+  let walk =
+    {|
+    Rule name: "done" head: [Walk a: #() b: #()] body: [True]
+    Rule name: "b step" head: [Walk a: A b: #(H | T)] body: [Walk a: A b: T]
+    Rule name: "a step" head: [Walk a: #(H | T) b: #()] body: [Walk a: T b: #(1 1)]
+    |}
+  in
+  Alcotest.(check int)
+    "the walk terminates" 1
+    (count_solutions (walk ^ {| Query expression: [Walk a: #(1 2) b: #(9)] |}))
+
 (* Bounded generation is the only enumeration. *)
 
 let test_between_generates () =
@@ -145,7 +181,7 @@ let test_fresh_variable_is_no_decrease () =
   | Error _ -> ()
   | Ok _ -> Alcotest.fail "a fresh variable is not a structural decrease"
 
-let test_mutual_recursion_rejected () =
+let test_undecreasing_mutual_recursion_rejected () =
   match
     load
       {|
@@ -154,7 +190,7 @@ let test_mutual_recursion_rejected () =
       |}
   with
   | Error _ -> ()
-  | Ok _ -> Alcotest.fail "mutual recursion must be rejected"
+  | Ok _ -> Alcotest.fail "mutual recursion without decrease must be rejected"
 
 let test_unbounded_membership_residuates () =
   (* Membership is not generation and not an error either: the
@@ -334,6 +370,10 @@ let () =
           Alcotest.test_case "length" `Quick test_length;
           Alcotest.test_case "length over strings" `Quick test_length_of_strings;
           Alcotest.test_case "deep recursion" `Quick test_deep_recursion;
+          Alcotest.test_case "mutual recursion admitted" `Quick
+            test_mutual_recursion_admitted;
+          Alcotest.test_case "lexicographic measure" `Quick
+            test_lexicographic_measure;
         ] );
       ( "search",
         [
@@ -345,8 +385,8 @@ let () =
           Alcotest.test_case "loop rejected" `Quick test_loop_rule_rejected;
           Alcotest.test_case "fresh variable is no decrease" `Quick
             test_fresh_variable_is_no_decrease;
-          Alcotest.test_case "mutual recursion rejected" `Quick
-            test_mutual_recursion_rejected;
+          Alcotest.test_case "undecreasing mutual recursion rejected" `Quick
+            test_undecreasing_mutual_recursion_rejected;
           Alcotest.test_case "open membership residuates" `Quick
             test_unbounded_membership_residuates;
           Alcotest.test_case "residue discharged by binding" `Quick