path: root/test/test_vm.ml

(* 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;
        ] );
    ]