defmodule Microwaveprop.GeoPropertyTest do
  @moduledoc """
  StreamData property tests for `Microwaveprop.Geo`.

  The haversine formula defines a metric on the surface of the Earth,
  so it must satisfy the three metric axioms: non-negativity with
  identity-of-indiscernibles, symmetry, and the triangle inequality.
  These properties encode those axioms directly, plus the global
  bound of half the Earth's circumference.
  """
  use ExUnit.Case, async: true
  use ExUnitProperties

  alias Microwaveprop.Geo

  @half_circumference_km 20_015.1

  describe "haversine_km/4 metric axioms" do
    property "distance from a point to itself is exactly 0" do
      check all(
              lat <- float(min: -89.9, max: 89.9),
              lon <- float(min: -179.9, max: 179.9)
            ) do
        assert Geo.haversine_km(lat, lon, lat, lon) == 0.0
      end
    end

    property "is non-negative for every pair of points" do
      check all(
              lat1 <- float(min: -89.9, max: 89.9),
              lon1 <- float(min: -179.9, max: 179.9),
              lat2 <- float(min: -89.9, max: 89.9),
              lon2 <- float(min: -179.9, max: 179.9)
            ) do
        assert Geo.haversine_km(lat1, lon1, lat2, lon2) >= 0
      end
    end

    property "is symmetric in its endpoints" do
      check all(
              lat1 <- float(min: -89.9, max: 89.9),
              lon1 <- float(min: -179.9, max: 179.9),
              lat2 <- float(min: -89.9, max: 89.9),
              lon2 <- float(min: -179.9, max: 179.9)
            ) do
        forward = Geo.haversine_km(lat1, lon1, lat2, lon2)
        reverse = Geo.haversine_km(lat2, lon2, lat1, lon1)
        assert_in_delta forward, reverse, 1.0e-9
      end
    end

    property "satisfies the triangle inequality for any three points" do
      check all(
              lat1 <- float(min: -89.9, max: 89.9),
              lon1 <- float(min: -179.9, max: 179.9),
              lat2 <- float(min: -89.9, max: 89.9),
              lon2 <- float(min: -179.9, max: 179.9),
              lat3 <- float(min: -89.9, max: 89.9),
              lon3 <- float(min: -179.9, max: 179.9)
            ) do
        d_ab = Geo.haversine_km(lat1, lon1, lat2, lon2)
        d_bc = Geo.haversine_km(lat2, lon2, lat3, lon3)
        d_ac = Geo.haversine_km(lat1, lon1, lat3, lon3)

        # Small epsilon for accumulated floating-point error.
        assert d_ac <= d_ab + d_bc + 1.0e-6
      end
    end

    property "is bounded above by half the Earth's circumference" do
      check all(
              lat1 <- float(min: -89.9, max: 89.9),
              lon1 <- float(min: -179.9, max: 179.9),
              lat2 <- float(min: -89.9, max: 89.9),
              lon2 <- float(min: -179.9, max: 179.9)
            ) do
        assert Geo.haversine_km(lat1, lon1, lat2, lon2) <= @half_circumference_km
      end
    end
  end

  describe "bearing_deg/4" do
    property "result is always in [0, 360) for distinct points" do
      check all(
              lat1 <- float(min: -80.0, max: 80.0),
              lon1 <- float(min: -179.0, max: 179.0),
              # Ensure a nonzero displacement.
              dlat <- float(min: 0.1, max: 5.0),
              dlon <- float(min: 0.1, max: 5.0)
            ) do
        b = Geo.bearing_deg(lat1, lon1, lat1 + dlat, lon1 + dlon)
        assert b >= 0.0
        assert b < 360.0
      end
    end
  end
end