3 files changed, 92 insertions, 1 deletions

diff --git a/test/dune b/test/dune
index 0c5313b..6e5e6eb 100644
--- a/test/dune
+++ b/test/dune
@@ -1,3 +1,3 @@
 (tests
- (names test_term test_vm)
+ (names test_term test_vm test_embedding)
  (libraries sol zarith alcotest))
diff --git a/test/test_embedding.ml b/test/test_embedding.ml
new file mode 100644
index 0000000..32effc2
--- /dev/null
+++ b/test/test_embedding.ml
@@ -0,0 +1,80 @@
+(* Decision 4, exercised: a host builds its own world in OCaml, no
+   parsing involved, and links the same solver. This is the shape of
+   the RNT embedding: the kernel's catalog answers [find], and the
+   engine runs in-process. *)
+
+let label s =
+  match Sol.Label.of_string s with
+  | Ok l -> l
+  | Error (`Invalid_label s) -> Alcotest.failf "invalid label: %s" s
+
+let int n = Sol.Term.integer (Z.of_int n)
+
+(* A toy kernel catalog: one stored relation, served from an OCaml
+   structure rather than program text. *)
+module Kernel_world = struct
+  type t = unit
+
+  let tuple pairs =
+    List.fold_left
+      (fun map (name, term) -> Sol.Label.Map.add (label name) term map)
+      Sol.Label.Map.empty pairs
+
+  let sensors =
+    Sol.World.Table
+      {
+        schema = [ (label "id", Sol.World.Primitive Sol.World.D_integer) ];
+        facts =
+          [
+            tuple [ ("id", int 1); ("reading", int 40) ];
+            tuple [ ("id", int 2); ("reading", int 75) ];
+            tuple [ ("id", int 3); ("reading", int 12) ];
+          ];
+      }
+
+  let find () name =
+    match name with "Sensor" -> Some sensors | _ -> None
+end
+
+module Kernel_vm = Sol.Vm.Make (Kernel_world)
+
+(* The host compiles query text itself through the exposed
+   expression compiler; its own catalog answers for relations. *)
+let solve source =
+  match Sol.Front.parse_string ("Query expression: " ^ source) with
+  | Error message -> Alcotest.failf "parse error: %s" message
+  | Ok [ Sol.Ast.Directive ("Query", [ ("expression", node) ]) ] -> (
+      match Sol.World.expr_of_node node with
+      | Error error -> Alcotest.failf "compile error: %a" Sol.World.pp_error error
+      | Ok query -> Kernel_vm.solve () query)
+  | Ok _ -> Alcotest.fail "expected one query statement"
+
+let show solutions =
+  solutions
+  |> List.map (fun solution ->
+         solution
+         |> List.map (fun (v, p) -> Format.asprintf "%s=%a" v Sol.Pattern.pp p)
+         |> String.concat ",")
+  |> String.concat "; "
+
+let test_kernel_scan () =
+  match solve {| [Sensor id: I reading: R] :and [GreaterThan left: R right: 30] |} with
+  | Ok solutions ->
+      Alcotest.(check string) "hot sensors" "I=1,R=40; I=2,R=75" (show solutions)
+  | Error error -> Alcotest.failf "solve error: %a" Sol.Vm.pp_error error
+
+let test_kernel_totality () =
+  match solve {| [Integer value: X] |} with
+  | Error (Sol.Vm.Non_total_plan _) -> ()
+  | Ok _ -> Alcotest.fail "the embedded engine must keep the totality guard"
+
+let () =
+  Alcotest.run "sol-embedding"
+    [
+      ( "kernel world",
+        [
+          Alcotest.test_case "scan over host relations" `Quick test_kernel_scan;
+          Alcotest.test_case "totality guard survives embedding" `Quick
+            test_kernel_totality;
+        ] );
+    ]
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",
         [