From 0886f3c71cf8551e4f8b3726654003a4f29645f0 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sat, 11 Jul 2026 22:12:53 -0300 Subject: residuation: open membership returns residual constraints --- test/test_embedding.ml | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) (limited to 'test/test_embedding.ml') 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; ] ); ] -- cgit v1.2.3