diff options
| author | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-11 22:03:21 -0300 |
|---|---|---|
| committer | Marcos Magueta <maguetamarcos@gmail.com> | 2026-07-11 22:03:21 -0300 |
| commit | f22834d3aaed2b2dd2c5d4203e937fc8fb4b5507 (patch) | |
| tree | d1408572183bf8826218b3a067a6c08489f99fe7 /test/test_vm.ml | |
| parent | 1832aca3f545f1f6ecadb7e12ed1ce02c2aa78be (diff) | |
| download | SOL-f22834d3aaed2b2dd2c5d4203e937fc8fb4b5507.tar.gz SOL-f22834d3aaed2b2dd2c5d4203e937fc8fb4b5507.zip | |
admission runs the containment checker extracted from rocq
Diffstat (limited to 'test/test_vm.ml')
| -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 |