(* 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.Program.load statements

let run source =
  match load source with
  | Error error -> Alcotest.failf "load error: %a" Sol.Program.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"

let test_deep_recursion () =
  (* The witness shrinks a thousand times; the engine must neither
     loop nor exhaust the stack on realistic depths. *)
  let items = String.concat " " (List.init 1000 (fun _ -> "0")) in
  check_answers "length of a thousand elements"
    (length_rules
    ^ Printf.sprintf {| Query expression: [Length list: #(%s) result: R] |}
        items)
    "R=1000"

(* 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.Program.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"

(* 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 () =
  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"

(* 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"
    [
      ( "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;
          Alcotest.test_case "deep recursion" `Quick test_deep_recursion;
        ] );
      ( "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;
        ] );
      ( "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;
        ] );
    ]