residuation: open membership returns residual constraints

2 files changed, 52 insertions, 12 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;
         ] );
     ]
diff --git a/test/test_vm.ml b/test/test_vm.ml
index bf7ea35..83532d6 100644
--- a/test/test_vm.ml
+++ b/test/test_vm.ml
@@ -19,9 +19,11 @@ let run 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 "; "
 
@@ -154,13 +156,32 @@ let test_mutual_recursion_rejected () =
   | Error _ -> ()
   | Ok _ -> Alcotest.fail "mutual recursion must be rejected"
 
-let test_unbounded_membership_is_non_total_plan () =
-  match load {| Query expression: [Integer value: X] |} with
+let test_unbounded_membership_residuates () =
+  (* Membership is not generation and not an error either: the
+     constraint comes back as the answer's condition. *)
+  check_answers "open membership residuates"
+    {| Query expression: [Integer value: X] |} "X=X,[Integer value: X]"
+
+let test_residue_discharged_by_binding () =
+  check_answers "a later equality grounds the membership"
+    {| Query expression: [Natural value: X] :and [Equal left: X right: 5] |}
+    "X=5"
+
+let test_residue_accumulates () =
+  check_answers "several open constraints residuate together"
+    {| Query expression: [Natural value: X] :and [GreaterThan left: X right: 5] |}
+    "X=X,[Natural value: X],[GreaterThan left: X right: 5]"
+
+let test_unbounded_search_still_rejected () =
+  match
+    load
+      (length_rules ^ {| Query expression: [Length list: L result: R] |})
+  with
   | Error error -> Alcotest.failf "load error: %a" Sol.Program.pp_error error
   | Ok (world, [ query ]) -> (
       match Sol.Vm.Standalone.solve world query with
       | Error (Sol.Vm.Non_total_plan _) -> ()
-      | Ok _ -> Alcotest.fail "must be rejected as a non-total plan")
+      | Ok _ -> Alcotest.fail "an unbounded recursion must still be rejected")
   | Ok _ -> Alcotest.fail "expected one query"
 
 let test_domain_constrains_when_ground () =
@@ -320,8 +341,14 @@ let () =
             test_fresh_variable_is_no_decrease;
           Alcotest.test_case "mutual recursion rejected" `Quick
             test_mutual_recursion_rejected;
-          Alcotest.test_case "unbounded membership rejected" `Quick
-            test_unbounded_membership_is_non_total_plan;
+          Alcotest.test_case "open membership residuates" `Quick
+            test_unbounded_membership_residuates;
+          Alcotest.test_case "residue discharged by binding" `Quick
+            test_residue_discharged_by_binding;
+          Alcotest.test_case "residue accumulates" `Quick
+            test_residue_accumulates;
+          Alcotest.test_case "unbounded search still rejected" `Quick
+            test_unbounded_search_still_rejected;
           Alcotest.test_case "membership once ground" `Quick
             test_domain_constrains_when_ground;
           Alcotest.test_case "fact domain violation" `Quick