aboutsummaryrefslogtreecommitdiffstats
path: root/test/test_vm.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--test/test_vm.ml200
1 files changed, 200 insertions, 0 deletions
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;
+ ] );
+ ]
generated by cgit v1.2.3 (git 2.25.1) at 2026-11-04 08:47:43 +0000