(* Decision 4, exercised: a host builds its own world in OCaml, no
   parsing involved, and links the same solver. This is the shape of
   the RNT embedding: the kernel's catalog answers [find], and the
   engine runs in-process. *)

let label s =
  match Sol.Label.of_string s with
  | Ok l -> l
  | Error (`Invalid_label s) -> Alcotest.failf "invalid label: %s" s

let int n = Sol.Term.integer (Z.of_int n)

(* A toy kernel catalog: one stored relation, served from an OCaml
   structure rather than program text. *)
module Kernel_world = struct
  type t = unit

  let tuple pairs =
    List.fold_left
      (fun map (name, term) -> Sol.Label.Map.add (label name) term map)
      Sol.Label.Map.empty pairs

  let sensors =
    Sol.World.Table
      {
        schema = [ (label "id", Sol.World.Primitive Sol.World.D_integer) ];
        facts =
          [
            tuple [ ("id", int 1); ("reading", int 40) ];
            tuple [ ("id", int 2); ("reading", int 75) ];
            tuple [ ("id", int 3); ("reading", int 12) ];
          ];
      }

  let find () name =
    match name with "Sensor" -> Some sensors | _ -> None
end

module Kernel_vm = Sol.Vm.Make (Kernel_world)

(* The host compiles query text itself through the exposed
   expression compiler; its own catalog answers for relations. *)
let solve source =
  match Sol.Front.parse_string ("Query expression: " ^ source) with
  | Error message -> Alcotest.failf "parse error: %s" message
  | Ok [ Sol.Ast.Directive ("Query", [ ("expression", node) ]) ] -> (
      match Sol.World.expr_of_node node with
      | Error error -> Alcotest.failf "compile error: %a" Sol.World.pp_error error
      | Ok query -> Kernel_vm.solve () query)
  | Ok _ -> Alcotest.fail "expected one query statement"

let show solutions =
  solutions
  |> List.map (fun { Sol.Vm.bindings; residue } ->
         List.map
           (fun (v, p) -> Format.asprintf "%s=%a" v Sol.Pattern.pp p)
           bindings
         @ List.map (Format.asprintf "%a" Sol.Vm.pp_residual) residue
         |> String.concat ",")
  |> String.concat "; "

let test_kernel_scan () =
  match solve {| [Sensor id: I reading: R] :and [GreaterThan left: R right: 30] |} with
  | Ok solutions ->
      Alcotest.(check string) "hot sensors" "I=1,R=40; I=2,R=75" (show solutions)
  | Error error -> Alcotest.failf "solve error: %a" Sol.Vm.pp_error error

let test_kernel_totality () =
  match
    solve
      {| [ForAll variable: X quantifier: [Integer value: X] body: [True]] |}
  with
  | Error (Sol.Vm.Non_total_plan _) -> ()
  | Ok _ -> Alcotest.fail "the embedded engine must keep the totality guard"

let test_kernel_residuation () =
  match solve {| [Integer value: X] |} with
  | Ok [ { Sol.Vm.residue = [ ("Integer", _) ]; _ } ] -> ()
  | Ok _ -> Alcotest.fail "open membership must residuate in the embedding too"
  | Error error -> Alcotest.failf "solve error: %a" Sol.Vm.pp_error error

let () =
  Alcotest.run "sol-embedding"
    [
      ( "kernel world",
        [
          Alcotest.test_case "scan over host relations" `Quick test_kernel_scan;
          Alcotest.test_case "totality guard survives embedding" `Quick
            test_kernel_totality;
          Alcotest.test_case "residuation survives embedding" `Quick
            test_kernel_residuation;
        ] );
    ]