diff options
Diffstat (limited to 'test/test_embedding.ml')
| -rw-r--r-- | test/test_embedding.ml | 21 |
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; ] ); ] |