diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/test_vm.ml | 134 |
1 files changed, 131 insertions, 3 deletions
diff --git a/test/test_vm.ml b/test/test_vm.ml index 3631ee5..e564a83 100644 --- a/test/test_vm.ml +++ b/test/test_vm.ml @@ -3,11 +3,11 @@ let load source = match Sol.Front.parse_string source with | Error message -> Alcotest.failf "parse error: %s" message - | Ok statements -> Sol.World.Standalone.load statements + | Ok statements -> Sol.Program.load statements let run source = match load source with - | Error error -> Alcotest.failf "load error: %a" Sol.World.pp_error error + | Error error -> Alcotest.failf "load error: %a" Sol.Program.pp_error error | Ok (world, queries) -> List.map (fun query -> @@ -133,7 +133,7 @@ let test_mutual_recursion_rejected () = let test_unbounded_membership_is_non_total_plan () = match load {| Query expression: [Integer value: X] |} with - | Error error -> Alcotest.failf "load error: %a" Sol.World.pp_error error + | 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 _) -> () @@ -145,6 +145,53 @@ let test_domain_constrains_when_ground () = {| Query expression: [Between value: X lower: -2 upper: 2] :and [Natural value: X] |} "X=0; X=1; X=2" +(* Negation: decidable denial over ground goals. *) + +let test_negation () = + check_answers "people who are not adults" + (people + ^ {| Query expression: ([Person name: N age: A]) :not [Adult name: N] |}) + {|A=12,N="Ana"|} + +let test_negation_defers_until_ground () = + check_answers "denial waits for its variables" + (people + ^ {| Query expression: ([Adult name: N] :not [Equal left: N right: "Rui"]) :and [Person name: N age: A] |}) + {|N="Marcos",A=30|} + +(* Quantifiers. *) + +let test_forall_holds () = + check_answers "every person is at least 10" + (people + ^ {| Query expression: [ForAll variable: P quantifier: [Person name: P age: B] body: [GreaterEqual left: B right: 10]] |}) + "" + +let test_forall_fails () = + match + run + (people + ^ {| Query expression: [ForAll variable: P quantifier: [Person name: P age: B] body: [GreaterEqual left: B right: 18]] |}) + with + | [ [] ] -> () + | [ _ :: _ ] -> Alcotest.fail "the universal must fail: Ana is 12" + | _ -> Alcotest.fail "expected one query" + +let test_forall_over_infinite_rejected () = + match load {| Query expression: [ForAll variable: X quantifier: [Integer value: X] body: [True]] |} 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 "a universal over an infinite domain must be rejected") + | Ok _ -> Alcotest.fail "expected one query" + +let test_exists () = + check_answers "existence lowers to conjunction" + (people + ^ {| Query expression: [Exists variable: P quantifier: [Person name: P age: B] body: [GreaterThan left: B right: 60]] |}) + "B=70" + (* Integrity control at loading: facts must satisfy their schema. *) let test_fact_domain_violation () = @@ -158,6 +205,63 @@ let test_fact_domain_violation () = | Error _ -> () | Ok _ -> Alcotest.fail "a fact violating its domain must be rejected" +(* Membership criteria as domains: refinements and foreign keys. *) + +let departments = + {| + Relation named: Department schema: #( [id domain: Integer] ) + [Department id: 1] + [Department id: 2] + Relation named: Employee schema: #( + [name domain: String] + [dept domain: ([Department id: D])] + [score domain: ([Natural value: S] :and [LessThanEqual left: S right: 100])] + ) + |} + +let test_criterion_admits () = + check_answers "a valid employee is admitted" + (departments + ^ {| + [Employee name: "Marcos" dept: 1 score: 90] + Query expression: [Employee name: N dept: D score: S] + |}) + {|D=1,N="Marcos",S=90|} + +let test_foreign_key_rejected () = + match + load (departments ^ {| [Employee name: "Ghost" dept: 9 score: 50] |}) + with + | Error (Sol.Program.Integrity { relation = "Employee"; label = "dept" }) -> () + | Error error -> Alcotest.failf "wrong error: %a" Sol.Program.pp_error error + | Ok _ -> Alcotest.fail "a dangling foreign key must be rejected" + +let test_refinement_rejected () = + match + load (departments ^ {| [Employee name: "Over" dept: 1 score: 101] |}) + with + | Error (Sol.Program.Integrity { relation = "Employee"; label = "score" }) -> () + | Error error -> Alcotest.failf "wrong error: %a" Sol.Program.pp_error error + | Ok _ -> Alcotest.fail "a score beyond the refinement must be rejected" + +let test_fact_order_is_irrelevant () = + (* The employee arrives before its department; integrity is judged + against the complete extension. *) + match + load + {| + Relation named: Department schema: #( [id domain: Integer] ) + Relation named: Employee schema: #( + [name domain: String] + [dept domain: ([Department id: D])] + ) + [Employee name: "Early" dept: 7] + [Department id: 7] + |} + with + | Ok _ -> () + | Error error -> Alcotest.failf "load error: %a" Sol.Program.pp_error error + let () = Alcotest.run "sol-vm" [ @@ -197,4 +301,28 @@ let () = Alcotest.test_case "fact domain violation" `Quick test_fact_domain_violation; ] ); + ( "negation", + [ + Alcotest.test_case "not adults" `Quick test_negation; + Alcotest.test_case "denial defers until ground" `Quick + test_negation_defers_until_ground; + ] ); + ( "quantifiers", + [ + Alcotest.test_case "forall holds" `Quick test_forall_holds; + Alcotest.test_case "forall fails" `Quick test_forall_fails; + Alcotest.test_case "forall over infinite rejected" `Quick + test_forall_over_infinite_rejected; + Alcotest.test_case "exists" `Quick test_exists; + ] ); + ( "criteria", + [ + Alcotest.test_case "criterion admits" `Quick test_criterion_admits; + Alcotest.test_case "foreign key rejected" `Quick + test_foreign_key_rejected; + Alcotest.test_case "refinement rejected" `Quick + test_refinement_rejected; + Alcotest.test_case "fact order irrelevant" `Quick + test_fact_order_is_irrelevant; + ] ); ] |