residuation: open membership returns residual constraints

1 files changed, 35 insertions, 8 deletions

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