defmodule Microwaveprop.Pskr.CalibrationSamplerPropertyTest do
  @moduledoc """
  Properties of the producer side of the PSKR calibration pipeline.
  These pin down the contract that future refactors of
  `enqueue_missing_hrrr/2` (currently inlined in
  `Microwaveprop.Pskr.CalibrationSampler.build_for_hour/1`) cannot
  silently break:

    1. Cells with HRRR coverage never get re-enqueued (no churn on
       `hrrr_fetch_tasks`).
    2. Cells without HRRR coverage are *all* enqueued (or, for
       multiple bands sharing a midpoint, exactly one task per
       distinct rounded grid point).
    3. Calibration sample row count equals distinct cell count
       regardless of HRRR availability.
  """
  use Microwaveprop.DataCase, async: true
  use ExUnitProperties

  alias Microwaveprop.Pskr.CalibrationSample
  alias Microwaveprop.Pskr.CalibrationSampler
  alias Microwaveprop.Pskr.SpotHourly
  alias Microwaveprop.Repo
  alias Microwaveprop.Weather.HrrrProfile

  @hour ~U[2026-05-04 18:00:00Z]

  # ── Generators ──────────────────────────────────────────────────

  defp band_gen, do: member_of(["10000", "24000", "47000"])

  # CONUS-ish: 25-50N, 67-125W — within HRRR domain so the
  # round_to_hrrr_grid output is well-defined.
  defp lat_gen, do: float(min: 25.0, max: 49.5)
  defp lon_gen, do: float(min: -125.0, max: -67.0)

  # Per-band cell. Coordinates stay in `bind` so all spots within a
  # generated cell share the same midpoint (otherwise bucket_by_cell
  # would split them).
  defp cell_spec_gen do
    gen all(
          band <- band_gen(),
          lat <- lat_gen(),
          lon <- lon_gen(),
          n_spots <- integer(1..3)
        ) do
      %{band: band, lat: lat, lon: lon, n_spots: n_spots}
    end
  end

  defp insert_spot!(attrs) do
    {:ok, _} =
      %SpotHourly{}
      |> SpotHourly.changeset(
        Map.merge(
          %{
            hour_utc: @hour,
            band: "10000",
            sender_grid: "EM00aa",
            receiver_grid: "DM00bb",
            spot_count: 1,
            distance_km: 100.0,
            modes: ["FT8"]
          },
          attrs
        )
      )
      |> Repo.insert()
  end

  defp insert_hrrr!(lat, lon) do
    {:ok, _} =
      %HrrrProfile{}
      |> HrrrProfile.changeset(%{
        valid_time: @hour,
        lat: lat,
        lon: lon,
        run_time: @hour,
        surface_temp_c: 20.0,
        surface_dewpoint_c: 15.0,
        pwat_mm: 25.0,
        surface_pressure_mb: 1013.0,
        min_refractivity_gradient: -100.0,
        hpbl_m: 500.0,
        ducting_detected: false,
        profile: []
      })
      |> Repo.insert()
  end

  defp seed_spots!(specs, base_callsign) do
    specs
    |> Enum.with_index()
    |> Enum.each(fn {spec, idx} ->
      Enum.each(1..spec.n_spots, fn s_idx ->
        insert_spot!(%{
          band: spec.band,
          midpoint_lat: spec.lat,
          midpoint_lon: spec.lon,
          # Each spot needs a distinct (band, sender, receiver) so
          # the unique index doesn't collapse them.
          sender_grid: "S#{base_callsign}#{idx}#{s_idx}",
          receiver_grid: "R#{base_callsign}#{idx}#{s_idx}"
        })
      end)
    end)
  end

  defp task_count, do: Repo.aggregate(from(t in "hrrr_fetch_tasks"), :count)

  defp task_points do
    case Repo.one(from(t in "hrrr_fetch_tasks", select: t.points)) do
      nil -> []
      pts -> Enum.map(pts, fn %{"lat" => la, "lon" => lo} -> {la, lo} end)
    end
  end

  # 0.125° snap matches CalibrationSampler @grid_step_deg.
  defp snap_cell(lat), do: Float.round(lat / 0.125) * 0.125

  defp expected_unique_cells(specs) do
    specs
    |> Enum.map(fn s -> {s.band, snap_cell(s.lat), snap_cell(s.lon)} end)
    |> Enum.uniq()
  end

  # ── Properties ──────────────────────────────────────────────────

  property "no HRRR profile inserted: every distinct cell midpoint is enqueued exactly once" do
    check all(specs <- list_of(cell_spec_gen(), min_length: 1, max_length: 6), max_runs: 15) do
      Repo.delete_all(SpotHourly)
      Repo.delete_all(CalibrationSample)
      Repo.delete_all(HrrrProfile)
      Repo.query!("DELETE FROM hrrr_fetch_tasks")
      seed_spots!(specs, "A")

      CalibrationSampler.build_for_hour(@hour)

      # One row per (band, snapped_cell) goes into samples.
      assert Repo.aggregate(CalibrationSample, :count) == length(expected_unique_cells(specs))

      # Exactly one hrrr_fetch_tasks row (one valid_time = one row by
      # unique index). The point list inside it must equal the unique
      # set of cell midpoints rounded to the HRRR grid.
      assert task_count() == 1

      expected_pts =
        specs
        |> Enum.map(fn s -> {snap_cell(s.lat), snap_cell(s.lon)} end)
        |> Enum.map(fn {la, lo} -> {Float.round(la, 2), Float.round(lo, 2)} end)
        |> Enum.uniq()

      got = Enum.map(task_points(), fn {la, lo} -> {Float.round(la, 2), Float.round(lo, 2)} end)
      assert Enum.sort(got) == Enum.sort(expected_pts)
    end
  end

  property "every cell covered by HRRR: nothing is enqueued" do
    check all(specs <- list_of(cell_spec_gen(), min_length: 1, max_length: 5), max_runs: 12) do
      Repo.delete_all(SpotHourly)
      Repo.delete_all(CalibrationSample)
      Repo.delete_all(HrrrProfile)
      Repo.query!("DELETE FROM hrrr_fetch_tasks")
      seed_spots!(specs, "B")

      # Plant an HRRR profile near every snapped cell midpoint so
      # nearest_hrrr finds a match for all cells.
      specs
      |> Enum.map(fn s -> {snap_cell(s.lat), snap_cell(s.lon)} end)
      |> Enum.uniq()
      |> Enum.each(fn {la, lo} -> insert_hrrr!(la, lo) end)

      CalibrationSampler.build_for_hour(@hour)

      assert task_count() == 0
      # Samples still get written, just with non-NULL HRRR fields.
      assert Repo.aggregate(CalibrationSample, :count) == length(expected_unique_cells(specs))
    end
  end

  property "sample row count is invariant under HRRR availability" do
    check all(specs <- list_of(cell_spec_gen(), min_length: 1, max_length: 5), max_runs: 12) do
      # No HRRR
      Repo.delete_all(SpotHourly)
      Repo.delete_all(CalibrationSample)
      Repo.delete_all(HrrrProfile)
      Repo.query!("DELETE FROM hrrr_fetch_tasks")
      seed_spots!(specs, "C")
      CalibrationSampler.build_for_hour(@hour)
      no_hrrr_count = Repo.aggregate(CalibrationSample, :count)

      # Reset, plant HRRR, re-run.
      Repo.delete_all(SpotHourly)
      Repo.delete_all(CalibrationSample)
      Repo.query!("DELETE FROM hrrr_fetch_tasks")
      seed_spots!(specs, "D")

      specs
      |> Enum.map(fn s -> {snap_cell(s.lat), snap_cell(s.lon)} end)
      |> Enum.uniq()
      |> Enum.each(fn {la, lo} -> insert_hrrr!(la, lo) end)

      CalibrationSampler.build_for_hour(@hour)
      with_hrrr_count = Repo.aggregate(CalibrationSample, :count)

      assert no_hrrr_count == with_hrrr_count
    end
  end
end