From c530682030e80ee2de2c263471e5eda7a3392e84 Mon Sep 17 00:00:00 2001 From: Marcos Magueta Date: Sat, 11 Jul 2026 03:07:56 -0300 Subject: working vm: parser, admission with totality checks, solver and repl --- test/test_vm.ml | 200 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 200 insertions(+) create mode 100644 test/test_vm.ml (limited to 'test/test_vm.ml') diff --git a/test/test_vm.ml b/test/test_vm.ml new file mode 100644 index 0000000..3631ee5 --- /dev/null +++ b/test/test_vm.ml @@ -0,0 +1,200 @@ +(* End-to-end: source text through parsing, admission, and solving. *) + +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 + +let run source = + match load source with + | Error error -> Alcotest.failf "load error: %a" Sol.World.pp_error error + | Ok (world, queries) -> + List.map + (fun query -> + match Sol.Vm.Standalone.solve world query with + | Ok solutions -> solutions + | Error error -> + Alcotest.failf "solve error: %a" Sol.Vm.pp_error error) + queries + +let show solutions = + solutions + |> List.map (fun solution -> + solution + |> List.map (fun (v, p) -> Format.asprintf "%s=%a" v Sol.Pattern.pp p) + |> String.concat ",") + |> String.concat "; " + +let check_answers description source expected = + match run source with + | [ solutions ] -> Alcotest.(check string) description expected (show solutions) + | results -> + Alcotest.failf "expected one query, got %d" (List.length results) + +(* Facts, joins, and rules over stored relations. *) + +let people = + {| + Relation named: Person schema: #( [name domain: String] [age domain: Integer] ) + [Person name: "Marcos" age: 30] + [Person name: "Ana" age: 12] + [Person name: "Rui" age: 70] + Rule name: "adults" head: [Adult name: N] body: + [Person name: N age: A] :and [GreaterEqual left: A right: 18] + |} + +let test_scan () = + check_answers "all people" + (people ^ {| Query expression: [Person name: N age: A] |}) + {|A=30,N="Marcos"; A=12,N="Ana"; A=70,N="Rui"|} + +let test_rule_join () = + check_answers "adults via rule" + (people ^ {| Query expression: [Adult name: N] |}) + {|N="Marcos"; N="Rui"|} + +let test_conjunction_is_commutative () = + let forward = + people + ^ {| Query expression: [Person name: N age: A] :and [GreaterThan left: A right: 20] |} + and backward = + people + ^ {| Query expression: [GreaterThan left: A right: 20] :and [Person name: N age: A] |} + in + Alcotest.(check string) + "order on the page means nothing" + (show (List.hd (run forward))) + (show (List.hd (run backward))) + +(* Arithmetic solves backwards; the numeric tower stays minimal + shape. *) + +let test_plus_backward () = + check_answers "X + 5 = 12" + {| Query expression: [Plus left: X right: 5 result: 12] |} "X=7" + +let test_times_rational () = + check_answers "3 * X = 2 solves in the rationals" + {| Query expression: [Times left: 3 right: X result: 2] |} "X=2/3" + +let test_rational_collapse_in_arithmetic () = + check_answers "1/2 + 1/2 collapses to the integer 1" + {| Query expression: [Plus left: 1/2 right: 1/2 result: R] |} "R=1" + +(* Structural recursion, admitted by the decrease witness. *) + +let length_rules = + {| + Rule name: "length nil" head: [Length list: #() result: 0] body: [True] + Rule name: "length cons" head: [Length list: #(H | T) result: R] body: + [Length list: T result: P] :and [Plus left: 1 right: P result: R] + |} + +let test_length () = + check_answers "length of #(1 2 3)" + (length_rules ^ {| Query expression: [Length list: #(1 2 3) result: R] |}) + "R=3" + +let test_length_of_strings () = + check_answers "length is polymorphic over members" + (length_rules + ^ {| Query expression: [Length list: #("a" "b") result: R] |}) + "R=2" + +(* Bounded generation is the only enumeration. *) + +let test_between_generates () = + check_answers "between enumerates its finite range" + {| Query expression: [Between value: X lower: 1 upper: 4] :and [GreaterThan left: X right: 2] |} + "X=3; X=4" + +let test_disjunction () = + check_answers "disjunction branches" + {| Query expression: [Equal left: X right: 1] :or [Equal left: X right: 2] |} + "X=1; X=2" + +(* Totality: what must be rejected, is. *) + +let test_loop_rule_rejected () = + match load {| Rule name: "loop" head: [Loop value: X] body: [Loop value: X] |} with + | Error _ -> () + | Ok _ -> Alcotest.fail "a rule with no structural decrease must be rejected" + +let test_mutual_recursion_rejected () = + match + load + {| + Rule name: "a" head: [A value: X] body: [B value: X] + Rule name: "b" head: [B value: X] body: [A value: X] + |} + with + | Error _ -> () + | Ok _ -> Alcotest.fail "mutual recursion must be 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 + | Ok (world, [ query ]) -> ( + match Sol.Vm.Standalone.solve world query with + | Error (Sol.Vm.Non_total_plan _) -> () + | Ok _ -> Alcotest.fail "must be rejected as a non-total plan") + | Ok _ -> Alcotest.fail "expected one query" + +let test_domain_constrains_when_ground () = + check_answers "membership checks once ground" + {| Query expression: [Between value: X lower: -2 upper: 2] :and [Natural value: X] |} + "X=0; X=1; X=2" + +(* Integrity control at loading: facts must satisfy their schema. *) + +let test_fact_domain_violation () = + match + load + {| + Relation named: Score schema: #( [value domain: Natural] ) + [Score value: -3] + |} + with + | Error _ -> () + | Ok _ -> Alcotest.fail "a fact violating its domain must be rejected" + +let () = + Alcotest.run "sol-vm" + [ + ( "relations", + [ + Alcotest.test_case "scan" `Quick test_scan; + Alcotest.test_case "rule and join" `Quick test_rule_join; + Alcotest.test_case "commutative conjunction" `Quick + test_conjunction_is_commutative; + ] ); + ( "arithmetic", + [ + Alcotest.test_case "plus backward" `Quick test_plus_backward; + Alcotest.test_case "times rational" `Quick test_times_rational; + Alcotest.test_case "minimal shape" `Quick + test_rational_collapse_in_arithmetic; + ] ); + ( "recursion", + [ + Alcotest.test_case "length" `Quick test_length; + Alcotest.test_case "length over strings" `Quick test_length_of_strings; + ] ); + ( "search", + [ + Alcotest.test_case "bounded generation" `Quick test_between_generates; + Alcotest.test_case "disjunction" `Quick test_disjunction; + ] ); + ( "totality", + [ + Alcotest.test_case "loop rejected" `Quick test_loop_rule_rejected; + Alcotest.test_case "mutual recursion rejected" `Quick + test_mutual_recursion_rejected; + Alcotest.test_case "unbounded membership rejected" `Quick + test_unbounded_membership_is_non_total_plan; + Alcotest.test_case "membership once ground" `Quick + test_domain_constrains_when_ground; + Alcotest.test_case "fact domain violation" `Quick + test_fact_domain_violation; + ] ); + ] -- cgit v1.2.3