residuation: open membership returns residual constraints

1 files changed, 17 insertions, 4 deletions

diff --git a/test/test_embedding.ml b/test/test_embedding.ml
index 32effc2..ea55e4f 100644
--- a/test/test_embedding.ml
+++ b/test/test_embedding.ml
@@ -51,9 +51,11 @@ let solve source =
 
 let show solutions =
   solutions
-  |> List.map (fun solution ->
-         solution
-         |> List.map (fun (v, p) -> Format.asprintf "%s=%a" v Sol.Pattern.pp p)
+  |> List.map (fun { Sol.Vm.bindings; residue } ->
+         List.map
+           (fun (v, p) -> Format.asprintf "%s=%a" v Sol.Pattern.pp p)
+           bindings
+         @ List.map (Format.asprintf "%a" Sol.Vm.pp_residual) residue
          |> String.concat ",")
   |> String.concat "; "
 
@@ -64,10 +66,19 @@ let test_kernel_scan () =
   | Error error -> Alcotest.failf "solve error: %a" Sol.Vm.pp_error error
 
 let test_kernel_totality () =
-  match solve {| [Integer value: X] |} with
+  match
+    solve
+      {| [ForAll variable: X quantifier: [Integer value: X] body: [True]] |}
+  with
   | Error (Sol.Vm.Non_total_plan _) -> ()
   | Ok _ -> Alcotest.fail "the embedded engine must keep the totality guard"
 
+let test_kernel_residuation () =
+  match solve {| [Integer value: X] |} with
+  | Ok [ { Sol.Vm.residue = [ ("Integer", _) ]; _ } ] -> ()
+  | Ok _ -> Alcotest.fail "open membership must residuate in the embedding too"
+  | Error error -> Alcotest.failf "solve error: %a" Sol.Vm.pp_error error
+
 let () =
   Alcotest.run "sol-embedding"
     [
@@ -76,5 +87,7 @@ let () =
           Alcotest.test_case "scan over host relations" `Quick test_kernel_scan;
           Alcotest.test_case "totality guard survives embedding" `Quick
             test_kernel_totality;
+          Alcotest.test_case "residuation survives embedding" `Quick
+            test_kernel_residuation;
         ] );
     ]