From 5d967951eb0b08c36ee59f70d7f4cca37b0ca72b Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sat, 11 Jul 2026 22:13:33 -0300 Subject: world relation as the universe for scoped negation --- lib/builtin.ml | 4 ++++ test/test_vm.ml | 8 ++++++++ 2 files changed, 12 insertions(+) diff --git a/lib/builtin.ml b/lib/builtin.ml index 694b688..082471b 100644 --- a/lib/builtin.ml +++ b/lib/builtin.ml @@ -13,6 +13,7 @@ let upper_l = forced_label "upper" let names = [ "True"; + "World"; "Integer"; "Natural"; "Rational"; @@ -143,6 +144,9 @@ let between subst bindings = let run subst name bindings = match name with | "True" -> Some (yes subst) + (* The universe: true of every tuple, per the specification. Its + role is to scope denial, as in [World] :not [Adult person: P]. *) + | "World" -> Some (yes subst) | "Integer" -> Some (domain_check subst bindings (function diff --git a/test/test_vm.ml b/test/test_vm.ml index 83532d6..0ae62e1 100644 --- a/test/test_vm.ml +++ b/test/test_vm.ml @@ -203,6 +203,12 @@ let test_negation_defers_until_ground () = ^ {| Query expression: ([Adult name: N] :not [Equal left: N right: "Rui"]) :and [Person name: N age: A] |}) {|N="Marcos",A=30|} +let test_world_scoped_negation () = + (* The specification's own negation form. *) + check_answers "no adult named Ana" + (people ^ {| Query expression: [World] :not [Adult name: "Ana"] |}) + "" + (* Quantifiers. *) let test_forall_holds () = @@ -359,6 +365,8 @@ let () = Alcotest.test_case "not adults" `Quick test_negation; Alcotest.test_case "denial defers until ground" `Quick test_negation_defers_until_ground; + Alcotest.test_case "world-scoped negation" `Quick + test_world_scoped_negation; ] ); ( "quantifiers", [ -- cgit v1.2.3