package Grl.Coordinates with
  SPARK_Mode => On
is

   --  ------------  --
   --  Helper Units  --
   --  ------------  --

   --  DD Meter Scale
   type DD_Meter_Scale_Lat is delta 1.0E-5 range -90.0 .. 90.0;
   type DD_Meter_Scale_Lon is delta 1.0E-5 range -180.0 .. 180.0;

   --  DD Centimeter Scale
   type DD_Centimeter_Scale_Lat is delta 1.0E-7 range -90.0 .. 90.0;
   type DD_Centimeter_Scale_Lon is delta 1.0E-7 range -180.0 .. 180.0;

   --  DM Scale
   type DM_Degree_Lat is range 0 .. 90;
   type DM_Degree_Lon is range 0 .. 180;
   --  1° = 60'; each Lat minute = 1.852km / 1 Naut Mile
   type DM_Minutes is range 0 .. 60;
   --  1° = 60'; each Lat minute = 1.852km / 1 Naut Mile
   type DDM_Minutes is delta 1.0E-3 range 0.0 .. 60.000;
   --  1' = 60''; 1° = 3600''; 1'' ~ 30.9m
   type DM_Seconds is delta 1.0E-1 range 0.0 .. 60.0;

   --  Cardinal directions
   type Cardinal is (North, South, East, West);
   type Ordinal is (North_East, South_East, South_West, North_West);

   --  ------------------  --
   --  Coordinate Formats  --
   --  ------------------  --

   --  Meter precision DD coordinates
   type Format_DD is record
      Latitude  : DD_Meter_Scale_Lat;
      Longitude : DD_Meter_Scale_Lon;
   end record;

   --  Centimeter precision DD coordinates
   type Format_DD_Fine is record
      Latitude  : DD_Centimeter_Scale_Lat;
      Longitude : DD_Centimeter_Scale_Lon;
   end record;

   --  DMS
   type Format_DMS is record
      Degree_Lat   : DM_Degree_Lat;
      Degree_Lon   : DM_Degree_Lon;
      Minutes_Lat  : DM_Minutes;
      Minutes_Lon  : DM_Minutes;
      Seconds_Lat  : DM_Seconds;
      Seconds_Lon  : DM_Seconds;
      Cardinal_Lat : Cardinal;
      Cardinal_Lon : Cardinal;
   end record with
     Dynamic_Predicate =>
      Format_DMS.Cardinal_Lat in North | South
      and then Format_DMS.Cardinal_Lon in East | West;

   --  DDM
   type Format_DDM is record
      Degree_Lat   : DM_Degree_Lat;
      Degree_Lon   : DM_Degree_Lon;
      Minutes_Lat  : DDM_Minutes;
      Minutes_Lon  : DDM_Minutes;
      Cardinal_Lat : Cardinal;
      Cardinal_Lon : Cardinal;
   end record with
     Dynamic_Predicate =>
      Format_DDM.Cardinal_Lat in North | South
      and then Format_DDM.Cardinal_Lon in East | West;

     --  --------------------------  --
     --  Coordinate Type Definition  --
     --  --------------------------  --

   type Format is (Relative, DD, DD_Fine, DMS, DDM);
   type Coordinate (Form : Format := Relative) is record
      case Form is
         when Relative =>
            null;
         when DD =>
            DD : Format_DD;
         when DD_Fine =>
            DD_Fine : Format_DD_Fine;
         when DMS =>
            DMS : Format_DMS;
         when DDM =>
            DDM : Format_DDM;
      end case;
   end record;

   --  ----------------------------  --
   --  Converter / helper functions  --
   --  ----------------------------  --

   --  Converter with DD target
   --  @name      To_DD
   --  @return    Coordinate
   --  @parameter DM_Base  :  Coordinate
   --  @description Take any coordinate and return a DD formatted coordinate.
   function To_DD (DM_Base : Coordinate) return Coordinate with
     Pre =>
      (DM_Base.Form = DD) or else (DM_Base.Form = DMS)
      or else (DM_Base.Form = DDM);

end Grl.Coordinates;