embedding surface, host world test, deep recursion, line tracking

1 files changed, 11 insertions, 0 deletions

diff --git a/test/test_vm.ml b/test/test_vm.ml
index e564a83..38bbcc9 100644
--- a/test/test_vm.ml
+++ b/test/test_vm.ml
@@ -101,6 +101,16 @@ let test_length_of_strings () =
    ^ {| Query expression: [Length list: #("a" "b") result: R] |})
     "R=2"
 
+let test_deep_recursion () =
+  (* The witness shrinks a thousand times; the engine must neither
+     loop nor exhaust the stack on realistic depths. *)
+  let items = String.concat " " (List.init 1000 (fun _ -> "0")) in
+  check_answers "length of a thousand elements"
+    (length_rules
+    ^ Printf.sprintf {| Query expression: [Length list: #(%s) result: R] |}
+        items)
+    "R=1000"
+
 (* Bounded generation is the only enumeration. *)
 
 let test_between_generates () =
@@ -283,6 +293,7 @@ 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;
         ] );
       ( "search",
         [