nichkara/grl
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Activity

Implement type system
All checks were successful
Alire installation and checkup / build (ubuntu-20.04) (push) Successful in 45s
Details

Browse Source
This commit is contained in:
Nina Chlóe Kassandra Reiß
2026-06-10 23:45:15 +02:00
parent 56799f0c23
commit 9d98de374f
2 changed files with 136 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

24
src/grl-coordinates.adb Normal file
View File

@@ -0,0 +1,24 @@
package body Grl.Coordinates is
function To_DD (DM_Base : Coordinate) return Coordinate is
DD_Target : Coordinate (DD);
begin
case DM_Base.Form is
when Relative => null;
when DD_Fine => null;
when DD => DD_Target := DM_Base;
when DDM =>
if DM_Base.DDM.Cardinal_Lat = North then
DD_Target.DD.Latitude :=
DD_Meter_Scale_Lat (DM_Base.DDM.Degree_Lat)
+
DD_Meter_Scale_Lat (DM_Base.DDM.Minutes_Lat / 60.0);
end if;
when DMS => null;
end case;
return DD_Target;
end To_DD;
end Grl.Coordinates;

112
src/grl-coordinates.ads Normal file
View File

@@ -0,0 +1,112 @@
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;