diff options
Diffstat (limited to '')
| -rw-r--r-- | test/test_vm.ml | 48 |
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 |