world relation as the universe for scoped negation

2 files changed, 12 insertions, 0 deletions

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",
         [