diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/test_vm.ml | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test/test_vm.ml b/test/test_vm.ml index 38bbcc9..bf7ea35 100644 --- a/test/test_vm.ml +++ b/test/test_vm.ml @@ -130,6 +130,19 @@ let test_loop_rule_rejected () = | Error _ -> () | Ok _ -> Alcotest.fail "a rule with no structural decrease must be rejected" +let test_fresh_variable_is_no_decrease () = + (* The recursive argument is a fresh variable, not a subterm of + the head. Leaf identity matters here: a checker that conflated + variables would wrongly accept this rule. *) + match + load + {| + Rule name: "cheat" head: [Cheat list: #(H | T)] body: [Cheat list: Z] + |} + with + | Error _ -> () + | Ok _ -> Alcotest.fail "a fresh variable is not a structural decrease" + let test_mutual_recursion_rejected () = match load @@ -303,6 +316,8 @@ let () = ( "totality", [ 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 "unbounded membership rejected" `Quick |